diff options
Diffstat (limited to '')
| -rw-r--r-- | test/ir/translators/smt2.py | 40 | ||||
| -rw-r--r-- | test/test_all.py | 2 |
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", |