Commit 74b6d4e8 authored by Marek Chalupa's avatar Marek Chalupa
Browse files

bse: fix running paths from the middle 

There it can happen, that we do not match all inputs
and we fail on assertions.
parent 72a097de

slowbeast/bse/bsestate.py

+16 −10
Original line number Original line Diff line number Diff line
@@ -117,22 +117,28 @@ class BSEState(LazySEState): 
        Add constraints from matching input reads of zeroed globals.

        Add constraints from matching input reads of zeroed globals.

        """

        """

        M, em = self.memory, self.expr_manager()

        M, em = self.memory, self.expr_manager()

        R, get_obj = M._input_reads, initstate.memory.get_obj

        IM = initstate.memory

        R, get_obj = M._input_reads, IM.get_obj

        constraints = []

        constraints = []

        # FIXME: we target globals, but we could in fact just try reading from initstate

        # FIXME: we target globals, but we could in fact just try reading from initstate

        # to get, e.g., values of bytes from objects.

        # to get, e.g., values of bytes from objects.

        # However, the problem is that symbolic offsets are not supported, so...

        # However, the problem is that symbolic offsets are not supported, so...

        for ptr, val in R.items():

        for ptr, val in R.items():

            obj = ptr.object()

            obj = ptr.object()

            assert obj.is_concrete(), "Initial state has symbolic object"

            # this can happen if we execute a path that does not contain all information

            if not obj.is_concrete():

            # to match all inputs. It is not a bug.

                continue

            # assert obj.is_concrete(), f"Initial state has symbolic object:\n{self}"

            if obj.is_concrete():

                mo = get_obj(obj)

                mo = get_obj(obj)

                if mo is None:

                if mo is None:

                    continue

                    continue

                # we found zeroed global from which we read

                # we found zeroed global from which we read

                if mo.is_global() and mo.is_zeroed():

                if mo.is_global() and mo.is_zeroed():

                    constraints.append(em.Eq(val[0], ConcreteInt(0, val[0].bitwidth())))

                    constraints.append(em.Eq(val[0], ConcreteInt(0, val[0].bitwidth())))

            else:

                for g, ptr in ((g, ptr) for (g, ptr) in IM.bound_globals() if g.is_zeroed()):

                    constraints.append(em.Or(em.Ne(obj, ptr.object()),

                                             em.Eq(val[0], ConcreteInt(0, val[0].bitwidth()))))

        return constraints

        return constraints





    def _memory_constraints(self):

    def _memory_constraints(self):

slowbeast/core/memory.py

+4 −0
Original line number Original line Diff line number Diff line
@@ -188,6 +188,10 @@ class Memory: 
            ret = self._cs.get(v)

            ret = self._cs.get(v)

        return ret

        return ret





    def bound_globals(self):

        """ Return the bound globals in this state """

        return self._glob_bindings.items()



    def globals_list(self):

    def globals_list(self):

        """ Return the list of globals in this state """

        """ Return the list of globals in this state """

        # return only list, so that we must get them through "get"

        # return only list, so that we must get them through "get"