about summary refs log tree commit diff stats
path: root/miasm2/ir/translators/smt2.py
diff options
context:
space:
mode:
Diffstat (limited to 'miasm2/ir/translators/smt2.py')
-rw-r--r--miasm2/ir/translators/smt2.py21
1 files changed, 20 insertions, 1 deletions
diff --git a/miasm2/ir/translators/smt2.py b/miasm2/ir/translators/smt2.py
index 18bcb9bd..6a6fec16 100644
--- a/miasm2/ir/translators/smt2.py
+++ b/miasm2/ir/translators/smt2.py
@@ -120,7 +120,7 @@ class TranslatorSMT2(Translator):
     # Implemented language
     __LANG__ = "smt2"
 
-    def __init__(self, endianness="<", **kwargs):
+    def __init__(self, endianness="<", symbol_pool=None, **kwargs):
         """Instance a SMT2 translator
         @endianness: (optional) memory endianness
         """
@@ -129,6 +129,8 @@ class TranslatorSMT2(Translator):
         self._mem = SMT2Mem(endianness)
         # map of translated bit vectors
         self._bitvectors = dict()
+        # symbol pool
+        self.symbol_pool = symbol_pool
 
     def from_ExprInt(self, expr):
         return bit_vec_val(expr.arg.arg, expr.size)
@@ -148,6 +150,23 @@ class TranslatorSMT2(Translator):
                 self._bitvectors[str(expr)] = expr.size
             return str(expr)
 
+    def from_ExprLoc(self, expr):
+        loc_key = expr.loc_key
+        if self.symbol_pool is None:
+            if str(loc_key) not in self._bitvectors:
+                self._bitvectors[str(loc_key)] = expr.size
+            return str(loc_key)
+
+        offset = self.symbol_pool.loc_key_to_offset(loc_key)
+        name = self.symbol_pool.loc_key_to_name(loc_key)
+
+        if offset is None:
+            return bit_vec_val(str(offset), expr.size)
+        name = "|{}|".format(str(name))
+        if name not in self._bitvectors:
+            self._bitvectors[name] = expr.size
+        return name
+
     def from_ExprMem(self, expr):
         addr = self.from_expr(expr.arg)
         # size to read from memory