Pointer operations are subtly wrong in the presence of global pointers

[RyanGlScott]

Most of the ptrOp-based operations attempt to classify whether pointer arguments are actually bitvectors (i.e., they have a block value of 0) or not (i.e., their block value is non-0). However, this is fragile in the presence of global pointers, which are represented by some bitvector offset into the global address space. These offsets looks like bitvectors (i.e., they have block 0) in isolation, so some parts of macaw-symbolic attempt to resolve these to proper pointers (with non-0 block values) using mapRegionPointers. The main place where this is used is in the execMacawStmtExtension cases for Macaw{Cond}ReadMem and Macaw{Cond}WriteMem, which is what powers much of the macaw-symbolic memory model.

However, not everything in execMacawStmtExtension uses mapRegionPointers. In particular, none of PtrEq and friends use it. This can become an issue if, say, PtrEq is used to compare pointers with different block numbers, which will result in an undefined, symbolic result. It might be the case that one of the arguments is a global pointer with a block value of 0, and running it through mapRegionPointers would produce a pointer with the same block value as the other pointer passed to PtrEq. This isn't just a hypothetical scenario, as we encountered an issue much like this one in an upstream project, and tweaking the PtrEq case to use mapRegionPointers resolved the issue.

If PtrEq should use mapRegionPointers, then should all of the other Ptr* cases in execMacawStmtExtension? That isn't as obvious. I attempted to do this in the aforementioned upstream project, but that actually resulted in several new failing proof goals being generated in the project's test suite when the PtrAnd, PtrXor, or PtrMux cases were altered. I'm not quite sure why this is yet, but this suggests that things may be a bit more delicate than a first glance would suggest.

One option would be to only change the PtrEq case (which doesn't change the project's test suite at all), but it feels somewhat inconsistent to only change one of the Ptr* cases and not the other. We should investigate this further.