-rwxr-xr-x 1987 djbsort-20180717/verif/unroll
#!/usr/bin/env python2
import sys
import angr
symbol = sys.argv[1]
n = int(sys.argv[2])
executable = sys.argv[3]
proj = angr.Project(executable)
state = proj.factory.full_init_state()
state.options -= {angr.options.SIMPLIFY_REGISTER_WRITES}
state.options -= {angr.options.SIMPLIFY_MEMORY_WRITES}
xaddr = proj.loader.find_symbol(symbol).rebased_addr
for i in range(n):
state.mem[xaddr + 4 * i].int = state.solver.BVS('in%d' % i,32)
simgr = proj.factory.simgr(state)
simgr.run()
exits = simgr.deadended
assert len(exits) == 1
walked = dict()
walknext = 0
def rename(op):
if op == '__add__': return 'add'
if op == '__sub__': return 'sub'
if op == '__mul__': return 'mul'
if op == '__or__': return 'or'
if op == '__xor__': return 'xor'
if op == '__and__': return 'and'
if op == '__invert__': return 'invert'
if op == '__eq__': return 'equal'
if op == '__rshift__': return 'signedrshift'
if op == 'SLE': return 'signedle'
if op == 'SLT': return 'signedlt'
return op
def informat(x):
if x.startswith('in'):
y = x[2:].split('_')
x = 'in_%s_%s' % (y[0],y[2])
return x
def walk(t):
global walknext
if t in walked: return walked[t]
if t.op == 'BVV':
walknext += 1
print 'v%d = constant(%d,%d)' % (walknext,t.size(),t.args[0])
elif t.op == 'BVS':
walknext += 1
print 'v%d = %s' % (walknext,informat(t.args[0]))
elif t.op == 'Extract':
assert len(t.args) == 3
input = 'v%d' % walk(t.args[2])
walknext += 1
print 'v%d = Extract(%s,%d,%d)' % (walknext,input,t.args[0],t.args[1])
else:
inputs = ['v%d' % walk(a) for a in t.args]
walknext += 1
if t.op == 'SGE':
t.op = 'SLE'
inputs = reversed(inputs)
if t.op == 'SGT':
t.op = 'SLT'
inputs = reversed(inputs)
print 'v%d = %s(%s)' % (walknext,rename(t.op),','.join(inputs))
walked[t] = walknext
return walknext
for i in range(n):
x = exits[0].mem[xaddr + 4 * i].int.resolved
print 'out%d = v%s' % (i,walk(x))