admin/cea-sec-miasm
1
0
Fork 0
mirror of https://github.com/cea-sec/miasm synced 2026-06-21 13:48:18 +00:00
Code Issues Packages Projects Releases Wiki Activity

IR: remove default regs_init for symbexec

Browse Source
This commit is contained in:
Fabrice Desclaux
2018-07-05 13:16:45 +02:00
parent 143196e691
commit 1d8dc96d6c
13 changed files with 247 additions and 150 deletions
Download Patch File Download Diff File Expand all files Collapse all files
README.md
+193 -124
View File
@@ -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
________________________________________________________________________________
>>>
```
example/expression/solve_condition_stp.py
+20 -7
View File
@@ -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)']
example/symbol_exec/single_instr.py
+1 -1
View File
@@ -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
miasm2/analysis/depgraph.py
+2 -2
View File
@@ -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()
miasm2/ir/ir.py
+13 -1
View File
@@ -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
miasm2/ir/symbexec.py
+10 -7
View File
@@ -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:
test/analysis/dg_test_02_implicit_expected.json
+1 -1
View File
@@ -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"}}]
test/analysis/dg_test_04_expected.json
+1 -1
View File
@@ -1 +1 @@
[{"EAX": "EBX_init", "has_loop": false}]
[{"EAX": "EBX", "has_loop": false}]
test/analysis/dg_test_04_implicit_expected.json
+1 -1
View File
@@ -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": {}}]
test/analysis/dg_test_06_implicit_expected.json
+1 -1
View File
@@ -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": {}}]
test/analysis/dg_test_10_implicit_expected.json
+1 -1
View File
@@ -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"}}]
test/arch/arm/sem.py
+1 -1
View File
@@ -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]
test/ir/symbexec.py
+2 -2
View File
@@ -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))