blob: c5d13be7ac4b58ec1bff2baab48b0114b57915e5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
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)
|
