CBMC: Pass uninitialized pointers in all verification harnesses #340
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hanno-becker
force-pushed
the
cbmc_harness_cleanup
branch
2 times, most recently
from
326c7e0 to
2a17cef
Compare
Previously, when a function under proof would assume a pointer to a structure, the verification harness would construct an instance of that structure on the stack and pass its address. This approach is unsound, because it adds to the contractual assumptions of the function the specifics of the function invocation in the test harness. For example, a missing bounds constraint in the spec might go undetected just because the stack-allocated variable happens to satisfy it. The most robust way to deal with this, so it seems, is to minimize the harnesses to merely pass uninitialized variables of the right type to the function under proof. In particular, where a pointer is expected, pass an uninitialized pointer, rather than the address of a stack allocated structure. Also, remove redundant `x != NULL` preconditions when `IS_FRESH(x,...)` is assumed. This is not only redundant, but also error prone because of diffblue/cbmc#8492. This commit implements those changes for all harnesses implemented so far. As it turns out, a few specs were incorrect because of missing IS_FRESH annotations, hidden by the correct allocation in the harness. Signed-off-by: Hanno Becker <[email protected]>
hanno-becker
force-pushed
the
cbmc_harness_cleanup
branch
from
2a17cef to
97b2a78
Compare
mkannwischer
approved these changes
Nov 5, 2024
There was a problem hiding this comment.
Thanks @hanno-becker. This looks good to me. I double checked that you have not missed any instances. Please make sure to adjust #306 with the same changes before you merge it.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Previously, when a function under proof would assume a pointer to a structure, the verification harness would construct an instance of that structure on the stack and pass its address.
This approach is unsound, because it adds to the contractual assumptions of the function the specifics of the function invocation in the test harness. For example, a missing bounds constraint in the spec might go undetected just because the stack-allocated variable happens to satisfy it.
The most robust way to deal with this, so it seems, is to minimize the harnesses to merely pass uninitialized variables of the right type to the function under proof. In particular, where a pointer is expected, pass an uninitialized pointer, rather than the address of a stack allocated structure.
Also, remove redundant
x != NULLpreconditions whenIS_FRESH(x,...)is assumed. This is not only redundant, but also error prone because of
diffblue/cbmc#8492.
This commit implements this change for all harnesses implemented so far.