soundtools.py

>>> import freki, z3; lift = freki.lift_instruction_at(bv,here); slv = z3.Solver(); lift.constrain(slv); lift
<module 'i8051.freki' from 'C:\Users\amtal\AppData\Roaming\Binary Ninja\plugins\i8051\freki.pyc'>
<Z3Lifter expr:1 constr:0 ssa_vars:['A']>
>>> slv
[Implies(0@0xc777,
         A#53 ==
         Concat(Extract(3, 0, A#52), Extract(7, 4, A#52)))]
>>> lift2 = freki.lift_function(current_function); lift2.constrain(slv); lift2
<Z3Lifter expr:5 constr:2 ssa_vars:['mem', 'rsp', 'rdi', 'rax']>
>>> SFR = lift2.ssa_vars['rax'][1]
>>> slv.push()
>>> SFR = lift2.ssa_vars['rax'][1]
>>> slv.assert_and_track(z3.And(lift.ssa_vars['A'][52] == lift2.ssa_vars['mem'][0][SFR+0x60], lift.ssa_vars['A'][53] != lift2.ssa_vars['mem'][1][SFR+0x60]), 'not-equivalent')
>>> slv.check()
unsat
>>> slv.unsat_core()  # <== !!working!!
[c0, 0@0xc777, not-equivalent]
>>> slv
[Implies(0@0xc777,
         A#53 ==
         Concat(Extract(3, 0, A#52), Extract(7, 4, A#52))),
 Implies(0@0xa737, rax#2 == 0),
 Implies(0@0xa72f,
         rax#1 ==
         Concat(mem#0[55 + rdi#0],
                mem#0[54 + rdi#0],
                mem#0[53 + rdi#0],
                mem#0[52 + rdi#0],
                mem#0[51 + rdi#0],
                mem#0[50 + rdi#0],
                mem#0[49 + rdi#0],
                mem#0[48 + rdi#0])),
 Implies(c0,
         mem#1 ==
         Store(mem#0,
               96 + rax#1,
               Concat(Extract(3, 0, mem#0[96 + rax#1]),
                      Extract(7, 4, mem#0[96 + rax#1])))),
 Implies(c1,
         mem#2 ==
         Store(Store(Store(Store(mem#1,
                                 59 + rdi#0,
                                 1 + mem#1[56 + rdi#0]),
                           58 + rdi#0,
                           Extract(15,
                                   8,
                                   1 +
                                   Concat(mem#1[59 + rdi#0],
                                        mem#1[58 + rdi#0],
                                        mem#1[57 + rdi#0],
                                        mem#1[56 + rdi#0]))),
                     57 + rdi#0,
                     Extract(23,
                             16,
                             1 +
                             Concat(mem#1[59 + rdi#0],
                                    mem#1[58 + rdi#0],
                                    mem#1[57 + rdi#0],
                                    mem#1[56 + rdi#0]))),
               56 + rdi#0,
               Extract(31,
                       24,
                       1 +
                       Concat(mem#1[59 + rdi#0],
                              mem#1[58 + rdi#0],
                              mem#1[57 + rdi#0],
                              mem#1[56 + rdi#0])))),
 Implies(not-equivalent,
         And(A#52 == mem#0[rax#1 + 96],
             A#53 != mem#1[rax#1 + 96]))]