1 files changed, 23 insertions, 0 deletions
diff --git a/example/symex.py b/example/symex.py
new file mode 100644
index 0000000..c5d13be
--- /dev/null
+++ b/example/symex.py
@@ -0,0 +1,23 @@
+import sys
+from satispi import *
+from example.program import *
+from example.symabs import *
+
+program = Program.from_file(sys.argv[1])
+worklist = [State(program, 0, [], None)]
+while worklist:
+    state = worklist.pop(0)
+
+    # Process state
+    print("Processing state ...")
+    exprs = [state.reg(reg) for reg in program.registers]
+    types = ["(_ BitVec 32)" for _ in program.registers]
+    cutoffs = [5 for _ in exprs]
+    possible = symabs(state.smtlib, exprs, types, cutoffs)
+    for reg, values in zip(program.registers, possible):
+        print("\t", reg, "\t->\t", values)
+
+    # Execute
+    for next_state in state.step():
+        if next_state.has_model():
+            worklist.append(next_state)