Commits on Dec 3, 2021

1. Invalidate memory properly with laxLoadsAndStores …

   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 committed Dec 3, 2021
   Configuration menu

   • View commit details
   • Copy full SHA for f241c80
   • Browse repository at this point

   Copy the full SHA

   f241c80 View commit details

   Browse the repository at this point in the history