diff options
Diffstat (limited to '')
| -rw-r--r-- | test/ir/translators/z3_ir.py | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index 997a3da9..6e483d61 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -1,5 +1,6 @@ import z3 +from miasm2.core.asmbloc import asm_label from miasm2.expression.expression import * from miasm2.ir.translators.translator import Translator from miasm2.ir.translators.z3_ir import TranslatorZ3, Z3Mem @@ -119,5 +120,34 @@ ez3 = Translator.to_language('z3').from_expr(e5) z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five assert equiv(ez3, z3_e5) +# -------------------------------------------------------------------------- +# Parity +seven = ExprInt32(7) +one0seven = ExprInt32(0x107) +for miasm_int, res in [(five, 1), (four, 0), (seven, 0), (one0seven, 0)]: + e6 = ExprOp('parity', miasm_int) + ez3 = Translator.to_language('z3').from_expr(e6) + z3_e6 = z3.BitVecVal(res, 1) + assert equiv(ez3, z3_e6) + +# -------------------------------------------------------------------------- +# '-' +for miasm_int, res in [(five, -5), (four, -4)]: + e6 = ExprOp('-', miasm_int) + ez3 = Translator.to_language('z3').from_expr(e6) + z3_e6 = z3.BitVecVal(res, 32) + assert equiv(ez3, z3_e6) + +# -------------------------------------------------------------------------- +e7 = ExprId(asm_label("label_histoire", 0xdeadbeef), 32) +ez3 = Translator.to_language('z3').from_expr(e7) +z3_e7 = z3.BitVecVal(0xdeadbeef, 32) +assert equiv(ez3, z3_e7) + +# Should just not throw anything to pass +e8 = ExprId(asm_label("label_jambe"), 32) +ez3 = Translator.to_language('z3').from_expr(e8) +assert not equiv(ez3, z3_e7) + print "TranslatorZ3 tests are OK." |