diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 27de3f81a..9e2d57d0c 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -1594,10 +1594,6 @@ let read_and_parse llcontext bc_file = |> [%Trace.retn fun {pf} _ -> pf ""] -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 check_datalayout llcontext lldatalayout = let check_size llt typ = let llsiz = @@ -1643,25 +1639,13 @@ let cleanup llmodule llcontext = Llvm.dispose_module llmodule ; Llvm.dispose_context llcontext -let translate ~models ~fuzzer ~internalize : string list -> Llair.program = - fun inputs -> - [%Trace.call fun {pf} -> - pf "@ %a" (List.pp "@ " Format.pp_print_string) inputs] +let translate ~internalize : string -> Llair.program = + fun input -> + [%Trace.call fun {pf} -> pf "@ %s" input] ; Llvm.install_fatal_error_handler invalid_llvm ; let llcontext = Llvm.global_context () in - 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 ~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.get_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/cli/frontend.mli b/sledge/cli/frontend.mli index f6a55cbe5..73f2070a2 100644 --- a/sledge/cli/frontend.mli +++ b/sledge/cli/frontend.mli @@ -9,11 +9,6 @@ exception Invalid_llvm of string -val translate : - models:bool - -> fuzzer:bool - -> internalize:bool - -> string list - -> Llair.program +val translate : internalize:bool -> string -> Llair.program (** 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/cli/sledge_buck.ml b/sledge/cli/sledge_buck.ml index cdfc60295..b46cf4dba 100644 --- a/sledge/cli/sledge_buck.ml +++ b/sledge/cli/sledge_buck.ml @@ -149,10 +149,7 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules = let modules = if fuzzer then "-" :: modules else modules in let open Process in eval ~context - ( ( if fuzzer then - echo ~n:() (Option.get_exn (Model.read "/lib_fuzzer_main.bc")) - else return () ) - |- run (Lazy.force llvm_bin ^ "llvm-link") ("-o=-" :: modules) + ( run (Lazy.force llvm_bin ^ "llvm-link") ("-o=-" :: modules) |- run (Lazy.force llvm_bin ^ "opt") [ "-o=" ^ bitcode_output @@ -184,13 +181,12 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules = module Command = Core.Command open Command.Let_syntax -let ( |*> ) a' f' = a' |> Command.Param.apply f' let ( |**> ) = Command.Param.map2 ~f:(fun a f b -> f b a) let abs_path_arg = Command.Param.(Arg_type.map string ~f:(make_absolute cwd)) -let main ~(command : Report.status Command.basic_command) ~analyze = +let main ~(command : Report.status Command.basic_command) = let bitcode_inputs = let%map_open target = anon ("" %: string) and modules = @@ -217,16 +213,6 @@ let main ~(command : Report.status Command.basic_command) ~analyze = let param = bitcode_inputs >>| fun _ () -> Report.Ok in command ~summary ~readme param in - let analyze_cmd = - let summary = "analyze buck target" in - let readme () = - "Analyze code in a buck target. This is a convenience wrapper for \ - the sequence `sledge buck bitcode`; `sledge llvm translate`; \ - `sledge analyze`." - in - let param = bitcode_inputs |*> analyze in - command ~summary ~readme param - in let link_cmd = let summary = "link buck target to LLVM bitcode" in let readme () = @@ -255,4 +241,4 @@ let main ~(command : Report.status Command.basic_command) ~analyze = which can be used to configure buck targets for sledge." in Command.group ~summary ~readme ~preserve_subcommand_order:() - [("analyze", analyze_cmd); ("bitcode", bitcode_cmd); ("link", link_cmd)] + [("bitcode", bitcode_cmd); ("link", link_cmd)] diff --git a/sledge/cli/sledge_buck.mli b/sledge/cli/sledge_buck.mli index e44ff0ace..2fcc55aed 100644 --- a/sledge/cli/sledge_buck.mli +++ b/sledge/cli/sledge_buck.mli @@ -7,7 +7,4 @@ open Core -val main : - command:Report.status Command.basic_command - -> analyze:(string list -> unit -> Report.status) Command.Param.t - -> Command.t +val main : command:Report.status Command.basic_command -> Command.t diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index 63198d09b..90ba39d20 100644 --- a/sledge/cli/sledge_cli.ml +++ b/sledge/cli/sledge_cli.ml @@ -190,38 +190,22 @@ let translate = let%map_open output = flag "output" (optional string) ~doc:" write generated binary 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" and no_internalize = flag "no-internalize" no_arg ~doc: "do not internalize all functions except the entry points \ specified in the config file" in - fun bitcode_inputs () -> + fun bitcode_input () -> let program = - Frontend.translate ~models:(not no_models) ~fuzzer - ~internalize:(not no_internalize) bitcode_inputs + Frontend.translate ~internalize:(not no_internalize) bitcode_input in Option.iter ~f:(marshal program) output ; program let llvm_grp = - let translate_inputs = - let expand_argsfile input = - if Char.equal input.[0] '@' then - In_channel.with_file ~f:In_channel.input_lines (String.drop 1 input) - else [input] - in - let open Command.Param in - let input_arg = Arg_type.map string ~f:expand_argsfile in - anon - (map_anons ~f:List.concat - (non_empty_sequence_as_list ("" %: input_arg))) - |*> translate + let translate_input = + Command.Param.(anon ("" %: string) |*> translate) in let translate_cmd = let summary = "translate LLVM bitcode to LLAIR" in @@ -232,7 +216,7 @@ let llvm_grp = names a file containing one per line." in let param = - translate_inputs >*> Command.Param.return (fun _ -> Report.Ok) + translate_input >*> Command.Param.return (fun _ -> Report.Ok) in command ~summary ~readme param in @@ -241,7 +225,7 @@ let llvm_grp = "translate LLVM bitcode to LLAIR and print in textual form" in let readme () = "The file must be LLVM bitcode." in - let param = translate_inputs |*> disassemble in + let param = translate_input |*> disassemble in command ~summary ~readme param in let analyze_cmd = @@ -251,7 +235,7 @@ let llvm_grp = convenience wrapper for the sequence `sledge llvm translate`; \ `sledge analyze`." in - let param = translate_inputs |*> analyze in + let param = translate_input |*> analyze in command ~summary ~readme param in let summary = "integration with LLVM" in @@ -291,7 +275,7 @@ Stdlib.Sys.catch_break true ;; Command.run ~version:Version.version ~build_info:Version.build_info (Command.group ~summary ~readme ~preserve_subcommand_order:() - [ ("buck", Sledge_buck.main ~command ~analyze:(translate >*> analyze)) + [ ("buck", Sledge_buck.main ~command) ; ("llvm", llvm_grp) ; ("analyze", analyze_cmd) ; ("disassemble", disassemble_cmd) diff --git a/sledge/dune b/sledge/dune index 26dce5bbc..5af7949cb 100644 --- a/sledge/dune +++ b/sledge/dune @@ -93,27 +93,6 @@ (pps ppx_sledge ppx_trace)) (inline_tests))) -(subdir - model - (rule - (targets cxxabi.bc) - (deps cxxabi.cpp Makefile llair_intrinsics.h) - (action - (run make ROOT=../../.. cxxabi.bc))) - (rule - (targets lib_fuzzer_main.bc) - (deps lib_fuzzer_main.c Makefile) - (action - (run make ROOT=../../.. lib_fuzzer_main.bc))) - (rule - (targets model.ml) - (deps cxxabi.bc lib_fuzzer_main.bc) - (action - (run ocaml-crunch -m plain -e bc -o model.ml .))) - (library - (name model) - (public_name sledge.model))) - (subdir cli (executable @@ -122,10 +101,9 @@ (package sledge) (libraries apron apron.boxMPQ core ctypes ctypes.foreign dune-build-info llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo - llvm.linker shexp.process yojson trace nonstdlib sledge model - smtlib-utils) + llvm.linker shexp.process yojson trace nonstdlib sledge smtlib-utils) (flags - (:standard -w -58 -open NS -open Sledge -open Model)) + (:standard -w -58 -open NS -open Sledge)) (preprocess (pps ppx_sledge ppx_trace)))) diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 0349a83e6..572265648 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -7,7 +7,6 @@ The [-trace ] argument of each subcommand enables debug tracing according === subcommands === buck integration with Buck - . analyze analyze buck target . bitcode report bitcode files in buck target . link link buck target to LLVM bitcode llvm integration with LLVM @@ -31,49 +30,11 @@ Code can be provided by a buck build target, such as //fully/qualified/build:tar === subcommands === - analyze analyze buck target bitcode report bitcode files in buck target link link buck target to LLVM bitcode help explain a given subcommand (perhaps recursively) -====== sledge buck analyze ====== - -analyze buck target - - sledge buck analyze - -Analyze code in a buck target. This is a convenience wrapper for the sequence `sledge buck bitcode`; `sledge llvm translate`; `sledge analyze`. - -=== flags === - - [-append-report] append to report file - [-bound ] stop execution exploration at depth - [-colors] enable printing in colors - [-domain ] select abstract domain; must be one of "sh" (default, - symbolic heap domain), "globals" (used-globals domain), - or "unit" (unit domain) - [-dump-query ] dump solver query and halt - [-function-summaries] use function summaries (in development) - [-fuzzer] add a harness for libFuzzer targets - [-margin ] wrap debug tracing at columns - [-modules ] write list of bitcode files to , or to standard - output if is `-` - [-no-internalize] do not internalize all functions except the entry - points specified in the config file - [-no-models] do not add models for C/C++ runtime and standard - libraries - [-no-simplify-states] do not simplify states during symbolic execution - [-output ] write generated binary LLAIR to - [-preanalyze-globals] pre-analyze global variables used by each function - [-report ] write report sexp to , or to standard error if - "-" - [-stats] output performance statistics to stderr - [-trace ] enable debug tracing - [-help] print this help text and exit - (alias: -?) - - ====== sledge buck bitcode ====== report bitcode files in buck target @@ -139,7 +100,7 @@ Code can be provided by one or more LLVM bitcode files. analyze LLVM bitcode - sledge llvm analyze [ ...] + sledge llvm analyze Analyze code in one or more LLVM bitcode files. This is a convenience wrapper for the sequence `sledge llvm translate`; `sledge analyze`. @@ -153,12 +114,9 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo or "unit" (unit domain) [-dump-query ] dump solver query and halt [-function-summaries] use function summaries (in development) - [-fuzzer] add a harness for libFuzzer targets [-margin ] wrap debug tracing at columns [-no-internalize] do not internalize all functions except the entry points specified in the config file - [-no-models] do not add models for C/C++ runtime and standard - libraries [-no-simplify-states] do not simplify states during symbolic execution [-output ] write generated binary LLAIR to [-preanalyze-globals] pre-analyze global variables used by each function @@ -174,7 +132,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo translate LLVM bitcode to LLAIR - sledge llvm translate [ ...] + sledge llvm translate Translate one or more LLVM bitcode files to LLAIR. Each filename may be either: an LLVM bitcode file, in binary (.bc) or textual (.ll) form; or of the form @, where names a file containing one per line. @@ -182,11 +140,9 @@ Translate one or more LLVM bitcode files to LLAIR. Each filename may be [-append-report] append to report file [-colors] enable printing in colors - [-fuzzer] add a harness for libFuzzer targets [-margin ] wrap debug tracing at columns [-no-internalize] do not internalize all functions except the entry points specified in the config file - [-no-models] do not add models for C/C++ runtime and standard libraries [-output ] write generated binary LLAIR to [-report ] write report sexp to , or to standard error if "-" [-trace ] enable debug tracing @@ -198,7 +154,7 @@ Translate one or more LLVM bitcode files to LLAIR. Each filename may be translate LLVM bitcode to LLAIR and print in textual form - sledge llvm disassemble [ ...] + sledge llvm disassemble The file must be LLVM bitcode. @@ -206,14 +162,11 @@ The file must be LLVM bitcode. [-append-report] append to report file [-colors] enable printing in colors - [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated textual LLAIR to , or to standard output if omitted [-margin ] wrap debug tracing at columns [-no-internalize] do not internalize all functions except the entry points specified in the config file - [-no-models] do not add models for C/C++ runtime and standard - libraries [-output ] write generated binary LLAIR to [-report ] write report sexp to , or to standard error if "-" diff --git a/sledge/sledge.opam b/sledge/sledge.opam index cbfc43dd9..153d9c9ec 100644 --- a/sledge/sledge.opam +++ b/sledge/sledge.opam @@ -15,7 +15,6 @@ depends: [ "containers" "containers-data" "core" {>= "v0.14"} - "crunch" {build} "ctypes" "ctypes-foreign" "dune" {build & >= "2.7"} diff --git a/sledge/test/Makefile b/sledge/test/Makefile index fae61d41b..d9446d99d 100644 --- a/sledge/test/Makefile +++ b/sledge/test/Makefile @@ -189,7 +189,7 @@ smt-status: smt.sexp sledge_report_exe # run sledge llvm translate tests .PHONY: llvm llvm: - -find -L llvm -name '*.ll' -or -name '*.bc' 2>/dev/null | parallel --bar $(sledge_dbg) llvm translate -no-models -no-internalize $(SLEDGE_T_ARGS) + -find -L llvm -name '*.ll' -or -name '*.bc' 2>/dev/null | parallel --bar $(sledge_dbg) llvm translate -no-internalize $(SLEDGE_T_ARGS) .PHONY: llvm.sexp llvm.sexp: