add weasel example

CHANGES.md

@@ -1,8 +1,7 @@
 ## unreleased
 
 - 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
+- add `--rac` and `--srac` option to `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,9 +70,6 @@ OPTIONS
        -p, --profiling
            profiling mode
 
-       --rac
-           runtime assertion checking mode
-
        -u, --unsafe
            skip typechecking pass
 

example/weasel/README.md

@@ -0,0 +1,138 @@
+# Weasel
+
+Weasel stands for WEbAssembly Specification Language, it can be used to annotate Webassembly text modules in [custom annotation](https://github.com/WebAssembly/annotations). Annotated modules can be instrumented to perform runtime assertion checking thanks to owi's code generator.
+
+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.
+- `--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`.
+
+## Basic example
+
+Suppose we have a function returning its parameter plus three:
+
+```wast
+(module
+  (;...;)
+  (func $plus_three (param $x i32) (result i32)
+    local.get $x
+    i32.const 3
+    i32.add
+  )
+  (;...;)
+)
+```
+
+With Weasel, we can annotate this function by specifying its postconditions:
+
+```wast
+(module
+  (;...;)
+  (@contract $plus_three
+    (ensures (= result (+ $x 3)))
+  )
+  (func $plus_three (param $x i32) (result i32)
+    local.get $x
+    i32.const 3
+    i32.add
+  )
+  (;...;)
+)
+```
+
+`owi instrument` generates a new wrapper function checking this postcondition:
+
+```sh
+$ owi instrument plus_three.wat
+$ cat plus_three.instrumented.wat
+(module
+  (import "symbolic" "assert" (func $assert  (param i32)))
+  (type (sub final  (func (param $x i32) (result i32))))
+  (type (sub final  (func)))
+  (type (sub final  (func (param i32))))
+  (type (sub final  (func (result i32))))
+  (func $plus_three (param $x i32) (result i32)
+    local.get 0
+    i32.const 3
+    i32.add
+  )
+  (func $start
+    i32.const 42
+    call 3
+    drop
+  )
+  (func $__weasel_plus_three (param $x i32) (result i32) (local $__weasel_temp i32) (local $__weasel_res_0 i32)
+    local.get 0
+    call 1
+    local.set 2
+    local.get 2
+    local.get 0
+    i32.const 3
+    i32.add
+    i32.eq
+    call 0
+    local.get 2
+  )
+  (start 2)
+)
+```
+
+We can perform runtime assertion checking either by `owi sym plus_three.instrumented.wat` or by `owi sym --rac plus_three.wat`.
+
+```sh
+$ owi sym plus_three.instrumented.wat
+All OK
+$ owi sym --rac plus_three.wat
+All OK
+```
+
+## Man page
+
+```sh
+$ owi instrument --help=plain
+NAME
+       owi-instrument - Generate an instrumented file with runtime assertion
+       checking coming from Weasel specifications
+
+SYNOPSIS
+       owi instrument [--debug] [--symbolic] [--unsafe] [OPTION]… [ARG]…
+
+OPTIONS
+       -d, --debug
+           debug mode
+
+       --symbolic
+           generate instrumented module that depends on symbolic execution
+
+       -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 instrument 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/weasel/dune

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

example/weasel/plus_three.instrumented.wat

@@ -0,0 +1,30 @@
+(module
+  (import "symbolic" "assert" (func $assert  (param i32)))
+  (type (sub final  (func (param $x i32) (result i32))))
+  (type (sub final  (func)))
+  (type (sub final  (func (param i32))))
+  (type (sub final  (func (result i32))))
+  (func $plus_three (param $x i32) (result i32)
+    local.get 0
+    i32.const 3
+    i32.add
+  )
+  (func $start
+    i32.const 42
+    call 3
+    drop
+  )
+  (func $__weasel_plus_three (param $x i32) (result i32) (local $__weasel_temp i32) (local $__weasel_res_0 i32)
+    local.get 0
+    call 1
+    local.set 2
+    local.get 2
+    local.get 0
+    i32.const 3
+    i32.add
+    i32.eq
+    call 0
+    local.get 2
+  )
+  (start 2)
+)

example/weasel/plus_three.wat

@@ -0,0 +1,16 @@
+(module
+  (@contract $plus_three
+    (ensures (= result (+ $x 3)))
+  )
+  (func $plus_three (param $x i32) (result i32)
+    local.get $x
+    i32.const 3
+    i32.add
+  )
+  (func $start
+    i32.const 42
+    call $plus_three
+    drop
+  )
+  (start $start)
+)

src/bin/owi.ml

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

src/cmd/cmd_run.ml

@@ -4,15 +4,15 @@
 
 open Syntax
 
-let run_file ~unsafe ~rac ~optimize filename =
+let run_file ~unsafe ~optimize filename =
   let name = None in
   let+ (_ : _ Link.state) =
-    Compile.File.until_interpret ~unsafe ~rac ~srac:false ~optimize ~name
+    Compile.File.until_interpret ~unsafe ~rac:false ~srac:false ~optimize ~name
       Link.empty_state filename
   in
   ()
 
-let cmd profiling debug unsafe rac optimize files =
+let cmd profiling debug unsafe optimize files =
   if profiling then Log.profiling_on := true;
   if debug then Log.debug_on := true;
-  list_iter (run_file ~unsafe ~rac ~optimize) files
+  list_iter (run_file ~unsafe ~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 -> bool -> Fpath.t list -> unit Result.t
+val cmd : bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t

test/opt/output.t

@@ -1,7 +1,6 @@
   $ owi opt fbinop.wat -o bar.wat
   $ owi fmt bar.wat
   (module
-
     (type (sub final  (func)))
     (func $start
 

test/wasm2wat/output.t

@@ -1,9 +1,7 @@
   $ owi wasm2wat done.wasm -o bar.wat
   $ owi fmt bar.wat
   (module
-
     (type (sub final  (func (param i32) (param i32) (result i32))))
-
     (type (sub final  (func)))
     (func (param i32) (param i32) (result i32)
       local.get 0