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]