Add unchecked/SIMD bitshift checks and disable CBMC flag#2630
Merged
adpaco-aws merged 8 commits intomodel-checking:mainfrom Jul 31, 2023
Merged
Add unchecked/SIMD bitshift checks and disable CBMC flag#2630adpaco-aws merged 8 commits intomodel-checking:mainfrom
adpaco-aws merged 8 commits intomodel-checking:mainfrom
Conversation
Checks are now implemented in Kani
Remove tests for shifting a negative value as that is not UB in rust.
celinval
reviewed
Jul 27, 2023
Contributor
celinval
left a comment
There was a problem hiding this comment.
It looks pretty good. Can you please add a test to ensure that CBMC does the expected thing for shift with negative values?
Something like:
#[kani::proof]
#[kani::unwind(32)]
fn check_shl() {
let val : i32 = kani::any();
let dist = kani::any_where(|d: &u8| *d < 32);
assert_eq!(val << dist, val.wrapping_mul(2_i32.wrapping_pow(dist.into())));
}you might also want to add a modified version of the test you created in the issue description.
Co-authored-by: Celina G. Val <celinval@amazon.com>
Contributor
Author
|
Will work on adding the tests when I can! Also, my clock somehow got out of sync so I apologize about any incorrect date/timestamps on these commits. |
adpaco-aws
approved these changes
Jul 31, 2023
Contributor
adpaco-aws
left a comment
There was a problem hiding this comment.
Thank you, @reisnera !
my clock somehow got out of sync so I apologize about any incorrect date/timestamps on these commits.
No worries, we use the "squash and merge" option for PRs.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
Description of changes:
The CBMB flag
--undefined-shift-checkis too strict. In particular, it flags shifting a negative value as being incorrect, which is not the case for Rust where shifts are valid unless the shift distance is negative or larger than the bit width of the value being shifted.This PR disables the CBMC flag and adds checks to Kani both for the unchecked shift BinOps as well as SIMD shift intrinsics.
Resolved issues:
Resolves #2374 - shifting a negative value now works.
Resolves #1963 - SIMD shifts now have the same checks as non-SIMD-shifts, namely that the shift distance is not negative or larger than the bit width of the value being shifted.
Related RFC:
n/a
Call-outs:
The changes in intrinsic.rs could probably be more DRY but I'm not sure it's worth it.
Testing:
How is this change tested?
I believe existing tests cover this PR.
Is this a refactor change?
No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.