Merge pull request #751 from serpilliere/ExprLabel

Expr Loc

1 files changed, 29 insertions, 22 deletions

diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index 6ae2dcd0..29b3c39d 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -1,12 +1,16 @@
 import z3
 
-from miasm2.core.asmblock import AsmLabel
+from miasm2.core.asmblock import AsmSymbolPool
 from miasm2.expression.expression import *
-from miasm2.ir.translators.translator import Translator
-from miasm2.ir.translators.z3_ir import Z3Mem
+from miasm2.ir.translators.z3_ir import Z3Mem, TranslatorZ3
 
 # Some examples of use/unit tests.
 
+symbol_pool = AsmSymbolPool()
+translator1 = TranslatorZ3(endianness="<", symbol_pool=symbol_pool)
+translator2 = TranslatorZ3(endianness=">", symbol_pool=symbol_pool)
+
+
 def equiv(z3_expr1, z3_expr2):
     s = z3.Solver()
     s.add(z3.Not(z3_expr1 == z3_expr2))
@@ -34,17 +38,17 @@ assert equiv(z3.BitVec('a', 32) + z3.BitVecVal(3, 32) - z3.BitVecVal(1, 32),
 
 # Z3Mem short tests
 # --------------------------------------------------------------------------
-mem = Z3Mem(endianness='<') # little endian  
+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), 
+         z3.Concat(mem.get(eax+2, 16),
                    mem.get(eax, 16)))
 
 # --------------------------------------------------------------------------
-ax = z3.BitVec('AX', 16) 
+ax = z3.BitVec('AX', 16)
 assert not equiv(
         # @16[EAX] with EAX = ZeroExtend(AX)
         mem.get(z3.ZeroExt(16, ax), 16),
@@ -54,7 +58,7 @@ assert not equiv(
 # TranslatorZ3 tests
 # --------------------------------------------------------------------------
 e = ExprId('x', 32)
-ez3 = Translator.to_language('z3').from_expr(e)
+ez3 = translator1.from_expr(e)
 
 z3_e = z3.BitVec('x', 32)
 assert equiv(ez3, z3_e)
@@ -63,7 +67,7 @@ assert equiv(ez3, z3_e)
 four = ExprInt(4, 32)
 five = ExprInt(5, 32)
 e2 = (e + five + four) * five
-ez3 = Translator.to_language('z3').from_expr(e2)
+ez3 = translator1.from_expr(e2)
 
 z3_four = z3.BitVecVal(4, 32)
 z3_five = z3.BitVecVal(5, 32)
@@ -74,7 +78,7 @@ assert equiv(ez3, z3_e2)
 emem = ExprMem(ExprInt(0xdeadbeef, 32), size=32)
 emem2 = ExprMem(ExprInt(0xfee1dead, 32), size=32)
 e3 = (emem + e) * ExprInt(2, 32) * emem2
-ez3 = Translator.to_language('z3').from_expr(e3)
+ez3 = translator1.from_expr(e3)
 
 mem = Z3Mem()
 z3_emem = mem.get(z3.BitVecVal(0xdeadbeef, 32), 32)
@@ -84,7 +88,7 @@ assert equiv(ez3, z3_e3)
 
 # --------------------------------------------------------------------------
 e4 = emem * five
-ez3 = Translator.to_language('z3').from_expr(e4)
+ez3 = translator1.from_expr(e4)
 
 z3_e4 = z3_emem * z3_five
 assert equiv(ez3, z3_e4)
@@ -98,7 +102,7 @@ check_interp(model[mem.get_mem_array(32)],
              [(0xdeadbeef, 2), (0xdeadbeef + 3, 0)])
 
 # --------------------------------------------------------------------------
-ez3 = Translator.to_language("z3", endianness=">").from_expr(e4)
+ez3 = translator2.from_expr(e4)
 
 memb = Z3Mem(endianness=">")
 z3_emem = memb.get(z3.BitVecVal(0xdeadbeef, 32), 32)
@@ -115,7 +119,7 @@ check_interp(model[memb.get_mem_array(32)],
 
 # --------------------------------------------------------------------------
 e5 = ExprSlice(ExprCompose(e, four), 0, 32) * five
-ez3 = Translator.to_language('z3').from_expr(e5)
+ez3 = translator1.from_expr(e5)
 
 z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five
 assert equiv(ez3, z3_e5)
@@ -126,7 +130,7 @@ seven = ExprInt(7, 32)
 one0seven = ExprInt(0x107, 32)
 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)
+    ez3 = translator1.from_expr(e6)
     z3_e6 = z3.BitVecVal(res, 1)
     assert equiv(ez3, z3_e6)
 
@@ -134,37 +138,40 @@ for miasm_int, res in [(five, 1), (four, 0), (seven, 0), (one0seven, 0)]:
 # '-'
 for miasm_int, res in [(five, -5), (four, -4)]:
     e6 = ExprOp('-', miasm_int)
-    ez3 = Translator.to_language('z3').from_expr(e6)
+    ez3 = translator1.from_expr(e6)
     z3_e6 = z3.BitVecVal(res, 32)
     assert equiv(ez3, z3_e6)
 
 # --------------------------------------------------------------------------
-e7 = ExprId(AsmLabel("label_histoire", 0xdeadbeef), 32)
-ez3 = Translator.to_language('z3').from_expr(e7)
+label_histoire = symbol_pool.add_location("label_histoire", 0xdeadbeef)
+e7 = ExprLoc(label_histoire, 32)
+ez3 = translator1.from_expr(e7)
 z3_e7 = z3.BitVecVal(0xdeadbeef, 32)
 assert equiv(ez3, z3_e7)
 
 # Should just not throw anything to pass
-e8 = ExprId(AsmLabel("label_jambe"), 32)
-ez3 = Translator.to_language('z3').from_expr(e8)
+lbl_e8 = symbol_pool.add_location("label_jambe")
+
+e8 = ExprLoc(lbl_e8, 32)
+ez3 = translator1.from_expr(e8)
 assert not equiv(ez3, z3_e7)
 
 # --------------------------------------------------------------------------
 # cntleadzeros, cnttrailzeros
 
 # cnttrailzeros(0x1138) == 3
-cnttrailzeros1 = Translator.to_language('z3').from_expr(ExprOp("cnttrailzeros", ExprInt(0x1138, 32)))
+cnttrailzeros1 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x1138, 32)))
 cnttrailzeros2 = z3.BitVecVal(3, 32)
 assert(equiv(cnttrailzeros1, cnttrailzeros2))
 
 # cntleadzeros(0x11300) == 0xf
-cntleadzeros1 = Translator.to_language('z3').from_expr(ExprOp("cntleadzeros", ExprInt(0x11300, 32)))
+cntleadzeros1 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x11300, 32)))
 cntleadzeros2 = z3.BitVecVal(0xf, 32)
 assert(equiv(cntleadzeros1, cntleadzeros2))
 
 # cnttrailzeros(0x8000) + 1 == cntleadzeros(0x8000)
-cnttrailzeros3 = Translator.to_language('z3').from_expr(ExprOp("cnttrailzeros", ExprInt(0x8000, 32)) + ExprInt(1, 32))
-cntleadzeros3 = Translator.to_language('z3').from_expr(ExprOp("cntleadzeros", ExprInt(0x8000, 32)))
+cnttrailzeros3 = translator1.from_expr(ExprOp("cnttrailzeros", ExprInt(0x8000, 32)) + ExprInt(1, 32))
+cntleadzeros3 = translator1.from_expr(ExprOp("cntleadzeros", ExprInt(0x8000, 32)))
 assert(equiv(cnttrailzeros3, cntleadzeros3))
 
 print "TranslatorZ3 tests are OK."