diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 8739ca57b..7b46c94c7 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -56,6 +56,8 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s [-margin ] wrap debug tracing at columns [-modules ] write list of bitcode files to , or to standard output if 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 ] 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 ] write generated LLAIR to [-margin ] wrap debug tracing at 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 ] enable debug tracing @@ -158,6 +162,8 @@ Translate one or more LLVM bitcode files to LLAIR. Each filename may be [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated LLAIR to [-margin ] wrap debug tracing at columns + [-no-models] do not add models for C/C++ runtime and standard + libraries [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index 70fea3dc1..9fa332cdd 100644 --- a/sledge/src/import/import.ml +++ b/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 diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli index af68fc744..70dea7fff 100644 --- a/sledge/src/import/import.mli +++ b/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 diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 106b002e3..1fda87aeb 100644 --- a/sledge/src/llair/frontend.ml +++ b/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 diff --git a/sledge/src/llair/frontend.mli b/sledge/src/llair/frontend.mli index 89cc9f150..0d2f59159 100644 --- a/sledge/src/llair/frontend.mli +++ b/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. *) diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 16a3a0935..a1afddf73 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -130,11 +130,16 @@ let translate = let%map_open llair_output = flag "llair-output" (optional string) ~doc:" write generated LLAIR to " + 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 diff --git a/sledge/test/Makefile b/sledge/test/Makefile index d1f7059dd..eb2b3c439 100644 --- a/sledge/test/Makefile +++ b/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: