about summary refs log tree commit diff stats
path: root/miasm2/ir
diff options
context:
space:
mode:
Diffstat (limited to 'miasm2/ir')
-rw-r--r--miasm2/ir/ir.py262
-rw-r--r--miasm2/ir/symbexec.py38
-rw-r--r--miasm2/ir/symbexec_top.py12
-rw-r--r--miasm2/ir/translators/C.py113
-rw-r--r--miasm2/ir/translators/python.py3
-rw-r--r--miasm2/ir/translators/smt2.py38
-rw-r--r--miasm2/ir/translators/translator.py7
-rw-r--r--miasm2/ir/translators/z3_ir.py22
8 files changed, 319 insertions, 176 deletions
diff --git a/miasm2/ir/ir.py b/miasm2/ir/ir.py
index 1c6895e0..0a7d1d84 100644
--- a/miasm2/ir/ir.py
+++ b/miasm2/ir/ir.py
@@ -23,11 +23,10 @@ from itertools import chain
 
 import miasm2.expression.expression as m2_expr
 from miasm2.expression.expression_helper import get_missing_interval
-from miasm2.core.asmblock import AsmSymbolPool, expr_is_label, AsmLabel, \
-    AsmBlock
+from miasm2.core.asmblock import AsmSymbolPool, AsmBlock, \
+    AsmConstraint, AsmBlockBad
 from miasm2.core.graph import DiGraph
 
-
 class AssignBlock(object):
     """Represent parallel IR assignment, such as:
     EAX = EBX
@@ -264,16 +263,16 @@ class IRBlock(object):
     Stand for an intermediate representation  basic block.
     """
 
-    __slots__ = ["label", "_assignblks", "_dst", "_dst_linenb"]
+    __slots__ = ["_loc_key", "_assignblks", "_dst", "_dst_linenb"]
 
-    def __init__(self, label, assignblks):
+    def __init__(self, loc_key, assignblks):
         """
-        @label: AsmLabel of the IR basic block
+        @loc_key: LocKey of the IR basic block
         @assignblks: list of AssignBlock
         """
 
-        assert isinstance(label, AsmLabel)
-        self.label = label
+        assert isinstance(loc_key, m2_expr.LocKey)
+        self._loc_key = loc_key
         for assignblk in assignblks:
             assert isinstance(assignblk, AssignBlock)
         self._assignblks = tuple(assignblks)
@@ -281,6 +280,13 @@ class IRBlock(object):
         self._dst_linenb = None
 
 
+    def get_label(self):
+        warnings.warn('DEPRECATION WARNING: use ".loc_key" instead of ".label"')
+        return self.loc_key
+
+    loc_key = property(lambda self:self._loc_key)
+    label = property(get_label)
+
     @property
     def assignblks(self):
         return self._assignblks
@@ -340,7 +346,7 @@ class IRBlock(object):
                 else:
                     new_assignblk[dst] = src
             irs.append(AssignBlock(new_assignblk, assignblk.instr))
-        return IRBlock(self.label, irs)
+        return IRBlock(self.loc_key, irs)
 
     @property
     def dst_linenb(self):
@@ -351,7 +357,7 @@ class IRBlock(object):
 
     def __str__(self):
         out = []
-        out.append('%s' % self.label)
+        out.append('loc_key_%s' % self.loc_key.key)
         for assignblk in self:
             for dst, src in assignblk.iteritems():
                 out.append('\t%s = %s' % (dst, src))
@@ -378,7 +384,7 @@ class IRBlock(object):
             for dst, src in assignblk.iteritems():
                 new_assignblk[mod_dst(dst)] = mod_src(src)
             assignblks.append(AssignBlock(new_assignblk, assignblk.instr))
-        return IRBlock(self.label, assignblks)
+        return IRBlock(self.loc_key, assignblks)
 
 
 class irbloc(IRBlock):
@@ -387,33 +393,53 @@ class irbloc(IRBlock):
     Use IRBlock instead of irbloc
     """
 
-    def __init__(self, label, irs, lines=None):
+    def __init__(self, loc_key, irs, lines=None):
         warnings.warn('DEPRECATION WARNING: use "IRBlock" instead of "irblock"')
-        super(irbloc, self).__init__(label, irs)
+        super(irbloc, self).__init__(loc_key, irs)
 
 
 class DiGraphIR(DiGraph):
 
     """DiGraph for IR instances"""
 
-    def __init__(self, blocks, *args, **kwargs):
+    def __init__(self, blocks, symbol_pool=None, *args, **kwargs):
         """Instanciate a DiGraphIR
         @blocks: IR blocks
         """
+        self.symbol_pool = symbol_pool
         self._blocks = blocks
         super(DiGraphIR, self).__init__(*args, **kwargs)
 
+    def _expr_loc_to_symb(self, expr):
+        if not expr.is_loc():
+            return expr
+        if self.symbol_pool is None:
+            name = str(expr)
+        else:
+            name = self.symbol_pool.loc_key_to_name(expr.loc_key)
+        return m2_expr.ExprId(name, expr.size)
+
     def node2lines(self, node):
-        yield self.DotCellDescription(text=str(node.name),
-                                      attr={'align': 'center',
-                                            'colspan': 2,
-                                            'bgcolor': 'grey'})
+        if self.symbol_pool is None:
+            node_name = str(node)
+        else:
+            node_name = self.symbol_pool.loc_key_to_name(node)
+        yield self.DotCellDescription(
+            text="%s" % node_name,
+            attr={
+                'align': 'center',
+                'colspan': 2,
+                'bgcolor': 'grey',
+            }
+        )
         if node not in self._blocks:
             yield [self.DotCellDescription(text="NOT PRESENT", attr={})]
             raise StopIteration
         for i, assignblk in enumerate(self._blocks[node]):
             for dst, src in assignblk.iteritems():
-                line = "%s = %s" % (dst, src)
+                new_src = src.visit(self._expr_loc_to_symb)
+                new_dst = dst.visit(self._expr_loc_to_symb)
+                line = "%s = %s" % (new_dst, new_src)
                 if self._dot_offset:
                     yield [self.DotCellDescription(text="%-4d" % i, attr={}),
                            self.DotCellDescription(text=line, attr={})]
@@ -427,11 +453,10 @@ class DiGraphIR(DiGraph):
         src_irdst = self._blocks[src].dst
         edge_color = "blue"
         if isinstance(src_irdst, m2_expr.ExprCond):
-            if (expr_is_label(src_irdst.src1) and
-                    src_irdst.src1.name == dst):
+            src1, src2 = src_irdst.src1, src_irdst.src2
+            if src1.is_loc(dst):
                 edge_color = "limegreen"
-            elif (expr_is_label(src_irdst.src2) and
-                  src_irdst.src2.name == dst):
+            elif src2.is_loc(dst):
                 edge_color = "red"
         return {"color": edge_color}
 
@@ -482,19 +507,18 @@ class IntermediateRepresentation(object):
             irs = []
             for assignblk in irb:
                 irs.append(AssignBlock(assignblk, instr))
-            extra_irblocks[index] = IRBlock(irb.label, irs)
+            extra_irblocks[index] = IRBlock(irb.loc_key, irs)
         assignblk = AssignBlock(ir_bloc_cur, instr)
         return assignblk, extra_irblocks
 
-    def get_label(self, addr):
-        """Transforms an ExprId/ExprInt/label/int into a label
-        @addr: an ExprId/ExprInt/label/int"""
+    def get_loc_key(self, addr):
+        """Transforms an ExprId/ExprInt/loc_key/int into a loc_key
+        @addr: an ExprId/ExprInt/loc_key/int"""
 
-        if (isinstance(addr, m2_expr.ExprId) and
-                isinstance(addr.name, AsmLabel)):
-            addr = addr.name
-        if isinstance(addr, AsmLabel):
+        if isinstance(addr, m2_expr.LocKey):
             return addr
+        elif isinstance(addr, m2_expr.ExprLoc):
+            return addr.loc_key
 
         try:
             addr = int(addr)
@@ -504,11 +528,13 @@ class IntermediateRepresentation(object):
         return self.symbol_pool.getby_offset_create(addr)
 
     def get_block(self, addr):
-        """Returns the irbloc associated to an ExprId/ExprInt/label/int
-        @addr: an ExprId/ExprInt/label/int"""
+        """Returns the irbloc associated to an ExprId/ExprInt/loc_key/int
+        @addr: an ExprId/ExprInt/loc_key/int"""
 
-        label = self.get_label(addr)
-        return self.blocks.get(label, None)
+        loc_key = self.get_loc_key(addr)
+        if loc_key is None:
+            return None
+        return self.blocks.get(loc_key, None)
 
     def get_bloc(self, addr):
         """
@@ -518,16 +544,21 @@ class IntermediateRepresentation(object):
         warnings.warn('DEPRECATION WARNING: use "get_block" instead of "get_bloc"')
         return self.get_block(addr)
 
-    def add_instr(self, line, addr=0, gen_pc_updt=False):
-        block = AsmBlock(self.gen_label())
+    def add_instr(self, line, loc_key=None, gen_pc_updt=False):
+        if loc_key is None:
+            loc_key = self.symbol_pool.gen_loc_key()
+        block = AsmBlock(loc_key)
         block.lines = [line]
         self.add_block(block, gen_pc_updt)
+        return loc_key
 
     def getby_offset(self, offset):
         out = set()
         for irb in self.blocks.values():
             for assignblk in irb:
                 instr = assignblk.instr
+                if instr is None:
+                    continue
                 if instr.offset <= offset < instr.offset + instr.l:
                     out.add(irb)
         return out
@@ -593,24 +624,26 @@ class IntermediateRepresentation(object):
         @gen_pc_updt: insert PC update effects between instructions
         """
 
-        label = None
+        loc_key = block.loc_key
         ir_blocks_all = []
+
+        assignments = []
         for instr in block.lines:
-            if label is None:
+            if loc_key is None:
                 assignments = []
-                label = self.get_instr_label(instr)
+                loc_key = self.get_loc_key_for_instr(instr)
             split = self.add_instr_to_irblock(block, instr, assignments,
                                               ir_blocks_all, gen_pc_updt)
             if split:
-                ir_blocks_all.append(IRBlock(label, assignments))
-                label = None
+                ir_blocks_all.append(IRBlock(loc_key, assignments))
+                loc_key = None
                 assignments = []
-        if label is not None:
-            ir_blocks_all.append(IRBlock(label, assignments))
+        if loc_key is not None:
+            ir_blocks_all.append(IRBlock(loc_key, assignments))
 
         new_ir_blocks_all = self.post_add_block(block, ir_blocks_all)
         for irblock in new_ir_blocks_all:
-            self.blocks[irblock.label] = irblock
+            self.blocks[irblock.loc_key] = irblock
         return new_ir_blocks_all
 
     def add_bloc(self, block, gen_pc_updt=False):
@@ -643,15 +676,25 @@ class IntermediateRepresentation(object):
         for index, irblock in enumerate(ir_blocks):
             if irblock.dst is not None:
                 continue
-            next_lbl = block.get_next()
-            if next_lbl is None:
-                dst = m2_expr.ExprId(self.get_next_label(block.lines[-1]),
-                                     self.pc.size)
+            next_loc_key = block.get_next()
+            if next_loc_key is None:
+                loc_key = None
+                if block.lines:
+                    line = block.lines[-1]
+                    if line.offset is not None:
+                        loc_key = self.symbol_pool.getby_offset_create(line.offset + line.l)
+                if loc_key is None:
+                    loc_key = self.symbol_pool.gen_loc_key()
+                block.add_cst(loc_key, AsmConstraint.c_next, self.symbol_pool)
+            else:
+                loc_key = next_loc_key
+            dst = m2_expr.ExprLoc(loc_key, self.pc.size)
+            if irblock.assignblks:
+                instr = irblock.assignblks[-1].instr
             else:
-                dst = m2_expr.ExprId(next_lbl,
-                                     self.pc.size)
-            assignblk = AssignBlock({self.IRDst: dst}, irblock[-1].instr)
-            ir_blocks[index] = IRBlock(irblock.label, list(irblock.assignblks) + [assignblk])
+                instr = None
+            assignblk = AssignBlock({self.IRDst: dst}, instr)
+            ir_blocks[index] = IRBlock(irblock.loc_key, list(irblock.assignblks) + [assignblk])
 
     def post_add_block(self, block, ir_blocks):
         self.set_empty_dst_to_next(block, ir_blocks)
@@ -659,7 +702,7 @@ class IntermediateRepresentation(object):
         new_irblocks = []
         for irblock in ir_blocks:
             new_irblock = self.irbloc_fix_regs_for_mode(irblock, self.attrib)
-            self.blocks[irblock.label] = new_irblock
+            self.blocks[irblock.loc_key] = new_irblock
             new_irblocks.append(new_irblock)
         # Forget graph if any
         self._graph = None
@@ -673,20 +716,22 @@ class IntermediateRepresentation(object):
         warnings.warn('DEPRECATION WARNING: use "post_add_block" instead of "post_add_bloc"')
         return self.post_add_block(block, ir_blocks)
 
-    def get_instr_label(self, instr):
-        """Returns the label associated to an instruction
+    def get_loc_key_for_instr(self, instr):
+        """Returns the loc_key associated to an instruction
         @instr: current instruction"""
-
         return self.symbol_pool.getby_offset_create(instr.offset)
 
-    def gen_label(self):
-        # TODO: fix hardcoded offset
-        label = self.symbol_pool.gen_label()
-        return label
+    def gen_loc_key_and_expr(self, size):
+        """
+        Return a loc_key and it's corresponding ExprLoc
+        @size: size of expression
+        """
+        loc_key = self.symbol_pool.gen_loc_key()
+        return loc_key, m2_expr.ExprLoc(loc_key, size)
 
-    def get_next_label(self, instr):
-        label = self.symbol_pool.getby_offset_create(instr.offset + instr.l)
-        return label
+    def get_next_loc_key(self, instr):
+        loc_key = self.symbol_pool.getby_offset_create(instr.offset + instr.l)
+        return loc_key
 
     def simplify(self, simplifier):
         """
@@ -694,14 +739,14 @@ class IntermediateRepresentation(object):
         @simplifier: ExpressionSimplifier instance
         """
         modified = False
-        for label, block in self.blocks.iteritems():
+        for loc_key, block in self.blocks.iteritems():
             assignblks = []
             for assignblk in block:
                 new_assignblk = assignblk.simplify(simplifier)
                 if assignblk != new_assignblk:
                     modified = True
                 assignblks.append(new_assignblk)
-            self.blocks[label] = IRBlock(label, assignblks)
+            self.blocks[loc_key] = IRBlock(loc_key, assignblks)
         return modified
 
     def replace_expr_in_ir(self, bloc, rep):
@@ -728,14 +773,14 @@ class IntermediateRepresentation(object):
         out = set()
         while todo:
             dst = todo.pop()
-            if expr_is_label(dst):
+            if dst.is_loc():
                 done.add(dst)
-            elif isinstance(dst, (m2_expr.ExprMem, m2_expr.ExprInt)):
+            elif dst.is_mem() or dst.is_int():
                 done.add(dst)
-            elif isinstance(dst, m2_expr.ExprCond):
+            elif dst.is_cond():
                 todo.add(dst.src1)
                 todo.add(dst.src2)
-            elif isinstance(dst, m2_expr.ExprId):
+            elif dst.is_id():
                 out.add(dst)
             else:
                 done.add(dst)
@@ -769,15 +814,16 @@ class IntermediateRepresentation(object):
         """
         Gen irbloc digraph
         """
-        self._graph = DiGraphIR(self.blocks)
+        self._graph = DiGraphIR(self.blocks, self.symbol_pool)
         for lbl, block in self.blocks.iteritems():
+            assert isinstance(lbl, m2_expr.LocKey)
             self._graph.add_node(lbl)
             for dst in self.dst_trackback(block):
                 if dst.is_int():
                     dst_lbl = self.symbol_pool.getby_offset_create(int(dst))
-                    dst = m2_expr.ExprId(dst_lbl, self.pc.size)
-                if expr_is_label(dst):
-                    self._graph.add_edge(lbl, dst.name)
+                    dst = m2_expr.ExprLoc(dst_lbl.loc_key, self.pc.size)
+                if dst.is_loc():
+                    self._graph.add_edge(lbl, dst.loc_key)
 
     @property
     def graph(self):
@@ -789,14 +835,14 @@ class IntermediateRepresentation(object):
 
     def remove_empty_assignblks(self):
         modified = False
-        for label, block in self.blocks.iteritems():
+        for loc_key, block in self.blocks.iteritems():
             irs = []
             for assignblk in block:
                 if len(assignblk):
                     irs.append(assignblk)
                 else:
                     modified = True
-            self.blocks[label] = IRBlock(label, irs)
+            self.blocks[loc_key] = IRBlock(loc_key, irs)
         return modified
 
     def remove_jmp_blocks(self):
@@ -814,62 +860,62 @@ class IntermediateRepresentation(object):
             if len(assignblk) > 1:
                 continue
             assert set(assignblk.keys()) == set([self.IRDst])
-            if len(self.graph.successors(block.label)) != 1:
+            if len(self.graph.successors(block.loc_key)) != 1:
                 continue
-            if not expr_is_label(assignblk[self.IRDst]):
+            if not assignblk[self.IRDst].is_loc():
                 continue
-            dst = assignblk[self.IRDst].name
-            if dst == block.label:
+            dst = assignblk[self.IRDst].loc_key
+            if dst == block.loc_key:
                 # Infinite loop block
                 continue
-            jmp_blocks.add(block.label)
+            jmp_blocks.add(block.loc_key)
 
         # Remove them, relink graph
         modified = False
-        for label in jmp_blocks:
-            block = self.blocks[label]
-            dst_label = block.dst.name
-            parents = self.graph.predecessors(block.label)
+        for loc_key in jmp_blocks:
+            block = self.blocks[loc_key]
+            dst_loc_key = block.dst
+            parents = self.graph.predecessors(block.loc_key)
             for lbl in parents:
                 parent = self.blocks.get(lbl, None)
                 if parent is None:
                     continue
                 dst = parent.dst
-                if dst.is_id(block.label):
-                    dst = m2_expr.ExprId(dst_label, dst.size)
+                if dst.is_id(block.loc_key):
+                    dst = m2_expr.ExprLoc(dst_loc_key, dst.size)
 
-                    self.graph.discard_edge(lbl, block.label)
-                    self.graph.discard_edge(block.label, dst_label)
+                    self.graph.discard_edge(lbl, block.loc_key)
+                    self.graph.discard_edge(block.loc_key, dst_loc_key)
 
-                    self.graph.add_uniq_edge(lbl, dst_label)
+                    self.graph.add_uniq_edge(lbl, dst_loc_key)
                     modified = True
                 elif dst.is_cond():
                     src1, src2 = dst.src1, dst.src2
-                    if src1.is_id(block.label):
-                        dst = m2_expr.ExprCond(dst.cond, m2_expr.ExprId(dst_label, dst.size), dst.src2)
-                        self.graph.discard_edge(lbl, block.label)
-                        self.graph.discard_edge(block.label, dst_label)
-                        self.graph.add_uniq_edge(lbl, dst_label)
+                    if src1.is_id(block.loc_key):
+                        dst = m2_expr.ExprCond(dst.cond, m2_expr.ExprLoc(dst_loc_key, dst.size), dst.src2)
+                        self.graph.discard_edge(lbl, block.loc_key)
+                        self.graph.discard_edge(block.loc_key, dst_loc_key)
+                        self.graph.add_uniq_edge(lbl, dst_loc_key)
                         modified = True
-                    if src2.is_id(block.label):
-                        dst = m2_expr.ExprCond(dst.cond, dst.src1, m2_expr.ExprId(dst_label, dst.size))
-                        self.graph.discard_edge(lbl, block.label)
-                        self.graph.discard_edge(block.label, dst_label)
-                        self.graph.add_uniq_edge(lbl, dst_label)
+                    if src2.is_id(block.loc_key):
+                        dst = m2_expr.ExprCond(dst.cond, dst.src1, m2_expr.ExprLoc(dst_loc_key, dst.size))
+                        self.graph.discard_edge(lbl, block.loc_key)
+                        self.graph.discard_edge(block.loc_key, dst_loc_key)
+                        self.graph.add_uniq_edge(lbl, dst_loc_key)
                         modified = True
                     if dst.src1 == dst.src2:
                         dst = dst.src1
                 else:
                     continue
                 new_parent = parent.set_dst(dst)
-                self.blocks[parent.label] = new_parent
+                self.blocks[parent.loc_key] = new_parent
 
         # Remove unlinked useless nodes
-        for label in jmp_blocks:
-            if (len(self.graph.predecessors(label)) == 0 and
-                len(self.graph.successors(label)) == 0):
-                self.graph.del_node(label)
-                del self.blocks[label]
+        for loc_key in jmp_blocks:
+            if (len(self.graph.predecessors(loc_key)) == 0 and
+                len(self.graph.successors(loc_key)) == 0):
+                self.graph.del_node(loc_key)
+                del self.blocks[loc_key]
         return modified
 
     def merge_blocks(self):
@@ -926,6 +972,6 @@ class ir(IntermediateRepresentation):
     Use IntermediateRepresentation instead of ir
     """
 
-    def __init__(self, label, irs, lines=None):
+    def __init__(self, loc_key, irs, lines=None):
         warnings.warn('DEPRECATION WARNING: use "IntermediateRepresentation" instead of "ir"')
-        super(ir, self).__init__(label, irs, lines)
+        super(ir, self).__init__(loc_key, irs, lines)
diff --git a/miasm2/ir/symbexec.py b/miasm2/ir/symbexec.py
index 4070f261..7ee55f97 100644
--- a/miasm2/ir/symbexec.py
+++ b/miasm2/ir/symbexec.py
@@ -2,8 +2,8 @@ import warnings
 import logging
 from collections import MutableMapping
 
-from miasm2.expression.expression import ExprOp, ExprId, ExprInt, ExprMem, \
-    ExprCompose, ExprSlice, ExprCond, ExprAff
+from miasm2.expression.expression import ExprOp, ExprId, ExprLoc, ExprInt, \
+    ExprMem, ExprCompose, ExprSlice, ExprCond, ExprAff
 from miasm2.expression.simplifications import expr_simp
 from miasm2.core import asmblock
 from miasm2.ir.ir import AssignBlock
@@ -17,9 +17,10 @@ log.setLevel(logging.INFO)
 
 def get_block(ir_arch, mdis, addr):
     """Get IRBlock at address @addr"""
-    lbl = ir_arch.get_label(addr)
+    lbl = ir_arch.get_loc_key(addr)
     if not lbl in ir_arch.blocks:
-        block = mdis.dis_block(lbl.offset)
+        offset = mdis.symbol_pool.loc_key_to_offset(lbl)
+        block = mdis.dis_block(offset)
         ir_arch.add_block(block)
     irblock = ir_arch.get_block(lbl)
     if irblock is None:
@@ -812,6 +813,7 @@ class SymbolicExecutionEngine(object):
         self.expr_to_visitor = {
             ExprInt: self.eval_exprint,
             ExprId: self.eval_exprid,
+            ExprLoc: self.eval_exprloc,
             ExprMem: self.eval_exprmem,
             ExprSlice: self.eval_exprslice,
             ExprCond: self.eval_exprcond,
@@ -885,10 +887,16 @@ class SymbolicExecutionEngine(object):
 
     def eval_exprid(self, expr, **kwargs):
         """[DEV]: Evaluate an ExprId using the current state"""
-        if isinstance(expr.name, asmblock.AsmLabel) and expr.name.offset is not None:
-            ret = ExprInt(expr.name.offset, expr.size)
+        ret = self.symbols.read(expr)
+        return ret
+
+    def eval_exprloc(self, expr, **kwargs):
+        """[DEV]: Evaluate an ExprLoc using the current state"""
+        offset = self.ir_arch.symbol_pool.loc_key_to_offset(expr.loc_key)
+        if offset is not None:
+            ret = ExprInt(offset, expr.size)
         else:
-            ret = self.symbols.read(expr)
+            ret = expr
         return ret
 
     def eval_exprmem(self, expr, **kwargs):
@@ -1040,7 +1048,17 @@ class SymbolicExecutionEngine(object):
                 self.dump(mems=False)
                 self.dump(ids=False)
                 print '_' * 80
-        return self.eval_expr(self.ir_arch.IRDst)
+        dst = self.eval_expr(self.ir_arch.IRDst)
+
+        # Best effort to resolve destination as ExprLoc
+        if dst.is_loc():
+            ret = dst
+        elif dst.is_int():
+            label = self.ir_arch.symbol_pool.getby_offset_create(int(dst))
+            ret = ExprLoc(label, dst.size)
+        else:
+            ret = dst
+        return ret
 
     def run_block_at(self, addr, step=False):
         """
@@ -1057,14 +1075,14 @@ class SymbolicExecutionEngine(object):
         """
         Symbolic execution starting at @addr
         @addr: address to execute (int or ExprInt or label)
-        @lbl_stop: AsmLabel to stop execution on
+        @lbl_stop: LocKey to stop execution on
         @step: display intermediate steps
         """
         while True:
             irblock = self.ir_arch.get_block(addr)
             if irblock is None:
                 break
-            if irblock.label == lbl_stop:
+            if irblock.loc_key == lbl_stop:
                 break
             addr = self.eval_updt_irblock(irblock, step=step)
         return addr
diff --git a/miasm2/ir/symbexec_top.py b/miasm2/ir/symbexec_top.py
index 1e1e76e9..64d428b4 100644
--- a/miasm2/ir/symbexec_top.py
+++ b/miasm2/ir/symbexec_top.py
@@ -121,14 +121,20 @@ class SymbExecTopNoMem(SymbolicExecutionEngine):
 
     def eval_exprid(self, expr, **kwargs):
         """[DEV]: Evaluate an ExprId using the current state"""
-        if isinstance(expr.name, asmblock.AsmLabel) and expr.name.offset is not None:
-            ret = ExprInt(expr.name.offset, expr.size)
-        elif expr in self.regstop:
+        if expr in self.regstop:
             ret = exprid_top(expr)
         else:
             ret = self.symbols.read(expr)
         return ret
 
+    def eval_exprloc(self, expr, **kwargs):
+        offset = self.ir_arch.symbol_pool.loc_key_to_offset(expr.loc_key)
+        if offset is not None:
+            ret = ExprInt(offset, expr.size)
+        else:
+            ret = expr
+        return ret
+
     def eval_exprcond(self, expr, **kwargs):
         """[DEV]: Evaluate an ExprCond using the current state"""
         cond = self.eval_expr_visitor(expr.cond, **kwargs)
diff --git a/miasm2/ir/translators/C.py b/miasm2/ir/translators/C.py
index 226f26f1..2f354d47 100644
--- a/miasm2/ir/translators/C.py
+++ b/miasm2/ir/translators/C.py
@@ -18,6 +18,14 @@ class TranslatorC(Translator):
                '>>>': 'rot_right',
                }
 
+    def __init__(self, symbol_pool=None, **kwargs):
+        """Instance a C translator
+        @symbol_pool: AsmSymbolPool instance
+        """
+        super(TranslatorC, self).__init__(**kwargs)
+        # symbol pool
+        self.symbol_pool = symbol_pool
+
     def _size2mask(self, size):
         """Return a C string corresponding to the size2mask operation, with support for
         @size <= 128"""
@@ -31,8 +39,6 @@ class TranslatorC(Translator):
         return "0x%x" % mask
 
     def from_ExprId(self, expr):
-        if isinstance(expr.name, asmblock.AsmLabel):
-            return "0x%x" % expr.name.offset
         return str(expr)
 
     def from_ExprInt(self, expr):
@@ -44,16 +50,32 @@ class TranslatorC(Translator):
             )
         return "0x%x" % expr.arg.arg
 
+    def from_ExprLoc(self, expr):
+        loc_key = expr.loc_key
+        if self.symbol_pool is None:
+            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 name
+        return "0x%x" % offset
+
     def from_ExprAff(self, expr):
-        return "%s = %s" % tuple(map(self.from_expr, (expr.dst, expr.src)))
+        new_dst = self.from_expr(expr.dst)
+        new_src = self.from_expr(expr.src)
+        return "%s = %s" % (new_dst, new_src)
 
     def from_ExprCond(self, expr):
-        return "(%s?%s:%s)" % tuple(map(self.from_expr,
-                                        (expr.cond, expr.src1, expr.src2)))
+        new_cond = self.from_expr(expr.cond)
+        new_src1 = self.from_expr(expr.src1)
+        new_src2 = self.from_expr(expr.src2)
+        return "(%s?%s:%s)" % (new_cond, new_src1, new_src2)
 
     def from_ExprMem(self, expr):
-        return "MEM_LOOKUP_%.2d(jitcpu, %s)" % (expr.size,
-                                                self.from_expr(expr.arg))
+        new_ptr = self.from_expr(expr.arg)
+        return "MEM_LOOKUP_%.2d(jitcpu, %s)" % (expr.size, new_ptr)
 
     def from_ExprOp(self, expr):
         if len(expr.args) == 1:
@@ -63,9 +85,11 @@ class TranslatorC(Translator):
                     self._size2mask(expr.args[0].size),
                 )
             elif expr.op in ['cntleadzeros', 'cnttrailzeros']:
-                return "%s(0x%x, %s)" % (expr.op,
-                                             expr.args[0].size,
-                                             self.from_expr(expr.args[0]))
+                return "%s(0x%x, %s)" % (
+                    expr.op,
+                    expr.args[0].size,
+                    self.from_expr(expr.args[0])
+                )
             elif expr.op == '!':
                 return "(~ %s)&%s" % (
                     self.from_expr(expr.args[0]),
@@ -78,7 +102,10 @@ class TranslatorC(Translator):
                   expr.op.startswith("fxam_c")     or
                   expr.op in ["-", "ftan", "frndint", "f2xm1",
                               "fsin", "fsqrt", "fabs", "fcos", "fchs"]):
-                return "%s(%s)" % (expr.op, self.from_expr(expr.args[0]))
+                return "%s(%s)" % (
+                    expr.op,
+                    self.from_expr(expr.args[0])
+                )
             else:
                 raise NotImplementedError('Unknown op: %r' % expr.op)
 
@@ -91,10 +118,12 @@ class TranslatorC(Translator):
                     self._size2mask(expr.args[1].size),
                 )
             elif expr.op in self.dct_shift:
-                return 'SHIFT_%s(%d, %s, %s)' % (self.dct_shift[expr.op].upper(),
-                                                 expr.args[0].size,
-                                                 self.from_expr(expr.args[0]),
-                                                 self.from_expr(expr.args[1]))
+                return 'SHIFT_%s(%d, %s, %s)' % (
+                    self.dct_shift[expr.op].upper(),
+                    expr.args[0].size,
+                    self.from_expr(expr.args[0]),
+                    self.from_expr(expr.args[1])
+                )
             elif expr.is_associative() or expr.op in ["%", "/"]:
                 oper = ['(%s&%s)' % (
                     self.from_expr(arg),
@@ -105,9 +134,11 @@ class TranslatorC(Translator):
                 return "((%s)&%s)" % (oper, self._size2mask(expr.args[0].size))
             elif expr.op in ['-']:
                 return '(((%s&%s) %s (%s&%s))&%s)' % (
-                    self.from_expr(expr.args[0]), self._size2mask(expr.args[0].size),
+                    self.from_expr(expr.args[0]),
+                    self._size2mask(expr.args[0].size),
                     str(expr.op),
-                    self.from_expr(expr.args[1]), self._size2mask(expr.args[1].size),
+                    self.from_expr(expr.args[1]),
+                    self._size2mask(expr.args[1].size),
                     self._size2mask(expr.args[0].size)
                 )
             elif expr.op in self.dct_rot:
@@ -125,21 +156,29 @@ class TranslatorC(Translator):
             elif (expr.op.startswith("fcom")  or
                   expr.op in ["fadd", "fsub", "fdiv", 'fmul', "fscale",
                               "fprem", "fprem_lsb", "fyl2x", "fpatan"]):
-                return "fpu_%s(%s, %s)" % (expr.op,
-                                           self.from_expr(expr.args[0]),
-                                           self.from_expr(expr.args[1]))
+                return "fpu_%s(%s, %s)" % (
+                    expr.op,
+                    self.from_expr(expr.args[0]),
+                    self.from_expr(expr.args[1])
+                )
             elif expr.op == "segm":
                 return "segm2addr(jitcpu, %s, %s)" % (
-                    self.from_expr(expr.args[0]), self.from_expr(expr.args[1]))
+                    self.from_expr(expr.args[0]),
+                    self.from_expr(expr.args[1])
+                )
             elif expr.op in ['udiv', 'umod', 'idiv', 'imod']:
-                return '%s%d(%s, %s)' % (expr.op,
-                                         expr.args[0].size,
-                                         self.from_expr(expr.args[0]),
-                                         self.from_expr(expr.args[1]))
+                return '%s%d(%s, %s)' % (
+                    expr.op,
+                    expr.args[0].size,
+                    self.from_expr(expr.args[0]),
+                    self.from_expr(expr.args[1])
+                )
             elif expr.op in ["bcdadd", "bcdadd_cf"]:
-                return "%s_%d(%s, %s)" % (expr.op, expr.args[0].size,
-                                          self.from_expr(expr.args[0]),
-                                          self.from_expr(expr.args[1]))
+                return "%s_%d(%s, %s)" % (
+                    expr.op, expr.args[0].size,
+                    self.from_expr(expr.args[0]),
+                    self.from_expr(expr.args[1])
+                )
             else:
                 raise NotImplementedError('Unknown op: %r' % expr.op)
 
@@ -159,9 +198,11 @@ class TranslatorC(Translator):
 
     def from_ExprSlice(self, expr):
         # XXX check mask for 64 bit & 32 bit compat
-        return "((%s>>%d) &%s)" % (self.from_expr(expr.arg),
-                                   expr.start,
-                                   self._size2mask(expr.stop - expr.start))
+        return "((%s>>%d) &%s)" % (
+            self.from_expr(expr.arg),
+            expr.start,
+            self._size2mask(expr.stop - expr.start)
+        )
 
     def from_ExprCompose(self, expr):
         out = []
@@ -178,10 +219,12 @@ class TranslatorC(Translator):
 
         dst_cast = "uint%d_t" % size
         for index, arg in expr.iter_args():
-            out.append("(((%s)(%s & %s)) << %d)" % (dst_cast,
-                                                    self.from_expr(arg),
-                                                    self._size2mask(arg.size),
-                                                    index))
+            out.append("(((%s)(%s & %s)) << %d)" % (
+                dst_cast,
+                self.from_expr(arg),
+                self._size2mask(arg.size),
+                index)
+            )
         out = ' | '.join(out)
         return '(' + out + ')'
 
diff --git a/miasm2/ir/translators/python.py b/miasm2/ir/translators/python.py
index d7369e9e..e05f5e4d 100644
--- a/miasm2/ir/translators/python.py
+++ b/miasm2/ir/translators/python.py
@@ -20,6 +20,9 @@ class TranslatorPython(Translator):
     def from_ExprId(self, expr):
         return str(expr)
 
+    def from_ExprLoc(self, expr):
+        return str(expr)
+
     def from_ExprMem(self, expr):
         return "memory(%s, 0x%x)" % (self.from_expr(expr.arg),
                                      expr.size / 8)
diff --git a/miasm2/ir/translators/smt2.py b/miasm2/ir/translators/smt2.py
index 18bcb9bd..f5d633e0 100644
--- a/miasm2/ir/translators/smt2.py
+++ b/miasm2/ir/translators/smt2.py
@@ -1,7 +1,6 @@
 import logging
 import operator
 
-from miasm2.core.asmblock import AsmLabel
 from miasm2.ir.translators.translator import Translator
 from miasm2.expression.smt2_helper import *
 
@@ -120,7 +119,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,24 +128,33 @@ 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)
 
     def from_ExprId(self, expr):
-        if isinstance(expr.name, AsmLabel):
-            if expr.name.offset is not None:
-                return bit_vec_val(str(expr.name.offset), expr.size)
-            else:
-                # SMT2-escape expression name
-                name = "|{}|".format(str(expr.name))
-                if name not in self._bitvectors:
-                    self._bitvectors[name] = expr.size
-                return name
-        else:
-            if str(expr) not in self._bitvectors:
-                self._bitvectors[str(expr)] = expr.size
-            return str(expr)
+        if str(expr) not in self._bitvectors:
+            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)
diff --git a/miasm2/ir/translators/translator.py b/miasm2/ir/translators/translator.py
index e3641843..557fdabe 100644
--- a/miasm2/ir/translators/translator.py
+++ b/miasm2/ir/translators/translator.py
@@ -53,6 +53,12 @@ class Translator(object):
         """
         raise NotImplementedError("Abstract method")
 
+    def from_ExprLoc(self, expr):
+        """Translate an ExprLoc
+        @expr: ExprLoc to translate
+        """
+        raise NotImplementedError("Abstract method")
+
     def from_ExprCompose(self, expr):
         """Translate an ExprCompose
         @expr: ExprCompose to translate
@@ -100,6 +106,7 @@ class Translator(object):
         # Handle Expr type
         handlers = {m2_expr.ExprInt: self.from_ExprInt,
                     m2_expr.ExprId: self.from_ExprId,
+                    m2_expr.ExprLoc: self.from_ExprLoc,
                     m2_expr.ExprCompose: self.from_ExprCompose,
                     m2_expr.ExprSlice: self.from_ExprSlice,
                     m2_expr.ExprOp: self.from_ExprOp,
diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index 536daff1..d01b73fa 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="<", symbol_pool=None, **kwargs):
         """Instance a Z3 translator
         @endianness: (optional) memory endianness
         """
@@ -126,15 +125,28 @@ class TranslatorZ3(Translator):
 
         super(TranslatorZ3, self).__init__(**kwargs)
         self._mem = Z3Mem(endianness)
+        # symbol pool
+        self.symbol_pool = symbol_pool
 
     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.symbol_pool is None:
+            # No symbol_pool, fallback to default name
             return z3.BitVec(str(expr), expr.size)
+        loc_key = expr.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 not None:
+            return z3.BitVecVal(offset, expr.size)
+        if name is not None:
+            return z3.BitVec(name, 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)