From d8b31701db213ea95fa1953b83e03fa017764342 Mon Sep 17 00:00:00 2001
From: zapashcanon <leo@ndrs.fr>
Date: Mon, 16 Oct 2023 16:25:34 +0200
Subject: [PATCH] add symbolic instructions in the README

---
 README.md           | 67 +++++++++++++++++++++++++++++++++++++++++++++
 test/mini_test.wast |  2 +-
 2 files changed, 68 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 9838f34eb..df3ca16b4 100644
--- a/README.md
+++ b/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.
diff --git a/test/mini_test.wast b/test/mini_test.wast
index 9b363ab0c..be4a73a63 100644
--- a/test/mini_test.wast
+++ b/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
     ))