diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index e783837b1..63a00e255 100644 --- a/doc/src/SUMMARY.md +++ b/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) diff --git a/doc/src/manpages/dune b/doc/src/manpages/dune index 4d6542a62..4ac136953 100644 --- a/doc/src/manpages/dune +++ b/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 diff --git a/doc/src/manpages/owi-llvm.md b/doc/src/manpages/owi-llvm.md new file mode 100644 index 000000000..da1ea031b --- /dev/null +++ b/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 . + +SEE ALSO + owi(1) + +``` diff --git a/doc/src/manpages/owi.md b/doc/src/manpages/owi.md index d5939b369..87f7bcaa8 100644 --- a/doc/src/manpages/owi.md +++ b/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 diff --git a/dune-project b/dune-project index 90849931f..1c16775e9 100644 --- a/dune-project +++ b/dune-project @@ -59,7 +59,7 @@ (bos (>= 0.2.1)) (cmdliner - (>= 2.1.0)) + (>= 2.1.1)) (digestif (>= 1.2.0)) (domainpc diff --git a/owi.opam b/owi.opam index dd6218b30..13258b6a3 100644 --- a/owi.opam +++ b/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"} diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 3f3a8a76a..699ca21b2 100644 --- a/src/bin/owi.ml +++ b/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 diff --git a/src/cmd/cmd_llvm.ml b/src/cmd/cmd_llvm.ml new file mode 100644 index 000000000..4a8c1276e --- /dev/null +++ b/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 diff --git a/src/cmd/cmd_llvm.mli b/src/cmd/cmd_llvm.mli new file mode 100644 index 000000000..e95076f63 --- /dev/null +++ b/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 diff --git a/src/dune b/src/dune index de33545ff..a3b07b15c 100644 --- a/src/dune +++ b/src/dune @@ -25,6 +25,7 @@ cmd_haskell cmd_instrument_label cmd_iso + cmd_llvm cmd_replay cmd_run cmd_rust diff --git a/src/owi.ml b/src/owi.ml index f27fb4221..f0f88fd1a 100644 --- a/src/owi.ml +++ b/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 diff --git a/src/owi.mli b/src/owi.mli index 7340a6334..6a5e87b53 100644 --- a/src/owi.mli +++ b/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 diff --git a/test/cram/help/help.t b/test/cram/help/help.t index 3eaf27674..b73a7718e 100644 --- a/test/cram/help/help.t +++ b/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 . + diff --git a/test/cram/llvm/bad.txt b/test/cram/llvm/bad.txt new file mode 100644 index 000000000..df441fe02 --- /dev/null +++ b/test/cram/llvm/bad.txt @@ -0,0 +1 @@ +not llvm diff --git a/test/cram/llvm/dune b/test/cram/llvm/dune new file mode 100644 index 000000000..50f102aa8 --- /dev/null +++ b/test/cram/llvm/dune @@ -0,0 +1,9 @@ +(cram + (deps + %{bin:owi} + bad.txt + simple.ll + simple.bc + trap_div_zero.ll + trap_div_zero.bc) + (alias quicktest)) diff --git a/test/cram/llvm/empty.t b/test/cram/llvm/empty.t new file mode 100644 index 000000000..53988fba1 --- /dev/null +++ b/test/cram/llvm/empty.t @@ -0,0 +1,4 @@ + $ owi llvm + Usage: owi llvm [--help] [OPTION]… FILE… + owi: required argument FILE is missing + [124] diff --git a/test/cram/llvm/not_exists.t b/test/cram/llvm/not_exists.t new file mode 100644 index 000000000..d2d7e0744 --- /dev/null +++ b/test/cram/llvm/not_exists.t @@ -0,0 +1,4 @@ + $ owi llvm not_exists.bc + Usage: owi llvm [--help] [OPTION]… FILE… + owi: FILE… arguments: no file 'not_exists.bc' + [124] diff --git a/test/cram/llvm/simple.bc b/test/cram/llvm/simple.bc new file mode 100644 index 000000000..5f4e73b87 Binary files /dev/null and b/test/cram/llvm/simple.bc differ diff --git a/test/cram/llvm/simple.ll b/test/cram/llvm/simple.ll new file mode 100644 index 000000000..6266b98be --- /dev/null +++ b/test/cram/llvm/simple.ll @@ -0,0 +1,4 @@ +define i32 @main() { +entry: + ret i32 0 +} diff --git a/test/cram/llvm/simple.t b/test/cram/llvm/simple.t new file mode 100644 index 000000000..b1cb21e75 --- /dev/null +++ b/test/cram/llvm/simple.t @@ -0,0 +1,6 @@ +simple.bc and simple.ll cramtests : + $ owi llvm simple.ll --entry-point=main --no-value + All OK! + + $ owi llvm simple.bc --entry-point=main --no-value + All OK! diff --git a/test/cram/llvm/trap_div_zero.bc b/test/cram/llvm/trap_div_zero.bc new file mode 100644 index 000000000..b15ac3947 Binary files /dev/null and b/test/cram/llvm/trap_div_zero.bc differ diff --git a/test/cram/llvm/trap_div_zero.ll b/test/cram/llvm/trap_div_zero.ll new file mode 100644 index 000000000..c7f5ad34b --- /dev/null +++ b/test/cram/llvm/trap_div_zero.ll @@ -0,0 +1,5 @@ +define i32 @main() { +entry: + %x = sdiv i32 1, 0 + ret i32 %x +} diff --git a/test/cram/llvm/trap_div_zero.t b/test/cram/llvm/trap_div_zero.t new file mode 100644 index 000000000..5a0859030 --- /dev/null +++ b/test/cram/llvm/trap_div_zero.t @@ -0,0 +1,12 @@ +trap_div_zero: + $ owi llvm trap_div_zero.ll --entry-point=main --no-value + owi: [ERROR] Trap: integer divide by zero + model + owi: [ERROR] Reached problem! + [13] + + $ owi llvm trap_div_zero.bc --entry-point=main --no-value + owi: [ERROR] Trap: integer divide by zero + model + owi: [ERROR] Reached problem! + [13] diff --git a/test/cram/llvm/unsupported_ext.t b/test/cram/llvm/unsupported_ext.t new file mode 100644 index 000000000..59d26d80d --- /dev/null +++ b/test/cram/llvm/unsupported_ext.t @@ -0,0 +1,3 @@ + $ owi llvm bad.txt + owi: [ERROR] Unsupported file extension `.txt` for LLVM command, expected .ll or .bc + [26]