angr / claripy

An abstraction layer for constraint solvers.
BSD 2-Clause "Simplified" License
273 stars 90 forks source link

Memory read tracking and BV comparions #395

Closed Voxanimus closed 2 months ago

Voxanimus commented 2 months ago

Question

I am currently using SimInspector to track some memory read during symbolic executions. I have something like this:

    def _breakpoint(self, state: SimState) -> None:
        self.studied_fetches.append(state.inspect.mem_read_address)

    def _install_breakpoint(self, state: SimState, address: int) -> None:
        state.inspect.b(
            "mem_read",
            when=BP_AFTER,
            instruction=address + 1,
            action=self._breakpoint,
        )

Later in my code I am checking if memory location are the same by compring the content of studied_fetches. I won't go into detailed but by construction len(studied_fetches) is always equal to 2 and the address are always BVV. Exemple: image

I am comparing the address like this :


    def is_same_memory_location(self) -> bool:
        """Check if the two studied fetches are the same

        Returns:
            bool: True if the two studied fetches are the same, False otherwise
        """

        if self.studied_fetches[0].symbolic or self.studied_fetches[1].symbolic:
            raise ValueError("One of the fetches is symbolic")
        result: bool = self.studied_fetches[0] == self.studied_fetches[1]

        # clear fetches
        self.studied_fetches = []

        return result
```nd I 

And I always get the same error: `claripy.errors.ClaripyOperationError: testing Expressions for truthiness does not do what you want, as these expressions can be symbolic` but the values compared are never supposed to be symbolic.

If anyone have a suggestion.