diff options
| -rw-r--r-- | test/expression/z3_div.py | 37 | ||||
| -rwxr-xr-x | test/test_all.py | 4 |
2 files changed, 41 insertions, 0 deletions
diff --git a/test/expression/z3_div.py b/test/expression/z3_div.py new file mode 100644 index 00000000..d436634b --- /dev/null +++ b/test/expression/z3_div.py @@ -0,0 +1,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 + diff --git a/test/test_all.py b/test/test_all.py index 2670761b..c2391572 100755 --- a/test/test_all.py +++ b/test/test_all.py @@ -332,6 +332,10 @@ testset += RegressionTest(["simplifications.py", "--z3"], base_dir="expression", tags=[TAGS["z3"]]) +testset += RegressionTest(["z3_div.py"], + base_dir="expression", + tags=[TAGS["z3"]]) + ## ObjC/CHandler testset += RegressionTest(["test_chandler.py"], base_dir="expr_type", tags=[TAGS["cparser"]]) |