1from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem 2 3def ADD(x, y): 4 return x + y 5 6def MUL(x, y): 7 return x * y 8 9def SUB(x, y): 10 return x - y 11 12def DIV(x, y): 13 return If(y == 0, 0, UDiv(x, y)) 14 15def SDIV(x, y): 16 return If(y == 0, 0, x / y) 17 18def MOD(x, y): 19 return If(y == 0, 0, URem(x, y)) 20 21def SMOD(x, y): 22 return If(y == 0, 0, x % y) 23 24def LT(x, y): 25 return If(ULT(x, y), BitVecVal(1, x.size()), BitVecVal(0, x.size())) 26 27def GT(x, y): 28 return If(UGT(x, y), BitVecVal(1, x.size()), BitVecVal(0, x.size())) 29 30def SLT(x, y): 31 return If(x < y, BitVecVal(1, x.size()), BitVecVal(0, x.size())) 32 33def SGT(x, y): 34 return If(x > y, BitVecVal(1, x.size()), BitVecVal(0, x.size())) 35 36def EQ(x, y): 37 return If(x == y, BitVecVal(1, x.size()), BitVecVal(0, x.size())) 38 39def ISZERO(x): 40 return If(x == 0, BitVecVal(1, x.size()), BitVecVal(0, x.size())) 41 42def AND(x, y): 43 return x & y 44 45def OR(x, y): 46 return x | y 47 48def NOT(x): 49 return ~(x) 50 51def SHL(x, y): 52 return y << x 53 54def SHR(x, y): 55 return LShR(y, x) 56 57def SAR(x, y): 58 return y >> x 59 60def BYTE(i, x): 61 bit = (i + 1) * 8 62 return If( 63 UGT(i, x.size() / 8 - 1), 64 BitVecVal(0, x.size()), 65 (LShR(x, (x.size() - bit))) & 0xff 66 ) 67 68def SIGNEXTEND(i, x): 69 bitBV = i * 8 + 7 70 bitInt = BV2Int(i) * 8 + 7 71 test = BitVecVal(1, x.size()) << bitBV 72 mask = test - 1 73 return If( 74 bitInt >= x.size(), 75 x, 76 If( 77 (x & test) == 0, 78 x & mask, 79 x | ~mask 80 ) 81 ) 82