Fix unsound dereferencing of unknown pointer offset chain in DDVerify #684
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
In goblint/bench#26, I found a case of unsoundness due to our handling of unknown pointers in dereferencing chains. Namely, when intermediate dereferings contain unknown pointers in addition to known ones, we very eagerly go to supertop and forget all the known pointers.
This causes unnecessary unsoundness by not calling operation function pointers that we could know about. It's especially relevant for DDVerify, where the implementation stubs for the operation struct management are actually provided as plain global arrays.
I'm not very sure about the fix though. When dereferencing, there's a check for downcast vs upcast safety, but that only allows known pointers. I'm not sure how it should extend to
NULL
and unknown pointers, but it somehow needs to such that we don't drop all known pointers so easily.