add a owi llvm or owi bc command

doc/src/SUMMARY.md

@@ -42,6 +42,7 @@
     - [`owi fmt`](manpages/owi-fmt.md)
     - [`owi instrument`](manpages/owi-instrument.md)
     - [`owi iso`](manpages/owi-iso.md)
+    - [`owi llvm`](manpages/owi-llvm.md)
     - [`owi replay`](manpages/owi-replay.md)
     - [`owi run`](manpages/owi-run.md)
     - [`owi rust`](manpages/owi-rust.md)

doc/src/manpages/dune

@@ -10,6 +10,7 @@
   owi-fmt.md
   owi-instrument.md
   owi-iso.md
+  owi-llvm.md
   owi-replay.md
   owi-run.md
   owi-rust.md

doc/src/manpages/owi-llvm.md

@@ -0,0 +1,141 @@
+# `owi llvm`
+
+```sh
+$ owi llvm --help=plain
+NAME
+       owi-llvm - Compile LLVM IR/bitcode to Wasm and run the symbolic
+       interpreter on it
+
+SYNOPSIS
+       owi llvm [OPTION]… FILE…
+
+ARGUMENTS
+       FILE (required)
+           source files
+
+OPTIONS
+       --deterministic-result-order
+           Guarantee a fixed deterministic order of found failures. This
+           implies --no-stop-at-failure.
+
+       --entry-point=FUNCTION
+           entry point of the executable
+
+       --exploration=VALUE (absent=fifo)
+           exploration strategy to use ("fifo", "lifo", "random",
+           "random-unseen-then-random", "rarity", "hot-path-penalty",
+           "rarity-aging", "rarity-depth-aging", "rarity-depth-loop-aging",
+           "rarity-depth-loop-aging-random")
+
+       --fail-on-assertion-only
+           ignore traps and only report assertion violations
+
+       --fail-on-trap-only
+           ignore assertion violations and only report traps
+
+       --invoke-with-symbols
+           Invoke the entry point of the program with symbolic values instead
+           of dummy constants.
+
+       --model-format=VALUE (absent=scfg)
+            The format of the model ("json" or "scfg")
+
+       --model-out-file=FILE
+           Output the generated model to FILE. if --no-stop-at-failure is
+           given this is used as a prefix and the ouputed files would have
+           PREFIX_%d.
+
+       --no-assert-failure-expression-printing
+           do not display the expression in the assert failure
+
+       --no-ite-for-select
+           do not use ite for select
+
+       --no-stop-at-failure
+           do not stop when a program failure is encountered
+
+       --no-value
+           do not display a value for each symbol
+
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
+       -o FILE, --output=FILE
+           Output the generated .wasm or .wat to FILE.
+
+       -s VALUE, --solver=VALUE (absent=Z3)
+           SMT solver to use. VALUE must be one of the 6 available solvers:
+           Z3, Bitwuzla, Colibri2, cvc5, Alt-Ergo, SMTZilla
+
+       --seed=I
+           Initial seed for the PRNG state
+
+       --timeout=S
+           Stop execution after S seconds.
+
+       --timeout-instr=I
+           Stop execution after running I instructions.
+
+       -u, --unsafe
+           skip typechecking pass
+
+       -w INT, --workers=INT (absent=n)
+           Number of workers for symbolic execution. Defaults to the number
+           of physical cores.
+
+       --with-breadcrumbs
+           add breadcrumbs to the generated model
+
+       --workspace=DIR
+           write results and intermediate compilation artifacts to dir
+
+COMMON OPTIONS
+       --bench
+           enable benchmarks
+
+       --color=WHEN (absent=auto)
+           Colorize the output. WHEN must be one of auto, always or never.
+
+       --help[=FMT] (default=auto)
+           Show this help in format FMT. The value FMT must be one of auto,
+           pager, groff or plain. With auto, the format is pager or plain
+           whenever the TERM env var is dumb or undefined.
+
+       -q, --quiet
+           Be quiet. Takes over -v and --verbosity.
+
+       -v, --verbose
+           Increase verbosity. Repeatable, but more than twice does not bring
+           more.
+
+       --verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
+           Be more or less verbose. LEVEL must be one of quiet, error,
+           warning, info or debug. Takes over -v.
+
+       --version
+           Show version information.
+
+EXIT STATUS
+       owi llvm exits with:
+
+       0   on success.
+
+       123 on indiscriminate errors reported on standard error.
+
+       124 on command line parsing errors.
+
+       125 on unexpected internal errors (bugs).
+
+ENVIRONMENT
+       These environment variables affect the execution of owi llvm:
+
+       OWI_VERBOSITY
+           See option --verbosity.
+
+BUGS
+       Email them to <contact@ndrs.fr>.
+
+SEE ALSO
+       owi(1)
+
+```

doc/src/manpages/owi.md

@@ -35,6 +35,10 @@ COMMANDS
            Check the iso-functionnality of two Wasm modules by comparing the
            output when calling their exports.
 
+       llvm [OPTION]… FILE…
+           Compile LLVM IR/bitcode to Wasm and run the symbolic interpreter
+           on it
+
        replay [OPTION]… FILE
            Replay a module containing symbols with concrete values in a
            replay file containing a model

dune-project

@@ -59,7 +59,7 @@
   (bos
    (>= 0.2.1))
   (cmdliner
-   (>= 2.1.0))
+   (>= 2.1.1))
   (digestif
    (>= 1.2.0))
   (domainpc

owi.opam

@@ -31,7 +31,7 @@ depends: [
   "dune-site" {build}
   "conf-clang"
   "bos" {>= "0.2.1"}
-  "cmdliner" {>= "2.1.0"}
+  "cmdliner" {>= "2.1.1"}
   "digestif" {>= "1.2.0"}
   "domainpc" {>= "0.2"}
   "logs" {>= "0.10.0"}

src/bin/owi.ml

@@ -499,6 +499,22 @@ let iso_cmd =
     ~no_stop_at_failure ~no_value ~seed ~solver ~unsafe ~workers
     ~no_worker_isolation ~workspace ~model_out_file ~with_breadcrumbs
 
+(* owi llvm *)
+
+let llvm_info =
+  let doc =
+    "Compile LLVM IR/bitcode to Wasm and run the symbolic interpreter on it"
+  in
+  let man = [] @ shared_man in
+  Cmd.info "llvm" ~version ~doc ~sdocs ~man
+
+let llvm_cmd =
+  let+ files
+  and+ out_file
+  and+ () = setup_log
+  and+ symbolic_parameters = symbolic_parameters None in
+  Cmd_llvm.cmd ~symbolic_parameters ~files ~out_file
+
 (* owi replay *)
 
 let replay_info =
@@ -701,6 +717,7 @@ let cli =
         [ Cmd.v instrument_label_info instrument_label_cmd ]
     ; Cmd.v haskell_info haskell_cmd
     ; Cmd.v iso_info iso_cmd
+    ; Cmd.v llvm_info llvm_cmd
     ; Cmd.v replay_info replay_cmd
     ; Cmd.v run_info run_cmd
     ; Cmd.v rust_info rust_cmd

src/cmd/cmd_llvm.ml

@@ -0,0 +1,121 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+open Bos
+open Syntax
+
+let resolve_binary name =
+  match OS.Cmd.resolve @@ Cmd.v name with
+  | Error _ ->
+    Fmt.error_msg
+      "The `%s` binary was not found, please make sure it is in your path." name
+  | Ok _ as ok -> ok
+
+let err_output =
+  match Logs.Src.level Log.main_src with
+  | Some (Logs.Debug | Logs.Info) -> OS.Cmd.err_run_out
+  | None | Some _ -> OS.Cmd.err_null
+
+let bitcode_of_input ~workspace ~llvm_as_bin file : Fpath.t Result.t =
+  match Fpath.get_ext ~multi:false file with
+  | ".bc" -> Ok file
+  | ".ll" ->
+    let out_bc = Fpath.(workspace // Fpath.base (file -+ ".bc")) in
+    let llvm_as_cmd : Cmd.t = Cmd.(llvm_as_bin % p file % "-o" % p out_bc) in
+    let+ () =
+      match OS.Cmd.run ~err:err_output llvm_as_cmd with
+      | Ok _ as v -> v
+      | Error (`Msg e) ->
+        Log.debug (fun m -> m "llvm-as failed: %s" e);
+        Fmt.error_msg
+          "llvm-as failed: run with -vv to get the full error message if it \
+           was not displayed above"
+    in
+    out_bc
+  | ext ->
+    Fmt.error_msg
+      "Unsupported file extension `%s` for LLVM command, expected .ll or .bc"
+      ext
+
+let compile ~workspace ~entry_point ~out_file (files : Fpath.t list) :
+  Fpath.t Result.t =
+  let* llvm_as_bin = resolve_binary "llvm-as" in
+  let* llc_bin = resolve_binary "llc" in
+  let* wasmld_bin = resolve_binary "wasm-ld" in
+
+  let* bc_files = list_map (bitcode_of_input ~workspace ~llvm_as_bin) files in
+
+  let files_bc = Cmd.of_list (List.map Cmd.p bc_files) in
+  let llc_cmd : Cmd.t =
+    Cmd.(
+      llc_bin % "-O0" % "-march=wasm32" % "-mtriple=wasm32-unknown-unknown"
+      % "-filetype=obj" %% files_bc )
+  in
+
+  let* () =
+    Log.bench_fn "llc time" @@ fun () ->
+    match OS.Cmd.run ~err:err_output llc_cmd with
+    | Ok _ as v -> v
+    | Error (`Msg e) ->
+      Log.debug (fun m -> m "llc failed: %s" e);
+      Fmt.error_msg "llc failed: run with -vv to get the full error message"
+  in
+
+  let files_o =
+    Cmd.of_list (List.map (fun file -> Cmd.p Fpath.(file -+ ".o")) bc_files)
+  in
+
+  let out = Option.value ~default:Fpath.(workspace / "a.out.wasm") out_file in
+
+  let* libc = Cmd_utils.find_installed_c_file (Fpath.v "libc.wasm") in
+  let* libowi = Cmd_utils.find_installed_c_file (Fpath.v "libowi.wasm") in
+
+  let wasmld_cmd : Cmd.t =
+    Cmd.(
+      wasmld_bin
+      %% of_list
+           ( [ "-z"; "stack-size=8388608" ]
+           @ ( match entry_point with
+             | None -> []
+             | Some entry_point ->
+               [ Fmt.str "--export=%s" entry_point
+               ; Fmt.str "--entry=%s" entry_point
+               ] )
+           @ [ "--allow-undefined" ]
+           @ [ p libc; p libowi ]
+           @ [ "-o"; p out ] )
+      %% files_o )
+  in
+
+  let+ () =
+    Log.bench_fn "wasm-ld time" @@ fun () ->
+    match OS.Cmd.run ~err:err_output wasmld_cmd with
+    | Ok _ as v -> v
+    | Error (`Msg e) ->
+      Log.debug (fun m -> m "wasm-ld failed: %s" e);
+      Fmt.error_msg
+        "wasm-ld failed: run with -vv to get the full error message if it was \
+         not displayed above"
+  in
+
+  out
+
+let cmd ~(symbolic_parameters : Symbolic_parameters.t) ~files ~out_file :
+  unit Result.t =
+  let* workspace =
+    match symbolic_parameters.workspace with
+    | Some path -> Ok path
+    | None -> OS.Dir.tmp "owi_llvm_%s"
+  in
+  let* _did_create : bool = OS.Dir.create ~path:true workspace in
+
+  let* source_file =
+    compile ~workspace ~entry_point:symbolic_parameters.entry_point ~out_file
+      files
+  in
+  let workspace = Some workspace in
+
+  let parameters = { symbolic_parameters with workspace } in
+
+  Cmd_sym.cmd ~parameters ~source_file

src/cmd/cmd_llvm.mli

@@ -0,0 +1,9 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+val cmd :
+     symbolic_parameters:Symbolic_parameters.t
+  -> files:Fpath.t list
+  -> out_file:Fpath.t option
+  -> unit Result.t

src/dune

@@ -25,6 +25,7 @@
   cmd_haskell
   cmd_instrument_label
   cmd_iso
+  cmd_llvm
   cmd_replay
   cmd_run
   cmd_rust

src/owi.ml

@@ -12,6 +12,7 @@ module Cmd_fuzz = Cmd_fuzz
 module Cmd_haskell = Cmd_haskell
 module Cmd_instrument_label = Cmd_instrument_label
 module Cmd_iso = Cmd_iso
+module Cmd_llvm = Cmd_llvm
 module Cmd_replay = Cmd_replay
 module Cmd_run = Cmd_run
 module Cmd_rust = Cmd_rust

src/owi.mli

@@ -1755,6 +1755,14 @@ module Cmd_iso : sig
     -> unit Result.t
 end
 
+module Cmd_llvm : sig
+  val cmd :
+       symbolic_parameters:Symbolic_parameters.t
+    -> files:Fpath.t list
+    -> out_file:Fpath.t option
+    -> unit Result.t
+end
+
 module Cmd_replay : sig
   val cmd :
        unsafe:bool

test/cram/help/help.t

@@ -33,6 +33,10 @@ no subcommand should print help
              Check the iso-functionnality of two Wasm modules by comparing the
              output when calling their exports.
 
+         llvm [OPTION]… FILE…
+             Compile LLVM IR/bitcode to Wasm and run the symbolic interpreter
+             on it
+
          replay [OPTION]… FILE
              Replay a module containing symbols with concrete values in a
              replay file containing a model
@@ -93,3 +97,4 @@ no subcommand should print help
   BUGS
          Email them to <contact@ndrs.fr>.
 
+

test/cram/llvm/bad.txt

@@ -0,0 +1 @@
+not llvm