(* Phase 3: Generate constraint system and solve it *) (* A function that generates a conjoined, quantifier-eliminated constraint of the form \forall i. i < len32 => mem[fakeaddr32+i] = (whatever happens to be in memory at location realaddr32+i) *) let memory_to_predicate realaddr32 fakeaddr32 len32 memvar = let rec aux pred i32 = if i32 = len32 then pred else let pred = IRUtil.mk_and pred (IRUtil.mk_eq (IR.Load(memvar,IRUtil.mk_dword (Int64.of_int32 (Int32.add fakeaddr32 i32)),IR.TypeReg_8)) (IRUtil.mk_byte (Int64.of_int32 (IDA.get_byte (Int32.add realaddr32 i32))))) in aux pred (Int32.succ i32) in aux IRUtil.mk_true 0l;; let ssa_memvar = IRUtil.mk_evar (Hashtbl.find tbl X86ToIRUtil.vMem);; (* The postcondition says that ... *) let pc = IRUtil.mk_and (IRUtil.mk_and (* At the beginning of the trace, ESI = 0x00 and EDI = 0x20 *) (IRUtil.mk_eq X86ToIRUtil.eEsi (IRUtil.mk_dword 0x00L)) (IRUtil.mk_eq X86ToIRUtil.eEdi (IRUtil.mk_dword 0x20L))) (IRUtil.mk_and (* At the beginning of the trace, the activation array contains whatever we happen to have in memory at that location *) (memory_to_predicate 0x004093A8l 0x00l 32l X86ToIRUtil.eMem) (* At the end of the trace, the output array contains the hard-coded value found in the crackme *) (memory_to_predicate 0x00409185l 0x20l 32l ssa_memvar)) in let ctx = Z3.mk_context_x [|("MODEL", "true");("SOFT_TIMEOUT", "1000000")|] in let before = Sys.time () in let model = Z3SymbolicExecute.symbolic_execute ctx ir_ssa pc in let after = Sys.time () in let total = after -. before in IDA.msg "%f: %s\n" total model;;