Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Apr 12, 2022

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.

@sim642
Copy link
Member Author

sim642 commented Apr 22, 2022

On a small example extracted from zstd, it seems that this fix is also needed to overcome #686 (comment) (on top of everything else there). I'll see if this also is sufficient on the entire zstd.

@sim642
Copy link
Member Author

sim642 commented Apr 22, 2022

Merging this since it seems to be crucial for zstd soundness.

@sim642 sim642 merged commit 8b44490 into master Apr 22, 2022
@sim642 sim642 deleted the ddverify-pcwd branch April 22, 2022 15:49
sim642 added a commit that referenced this pull request Apr 22, 2022
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants