diff options
Diffstat (limited to '')
| -rw-r--r-- | test/ir/translators/smt2.py | 35 |
1 files changed, 24 insertions, 11 deletions
diff --git a/test/ir/translators/smt2.py b/test/ir/translators/smt2.py index 2b5c8df3..81f63b45 100644 --- a/test/ir/translators/smt2.py +++ b/test/ir/translators/smt2.py @@ -1,7 +1,7 @@ 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 +from miasm.expression.expression import * +from miasm.ir.translators.smt2 import TranslatorSMT2 +from miasm.ir.translators.z3_ir import TranslatorZ3 # create nested expression a = ExprId("a", 64) @@ -10,14 +10,26 @@ 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(0x5L, 8)) -right = ExprCond(cond, - a + ExprInt(0x64L, 64), - ExprInt(0x16L, 64)) +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(0x5, 8)) +) +right = ExprCond( + cond, + a + ExprInt(0x64, 64), + ExprInt(0x16, 64) +) e = ExprAssign(left, right) @@ -32,6 +44,7 @@ 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() |