Merge pull request #128 from fmonjalet/z3_unary_op_fix

TranslatorZ3: Handling 'parity' and '-' unary operators, and raising err...

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."