Add demo LLAIR client

Reviewed By: mbouaziz

Differential Revision: D6892205

fbshipit-source-id: cae4354
master
Josh Berdine 7 years ago committed by Facebook Github Bot
parent 446ac6d87c
commit dcc0f646fe

1
.gitignore vendored

@ -103,6 +103,7 @@ buck-out/
/infer/bin/infer-run
/infer/bin/InferCreateTraceViewLinks
/infer/bin/InferUnit
/infer/bin/llvm_sil
/infer/man
/infer/src/base/Version.ml

@ -36,6 +36,7 @@ PKG findlib.top
PKG jane-street-headers
PKG javalib
PKG lambda-term
PKG llair
PKG lwt
PKG lwt.log
PKG lwt.react

@ -283,6 +283,7 @@ clean:
# only existed in previous versions get removed as well
$(REMOVE) $(BIN_DIR)/Infer* $(BIN_DIR)/infer-* $(INFER_BIN){,.bc,.exe} $(INFER_BIN_ALIASES) \
$(INFERUNIT_BIN) $(CHECKCOPYRIGHT_BIN)
$(REMOVE) $(BIN_DIR)/llvm_sil
$(REMOVE) $(INFER_CREATE_TRACEVIEW_LINKS_BIN)
$(REMOVE) atd/*_{j,t,v}.ml{,i} atd/clang_*
$(REMOVE) mod_dep.dot

@ -0,0 +1,28 @@
# Copyright (c) 2018 - present Facebook, Inc.
# All rights reserved.
#
# This source code is licensed under the BSD style license found in the
# LICENSE file in the root directory of this source tree. An additional grant
# of patent rights can be found in the PATENTS file in the same directory.
ROOT_DIR = ../../..
include $(ROOT_DIR)/Makefile.config
INFER_BUILD_DIR = ../_build/default
default: llvm_sil
$(BIN_DIR)/llvm_sil:
rm -f $(INFER_BUILD_DIR)/llvm_sil.ml
make -C .. infer
cp llvm_sil.ml $(INFER_BUILD_DIR)
cd $(INFER_BUILD_DIR) && \
ocamlfind ocamlopt -package llair -linkpkg llvm_sil.ml -o $(BIN_DIR)/llvm_sil
rm -f $(INFER_BUILD_DIR)/llvm_sil.ml
.PHONY: llvm_sil
llvm_sil: $(BIN_DIR)/llvm_sil
.PHONY: clean
clean:
rm -f $(INFER_BUILD_DIR)/llvm_sil.ml $(BIN_DIR)/llvm_sil

@ -0,0 +1,38 @@
(*
* Copyright (c) 2018 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open Import
open Core_kernel
open Llair_
let main ~input ~output =
try
let program = Frontend.translate input in
Option.iter output ~f:(function
| "-" -> Format.printf "%a@." Llair.fmt program
| filename ->
Out_channel.with_file filename ~f:(fun oc ->
let ff = Format.formatter_of_out_channel oc in
Format.fprintf ff "%a@." Llair.fmt program ) ) ;
Format.printf "@\nRESULT: Success@."
with exn ->
let bt = Caml.Printexc.get_raw_backtrace () in
( match exn with
| Frontend.Invalid_llvm msg ->
Format.printf "@\nRESULT: Invalid input: %s@." msg
| Unimplemented msg ->
Format.printf "@\nRESULT: Unimplemented: %s@." msg
| Failure msg -> Format.printf "@\nRESULT: Internal error: %s@." msg
| _ ->
Format.printf "@\nRESULT: Unknown error: %s@."
(Caml.Printexc.to_string exn) ) ;
Caml.Printexc.raise_with_backtrace exn bt
;; main ~input:Caml.Sys.argv.(1) ~output:(Some "-")

@ -27,16 +27,21 @@
+ opam pin edit llvm
- edit llvm and conf-llvm version number to match that of the llvm clone (= 7.0.0)
- when prompted, ok to save new opam file
5. hush `ld: warning: directory not found for option '-L/opt/local/lib'`
5. install llair for llvm_sil
- cd ~/path/to/sledge
- opam pin add -n -k git llair .
+ when prompted, ok to create new package
- opam install llair
6. hush `ld: warning: directory not found for option '-L/opt/local/lib'`
- the zarith package adds a spurious linker option unless you have both brew and macports, so if you see this linker warning when compiling, execute
+ sudo mkdir -p /opt/local/lib
6. install dev tools
7. install dev tools
- opam install merlin ocp-indent tuareg user-setup
- install ocamlformat
7. if needed: point new clang to xcode c++ lib
8. if needed: point new clang to xcode c++ lib
- cd ~/.local/llvm_$(opam config var switch)/include
- ln -s /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++ .
8. llvm dev workflow
9. llvm dev workflow
- modify llvm sources
- cd ~/path/to/sledge/llvm/_build; ninja -j8
- iterate
@ -44,7 +49,7 @@
- ninja -j8 && ninja ocaml_doc && ninja install && opam upgrade llvm
- cd ~/path/to/sledge; make
- it is not uncommon to get "inconsistent assumptions" errors: clean and re-make
9. llvm emacs mode
10. llvm emacs mode
- (add-to-list 'load-path (expand-file-name "~/path/to/sledge/llvm/utils/emacs"))
- (require 'llvm-mode)
- (require 'autodisass-llvm-bitcode)

Loading…
Cancel
Save