Concolic execution

CHANGES.md

@@ -3,6 +3,7 @@
 - `owi opt` and `owi sym` can run on `.wasm` files directly
 - remove dependency on `wabt`
 - better API for `Parse`, `Compile` and `Simplified` (renamed to `Binary`), added a `Binary_to_tex` module
+- add `owi conc` subcommands and `owi c --concolic`: concolic mode
 
 ## 0.2 - 2024-04-24
 

README.md

@@ -3,12 +3,13 @@
 [Owi] is a toolchain to work with WebAssembly. It is written in [OCaml]. It provides a binary with many subcommands:
 
 - [`owi c`]: a bug finding tool for C code that performs symbolic execution by compiling to Wasm and using our symbolic Wasm interpreter;
+- [`owi conc`]: a concolic Wasm interpreter;
 - [`owi fmt`]: a formatter for Wasm;
 - [`owi opt`]: an optimizer for Wasm;
 - [`owi run`]: a concrete Wasm interpreter;
 - [`owi script`]: an interpreter for [Wasm scripts];
 - [`owi sym`]: a symbolic Wasm interpreter;
-- [`owi validate`]: a validator for Wasm modules.
+- [`owi validate`]: a validator for Wasm modules;
 - [`owi wasm2wat`]: a Wasm binary to text format translater.
 
 It also provides an [OCaml library] which allows for instance to [import OCaml functions in a Wasm module] in a type-safe way!
@@ -176,6 +177,7 @@ This project was funded through the [NGI0 Core] Fund, a fund established by [NLn
 [JS Promise Integration]: https://github.com/WebAssembly/js-promise-integration
 
 [`owi c`]: example/c
+[`owi conc`]: example/conc
 [`owi fmt`]: example/fmt
 [`owi opt`]: example/opt
 [`owi run`]: example/run

example/README.md

@@ -3,6 +3,7 @@
 ## Owi binary
 
 - [`owi c`]
+- [`owi conc`]
 - [`owi fmt`]
 - [`owi opt`]
 - [`owi run`]
@@ -30,6 +31,9 @@ COMMANDS
        c [OPTION]… [ARG]…
            Compile a C file to Wasm and run the symbolic interpreter on it
 
+       conc [OPTION]… [ARG]…
+           Run the concolic interpreter
+
        fmt [--inplace] [OPTION]… [ARG]…
            Format a .wat or .wast file
 

example/c/README.md

@@ -286,6 +286,9 @@ SYNOPSIS
        owi c [OPTION]… [ARG]…
 
 OPTIONS
+       --concolic
+           concolic mode
+
        -d, --debug
            debug mode
 

example/conc/README.md

@@ -0,0 +1,103 @@
+# Concolic interpreter
+
+## Basic example
+
+The symbolic interpreter allows to define *symbolic variables* whose values is considered to be any possible value. Then, we collect informations during the execution and when an error is reached, we try to see if there's a possible value for all the symbolic variables by taking all our informations into account.
+
+In the following file, we define `x` as a symbolic variable. Then if `5 < x`, we fail.
+
+<!-- $MDX file=mini.wat -->
+```wat
+(module
+  (import "symbolic" "i32_symbol" (func $gen_i32 (result i32)))
+
+  (func $start (local $x i32)
+    (local.set $x (call $gen_i32))
+    (if (i32.lt_s (i32.const 5) (local.get $x)) (then
+      unreachable
+    )))
+
+  (start $start)
+)
+```
+
+Let's see if owi is able to find a value for `x` that lead to an error:
+
+```sh
+$ owi conc ./mini.wat
+Trap: unreachable
+Model:
+  (model
+    (symbol_1 (i32 6)))
+```
+
+Indeed, if `x` is equal to `6` then, the `unreachable` instruction will be reached.
+
+## Man page
+
+```sh
+$ owi conc --help=plain
+NAME
+       owi-conc - Run the concolic interpreter
+
+SYNOPSIS
+       owi conc [OPTION]… [ARG]…
+
+OPTIONS
+       -d, --debug
+           debug mode
+
+       --deterministic-result-order
+           Guarantee a fixed deterministic order of found failures. This
+           implies --no-stop-at-failure.
+
+       --no-stop-at-failure
+           do not stop when a program failure is encountered
+
+       --no-value
+           do not display a value for each symbol
+
+       --optimize
+           optimize mode
+
+       -p, --profiling
+           profiling mode
+
+       -u, --unsafe
+           skip typechecking pass
+
+       -w VAL, --workers=VAL (absent=n)
+           number of workers for symbolic execution. Defaults to a
+           machine-specific value given by the OCaml
+           Domain.recommended_domain_count function.
+
+       --workspace=VAL (absent=owi-out)
+           path to the workspace directory
+
+COMMON OPTIONS
+       --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.
+
+       --version
+           Show version information.
+
+EXIT STATUS
+       owi conc 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).
+
+BUGS
+       Email them to <contact@ndrs.fr>.
+
+SEE ALSO
+       owi(1)
+
+```

example/conc/dune

@@ -0,0 +1,4 @@
+(mdx
+ (libraries owi)
+ (deps %{bin:owi} mini.wat)
+ (files README.md))

example/conc/mini.wat

@@ -0,0 +1,11 @@
+(module
+  (import "symbolic" "i32_symbol" (func $gen_i32 (result i32)))
+
+  (func $start (local $x i32)
+    (local.set $x (call $gen_i32))
+    (if (i32.lt_s (i32.const 5) (local.get $x)) (then
+      unreachable
+    )))
+
+  (start $start)
+)

src/bin/owi.ml

@@ -115,11 +115,15 @@ let c_cmd =
     let doc = "write results to dir" in
     Arg.(value & opt string "owi-out" & info [ "output"; "o" ] ~doc)
   in
+  let concolic =
+    let doc = "concolic mode" in
+    Arg.(value & flag & info [ "concolic" ] ~doc)
+  in
   Cmd.v info
     Term.(
       const Cmd_c.cmd $ debug $ arch $ property $ testcomp $ output $ workers
       $ opt_lvl $ includes $ files $ profiling $ unsafe $ optimize
-      $ no_stop_at_failure $ no_values $ deterministic_result_order )
+      $ no_stop_at_failure $ no_values $ deterministic_result_order $ concolic )
 
 let fmt_cmd =
   let open Cmdliner in
@@ -187,6 +191,19 @@ let sym_cmd =
       $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace
       $ files )
 
+let conc_cmd =
+  let open Cmdliner in
+  let info =
+    let doc = "Run the concolic interpreter" in
+    let man = [] @ shared_man in
+    Cmd.info "conc" ~version ~doc ~sdocs ~man
+  in
+  Cmd.v info
+    Term.(
+      const Cmd_conc.cmd $ profiling $ debug $ unsafe $ optimize $ workers
+      $ no_stop_at_failure $ no_values $ deterministic_result_order $ workspace
+      $ files )
+
 let wasm2wat_cmd =
   let open Cmdliner in
   let info =
@@ -217,6 +234,7 @@ let cli =
     ; run_cmd
     ; script_cmd
     ; sym_cmd
+    ; conc_cmd
     ; validate_cmd
     ; wasm2wat_cmd
     ]
@@ -273,7 +291,7 @@ let exit_code =
       | `Unexpected_token -> 40
       | `Unknown_function _id -> 41
       | `Unknown_global -> 42
-      | `Unknown_import -> 43
+      | `Unknown_import _ -> 43
       | `Unknown_label -> 44
       | `Unknown_local _id -> 45
       | `Unknown_memory _id -> 46

src/cmd/cmd_c.ml

@@ -195,7 +195,7 @@ let metadata ~workspace arch property files : unit Result.t =
 
 let cmd debug arch property testcomp workspace workers opt_lvl includes files
   profiling unsafe optimize no_stop_at_failure no_values
-  deterministic_result_order : unit Result.t =
+  deterministic_result_order concolic : unit Result.t =
   if debug then Logs.set_level (Some Debug);
   let workspace = Fpath.v workspace in
   let includes = C_share.lib_location @ includes in
@@ -213,5 +213,9 @@ let cmd debug arch property testcomp workspace workers opt_lvl includes files
   let* () = metadata ~workspace arch property files in
   let files = [ modul ] in
   let workspace = Fpath.(workspace / "test-suite") in
-  Cmd_sym.cmd profiling debug unsafe optimize workers no_stop_at_failure
-    no_values deterministic_result_order workspace files
+  if concolic then
+    Cmd_conc.cmd profiling debug unsafe optimize workers no_stop_at_failure
+      no_values deterministic_result_order workspace files
+  else
+    Cmd_sym.cmd profiling debug unsafe optimize workers no_stop_at_failure
+      no_values deterministic_result_order workspace files

src/cmd/cmd_c.mli

@@ -18,4 +18,5 @@ val cmd :
   -> bool
   -> bool
   -> bool
+  -> bool
   -> unit Result.t