Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix unsound dereferencing of unknown pointer offset chain in DDVerify #684

Merged
merged 3 commits into from
Apr 22, 2022

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.

1 participant