Merge pull request #128 from fmonjalet/z3_unary_op_fix

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

2 files changed, 56 insertions, 12 deletions

diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index f3f9a6bf..6f0b1aef 100644
--- a/miasm2/ir/translators/z3_ir.py
+++ b/miasm2/ir/translators/z3_ir.py
@@ -3,6 +3,7 @@ import operator
 
 import z3
 
+from miasm2.core.asmbloc import asm_label
 from miasm2.ir.translators.translator import Translator
 
 log = logging.getLogger("translator_z3")
@@ -117,7 +118,10 @@ class TranslatorZ3(Translator):
 
     @classmethod
     def from_ExprId(cls, expr):
-        return z3.BitVec(expr.name, expr.size)
+        if isinstance(expr.name, asm_label) and expr.name.offset is not None:
+            return z3.BitVecVal(expr.name.offset, expr.size)
+        else:
+            return z3.BitVec(str(expr), expr.size)
 
     @classmethod
     def from_ExprMem(cls, expr):
@@ -154,17 +158,27 @@ class TranslatorZ3(Translator):
     def from_ExprOp(cls, expr):
         args = map(cls.from_expr, expr.args)
         res = args[0]
-        for arg in args[1:]:
-            if expr.op in cls.trivial_ops:
-                res = eval("res %s arg" % expr.op)
-            elif expr.op == ">>":
-                res = z3.LShR(res, arg)
-            elif expr.op == "a>>":
-                res = res >> arg
-            elif expr.op == "a<<":
-                res = res << arg
-            else:
-                raise NotImplementedError("Unsupported OP yet: %s" % expr.op)
+        if len(args) > 1:
+            for arg in args[1:]:
+                if expr.op in cls.trivial_ops:
+                    res = eval("res %s arg" % expr.op)
+                elif expr.op == ">>":
+                    res = z3.LShR(res, arg)
+                elif expr.op == "a>>":
+                    res = res >> arg
+                elif expr.op == "a<<":
+                    res = res << arg
+                else:
+                    raise NotImplementedError("Unsupported OP yet: %s" % expr.op)
+        elif expr.op == 'parity':
+            arg = z3.Extract(7, 0, res)
+            res = z3.BitVecVal(1, 1)
+            for i in xrange(8):
+                res = res ^ z3.Extract(i, i, arg)
+        elif expr.op == '-':
+            res = -res
+        else:
+            raise NotImplementedError("Unsupported OP yet: %s" % expr.op)
         return res
 
     @classmethod
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."