Welcome to Owi
Owi is an open-source framework for advanced WebAssembly analysis and manipulation, with a focus on practical symbolic execution and robust tooling. It is designed for researchers, engineers, programming language enthusiasts and practitioners requiring precise, flexible, and extensible support program reasoning.
Owi provides three primary components:
🔬 Symbolic Execution Engine for Wasm, C, C++, Rust, and Zig
Owi includes a cross-language symbolic execution engine supporting:
- Automated testing, bug finding and pentesting through symbolic testing and constraint solving;
- Solver-aided programming for problem solving and synthesis tasks;
- Test case generation aligned with advanced coverage criteria;
- Formal verification: prove properties or find counterexamples in real-world programs.
The engine is designed for precision, scalability, interoperability across languages, and extensibility toward both experimental and applied verification use-cases. It offers a practical path from fuzzing to formal proofs.
🔧 The Wasm Swiss Army Knife
Owi offers a set of practical tools for Wasm development and analysis:
- Formatter and optimizer for Wasm modules;
- Interpreter for
.wasm,.wat, and even Wasm scripts (.wast) files that are used in the reference test suite; - Specification-compliant validator;
- Bidirectional translation between binary (
.wasm) and text (.wat) formats; - Randomized fuzzer generating valid (well-typed) Wasm modules.
These tools aim to support everyday development tasks as well as research on program analysis, fuzzing, and program transformation.
🐪 Native OCaml Library for Wasm Integration
Owi is written in OCaml, thus it also provides a library for:
- Embedding Wasm modules into OCaml applications;
- Importing OCaml functions into Wasm modules with full type safety.
This allows for tightly integrating Wasm-based computation within OCaml-based systems while maintaining strong type guarantees.
⚠️ Warning
For now, the optimizer and the formatter are quite experimental. The optimizer is well tested but only performs basic optimizations in an inefficient way. The formatter is mainly used for debugging purpose and is probably incorrect on some cases. Moreover, the concolic mode is currently broken, use the symbolic one.
🧑🎓Want to join us?
We are looking for interns, have a look at the internship labeled issues.
Installation
owi can be installed with opam:
$ opam install owi
# if you intend to use symbolic execution you must install one solver
# you can choose any solver supported by smtml
# z3, colibri2, bitwuzla-cxx or cvc5 for instance
$ opam install z3
If you don't have opam, you can install it following the how to install opam guide.
If you can't or don't want to use opam, you can build the package with dune build -p owi @install but you'll first have to install the dependencies by yourself. You can find the list of dependencies in the dune-project file.
Development version
To get the development version:
$ git clone git@github.com:OCamlPro/owi.git
$ cd owi
$ opam install . --deps-only
$ dune build -p owi @install
$ dune install
Supported Wasm proposals
The 🐌 status means the proposal is not applicable to Owi.
Adopted proposals
Current proposals
We only list proposals that reached phase 3 at least.
Overview
Symbolic Execution 101
Quickstart
C Quickstart
C++ Quickstart
Checking the equivalence of two functions
#include <owi.h>
struct IntPair {
int x, y;
int mean1() const { return (x & y) + ((x ^ y) >> 1); }
int mean2() const { return (x + y) / 2; }
};
int main() {
IntPair p{owi_i32(), owi_i32()};
owi_assert(p.mean1() == p.mean2());
}
$ owi c++ ./mean.cpp --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32 -2147483648
symbol symbol_1 i32 -2147483646
}
owi: [ERROR] Reached problem!
[13]
Rust Quickstart
Given the following main.rs file:
use owi_sym::Symbolic;
fn mean_wrong(x: i32, y: i32) -> i32 {
(x + y) / 2
}
fn mean_correct(x: i32, y: i32) -> i32 {
(x & y) + ((x ^ y) >> 1)
}
fn main() {
let x = i32::symbol();
let y = i32::symbol();
owi_sym::assert(mean_wrong(x, y) == mean_correct(x, y))
}
Let's check if the two functions are the same for any input:
$ owi rust ./mean.rs -w1 --fail-on-assertion-only --no-assert-failure-expression-printing --deterministic-result-order
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32 -487586839
symbol symbol_1 i32 486539486
}
owi: [ERROR] Reached problem!
[13]
Indeed, in this case, there will be an integer overflow in one of the two functions and thus they won't give the same result.
Zig Quickstart
Fibonacci example
Given the following fib.zig file:
// TODO: replace this by a proper include of the owi header?
extern "symbolic" fn i32_symbol() i32;
extern "symbolic" fn assume(bool) void;
extern "symbolic" fn assert(bool) void;
fn fibonacci(n: i32) i32 {
if (n < 0) {
@panic("expected a positive number");
}
if (n <= 2) return n;
return fibonacci(n - 1) + fibonacci(n - 2);
}
pub fn main() void {
const n: i32 = i32_symbol();
assume(n > 0);
assume(n < 10);
const result = fibonacci(n);
assert(result != 21);
}
Owi can find a crash with:
$ owi zig ./fib.zig -w1 --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32 7
}
owi: [ERROR] Reached problem!
[13]
WebAssembly Quickstart
Symbolic engine
The symbolic interpreter provides functions that allows to create symbolic values.
For instance, here, the $i32_symbol function creates a symbol of type i32.
This value will represent "any possible value".
Then, during the execution we collect informations and when an error is reached, we are able to find a concrete value for each symbol such that this value lead to the error.
For instance, in the following file, we define x as a symbolic variable.
Then if 5 < x, we fail:
(module
(import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
(func $start (local $x i32)
(local.set $x (call $i32_symbol))
(if (i32.lt_s (i32.const 5) (local.get $x)) (then
unreachable
))
)
(start $start))
Let's see if owi is able to find a value for x that lead to an error:
$ owi sym ./mini.wat
owi: [ERROR] Trap: unreachable
model {
symbol symbol_0 i32 6
}
owi: [ERROR] Reached problem!
[13]
Indeed, if x is equal to 6 then, the unreachable instruction will be reached.
Concolic engine
The concolic engine works exactly in the same way than the symbolic engine:
$ owi conc ./mini.wat
owi: [ERROR] Trap: unreachable
Model:
model {
symbol symbol_1 i32 6
}
owi: [ERROR] Reached problem!
[13]
Bug-Finding, Testing & Pen-testing
Examples of Bug Finding
How to Speed it Up
Replaying a model
Let's say you found a bug and want to check what is going on with the concrete input it contains.
The replay commands can help with that.
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:
(module
(import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
(func $start (local $x i32)
(local.set $x (call $i32_symbol))
(if (i32.lt_s (i32.const 5) (local.get $x)) (then
unreachable
))
)
(start $start))
You can get a model like this:
$ owi sym ./mini.wat > mini.scfg
owi: [ERROR] Trap: unreachable
owi: [ERROR] Reached problem!
[13]
Then you can replay the module execution with the values in the model like this:
$ owi replay --replay-file mini.scfg mini.wat -v
owi: [INFO] parsing ...
owi: [INFO] checking ...
owi: [INFO] typechecking ...
owi: [INFO] typechecking ...
owi: [INFO] linking ...
owi: [INFO] interpreting ...
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 1
owi: [INFO] calling func : func start
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 0
owi: [INFO] stack : [ i32.const 6 ]
owi: [INFO] running instr : local.set 0
owi: [INFO] stack : [ ]
owi: [INFO] running instr : i32.const 5
owi: [INFO] stack : [ i32.const 5 ]
owi: [INFO] running instr : local.get 0
owi: [INFO] stack : [ i32.const 6 ; i32.const 5 ]
owi: [INFO] running instr : i32.lt_s
owi: [INFO] stack : [ i32.const 1 ]
owi: [INFO] running instr : if
owi: [INFO] stack : [ ]
owi: [INFO] running instr : unreachable
owi: [ERROR] unreachable
[94]
Comparing iso-functionnality of two modules
The owi iso command takes two Wasm modules as input.
Then, for every common exports between these two modules, Owi will check their equivalence.
Given the following mul1.wat file:
(module
(func (export "unused1") (param $x i32)
local.get $x
drop
)
(func (export "mul") (param $x i32) (param $y i32) (result i32)
local.get $x
local.get $y
i32.mul
)
)
And the following mul2.wat file:
(module
(func (export "unused2") (param $x i32) (param $y i64) (result i64)
local.get $x
(if (then (unreachable)))
local.get $y
)
(func (export "mul") (param $x i32) (param $y i32) (result i32)
local.get $y
local.get $x
i32.mul
i32.const 1
i32.add
)
)
Owi can find an input for which the mul function of these two modules is not equivalent:
$ owi iso ./mul1.wat ./mul2.wat -v -w1
owi: [INFO] comparing ./mul1.wat and ./mul2.wat
owi: [INFO] module owi_iso_module1 is ./mul1.wat
owi: [INFO] module owi_iso_module2 is ./mul2.wat
owi: [INFO] Compiling ./mul1.wat
owi: [INFO] parsing ...
owi: [INFO] checking ...
owi: [INFO] typechecking ...
owi: [INFO] Compiling ./mul2.wat
owi: [INFO] parsing ...
owi: [INFO] checking ...
owi: [INFO] typechecking ...
owi: [INFO] common exports: mul
owi: [INFO] checking export mul
owi: [INFO] typechecking ...
owi: [INFO] linking ...
owi: [INFO] typechecking ...
owi: [INFO] linking ...
owi: [INFO] typechecking ...
owi: [INFO] linking ...
owi: [INFO] interpreting ...
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 8
owi: [INFO] calling func : func start
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 3
owi: [INFO] stack : [ symbol_0 ]
owi: [INFO] running instr : call 3
owi: [INFO] stack : [ symbol_1 ; symbol_0 ]
owi: [INFO] running instr : call 7
owi: [INFO] calling func : func check_iso_func
owi: [INFO] stack : [ ]
owi: [INFO] running instr : local.get 0
owi: [INFO] stack : [ symbol_0 ]
owi: [INFO] running instr : local.get 1
owi: [INFO] stack : [ symbol_1 ; symbol_0 ]
owi: [INFO] running instr : call 0
owi: [INFO] calling func : func anonymous
owi: [INFO] stack : [ ]
owi: [INFO] running instr : local.get 0
owi: [INFO] stack : [ symbol_0 ]
owi: [INFO] running instr : local.get 1
owi: [INFO] stack : [ symbol_1 ; symbol_0 ]
owi: [INFO] running instr : i32.mul
owi: [INFO] stack : [ (i32.mul symbol_0 symbol_1) ]
owi: [INFO] running instr : local.get 0
owi: [INFO] stack : [ symbol_0 ; (i32.mul symbol_0 symbol_1) ]
owi: [INFO] running instr : local.get 1
owi: [INFO] stack : [ symbol_1 ; symbol_0 ; (i32.mul symbol_0
symbol_1) ]
owi: [INFO] running instr : call 1
owi: [INFO] calling func : func anonymous
owi: [INFO] stack : [ ]
owi: [INFO] running instr : local.get 1
owi: [INFO] stack : [ symbol_1 ]
owi: [INFO] running instr : local.get 0
owi: [INFO] stack : [ symbol_0 ; symbol_1 ]
owi: [INFO] running instr : i32.mul
owi: [INFO] stack : [ (i32.mul symbol_1 symbol_0) ]
owi: [INFO] running instr : i32.const 1
owi: [INFO] stack : [ 1 ; (i32.mul symbol_1 symbol_0) ]
owi: [INFO] running instr : i32.add
owi: [INFO] stack : [ (i32.add (i32.mul symbol_1 symbol_0) 1) ;
(i32.mul symbol_0 symbol_1) ]
owi: [INFO] running instr : i32.eq
owi: [INFO] stack : [ (i32.of_bool
(bool.eq (i32.mul symbol_0 symbol_1)
(i32.add (i32.mul symbol_1 symbol_0) 1))) ]
owi: [INFO] running instr : call 2
owi: [ERROR] Assert failure: (bool.eq (i32.mul symbol_0 symbol_1)
(i32.add (i32.mul symbol_1 symbol_0) 1))
model {
symbol symbol_0 i32 0
symbol symbol_1 i32 0
}
owi: [INFO] Completed paths: 1
owi: [ERROR] Reached problem!
[13]
Comparison to Fuzzing and Abstract Interpretation
Bugs Found by Owi
Solver-Aided Programming
Examples of Problem Solving
Solving polynomials
C
Given the following poly.c file:
#include <owi.h>
int main() {
int x = owi_i32();
int x2 = x * x;
int x3 = x * x * x;
int a = 1;
int b = -7;
int c = 14;
int d = -8;
int poly = a * x3 + b * x2 + c * x + d;
owi_assert(poly != 0);
return 0;
}
We are defining one symbolic variable x using the function owi_i32(void). Then we build a polynomial poly equal to $x^3 - 7x^2 + 14x - 8$.
Then we use owi_assert(poly != 0). Which should fail as this polynomial has multiple roots. Let's see what owi says about it:
$ owi c ./poly.c -w1 --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32 4
}
owi: [ERROR] Reached problem!
[13]
Indeed, 4 is a root of the polynomial and thus it is expected to be equal to 0 in this case. We know the three roots are 1, 2 and 4, so let's inform owi that we are not interested in this cases.
We can do so by assuming that x is not equal to any of these with the function owi_assume(bool):
#include <owi.h>
int main() {
int x = owi_i32();
int x2 = x * x;
int x3 = x * x * x;
int a = 1;
int b = -7;
int c = 14;
int d = -8;
int poly = a * x3 + b * x2 + c * x + d;
owi_assume(x != 1);
owi_assume(x != 2);
owi_assume(x != 4);
// Make model output deterministic
owi_assume(x > -2147483646);
owi_assert(poly != 0);
return 0;
}
Let's run owi on this new input:
$ owi c ./poly2.c --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32 -2147483644
}
owi: [ERROR] Reached problem!
[13]
And indeed, -2147483644 is a root of the polynomial! Well, not quite…
Remember that we are working on 32 bits integers here. Thus overflows are a thing we have to think about. And indeed when x is equal to -2147483644, because of overflows, the polynomial will be equal to zero.
Exercise: can you find another "root" of the polynomial ? :-)
C++
Given the following poly.cpp file:
#include <owi.h>
class Poly {
private:
int poly;
public:
Poly(int a, int b, int c, int d) {
int x = owi_i32();
int x2 = x * x;
int x3 = x2 * x;
poly = a*x3 + b*x2 + c*x + d;
}
int hasRoot() const { return poly == 0; }
};
int main() {
Poly p(1, -7, 14, -8);
owi_assert(not(p.hasRoot()));
}
We are defining one symbolic variable x using the function owi_i32(void). Then we build a polynomial poly equal to $x^3 - 7x^2 + 14x - 8$.
Then we use owi_assert(p.getPoly() != 0). Which should fail as this polynomial has multiple roots. Let's see what owi says about it:
$ owi c++ ./poly.cpp -w1 --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32 4
}
owi: [ERROR] Reached problem!
[13]
Indeed, 4 is a root of the polynomial and thus it is expected to be equal to 0 in this case. We know the three roots are 1, 2 and 4, so let's inform owi that we are not interested in this cases.
We can do so by assuming that x is not equal to any of these with the function owi_assume(bool):
#include <owi.h>
class Poly {
private:
int poly;
public:
Poly(int a, int b, int c, int d) {
int x = owi_i32();
int x2 = x * x;
int x3 = x2 * x;
owi_assume(x != 1);
owi_assume(x != 2);
// make model output deterministic
owi_assume(x > -2147483646);
owi_assume(x != 4);
poly = a*x3 + b*x2 + c*x + d;
}
int hasRoot() const { return poly == 0; }
};
int main() {
Poly p(1, -7, 14, -8);
owi_assert(not(p.hasRoot()));
}
Let's run owi on this new input:
$ owi c++ ./poly2.cpp --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32 -2147483644
}
owi: [ERROR] Reached problem!
[13]
And indeed, -2147483644 is a root of the polynomial! Well, not quite…
Remember that we are working on 32 bits integers here. Thus overflows are a thing we have to think about. And indeed when x is equal to -2147483644, because of overflows, the polynomial will be equal to zero.
Exercise: can you find another "root" of the polynomial ? :-)
Solving a maze
#include <owi.h>
// example from https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/
#define H 7
#define W 11
#define ITERS 28
char maze[H][W] = {
"+-+---+---+",
"| | |#|",
"| | --+ | |",
"| | | | |",
"| +-- | | |",
"| | |",
"+-----+---+"
};
int main (void) {
int x = 1;
int y = 1;
maze[y][x]='X';
char program[ITERS];
for (int i = 0; i < ITERS; i++) {
program[i] = owi_i32();
}
int old_x = x;
int old_y = y;
for (int i = 0; i < ITERS; i++) {
old_x = x;
old_y = y;
switch (program[i]) {
case 'w':
y--;
break;
case 's':
y++;
break;
case 'a':
x--;
break;
case 'd':
x++;
break;
default:
return 1;
}
if (maze[y][x] == '#') {
// TODO: print the result
owi_assert(0);
return 0;
}
if (maze[y][x] != ' ' && !((y == 2 && maze[y][x] == '|' && x > 0 && x < W))) {
return 1;
}
if (old_x == x && old_y == y) {
return 1;
}
maze[y][x] = 'X';
}
return 1;
}
$ owi c ./maze.c --no-value --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32
symbol symbol_1 i32
symbol symbol_2 i32
symbol symbol_3 i32
symbol symbol_4 i32
symbol symbol_5 i32
symbol symbol_6 i32
symbol symbol_7 i32
symbol symbol_8 i32
symbol symbol_9 i32
symbol symbol_10 i32
symbol symbol_11 i32
symbol symbol_12 i32
symbol symbol_13 i32
symbol symbol_14 i32
symbol symbol_15 i32
symbol symbol_16 i32
symbol symbol_17 i32
symbol symbol_18 i32
symbol symbol_19 i32
symbol symbol_20 i32
symbol symbol_21 i32
symbol symbol_22 i32
symbol symbol_23 i32
symbol symbol_24 i32
symbol symbol_25 i32
symbol symbol_26 i32
symbol symbol_27 i32
}
owi: [ERROR] Reached problem!
[13]
Dobble example
// An encoding representing the problem of finding a suitable
// set of cards for https://en.wikipedia.org/wiki/Dobble.
// Cards are encoded on integers, with each position
// representing one of N_CARDS possible symbols.
#include <owi.h>
#include <stdlib.h>
// Number of symbols per card
#define CARD_SIZE 3
#define N_CARDS ((CARD_SIZE*CARD_SIZE) - CARD_SIZE + 1)
int popcount(unsigned int x) {
int count = 0;
for (int i = 0; i < N_CARDS; i++) {
count += x & 1;
x >>= 1;
}
return count;
}
int main() {
unsigned int cards[N_CARDS];
for (int i=0;i < N_CARDS; i++) {
unsigned int x = owi_i32();
owi_assume((x >> N_CARDS) == 0);
owi_assume(popcount(x) == CARD_SIZE);
cards[i] = x;
if (i > 0) {
owi_assume(cards[i] > cards[i-1]);
}
}
unsigned int acc = 1;
for (int i=0;i < N_CARDS; i++) {
for(int j=i+1; j < N_CARDS;j++) {
owi_assume(cards[i] != cards[j]);
unsigned int z = cards[i] & cards[j];
acc = acc & (z != 0);
acc = acc & ((z & (z-1)) == 0);
}
}
owi_assert(!acc);
}
$ owi c -O1 ./dobble.c -w1 --no-value --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
symbol symbol_0 i32
symbol symbol_1 i32
symbol symbol_2 i32
symbol symbol_3 i32
symbol symbol_4 i32
symbol symbol_5 i32
symbol symbol_6 i32
}
owi: [ERROR] Reached problem!
[13]
How to Speed it Up
Comparison to Rosette, Prolog, etc.
Test-Case Generation
Labels
Verification and Proof of Programs
Comparison with Deductive Verification and Abstract Interpretation
E-ACSL
Combining symbolic execution with runtime assertion checking (RAC)
E-ACSL is a specification language of C codes, as well as a runtime assertion checking tool within Frama-C. It works by consuming a C program annotated with E-ACSL specifications, it generates a monitored C program which aborts its execution when the specified properties are violated at runtime.
Generally, such a C program runs on concrete values. Yet we can combine symbolic execution with runtime assertion checking, in order to check the properties using symbolic values. This will lead to better coverage of potential execution paths and scenarios.
Finding primes
Consider the following (faulty) function primes, it implements the algorithm of the Sieve of Eratosthenes to find all the prime numbers smaller than n:
void primes(int *is_prime, int n) {
for (int i = 1; i < n; ++i) is_prime[i] = 1;
for (int i = 2; i * i < n; ++i) {
if (!is_prime[i]) continue;
for (int j = i; i * j < n; ++j) {
is_prime[i * j] = 0;
}
}
}
Initially, it marks each number as prime. It then marks as composite the multiples of each prime, iterating in an ascending order. If a number is still marked as prime at the point of iteration, then it does not admit a nontrivial factor and should be a prime.
In order to verify the implementation, we annotate the function primes using the E-ACSL specification language. The annotations should be written immediately above the function and surrounded by /*@ ... */.
#define MAX_SIZE 100
/*@ requires 2 <= n <= MAX_SIZE;
requires \valid(is_prime + (0 .. (n - 1)));
ensures \forall integer i; 0 <= i < n ==>
(is_prime[i] <==>
(i >= 2 && \forall integer j; 2 <= j < i ==> i % j != 0));
*/
void primes(int *is_prime, int n) {
for (int i = 0; i < n; ++i) is_prime[i] = 1;
for (int i = 2; i * i < n; ++i) {
if (!is_prime[i]) continue;
for (int j = i; i * j < n; ++j) {
is_prime[i * j] = 0;
}
}
}
Here, requires and ensures specify the pre-condition and post-condition of the function. The annotation means:
- When the function is called,
- the argument
nshould be between2andMAX_SIZE - for all
ibetween0andn - 1,is_prime + ishould be memory locations safe to read and write
- the argument
- When the function returns,
- for all
ibetween0andn - 1,is_prime[i]evaluates totrueif and only ifiis larger than2and does not have a factor between2andi - 1(which indicates the primality ofi)
- for all
We can then call the function with symbolic values and see what happens. We should pass the option --e-acsl to let owi invoke the E-ACSL plugin.
#define MAX_SIZE 100
#include <owi.h>
#include <stdlib.h>
/*@ requires 2 <= n <= MAX_SIZE;
requires \valid(is_prime + (0 .. (n - 1)));
ensures \forall integer i; 0 <= i < n ==>
(is_prime[i] <==>
(i >= 2 && \forall integer j; 2 <= j < i ==> i % j != 0));
*/
void primes(int *is_prime, int n) {
for (int i = 0; i < n; ++i) is_prime[i] = 1;
for (int i = 2; i * i < n; ++i) {
if (!is_prime[i]) continue;
for (int j = i; i * j < n; ++j) {
is_prime[i * j] = 0;
}
}
}
int main(void) {
int *is_prime;
is_prime = malloc(MAX_SIZE * sizeof(int));
int n = owi_i32();
owi_assume(n >= 2);
owi_assume(n <= MAX_SIZE);
primes(is_prime, n);
free(is_prime);
return 0;
}
$ owi c --e-acsl primes.c -w1
owi: [ERROR] Assert failure: false
model {
symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]
The execution got aborted because one of the specifications has been violated with n = 2. (The error message is not so informative for the time being, extra information aiding the diagnostic of errors may be added in the future.)
The problem is that we should mark 0 and 1 as non-prime during the initialization. Let's fix it and rerun the program.
#define MAX_SIZE 100
#include <owi.h>
#include <stdlib.h>
/*@ requires 2 <= n <= MAX_SIZE;
requires \valid(is_prime + (0 .. (n - 1)));
ensures \forall integer i; 0 <= i < n ==>
(is_prime[i] <==>
(i >= 2 && \forall integer j; 2 <= j < i ==> i % j != 0));
*/
void primes(int *is_prime, int n) {
for (int i = 0; i < n; ++i) is_prime[i] = 1;
is_prime[0] = is_prime[1] = 0;
for (int i = 2; i * i < n; ++i) {
if (!is_prime[i]) continue;
for (int j = i; i * j < n; ++j) {
is_prime[i * j] = 0;
}
}
}
int main(void) {
int *is_prime;
is_prime = malloc(MAX_SIZE * sizeof(int));
int n = owi_i32();
owi_assume(n >= 2);
owi_assume(n <= MAX_SIZE);
primes(is_prime, n);
free(is_prime);
return 0;
}
$ owi c --e-acsl primes2.c -w1
All OK!
All the specified properties have been satisfied during the execution.
Weasel
Weasel stands for WEbAssembly Specification Language, it can be used to annotate Webassembly text modules in custom annotation. Annotated modules can be instrumented to perform runtime assertion checking thanks to owi's code generator.
Commands and options related to Weasel:
owi instrumentto instrument an annotated text module.--racforrun,symandconcto instrument an annotated text module and perform runtime assertion checking.--sracforsymandconcto 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:
(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:
(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:
$ owi instrument plus_three.wat
$ cat plus_three.instrumented.wat
(module
(import "symbolic" "assert" (func $assert (param i32)))
(type (func (param $x i32) (result i32)))
(type (func))
(type (func (param i32)))
(type (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.
$ owi sym plus_three.instrumented.wat
All OK!
$ owi sym --rac plus_three.wat
All OK!
Going Further
Comparison with Other Engines
Talks and Papers
Publications
- Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly, 2024
- Exécution symbolique pour tous ou Compilation d'OCaml vers WebAssembly, 2024
- Cross-Language Symbolic Runtime Annotation Checking, 2025
Talks
- september 2023: ICFP OCaml track
- october 2023: Wasm Research Day organized by the WebAssembly Research Center and hosted in Google Munich
- april 2024: OUPS (OCaml UserS in Paris)
- november 2024: LVP working group day of the GdR GPL
- december 2024: Léo Andrès' PhD defense
- january 2025: JFLA 2025
- february 2025: Wasm Research Day 2025
- february 2025: PPS Seminar
- may 2025: 15th MirageOS hack retreat
Commands and Options
API: Symbols and Helpers
Overview
Formatter
Given a file horrible.wat:
(module (memory
10) (func
$f (param
$n i32) (result
i32) (if
( i32.lt_s
(
local.get $n)
(
i32.const
0))
( then
(
unreachable)))
(
if
(
i32.lt_s
(local.get $n)
(i32.const 2))
(then (return (local.get $n)))) (if
(i32.eqz
(i32.load (i32.mul (i32.const 4) (local.get $n)))) (then local.get $n i32.const 4 i32.mul
(call $f (i32.sub (local.get $n) (i32.const 1)))
(call $f (i32.sub (local.get $n)
(i32.const 2))) i32.add i32.store )) local.get $n i32.const 4 i32.mul i32.load return))
Owi will format it like this:
$ owi fmt horrible.wat
(module
(memory 10)
(func $f (param $n i32) (result i32)
local.get $n
i32.const 0
i32.lt_s
(if
(then
unreachable
)
)
local.get $n
i32.const 2
i32.lt_s
(if
(then
local.get $n
return
)
)
i32.const 4
local.get $n
i32.mul
i32.load align=1
i32.eqz
(if
(then
local.get $n
i32.const 4
i32.mul
local.get $n
i32.const 1
i32.sub
call $f
local.get $n
i32.const 2
i32.sub
call $f
i32.add
i32.store align=1
)
)
local.get $n
i32.const 4
i32.mul
i32.load align=1
return
)
)
Are you able to recognize the program now?
Interpreter
Given a file 42.wat with the following content:
(module $quickstart
(func $f
i32.const 20
i32.const 22
i32.add
drop
)
(start $f)
)
Running the interpreter is as simple as:
$ owi run ./42.wat
Nothing is happening, so you can add the -v option to print an execution trace:
$ owi run ./42.wat -v
owi: [INFO] parsing ...
owi: [INFO] checking ...
owi: [INFO] typechecking ...
owi: [INFO] linking ...
owi: [INFO] interpreting ...
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 0
owi: [INFO] calling func : func f
owi: [INFO] stack : [ ]
owi: [INFO] running instr : i32.const 20
owi: [INFO] stack : [ i32.const 20 ]
owi: [INFO] running instr : i32.const 22
owi: [INFO] stack : [ i32.const 22 ; i32.const 20 ]
owi: [INFO] running instr : i32.add
owi: [INFO] stack : [ i32.const 42 ]
owi: [INFO] running instr : drop
Script using the spectest module
Given the following print.wast file:
(module
(func $print_i32 (import "spectest" "print_i32") (param i32))
(func $main
i32.const 42
call $print_i32
)
(start $main)
)
You can print the value thanks to the print_i32 function imported from the spectest module:
$ owi script ./print.wast
42
Optimizer
Given the useless program useless.wat:
(module
(func $i32binop
i32.const 21
i32.const 21
i32.add
i32.const 0
drop
drop
i32.const 63
i32.const 21
i32.sub
i32.const 0
drop
drop
i32.const 21
i32.const 2
i32.mul
i32.const 0
drop
drop
i32.const 84
i32.const 2
i32.div_s
i32.const 0
drop
drop
i32.const 84
i32.const 2
i32.div_u
i32.const 0
drop
drop
i32.const -42
i32.const 4
i32.rem_s ;; 4*10 + 2 > =-2
i32.const 0
drop
drop
i32.const -42
i32.const 4
i32.rem_u ;; 4*10 + 2 > =2
i32.const 0
drop
drop
i32.const 1
i32.const 3
i32.and ;; bitwise ope > =1
i32.const 0
drop
drop
i32.const 1
i32.const 3
i32.or ;; bitwise ope > =3
i32.const 0
drop
drop
i32.const 1
i32.const 3
i32.xor ;; bitwise ope > =2
i32.const 0
drop
drop
i32.const 1
i32.const 3
i32.shl ;; shift left ope > =8
i32.const 0
drop
drop
i32.const 8
i32.const 3
i32.shr_u ;; shift right ope > =1
i32.const 0
drop
drop
i32.const 8
i32.const 3
i32.shr_s ;; shift right ope > =1
i32.const 0
drop
drop
i32.const 1
i32.const 3
i32.rotl ;; rotation left ope > =8
i32.const 0
drop
drop
i32.const 8
i32.const 3
i32.rotr ;; rotation left ope > =1
i32.const 0
drop
drop
)
(func $i64binop
i64.const 21
i64.const 21
i64.add
i32.const 0
drop
drop
i64.const 63
i64.const 21
i64.sub
i32.const 0
drop
drop
i64.const 21
i64.const 2
i64.mul
i32.const 0
drop
drop
i64.const 84
i64.const 2
i64.div_s
i32.const 0
drop
drop
i64.const 84
i64.const 2
i64.div_u
i32.const 0
drop
drop
i64.const -42
i64.const 4
i64.rem_s ;; 4*10 + 2 > =-2
i32.const 0
drop
drop
i64.const -42
i64.const 4
i64.rem_u ;; 4*10 + 2 > =2
i32.const 0
drop
drop
i64.const 1
i64.const 3
i64.and ;; bitwise ope > =1
i32.const 0
drop
drop
i64.const 1
i64.const 3
i64.or ;; bitwise ope > =3
i32.const 0
drop
drop
i64.const 1
i64.const 3
i64.xor ;; bitwise ope > =2
i32.const 0
drop
drop
i64.const 1
i64.const 3
i64.shl ;; shift left ope > =8
i32.const 0
drop
drop
i64.const 8
i64.const 3
i64.shr_u ;; shift right ope > =1
i32.const 0
drop
drop
i64.const 8
i64.const 3
i64.shr_s ;; shift right ope > =1
i32.const 0
drop
drop
i64.const 1
i64.const 3
i64.rotl ;; rotation left ope > =8
i32.const 0
drop
drop
i64.const 8
i64.const 3
i64.rotr ;; rotation left ope > =1
i32.const 0
drop
drop
)
(func $f32binop
f32.const 21
f32.const 21
f32.add
i32.const 0
drop
drop
f32.const 63
f32.const 21
f32.sub
i32.const 0
drop
drop
f32.const 21
f32.const 2
f32.mul
i32.const 0
drop
drop
f32.const 84
f32.const 2
f32.div
i32.const 0
drop
drop
f32.const 42
f32.const 21
f32.max
i32.const 0
drop
drop
f32.const 42
f32.const 84
f32.min
i32.const 0
drop
drop
f32.const -42
f32.const 21
f32.copysign
i32.const 0
drop
drop
)
(func $f64binop
f64.const 21
f64.const 21
f64.add
i32.const 0
drop
drop
f64.const 63
f64.const 21
f64.sub
i32.const 0
drop
drop
f64.const 21
f64.const 2
f64.mul
i32.const 0
drop
drop
f64.const 84
f64.const 2
f64.div
i32.const 0
drop
drop
f64.const 42
f64.const 21
f64.max
i32.const 0
drop
drop
f64.const 42
f64.const 84
f64.min
i32.const 0
drop
drop
f64.const -42
f64.const 21
f64.copysign
i32.const 0
drop
drop
)
(func $start
call $i32binop
call $i64binop
call $f32binop
call $f64binop
)
(start $start)
)
Owi is able to get rid of most of the code:
$ owi opt useless.wat
(module
(type (func))
(func $i32binop
)
(func $i64binop
)
(func $f32binop
)
(func $f64binop
)
(func $start
call 0
call 1
call 2
call 3
)
(start 4)
)
Validator
Given a file type_error.wat with the following content:
(module $quickstart
(func $f
i32.const 20
i32.const 22
i32.add
i32.add
drop
)
(start $f)
)
Running the validator is as simple as:
$ owi validate ./type_error.wat
owi: [ERROR] type mismatch (expected [i32 i32] but stack is [i32])
[35]
You can also print a more detailed trace with the -v option:
$ owi validate ./type_error.wat -v
owi: [INFO] parsing ...
owi: [INFO] checking ...
owi: [INFO] typechecking ...
owi: [ERROR] type mismatch (expected [i32 i32] but stack is [i32])
[35]
Wasm2wat
Given a file 42.wasm, you can convert it to result.wat and then run it:
$ owi wasm2wat 42.wasm -o result.wat
$ cat result.wat
(module
(type (func))
(func
i32.const 20
i32.const 22
i32.add
drop
)
(start 0)
)
$ owi run result.wat -v
owi: [INFO] parsing ...
owi: [INFO] checking ...
owi: [INFO] typechecking ...
owi: [INFO] linking ...
owi: [INFO] interpreting ...
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 0
owi: [INFO] calling func : func anonymous
owi: [INFO] stack : [ ]
owi: [INFO] running instr : i32.const 20
owi: [INFO] stack : [ i32.const 20 ]
owi: [INFO] running instr : i32.const 22
owi: [INFO] stack : [ i32.const 22 ; i32.const 20 ]
owi: [INFO] running instr : i32.add
owi: [INFO] stack : [ i32.const 42 ]
owi: [INFO] running instr : drop
Wat2wasm
Given a file 42.wat, you can convert it to result.wasm and then run it:
$ owi wat2wasm 42.wat -o result.wasm
$ owi run result.wasm -v
owi: [INFO] typechecking ...
owi: [INFO] linking ...
owi: [INFO] interpreting ...
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 0
owi: [INFO] calling func : func anonymous
owi: [INFO] stack : [ ]
owi: [INFO] running instr : i32.const 20
owi: [INFO] stack : [ i32.const 20 ]
owi: [INFO] running instr : i32.const 22
owi: [INFO] stack : [ i32.const 22 ; i32.const 20 ]
owi: [INFO] running instr : i32.add
owi: [INFO] stack : [ i32.const 42 ]
owi: [INFO] running instr : drop
Comparison with Other Tools
owi
$ owi --help=plain
NAME
owi - OCaml WebAssembly Interpreter
SYNOPSIS
owi [COMMAND] …
COMMANDS
c [OPTION]… FILE…
Compile a C file to Wasm and run the symbolic interpreter on it
c++ [OPTION]… FILE…
Compile a C++ file to Wasm and run the symbolic interpreter on it
conc [OPTION]… FILE…
Run the concolic interpreter
fmt [OPTION]… FILE…
Format a .wat or .wast file
instrument [OPTION]… FILE…
Generate an instrumented file with runtime assertion checking
coming from Weasel specifications
iso [OPTION]… FILE…
Check the iso-functionnality of two Wasm modules by comparing the
output when calling their exports.
opt [OPTION]… FILE
Optimize a module
replay [OPTION]… FILE
Replay a module containing symbols with concrete values in a
replay file containing a model
run [OPTION]… FILE…
Run the concrete interpreter
rust [OPTION]… FILE…
Compile a Rust file to Wasm and run the symbolic interpreter on it
script [OPTION]… FILE…
Run a reference test suite script
sym [OPTION]… FILE…
Run the symbolic interpreter
validate [OPTION]… FILE…
Validate a module
version [OPTION]…
Print some version informations
wasm2wat [OPTION]… FILE
Generate a text format file (.wat) from a binary format file
(.wasm)
wat2wasm [OPTION]… FILE
Generate a binary format file (.wasm) from a text format file
(.wat)
zig [OPTION]… FILE…
Compile a Zig file to Wasm and run the symbolic interpreter on it
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 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 <contact@ndrs.fr>.
owi c
$ owi c --help=plain
NAME
owi-c - Compile a C file to Wasm and run the symbolic interpreter on
it
SYNOPSIS
owi c [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--concolic
concolic mode
--deterministic-result-order
Guarantee a fixed deterministic order of found failures. This
implies --no-stop-at-failure.
--e-acsl
e-acsl mode, refer to
https://frama-c.com/download/e-acsl/e-acsl-implementation.pdf for
Frama-C's current language feature implementations
--entry-point=FUNCTION
entry point of the executable
--fail-on-assertion-only
ignore traps and only report assertion violations
--fail-on-trap-only
ignore assertion violations and only report traps
-I VAL
headers path
--invoke-with-symbols
Invoke the entry point of the program with symbolic values instead
of dummy constants.
-m VAL, --arch=VAL (absent=32)
data model
--model-format=VAL (absent=scfg)
The format of the model ("json" or "scfg")
--model-out-file=FILE
Output the generated model to FILE. if --no-stop-at-failure is
given this is used as a prefix and the ouputed files would have
PREFIX_%d.
--no-assert-failure-expression-printing
do not display the expression in the assert failure
--no-stop-at-failure
do not stop when a program failure is encountered
--no-value
do not display a value for each symbol
-o FILE, --output=FILE
Output the generated .wasm or .wat to FILE.
-O VAL (absent=3)
specify which optimization level to use
--optimize
optimize mode
--property=FILE
property file
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-s VAL, --solver=VAL (absent=Z3)
SMT solver to use
--testcomp
test-comp mode
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
-w VAL, --workers=VAL (absent=n)
number of workers for symbolic execution. Defaults to the number
of physical cores.
--with-breadcrumbs
add breadcrumbs to the generated model
--workspace=DIR
write results and intermediate compilation artifacts to dir
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 c 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).
ENVIRONMENT
These environment variables affect the execution of owi c:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi c++
$ owi c++ --help=plain
NAME
owi-c++ - Compile a C++ file to Wasm and run the symbolic interpreter
on it
SYNOPSIS
owi c++ [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--concolic
concolic mode
--deterministic-result-order
Guarantee a fixed deterministic order of found failures. This
implies --no-stop-at-failure.
--entry-point=FUNCTION
entry point of the executable
--fail-on-assertion-only
ignore traps and only report assertion violations
--fail-on-trap-only
ignore assertion violations and only report traps
-I VAL
headers path
--invoke-with-symbols
Invoke the entry point of the program with symbolic values instead
of dummy constants.
-m VAL, --arch=VAL (absent=32)
data model
--model-format=VAL (absent=scfg)
The format of the model ("json" or "scfg")
--model-out-file=FILE
Output the generated model to FILE. if --no-stop-at-failure is
given this is used as a prefix and the ouputed files would have
PREFIX_%d.
--no-assert-failure-expression-printing
do not display the expression in the assert failure
--no-stop-at-failure
do not stop when a program failure is encountered
--no-value
do not display a value for each symbol
-o FILE, --output=FILE
Output the generated .wasm or .wat to FILE.
-O VAL (absent=3)
specify which optimization level to use
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-s VAL, --solver=VAL (absent=Z3)
SMT solver to use
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
-w VAL, --workers=VAL (absent=n)
number of workers for symbolic execution. Defaults to the number
of physical cores.
--with-breadcrumbs
add breadcrumbs to the generated model
--workspace=DIR
write results and intermediate compilation artifacts to dir
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 c++ 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).
ENVIRONMENT
These environment variables affect the execution of owi c++:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi conc
$ owi conc --help=plain
NAME
owi-conc - Run the concolic interpreter
SYNOPSIS
owi conc [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--deterministic-result-order
Guarantee a fixed deterministic order of found failures. This
implies --no-stop-at-failure.
--entry-point=FUNCTION
entry point of the executable
--fail-on-assertion-only
ignore traps and only report assertion violations
--fail-on-trap-only
ignore assertion violations and only report traps
--invoke-with-symbols
Invoke the entry point of the program with symbolic values instead
of dummy constants.
--model-format=VAL (absent=scfg)
The format of the model ("json" or "scfg")
--model-out-file=FILE
Output the generated model to FILE. if --no-stop-at-failure is
given this is used as a prefix and the ouputed files would have
PREFIX_%d.
--no-assert-failure-expression-printing
do not display the expression in the assert failure
--no-stop-at-failure
do not stop when a program failure is encountered
--no-value
do not display a value for each symbol
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
--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
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
-w VAL, --workers=VAL (absent=n)
number of workers for symbolic execution. Defaults to the number
of physical cores.
--with-breadcrumbs
add breadcrumbs to the generated model
--workspace=DIR
write results and intermediate compilation artifacts to dir
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 conc 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).
ENVIRONMENT
These environment variables affect the execution of owi conc:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi fmt
$ owi fmt --help=plain
NAME
owi-fmt - Format a .wat or .wast file
SYNOPSIS
owi fmt [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
-i, --inplace
Format in-place, overwriting input file
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 fmt 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).
ENVIRONMENT
These environment variables affect the execution of owi fmt:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi instrument
$ owi instrument --help=plain
NAME
owi-instrument - Generate an instrumented file with runtime assertion
checking coming from Weasel specifications
SYNOPSIS
owi instrument [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
-q, --quiet
Be quiet. Takes over -v and --verbosity.
--symbolic
generate instrumented module that depends on symbolic execution
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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).
ENVIRONMENT
These environment variables affect the execution of owi instrument:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi iso
$ owi iso --help=plain
NAME
owi-iso - Check the iso-functionnality of two Wasm modules by
comparing the output when calling their exports.
SYNOPSIS
owi iso [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--deterministic-result-order
Guarantee a fixed deterministic order of found failures. This
implies --no-stop-at-failure.
--fail-on-assertion-only
ignore traps and only report assertion violations
--fail-on-trap-only
ignore assertion violations and only report traps
--model-format=VAL (absent=scfg)
The format of the model ("json" or "scfg")
--model-out-file=FILE
Output the generated model to FILE. if --no-stop-at-failure is
given this is used as a prefix and the ouputed files would have
PREFIX_%d.
--no-assert-failure-expression-printing
do not display the expression in the assert failure
--no-stop-at-failure
do not stop when a program failure is encountered
--no-value
do not display a value for each symbol
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-s VAL, --solver=VAL (absent=Z3)
SMT solver to use
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
-w VAL, --workers=VAL (absent=n)
number of workers for symbolic execution. Defaults to the number
of physical cores.
--with-breadcrumbs
add breadcrumbs to the generated model
--workspace=DIR
write results and intermediate compilation artifacts to dir
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 iso 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).
ENVIRONMENT
These environment variables affect the execution of owi iso:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi opt
$ owi opt --help=plain
NAME
owi-opt - Optimize a module
SYNOPSIS
owi opt [OPTION]… FILE
ARGUMENTS
FILE (required)
source file
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
-o FILE, --output=FILE
Output the generated .wasm or .wat to FILE.
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 opt 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).
ENVIRONMENT
These environment variables affect the execution of owi opt:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi replay
$ 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]… FILE
ARGUMENTS
FILE (required)
source file
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--entry-point=FUNCTION
entry point of the executable
--invoke-with-symbols
Invoke the entry point of the program with symbolic values instead
of dummy constants.
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
--replay-file=FILE (required)
Which replay file to use
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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).
ENVIRONMENT
These environment variables affect the execution of owi replay:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi run
$ owi run --help=plain
NAME
owi-run - Run the concrete interpreter
SYNOPSIS
owi run [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
--rac
runtime assertion checking mode
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 run 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).
ENVIRONMENT
These environment variables affect the execution of owi run:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi rust
$ owi rust --help=plain
NAME
owi-rust - Compile a Rust file to Wasm and run the symbolic
interpreter on it
SYNOPSIS
owi rust [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--concolic
concolic mode
--deterministic-result-order
Guarantee a fixed deterministic order of found failures. This
implies --no-stop-at-failure.
--entry-point=FUNCTION
entry point of the executable
--fail-on-assertion-only
ignore traps and only report assertion violations
--fail-on-trap-only
ignore assertion violations and only report traps
-I VAL
headers path
--invoke-with-symbols
Invoke the entry point of the program with symbolic values instead
of dummy constants.
-m VAL, --arch=VAL (absent=32)
data model
--model-format=VAL (absent=scfg)
The format of the model ("json" or "scfg")
--model-out-file=FILE
Output the generated model to FILE. if --no-stop-at-failure is
given this is used as a prefix and the ouputed files would have
PREFIX_%d.
--no-assert-failure-expression-printing
do not display the expression in the assert failure
--no-stop-at-failure
do not stop when a program failure is encountered
--no-value
do not display a value for each symbol
-o FILE, --output=FILE
Output the generated .wasm or .wat to FILE.
-O VAL (absent=3)
specify which optimization level to use
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-s VAL, --solver=VAL (absent=Z3)
SMT solver to use
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
-w VAL, --workers=VAL (absent=n)
number of workers for symbolic execution. Defaults to the number
of physical cores.
--with-breadcrumbs
add breadcrumbs to the generated model
--workspace=DIR
write results and intermediate compilation artifacts to dir
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 rust 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).
ENVIRONMENT
These environment variables affect the execution of owi rust:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi script
$ owi script --help=plain
NAME
owi-script - Run a reference test suite script
SYNOPSIS
owi script [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--no-exhaustion
no exhaustion tests
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 script 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).
ENVIRONMENT
These environment variables affect the execution of owi script:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi sym
$ owi sym --help=plain
NAME
owi-sym - Run the symbolic interpreter
SYNOPSIS
owi sym [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--deterministic-result-order
Guarantee a fixed deterministic order of found failures. This
implies --no-stop-at-failure.
--entry-point=FUNCTION
entry point of the executable
--fail-on-assertion-only
ignore traps and only report assertion violations
--fail-on-trap-only
ignore assertion violations and only report traps
--invoke-with-symbols
Invoke the entry point of the program with symbolic values instead
of dummy constants.
--model-format=VAL (absent=scfg)
The format of the model ("json" or "scfg")
--model-out-file=FILE
Output the generated model to FILE. if --no-stop-at-failure is
given this is used as a prefix and the ouputed files would have
PREFIX_%d.
--no-assert-failure-expression-printing
do not display the expression in the assert failure
--no-stop-at-failure
do not stop when a program failure is encountered
--no-value
do not display a value for each symbol
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
--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
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
-w VAL, --workers=VAL (absent=n)
number of workers for symbolic execution. Defaults to the number
of physical cores.
--with-breadcrumbs
add breadcrumbs to the generated model
--workspace=DIR
write results and intermediate compilation artifacts to dir
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 sym 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).
ENVIRONMENT
These environment variables affect the execution of owi sym:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi validate
$ owi validate --help=plain
NAME
owi-validate - Validate a module
SYNOPSIS
owi validate [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 validate 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).
ENVIRONMENT
These environment variables affect the execution of owi validate:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi version
$ owi version --help=plain
NAME
owi-version - Print some version informations
SYNOPSIS
owi version [OPTION]…
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 version 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).
ENVIRONMENT
These environment variables affect the execution of owi version:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi wasm2wat
$ owi wasm2wat --help=plain
NAME
owi-wasm2wat - Generate a text format file (.wat) from a binary format
file (.wasm)
SYNOPSIS
owi wasm2wat [OPTION]… FILE
ARGUMENTS
FILE (required)
source file
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--emit-file
Emit (.wat) files from corresponding (.wasm) files.
-o FILE, --output=FILE
Output the generated .wasm or .wat to FILE.
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 wasm2wat 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).
ENVIRONMENT
These environment variables affect the execution of owi wasm2wat:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi wat2wasm
$ owi wat2wasm --help=plain
NAME
owi-wat2wasm - Generate a binary format file (.wasm) from a text
format file (.wat)
SYNOPSIS
owi wat2wasm [OPTION]… FILE
ARGUMENTS
FILE (required)
source file
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
-o FILE, --output=FILE
Output the generated .wasm or .wat to FILE.
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
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 wat2wasm 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).
ENVIRONMENT
These environment variables affect the execution of owi wat2wasm:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
owi zig
$ owi zig --help=plain
NAME
owi-zig - Compile a Zig file to Wasm and run the symbolic interpreter
on it
SYNOPSIS
owi zig [OPTION]… FILE…
ARGUMENTS
FILE (required)
source files
OPTIONS
--color=WHEN (absent=auto)
Colorize the output. WHEN must be one of auto, always or never.
--concolic
concolic mode
--deterministic-result-order
Guarantee a fixed deterministic order of found failures. This
implies --no-stop-at-failure.
--entry-point=FUNCTION
entry point of the executable
--fail-on-assertion-only
ignore traps and only report assertion violations
--fail-on-trap-only
ignore assertion violations and only report traps
-I VAL
headers path
--invoke-with-symbols
Invoke the entry point of the program with symbolic values instead
of dummy constants.
--model-format=VAL (absent=scfg)
The format of the model ("json" or "scfg")
--model-out-file=FILE
Output the generated model to FILE. if --no-stop-at-failure is
given this is used as a prefix and the ouputed files would have
PREFIX_%d.
--no-assert-failure-expression-printing
do not display the expression in the assert failure
--no-stop-at-failure
do not stop when a program failure is encountered
--no-value
do not display a value for each symbol
-o FILE, --output=FILE
Output the generated .wasm or .wat to FILE.
--optimize
optimize mode
-q, --quiet
Be quiet. Takes over -v and --verbosity.
-s VAL, --solver=VAL (absent=Z3)
SMT solver to use
-u, --unsafe
skip typechecking pass
-v, --verbose
Increase verbosity. Repeatable, but more than twice does not bring
more.
--verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
Be more or less verbose. LEVEL must be one of quiet, error,
warning, info or debug. Takes over -v.
-w VAL, --workers=VAL (absent=n)
number of workers for symbolic execution. Defaults to the number
of physical cores.
--with-breadcrumbs
add breadcrumbs to the generated model
--workspace=DIR
write results and intermediate compilation artifacts to dir
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 zig 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).
ENVIRONMENT
These environment variables affect the execution of owi zig:
OWI_VERBOSITY
See option --verbosity.
BUGS
Email them to <contact@ndrs.fr>.
SEE ALSO
owi(1)
Overview
Given a file quickstart.wat, here's how to parse and run this file:
# open Prelude;;
# open Owi;;
# Fmt_tty.setup_std_outputs ();;
- : unit = ()
# Logs.set_level ~all:true (Some Logs.Info);;
- : unit = ()
# Logs.set_reporter (Logs_fmt.reporter ())
- : unit = ()
# let filename = Fpath.v "quickstart.wat";;
val filename : Fpath.t = <abstr>
# let m =
match Parse.Text.Module.from_file filename with
| Ok script -> script
| Error e -> assert false;;
mdx_gen.bc.exe: [INFO] parsing ...
...
annots = []}
# let module_to_run, link_state =
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;;
mdx_gen.bc.exe: [INFO] checking ...
mdx_gen.bc.exe: [INFO] typechecking ...
mdx_gen.bc.exe: [INFO] linking ...
...
# let () =
match Interpret.Concrete.modul link_state.envs module_to_run with
| Ok () -> ()
| Error _ -> assert false;;
mdx_gen.bc.exe: [INFO] interpreting ...
mdx_gen.bc.exe: [INFO] stack : [ ]
mdx_gen.bc.exe: [INFO] running instr : call 0
mdx_gen.bc.exe: [INFO] calling func : func f
mdx_gen.bc.exe: [INFO] stack : [ ]
mdx_gen.bc.exe: [INFO] running instr : i32.const 24
mdx_gen.bc.exe: [INFO] stack : [ i32.const 24 ]
mdx_gen.bc.exe: [INFO] running instr : i32.const 24
mdx_gen.bc.exe: [INFO] stack : [ i32.const 24 ; i32.const 24 ]
mdx_gen.bc.exe: [INFO] running instr : i32.add
mdx_gen.bc.exe: [INFO] stack : [ i32.const 48 ]
mdx_gen.bc.exe: [INFO] running instr : drop
Using and defining external functions (host functions)
Dealing with the Stack
Given the following extern.wat file:
(module $extern
(import "sausage" "fresh"
(func $fresh (param i32) (result externref)))
(import "sausage" "get_i32r"
(func $get (param externref) (result i32)))
(import "sausage" "set_i32r"
(func $set (param externref) (param i32)))
(import "sausage" "print_i32"
(func $print_i32 (param i32)))
(func $start (local $ref externref)
;; let ref = fresh 42
(local.set $ref (call $fresh (i32.const 42)))
;; print_i32 (get ref)
(call $print_i32 (call $get (local.get $ref)))
;; set ref 13
(call $set (local.get $ref) (i32.const 13) )
;; print_i32 (get ref)
(call $print_i32 (call $get (local.get $ref)))
)
(start $start)
)
You can define the various required external functions in OCaml like this :
open Owi
(* an extern module that will be linked with a wasm module *)
let extern_module : Concrete_extern_func.extern_func Link.extern_module =
(* some custom functions *)
let rint : int32 ref Type.Id.t = Type.Id.make () in
let fresh i = Ok (ref i) in
let set r (i : int32) =
r := i;
Ok ()
in
let get r = Ok !r in
let print_i32 (i : int32) =
Printf.printf "%li\n%!" i;
Ok ()
in
(* we need to describe their types *)
let functions =
[ ( "print_i32"
, Concrete_extern_func.Extern_func (Func (Arg (I32, Res), R0), print_i32)
)
; ( "fresh"
, Concrete_extern_func.Extern_func
(Func (Arg (I32, Res), R1 (Externref rint)), fresh) )
; ( "set_i32r"
, Concrete_extern_func.Extern_func
(Func (Arg (Externref rint, Arg (I32, Res)), R0), set) )
; ( "get_i32r"
, Concrete_extern_func.Extern_func
(Func (Arg (Externref rint, Res), R1 I32), get) )
]
in
{ functions }
(* a link state that contains our custom module, available under the name `sausage` *)
let link_state =
Link.extern_module Link.empty_state ~name:"sausage" extern_module
(* a pure wasm module refering to `sausage` *)
let pure_wasm_module =
match Parse.Text.Module.from_file (Fpath.v "extern.wat") with
| Error _ -> assert false
| Ok modul -> modul
(* our pure wasm module, linked with `sausage` *)
let module_to_run, link_state =
match
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
(* let's run it ! it will print the values as defined in the print_i32 function *)
let () =
match Interpret.Concrete.modul link_state.envs module_to_run with
| Error _ -> assert false
| Ok () -> ()
You'll get the expected result:
$ ./extern.exe
42
13
Dealing with the Linear Memory
Owi also allows interacting with linear memory through external functions. This is helpful because it enables the host system to communicate directly with a Wasm instance through its linear memory. Consider the tiny example below to illustrate this:
(module $extern_mem
(import "chorizo" "memset" (func $memset (param i32 i32 i32)))
(import "chorizo" "print_x64" (func $print_x64 (param i64)))
(memory 1)
(func $start
;; memset 0 0xAA 8
(call $memset (i32.const 0) (i32.const 0xAA) (i32.const 8))
;; print_x64 (load 0)
(call $print_x64 (i64.load (i32.const 0)))
)
(start $start)
)
In the module $extern_mem, we first import $memset and $print_x64. Then,
in the $start function, we initialize the memory starting at address
(i32.const 0) with a sequence of length (i32.const 8) with bytes of
(i32.const 0xAA).
The definition of the external functions follows the same format as the previous example. The difference is that, now, in the GADT definition of memset to allow the memory to be passed to this function, we need to wrap the three I32 arguments in a Mem variant. That is, instead of writing memset as:
(Func (Arg (I32, (Arg (I32, (Arg (I32, Res))))), R0), memset)
One should use:
(Func (Mem (Arg (I32, (Arg (I32, (Arg (I32, Res)))))), R0), memset)
See the module below for the whole implementation:
open Owi
(* an extern module that will be linked with a wasm module *)
let extern_module : Concrete_extern_func.extern_func Link.extern_module =
(* some custom functions *)
let memset m start byte length =
let rec loop offset =
if Int32.le offset length then begin
match Concrete_memory.store_8 m ~addr:(Int32.add start offset) byte with
| Error _ as e -> e
| Ok () -> loop (Int32.add offset 1l)
end
else Ok ()
in
loop 0l
in
let print_x64 (i : int64) =
Printf.printf "0x%LX\n%!" i;
Ok ()
in
(* we need to describe their types *)
let functions =
[ ( "print_x64"
, Concrete_extern_func.Extern_func (Func (Arg (I64, Res), R0), print_x64)
)
; ( "memset"
, Concrete_extern_func.Extern_func
(Func (Mem (Arg (I32, Arg (I32, Arg (I32, Res)))), R0), memset) )
]
in
{ functions }
(* a link state that contains our custom module, available under the name `chorizo` *)
let link_state =
Link.extern_module Link.empty_state ~name:"chorizo" extern_module
(* a pure wasm module refering to `$extern_mem` *)
let pure_wasm_module =
match Parse.Text.Module.from_file (Fpath.v "extern_mem.wat") with
| Error _ -> assert false
| Ok modul -> modul
(* our pure wasm module, linked with `chorizo` *)
let module_to_run, link_state =
match
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
(* let's run it ! it will print the values as defined in the print_i64 function *)
let () =
match Interpret.Concrete.modul link_state.envs module_to_run with
| Error _ -> assert false
| Ok () -> ()
Running the above program should yield:
$ ./extern_mem.exe
0xAAAAAAAAAAAAAAAA
Advanced Usage
To learn more, see our advanced Game of Life example
based on the famous cellular automaton by Conway. It show how to link several modules from different .wat files.
Conway's Game of Life
This example is a Conway's Game of Life implementation. 3 outputs are proposed (console, OCaml Graphics and HTML/JavaScript), each one using the same WebAssembly modules.
Console and OCaml Graphics
Console and Graphics implementations use external functions technique as the standard example. Here are the command lines to run in this directory to execute the programs:
- Console mode:
dune exec -- ./life_graphics.exe - Graphics mode:
dune exec -- ./life_console.exe
Several modules (defined in life.wat and life_loop.wat files) are linked.
Why are two .wat files required ?
Because, in JavaScript, the Sleep function uses the
Promise system
which cannot work in a wasm call context.
So, if we want to use the same WebAssembly components in all contexts,
the game loop had to be extracted in a separate module.
See the following section for JavaScript implementation details.
HTML/JavaScript
Here is a standard example of a wasm module called in a web page using the JavaScript API.
First of all, a compiled version of the WebAssembly module is needed, obtained by the
command line wat2wasm life.wat. wat2wasm is part of the
WABT: The WebAssembly Binary Toolkit.
As in OCaml in the previous contexts, external functions are defined in the environment execution
(here in JavaScript). As explained before, only one wasm module is imported (life.wasm) and
the game loop has been written directly in JavaScript.
This function (life()) must be async because sleep function is called in await mode.
To see the final result, simply open life.html in your favorite browser.
However, the command line dune exec -- ./runweb.exe launches a full build and open it
directly in your browser. Some additional dependencies are required including
ocaml-cohttp and
ocaml-crunch.
Generated API Documentation
Development Setup
To get a proper development setup:
$ git clone git@github.com:OCamlPro/owi.git
$ cd owi
$ opam install . --deps-only --with-test --with-doc --with-dev-setup
$ git submodule update --init --recursive
$ dune build @all
Coding Guidelines
The prelude library
We use the prelude library to hide dangerous functions from the standard library.
It is automatically opened in the whole project.
More than dangerous functions, this library also hide some modules for which better alternatives exists.
For instance, all system interactions are done using Bos and all the formatting is done with Fmt.
Printing
Read the Logs basics and in particular, the usage conventions.
Documentation
API
You can build the documentation with:
$ dune build @doc
$ xdg-open _build/default/doc/index.html
Full documentation
$ cd ./doc
$ mdbook serve
Testing
Unit tests
Tests are mostly written using Cram Tests. The ones that are integrated into documentation are using MDX. You can run them as follow:
$ dune runtest
If you made some changes and the output of some tests is changing, the diff will be displayed. If you want to automatically accept the diff as being the new expected output, you can run:
$ dune promote
Code coverage
You can generate the code coverage report with:
BISECT_FILE=$(pwd)/bisect odune runtest --force --instrument-with bisect_ppx
bisect-ppx-report html -o _coverage
xdg-open _coverage/index.html
Fuzzing
See test/fuzz.
Benchmarking
Landmarks
OCAML_LANDMARKS=on dune exec --instrument-with landmarks --profile release -- owi run test/run/binary_loop.wasm
Note: it seems landmarks is not compatible with domains and thus won't work with most sub-commands.
Test-comp
See bench.
History of Owi
Spelling and pronunciation
Although the name Owi comes from an acronym (OCaml WebAssembly Interpreter), it must be written as a proper noun and only the first letter must be capitalized. It is possible to write the name in full lowercase when referring to the opam package or to the name of the binary.
The reason we chose this spelling rather than the fully capitalized version is that in French, Owi is pronounced [o’wi(ʃ)] which sounds like "Oh oui !" which means "Oh yes!". Thus it should be pronounced this way and not by spelling the three letters it is made of.
Authors and Contributors
License
Owi
Copyright (C) 2021-2024 OCamlPro
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU Affero General Public License for more details.
You should have received a copy of the GNU Affero General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
See LICENSE.
A few files have been taken from the WebAssembly reference interpreter. They are licensed under the Apache License 2.0 and have a different copyright which is stated in the header of the files.
Some code has been taken from the base library from Jane Street. It is licensed under the MIT License and have a different copyright which is stated in the header of the files.
Some code has been taken from the E-ACSL plugin of Frama-C. It is licensed under the GNU Lesser General Public License 2.1 and have a different copyright which is stated in the header of the files.
Funding
This project was partly funded through the NGI0 Core Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme. See Owi project on NLnet.
Changelog
See CHANGELOG.