Invalidate memory properly with laxLoadsAndStores

[RyanGlScott]

Prior to this change, invalidated memory would always result in an error when read from. This isn't quite the semantics that we would want when laxLoadsAndStores is enabled, however, since reading should always result in a symbolic value of some sort. This patch changes the mechanics of doInvalidate and readMemInvalidate such that when laxLoadsAndStores is enabled, the memory is given the appropriate semantics depending on whether indeterminateLoadBehavior is StableSymbolic or UnstableSymbolic.

This adds a ?memOpts :: MemOptions constraint to doInvalidate, which is a breaking API change. That being said, the only call site that I am aware of for the doInvalidate function is SAW, so the breakage should be relatively minor. Furthermore, there were no test cases for doInvalidate before this, so this patch adds some.

[RyanGlScott]

I've marked this as a draft for now since I'd like to test this more in SAW (the intended use case) before I land it. Feedback is very much welcome in the meantime.

[robdockins]

Sadly, this is too easy to be correct, I think. I think this has to be pushed down into the InRange cases of the subFn functions below, which implement the case that the requested read actually overlaps with the invalidation in question.

[RyanGlScott]

Darn. I'm a bit alarmed that this causes the test case that I wrote for UnstableSymbolic to pass, and moreover, it seems to do what I'd expect on the SAW side. Perhaps I'm not tickling the right code paths. In any case, I'll look into pushing this logic down lower.

[robdockins]

I think the logic you have here will work correctly iff you invalidate all the memory in an allocation. Otherwise, you actually have to check to what degree the requested read overlaps with the invalidation write, which is what the more complicated logic in the body does.

[RyanGlScott]

Gotcha. Let me know if you'd prefer the test case to distinguish between these two cases of readMemInvalidate, but I'm pretty confident that the changes I've just pushed should do the right thing now.

[RyanGlScott]

I've had the chance to test this on SAW, and everything works pretty well in the UnstableSymbolic case. Things aren't quite working yet in the StableSymbolic case, however:

[21:26:38.432] Stack trace:
"llvm_verify" (/home/rscott/Documents/Hacking/Haskell/saw-script/intTests/test_bitfield_basic/test.saw:21:1-21:12):
"z3" (/home/rscott/Documents/Hacking/Haskell/saw-script/intTests/test_bitfield_basic/test.saw:21:43-21:45):
FOTArray unimplemented for backend

I need to do some further digging to figure out if this is the fault of Crucible or SAW.

[RyanGlScott]

The FOTArray unimplemented for backend error message arises from saw-core-sbv, which seems to indicate that SBV just can't handle to the new array-based functionality used in the StableSymbolic approach. Indeed, if I change my test script such that it uses w4_unint_z3 instead of sbv_z3, then everything works as expected. I guess this is a potential pitfall we'd have to document on the SAW side? Bummer.

In any case, this gives me confidence that everything is working as expected (SBV limitations notwithstanding). I'll mark this as ready for review.