diff options
Diffstat (limited to 'example/expression/solve_condition_stp.py')
| -rw-r--r-- | example/expression/solve_condition_stp.py | 73 |
1 files changed, 41 insertions, 32 deletions
diff --git a/example/expression/solve_condition_stp.py b/example/expression/solve_condition_stp.py index 201d9f26..acb3abf4 100644 --- a/example/expression/solve_condition_stp.py +++ b/example/expression/solve_condition_stp.py @@ -5,16 +5,14 @@ from pdb import pm from miasm2.analysis.machine import Machine from miasm2.expression.expression import ExprInt, ExprCond, ExprId, \ - get_expr_ids, ExprAff + get_expr_ids, ExprAff, ExprLoc from miasm2.core.bin_stream import bin_stream_str -from miasm2.core import asmblock from miasm2.ir.symbexec import SymbolicExecutionEngine, get_block from miasm2.expression.simplifications import expr_simp from miasm2.core import parse_asm from miasm2.arch.x86.disasm import dis_x86_32 as dis_engine from miasm2.ir.translators.translator import Translator - machine = Machine("x86_32") @@ -28,7 +26,7 @@ if not args: sys.exit(0) -def emul_symb(ir_arch, mdis, states_todo, states_done): +def emul_symb(ir_arch, ircfg, mdis, states_todo, states_done): while states_todo: addr, symbols, conds = states_todo.pop() print '*' * 40, "addr", addr, '*' * 40 @@ -36,11 +34,11 @@ 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] - irblock = get_block(ir_arch, mdis, addr) + irblock = get_block(ir_arch, ircfg, mdis, addr) print 'Run block:' print irblock @@ -55,8 +53,8 @@ def emul_symb(ir_arch, mdis, states_todo, states_done): cond_group_b = {addr.cond: ExprInt(1, addr.cond.size)} addr_a = expr_simp(symbexec.eval_expr(addr.replace_expr(cond_group_a), {})) addr_b = expr_simp(symbexec.eval_expr(addr.replace_expr(cond_group_b), {})) - if not (addr_a.is_int() or asmblock.expr_is_label(addr_a) and - addr_b.is_int() or asmblock.expr_is_label(addr_b)): + if not (addr_a.is_int() or addr_a.is_loc() and + addr_b.is_int() or addr_b.is_loc()): print str(addr_a), str(addr_b) raise ValueError("Unsupported condition") if isinstance(addr_a, ExprInt): @@ -68,11 +66,10 @@ def emul_symb(ir_arch, mdis, states_todo, states_done): elif addr == ret_addr: print 'Return address reached' continue - elif isinstance(addr, ExprInt): + elif addr.is_int(): addr = int(addr.arg) states_todo.add((addr, symbexec.symbols.copy(), tuple(conds))) - elif asmblock.expr_is_label(addr): - addr = addr.name + elif addr.is_loc(): states_todo.add((addr, symbexec.symbols.copy(), tuple(conds))) else: raise ValueError("Unsupported destination") @@ -88,39 +85,51 @@ if __name__ == '__main__': addr = int(options.address, 16) - symbols_init = dict(machine.mn.regs.regs_init) - - ir_arch = machine.ir(mdis.symbol_pool) - symbexec = SymbolicExecutionEngine(ir_arch, symbols_init) + ir_arch = machine.ir(mdis.loc_db) + ircfg = ir_arch.new_ircfg() + symbexec = SymbolicExecutionEngine(ir_arch) - blocks, symbol_pool = parse_asm.parse_txt(machine.mn, 32, ''' + asmcfg, loc_db = parse_asm.parse_txt(machine.mn, 32, ''' + init: PUSH argv PUSH argc PUSH ret_addr ''', - symbol_pool=mdis.symbol_pool) + loc_db=mdis.loc_db) + + + argc_lbl = loc_db.get_name_location('argc') + argv_lbl = loc_db.get_name_location('argv') + ret_addr_lbl = loc_db.get_name_location('ret_addr') + init_lbl = loc_db.get_name_location('init') + argc_loc = ExprLoc(argc_lbl, 32) + argv_loc = ExprLoc(argv_lbl, 32) + ret_addr_loc = ExprLoc(ret_addr_lbl, 32) - argc_lbl = symbol_pool.getby_name('argc') - argv_lbl = symbol_pool.getby_name('argv') - ret_addr_lbl = symbol_pool.getby_name('ret_addr') - argc = ExprId(argc_lbl, 32) - argv = ExprId(argv_lbl, 32) - ret_addr = ExprId(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 - b = list(blocks)[0] - print b # add fake address and len to parsed instructions - for i, line in enumerate(b.lines): - line.offset, line.l = i, 1 - ir_arch.add_block(b) - irb = get_block(ir_arch, mdis, 0) + ir_arch.add_asmblock_to_ircfg(block, ircfg) + irb = ircfg.blocks[init_lbl] symbexec.eval_updt_irblock(irb) symbexec.dump(ids=False) - # reset ir_arch blocks ir_arch.blocks = {} @@ -129,7 +138,7 @@ if __name__ == '__main__': states_todo.add((addr, symbexec.symbols, ())) # emul blocks, propagate states - emul_symb(ir_arch, mdis, states_todo, states_done) + emul_symb(ir_arch, ircfg, mdis, states_todo, states_done) all_info = [] @@ -144,7 +153,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)'] |