diff options
Diffstat (limited to 'miasm2/ir/translators/z3_ir.py')
| -rw-r--r-- | miasm2/ir/translators/z3_ir.py | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index 536daff1..887c68d0 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -5,7 +5,6 @@ import operator # Raise an ImportError if z3 is not available WITHOUT actually importing it imp.find_module("z3") -from miasm2.core.asmblock import AsmLabel from miasm2.ir.translators.translator import Translator log = logging.getLogger("translator_z3") @@ -116,7 +115,7 @@ class TranslatorZ3(Translator): # Operations translation trivial_ops = ["+", "-", "/", "%", "&", "^", "|", "*", "<<"] - def __init__(self, endianness="<", **kwargs): + def __init__(self, endianness="<", loc_db=None, **kwargs): """Instance a Z3 translator @endianness: (optional) memory endianness """ @@ -126,15 +125,24 @@ class TranslatorZ3(Translator): super(TranslatorZ3, self).__init__(**kwargs) self._mem = Z3Mem(endianness) + self.loc_db = loc_db def from_ExprInt(self, expr): return z3.BitVecVal(expr.arg.arg, expr.size) def from_ExprId(self, expr): - if isinstance(expr.name, AsmLabel) and expr.name.offset is not None: - return z3.BitVecVal(expr.name.offset, expr.size) - else: + return z3.BitVec(str(expr), expr.size) + + def from_ExprLoc(self, expr): + if self.loc_db is None: + # No loc_db, fallback to default name return z3.BitVec(str(expr), expr.size) + loc_key = expr.loc_key + offset = self.loc_db.get_location_offset(loc_key) + if offset is not None: + return z3.BitVecVal(offset, expr.size) + # fallback to default name + return z3.BitVec(str(loc_key), expr.size) def from_ExprMem(self, expr): addr = self.from_expr(expr.arg) |