about summary refs log tree commit diff stats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--README.md317
-rw-r--r--example/expression/solve_condition_stp.py27
-rw-r--r--example/symbol_exec/single_instr.py2
-rw-r--r--miasm2/analysis/data_analysis.py30
-rw-r--r--miasm2/analysis/depgraph.py4
-rw-r--r--miasm2/ir/ir.py14
-rw-r--r--miasm2/ir/symbexec.py17
-rw-r--r--test/analysis/dg_test_02_implicit_expected.json2
-rw-r--r--test/analysis/dg_test_04_expected.json2
-rw-r--r--test/analysis/dg_test_04_implicit_expected.json2
-rw-r--r--test/analysis/dg_test_06_implicit_expected.json2
-rw-r--r--test/analysis/dg_test_10_implicit_expected.json2
-rwxr-xr-xtest/arch/arm/sem.py2
-rwxr-xr-xtest/ir/symbexec.py4
14 files changed, 247 insertions, 180 deletions
diff --git a/README.md b/README.md
index e3f16159..f4464eaf 100644
--- a/README.md
+++ b/README.md
@@ -113,9 +113,9 @@ Print current pool:
 ...
 loc_0000000000000000:0x00000000
 
-        R2 = (R8+R0)
+	R2 = (R8+R0)
 
-        IRDst = loc_0000000000000004:0x00000004
+	IRDst = loc_0000000000000004:0x00000004
 ```
 Working with IR, for instance by getting side effects:
 ```
@@ -167,25 +167,24 @@ Disassembling the shellcode at address `0`:
 >>> mdis = machine.dis_engine(c.bin_stream)
 >>> asmcfg = mdis.dis_multiblock(0)
 >>> for block in asmcfg.blocks:
-...  print block
+...  print block.to_string(asmcfg.loc_db)
 ...
-loc_0000000000000000:0x00000000
-LEA        ECX, DWORD PTR [ECX+0x4]
-LEA        EBX, DWORD PTR [EBX+0x1]
+loc_0
+LEA        ECX, DWORD PTR [ECX + 0x4]
+LEA        EBX, DWORD PTR [EBX + 0x1]
 CMP        CL, 0x1
-JZ         loc_0000000000000010:0x00000010
-->      c_next:loc_000000000000000B:0x0000000b  c_to:loc_0000000000000010:0x00000010
-loc_0000000000000010:0x00000010
-LEA        EBX, DWORD PTR [EBX+0x1]
-->      c_next:loc_0000000000000013:0x00000013
-loc_000000000000000B:0x0000000b
-LEA        EBX, DWORD PTR [EBX+0xFFFFFFFF]
-JMP        loc_0000000000000013:0x00000013
-->      c_to:loc_0000000000000013:0x00000013
-loc_0000000000000013:0x00000013
+JZ         loc_10
+->      c_next:loc_b    c_to:loc_10
+loc_10
+LEA        EBX, DWORD PTR [EBX + 0x1]
+->      c_next:loc_13
+loc_b
+LEA        EBX, DWORD PTR [EBX + 0xFFFFFFFF]
+JMP        loc_13
+->      c_to:loc_13
+loc_13
 MOV        EAX, EBX
 RET
->>>
 ```
 
 Initializing the Jit engine with a stack:
@@ -267,9 +266,11 @@ Symbolic execution
 Initializing the IR pool:
 
 ```
->>> ira = machine.ira()
+>>> ira = machine.ira(loc_db=mdis.loc_db)
+>>>
 >>> for block in asmcfg.blocks:
-...    ira.add_block(block)
+...  ira.add_block(block)
+...
 ...
 ```
 
@@ -277,7 +278,7 @@ Initializing the engine with default symbolic values:
 
 ```
 >>> from miasm2.ir.symbexec import SymbolicExecutionEngine
->>> sb = SymbolicExecutionEngine(ira, machine.mn.regs.regs_init)
+>>> sb = SymbolicExecutionEngine(ira)
 ```
 
 Launching the execution:
@@ -285,135 +286,203 @@ Launching the execution:
 ```
 >>> symbolic_pc = sb.run_at(0)
 >>> print symbolic_pc
-((ECX_init+0x4)[0:8]+0xFF)?(0xB,0x10)
+((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
 ```
 
 Same, with step logs (only changes are displayed):
 
 ```
->>> sb = SymbolicExecutionEngine(ira, machine.mn.regs.regs_init)
+>>> sb = SymbolicExecutionEngine(ira)
 >>> symbolic_pc = sb.run_at(0, step=True)
+Instr LEA        ECX, DWORD PTR [ECX + 0x4]
+Assignblk:
+ECX = ECX + 0x4
 ________________________________________________________________________________
-ECX (ECX_init+0x4)
+ECX                = ECX + 0x4
 ________________________________________________________________________________
-ECX (ECX_init+0x4)
-EBX (EBX_init+0x1)
+Instr LEA        EBX, DWORD PTR [EBX + 0x1]
+Assignblk:
+EBX = EBX + 0x1
 ________________________________________________________________________________
-zf ((ECX_init+0x4)[0:8]+0xFF)?(0x0,0x1)
-nf ((ECX_init+0x4)[0:8]+0xFF)[7:8]
-pf (parity ((ECX_init+0x4)[0:8]+0xFF))
-of ((((ECX_init+0x4)[0:8]+0xFF)^(ECX_init+0x4)[0:8])&((ECX_init+0x4)[0:8]^0x1))[7:8]
-cf (((((ECX_init+0x4)[0:8]+0xFF)^(ECX_init+0x4)[0:8])&((ECX_init+0x4)[0:8]^0x1))^((ECX_init+0x4)[0:8]+0xFF)^(ECX_init+0x4)[0:8]^0x1)[7:8]
-af (((ECX_init+0x4)[0:8]+0xFF)&0x10)?(0x1,0x0)
-ECX (ECX_init+0x4)
-EBX (EBX_init+0x1)
+EBX                = EBX + 0x1
+ECX                = ECX + 0x4
 ________________________________________________________________________________
-IRDst ((ECX_init+0x4)[0:8]+0xFF)?(0xB,0x10)
-zf ((ECX_init+0x4)[0:8]+0xFF)?(0x0,0x1)
-nf ((ECX_init+0x4)[0:8]+0xFF)[7:8]
-pf (parity ((ECX_init+0x4)[0:8]+0xFF))
-of ((((ECX_init+0x4)[0:8]+0xFF)^(ECX_init+0x4)[0:8])&((ECX_init+0x4)[0:8]^0x1))[7:8]
-cf (((((ECX_init+0x4)[0:8]+0xFF)^(ECX_init+0x4)[0:8])&((ECX_init+0x4)[0:8]^0x1))^((ECX_init+0x4)[0:8]+0xFF)^(ECX_init+0x4)[0:8]^0x1)[7:8]
-af (((ECX_init+0x4)[0:8]+0xFF)&0x10)?(0x1,0x0)
-EIP ((ECX_init+0x4)[0:8]+0xFF)?(0xB,0x10)
-ECX (ECX_init+0x4)
-EBX (EBX_init+0x1)
+Instr CMP        CL, 0x1
+Assignblk:
+zf = (ECX[0:8] + -0x1)?(0x0,0x1)
+nf = (ECX[0:8] + -0x1)[7:8]
+pf = parity((ECX[0:8] + -0x1) & 0xFF)
+of = ((ECX[0:8] ^ (ECX[0:8] + -0x1)) & (ECX[0:8] ^ 0x1))[7:8]
+cf = (((ECX[0:8] ^ 0x1) ^ (ECX[0:8] + -0x1)) ^ ((ECX[0:8] ^ (ECX[0:8] + -0x1)) & (ECX[0:8] ^ 0x1)))[7:8]
+af = ((ECX[0:8] ^ 0x1) ^ (ECX[0:8] + -0x1))[4:5]
+________________________________________________________________________________
+af                 = (((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[4:5]
+pf                 = parity((ECX + 0x4)[0:8] + 0xFF)
+zf                 = ((ECX + 0x4)[0:8] + 0xFF)?(0x0,0x1)
+ECX                = ECX + 0x4
+of                 = ((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1))[7:8]
+nf                 = ((ECX + 0x4)[0:8] + 0xFF)[7:8]
+cf                 = (((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1)) ^ ((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[7:8]
+EBX                = EBX + 0x1
+________________________________________________________________________________
+Instr JZ         loc_key_1
+Assignblk:
+IRDst = zf?(loc_key_1,loc_key_2)
+EIP = zf?(loc_key_1,loc_key_2)
+________________________________________________________________________________
+af                 = (((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[4:5]
+EIP                = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+pf                 = parity((ECX + 0x4)[0:8] + 0xFF)
+IRDst              = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+zf                 = ((ECX + 0x4)[0:8] + 0xFF)?(0x0,0x1)
+ECX                = ECX + 0x4
+of                 = ((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1))[7:8]
+nf                 = ((ECX + 0x4)[0:8] + 0xFF)[7:8]
+cf                 = (((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1)) ^ ((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[7:8]
+EBX                = EBX + 0x1
+________________________________________________________________________________
+>>>
 ```
 
 
 Retry execution with a concrete ECX. Here, the symbolic / concolic execution reach the shellcode's end:
 
 ```
->>> from miasm2.expression.expression import ExprInt32
->>> sb.symbols[machine.mn.regs.ECX] = ExprInt32(-3)
+>>> from miasm2.expression.expression import ExprInt
+>>> sb.symbols[machine.mn.regs.ECX] = ExprInt(-3, 32)
 >>> symbolic_pc = sb.run_at(0, step=True)
+Instr LEA        ECX, DWORD PTR [ECX + 0x4]
+Assignblk:
+ECX = ECX + 0x4
 ________________________________________________________________________________
-ECX 0x1
+af                 = (((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[4:5]
+EIP                = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+pf                 = parity((ECX + 0x4)[0:8] + 0xFF)
+IRDst              = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+zf                 = ((ECX + 0x4)[0:8] + 0xFF)?(0x0,0x1)
+ECX                = 0x1
+of                 = ((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1))[7:8]
+nf                 = ((ECX + 0x4)[0:8] + 0xFF)[7:8]
+cf                 = (((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1)) ^ ((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[7:8]
+EBX                = EBX + 0x1
 ________________________________________________________________________________
-ECX 0x1
-EBX (EBX_init+0x1)
+Instr LEA        EBX, DWORD PTR [EBX + 0x1]
+Assignblk:
+EBX = EBX + 0x1
 ________________________________________________________________________________
-zf 0x1
-nf 0x0
-pf 0x1
-of 0x0
-cf 0x0
-af 0x0
-ECX 0x1
-EBX (EBX_init+0x1)
+af                 = (((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[4:5]
+EIP                = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+pf                 = parity((ECX + 0x4)[0:8] + 0xFF)
+IRDst              = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+zf                 = ((ECX + 0x4)[0:8] + 0xFF)?(0x0,0x1)
+ECX                = 0x1
+of                 = ((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1))[7:8]
+nf                 = ((ECX + 0x4)[0:8] + 0xFF)[7:8]
+cf                 = (((((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8]) & ((ECX + 0x4)[0:8] ^ 0x1)) ^ ((ECX + 0x4)[0:8] + 0xFF) ^ (ECX + 0x4)[0:8] ^ 0x1)[7:8]
+EBX                = EBX + 0x2
 ________________________________________________________________________________
-IRDst 0x10
-zf 0x1
-nf 0x0
-pf 0x1
-of 0x0
-cf 0x0
-af 0x0
-EIP 0x10
-ECX 0x1
-EBX (EBX_init+0x1)
+Instr CMP        CL, 0x1
+Assignblk:
+zf = (ECX[0:8] + -0x1)?(0x0,0x1)
+nf = (ECX[0:8] + -0x1)[7:8]
+pf = parity((ECX[0:8] + -0x1) & 0xFF)
+of = ((ECX[0:8] ^ (ECX[0:8] + -0x1)) & (ECX[0:8] ^ 0x1))[7:8]
+cf = (((ECX[0:8] ^ 0x1) ^ (ECX[0:8] + -0x1)) ^ ((ECX[0:8] ^ (ECX[0:8] + -0x1)) & (ECX[0:8] ^ 0x1)))[7:8]
+af = ((ECX[0:8] ^ 0x1) ^ (ECX[0:8] + -0x1))[4:5]
 ________________________________________________________________________________
-IRDst 0x10
-zf 0x1
-nf 0x0
-pf 0x1
-of 0x0
-cf 0x0
-af 0x0
-EIP 0x10
-ECX 0x1
-EBX (EBX_init+0x2)
+af                 = 0x0
+EIP                = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+pf                 = 0x1
+IRDst              = ((ECX + 0x4)[0:8] + 0xFF)?(0xB,0x10)
+zf                 = 0x1
+ECX                = 0x1
+of                 = 0x0
+nf                 = 0x0
+cf                 = 0x0
+EBX                = EBX + 0x2
 ________________________________________________________________________________
-IRDst 0x13
-zf 0x1
-nf 0x0
-pf 0x1
-of 0x0
-cf 0x0
-af 0x0
-EIP 0x10
-ECX 0x1
-EBX (EBX_init+0x2)
+Instr JZ         loc_key_1
+Assignblk:
+IRDst = zf?(loc_key_1,loc_key_2)
+EIP = zf?(loc_key_1,loc_key_2)
 ________________________________________________________________________________
-IRDst 0x13
-zf 0x1
-nf 0x0
-pf 0x1
-of 0x0
-cf 0x0
-af 0x0
-EIP 0x10
-EAX (EBX_init+0x2)
-ECX 0x1
-EBX (EBX_init+0x2)
+af                 = 0x0
+EIP                = 0x10
+pf                 = 0x1
+IRDst              = 0x10
+zf                 = 0x1
+ECX                = 0x1
+of                 = 0x0
+nf                 = 0x0
+cf                 = 0x0
+EBX                = EBX + 0x2
 ________________________________________________________________________________
-IRDst @32[ESP_init]
-zf 0x1
-nf 0x0
-pf 0x1
-of 0x0
-cf 0x0
-af 0x0
-EIP @32[ESP_init]
-EAX (EBX_init+0x2)
-ECX 0x1
-EBX (EBX_init+0x2)
-ESP (ESP_init+0x4)
->>> print symbolic_pc
-@32[ESP_init]
->>> sb.dump_id()
-IRDst @32[ESP_init]
-zf 0x1
-nf 0x0
-pf 0x1
-of 0x0
-cf 0x0
-af 0x0
-EIP @32[ESP_init]
-EAX (EBX_init+0x2)
-ECX 0x1
-EBX (EBX_init+0x2)
-ESP (ESP_init+0x4)
+Instr LEA        EBX, DWORD PTR [EBX + 0x1]
+Assignblk:
+EBX = EBX + 0x1
+________________________________________________________________________________
+af                 = 0x0
+EIP                = 0x10
+pf                 = 0x1
+IRDst              = 0x10
+zf                 = 0x1
+ECX                = 0x1
+of                 = 0x0
+nf                 = 0x0
+cf                 = 0x0
+EBX                = EBX + 0x3
+________________________________________________________________________________
+Instr LEA        EBX, DWORD PTR [EBX + 0x1]
+Assignblk:
+IRDst = loc_key_3
+________________________________________________________________________________
+af                 = 0x0
+EIP                = 0x10
+pf                 = 0x1
+IRDst              = 0x13
+zf                 = 0x1
+ECX                = 0x1
+of                 = 0x0
+nf                 = 0x0
+cf                 = 0x0
+EBX                = EBX + 0x3
+________________________________________________________________________________
+Instr MOV        EAX, EBX
+Assignblk:
+EAX = EBX
+________________________________________________________________________________
+af                 = 0x0
+EIP                = 0x10
+pf                 = 0x1
+IRDst              = 0x13
+zf                 = 0x1
+ECX                = 0x1
+of                 = 0x0
+nf                 = 0x0
+cf                 = 0x0
+EBX                = EBX + 0x3
+EAX                = EBX + 0x3
+________________________________________________________________________________
+Instr RET
+Assignblk:
+IRDst = @32[ESP[0:32]]
+ESP = {ESP[0:32] + 0x4 0 32}
+EIP = @32[ESP[0:32]]
+________________________________________________________________________________
+af                 = 0x0
+EIP                = @32[ESP]
+pf                 = 0x1
+IRDst              = @32[ESP]
+zf                 = 0x1
+ECX                = 0x1
+of                 = 0x0
+nf                 = 0x0
+cf                 = 0x0
+EBX                = EBX + 0x3
+ESP                = ESP + 0x4
+EAX                = EBX + 0x3
+________________________________________________________________________________
+>>>
 ```
 
 
diff --git a/example/expression/solve_condition_stp.py b/example/expression/solve_condition_stp.py
index 41b812cd..3c850445 100644
--- a/example/expression/solve_condition_stp.py
+++ b/example/expression/solve_condition_stp.py
@@ -35,7 +35,7 @@ def emul_symb(ir_arch, mdis, states_todo, states_done):
             print 'Known state, skipping', addr
             continue
         states_done.add((addr, symbols, conds))
-        symbexec = SymbolicExecutionEngine(ir_arch, {})
+        symbexec = SymbolicExecutionEngine(ir_arch)
         symbexec.symbols = symbols.copy()
         if ir_arch.pc in symbexec.symbols:
             del symbexec.symbols[ir_arch.pc]
@@ -86,11 +86,10 @@ if __name__ == '__main__':
 
     addr = int(options.address, 16)
 
-    symbols_init = dict(machine.mn.regs.regs_init)
 
     ir_arch = machine.ir(mdis.loc_db)
 
-    symbexec = SymbolicExecutionEngine(ir_arch, symbols_init)
+    symbexec = SymbolicExecutionEngine(ir_arch)
 
     asmcfg, loc_db = parse_asm.parse_txt(machine.mn, 32, '''
     init:
@@ -106,13 +105,27 @@ if __name__ == '__main__':
     ret_addr_lbl = loc_db.get_name_location('ret_addr')
     init_lbl = loc_db.get_name_location('init')
 
-    argc = ExprLoc(argc_lbl, 32)
-    argv = ExprLoc(argv_lbl, 32)
-    ret_addr = ExprLoc(ret_addr_lbl, 32)
+    argc_loc = ExprLoc(argc_lbl, 32)
+    argv_loc = ExprLoc(argv_lbl, 32)
+    ret_addr_loc = ExprLoc(ret_addr_lbl, 32)
+
+
+    ret_addr = ExprId("ret_addr", ret_addr_loc.size)
+
+    fix_args = {
+        argc_loc: ExprId("argc", argc_loc.size),
+        argv_loc: ExprId("argv", argv_loc.size),
+        ret_addr_loc: ret_addr,
+    }
+
 
 
     block = asmcfg.loc_key_to_block(init_lbl)
+    for instr in block.lines:
+        for i, arg in enumerate(instr.args):
+            instr.args[i]= arg.replace_expr(fix_args)
     print block
+
     # add fake address and len to parsed instructions
     ir_arch.add_block(block)
     irb = ir_arch.blocks[init_lbl]
@@ -141,7 +154,7 @@ if __name__ == '__main__':
 
     all_cases = set()
 
-    symbexec = SymbolicExecutionEngine(ir_arch, symbols_init)
+    symbexec = SymbolicExecutionEngine(ir_arch)
     for addr, reqs_cond in all_info:
         out = ['(set-logic QF_ABV)',
                '(set-info :smt-lib-version 2.0)']
diff --git a/example/symbol_exec/single_instr.py b/example/symbol_exec/single_instr.py
index fd454212..6ddd2608 100644
--- a/example/symbol_exec/single_instr.py
+++ b/example/symbol_exec/single_instr.py
@@ -24,7 +24,7 @@ ira = machine.ira(mdis.loc_db)
 ira.add_block(asm_block)
 
 # Instanciate a Symbolic Execution engine with default value for registers
-symb = SymbolicExecutionEngine(ira, {})
+symb = SymbolicExecutionEngine(ira)
 
 # Emulate one IR basic block
 ## Emulation of several basic blocks can be done through .emul_ir_blocks
diff --git a/miasm2/analysis/data_analysis.py b/miasm2/analysis/data_analysis.py
index 0782c12c..aa1c0d1a 100644
--- a/miasm2/analysis/data_analysis.py
+++ b/miasm2/analysis/data_analysis.py
@@ -58,36 +58,6 @@ def intra_block_flow_raw(ir_arch, flow_graph, irb, in_nodes, out_nodes):
                 flow_graph.add_uniq_edge(node_n_r, node_n_w)
 
 
-def intra_block_flow_symbexec(ir_arch, flow_graph, irb, in_nodes, out_nodes):
-    """
-    Create data flow for an irbloc using symbolic execution
-    """
-    current_nodes = {}
-
-    symbols_init = dict(ir_arch.arch.regs.regs_init)
-
-    sb = SymbolicExecutionEngine(ir_arch, dict(symbols_init))
-    sb.emulbloc(irb)
-
-    for n_w in sb.symbols:
-        v = sb.symbols[n_w]
-        if n_w in symbols_init and symbols_init[n_w] == v:
-            continue
-        read_values = v.get_r(cst_read=True)
-        node_n_w = get_node_name(irb.loc_key, len(irb), n_w)
-
-        for n_r in read_values:
-            if n_r in current_nodes:
-                node_n_r = current_nodes[n_r]
-            else:
-                node_n_r = get_node_name(irb.loc_key, 0, n_r)
-                current_nodes[n_r] = node_n_r
-                in_nodes[n_r] = node_n_r
-
-            out_nodes[n_w] = node_n_w
-            flow_graph.add_uniq_edge(node_n_r, node_n_w)
-
-
 def inter_block_flow_link(ir_arch, flow_graph, irb_in_nodes, irb_out_nodes, todo, link_exec_to_data):
     lbl, current_nodes, exec_nodes = todo
     current_nodes = dict(current_nodes)
diff --git a/miasm2/analysis/depgraph.py b/miasm2/analysis/depgraph.py
index f5a2b043..11476f79 100644
--- a/miasm2/analysis/depgraph.py
+++ b/miasm2/analysis/depgraph.py
@@ -281,7 +281,7 @@ class DependencyResult(DependencyState):
         variant.
         """
         # Init
-        ctx_init = self._ira.arch.regs.regs_init
+        ctx_init = {}
         if ctx is not None:
             ctx_init.update(ctx)
         assignblks = []
@@ -352,7 +352,7 @@ class DependencyResultImplicit(DependencyResult):
 
     def emul(self, ctx=None, step=False):
         # Init
-        ctx_init = self._ira.arch.regs.regs_init
+        ctx_init = {}
         if ctx is not None:
             ctx_init.update(ctx)
         solver = z3.Solver()
diff --git a/miasm2/ir/ir.py b/miasm2/ir/ir.py
index 8ee35ed5..73c184dd 100644
--- a/miasm2/ir/ir.py
+++ b/miasm2/ir/ir.py
@@ -539,7 +539,19 @@ class IntermediateRepresentation(object):
         except (ValueError, TypeError):
             return None
 
-        return self.loc_db.get_or_create_offset_location(addr)
+        return self.loc_db.get_offset_location(addr)
+
+
+    def get_or_create_loc_key(self, addr):
+        """Transforms an ExprId/ExprInt/loc_key/int into a loc_key
+        If the offset @addr is not in the LocationDB, create it
+        @addr: an ExprId/ExprInt/loc_key/int"""
+
+        loc_key = self.get_loc_key(addr)
+        if loc_key is not None:
+            return loc_key
+
+        return self.loc_db.add_location(offset=int(addr))
 
     def get_block(self, addr):
         """Returns the irbloc associated to an ExprId/ExprInt/loc_key/int
diff --git a/miasm2/ir/symbexec.py b/miasm2/ir/symbexec.py
index 288a46e4..d137e71f 100644
--- a/miasm2/ir/symbexec.py
+++ b/miasm2/ir/symbexec.py
@@ -17,14 +17,14 @@ log.setLevel(logging.INFO)
 
 def get_block(ir_arch, mdis, addr):
     """Get IRBlock at address @addr"""
-    lbl = ir_arch.get_loc_key(addr)
-    if not lbl in ir_arch.blocks:
-        offset = mdis.loc_db.get_location_offset(lbl)
+    loc_key = ir_arch.get_or_create_loc_key(addr)
+    if loc_key not in ir_arch.blocks:
+        offset = mdis.loc_db.get_location_offset(loc_key)
         block = mdis.dis_block(offset)
         ir_arch.add_block(block)
-    irblock = ir_arch.get_block(lbl)
+    irblock = ir_arch.get_block(loc_key)
     if irblock is None:
-        raise LookupError('No block found at that address: %s' % lbl)
+        raise LookupError('No block found at that address: %s' % ir_arch.loc_db.pretty_str(loc_key))
     return irblock
 
 
@@ -805,7 +805,7 @@ class SymbolicExecutionEngine(object):
 
     StateEngine = SymbolicState
 
-    def __init__(self, ir_arch, state,
+    def __init__(self, ir_arch, state=None,
                  func_read=None,
                  func_write=None,
                  sb_expr_simp=expr_simp):
@@ -821,6 +821,9 @@ class SymbolicExecutionEngine(object):
             ExprCompose: self.eval_exprcompose,
         }
 
+        if state is None:
+            state = {}
+
         self.symbols = SymbolMngr(addrsize=ir_arch.addrsize, expr_simp=expr_simp)
 
         for dst, src in state.iteritems():
@@ -961,7 +964,7 @@ class SymbolicExecutionEngine(object):
         @mems: track mems only
         """
         if init_state is None:
-            init_state = self.ir_arch.arch.regs.regs_init
+            init_state = {}
         if ids:
             for variable, value in self.symbols.symbols_id.iteritems():
                 if variable in init_state and init_state[variable] == value:
diff --git a/test/analysis/dg_test_02_implicit_expected.json b/test/analysis/dg_test_02_implicit_expected.json
index 9394f01d..cfcf7258 100644
--- a/test/analysis/dg_test_02_implicit_expected.json
+++ b/test/analysis/dg_test_02_implicit_expected.json
@@ -1 +1 @@
-[{"has_loop": false, "EAX": "0x4", "satisfiability": true, "constraints": {"zf_init": "0x1"}}, {"has_loop": false, "EAX": "0x3", "satisfiability": true, "constraints": {"zf_init": "0x0"}}]
+[{"has_loop": false, "EAX": "0x4", "satisfiability": true, "constraints": {"zf": "0x1"}}, {"has_loop": false, "EAX": "0x3", "satisfiability": true, "constraints": {"zf": "0x0"}}]
diff --git a/test/analysis/dg_test_04_expected.json b/test/analysis/dg_test_04_expected.json
index fb115835..24687e4a 100644
--- a/test/analysis/dg_test_04_expected.json
+++ b/test/analysis/dg_test_04_expected.json
@@ -1 +1 @@
-[{"EAX": "EBX_init", "has_loop": false}]
+[{"EAX": "EBX", "has_loop": false}]
diff --git a/test/analysis/dg_test_04_implicit_expected.json b/test/analysis/dg_test_04_implicit_expected.json
index 73e7209e..21dbfc96 100644
--- a/test/analysis/dg_test_04_implicit_expected.json
+++ b/test/analysis/dg_test_04_implicit_expected.json
@@ -1 +1 @@
-[{"has_loop": false, "EAX": "EBX_init", "satisfiability": true, "constraints": {}}, {"has_loop": true, "EAX": "EBX_init", "satisfiability": false, "constraints": {}}]
+[{"has_loop": false, "EAX": "EBX", "satisfiability": true, "constraints": {}}, {"has_loop": true, "EAX": "EBX", "satisfiability": false, "constraints": {}}]
diff --git a/test/analysis/dg_test_06_implicit_expected.json b/test/analysis/dg_test_06_implicit_expected.json
index bda75296..be4e9afb 100644
--- a/test/analysis/dg_test_06_implicit_expected.json
+++ b/test/analysis/dg_test_06_implicit_expected.json
@@ -1 +1 @@
-[{"has_loop": false, "EAX": "0x1", "satisfiability": true, "constraints": {"EAX_init": "0xffffffff"}}, {"has_loop": false, "EAX": "0x2", "satisfiability": false, "constraints": {}}]
+[{"has_loop": false, "EAX": "0x1", "satisfiability": true, "constraints": {"EAX": "0xffffffff"}}, {"has_loop": false, "EAX": "0x2", "satisfiability": false, "constraints": {}}]
diff --git a/test/analysis/dg_test_10_implicit_expected.json b/test/analysis/dg_test_10_implicit_expected.json
index 05b34918..36a84788 100644
--- a/test/analysis/dg_test_10_implicit_expected.json
+++ b/test/analysis/dg_test_10_implicit_expected.json
@@ -1 +1 @@
-[{"has_loop": false, "EAX": "0x1", "EBX": "0x3", "satisfiability": true, "constraints": {"zf_init": "0x0"}}, {"has_loop": false, "EAX": "0x2", "EBX": "0x3", "satisfiability": false, "constraints": {}}, {"has_loop": false, "EAX": "0x1", "EBX": "0x4", "satisfiability": false, "constraints": {}}, {"has_loop": false, "EAX": "0x2", "EBX": "0x4", "satisfiability": true, "constraints": {"zf_init": "0x1"}}]
+[{"has_loop": false, "EAX": "0x1", "EBX": "0x3", "satisfiability": true, "constraints": {"zf": "0x0"}}, {"has_loop": false, "EAX": "0x2", "EBX": "0x3", "satisfiability": false, "constraints": {}}, {"has_loop": false, "EAX": "0x1", "EBX": "0x4", "satisfiability": false, "constraints": {}}, {"has_loop": false, "EAX": "0x2", "EBX": "0x4", "satisfiability": true, "constraints": {"zf": "0x1"}}]
diff --git a/test/arch/arm/sem.py b/test/arch/arm/sem.py
index 252e5954..57dd2b77 100755
--- a/test/arch/arm/sem.py
+++ b/test/arch/arm/sem.py
@@ -24,7 +24,7 @@ def M(addr):
 def compute(asm, inputstate={}, debug=False):
     sympool = dict(regs_init)
     sympool.update({k: ExprInt(v, k.size) for k, v in inputstate.iteritems()})
-    interm = ir_arch()
+    interm = ir_arch(loc_db)
     symexec = SymbolicExecutionEngine(interm, sympool)
     instr = mn.fromstring(asm, loc_db, "l")
     code = mn.asm(instr)[0]
diff --git a/test/ir/symbexec.py b/test/ir/symbexec.py
index 7d5bf44a..d57bcba0 100755
--- a/test/ir/symbexec.py
+++ b/test/ir/symbexec.py
@@ -222,7 +222,7 @@ class TestSymbExec(unittest.TestCase):
         assert found
 
 
-        sb_empty = SymbolicExecutionEngine(ir_x86_32(), {})
+        sb_empty = SymbolicExecutionEngine(ir_x86_32())
         sb_empty.dump()
 
 
@@ -231,7 +231,7 @@ class TestSymbExec(unittest.TestCase):
         arch_addr8 = ir_x86_32()
         # Hack to obtain tiny address space
         arch_addr8.addrsize = 5
-        sb_addr8 = SymbolicExecutionEngine(arch_addr8, {})
+        sb_addr8 = SymbolicExecutionEngine(arch_addr8)
         sb_addr8.dump()
         # Fulfill memory
         sb_addr8.apply_change(ExprMem(ExprInt(0, 5), 256), ExprInt(0, 256))