(self, sl, sr)
return True
Compares two states for similarity.
Compares two states for similarity.
Compares two states for similarity .
def compare_states(self, sl, sr):
        """
        Compares two states for similarity.
        """
        joint_solver = claripy.Solver()

        # make sure the canonicalized constraints are the same
        n_map, n_counter, n_canon_constraint = claripy.And(*sr.solver.constraints).canonicalize() #pylint:disable=no-member
        u_map, u_counter, u_canon_constraint = claripy.And(*sl.solver.constraints).canonicalize() #pylint:disable=no-member
        if n_canon_constraint is not u_canon_constraint:
            # https://github.com/Z3Prover/z3/issues/2359
            # don't try to simplify unless we really need to, as it can introduce serious nondeterminism
            n_canoner_constraint = sr.solver.simplify(n_canon_constraint)
            u_canoner_constraint = sl.solver.simplify(u_canon_constraint)
        else:
            n_canoner_constraint = u_canoner_constraint = n_canon_constraint
        joint_solver.add((n_canoner_constraint, u_canoner_constraint))
        if n_canoner_constraint is not u_canoner_constraint:
            # extra check: are these two constraints equivalent?
            tmp_solver = claripy.Solver()
            a = tmp_solver.satisfiable(extra_constraints=(n_canoner_constraint == u_canoner_constraint,))
            b = tmp_solver.satisfiable(extra_constraints=(n_canoner_constraint != u_canoner_constraint,))

            if not (a is True and b is False):
                self._report_incongruency("Different constraints!")
                return False

        # get the differences in registers and memory
        mem_diff = sr.memory.changed_bytes(sl.memory)
        reg_diff = sr.registers.changed_bytes(sl.registers)

        # this is only for unicorn
        if "UNICORN" in sl.options or "UNICORN" in sr.options:
            if sl.arch.name == "X86":
                reg_diff -= set(range(40, 52)) #ignore cc psuedoregisters
                reg_diff -= set(range(320, 324)) #some other VEX weirdness
                reg_diff -= set(range(340, 344)) #ip_at_syscall
            elif sl.arch.name == "AMD64":
                reg_diff -= set(range(144, 168)) #ignore cc psuedoregisters

        # make sure the differences in registers and memory are actually just renamed
        # versions of the same ASTs
        for diffs,(um,nm) in (
            (reg_diff, (sl.registers, sr.registers)),
            (mem_diff, (sl.memory, sr.memory)),
        ):
            for i in diffs:
                bn = nm.load(i, 1)
                bu = um.load(i, 1)

                bnc = bn.canonicalize(var_map=n_map, counter=n_counter)[-1]
                buc = bu.canonicalize(var_map=u_map, counter=u_counter)[-1]

                if bnc is not buc:
                    self._report_incongruency("Different memory or registers (index %d, values %r and %r)!", i, bn, bu)
                    return False

        # make sure the flags are the same
        if sl.arch.name in ("AMD64", "X86", "ARM", "ARMEL", "ARMHF", "AARCH64"):
            # pylint: disable=unused-variable
            n_bkp = sr.regs.cc_op, sr.regs.cc_dep1, sr.regs.cc_dep2, sr.regs.cc_ndep
            u_bkp = sl.regs.cc_op, sl.regs.cc_dep1, sl.regs.cc_dep2, sl.regs.cc_ndep
            if sl.arch.name in ('AMD64', 'X86'):
                n_flags = sr.regs.eflags.canonicalize(var_map=n_map, counter=n_counter)[-1]
                u_flags = sl.regs.eflags.canonicalize(var_map=u_map, counter=u_counter)[-1]
            else:
                n_flags = sr.regs.flags.canonicalize(var_map=n_map, counter=n_counter)[-1]
                u_flags = sl.regs.flags.canonicalize(var_map=u_map, counter=u_counter)[-1]
            if n_flags is not u_flags and sl.solver.simplify(n_flags) is not sr.solver.simplify(u_flags):
                self._report_incongruency("Different flags!")
                return False

        return True
def compare_states ( self , sl , sr ) : joint_solver = claripy . Solver ( ) # make sure the canonicalized constraints are the same n_map , n_counter , n_canon_constraint = claripy . And ( * sr . solver . constraints ) . canonicalize ( ) #pylint:disable=no-member u_map , u_counter , u_canon_constraint = claripy . And ( * sl . solver . constraints ) . canonicalize ( ) #pylint:disable=no-member if n_canon_constraint is not u_canon_constraint : # https://github.com/Z3Prover/z3/issues/2359 # don't try to simplify unless we really need to, as it can introduce serious nondeterminism n_canoner_constraint = sr . solver . simplify ( n_canon_constraint ) u_canoner_constraint = sl . solver . simplify ( u_canon_constraint ) else : n_canoner_constraint = u_canoner_constraint = n_canon_constraint joint_solver . add ( ( n_canoner_constraint , u_canoner_constraint ) ) if n_canoner_constraint is not u_canoner_constraint : # extra check: are these two constraints equivalent? tmp_solver = claripy . Solver ( ) a = tmp_solver . satisfiable ( extra_constraints = ( n_canoner_constraint == u_canoner_constraint , ) ) b = tmp_solver . satisfiable ( extra_constraints = ( n_canoner_constraint != u_canoner_constraint , ) ) if not ( a is True and b is False ) : self . _report_incongruency ( "Different constraints!" ) return False # get the differences in registers and memory mem_diff = sr . memory . changed_bytes ( sl . memory ) reg_diff = sr . registers . changed_bytes ( sl . registers ) # this is only for unicorn if "UNICORN" in sl . options or "UNICORN" in sr . options : if sl . arch . name == "X86" : reg_diff -= set ( range ( 40 , 52 ) ) #ignore cc psuedoregisters reg_diff -= set ( range ( 320 , 324 ) ) #some other VEX weirdness reg_diff -= set ( range ( 340 , 344 ) ) #ip_at_syscall elif sl . arch . name == "AMD64" : reg_diff -= set ( range ( 144 , 168 ) ) #ignore cc psuedoregisters # make sure the differences in registers and memory are actually just renamed # versions of the same ASTs for diffs , ( um , nm ) in ( ( reg_diff , ( sl . registers , sr . registers ) ) , ( mem_diff , ( sl . memory , sr . memory ) ) , ) : for i in diffs : bn = nm . load ( i , 1 ) bu = um . load ( i , 1 ) bnc = bn . canonicalize ( var_map = n_map , counter = n_counter ) [ - 1 ] buc = bu . canonicalize ( var_map = u_map , counter = u_counter ) [ - 1 ] if bnc is not buc : self . _report_incongruency ( "Different memory or registers (index %d, values %r and %r)!" , i , bn , bu ) return False # make sure the flags are the same if sl . arch . name in ( "AMD64" , "X86" , "ARM" , "ARMEL" , "ARMHF" , "AARCH64" ) : # pylint: disable=unused-variable n_bkp = sr . regs . cc_op , sr . regs . cc_dep1 , sr . regs . cc_dep2 , sr . regs . cc_ndep u_bkp = sl . regs . cc_op , sl . regs . cc_dep1 , sl . regs . cc_dep2 , sl . regs . cc_ndep if sl . arch . name in ( 'AMD64' , 'X86' ) : n_flags = sr . regs . eflags . canonicalize ( var_map = n_map , counter = n_counter ) [ - 1 ] u_flags = sl . regs . eflags . canonicalize ( var_map = u_map , counter = u_counter ) [ - 1 ] else : n_flags = sr . regs . flags . canonicalize ( var_map = n_map , counter = n_counter ) [ - 1 ] u_flags = sl . regs . flags . canonicalize ( var_map = u_map , counter = u_counter ) [ - 1 ] if n_flags is not u_flags and sl . solver . simplify ( n_flags ) is not sr . solver . simplify ( u_flags ) : self . _report_incongruency ( "Different flags!" ) return False return True