smt2_translator: added regression tests

2 files changed, 41 insertions, 1 deletions

diff --git a/test/ir/translators/smt2.py b/test/ir/translators/smt2.py
new file mode 100644
index 00000000..97877a3b
--- /dev/null
+++ b/test/ir/translators/smt2.py
@@ -0,0 +1,40 @@
+from z3 import Solver, unsat, parse_smt2_string
+from miasm2.expression.expression import *
+from miasm2.ir.translators.smt2 import TranslatorSMT2
+from miasm2.ir.translators.z3_ir import TranslatorZ3
+
+# create nested expression
+a = ExprId("a", 64)
+b = ExprId('b', 32)
+c = ExprId('c', 16)
+d = ExprId('d', 8)
+e = ExprId('e', 1)
+
+left = ExprCond(e + ExprOp('parity', a),
+                ExprMem(a * a, 64),
+                ExprMem(a, 64))
+
+cond = ExprSlice(ExprSlice(ExprSlice(a, 0, 32) + b, 0, 16) * c, 0, 8) << ExprOp('>>>', d, ExprInt(uint8(0x5L)))
+right = ExprCond(cond,
+                 a + ExprInt(uint64(0x64L)),
+                 ExprInt(uint64(0x16L)))
+
+e = ExprAff(left, right)
+
+# initialise translators
+t_z3 = TranslatorZ3()
+t_smt2 = TranslatorSMT2()
+
+# translate to z3
+e_z3 = t_z3.from_expr(e)
+# translate to smt2
+smt2 = t_smt2.to_smt2([t_smt2.from_expr(e)])
+
+# parse smt2 string with z3
+smt2_z3 = parse_smt2_string(smt2)
+# initialise SMT solver
+s = Solver()
+
+# prove equivalence of z3 and smt2 translation
+s.add(e_z3 != smt2_z3)
+assert (s.check() == unsat)
diff --git a/test/test_all.py b/test/test_all.py
index 71ea51a5..8b57bd23 100644
--- a/test/test_all.py
+++ b/test/test_all.py
@@ -202,7 +202,7 @@ testset += RegressionTest(["analysis.py"], base_dir="ir",
             ["simp_graph_%02d.dot" % test_nb, "graph_%02d.dot" % test_nb]
             for test_nb in xrange(1, 18))
                                     for fname in fnames])
-testset += RegressionTest(["z3_ir.py"], base_dir="ir/translators",
+testset += RegressionTest(["z3_ir.py", "smt2.py"], base_dir="ir/translators",
                           tags=[TAGS["z3"]])
 ## OS_DEP
 for script in ["win_api_x86_32.py",