CBMC: Don't declare structures in harnesses #1039
Merged
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_fix
branch
from
3f2f72d to
513e073
Compare
hanno-becker
changed the title
mkannwischer
approved these changes
May 21, 2025
There was a problem hiding this comment.
Thanks @hanno-becker for fixing this.
Note that this was uncovered during proof development in mldsa-native: pq-code-package/mldsa-native#254
When CBMC checks a function contract, it seems that the preconditions set out in the contract are overlayed by the context set out in the harness. For example, if a function takes a pointer to `foo`, and the harness passes `&f` for `foo f`, then the function would never be evaluated for the possibility of an invalid pointer being passed. For that reason, harnesses must be as minimal as possible, merely declaring uninitialized variables of the expected type and calling the function under proof. This commit fixes a few instances in mlkem-native where this was not yet the case. Signed-off-by: Hanno Becker <[email protected]>
mkannwischer
force-pushed
the
cbmc_harness_fix
branch
from
513e073 to
0e9c732
Compare
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.
When CBMC checks a function contract, it seems that the preconditions set out in the contract are overlayed by the context set out in the harness. For example, if a function takes a pointer to
foo, and the harness passes&fforfoo f, then the function would never be evaluated for the possibility of an invalid pointer being passed. For that reason, harnesses must be as minimal as possible, merely declaring uninitialized variables of the expected type and calling the function under proof.This commit fixes a few instances in mlkem-native where this was not yet the case.