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