Merge pull request #128 from fmonjalet/z3_unary_op_fix

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

1 files changed, 26 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