Cxx/lax memory #294
Cxx/lax memory #294
Conversation
regarding pointer identity to be relaxed. In particular, there is a flag to allow order comparisons on arbitrary pointers (i.e., not from the same allocation block) and for equality comaprisons on pointers to constant data.
robdockins
force-pushed
the
cxx/lax-memory
branch
from
ee39613 to
ec533d3
Compare
|
I think this is ready to go in now. The two pointer relaxations this branch considers are now controlled by a pair of boolean flags in a |
| llvmExtensionImpl = | ||
| llvmExtensionImpl :: (HasPtrWidth (ArchWidth arch)) => MemOptions -> ExtensionImpl p sym (LLVM arch) | ||
| llvmExtensionImpl mo = | ||
| let ?memOpts = mo in |
There was a problem hiding this comment.
I'm assuming that this is an implicit param to avoid a much more intrusive implementation that would have threaded this explicitly through lots of places to make it available where it was needed? If so, you might want to mention that in the PR description for posterity.
There was a problem hiding this comment.
Yeah... at the moment it doesn't make much difference, but if similar options become more prevalent, I expect it will be a win.
There was a problem hiding this comment.
A more general solution would be allowing clients of the memory model to construct a filter function
UndefinedBehavior e -> Booland only using that in MemModel.assertUndefined to only make assertions that the client cares about. That being said, we can consider that at another time if this is easier for now.
|
Although deferring the control to the client is a nice option, we would still need to have some sort of indicator for what was being attempted to allow the client to decide what type of undefined operation was being attempted and at this stage the only real options are "fail" or "continue", so I don't think it would simplify the implementation very much. Like you said though, we could transition to that later on if it turns out to be useful. |
|
I'd be open to that kind of refactoring at some point, but I don't think it would simplify things much now. Also, we actually change the definition of pointer comparison depending on the flag, so a system for filtering UB isn't quite enough. |
|
@kquick I don't understand your comment. I'm suggesting a similar mechanism to what is in this MR, the difference would be allowing clients to enable or disable checking for any kind of undefined behavior, whereas this MR addresses two specific instances. @robdockins Doesn't the "lax" definition of pointer equality subsume the default one? It seems to me we just need to perform the lax check and toggle whether the assertion about the base pointer equality is made. |
|
I was suggesting that we would need to define various |
|
@kquick Thanks for clarifying! |
This PR relaxes some of the rules regarding when pointers can be compared in ways that are disallowed by the C standard, but are nonetheless common and appear in
libcxx.This PR exists as a reminder to