Merge pull request #1319 from serpilliere/fix_z3_div_add_simpl

Fix z3 div; add simpl

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"]])