-rwxr-xr-x 1265 djbsort-20180710/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()

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 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 = %d' % (walknext,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
    print 'v%d = %s(%s)' % (walknext,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))