|
| 1 | +from z3 import * |
| 2 | + |
| 3 | +data = """0x00081002 == 0x00001000 |
| 4 | +0x00029065 == 0x00029061 |
| 5 | +0x00000000 == 0x00000000 |
| 6 | +0x00016c40 == 0x00016c00 |
| 7 | +0x00020905 == 0x00000805 |
| 8 | +0x00010220 == 0x00000220 |
| 9 | +0x00098868 == 0x00080860 |
| 10 | +0x00021102 == 0x00021000 |
| 11 | +0x00000491 == 0x00000481 |
| 12 | +0x00031140 == 0x00001000 |
| 13 | +0x00000801 == 0x00000000 |
| 14 | +0x00060405 == 0x00000400 |
| 15 | +0x0000c860 == 0x00000060 |
| 16 | +0x00000508 == 0x00000400 |
| 17 | +0x00040900 == 0x00000800 |
| 18 | +0x00012213 == 0x00010003 |
| 19 | +0x000428c0 == 0x00000840 |
| 20 | +0x0000840c == 0x0000000c |
| 21 | +0x00043500 == 0x00002000 |
| 22 | +0x0008105a == 0x00001000""".split("\n") |
| 23 | + |
| 24 | +s = Solver() |
| 25 | +cons = [] |
| 26 | + |
| 27 | +for i in data: |
| 28 | + temp = i.split(" == ") |
| 29 | + cons.append((int(temp[0], 16), int(temp[1], 16))) |
| 30 | + |
| 31 | +bits = [] |
| 32 | +for i in range(20): |
| 33 | + a = [] |
| 34 | + for j in range(20): |
| 35 | + test = BitVec("f" + str(i).zfill(2) + str(j).zfill(2), 8) |
| 36 | + s.add(Or(test == 0, test == 1)) |
| 37 | + a.append(test) |
| 38 | + bits.append(a) |
| 39 | +print(bits) |
| 40 | + |
| 41 | +for i in range(len(cons)): |
| 42 | + for j in range(20): |
| 43 | + mask = (cons[i][0] >> j) & 1 |
| 44 | + bit = (cons[i][1] >> j) & 1 |
| 45 | + if mask == 1: |
| 46 | + # print(bits[i][j]) |
| 47 | + s.add(bits[i][j] == BitVecVal(bit, 8)) |
| 48 | + |
| 49 | +for i in range(20): |
| 50 | + tot = 0 |
| 51 | + tot2 = 0 |
| 52 | + for j in range(20): |
| 53 | + tot += bits[i][j] |
| 54 | + tot2 += bits[j][i] |
| 55 | + s.add(tot == BitVecVal(10, 8)) |
| 56 | + s.add(tot2 == BitVecVal(10, 8)) |
| 57 | + |
| 58 | +for i in range(20): |
| 59 | + for j in range(i + 1, 20): |
| 60 | + conds = [] |
| 61 | + conds2 = [] |
| 62 | + for k in range(20): |
| 63 | + conds.append(bits[i][k] != bits[j][k]) |
| 64 | + conds2.append(bits[k][i] != bits[k][j]) |
| 65 | + s.add(reduce(Or, conds)) |
| 66 | + s.add(reduce(Or, conds2)) |
| 67 | + |
| 68 | +for i in range(18): |
| 69 | + for j in range(20): |
| 70 | + cur = bits[i][j] + bits[i + 1][j] + bits[i + 2][j] |
| 71 | + cur2 = bits[j][i] + bits[j][i + 1] + bits[j][i + 2] |
| 72 | + s.add(cur != BitVecVal(3, 8)) |
| 73 | + s.add(cur != BitVecVal(0, 8)) |
| 74 | + s.add(cur2 != BitVecVal(3, 8)) |
| 75 | + s.add(cur2 != BitVecVal(0, 8)) |
| 76 | + |
| 77 | +print(s.check()) |
| 78 | +m = s.model() |
| 79 | +print(m) |
| 80 | + |
| 81 | +sices = [] |
| 82 | +for i in range(20): |
| 83 | + sice = "" |
| 84 | + for j in range(20): |
| 85 | + sice += str(m.eval(bits[i][j])) |
| 86 | + sices.append(int(sice[::-1], 2)) |
| 87 | + # print(bin(sices[-1])[2:].zfill(20)) |
| 88 | + print(sices[-1]) |
| 89 | +for i in range(20): |
| 90 | + print(sices[i] & cons[i][0] == cons[i][1]) |
| 91 | + |
| 92 | + |
0 commit comments