add owi replay

CHANGES.md

@@ -1,5 +1,6 @@
 ## unreleased
 
+- add `owi replay` command to check a model produced by symbolic execution on a concrete execution
 - add `owi instrument` to instrument Webassembly module annotated by Weasel specification language
 - add `--srac` option to `sym` and `conc` cmd
 - add `--rac` option to `run`, `sym` and `conc` cmd

README.md

@@ -6,6 +6,7 @@
 - [`owi conc`]: a concolic Wasm interpreter;
 - [`owi fmt`]: a formatter for Wasm;
 - [`owi opt`]: an optimizer for Wasm;
+- [`owi replay`]: run a module containing symbols with concrete values from a model produced by a previous symbolic execution
 - [`owi run`]: a concrete Wasm interpreter;
 - [`owi script`]: an interpreter for [Wasm scripts];
 - [`owi sym`]: a symbolic Wasm interpreter;
@@ -214,6 +215,7 @@ This project was partly funded through the [NGI0 Core] Fund, a fund established
 [`owi conc`]: example/conc
 [`owi fmt`]: example/fmt
 [`owi opt`]: example/opt
+[`owi replay`]: example/replay
 [`owi run`]: example/run
 [`owi script`]: example/script
 [`owi sym`]: example/sym

example/README.md

@@ -45,6 +45,10 @@ COMMANDS
        opt [--debug] [--output=FILE] [--unsafe] [OPTION]… ARG
            Optimize a module
 
+       replay [OPTION]… ARG
+           Replay a module containing symbols with concrete values in a
+           replay file containing a model
+
        run [OPTION]… [ARG]…
            Run the concrete interpreter
 

example/replay/README.md

@@ -0,0 +1,91 @@
+# Symbolic interpreter
+
+## Basic example
+
+First, you need to perform a symbolic run and to store the output model in a file. Given the following `mini.wat` file containing symbols:
+
+<!-- $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)
+)
+```
+
+You can get a model like this:
+
+```sh
+$ owi sym ./mini.wat > mini.model
+Reached problem!
+[13]
+```
+
+Then you can replay the module execution with the values in the model like this:
+
+```sh
+$ owi replay --replay-file mini.model mini.wat
+invalid model: can not find the directive `model` while parsing the scfg config
+[78]
+```
+
+## Man page
+
+```sh
+$ owi replay --help=plain
+NAME
+       owi-replay - Replay a module containing symbols with concrete values
+       in a replay file containing a model
+
+SYNOPSIS
+       owi replay [OPTION]… ARG
+
+OPTIONS
+       -d, --debug
+           debug mode
+
+       --optimize
+           optimize mode
+
+       -p, --profiling
+           profiling mode
+
+       --replay-file=VAL (required)
+           Which replay file to use
+
+       -u, --unsafe
+           skip typechecking pass
+
+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 replay 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 <[email protected]>.
+
+SEE ALSO
+       owi(1)
+
+```

example/replay/dune

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

example/replay/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

@@ -41,8 +41,21 @@ let files =
 
 let sourcefile =
   let doc = "source file" in
-  let f = existing_non_dir_file in
-  Cmdliner.Arg.(required & pos 0 (some f) None (info [] ~doc))
+  Cmdliner.Arg.(
+    required & pos 0 (some existing_non_dir_file) None (info [] ~doc) )
+
+let replay_file =
+  let parse s =
+    let path = Fpath.v s in
+    match Bos.OS.File.exists path with
+    | Ok true -> Ok path
+    | Ok false -> Error (`Msg (Fmt.str "no file '%a'" Fpath.pp path))
+    | Error _e as e -> e
+  in
+  let replay_file = Cmdliner.Arg.conv (parse, Fpath.pp) in
+  let doc = "Which replay file to use" in
+  Cmdliner.Arg.(
+    required & opt (some replay_file) None & info [ "replay-file" ] ~doc )
 
 let outfile =
   let doc = "Write output to a file." in
@@ -273,6 +286,21 @@ let sym_cmd =
       $ no_assert_failure_expression_printing $ deterministic_result_order
       $ fail_mode $ workspace $ solver $ files )
 
+let replay_cmd =
+  let open Cmdliner in
+  let info =
+    let doc =
+      "Replay a module containing symbols with concrete values in a replay \
+       file containing a model"
+    in
+    let man = [] @ shared_man in
+    Cmd.info "replay" ~version ~doc ~sdocs ~man
+  in
+  Cmd.v info
+    Term.(
+      const Cmd_replay.cmd $ profiling $ debug $ unsafe $ optimize $ replay_file
+      $ sourcefile )
+
 let conc_cmd =
   let open Cmdliner in
   let info =
@@ -325,13 +353,14 @@ let cli =
   in
   Cmd.group info ~default
     [ c_cmd
+    ; conc_cmd
     ; fmt_cmd
-    ; opt_cmd
     ; instrument_cmd
+    ; opt_cmd
+    ; replay_cmd
     ; run_cmd
     ; script_cmd
     ; sym_cmd
-    ; conc_cmd
     ; validate_cmd
     ; wasm2wat_cmd
     ; wat2wasm_cmd
@@ -424,6 +453,7 @@ let exit_code =
       | `Unclosed_comment -> 75
       | `Unclosed_string -> 76
       | `Unbounded_quantification -> 77
+      | `Invalid_model _msg -> 78
     end
   end
   | Error e -> (

src/cmd/cmd_c.ml

@@ -20,7 +20,7 @@ let find location file : Fpath.t Result.t =
     list_map
       (fun dir ->
         let filename = Fpath.append dir file in
-        match Bos.OS.File.exists filename with
+        match OS.File.exists filename with
         | Ok true -> Ok (Some filename)
         | Ok false -> Ok None
         | Error (`Msg msg) -> Error (`Msg msg) )
@@ -68,7 +68,7 @@ let eacsl_instrument eacsl debug ~includes (files : Fpath.t list) :
         files
     in
 
-    let framac : Fpath.t -> Fpath.t -> Bos.Cmd.t =
+    let framac : Fpath.t -> Fpath.t -> Cmd.t =
      fun file out -> Cmd.(framac_bin %% flags1 % p file %% flags2 % p out)
     in
 
@@ -120,7 +120,7 @@ let compile ~includes ~opt_lvl debug (files : Fpath.t list) : Fpath.t Result.t =
   let* libc = find binc_location (Fpath.v "libc.wasm") in
 
   let files = Cmd.of_list (List.map Fpath.to_string (libc :: files)) in
-  let clang : Bos.Cmd.t = Cmd.(clang_bin %% flags % "-o" % p out %% files) in
+  let clang : Cmd.t = Cmd.(clang_bin %% flags % "-o" % p out %% files) in
 
   let+ () =
     match OS.Cmd.run clang with
@@ -152,7 +152,7 @@ let metadata ~workspace arch property files : unit Result.t =
     let* hash =
       list_fold_left
         (fun context file ->
-          let+ str = Bos.OS.File.read file in
+          let+ str = OS.File.read file in
           Digestif.SHA256.feed_string context str )
         Digestif.SHA256.empty files
     in

src/cmd/cmd_replay.ml

@@ -0,0 +1,116 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+open Syntax
+
+let run_file ~unsafe ~optimize filename model =
+  let next =
+    let next = ref ~-1 in
+    fun () ->
+      incr next;
+      !next
+  in
+
+  let assume_i32 _ = () in
+
+  let assume_positive_i32 _ = () in
+
+  let assert_i32 n = assert (not @@ Prelude.Int32.equal n 0l) in
+
+  let symbol_i32 () =
+    match model.(next ()) with Concrete_value.I32 n -> n | _ -> assert false
+  in
+
+  let symbol_char = symbol_i32 in
+
+  let symbol_i8 = symbol_i32 in
+
+  let symbol_i64 () =
+    match model.(next ()) with Concrete_value.I64 n -> n | _ -> assert false
+  in
+
+  let symbol_f32 () =
+    match model.(next ()) with Concrete_value.F32 n -> n | _ -> assert false
+  in
+
+  let symbol_f64 () =
+    match model.(next ()) with Concrete_value.F64 n -> n | _ -> assert false
+  in
+
+  let replay_extern_module =
+    let functions =
+      [ ( "i8_symbol"
+        , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_i8)
+        )
+      ; ( "char_symbol"
+        , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_char)
+        )
+      ; ( "i32_symbol"
+        , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_i32)
+        )
+      ; ( "i64_symbol"
+        , Concrete_value.Func.Extern_func (Func (UArg Res, R1 I64), symbol_i64)
+        )
+      ; ( "f32_symbol"
+        , Concrete_value.Func.Extern_func (Func (UArg Res, R1 F32), symbol_f32)
+        )
+      ; ( "f64_symbol"
+        , Concrete_value.Func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
+        )
+      ; ( "assume"
+        , Concrete_value.Func.Extern_func (Func (Arg (I32, Res), R0), assume_i32)
+        )
+      ; ( "assume_positive_i32"
+        , Concrete_value.Func.Extern_func
+            (Func (Arg (I32, Res), R0), assume_positive_i32) )
+      ; ( "assert"
+        , Concrete_value.Func.Extern_func (Func (Arg (I32, Res), R0), assert_i32)
+        )
+      ]
+    in
+    { Link.functions }
+  in
+
+  let link_state =
+    Link.extern_module Link.empty_state ~name:"symbolic" replay_extern_module
+  in
+
+  let* m =
+    Compile.File.until_binary_validate ~rac:false ~srac:false ~unsafe filename
+  in
+  let* m = Cmd_utils.add_main_as_start m in
+  let* m, link_state =
+    Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m
+  in
+  let c = Interpret.Concrete.modul link_state.envs m in
+  c
+
+let cmd profiling debug unsafe optimize replay_file file =
+  if profiling then Log.profiling_on := true;
+  if debug then Log.debug_on := true;
+  let* model =
+    match Smtml.Model.Parse.Scfg.from_file replay_file with
+    | Error msg -> Error (`Invalid_model msg)
+    | Ok model ->
+      let+ model =
+        list_map
+          (fun (_sym, v) ->
+            match v with
+            | Smtml.Value.False -> Ok (Concrete_value.I32 0l)
+            | True -> Ok (Concrete_value.I32 1l)
+            | Num (I8 n) -> Ok (Concrete_value.I32 (Int32.of_int n))
+            | Num (I32 n) -> Ok (Concrete_value.I32 n)
+            | Num (I64 n) -> Ok (Concrete_value.I64 n)
+            | Num (F32 n) -> Ok (Concrete_value.F32 (Float32.of_bits n))
+            | Num (F64 n) -> Ok (Concrete_value.F64 (Float64.of_bits n))
+            | Unit | Int _ | Real _ | Str _ | List _ | App _ | Nothing ->
+              Error
+                (`Invalid_model
+                  (Fmt.str "unexpected value type: %a" Smtml.Value.pp v) ) )
+          (Smtml.Model.get_bindings model)
+      in
+      Array.of_list model
+  in
+  let+ () = run_file ~unsafe ~optimize file model in
+  Fmt.pr "All OK@."

src/cmd/cmd_replay.mli

@@ -0,0 +1,5 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+val cmd : bool -> bool -> bool -> bool -> Fpath.t -> Fpath.t -> unit Result.t