Allow writing function contracts in webassembly code

CHANGES.md

@@ -1,5 +1,8 @@
 ## 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 `--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/README.md

@@ -38,6 +38,10 @@ COMMANDS
        fmt [--inplace] [OPTION]… [ARG]…
            Format a .wat or .wast file
 
+       instrument [--debug] [--symbolic] [--unsafe] [OPTION]… [ARG]…
+           Generate an instrumented file with runtime assertion checking
+           coming from Weasel specifications
+
        opt [--debug] [--output=FILE] [--unsafe] [OPTION]… ARG
            Optimize a module
 

example/conc/README.md

@@ -71,9 +71,15 @@ OPTIONS
        -p, --profiling
            profiling mode
 
+       --rac
+           runtime assertion checking mode
+
        -s VAL, --solver=VAL (absent=Z3)
            SMT solver to use
 
+       --srac
+           symbolic runtime assertion checking mode
+
        -u, --unsafe
            skip typechecking pass
 

example/define_host_function/README.md

@@ -85,8 +85,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `sausage` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v
@@ -203,8 +203,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `chorizo` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v

example/define_host_function/extern.ml

@@ -39,8 +39,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `sausage` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v

example/define_host_function/extern_mem.ml

@@ -38,8 +38,8 @@ let pure_wasm_module =
 (* our pure wasm module, linked with `chorizo` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module
   with
   | Error _ -> assert false
   | Ok v -> v

example/define_host_function/life_game/life_console.ml

@@ -64,8 +64,8 @@ let pure_wasm_module_1 =
 (* our first pure wasm module, linked with `life_ext` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true
-      ~name:(Some "life") pure_wasm_module_1
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:(Some "life") pure_wasm_module_1
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)
@@ -85,8 +85,8 @@ let pure_wasm_module_2 =
 (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module_2
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module_2
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)

example/define_host_function/life_game/life_graphics.ml

@@ -76,8 +76,8 @@ let pure_wasm_module_1 =
 (* our first pure wasm module, linked with `life_ext` *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true
-      ~name:(Some "life") pure_wasm_module_1
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:(Some "life") pure_wasm_module_1
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)
@@ -97,8 +97,8 @@ let pure_wasm_module_2 =
 (* our second pure wasm module, linked with `life_ext` and `life` interpreted before *)
 let module_to_run, link_state =
   match
-    Compile.Text.until_link link_state ~unsafe:false ~optimize:true ~name:None
-      pure_wasm_module_2
+    Compile.Text.until_link link_state ~unsafe:false ~rac:false ~srac:false
+      ~optimize:true ~name:None pure_wasm_module_2
   with
   | Error _ -> assert false
   | Ok (m, state) -> (m, state)

example/lib/README.md

@@ -16,7 +16,7 @@ val filename : Fpath.t = <abstr>
 val m : Text.modul =
 ...
 # let module_to_run, link_state =
-    match Compile.Text.until_link Link.empty_state ~unsafe:false ~optimize:false ~name:None m with
+    match Compile.Text.until_link Link.empty_state ~unsafe:false ~rac:false ~srac:false ~optimize:false ~name:None m with
     | Ok v -> v
     | Error _ -> assert false;;
 val module_to_run : '_weak1 Link.module_to_run =

example/run/README.md

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

example/sym/README.md

@@ -75,9 +75,15 @@ OPTIONS
        -p, --profiling
            profiling mode
 
+       --rac
+           runtime assertion checking mode
+
        -s VAL, --solver=VAL (absent=Z3)
            SMT solver to use
 
+       --srac
+           symbolic 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 `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`.
+
+## 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/annot/annot.ml

@@ -0,0 +1,35 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+open Fmt
+
+type t =
+  { annotid : string
+  ; items : Sexp.t
+  }
+
+type 'a annot =
+  | Contract of 'a Contract.t
+  | Annot of t
+
+let pp_annot fmt = function
+  | Contract contract ->
+    pf fmt "(@%a@\n  @[<v>%a@]@\n)" string "contract" Contract.pp_contract
+      contract
+  | Annot annot ->
+    pf fmt "(@%a@\n  @[<hv>%a@]@\n)" string annot.annotid Sexp.pp_sexp
+      annot.items
+
+let annot_recorder : (string, Sexp.t) Hashtbl.t = Hashtbl.create 17
+
+let record_annot annotid sexp = Hashtbl.add annot_recorder annotid sexp
+
+let get_annots () =
+  let res =
+    Hashtbl.fold
+      (fun annotid items acc -> { annotid; items } :: acc)
+      annot_recorder []
+  in
+  Hashtbl.reset annot_recorder;
+  res