TranslatorZ3: Handling 'parity' and '-' unary operators, and raising errors properly for other unhandled operators.

2 files changed, 34 insertions, 11 deletions

diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index f3f9a6bf..04ed9332 100644
--- a/miasm2/ir/translators/z3_ir.py
+++ b/miasm2/ir/translators/z3_ir.py
@@ -154,17 +154,24 @@ 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':
+            res = z3.Extract(0, 0, res)
+        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..99d77c5a 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -119,5 +119,21 @@ 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
+for miasm_int, res in [(five, 1), (four, 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)
+
 print "TranslatorZ3 tests are OK."