add symbolic instructions in the README

README.md

@@ -16,6 +16,8 @@ If you can't or don't want to use `opam`, you can build the package with `dune b
 
 ## Quickstart
 
+### Concrete interpretation
+
 Given a file `test/passing/quickstart.wast` with the following content:
 
 <!-- $MDX file=test/passing/quickstart.wast -->
@@ -102,6 +104,71 @@ stack : [ ]
 
 For more, have a look at the [example] folder, at the [documentation] or at the [test suite].
 
+### Symbolic interpretation
+
+The interpreter can also be used in symbolic mode. This allows to find which input values are leading to a trap.
+
+Given a file `test/mini_test.wast` with the following content:
+
+<!-- $MDX file=test/mini_test.wast -->
+```wast
+(module
+ (import "print" "i32" (func $print_i32 (param i32)))
+ (import "symbolic" "i32" (func $gen_i32 (param i32) (result i32)))
+ (func $factR (export "fact") (param $n i32) (result i32)
+ local.get $n
+ local.get $n
+ i32.const 1
+ i32.eq
+ br_if 0
+ i32.const 1
+ i32.sub
+ call $factR
+ local.get $n
+ i32.mul
+ )
+
+ (func $start
+ (local $x i32)
+ (i32.const 123)
+ (call $print_i32)
+ (local.set $x (call $gen_i32 (i32.const 42)))
+ (if (i32.lt_s (i32.const 5) (local.get $x)) (then
+ unreachable
+ ))
+ (if (i32.gt_s (i32.const 1) (local.get $x)) (then
+ unreachable
+ ))
+ (local.get $x)
+ (call $factR)
+ (call $print_i32))
+
+ (start $start)
+)
+```
+
+You can run the symbolic interpreter through the `sym` command:
+```sh
+$ dune exec owi -- sym test/mini_test.wast
+(i32 123)
+CHOICE: (i32.lt_s (i32 5) x_1)
+PATH CONDITION:
+(i32.lt_s (i32 5) x_1)
+TRAP: unreachable
+CHOICE: (i32.gt_s (i32 1) x_1)
+CHOICE: (i32.eq x_1 (i32 1))
+Model:
+(model
+(x_1 i32 (i32 6))
+)
+Reached problem!
+
+x_1
+Solver time 0.003568s
+ calls 1
+ mean time 3.568000ms
+```
+
 ## Supported proposals
 
 The 🐌 status means the proposal is not applicable to owi.

test/mini_test.wast

@@ -18,7 +18,7 @@
  (local $x i32)
  (i32.const 123)
  (call $print_i32)
- (local.set $x (call $gen_i32 (i32.const 1)))
+ (local.set $x (call $gen_i32 (i32.const 42)))
  (if (i32.lt_s (i32.const 5) (local.get $x)) (then
  unreachable
  ))