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:

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_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_2 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
  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
}
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 n should be between 2 and MAX_SIZE
    • for all i between 0 and n - 1, is_prime + i should be memory locations safe to read and write
  • When the function returns,
    • for all i between 0 and n - 1, is_prime[i] evaluates to true if and only if i is larger than 2 and does not have a factor between 2 and i - 1 (which indicates the primality of i)

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 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:

(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 (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.

$ 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

Talks

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 (sub final  (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 (sub final  (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.

Projects and People Using Owi