Add unchecked/SIMD bitshift checks and disable CBMC flag #2630
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-check
is 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.