diff options
author | Matthew Sotoudeh <matthew@masot.net> | 2023-07-14 07:25:31 -0700 |
---|---|---|
committer | Matthew Sotoudeh <matthew@masot.net> | 2023-07-14 07:25:31 -0700 |
commit | 0b12ba0ca00f7cdfb50b614fb24b673fb7e4e322 (patch) | |
tree | c8dc0b54c6f9df2f10185fc93f4276f1a8535802 /example/symex.py |
initial code
Diffstat (limited to 'example/symex.py')
-rw-r--r-- | example/symex.py | 23 |
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) |