From 916ae44b5ba1b635d2447edbf2dae8d3f54dbd43 Mon Sep 17 00:00:00 2001 From: Zhicheng HUI Date: Fri, 6 Sep 2024 14:24:15 +0200 Subject: [PATCH] add weasel example --- CHANGES.md | 3 +- example/run/README.md | 3 - example/weasel/README.md | 138 +++++++++++++++++++++ example/weasel/dune | 4 + example/weasel/plus_three.instrumented.wat | 30 +++++ example/weasel/plus_three.wat | 16 +++ src/bin/owi.ml | 2 +- src/cmd/cmd_run.ml | 8 +- src/cmd/cmd_run.mli | 2 +- test/opt/output.t | 1 - test/wasm2wat/output.t | 2 - 11 files changed, 195 insertions(+), 14 deletions(-) create mode 100644 example/weasel/README.md create mode 100644 example/weasel/dune create mode 100644 example/weasel/plus_three.instrumented.wat create mode 100644 example/weasel/plus_three.wat diff --git a/CHANGES.md b/CHANGES.md index 954e3741b..196b4a2f7 100644 --- a/CHANGES.md +++ b/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 diff --git a/example/run/README.md b/example/run/README.md index 7a549eb66..781d3b20e 100644 --- a/example/run/README.md +++ b/example/run/README.md @@ -70,9 +70,6 @@ OPTIONS -p, --profiling profiling mode - --rac - runtime assertion checking mode - -u, --unsafe skip typechecking pass diff --git a/example/weasel/README.md b/example/weasel/README.md new file mode 100644 index 000000000..f11ef0cfd --- /dev/null +++ b/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 . + +SEE ALSO + owi(1) + +``` diff --git a/example/weasel/dune b/example/weasel/dune new file mode 100644 index 000000000..6588b0ba6 --- /dev/null +++ b/example/weasel/dune @@ -0,0 +1,4 @@ +(mdx + (libraries owi) + (deps %{bin:owi} plus_three.wat plus_three.instrumented.wat) + (files README.md)) diff --git a/example/weasel/plus_three.instrumented.wat b/example/weasel/plus_three.instrumented.wat new file mode 100644 index 000000000..60de0f0e1 --- /dev/null +++ b/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) +) \ No newline at end of file diff --git a/example/weasel/plus_three.wat b/example/weasel/plus_three.wat new file mode 100644 index 000000000..d1b3eed01 --- /dev/null +++ b/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) +) diff --git a/src/bin/owi.ml b/src/bin/owi.ml index 53ae9342e..6702c481d 100644 --- a/src/bin/owi.ml +++ b/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 diff --git a/src/cmd/cmd_run.ml b/src/cmd/cmd_run.ml index 3f159327d..b791c8546 100644 --- a/src/cmd/cmd_run.ml +++ b/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 diff --git a/src/cmd/cmd_run.mli b/src/cmd/cmd_run.mli index 63aec0acf..5cef2e0c3 100644 --- a/src/cmd/cmd_run.mli +++ b/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 diff --git a/test/opt/output.t b/test/opt/output.t index f99c975c9..310f5cdaf 100644 --- a/test/opt/output.t +++ b/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 diff --git a/test/wasm2wat/output.t b/test/wasm2wat/output.t index ad270c4f6..a3f3c79d7 100644 --- a/test/wasm2wat/output.t +++ b/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