readd owi run --rac

CHANGES.md

@@ -1,7 +1,8 @@
 ## unreleased
 
 - add `owi instrument` to instrument Webassembly module annotated by Weasel specification language
-- add `--rac` and `--srac` option to `sym` and `conc` cmd
+- add `--srac` option to `sym` and `conc` cmd
+- add `--rac` option to `run`, `sym` and `conc` cmd
 - add `--output` option to `wat2wasm`, `wasm2wat` and `opt` cmd
 - Change `free` prototype to now return a pointer on which tracking is deactivated
 - add `--emit-file` option to `wasm2wat` to emit .wat files

example/run/README.md

@@ -70,6 +70,9 @@ OPTIONS
        -p, --profiling
            profiling mode
 
+       --rac
+           runtime assertion checking mode
+
        -u, --unsafe
            skip typechecking pass
 

example/weasel/README.md

@@ -4,7 +4,7 @@ Weasel stands for WEbAssembly Specification Language, it can be used to annotate
 
 Commands and options related to Weasel:
 - `owi instrument` to instrument an annotated text module.
-- `--rac` for `sym` and `conc` to instrument an annotated text module and perform runtime assertion checking.
+- `--rac` for `run`, `sym` and `conc` to instrument an annotated text module and perform runtime assertion checking.
 - `--srac` for `sym` and `conc` to instrument an annotated text module and perform runtime assertion checking symbolically.
 
 The formal specification of Weasel can be found in `src/annot/spec.ml`.

src/bin/owi.ml

@@ -231,7 +231,7 @@ let run_cmd =
   in
   Cmd.v info
     Term.(
-      const Cmd_run.cmd $ profiling $ debug $ unsafe $ optimize $ files )
+      const Cmd_run.cmd $ profiling $ debug $ unsafe $ rac $ optimize $ files )
 
 let validate_cmd =
   let open Cmdliner in

src/cmd/cmd_run.ml

@@ -4,15 +4,15 @@
 
 open Syntax
 
-let run_file ~unsafe ~optimize filename =
+let run_file ~unsafe ~rac ~optimize filename =
   let name = None in
   let+ (_ : _ Link.state) =
-    Compile.File.until_interpret ~unsafe ~rac:false ~srac:false ~optimize ~name
+    Compile.File.until_interpret ~unsafe ~rac ~srac:false ~optimize ~name
       Link.empty_state filename
   in
   ()
 
-let cmd profiling debug unsafe optimize files =
+let cmd profiling debug unsafe rac optimize files =
   if profiling then Log.profiling_on := true;
   if debug then Log.debug_on := true;
-  list_iter (run_file ~unsafe ~optimize) files
+  list_iter (run_file ~unsafe ~rac ~optimize) files

src/cmd/cmd_run.mli

@@ -2,4 +2,4 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-val cmd : bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t
+val cmd : bool -> bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t