PartialSymbolicAnalysis + MemoryCellList = multiple values stored at the same memory location
markasoftware opened this issue · 3 comments
I frequently encounter situations like this:
The root of the problem seems to be that reading (and writing) memory causes MemoryCellList to try and find the set of other cells overlapping that memory location, but the relatively complicated sequence of instructions involved in finding overlapping cells is too much for the PartialSymbolicAnalysis, causing the symbolic values to revert to newly created abstract identifiers, in turn causing the MemoryCellList to not find anything that must alias the requested address, and instead insert a new cell with protoval.
Perhaps a solution is to first check if the addresses are mustEqual before trying to do the more complicated overlap checking when memory is read and written?
(Should be noted that MemoryCellList is the recommended MemoryState for PartialSymbolicAnalysis)
Id just like to confirm nobody is working on this, in which case ill try to take a stab at it myself. Dont want to duplicate work
Nobody is working on this yet. If you want to provide a small example that calls some PartialSymbolicSemantics::RiscOperators methods to demonstrate this, I can at least verify that it's a bug before you spend too much time on it.
After thinking more, I've determined this isn't a bug -- in fact, it's usually not possible to determine unambiguously that two partial symbolic values certainly don't alias, because any two svalues with different names might plausibly alias.
While Rose's existing behavior is mostly correct, it's possible to do a little better. For example, if two partial symbolic values have the same name but the values/offsets are sufficiently different, they certainly don't alias. Similarly, if two partial symbolic values have the same name and offset, they must alias. However, because of the overall coarseness of partial symbolic, I'm not sure these changes would really make Rose more useful for anyone.
In my application, some unsoundness is okay, so I'm just using a Rose fork where I modify the MemoryCell logic to assume that partial symbolic svalues don't alias unless they must alias, which is obviously unsuitable in upstream Rose.