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;
}
#![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!
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));
}