From dcc0f646fe3c73838503b148ef1eb61408038785 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 23 Mar 2018 15:50:41 -0700 Subject: [PATCH] Add demo LLAIR client Reviewed By: mbouaziz Differential Revision: D6892205 fbshipit-source-id: cae4354 --- .gitignore | 1 + infer/src/.merlin | 1 + infer/src/Makefile | 1 + infer/src/llvm/Makefile | 28 ++++++++++++++++++++++++++++ infer/src/llvm/llvm_sil.ml | 38 ++++++++++++++++++++++++++++++++++++++ sledge/SETUP.org | 21 +++++++++++++-------- 6 files changed, 82 insertions(+), 8 deletions(-) create mode 100644 infer/src/llvm/Makefile create mode 100644 infer/src/llvm/llvm_sil.ml diff --git a/.gitignore b/.gitignore index 72b746c12..46fd96e39 100644 --- a/.gitignore +++ b/.gitignore @@ -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 diff --git a/infer/src/.merlin b/infer/src/.merlin index 228778e87..499eb37ff 100644 --- a/infer/src/.merlin +++ b/infer/src/.merlin @@ -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 diff --git a/infer/src/Makefile b/infer/src/Makefile index 56a7247b8..dbafacdc6 100644 --- a/infer/src/Makefile +++ b/infer/src/Makefile @@ -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 diff --git a/infer/src/llvm/Makefile b/infer/src/llvm/Makefile new file mode 100644 index 000000000..20511dc41 --- /dev/null +++ b/infer/src/llvm/Makefile @@ -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 diff --git a/infer/src/llvm/llvm_sil.ml b/infer/src/llvm/llvm_sil.ml new file mode 100644 index 000000000..c15055181 --- /dev/null +++ b/infer/src/llvm/llvm_sil.ml @@ -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 "-") diff --git a/sledge/SETUP.org b/sledge/SETUP.org index f0e23ec04..b337ec4dc 100644 --- a/sledge/SETUP.org +++ b/sledge/SETUP.org @@ -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 - - (add-to-list 'load-path (expand-file-name "~/path/to/sledge/llvm/utils/emacs")) - - (require 'llvm-mode) - - (require 'autodisass-llvm-bitcode) +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)