1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
import z3
from miasm.ir.translators import Translator
from miasm.expression.expression import *
translator = Translator.to_language("z3")
values = [
(42, 10, 4, 2),
(-42, 10, -4, -2),
(42, -10, -4, 2),
(-42, -10, 4, -2)
]
for a, b, c, d in values:
cst_a = ExprInt(a, 8)
cst_b = ExprInt(b, 8)
div_result = ExprInt(c, 8)
div = ExprOp("sdiv", cst_a, cst_b)
print("%d / %d == %d" % (a, b, div_result))
solver = z3.Solver()
print("%s == %s" %(div, div_result))
eq1 = translator.from_expr(div) != translator.from_expr(div_result)
solver.add(eq1)
result = solver.check()
assert result == z3.unsat
mod_result = ExprInt(d, 8)
print("%d %% %d == %d" % (a, b, mod_result))
res2 = ExprOp("smod", cst_a, cst_b)
solver = z3.Solver()
print("%s == %s" %(res2, mod_result))
eq2 = translator.from_expr(res2) != translator.from_expr(mod_result)
solver.add(eq2)
result = solver.check()
assert result == z3.unsat
|