From 0b12ba0ca00f7cdfb50b614fb24b673fb7e4e322 Mon Sep 17 00:00:00 2001 From: Matthew Sotoudeh Date: Fri, 14 Jul 2023 07:25:31 -0700 Subject: initial code --- example/symex.py | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 example/symex.py (limited to 'example/symex.py') 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) -- cgit v1.2.3