[sledge] Add flag to disable linking in the models

Summary:
Sometimes the models for the C/C++ runtime and standard libraries are
not needed. Furthermore, sometimes, e.g. when analyzing llvm tests,
trying to link them fails.

Reviewed By: bennostein

Differential Revision: D17725616

fbshipit-source-id: 76a4bcf90

sledge/sledge-help.txt

@@ -56,6 +56,8 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
   [-margin <cols>]        wrap debug tracing at <cols> columns
   [-modules <file>]       write list of bitcode files to <file>, or to standard
                           output if <file> is `-`
+  [-no-models]            do not add models for C/C++ runtime and standard
+                          libraries
   [-preanalyze-globals]   pre-analyze global variables used by each function
   [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
@@ -137,6 +139,8 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
   [-margin <cols>]        wrap debug tracing at <cols> columns
+  [-no-models]            do not add models for C/C++ runtime and standard
+                          libraries
   [-preanalyze-globals]   pre-analyze global variables used by each function
   [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
@@ -158,6 +162,8 @@ Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
   [-margin <cols>]        wrap debug tracing at <cols> columns
+  [-no-models]            do not add models for C/C++ runtime and standard
+                          libraries
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
                           (alias: -?)

sledge/src/import/import.ml

@@ -160,6 +160,8 @@ module List = struct
         | xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ;
         Option.iter suf ~f:(Format.fprintf fs)
 
+  let pop_exn = function x :: xs -> (x, xs) | [] -> raise Caml.Not_found
+
   let find_map_remove xs ~f =
     let rec find_map_remove_ ys = function
       | [] -> None

sledge/src/import/import.mli

@@ -132,6 +132,8 @@ module List : sig
     -> 'a list pp
   (** Pretty-print a list. *)
 
+  val pop_exn : 'a list -> 'a * 'a list
+
   val find_map_remove :
     'a list -> f:('a -> 'b option) -> ('b * 'a list) option
 

sledge/src/llair/frontend.ml

@@ -1333,45 +1333,40 @@ let transform : Llvm.llmodule -> unit =
   Llvm.PassManager.run_module llmodule pm |> (ignore : bool -> _) ;
   Llvm.PassManager.dispose pm
 
-let link_in : Llvm.llcontext -> Llvm.lllinker -> string -> unit =
- fun llcontext link_ctx bc_file ->
+let read_and_parse llcontext bc_file =
   [%Trace.call fun {pf} -> pf "%s" bc_file]
   ;
-  let read_and_parse bc_file =
-    let llmemorybuffer =
-      try Llvm.MemoryBuffer.of_file bc_file
-      with Llvm.IoError msg -> fail "%s: %s" bc_file msg ()
-    in
-    try Llvm_irreader.parse_ir llcontext llmemorybuffer
-    with Llvm_irreader.Error msg -> invalid_llvm msg
+  let llmemorybuffer =
+    try Llvm.MemoryBuffer.of_file bc_file
+    with Llvm.IoError msg -> fail "%s: %s" bc_file msg ()
   in
-  Llvm_linker.link_in link_ctx (read_and_parse bc_file)
+  ( try Llvm_irreader.parse_ir llcontext llmemorybuffer
+    with Llvm_irreader.Error msg -> invalid_llvm msg )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let translate ~fuzzer : string list -> Llair.t =
+let link_in : Llvm.llcontext -> Llvm.lllinker -> string -> unit =
+ fun llcontext link_ctx bc_file ->
+  Llvm_linker.link_in link_ctx (read_and_parse llcontext bc_file)
+
+let translate ~models ~fuzzer : string list -> Llair.t =
  fun inputs ->
   [%Trace.call fun {pf} ->
     pf "%a" (List.pp "@ " Format.pp_print_string) inputs]
   ;
   Llvm.install_fatal_error_handler invalid_llvm ;
   let llcontext = Llvm.global_context () in
-  let llmodule =
-    let model_memorybuffer =
-      Llvm.MemoryBuffer.of_string
-        (Option.value_exn (Model.read "/cxxabi.bc"))
-    in
-    Llvm_irreader.parse_ir llcontext model_memorybuffer
-  in
-  ( if fuzzer then
-    let lib_fuzzer_memorybuffer =
-      Llvm.MemoryBuffer.of_string
-        (Option.value_exn (Model.read "/lib_fuzzer_main.bc"))
-    in
-    Llvm_linker.link_modules' llmodule
-      (Llvm_irreader.parse_ir llcontext lib_fuzzer_memorybuffer) ) ;
+  let input, inputs = List.pop_exn inputs in
+  let llmodule = read_and_parse llcontext input in
   let link_ctx = Llvm_linker.get_linker llmodule in
-  List.iter inputs ~f:(link_in llcontext link_ctx) ;
+  List.iter ~f:(link_in llcontext link_ctx) inputs ;
+  let link_model_file name =
+    Llvm_linker.link_in link_ctx
+      (Llvm_irreader.parse_ir llcontext
+         (Llvm.MemoryBuffer.of_string (Option.value_exn (Model.read name))))
+  in
+  if models then link_model_file "/cxxabi.bc" ;
+  if fuzzer then link_model_file "/lib_fuzzer_main.bc" ;
   Llvm_linker.linker_dispose link_ctx ;
   assert (
     Llvm_analysis.verify_module llmodule |> Option.for_all ~f:invalid_llvm

sledge/src/llair/frontend.mli

@@ -9,6 +9,6 @@
 
 exception Invalid_llvm of string
 
-val translate : fuzzer:bool -> string list -> Llair.t
+val translate : models:bool -> fuzzer:bool -> string list -> Llair.t
 (** Translate the compilation units in the named (llvm or bitcode) files to
     LLAIR. Attempts to raise [Invalid_llvm] when the input is invalid LLVM. *)

sledge/src/sledge.ml

@@ -130,11 +130,16 @@ let translate =
   let%map_open llair_output =
     flag "llair-output" (optional string)
       ~doc:"<file> write generated LLAIR to <file>"
+  and no_models =
+    flag "no-models" no_arg
+      ~doc:"do not add models for C/C++ runtime and standard libraries"
   and fuzzer =
     flag "fuzzer" no_arg ~doc:"add a harness for libFuzzer targets"
   in
   fun bitcode_inputs () ->
-    let program = Frontend.translate ~fuzzer bitcode_inputs in
+    let program =
+      Frontend.translate ~models:(not no_models) ~fuzzer bitcode_inputs
+    in
     Option.iter ~f:(marshal program) llair_output ;
     program
 

sledge/test/Makefile

@@ -7,7 +7,7 @@
 CLANG_ARGS?=-O0
 
 # executable to test
-SLEDGE_EXE=$(CURDIR)/../_build/dev/src/sledge.exe
+SLEDGE_EXE=$(CURDIR)/../_build/_install/dbg/bin/sledge
 
 # additional arguments to pass to sledge
 SLEDGE_ARGS?=
@@ -28,7 +28,7 @@ default: test
 # all analyze tests
 translate:
 	@find -L llvm -name '*.ll' -or -name '*.bc' \
-	 | parallel --bar $(SLEDGE) llvm translate $(SLEDGE_ARGS)
+	 | parallel --bar $(SLEDGE) llvm translate -no-models $(SLEDGE_ARGS)
 
 _translate-report-raw:
 	@find -L llvm -name '*.out' \
@@ -79,10 +79,10 @@ analyze: compile
 # run all tests and generate code coverage information
 BISECT_DIR=$(CURDIR)/../_coverage/out
 coverage:
-	@cd ..; dune build _build/coverage/src/sledge.exe
+	@cd ..; dune build _build/_install/coverage/bin/sledge
 	@mkdir -p $(BISECT_DIR)
-	@-$(MAKE) BISECT_FILE=$(BISECT_DIR)/bisect SLEDGE_EXE=$(CURDIR)/../_build/coverage/src/sledge.exe test -k
-	@find $(BISECT_DIR) -type f | xargs bisect-ppx-report -I ../_build/coverage/ -text ../_coverage/summary.txt -html ../_coverage/
+	@-$(MAKE) BISECT_FILE=$(BISECT_DIR)/bisect SLEDGE_EXE=$(CURDIR)/../_build/_install/coverage/bin/sledge test -k
+	@find $(BISECT_DIR) -type f | xargs bisect-ppx-report -I ../_build/_install/coverage/ -text ../_coverage/summary.txt -html ../_coverage/
 	@echo "open ../_coverage/index.html"
 
 _analyze-report-raw: