rev_realism400.py

#!/usr/bin/python
from z3 import *


orig = [0x61, 0x62, 0x63, 0x64, 0x65, 0x66, 0x67, 0x68, 0x69, 0x6a, 0x6b, 0x6c, 0x6d, 0x6e, 0x6f, 0x70]
shuf = [0x69, 0x6a, 0x6b, 0x6c, 0x6d, 0x6e, 0x6f, 0x70, 0x65, 0x66, 0x67, 0x68, 0x61, 0x62, 0x63, 0x64]

x = [0xb8, 0x13, 0x0, 0xcd, 0x10, 0xf, 0x20, 0xc0, 0x83, 0xe0, 0xfb, 0x83, 0xc8, 0x2, 0xf, 0x22]
d = [0x270,0x211,0x255,0x229,0x291,0x25E,0x233,0x1F9,0x278,0x27B,0x221,0x209,0x25D,0x290,0x28F,0x2DF]

x = x[8:]
d = d[0::2][::-1]
print map(hex, d)

s = Solver()
y = [BitVec("y%d" % i, 32) for i in xrange(8)]

for i in xrange(8):
    s.add(And(y[i] >= 0x0, y[i] < 0x80))

for i in xrange(8):
    #print map(hex, x)

    t = "+abs(%d - y[%d])"
    tt = ""
    for j in xrange(8):
        if j != i:
            tt = tt + t % (x[j], j)
        else:
            tt = tt + "+ %d" % (x[j])
    tt += " == %d" % d[i]
    print "s.add(%s)" % tt

    x = [0, 0, 0, 0, 0, 0, 0, 0]
    x[0] = d[i] % 256
    x[1] = d[i] / 256

def abs(x):
    return If(x >= 0,x,-x)

def get_result_from_z3(result):
    dic = {}
    for d in result.decls():
        dic[d.name().lstrip('S')] = result[d].as_long() 
    return dic

s.add(+ 131+abs(224 - y[1])+abs(251 - y[2])+abs(131 - y[3])+abs(200 - y[4])+abs(2 - y[5])+abs(15 - y[6])+abs(34 - y[7]) == 655)
s.add(+abs(143 - y[0])+ 2+abs(0 - y[2])+abs(0 - y[3])+abs(0 - y[4])+abs(0 - y[5])+abs(0 - y[6])+abs(0 - y[7]) == 605)
s.add(+abs(93 - y[0])+abs(2 - y[1])+ 0+abs(0 - y[3])+abs(0 - y[4])+abs(0 - y[5])+abs(0 - y[6])+abs(0 - y[7]) == 545)
s.add(+abs(33 - y[0])+abs(2 - y[1])+abs(0 - y[2])+ 0+abs(0 - y[4])+abs(0 - y[5])+abs(0 - y[6])+abs(0 - y[7]) == 632)
s.add(+abs(120 - y[0])+abs(2 - y[1])+abs(0 - y[2])+abs(0 - y[3])+ 0+abs(0 - y[5])+abs(0 - y[6])+abs(0 - y[7]) == 563)
s.add(+abs(51 - y[0])+abs(2 - y[1])+abs(0 - y[2])+abs(0 - y[3])+abs(0 - y[4])+ 0+abs(0 - y[6])+abs(0 - y[7]) == 657)
s.add(+abs(145 - y[0])+abs(2 - y[1])+abs(0 - y[2])+abs(0 - y[3])+abs(0 - y[4])+abs(0 - y[5])+ 0+abs(0 - y[7]) == 597)
s.add(+abs(85 - y[0])+abs(2 - y[1])+abs(0 - y[2])+abs(0 - y[3])+abs(0 - y[4])+abs(0 - y[5])+abs(0 - y[6])+ 0 == 624)



result = []
while s.check() == sat:
    m = s.model()
    dic = get_result_from_z3(m)
    msg = ''
    try:
        for i in sorted(dic):
            msg += chr(dic[i])

        print `msg`
    except:
        pass

    result.append(m)
    block = []
    for d in m:
         # d is a declaration
         if d.arity() > 0:
             raise Z3Exception("uninterpreted functions are not supported")
         # create a constant from declaration
         c = d()
         if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
             raise Z3Exception("arrays and uninterpreted sorts are not supported")
         block.append(c != m[d])
    s.add(Or(block))