about summary refs log tree commit diff stats
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/analysis/data_flow.py88
-rw-r--r--test/analysis/depgraph.py87
-rwxr-xr-xtest/arch/arm/sem.py4
-rwxr-xr-xtest/arch/msp430/sem.py4
-rwxr-xr-xtest/arch/x86/sem.py11
-rw-r--r--test/core/asmblock.py32
-rw-r--r--test/core/sembuilder.py6
-rw-r--r--test/expression/parser.py3
-rw-r--r--test/ir/translators/z3_ir.py51
9 files changed, 155 insertions, 131 deletions
diff --git a/test/analysis/data_flow.py b/test/analysis/data_flow.py
index d0a85e13..24335f45 100644
--- a/test/analysis/data_flow.py
+++ b/test/analysis/data_flow.py
@@ -1,10 +1,12 @@
 """ Test cases for dead code elimination"""
 from miasm2.expression.expression import ExprId, ExprInt, ExprAff, ExprMem
-from miasm2.core.asmblock import AsmLabel
+from miasm2.core.asmblock import AsmLabel, AsmSymbolPool
 from miasm2.analysis.data_flow import *
 from miasm2.ir.analysis import ira
 from miasm2.ir.ir import IRBlock, AssignBlock
 
+symbol_pool = AsmSymbolPool()
+
 a = ExprId("a", 32)
 b = ExprId("b", 32)
 c = ExprId("c", 32)
@@ -24,13 +26,13 @@ CST1 = ExprInt(0x11, 32)
 CST2 = ExprInt(0x12, 32)
 CST3 = ExprInt(0x13, 32)
 
-LBL0 = AsmLabel("lbl0")
-LBL1 = AsmLabel("lbl1")
-LBL2 = AsmLabel("lbl2")
-LBL3 = AsmLabel("lbl3")
-LBL4 = AsmLabel("lbl4")
-LBL5 = AsmLabel("lbl5")
-LBL6 = AsmLabel("lbl6")
+LBL0 = symbol_pool.add_label("lbl0", 0)
+LBL1 = symbol_pool.add_label("lbl1", 1)
+LBL2 = symbol_pool.add_label("lbl2", 2)
+LBL3 = symbol_pool.add_label("lbl3", 3)
+LBL4 = symbol_pool.add_label("lbl4", 4)
+LBL5 = symbol_pool.add_label("lbl5", 5)
+LBL6 = symbol_pool.add_label("lbl6", 6)
 
 IRDst = ExprId('IRDst', 32)
 dummy = ExprId('dummy', 32)
@@ -45,7 +47,7 @@ def gen_irblock(label, exprs_list):
             irs.append(AssignBlock(exprs))
 
     irs.append(AssignBlock({IRDst:dummy}))
-    irbl = IRBlock(label, irs)
+    irbl = IRBlock(label.loc_key, irs)
     return irbl
 
 
@@ -77,7 +79,7 @@ class IRATest(ira):
 
 # graph 1 : Simple graph with dead and alive variables
 
-G1_IRA = IRATest()
+G1_IRA = IRATest(symbol_pool)
 
 G1_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(b, CST2)]])
 G1_IRB1 = gen_irblock(LBL1, [[ExprAff(a, b)]])
@@ -89,7 +91,7 @@ G1_IRA.graph.add_uniq_edge(G1_IRB0.label, G1_IRB1.label)
 G1_IRA.graph.add_uniq_edge(G1_IRB1.label, G1_IRB2.label)
 
 # Expected output for graph 1
-G1_EXP_IRA = IRATest()
+G1_EXP_IRA = IRATest(symbol_pool)
 
 G1_EXP_IRB0 = gen_irblock(LBL0, [[], [ExprAff(b, CST2)]])
 G1_EXP_IRB1 = gen_irblock(LBL1, [[ExprAff(a, b)]])
@@ -100,7 +102,7 @@ G1_EXP_IRA.blocks = {irb.label : irb for irb in [G1_EXP_IRB0, G1_EXP_IRB1,
 
 # graph 2 : Natural loop with dead variable
 
-G2_IRA = IRATest()
+G2_IRA = IRATest(symbol_pool)
 
 G2_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(r, CST1)]])
 G2_IRB1 = gen_irblock(LBL1, [[ExprAff(a, a+CST1)]])
@@ -113,7 +115,7 @@ G2_IRA.graph.add_uniq_edge(G2_IRB1.label, G2_IRB2.label)
 G2_IRA.graph.add_uniq_edge(G2_IRB1.label, G2_IRB1.label)
 
 # Expected output for graph 2
-G2_EXP_IRA = IRATest()
+G2_EXP_IRA = IRATest(symbol_pool)
 
 G2_EXP_IRB0 = gen_irblock(LBL0, [[], [ExprAff(r, CST1)]])
 G2_EXP_IRB1 = gen_irblock(LBL1, [[]])
@@ -124,7 +126,7 @@ G2_EXP_IRA.blocks = {irb.label : irb for irb in [G2_EXP_IRB0, G2_EXP_IRB1,
 
 # graph 3 : Natural loop with alive variables
 
-G3_IRA = IRATest()
+G3_IRA = IRATest(symbol_pool)
 
 G3_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)]])
 G3_IRB1 = gen_irblock(LBL1, [[ExprAff(a, a+CST1)]])
@@ -137,7 +139,7 @@ G3_IRA.graph.add_uniq_edge(G3_IRB1.label, G3_IRB2.label)
 G3_IRA.graph.add_uniq_edge(G3_IRB1.label, G3_IRB1.label)
 
 # Expected output for graph 3
-G3_EXP_IRA = IRATest()
+G3_EXP_IRA = IRATest(symbol_pool)
 
 G3_EXP_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)]])
 G3_EXP_IRB1 = gen_irblock(LBL1, [[ExprAff(a, a+CST1)]])
@@ -148,7 +150,7 @@ G3_EXP_IRA.blocks = {irb.label : irb for irb in [G3_EXP_IRB0, G3_EXP_IRB1,
 
 # graph 4 : If/else with dead variables
 
-G4_IRA = IRATest()
+G4_IRA = IRATest(symbol_pool)
 
 G4_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)]])
 G4_IRB1 = gen_irblock(LBL1, [[ExprAff(a, a+CST1)]])
@@ -164,7 +166,7 @@ G4_IRA.graph.add_uniq_edge(G4_IRB1.label, G4_IRB3.label)
 G4_IRA.graph.add_uniq_edge(G4_IRB2.label, G4_IRB3.label)
 
 # Expected output for graph 4
-G4_EXP_IRA = IRATest()
+G4_EXP_IRA = IRATest(symbol_pool)
 
 G4_EXP_IRB0 = gen_irblock(LBL0, [[]])
 G4_EXP_IRB1 = gen_irblock(LBL1, [[]])
@@ -176,7 +178,7 @@ G4_EXP_IRA.blocks = {irb.label : irb for irb in [G4_EXP_IRB0, G4_EXP_IRB1,
 
 # graph 5 : Loop and If/else with dead variables
 
-G5_IRA = IRATest()
+G5_IRA = IRATest(symbol_pool)
 
 G5_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)]])
 G5_IRB1 = gen_irblock(LBL1, [[ExprAff(r, CST2)]])
@@ -197,7 +199,7 @@ G5_IRA.graph.add_uniq_edge(G5_IRB4.label, G5_IRB5.label)
 G5_IRA.graph.add_uniq_edge(G5_IRB4.label, G5_IRB1.label)
 
 # Expected output for graph 5
-G5_EXP_IRA = IRATest()
+G5_EXP_IRA = IRATest(symbol_pool)
 
 G5_EXP_IRB0 = gen_irblock(LBL0, [[]])
 G5_EXP_IRB1 = gen_irblock(LBL1, [[ExprAff(r, CST2)]])
@@ -213,7 +215,7 @@ G5_EXP_IRA.blocks = {irb.label : irb for irb in [G5_EXP_IRB0, G5_EXP_IRB1,
 # graph 6 : Natural loop with dead variables symetric affectation
 # (a = b <-> b = a )
 
-G6_IRA = IRATest()
+G6_IRA = IRATest(symbol_pool)
 
 G6_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)]])
 G6_IRB1 = gen_irblock(LBL1, [[ExprAff(b, a)]])
@@ -229,7 +231,7 @@ G6_IRA.graph.add_uniq_edge(G6_IRB2.label, G6_IRB1.label)
 G6_IRA.graph.add_uniq_edge(G6_IRB2.label, G6_IRB3.label)
 
 # Expected output for graph 6
-G6_EXP_IRA = IRATest()
+G6_EXP_IRA = IRATest(symbol_pool)
 
 G6_EXP_IRB0 = gen_irblock(LBL0, [[]])
 G6_EXP_IRB1 = gen_irblock(LBL1, [[]])
@@ -241,7 +243,7 @@ G6_EXP_IRA.blocks = {irb.label : irb for irb in [G6_EXP_IRB0, G6_EXP_IRB1,
 
 # graph 7 : Double entry loop with dead variables
 
-G7_IRA = IRATest()
+G7_IRA = IRATest(symbol_pool)
 
 G7_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(r, CST1)]])
 G7_IRB1 = gen_irblock(LBL1, [[ExprAff(a, a+CST1)]])
@@ -259,7 +261,7 @@ G7_IRA.graph.add_uniq_edge(G7_IRB0.label, G7_IRB2.label)
 
 
 # Expected output for graph 7
-G7_EXP_IRA = IRATest()
+G7_EXP_IRA = IRATest(symbol_pool)
 
 G7_EXP_IRB0 = gen_irblock(LBL0, [[], [ExprAff(r, CST1)]])
 G7_EXP_IRB1 = gen_irblock(LBL1, [[]])
@@ -271,7 +273,7 @@ G7_EXP_IRA.blocks = {irb.label : irb for irb in [G7_EXP_IRB0, G7_EXP_IRB1,
 
 # graph 8 : Nested loops with dead variables
 
-G8_IRA = IRATest()
+G8_IRA = IRATest(symbol_pool)
 
 G8_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(b, CST1)]])
 G8_IRB1 = gen_irblock(LBL1, [[ExprAff(a, a+CST1)]])
@@ -291,7 +293,7 @@ G8_IRA.graph.add_uniq_edge(G8_IRB3.label, G8_IRB2.label)
 
 # Expected output for graph 8
 
-G8_EXP_IRA = IRATest()
+G8_EXP_IRA = IRATest(symbol_pool)
 
 G8_EXP_IRB0 = gen_irblock(LBL0, [[], []])
 G8_EXP_IRB1 = gen_irblock(LBL1, [[]])
@@ -303,7 +305,7 @@ G8_EXP_IRA.blocks = {irb.label : irb for irb in [G8_EXP_IRB0, G8_EXP_IRB1,
 
 # graph 9 : Miultiple-exits loops with dead variables
 
-G9_IRA = IRATest()
+G9_IRA = IRATest(symbol_pool)
 
 G9_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(b, CST1)]])
 G9_IRB1 = gen_irblock(LBL1, [[ExprAff(a, a+CST1)], [ExprAff(b, b+CST1)]])
@@ -326,7 +328,7 @@ G9_IRA.graph.add_uniq_edge(G9_IRB3.label, G9_IRB4.label)
 
 # Expected output for graph 9
 
-G9_EXP_IRA = IRATest()
+G9_EXP_IRA = IRATest(symbol_pool)
 
 G9_EXP_IRB0 = gen_irblock(LBL0, [[], [ExprAff(b, CST1)]])
 G9_EXP_IRB1 = gen_irblock(LBL1, [[], [ExprAff(b, b+CST1)]])
@@ -341,7 +343,7 @@ G9_EXP_IRA.blocks = {irb.label : irb for irb in [G9_EXP_IRB0, G9_EXP_IRB1,
 # graph 10 : Natural loop with alive variables symetric affectation
 # (a = b <-> b = a )
 
-G10_IRA = IRATest()
+G10_IRA = IRATest(symbol_pool)
 
 G10_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)]])
 G10_IRB1 = gen_irblock(LBL1, [[ExprAff(b, a)]])
@@ -357,7 +359,7 @@ G10_IRA.graph.add_uniq_edge(G10_IRB2.label, G10_IRB1.label)
 G10_IRA.graph.add_uniq_edge(G10_IRB2.label, G10_IRB3.label)
 
 # Expected output for graph 10
-G10_EXP_IRA = IRATest()
+G10_EXP_IRA = IRATest(symbol_pool)
 
 G10_EXP_IRB0 = gen_irblock(LBL0, [[]])
 G10_EXP_IRB1 = gen_irblock(LBL1, [[]])
@@ -369,7 +371,7 @@ G10_EXP_IRA.blocks = {irb.label : irb for irb in [G10_EXP_IRB0, G10_EXP_IRB1,
 
 # graph 11 : If/Else conditions with alive variables
 
-G11_IRA = IRATest()
+G11_IRA = IRATest(symbol_pool)
 
 G11_IRB0 = gen_irblock(LBL0, [[ExprAff(a, b)]])
 G11_IRB1 = gen_irblock(LBL1, [[ExprAff(b, a)]])
@@ -388,7 +390,7 @@ G11_IRA.graph.add_uniq_edge(G11_IRB1.label, G11_IRB2.label)
 
 
 # Expected output for graph 11
-G11_EXP_IRA = IRATest()
+G11_EXP_IRA = IRATest(symbol_pool)
 
 G11_EXP_IRB0 = gen_irblock(LBL0, [[ExprAff(a, b)]])
 G11_EXP_IRB1 = gen_irblock(LBL1, [[ExprAff(b, a)]])
@@ -402,7 +404,7 @@ G11_EXP_IRA.blocks = {irb.label : irb for irb in [G11_EXP_IRB0, G11_EXP_IRB1,
 # graph 12 : Graph with multiple out points and useless definitions
 # of return register
 
-G12_IRA = IRATest()
+G12_IRA = IRATest(symbol_pool)
 
 G12_IRB0 = gen_irblock(LBL0, [[ExprAff(r, CST1)], [ExprAff(a, CST2)]])
 G12_IRB1 = gen_irblock(LBL1, [[ExprAff(r, CST2)]])
@@ -421,7 +423,7 @@ G12_IRA.graph.add_uniq_edge(G12_IRB2.label, G12_IRB4.label)
 G12_IRA.graph.add_uniq_edge(G12_IRB4.label, G12_IRB5.label)
 
 # Expected output for graph 12
-G12_EXP_IRA = IRATest()
+G12_EXP_IRA = IRATest(symbol_pool)
 
 G12_EXP_IRB0 = gen_irblock(LBL0, [[], []])
 G12_EXP_IRB1 = gen_irblock(LBL1, [[ExprAff(r, CST2)]])
@@ -437,7 +439,7 @@ G12_EXP_IRA.blocks = {irb.label : irb for irb in [G12_EXP_IRB0, G12_EXP_IRB1,
 
 # graph 13 : Graph where a leaf has lost its son
 
-G13_IRA = IRATest()
+G13_IRA = IRATest(symbol_pool)
 
 G13_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(b, CST2)]])
 G13_IRB1 = gen_irblock(LBL1, [[ExprAff(r, b)]])
@@ -455,7 +457,7 @@ G13_IRA.graph.add_uniq_edge(G13_IRB2.label, G13_IRB3.label)
 G13_IRA.graph.add_uniq_edge(G13_IRB4.label, G13_IRB2.label)
 
 # Expected output for graph 13
-G13_EXP_IRA = IRATest()
+G13_EXP_IRA = IRATest(symbol_pool)
 
 G13_EXP_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(b, CST2)]])
 G13_EXP_IRB1 = gen_irblock(LBL1, [[ExprAff(r, b)]])
@@ -472,7 +474,7 @@ G13_EXP_IRA.blocks = {irb.label: irb for irb in [G13_EXP_IRB0, G13_EXP_IRB1,
 # graph 14 : Graph where variable assigned multiple times in a block but still
 # useful in the end
 
-G14_IRA = IRATest()
+G14_IRA = IRATest(symbol_pool)
 
 G14_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(c, a)],
                               [ExprAff(a, CST2)]])
@@ -483,7 +485,7 @@ G14_IRA.blocks = {irb.label : irb for irb in [G14_IRB0, G14_IRB1]}
 G14_IRA.graph.add_uniq_edge(G14_IRB0.label, G14_IRB1.label)
 
 # Expected output for graph 1
-G14_EXP_IRA = IRATest()
+G14_EXP_IRA = IRATest(symbol_pool)
 
 G14_EXP_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1)], [ExprAff(c, a)],
                                   [ExprAff(a, CST2)]])
@@ -494,7 +496,7 @@ G14_EXP_IRA.blocks = {irb.label: irb for irb in [G14_EXP_IRB0, G14_EXP_IRB1]}
 # graph 15 : Graph where variable assigned multiple and read at the same time,
 # but useless
 
-G15_IRA = IRATest()
+G15_IRA = IRATest(symbol_pool)
 
 G15_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST2)], [ExprAff(a, CST1),
                                                    ExprAff(b, a+CST2),
@@ -506,7 +508,7 @@ G15_IRA.blocks = {irb.label : irb for irb in [G15_IRB0, G15_IRB1]}
 G15_IRA.graph.add_uniq_edge(G15_IRB0.label, G15_IRB1.label)
 
 # Expected output for graph 1
-G15_EXP_IRA = IRATest()
+G15_EXP_IRA = IRATest(symbol_pool)
 
 G15_EXP_IRB0 = gen_irblock(LBL0, [[], [ExprAff(a, CST1)]])
 G15_EXP_IRB1 = gen_irblock(LBL1, [[ExprAff(r, a)]])
@@ -515,7 +517,7 @@ G15_EXP_IRA.blocks = {irb.label: irb for irb in [G15_EXP_IRB0, G15_EXP_IRB1]}
 
 # graph 16 : Graph where variable assigned multiple times in the same bloc
 
-G16_IRA = IRATest()
+G16_IRA = IRATest(symbol_pool)
 
 G16_IRB0 = gen_irblock(LBL0, [[ExprAff(a, CST1), ExprAff(b, CST2),
                                ExprAff(c, CST3)], [ExprAff(a, c+CST1),
@@ -531,7 +533,7 @@ G16_IRA.graph.add_uniq_edge(G16_IRB1.label, G16_IRB2.label)
 G16_IRA.blocks = {irb.label : irb for irb in [G16_IRB0, G16_IRB1]}
 
 # Expected output for graph 1
-G16_EXP_IRA = IRATest()
+G16_EXP_IRA = IRATest(symbol_pool)
 
 G16_EXP_IRB0 = gen_irblock(LBL0, [[ExprAff(c, CST3)], [ExprAff(a, c + CST1),
                                                        ExprAff(b, c + CST2)]])
@@ -541,7 +543,7 @@ G16_EXP_IRA.blocks = {irb.label: irb for irb in [G16_EXP_IRB0, G16_EXP_IRB1]}
 
 # graph 17 : parallel ir
 
-G17_IRA = IRATest()
+G17_IRA = IRATest(symbol_pool)
 
 G17_IRB0 = gen_irblock(LBL0, [[ExprAff(a, a*b),
                                ExprAff(b, c),
@@ -602,7 +604,7 @@ G17_IRA.blocks = {irb.label : irb for irb in [G17_IRB0]}
 G17_IRA.graph.add_node(G17_IRB0.label)
 
 # Expected output for graph 17
-G17_EXP_IRA = IRATest()
+G17_EXP_IRA = IRATest(symbol_pool)
 
 G17_EXP_IRB0 = gen_irblock(LBL0, [[],
 
diff --git a/test/analysis/depgraph.py b/test/analysis/depgraph.py
index 9fb046d0..545269e7 100644
--- a/test/analysis/depgraph.py
+++ b/test/analysis/depgraph.py
@@ -1,6 +1,6 @@
 """Regression test module for DependencyGraph"""
-from miasm2.expression.expression import ExprId, ExprInt, ExprAff, ExprCond
-from miasm2.core.asmblock import AsmLabel
+from miasm2.expression.expression import ExprId, ExprInt, ExprAff, ExprCond, ExprLoc
+from miasm2.core.asmblock import AsmLabel, AsmSymbolPool
 from miasm2.ir.analysis import ira
 from miasm2.ir.ir import IRBlock, AssignBlock
 from miasm2.core.graph import DiGraph
@@ -9,6 +9,8 @@ from itertools import count
 from pdb import pm
 import re
 
+symbol_pool = AsmSymbolPool()
+
 EMULATION = True
 try:
     import z3
@@ -41,13 +43,13 @@ CST33 = ExprInt(0x33, 32)
 CST35 = ExprInt(0x35, 32)
 CST37 = ExprInt(0x37, 32)
 
-LBL0 = AsmLabel("lbl0")
-LBL1 = AsmLabel("lbl1")
-LBL2 = AsmLabel("lbl2")
-LBL3 = AsmLabel("lbl3")
-LBL4 = AsmLabel("lbl4")
-LBL5 = AsmLabel("lbl5")
-LBL6 = AsmLabel("lbl6")
+LBL0 = symbol_pool.add_label("lbl0", 0)
+LBL1 = symbol_pool.add_label("lbl1", 1)
+LBL2 = symbol_pool.add_label("lbl2", 2)
+LBL3 = symbol_pool.add_label("lbl3", 3)
+LBL4 = symbol_pool.add_label("lbl4", 4)
+LBL5 = symbol_pool.add_label("lbl5", 5)
+LBL6 = symbol_pool.add_label("lbl6", 6)
 
 def gen_irblock(label, exprs_list):
     """ Returns an IRBlock.
@@ -60,7 +62,7 @@ def gen_irblock(label, exprs_list):
         else:
             irs.append(AssignBlock(exprs))
 
-    irbl = IRBlock(label, irs)
+    irbl = IRBlock(label.loc_key, irs)
     return irbl
 
 
@@ -186,7 +188,8 @@ def dg2graph(graph, label=False, lines=True):
     out_blocks = []
     for label in graph.nodes():
         if isinstance(label, DependencyNode):
-            label_name = "%s %s %s" % (label.label.name,
+            lbl = symbol_pool.loc_key_to_label(label.label)
+            label_name = "%s %s %s" % (lbl.name,
                                        label.element,
                                        label.line_nb)
         else:
@@ -228,7 +231,7 @@ DNC3 = DependencyNode(LBL1, C, 0)
 
 # graph 1
 
-G1_IRA = IRATest()
+G1_IRA = IRATest(symbol_pool)
 
 G1_IRB0 = gen_irblock(LBL0, [[ExprAff(C, CST1)]])
 G1_IRB1 = gen_irblock(LBL1, [[ExprAff(B, C)]])
@@ -241,7 +244,7 @@ G1_IRA.blocks = dict([(irb.label, irb) for irb in [G1_IRB0, G1_IRB1, G1_IRB2]])
 
 # graph 2
 
-G2_IRA = IRATest()
+G2_IRA = IRATest(symbol_pool)
 
 G2_IRB0 = gen_irblock(LBL0, [[ExprAff(C, CST1)]])
 G2_IRB1 = gen_irblock(LBL1, [[ExprAff(B, CST2)]])
@@ -255,7 +258,7 @@ G2_IRA.blocks = dict([(irb.label, irb) for irb in [G2_IRB0, G2_IRB1, G2_IRB2]])
 
 # graph 3
 
-G3_IRA = IRATest()
+G3_IRA = IRATest(symbol_pool)
 
 G3_IRB0 = gen_irblock(LBL0, [[ExprAff(C, CST1)]])
 G3_IRB1 = gen_irblock(LBL1, [[ExprAff(B, CST2)]])
@@ -272,13 +275,13 @@ G3_IRA.blocks = dict([(irb.label, irb) for irb in [G3_IRB0, G3_IRB1,
 
 # graph 4
 
-G4_IRA = IRATest()
+G4_IRA = IRATest(symbol_pool)
 
 G4_IRB0 = gen_irblock(LBL0, [[ExprAff(C, CST1)]])
 G4_IRB1 = gen_irblock(LBL1, [[ExprAff(C, C + CST2)],
                              [ExprAff(G4_IRA.IRDst,
-                                      ExprCond(C, ExprId(LBL2, 32),
-                                               ExprId(LBL1, 32)))]])
+                                      ExprCond(C, ExprLoc(LBL2.loc_key, 32),
+                                               ExprLoc(LBL1.loc_key, 32)))]])
 
 G4_IRB2 = gen_irblock(LBL2, [[ExprAff(A, B)]])
 
@@ -291,13 +294,13 @@ G4_IRA.blocks = dict([(irb.label, irb) for irb in [G4_IRB0, G4_IRB1, G4_IRB2]])
 
 # graph 5
 
-G5_IRA = IRATest()
+G5_IRA = IRATest(symbol_pool)
 
 G5_IRB0 = gen_irblock(LBL0, [[ExprAff(B, CST1)]])
 G5_IRB1 = gen_irblock(LBL1, [[ExprAff(B, B + CST2)],
                              [ExprAff(G5_IRA.IRDst,
-                                      ExprCond(B, ExprId(LBL2, 32),
-                                               ExprId(LBL1, 32)))]])
+                                      ExprCond(B, ExprLoc(LBL2.loc_key, 32),
+                                               ExprLoc(LBL1.loc_key, 32)))]])
 
 G5_IRB2 = gen_irblock(LBL2, [[ExprAff(A, B)]])
 
@@ -309,7 +312,7 @@ G5_IRA.blocks = dict([(irb.label, irb) for irb in [G5_IRB0, G5_IRB1, G5_IRB2]])
 
 # graph 6
 
-G6_IRA = IRATest()
+G6_IRA = IRATest(symbol_pool)
 
 G6_IRB0 = gen_irblock(LBL0, [[ExprAff(B, CST1)]])
 G6_IRB1 = gen_irblock(LBL1, [[ExprAff(A, B)]])
@@ -321,7 +324,7 @@ G6_IRA.blocks = dict([(irb.label, irb) for irb in [G6_IRB0, G6_IRB1]])
 
 # graph 7
 
-G7_IRA = IRATest()
+G7_IRA = IRATest(symbol_pool)
 
 G7_IRB0 = gen_irblock(LBL0, [[ExprAff(C, CST1)]])
 G7_IRB1 = gen_irblock(LBL1, [[ExprAff(B, C)], [ExprAff(A, B)]])
@@ -335,7 +338,7 @@ G7_IRA.blocks = dict([(irb.label, irb) for irb in [G7_IRB0, G7_IRB1, G7_IRB2]])
 
 # graph 8
 
-G8_IRA = IRATest()
+G8_IRA = IRATest(symbol_pool)
 
 G8_IRB0 = gen_irblock(LBL0, [[ExprAff(C, CST1)]])
 G8_IRB1 = gen_irblock(LBL1, [[ExprAff(B, C)], [ExprAff(C, D)]])
@@ -351,7 +354,7 @@ G8_IRA.blocks = dict([(irb.label, irb) for irb in [G8_IRB0, G8_IRB1, G8_IRB2]])
 
 # graph 10
 
-G10_IRA = IRATest()
+G10_IRA = IRATest(symbol_pool)
 
 G10_IRB1 = gen_irblock(LBL1, [[ExprAff(B, B + CST2)]])
 G10_IRB2 = gen_irblock(LBL2, [[ExprAff(A, B)]])
@@ -363,7 +366,7 @@ G10_IRA.blocks = dict([(irb.label, irb) for irb in [G10_IRB1, G10_IRB2]])
 
 # graph 11
 
-G11_IRA = IRATest()
+G11_IRA = IRATest(symbol_pool)
 
 G11_IRB0 = gen_irblock(LBL0, [[ExprAff(A, CST1),
                                ExprAff(B, CST2)]])
@@ -379,7 +382,7 @@ G11_IRA.blocks = dict([(irb.label, irb)
 
 # graph 12
 
-G12_IRA = IRATest()
+G12_IRA = IRATest(symbol_pool)
 
 G12_IRB0 = gen_irblock(LBL0, [[ExprAff(B, CST1)]])
 G12_IRB1 = gen_irblock(LBL1, [[ExprAff(A, B)], [ExprAff(B, B + CST2)]])
@@ -395,21 +398,21 @@ G12_IRA.blocks = dict([(irb.label, irb) for irb in [G12_IRB0, G12_IRB1,
 
 # graph 13
 
-G13_IRA = IRATest()
+G13_IRA = IRATest(symbol_pool)
 
 G13_IRB0 = gen_irblock(LBL0, [[ExprAff(A, CST1)],
                               #[ExprAff(B, A)],
                               [ExprAff(G13_IRA.IRDst,
-                                       ExprId(LBL1, 32))]])
+                                       ExprLoc(LBL1.loc_key, 32))]])
 G13_IRB1 = gen_irblock(LBL1, [[ExprAff(C, A)],
                               #[ExprAff(A, A + CST1)],
                               [ExprAff(G13_IRA.IRDst,
-                                       ExprCond(R, ExprId(LBL2, 32),
-                                                ExprId(LBL1, 32)))]])
+                                       ExprCond(R, ExprLoc(LBL2.loc_key, 32),
+                                                ExprLoc(LBL1.loc_key, 32)))]])
 
 G13_IRB2 = gen_irblock(LBL2, [[ExprAff(B, A + CST3)], [ExprAff(A, B + CST3)],
                               [ExprAff(G13_IRA.IRDst,
-                                       ExprId(LBL1, 32))]])
+                                       ExprLoc(LBL1.loc_key, 32))]])
 
 G13_IRB3 = gen_irblock(LBL3, [[ExprAff(R, C)]])
 
@@ -423,22 +426,22 @@ G13_IRA.blocks = dict([(irb.label, irb) for irb in [G13_IRB0, G13_IRB1,
 
 # graph 14
 
-G14_IRA = IRATest()
+G14_IRA = IRATest(symbol_pool)
 
 G14_IRB0 = gen_irblock(LBL0, [[ExprAff(A, CST1)],
                               [ExprAff(G14_IRA.IRDst,
-                                       ExprId(LBL1, 32))]
+                                       ExprLoc(LBL1.loc_key, 32))]
                              ])
 G14_IRB1 = gen_irblock(LBL1, [[ExprAff(B, A)],
                               [ExprAff(G14_IRA.IRDst,
-                                       ExprCond(C, ExprId(LBL2, 32),
-                                                ExprId(LBL3, 32)))]
+                                       ExprCond(C, ExprLoc(LBL2.loc_key, 32),
+                                                ExprLoc(LBL3.loc_key, 32)))]
                              ])
 
 G14_IRB2 = gen_irblock(LBL2, [[ExprAff(D, A)],
                               [ExprAff(A, D + CST1)],
                               [ExprAff(G14_IRA.IRDst,
-                                       ExprId(LBL1, 32))]
+                                       ExprLoc(LBL1.loc_key, 32))]
                              ])
 
 G14_IRB3 = gen_irblock(LBL3, [[ExprAff(R, D + B)]])
@@ -453,7 +456,7 @@ G14_IRA.blocks = dict([(irb.label, irb) for irb in [G14_IRB0, G14_IRB1,
 
 # graph 16
 
-G15_IRA = IRATest()
+G15_IRA = IRATest(symbol_pool)
 
 G15_IRB0 = gen_irblock(LBL0, [[ExprAff(A, CST1)]])
 G15_IRB1 = gen_irblock(LBL1, [[ExprAff(D, A + B)],
@@ -470,7 +473,7 @@ G15_IRA.blocks = dict([(irb.label, irb) for irb in [G15_IRB0, G15_IRB1,
 
 # graph 16
 
-G16_IRA = IRATest()
+G16_IRA = IRATest(symbol_pool)
 
 G16_IRB0 = gen_irblock(LBL0, [[ExprAff(A, CST1)]])
 G16_IRB1 = gen_irblock(LBL1, [[ExprAff(R, D)]])
@@ -494,7 +497,7 @@ G16_IRA.blocks = dict([(irb.label, irb) for irb in [G16_IRB0, G16_IRB1,
 
 # graph 17
 
-G17_IRA = IRATest()
+G17_IRA = IRATest(symbol_pool)
 
 G17_IRB0 = gen_irblock(LBL0, [[ExprAff(A, CST1),
                                ExprAff(D, CST2)]])
@@ -638,7 +641,8 @@ def flatNode(node):
             element = int(node.element.arg)
         else:
             RuntimeError("Unsupported type '%s'" % type(enode.element))
-        return (node.label.name,
+        label = symbol_pool.loc_key_to_label(node.label)
+        return (label.name,
                 element,
                 node.line_nb)
     else:
@@ -736,7 +740,8 @@ def match_results(resultsA, resultsB, nodes):
 def get_flat_init_depnodes(depnodes):
     out = []
     for node in depnodes:
-        out.append((node.label.name,
+        label = symbol_pool.loc_key_to_label(node.label)
+        out.append((label.name,
                     node.element.name,
                     node.line_nb,
                     0))
diff --git a/test/arch/arm/sem.py b/test/arch/arm/sem.py
index d9e6aa76..05d26f5c 100755
--- a/test/arch/arm/sem.py
+++ b/test/arch/arm/sem.py
@@ -30,8 +30,8 @@ def compute(asm, inputstate={}, debug=False):
     code = mn.asm(instr)[0]
     instr = mn.dis(code, "l")
     instr.offset = inputstate.get(PC, 0)
-    interm.add_instr(instr)
-    symexec.run_at(instr.offset)
+    lbl = interm.add_instr(instr)
+    symexec.run_at(lbl)
     if debug:
         for k, v in symexec.symbols.items():
             if regs_init.get(k, None) != v:
diff --git a/test/arch/msp430/sem.py b/test/arch/msp430/sem.py
index 3b2c2f2e..a7a9e4be 100755
--- a/test/arch/msp430/sem.py
+++ b/test/arch/msp430/sem.py
@@ -26,8 +26,8 @@ def compute(asm, inputstate={}, debug=False):
     code = mn.asm(instr)[0]
     instr = mn.dis(code, mode)
     instr.offset = inputstate.get(PC, 0)
-    interm.add_instr(instr)
-    symexec.run_at(instr.offset)
+    lbl = interm.add_instr(instr)
+    symexec.run_at(lbl, step=True)
     if debug:
         for k, v in symexec.symbols.items():
             if regs_init.get(k, None) != v:
diff --git a/test/arch/x86/sem.py b/test/arch/x86/sem.py
index b3b7e940..78cbc243 100755
--- a/test/arch/x86/sem.py
+++ b/test/arch/x86/sem.py
@@ -25,11 +25,11 @@ symbol_pool = AsmSymbolPool()
 m32 = 32
 m64 = 64
 
-def symb_exec(interm, inputstate, debug):
+def symb_exec(lbl, interm, inputstate, debug):
     sympool = dict(regs_init)
     sympool.update(inputstate)
     symexec = SymbolicExecutionEngine(interm, sympool)
-    symexec.run_at(0)
+    symexec.run_at(lbl)
     if debug:
         for k, v in symexec.symbols.items():
             if regs_init.get(k, None) != v:
@@ -43,8 +43,8 @@ def compute(ir, mode, asm, inputstate={}, debug=False):
     instr = mn.dis(code, mode)
     instr.offset = inputstate.get(EIP, 0)
     interm = ir()
-    interm.add_instr(instr)
-    return symb_exec(interm, inputstate, debug)
+    lbl = interm.add_instr(instr)
+    return symb_exec(lbl, interm, inputstate, debug)
 
 
 def compute_txt(ir, mode, txt, inputstate={}, debug=False):
@@ -52,9 +52,10 @@ def compute_txt(ir, mode, txt, inputstate={}, debug=False):
     symbol_pool.set_offset(symbol_pool.getby_name("main"), 0x0)
     patches = asmblock.asm_resolve_final(mn, blocks, symbol_pool)
     interm = ir(symbol_pool)
+    lbl = symbol_pool.getby_name("main")
     for bbl in blocks:
         interm.add_block(bbl)
-    return symb_exec(interm, inputstate, debug)
+    return symb_exec(lbl, interm, inputstate, debug)
 
 op_add = lambda a, b: a+b
 op_sub = lambda a, b: a-b
diff --git a/test/core/asmblock.py b/test/core/asmblock.py
index 7f0dbc5f..5d240c56 100644
--- a/test/core/asmblock.py
+++ b/test/core/asmblock.py
@@ -104,7 +104,8 @@ open("graph2.dot", "w").write(blocks.dot())
 # Test helper methods
 ## Label2block should always be updated
 assert blocks.label2block(first_block.label) == first_block
-my_block = AsmBlock(AsmLabel("testlabel"))
+testlabel = mdis.symbol_pool.getby_name_create("testlabel")
+my_block = AsmBlock(testlabel)
 blocks.add_node(my_block)
 assert len(blocks) == 3
 assert blocks.label2block(first_block.label) == first_block
@@ -114,7 +115,8 @@ assert blocks.label2block(my_block.label) == my_block
 assert len(list(blocks.get_bad_blocks())) == 0
 assert len(list(blocks.get_bad_blocks_predecessors())) == 0
 ### Add a bad block, not linked
-my_bad_block = AsmBlockBad(AsmLabel("testlabel_bad"))
+testlabel_bad = mdis.symbol_pool.getby_name_create("testlabel_bad")
+my_bad_block = AsmBlockBad(testlabel_bad)
 blocks.add_node(my_bad_block)
 assert list(blocks.get_bad_blocks()) == [my_bad_block]
 assert len(list(blocks.get_bad_blocks_predecessors())) == 0
@@ -132,7 +134,8 @@ assert len(list(blocks.get_bad_blocks_predecessors(strict=True))) == 0
 ## Sanity check
 blocks.sanity_check()
 ### Next on itself
-my_block_ni = AsmBlock(AsmLabel("testlabel_nextitself"))
+testlabel_nextitself = mdis.symbol_pool.getby_name_create("testlabel_nextitself")
+my_block_ni = AsmBlock(testlabel_nextitself)
 my_block_ni.bto.add(AsmConstraintNext(my_block_ni.label))
 blocks.add_node(my_block_ni)
 error_raised = False
@@ -145,10 +148,13 @@ assert error_raised
 blocks.del_node(my_block_ni)
 blocks.sanity_check()
 ### Multiple next on the same node
-my_block_target = AsmBlock(AsmLabel("testlabel_target"))
+testlabel_target = mdis.symbol_pool.getby_name_create("testlabel_target")
+my_block_target = AsmBlock(testlabel_target)
 blocks.add_node(my_block_target)
-my_block_src1 = AsmBlock(AsmLabel("testlabel_src1"))
-my_block_src2 = AsmBlock(AsmLabel("testlabel_src2"))
+testlabel_src1 = mdis.symbol_pool.getby_name_create("testlabel_src1")
+testlabel_src2 = mdis.symbol_pool.getby_name_create("testlabel_src2")
+my_block_src1 = AsmBlock(testlabel_src1)
+my_block_src2 = AsmBlock(testlabel_src2)
 my_block_src1.bto.add(AsmConstraintNext(my_block_target.label))
 blocks.add_node(my_block_src1)
 ### OK for now
@@ -177,8 +183,10 @@ assert blocks.label2block(my_block_src1.label).max_size == 0
 
 ## Check pendings
 ### Create a pending element
-my_block_src = AsmBlock(AsmLabel("testlabel_pend_src"))
-my_block_dst = AsmBlock(AsmLabel("testlabel_pend_dst"))
+testlabel_pend_src = mdis.symbol_pool.getby_name_create("testlabel_pend_src")
+testlabel_pend_dst = mdis.symbol_pool.getby_name_create("testlabel_pend_dst")
+my_block_src = AsmBlock(testlabel_pend_src)
+my_block_dst = AsmBlock(testlabel_pend_dst)
 my_block_src.bto.add(AsmConstraintTo(my_block_dst.label))
 blocks.add_node(my_block_src)
 ### Check resulting state
@@ -238,7 +246,7 @@ assert len(entry_block.lines) == 4
 assert map(str, entry_block.lines) == ['XOR        EAX, EAX',
                                        'XOR        EBX, EBX',
                                        'XOR        ECX, ECX',
-                                       'JNZ        loc_0000000000000014:0x00000014']
+                                       'JNZ        label_3']
 assert len(blocks.successors(entry_block)) == 2
 assert len(entry_block.bto) == 2
 nextb = blocks.label2block((cons.label for cons in entry_block.bto
@@ -249,11 +257,11 @@ assert len(nextb.lines) == 4
 assert map(str, nextb.lines) == ['XOR        EDX, EDX',
                                  'XOR        ESI, ESI',
                                  'XOR        EDI, EDI',
-                                 'JMP        loc_0000000000000008:0x00000008']
+                                 'JMP        label_4']
 assert blocks.successors(nextb) == [nextb]
 assert len(tob.lines) == 2
 assert map(str, tob.lines) == ['XOR        EBP, EBP',
-                               'JMP        loc_0000000000000014:0x00000014']
+                               'JMP        label_3']
 assert blocks.successors(tob) == [tob]
 
 # Check split_block
@@ -278,7 +286,7 @@ assert len(blocks.successors(entry_block)) == 1
 newb = blocks.successors(entry_block)[0]
 assert len(newb.lines) == 2
 assert map(str, newb.lines) == ['XOR        ECX, ECX',
-                                'JNZ        loc_0000000000000014:0x00000014']
+                                'JNZ        label_3']
 preds = blocks.predecessors(newb)
 assert len(preds) == 2
 assert entry_block in preds
diff --git a/test/core/sembuilder.py b/test/core/sembuilder.py
index ebf9f385..f3894927 100644
--- a/test/core/sembuilder.py
+++ b/test/core/sembuilder.py
@@ -11,13 +11,13 @@ class IR(object):
     IRDst = m2_expr.ExprId("IRDst", 32)
 
     def get_next_instr(self, _):
-        return AsmLabel("NEXT")
+        return AsmLabel(m2_expr.LocKey(0), "NEXT")
 
     def get_next_label(self, _):
-        return AsmLabel("NEXT")
+        return AsmLabel(m2_expr.LocKey(0), "NEXT")
 
     def gen_label(self):
-        return AsmLabel("GEN")
+        return AsmLabel(m2_expr.LocKey(1), "GEN")
 
 class Instr(object):
     mode = 32
diff --git a/test/expression/parser.py b/test/expression/parser.py
index 9c01c8a1..1d5889fb 100644
--- a/test/expression/parser.py
+++ b/test/expression/parser.py
@@ -1,9 +1,10 @@
 from miasm2.expression.parser import str_to_expr
 from miasm2.expression.expression import ExprInt, ExprId, ExprSlice, ExprMem, \
-    ExprCond, ExprCompose, ExprOp, ExprAff
+    ExprCond, ExprCompose, ExprOp, ExprAff, ExprLoc, LocKey
 
 for expr_test in [ExprInt(0x12, 32),
                   ExprId('test', 32),
+                  ExprLoc(LocKey(12), 32),
                   ExprSlice(ExprInt(0x10, 32), 0, 8),
                   ExprMem(ExprInt(0x10, 32), 32),
                   ExprCond(ExprInt(0x10, 32), ExprInt(0x11, 32), ExprInt(0x12, 32)),
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index 6ae2dcd0..643c59e4 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 AsmLabel, 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_label("label_histoire", 0xdeadbeef)
+e7 = ExprLoc(label_histoire.loc_key, 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_label("label_jambe")
+
+e8 = ExprLoc(lbl_e8.loc_key, 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."