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]