Owi User’s Manual

This is the user manual of Owi. For more general information, have a look at Owi’s git repository.

If it looks interesting to you, you can check out the Quickstart.

Comparison with other tools

Quickstart

Finding a crash in a function

Let’s say you wrote a function f and want to check if it can crash for some input. The function could for instance be the following one (choose your programming language to get a specialized example):

int f(int x) {

  int arr[4] = {1, 2, 0, 4};

  if (x >= 0 && x < 4) {
    return 10 / arr[x];
  }

  return -1;
}

extern "C" int f(int x) {

  int arr[4] = {1, 2, 0, 4};

  if (x >= 0 && x < 4) {
    return 10 / arr[x];
  }

  return -1;
}

package main

//go:export f
func f(x int32) int32 {
	arr := [4]int32{1, 2, 0, 4}

	if x >= 0 && x < 4 {
		return 10 / arr[x]
	}

	return -1
}

// main is required by the tinygo compiler, even if it isn't used.
func main() {}

#![no_main]

#[no_mangle]
pub extern "C" fn f(x: usize) -> i32 {

  let arr = [1, 2, 0, 4];

  if x < arr.len() {
    return 10 / arr[x];
  }

  -1
}

export fn f(x: usize) i32 {

  const arr = [_]i32{ 1, 2, 0, 4 };

  if (x < arr.len) {
    return @divTrunc(10, arr[x]);
  }

  return -1;
}

(module
  (memory 1)
  (func $f (export "f") (param $x i32) (result i32)
    (local $value i32)

    (i32.store (i32.mul (i32.const 4) (i32.const 0)) (i32.const 1))
    (i32.store (i32.mul (i32.const 4) (i32.const 1)) (i32.const 2))
    (i32.store (i32.mul (i32.const 4) (i32.const 2)) (i32.const 0))
    (i32.store (i32.mul (i32.const 4) (i32.const 3)) (i32.const 4))

    (if (i32.ge_u (local.get $x) (i32.const 4) )
      (then (return (i32.const -1))))

    (local.set $value
      (i32.load
        (i32.mul
          (local.get $x)
          (i32.const 4))))

    (i32.div_s
      (i32.const 10)
      (local.get $value))
  )
)

We are going to use owi to look for a crash in the function. Owi has one subcommand for each programming language it supports. For instance, if you are analyzing a C program the command will be owi c <...>, whereas for a Rust program it will be owi rust <...>.

Then, we use the --entry-point=f option to tell Owi to starts its analysis on the function we are interested in.

Finally, we use the --invoke-with-symbols option to tell Owi it should invoke the functions with symbolic values. Here, it means that x will be a value representing “any possible integer”, and not a concrete one. You’ll learn more about this in the next example. What you should remember is that it allows Owi to check all possible execution path, for any value of x.

All the others parameters are only here to make the output deterministic while generating the documentation and you should ignore them.

$ owi c sym ./f.c --entry-point=f --invoke-with-symbols --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: integer divide by zero
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi c++ sym ./f.cpp --entry-point=f --invoke-with-symbols --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: integer divide by zero
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi go sym ./f.go --entry-point=f --invoke-with-symbols --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: unreachable
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi rust sym ./f.rs --entry-point=f --invoke-with-symbols --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: unreachable
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi zig sym ./f.zig --entry-point=f --invoke-with-symbols --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: unreachable
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi wasm sym ./f.wat --entry-point=f --invoke-with-symbols --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: integer divide by zero
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

Owi says he reached a trap, which corresponds to a programming error. The exact trap depends on the input language and how it is compiled to Wasm. But here it’ll either be “integer divide by zero” or “unreachable”.

Then Owi gives us a model, that is, the set of input values of the program leading to this trap. The model is a list of symbols, each symbols representing an input.

Here we have a single symbol in the model, whose name is symbol_0, of type i32 and whose value is 2. And indeed, if we use 2 as the input value of the function f, there will be a crash in the program because of a division by zero!

Defining symbols by hand

In the previous example, we used the --invoke-with-symbol flag. It is useful for simple examples, but when building more involved inputs, it is better to get more control. This is achieved by defining symbols by hand instead of using the --invoke-with-symbol flag. Here is an example which is the exact same as the previous one, but where the unique symbol is created by hand through a function provided by Owi. We define this symbol in another function check which simply calls f with the symbol as input.

#include <owi.h>

int f(int x) {

  int arr[4] = {1, 2, 0, 4};

  if (x >= 0 && x < 4) {
    return 10 / arr[x];
  }

  return -1;
}

int check(void) {
  int x = owi_int();
  return f(x);
}

#include <owi.h>

int f(int x) {

  int arr[4] = {1, 2, 0, 4};

  if (x >= 0 && x < 4) {
    return 10 / arr[x];
  }

  return -1;
}

extern "C" int check(void) {
  int x = owi_int();
  return f(x);
}

package main

func f(x int32) int32 {
	arr := [4]int32{1, 2, 0, 4}

	if x >= 0 && x < 4 {
		return 10 / arr[x]
	}

	return -1
}


//go:wasm-module owi
//export i32_symbol
func i32_symbol() int32

//go:export check
func check() {
	var x int32 = i32_symbol()
	var _ int32 = f(x)
}

// main is required by the tinygo compiler, even if it isn't used.
func main() {}

#![no_main]

fn f(x: usize) -> i32 {

  let arr = [1, 2, 0, 4];

  if x < arr.len() {
    return 10 / arr[x];
  }

  -1
}

use owi_sym::Symbolic;

#[no_mangle]
pub extern "C" fn check() -> () {
  let x = usize::symbol();
  let res = f(x);
}

fn f(x: usize) i32 {

  const arr = [_]i32{ 1, 2, 0, 4 };

  if (x < arr.len) {
    return @divTrunc(10, arr[x]);
  }

  return -1;
}

extern "owi" fn i32_symbol() usize;

export fn check() void {
  const x: usize = i32_symbol();
  _ = &f(x);
}

(module
  (import "owi" "i32_symbol" (func $i32_symbol (result i32)))
  (memory 1)

  (func $f (param $x i32) (result i32)
    (local $value i32)

    (i32.store (i32.mul (i32.const 4) (i32.const 0)) (i32.const 1))
    (i32.store (i32.mul (i32.const 4) (i32.const 1)) (i32.const 2))
    (i32.store (i32.mul (i32.const 4) (i32.const 2)) (i32.const 0))
    (i32.store (i32.mul (i32.const 4) (i32.const 3)) (i32.const 4))

    (if (i32.ge_u (local.get $x) (i32.const 4) )
      (then (return (i32.const -1))))

    (local.set $value
      (i32.load
        (i32.mul
          (local.get $x)
          (i32.const 4))))

    (i32.div_s
      (i32.const 10)
      (local.get $value))
  )

  (func $check (export "check")
    call $i32_symbol
    call $f
    drop
  )
)

The invokation on Owi is the same as in the previous example, we simply removed the --invoke-with-symbol flag and changed the entry point from f to check.

$ owi c sym ./f_byhand.c --entry-point=check --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: integer divide by zero
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi c++ sym ./f_byhand.cpp --entry-point=check --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: integer divide by zero
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi go sym ./f_byhand.go --entry-point=check --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: unreachable
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi rust sym ./f_byhand.rs --entry-point=check --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: unreachable
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi zig sym ./f_byhand.zig --entry-point=check --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: unreachable
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

$ owi wasm sym ./f_byhand.wat --entry-point=check --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Trap: integer divide by zero
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

Checking the equivalence of two functions

Here, we have two functions that we expect to be the same but we are not completely sure. This can be the case for instance when refactoring or optimizing a given function. Owi can check that the old one is equivalent to the new one.

We have the original function, mean_old, that computes the mean of two integers. Then, we define the new function, mean_new, which we expect to do the same. Then, our main function is creating two symbolic integers, n1 and n2, and asserts that the two functions always return the same value when given these symbolic integers as input.

#include <owi.h>

int mean1(int x, int y) {
  return (x & y) + ((x ^ y) >> 1);
}

int mean2(int x, int y) {
  return (x + y) / 2;
}

void check(int x, int y) {
  owi_assert(mean1(x, y) == mean2(x, y));
}

#include <owi.h>

int mean1(int x, int y) {
  return (x & y) + ((x ^ y) >> 1);
}

int mean2(int x, int y) {
  return (x + y) / 2;
}

extern "C" void check(int x, int y) {
  owi_assert(mean1(x, y) == mean2(x, y));
}

package main

//go:wasm-module owi
//export assert
func owi_assert(bool)


func mean1(x, y int32) int32 {
	return (x & y) + ((x ^ y) >> 1)
}

func mean2(x, y int32) int32 {
	return (x + y) / 2
}

//go:export check
func check(x, y int32) {
	owi_assert(mean1(x, y) == mean2(x, y))
}

// main is required by the tinygo compiler, even if it isn't used.
func main() {}

#![no_main]

fn mean1(x: i32, y: i32) -> i32 {
    (x & y) + ((x ^ y) >> 1)
}

fn mean2(x: i32, y: i32) -> i32 {
    (x + y) / 2
}

#[no_mangle]
pub extern "C" fn check(x : i32, y: i32) {
  owi_sym::assert(mean1(x, y) == mean2(x, y))
}

extern "owi" fn assert(bool) void;

fn mean1(x: i32, y: i32) i32 {
  return (x & y) + ((x ^ y) >> 1);
}

fn mean2(x: i32, y: i32) i32 {
  return @divTrunc(x + y, 2);
}

export fn check(x: i32, y: i32) void {
  assert(mean1(x, y) == mean2(x, y));
}

(module
  (func $mean1 (param $x i32) (param $y i32) (result i32)
    local.get $x
    local.get $y
    i32.and

    local.get $x
    local.get $y
    i32.xor
    i32.const 1
    i32.shr_s

    i32.add
  )

  (func $mean2 (param $x i32) (param $y i32) (result i32)
    local.get $x
    local.get $y
    i32.add
    i32.const 2
    i32.div_s
  )

  (func $check  (export "check") (param $x i32) (param $y i32)
    local.get $x
    local.get $y
    call $mean1

    local.get $x
    local.get $y
    call $mean2

    i32.ne
    if
      unreachable
    end
  )
)

We can now run Owi on our program to check if they are the same:

$ owi c sym ./mean.c --entry-point=check --invoke-with-symbols --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 -1570748002
  symbol symbol_1 i32 -1425538774
}
owi: [ERROR] Reached problem!
[13]

$ owi c++ sym ./mean.cpp --entry-point=check --invoke-with-symbols --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 -1570748002
  symbol symbol_1 i32 -1425538774
}
owi: [ERROR] Reached problem!
[13]

$ owi go sym ./mean.go --entry-point=check --invoke-with-symbols --no-assert-failure-expression-printing --verbosity=error
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 -2147483648
  symbol symbol_1 i32 -2147483646
}
owi: [ERROR] Reached problem!
[13]

$ owi rust sym ./mean.rs --entry-point=check --invoke-with-symbols -w1 --fail-on-assertion-only --no-assert-failure-expression-printing --deterministic-result-order
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 755812345
  symbol symbol_1 i32 -755812346
}

owi: [ERROR] Reached problem!
[13]

$ owi zig sym ./mean.zig --entry-point=check --invoke-with-symbols -w1 --fail-on-assertion-only --no-assert-failure-expression-printing --deterministic-result-order
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 -1001584422
  symbol symbol_1 i32 -72157403
}

owi: [ERROR] Reached problem!
[13]

$ owi wasm sym ./mean.wat --entry-point=check --invoke-with-symbols
owi: [ERROR] Trap: unreachable
model {
  symbol symbol_0 i32 -2147483648
  symbol symbol_1 i32 -2147483646
}
owi: [ERROR] Reached problem!
[13]

And indeed, in the mean1 function, when using these values, there will be an overflow, leading to a wrong result.

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 "owi" "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 wasm 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 wasm replay --replay-file mini.scfg mini.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 18 (executed 0 times)
owi: [INFO] calling func  : func start
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 0 (executed 0 times)
owi: [INFO] stack         : [ i32.const 6 ]
owi: [INFO] running instr : local.set 0 (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 5 (executed 0 times)
owi: [INFO] stack         : [ i32.const 5 ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ i32.const 6 ; i32.const 5 ]
owi: [INFO] running instr : i32.lt_s (executed 0 times)
owi: [INFO] stack         : [ i32.const 1 ]
owi: [INFO] running instr : if (executed 0 times)
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : unreachable (executed 0 times)
owi: [ERROR] unreachable
[96]

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 wasm 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] checking     ...
owi: [INFO] typechecking ...
owi: [INFO] compiling ./mul2.wat
owi: [INFO] parsing      ...
owi: [INFO] checking     ...
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 39 (executed 0 times)
owi: [INFO] calling func  : func start
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ]
owi: [INFO] running instr : call 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_1 ; symbol_0 ]
owi: [INFO] running instr : call 38 (executed 0 times)
owi: [INFO] calling func  : func check_iso_func
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ]
owi: [INFO] running instr : local.get 1 (executed 0 times)
owi: [INFO] stack         : [ symbol_1 ; symbol_0 ]
owi: [INFO] running instr : call 28 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ]
owi: [INFO] running instr : local.get 1 (executed 0 times)
owi: [INFO] stack         : [ symbol_1 ; symbol_0 ]
owi: [INFO] running instr : i32.mul (executed 0 times)
owi: [INFO] stack         : [ (i32.mul symbol_0 symbol_1) ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ; (i32.mul symbol_0 symbol_1) ]
owi: [INFO] running instr : local.get 1 (executed 0 times)
owi: [INFO] stack         : [ symbol_1 ; symbol_0 ; (i32.mul symbol_0
                                                     symbol_1) ]
owi: [INFO] running instr : call 30 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : local.get 1 (executed 0 times)
owi: [INFO] stack         : [ symbol_1 ]
owi: [INFO] running instr : local.get 0 (executed 0 times)
owi: [INFO] stack         : [ symbol_0 ; symbol_1 ]
owi: [INFO] running instr : i32.mul (executed 0 times)
owi: [INFO] stack         : [ (i32.mul symbol_1 symbol_0) ]
owi: [INFO] running instr : i32.const 1 (executed 0 times)
owi: [INFO] stack         : [ 1 ; (i32.mul symbol_1 symbol_0) ]
owi: [INFO] running instr : i32.add (executed 0 times)
owi: [INFO] stack         : [ (i32.add (i32.mul symbol_1 symbol_0) 1) ;
            (i32.mul symbol_0 symbol_1) ]
owi: [INFO] running instr : i32.eq (executed 0 times)
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 8 (executed 0 times)
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: 2
owi: [ERROR] Reached problem!
[13]

Bugs Found by Owi

• Wrong neutral element of <fNN as iter::Sum> in the Rust standard library

Code Coverage Criteria

When we write tests for a codebase, it is common to wonder how good is the test-suite. One way to measure it is through code coverage. That is: how much how the code base is covered by the tests? Most of the time, this notion is not precise. Most tools measuring code coverage can give you a percentage of the coverage, without a clear definition.

Yet there exists some precise definitions for various ways of measuring code coverage. They are called code coverage criteria.

Function Coverage

The easiest one is called function coverage (FC). It measure the percentage of the functions of your programs that are called by the test-suite. For instance, if your whole code base has only two functions, and in your test-suite, only one of them gets execution, then it means you have a function coverage of 50%.

Statement Coverage

This criteria (SC) measure the percentage of instructions of your program that are executed.

Decision Coverage

This criteria (DC) measure the percentage of decisions covered for you test-suite. For instance, if you have some code looking like the following:

void f(int x) {
  if (x) {
    // A
  } else {
    // B
  }
}

When the conditional is reached, there are two possible decisions. If x is true, then, we execute A. If x is false, then, we execute B.

Condition Coverage

This criteria (CC) … TODO

TODO

All the others (MC/DC)

TODO: explain that there is a correspondence with the CFG (covering nodes versus covering edges and such)

References

TODO

Labels

There exists many code coverage criteria. Having to implement a different mechanism for all of them is tedious. This is a problem solved by labels.

Labels are annotations added to a program (often via an instrumentation pass). Each label correspond to a point that must be reached by the test-suite. The percentage of labels reached by the test-suite is the percentage of code coverage for the criteria that was chosen when adding labels.

Example

For instance, if we are interested in the following program:

void f(void) {
  // A
}

void g(void) {
  // B
}

We could instrument the program to add labels for the FC criteria this way:

void f(void) {
  label_reached(0);
  // A
}

void g(void) {
  label_reached(1);
  // B
}

Then, by providing an appropriate definition of label_reached and knowing how many of them are in the program, we can count how many of them are reached by the test-suite by running it on the instrumented program. Then, we can compute the percentage of code coverage for the FC criteria.

Labels in Owi

Owi has the ability to :

1. Annotate a Wasm program with labels for a few criteria (see the owi instrument label sub-command).
2. Generate tests for annotated programs in order to automatically get a high code coverage percentage (run your program with owi sym instrumented.wasm.

TODO: complete example with more details on test-case generation

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 = malloc(MAX_SIZE * sizeof(int));

  int n = owi_int("n");
  owi_assume(n >= 2);
  owi_assume(n <= MAX_SIZE);

  primes(is_prime, n);
  free(is_prime);
  return 0;
}

$ owi c sym --e-acsl primes.c -w1
owi: [ERROR] Assert failure: false
model {
  symbol symbol_0 i32 2 n
}
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_int("n");
  owi_assume(n >= 2);
  owi_assume(n <= MAX_SIZE);

  primes(is_prime, n);
  free(is_prime);
  return 0;
}

$ owi c sym --e-acsl primes2.c -w1
All OK!

All the specified properties have been satisfied during the execution.

Examples of Problem Solving

Solving polynomials

#include <owi.h>

int main() {
  int x = owi_int();
  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;
}

$ owi c sym ./poly.c -w1 --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 4
}
owi: [ERROR] Reached problem!
[13]

#include <owi.h>

int main() {
  int x = owi_int();
  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;
}

$ owi c sym ./poly2.c --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 -2147483644
}
owi: [ERROR] Reached problem!
[13]

#include <owi.h>

class Poly {
private:
  int poly;
public:
  Poly(int a, int b, int c, int d) {
    int x = owi_int();
    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()));
}

$ owi c++ sym ./poly.cpp -w1 --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 2
}
owi: [ERROR] Reached problem!
[13]

#include <owi.h>

class Poly {
private:
  int poly;
public:
  Poly(int a, int b, int c, int d) {
    int x = owi_int();
    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()));
}

$ owi c++ sym ./poly2.cpp --no-assert-failure-expression-printing
owi: [ERROR] Assert failure
model {
  symbol symbol_0 i32 -2147483644
}
owi: [ERROR] Reached problem!
[13]

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_char();
  }

  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 sym ./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_unsigned_int();
        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 sym ./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]

Rust: cargo owi

A Cargo subcommand to run Rust programs through Owi’s symbolic execution engine for automated bug finding.

cargo-owi compiles your crate to WebAssembly and passes it to owi for symbolic analysis.

Prerequisites

• owi must be installed and available on $PATH
• The wasm32-unknown-unknown target must be installed: rustup target add wasm32-unknown-unknown
• Your crate should use the owi library to declare symbolic values and assumptions

Installation

$ cargo install cargo-owi

Usage

cargo owi sym [OPTIONS] [-- [OWI_OPTIONS]]

Run symbolic execution on the current package:

$ cargo owi sym

Pass extra options to owi after --:

$ cargo owi sym -- --timeout 60

Options

Any arguments after -- are forwarded verbatim to owi sym.

Example

Add symbolic inputs to your code using the owi crate:

fn add(a: i32, b: i32) -> i32 {
    a + b
}

fn main() {
    let x: i32 = owi::symbolic();
    let y: i32 = owi::symbolic();
    owi::assume(x > 0 && y > 0);
    assert!(add(x, y) > 0);
}

Then run:

cargo owi sym

Owi will explore execution paths symbolically and report any path that violates an assertion or triggers undefined behavior.

Concrete Interpreter

Concrete 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 wasm run ./42.wat

Nothing is happening, so you can add the -v option to print an execution trace:

$ owi wasm run ./42.wat -v
owi: [INFO] parsing      ...
owi: [INFO] checking     ...
owi: [INFO] checking     ...
owi: [INFO] typechecking ...
owi: [INFO] linking      ...
owi: [INFO] interpreting ...
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 0 (executed 0 times)
owi: [INFO] calling func  : func f
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 20 (executed 0 times)
owi: [INFO] stack         : [ i32.const 20 ]
owi: [INFO] running instr : i32.const 22 (executed 0 times)
owi: [INFO] stack         : [ i32.const 22 ; i32.const 20 ]
owi: [INFO] running instr : i32.add (executed 0 times)
owi: [INFO] stack         : [ i32.const 42 ]
owi: [INFO] running instr : drop (executed 0 times)

Converter

Wasm2wat

Given a file 42.wasm, you can convert it to result.wat and then run it:

$ owi wasm to_wat 42.wasm -o result.wat
$ cat result.wat
(module
  (type (func))
  (func
    i32.const 20
    i32.const 22
    i32.add
    drop
  )
  (start 0)
)
$ owi wasm run result.wat -v
owi: [INFO] parsing      ...
owi: [INFO] checking     ...
owi: [INFO] checking     ...
owi: [INFO] typechecking ...
owi: [INFO] linking      ...
owi: [INFO] interpreting ...
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 0 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 20 (executed 0 times)
owi: [INFO] stack         : [ i32.const 20 ]
owi: [INFO] running instr : i32.const 22 (executed 0 times)
owi: [INFO] stack         : [ i32.const 22 ; i32.const 20 ]
owi: [INFO] running instr : i32.add (executed 0 times)
owi: [INFO] stack         : [ i32.const 42 ]
owi: [INFO] running instr : drop (executed 0 times)

Wat2wasm

Given a file 42.wat, you can convert it to result.wasm and then run it:

$ owi wasm of_wat 42.wat -o result.wasm
$ owi wasm run result.wasm -v
owi: [INFO] typechecking ...
owi: [INFO] linking      ...
owi: [INFO] interpreting ...
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : call 0 (executed 0 times)
owi: [INFO] calling func  : func anonymous
owi: [INFO] stack         : [  ]
owi: [INFO] running instr : i32.const 20 (executed 0 times)
owi: [INFO] stack         : [ i32.const 20 ]
owi: [INFO] running instr : i32.const 22 (executed 0 times)
owi: [INFO] stack         : [ i32.const 22 ; i32.const 20 ]
owi: [INFO] running instr : i32.add (executed 0 times)
owi: [INFO] stack         : [ i32.const 42 ]
owi: [INFO] running instr : drop (executed 0 times)

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 wasm 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
    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
      )
    )
    local.get $n
    i32.const 4
    i32.mul
    i32.load
    return
  )
)

Are you able to recognize the program now?

Program Analyzer

Call Graph

Given a file useless.wat with the following content:

(module

  (func $start
    i32.const 0
    (if
    (then call $a)
    (else call $b)
    )
  )

  (func $a 
  (block
  call $b)
  call $c)

  (func $b)

  (func $c)

  (start $start))

You can then create a file useless.dot containing the call graph of the programm:

$ owi wasm analyze cg useless.wat

Control-Flow Graph

Given a file useless.wat with the following content:

(module
    (func $foo (param i32) (result i32)
       (local i32)
       (block
           (block
               (block
                   local.get 0
                   i32.eqz
                   br_if 0

                   local.get 0
                   i32.const 1
                   i32.eq
                   br_if 1

                   i32.const 7
                   local.set 1
                   br 2)
             i32.const 42
             local.set 1
             br 1)
         i32.const 99
         local.set 1)
       local.get 1)
)

You can then create a file useless.dot containing the control flow graph of the function foo:

$ owi wasm analyze cfg useless.wat --entry-point=foo

Script Interpreter

Script Interpreter 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 wasm script concrete ./print.wast
42

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 wasm 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 wasm validate ./type_error.wat -v
owi: [INFO] parsing      ...
owi: [INFO] checking     ...
owi: [INFO] checking     ...
owi: [INFO] typechecking ...
owi: [ERROR] type mismatch (expected [i32 i32] but stack is [i32])
[35]

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      ...
...
# let env = Env.Concrete.empty ~context:()
val env : Env.Concrete.t = <abstr>
# let modul, env =
    match Compile.Text.until_concrete_link env ~unsafe:false ~name:None m with
    | Ok v -> v
    | Error _ -> assert false;;
mdx_gen.bc.exe: [INFO] checking     ...
mdx_gen.bc.exe: [INFO] checking     ...
mdx_gen.bc.exe: [INFO] typechecking ...
...
mdx_gen.bc.exe: [INFO] linking      ...
...
# module I = Interpret.Concrete (Interpret.Default_parameters);;
module I :
  sig
    val modul :
      env:Env.Concrete.t ->
      modul:Env.Concrete.modul -> Env.Concrete.t Owi__Concrete_choice.t
  end
# let () =
    match I.modul ~env ~modul with
    | Ok _env -> ()
    | Error _ -> assert false;;
mdx_gen.bc.exe: [INFO] interpreting ...
mdx_gen.bc.exe: [INFO] stack         : [  ]
mdx_gen.bc.exe: [INFO] running instr : call 0 (executed 0 times)
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 (executed 0 times)
mdx_gen.bc.exe: [INFO] stack         : [ i32.const 24 ]
mdx_gen.bc.exe: [INFO] running instr : i32.const 24 (executed 0 times)
mdx_gen.bc.exe: [INFO] stack         : [ i32.const 24 ; i32.const 24 ]
mdx_gen.bc.exe: [INFO] running instr : i32.add (executed 0 times)
mdx_gen.bc.exe: [INFO] stack         : [ i32.const 48 ]
mdx_gen.bc.exe: [INFO] running instr : drop (executed 0 times)

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.Module.t =
  (* some custom functions *)
  let rint : Concrete_i32.t ref Type.Id.t = Type.Id.make () in
  let fresh i = Ok (ref i) in
  let set r (i : Concrete_i32.t) =
    r := i;
    Ok ()
  in
  let get r = Ok !r in
  let print_i32 (i : Concrete_i32.t) =
    Format.printf "%a\n%!" Concrete_i32.pp i;
    Ok ()
  in
  (* we need to describe their types *)
  let open Concrete_extern.Func in
  let open Concrete_extern.Func.Syntax in
  [ ("print_i32", Extern_func (i32 ^->. unit, print_i32))
  ; ("fresh", Extern_func (i32 ^->. externref rint, fresh))
  ; ("set_i32r", Extern_func (externref rint ^-> i32 ^->. unit, set))
  ; ("get_i32r", Extern_func (externref rint ^->. i32, get))
  ]

(* an environment that contains our custom module, available under the name `sausage` *)
let env =
  let env = Env.Concrete.empty ~context:() in
  Env.Concrete.link_extern_module ~env ~name:"sausage" extern_module
  |> Stdlib.Result.get_ok

(* a pure wasm module refering to `sausage` *)
let pure_wasm_module =
  Parse.Text.Module.from_file (Fpath.v "extern.wat") |> Stdlib.Result.get_ok

(* our pure wasm module, linked with `sausage` *)
let modul, env =
  Compile.Text.until_concrete_link env ~unsafe:false ~name:None pure_wasm_module
  |> Stdlib.Result.get_ok

module I = Interpret.Concrete (Interpret.Default_parameters)

(* let's run it ! it will print the values as defined in the print_i32 function *)
let () =
  match I.modul ~env ~modul with Error _o -> assert false | Ok _env -> ()

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.Module.t =
  (* some custom functions *)
  let memset m start byte length =
    let rec loop offset =
      let b = Concrete_i32.le offset length |> Concrete_boolean.to_bool in
      if b then
        begin match
          Concrete_memory.store_8 m ~addr:(Concrete_i32.add start offset) byte
        with
        | Error _ as e -> e
        | Ok _mem -> loop (Concrete_i32.add offset (Concrete_i32.of_int 1))
        end
      else Ok ()
    in
    loop Concrete_i32.zero
  in
  let print_x64 (n : Concrete_i64.t) =
    let n = Concrete_i64.to_int64 n in
    Format.printf "0x%LX@\n" n;
    Ok ()
  in
  (* we need to describe their types *)
  let open Concrete_extern.Func in
  let open Concrete_extern.Func.Syntax in
  [ ("print_x64", Extern_func (i64 ^->. unit, print_x64))
  ; ("memset", Extern_func (memory 0 ^-> i32 ^-> i32 ^-> i32 ^->. unit, memset))
  ]

(* an environment that contains our custom module, available under the name `chorizo` *)
let env =
  let env = Env.Concrete.empty ~context:() in
  Env.Concrete.link_extern_module ~env ~name:"chorizo" extern_module
  |> Stdlib.Result.get_ok

(* 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 modul, env =
  match
    Compile.Text.until_concrete_link env ~unsafe:false ~name:None
      pure_wasm_module
  with
  | Error _ -> assert false
  | Ok v -> v

module I = Interpret.Concrete (Interpret.Default_parameters)

(* let's run it ! it will print the values as defined in the print_i64 function *)
let () =
  match I.modul ~env ~modul with Error _ -> assert false | Ok _env -> ()

Running the above program should yield:

$ ./extern_mem.exe
0xAAAAAAAAAAAAAAAA