[sledge] Remove functionality depending on Llvm_linker.link_in

Summary:
This allows using the upsteam LLVM 11 library unchanged, only
extensions to the OCaml bindings are needed. Therefore this is to
enable building sledge using e.g. `dnf install llvm-11` or `brew
install llvm@11` instead of cloning and building a fork of llvm.

Reviewed By: jvillard

Differential Revision: D27188301

fbshipit-source-id: f441dbecd

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 =
+let translate ~internalize : string -> Llair.program =
- fun inputs ->
+ fun input ->
-  [%Trace.call fun {pf} ->
+  [%Trace.call fun {pf} -> pf "@ %s" input]
-    pf "@ %a" (List.pp "@ " Format.pp_print_string) inputs]
   ;
   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
   ) ;

sledge/cli/frontend.mli

@@ -9,11 +9,6 @@
 
 exception Invalid_llvm of string
 
-val translate :
+val translate : internalize:bool -> string -> Llair.program
-     models:bool
-  -> fuzzer:bool
-  -> internalize:bool
-  -> string list
-  -> 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. *)

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
+    ( run (Lazy.force llvm_bin ^ "llvm-link") ("-o=-" :: modules)
-        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 ^ "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 ("<target>" %: 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)]

sledge/cli/sledge_buck.mli

@@ -7,7 +7,4 @@
 
 open Core
 
-val main :
+val main : command:Report.status Command.basic_command -> Command.t
-     command:Report.status Command.basic_command
-  -> analyze:(string list -> unit -> Report.status) Command.Param.t
-  -> Command.t

sledge/cli/sledge_cli.ml

@@ -190,38 +190,22 @@ let translate =
   let%map_open output =
     flag "output" (optional string)
       ~doc:"<file> write generated binary 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"
   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
+      Frontend.translate ~internalize:(not no_internalize) bitcode_input
-        ~internalize:(not no_internalize) bitcode_inputs
     in
     Option.iter ~f:(marshal program) output ;
     program
 
 let llvm_grp =
-  let translate_inputs =
+  let translate_input =
-    let expand_argsfile input =
+    Command.Param.(anon ("<input>" %: string) |*> translate)
-      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>" %: input_arg)))
-    |*> 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 <input> 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 <input> 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)

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
+    llvm.linker shexp.process yojson trace nonstdlib sledge smtlib-utils)
-    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))))
 

sledge/sledge-help.txt

@@ -7,7 +7,6 @@ The [-trace <spec>] 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 <target>
-
-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 <int>]         stop execution exploration at depth <int>
-  [-colors]              enable printing in colors
-  [-domain <string>]     select abstract domain; must be one of "sh" (default,
-                         symbolic heap domain), "globals" (used-globals domain),
-                         or "unit" (unit domain)
-  [-dump-query <int>]    dump solver query <int> and halt
-  [-function-summaries]  use function summaries (in development)
-  [-fuzzer]              add a harness for libFuzzer targets
-  [-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-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 <file>]       write generated binary LLAIR to <file>
-  [-preanalyze-globals]  pre-analyze global variables used by each function
-  [-report <file>]       write report sexp to <file>, or to standard error if
-                         "-"
-  [-stats]               output performance statistics to stderr
-  [-trace <spec>]        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 <input> [<input> ...]
+  sledge llvm analyze <input>
 
 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 <int>]    dump solver query <int> and halt
   [-function-summaries]  use function summaries (in development)
-  [-fuzzer]              add a harness for libFuzzer targets
   [-margin <cols>]       wrap debug tracing at <cols> 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 <file>]       write generated binary LLAIR to <file>
   [-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 <input> [<input> ...]
+  sledge llvm translate <input>
 
 Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be either: an LLVM bitcode file, in binary (.bc) or textual (.ll) form; or of the form @<argsfile>, where <argsfile> names a file containing one <input> per line.
 
@@ -182,11 +140,9 @@ Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be
 
   [-append-report]   append to report file
   [-colors]          enable printing in colors
-  [-fuzzer]          add a harness for libFuzzer targets
   [-margin <cols>]   wrap debug tracing at <cols> 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 <file>]   write generated binary LLAIR to <file>
   [-report <file>]   write report sexp to <file>, or to standard error if "-"
   [-trace <spec>]    enable debug tracing
@@ -198,7 +154,7 @@ Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be
 
 translate LLVM bitcode to LLAIR and print in textual form
 
-  sledge llvm disassemble <input> [<input> ...]
+  sledge llvm disassemble <input>
 
 The <input> file must be LLVM bitcode.
 
@@ -206,14 +162,11 @@ The <input> 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 <file>]  write generated textual LLAIR to <file>, or to
                           standard output if omitted
   [-margin <cols>]        wrap debug tracing at <cols> 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 <file>]        write generated binary LLAIR to <file>
   [-report <file>]        write report sexp to <file>, or to standard error if
                           "-"

sledge/sledge.opam

@@ -15,7 +15,6 @@ depends: [
   "containers"
   "containers-data"
   "core" {>= "v0.14"}
-  "crunch" {build}
   "ctypes"
   "ctypes-foreign"
   "dune" {build & >= "2.7"}

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: