Merge pull request #41 from fmonjalet/translator_z3

TranslatorZ3

2 files changed, 135 insertions, 0 deletions

diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
new file mode 100644
index 00000000..997a3da9
--- /dev/null
+++ b/test/ir/translators/z3_ir.py
@@ -0,0 +1,123 @@
+import z3
+
+from miasm2.expression.expression import *
+from miasm2.ir.translators.translator import Translator
+from miasm2.ir.translators.z3_ir import TranslatorZ3, Z3Mem
+
+# Some examples of use/unit tests.
+
+def equiv(z3_expr1, z3_expr2):
+    s = z3.Solver()
+    s.add(z3.Not(z3_expr1 == z3_expr2))
+    return s.check() == z3.unsat
+
+def check_interp(interp, constraints, bits=32, valbits=8):
+    """Checks that a list of @constraints (addr, value) (as python ints)
+    match a z3 FuncInterp (@interp).
+    """
+    constraints = dict((addr,
+                        z3.BitVecVal(val, valbits))
+                       for addr, val in constraints)
+    l = interp.as_list()
+    for entry in l:
+        if not isinstance(entry, list) or len(entry) < 2:
+            continue
+        addr, value = entry[0], entry[1]
+        if addr.as_long() in constraints:
+            assert equiv(value, constraints[addr.as_long()])
+
+# equiv short test
+# --------------------------------------------------------------------------
+assert equiv(z3.BitVec('a', 32) + z3.BitVecVal(3, 32) - z3.BitVecVal(1, 32),
+             z3.BitVec('a', 32) + z3.BitVecVal(2, 32))
+
+# Z3Mem short tests
+# --------------------------------------------------------------------------
+mem = Z3Mem(endianness='<') # little endian  
+eax = z3.BitVec('EAX', 32)
+assert equiv(
+         # @32[EAX]
+         mem.get(eax, 32),
+         # @16[EAX+2] . @16[EAX]
+         z3.Concat(mem.get(eax+2, 16), 
+                   mem.get(eax, 16)))
+
+# --------------------------------------------------------------------------
+ax = z3.BitVec('AX', 16) 
+assert not equiv(
+        # @16[EAX] with EAX = ZeroExtend(AX)
+        mem.get(z3.ZeroExt(16, ax), 16),
+        # @16[AX]
+        mem.get(ax, 16))
+
+# TranslatorZ3 tests
+# --------------------------------------------------------------------------
+e = ExprId('x', 32)
+ez3 = Translator.to_language('z3').from_expr(e)
+
+z3_e = z3.BitVec('x', 32)
+assert equiv(ez3, z3_e)
+
+# --------------------------------------------------------------------------
+four = ExprInt32(4)
+five = ExprInt32(5)
+e2 = (e + five + four) * five
+ez3 = Translator.to_language('z3').from_expr(e2)
+
+z3_four = z3.BitVecVal(4, 32)
+z3_five = z3.BitVecVal(5, 32)
+z3_e2 = (z3_e + z3_five + z3_four) * z3_five
+assert equiv(ez3, z3_e2)
+
+# --------------------------------------------------------------------------
+emem = ExprMem(ExprInt32(0xdeadbeef), size=32)
+emem2 = ExprMem(ExprInt32(0xfee1dead), size=32)
+e3 = (emem + e) * ExprInt32(2) * emem2
+ez3 = Translator.to_language('z3').from_expr(e3)
+
+mem = Z3Mem()
+z3_emem = mem.get(z3.BitVecVal(0xdeadbeef, 32), 32)
+z3_emem2 = mem.get(z3.BitVecVal(0xfee1dead, 32), 32)
+z3_e3 = (z3_emem + z3_e) * z3.BitVecVal(2, 32) * z3_emem2
+assert equiv(ez3, z3_e3)
+
+# --------------------------------------------------------------------------
+e4 = emem * five
+ez3 = Translator.to_language('z3').from_expr(e4)
+
+z3_e4 = z3_emem * z3_five
+assert equiv(ez3, z3_e4)
+
+# Solve constraint and check endianness
+solver = z3.Solver()
+solver.add(ez3 == 10)
+solver.check()
+model = solver.model()
+check_interp(model[mem.get_mem_array(32)],
+             [(0xdeadbeef, 2), (0xdeadbeef + 3, 0)])
+
+# --------------------------------------------------------------------------
+ez3 = TranslatorZ3.from_expr(e4, endianness=">")
+
+memb = Z3Mem(endianness=">")
+z3_emem = memb.get(z3.BitVecVal(0xdeadbeef, 32), 32)
+z3_e4 = z3_emem * z3_five
+assert equiv(ez3, z3_e4)
+
+# Solve constraint and check endianness
+solver = z3.Solver()
+solver.add(ez3 == 10)
+solver.check()
+model = solver.model()
+check_interp(model[memb.get_mem_array(32)],
+             [(0xdeadbeef, 0), (0xdeadbeef + 3, 2)])
+
+# --------------------------------------------------------------------------
+e5 = ExprSlice(ExprCompose(((e, 0, 32), (four, 32, 64))), 0, 32) * five
+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)
+
+print "TranslatorZ3 tests are OK."
+
diff --git a/test/test_all.py b/test/test_all.py
index 27ae8559..5e43ce3f 100644
--- a/test/test_all.py
+++ b/test/test_all.py
@@ -11,6 +11,7 @@ TAGS = {"regression": "REGRESSION", # Regression tests
         "example": "EXAMPLE", # Examples
         "long": "LONG", # Very time consumming tests
         "llvm": "LLVM", # LLVM dependency is required
+        "z3": "Z3", # Z3 dependecy is needed
         }
 
 # Regression tests
@@ -59,6 +60,8 @@ for script in ["ir2C.py",
                "symbexec.py",
                ]:
     testset += RegressionTest([script], base_dir="ir")
+testset += RegressionTest(["z3_ir.py"], base_dir="ir/translators",
+                          tags=[TAGS["z3"]])
 ## OS_DEP
 for script in ["win_api_x86_32.py",
                ]:
@@ -280,6 +283,15 @@ By default, no tag is ommited." % ", ".join(TAGS.keys()), default="")
         if TAGS["llvm"] not in exclude_tags:
             exclude_tags.append(TAGS["llvm"])
 
+    # Handle Z3 dependency
+    try:
+        import z3
+    except ImportError:
+        print "%(red)s[Z3]%(end)s" % cosmetics.colors + \
+            "Z3 and its python binding are necessary for TranslatorZ3."
+        if TAGS["z3"] not in exclude_tags:
+            exclude_tags.append(TAGS["z3"])
+
     # Set callbacks
     if multiproc is False:
         testset.set_callback(task_done=monothread.task_done,