Skip to content

Adjust PropertyClass of assertions to identify UB #3860

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 14 commits into from
Feb 18, 2025
Merged

Adjust PropertyClass of assertions to identify UB #3860

merged 14 commits into from
Feb 18, 2025

Conversation

tautschnig
Copy link
Member

Anything listed as undefined behavior (UB) at
https://doc.rust-lang.org/reference/behavior-considered-undefined.html must also be considered UB by Kani and should not pass under should_fail. In preparation of this PR, all occurrences of PropertyClass in the code base were audited and, where necessary, adjusted.

Also, all uses of kani::assert were audited to confirm or adjust them. This resulted in first-time use of the UnsupportedCheck hook, which implied fixes to its implementation.

Resolves: #3571

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@tautschnig
Adjust PropertyClass of assertions to identify UB
756d938 
Anything listed as undefined behavior (UB) at
https://doc.rust-lang.org/reference/behavior-considered-undefined.html
must also be considered UB by Kani and should not pass under
`should_fail`. In preparation of this PR, all occurrences of
`PropertyClass` in the code base were audited and, where necessary,
adjusted.

Also, all uses of `kani::assert` were audited to confirm or adjust them.
This resulted in first-time use of the `UnsupportedCheck` hook, which
implied fixes to its implementation.

Resolves: model-checking#3571
@tautschnig tautschnig requested a review from a team as a code owner January 28, 2025 14:36
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jan 28, 2025
celinval
celinval reviewed Jan 28, 2025
View reviewed changes
celinval
celinval approved these changes Jan 28, 2025
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about value validity, memory initialization? I think they are all still using assertions.

celinval
celinval previously requested changes Jan 28, 2025
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

sorry, wrong selection... 😳

@tautschnig
Copy link
Member Author

What about value validity, memory initialization? I think they are all still using assertions.

Given how those were designed, is the only way to fix this to filter for their specific messages? My understanding is that those insert MIR-level assert calls, making them indistinguishable from user-provided assertions. Am I getting this wrong?

@celinval
Copy link
Contributor

What about value validity, memory initialization? I think they are all still using assertions.

Given how those were designed, is the only way to fix this to filter for their specific messages? My understanding is that those insert MIR-level assert calls, making them indistinguishable from user-provided assertions. Am I getting this wrong?

Can we insert calls to kani::safety_check instead of kani::assert here?

I think we can just swap this code to retrieve kani::safety_check instead of kani::assert, but it's worth checking that all users of this code are adding safety properties. Otherwise, we can create a second variant to this enum, which allows instrumentation passes to use different checks.

By looking at this code, it reminded me that we also have an internal function named kani::check. I think that's also intended to check for safety.

@tautschnig
Copy link
Member Author

tautschnig commented Feb 12, 2025 •
edited
Loading

Can we insert calls to kani::safety_check instead of kani::assert here?

@celinval If time permits, could you take a look at my proposed changes whether they match your expectations?

@tautschnig tautschnig assigned celinval and unassigned tautschnig Feb 13, 2025
@carolynzech carolynzech assigned carolynzech and unassigned celinval Feb 14, 2025
carolynzech
carolynzech approved these changes Feb 17, 2025
View reviewed changes
Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM modulo these nits. Thanks!

@tautschnig tautschnig dismissed celinval’s stale review February 18, 2025 10:34

Overridden by Carolyn's review per out-of-band communication.

@tautschnig tautschnig enabled auto-merge February 18, 2025 10:35
@tautschnig tautschnig added this pull request to the merge queue Feb 18, 2025
Merged via the queue into model-checking:main with commit ac8e0b9 Feb 18, 2025
27 of 28 checks passed
@tautschnig tautschnig deleted the audit-property-class branch February 18, 2025 12:21
@qinheping qinheping mentioned this pull request Mar 5, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 6, 2025
@qinheping @carolynzech
Bump Kani version to 0.60.0 (#3923)
67cd1e6 
## What's Changed
* Automatic cargo update to 2025-02-10 by @github-actions in
#3880
* Bump tests/perf/s2n-quic from `82dd0b5` to `a5d8422` by @dependabot in
#3882
* Fast fail feature - Stops verification process as soon as one failure
is observed - Use case : CI speed up by @rajath-mk in
#3879
* Autoharness Subcommand by @carolynzech in
#3874
* Upgrade toolchain to 2/10 by @carolynzech in
#3883
* Add loop-contracts doc to SUMMARY by @qinheping in
#3886
* Support concrete playback for arrays of length 65 or greater by
@carolynzech in #3888
* Automatic cargo update to 2025-02-17 by @github-actions in
#3889
* Bump tests/perf/s2n-quic from `a5d8422` to `00e3371` by @dependabot in
#3894
* Adjust PropertyClass of assertions to identify UB by @tautschnig in
#3860
* Fix: regression test from #3888 has version control change by
@carolynzech in #3892
* Upgrade toolchain to 2025-02-11 by @thanhnguyen-aws in
#3887
* Remove isize overflow check for zst offsets by @carolynzech in
#3897
* Automatic toolchain upgrade to nightly-2025-02-12 by @github-actions
in #3898
* Upgrade the toolchain to 2025-02-21 by @zhassan-aws in
#3899
* Automatic cargo update to 2025-02-24 by @github-actions in
#3901
* Bump ncipollo/release-action from 1.15.0 to 1.16.0 by @dependabot in
#3902
* Bump tests/perf/s2n-quic from `00e3371` to `cfb314b` by @dependabot in
#3903
* Convert raw URL to link by @flba-eb in
#3907
* Automatic cargo update to 2025-03-03 by @github-actions in
#3913
* Install toolchain with rustup >= 1.28.0 by @tautschnig in
#3917
* Bump tests/perf/s2n-quic from `cfb314b` to `d88faa4` by @dependabot in
#3916
* Remove Ubuntu 20.04 CI usage by @tautschnig in
#3918
* Move standard-library metrics script to verify-rust-std repo by
@tautschnig in #3914
* scanner: Fix loop stats in overall function stats summary by
@tautschnig in #3915
* Update toolchain to 2025-03-02 by @remi-delmas-3000 in
#3911

## New Contributors
* @flba-eb made their first contribution in
#3907

**Full Changelog**:
kani-0.59.0...kani-0.60.0

---------

Co-authored-by: Carolyn Zech <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@carolynzech carolynzech carolynzech approved these changes

@celinval celinval celinval left review comments

Assignees

@carolynzech carolynzech

Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

UB checks should fail verification for harnesses annotated with #[should_panic]
3 participants
@tautschnig @celinval @carolynzech