TranslatorZ3: Better handling of asm_labels (translating to BitVecVal when possible)

2 files changed, 12 insertions, 2 deletions

diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index db038fe1..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(str(expr), 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):
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index fa656ed0..6e483d61 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -139,9 +139,15 @@ for miasm_int, res in [(five, -5), (four, -4)]:
     assert equiv(ez3, z3_e6)
 
 # --------------------------------------------------------------------------
-# Should just not throw anything
 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."