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
}
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 ./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++ ./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 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!
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 = u32::symbol(); // TODO: replace by usize::symbol()
let res = f(x.try_into().unwrap());
}
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 ./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++ ./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]
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() {}