-
Notifications
You must be signed in to change notification settings - Fork 100
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.
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
Add UB checks for ptr_offset_from* intrinsics #3757
Add UB checks for ptr_offset_from* intrinsics #3757
Conversation
Still need to adjust tests
Add a new model for `ptr_offset_from` and `ptr_offset_from_unsigned` intrinsics that check allocation and address order.
Moved the ZST check above the check for the same pointer, since the function panics for all ZST pointers
I did some digging into the failing perf tests. The problem seems to be that these models don't properly handle iteration over vectors of vectors, e.g. #[kani::proof]
#[kani::unwind(5)]
#[kani::solver(minisat)]
fn main() {
let v1: Vec<Vec<i32>> = vec![vec![1], vec![2]];
v1.into_iter();
} This code fails with:
|
and adjust test to use byte_offset_from
I'm investigating this issue. It seems that the failure occurs inside |
My bad... I confused size and alignment. Only the second is a power of two. 😊 |
and test adjustments
7a72f0e
to
509c6af
Compare
4d477f6
## What's Changed * Package Docker release step: ensure compiler is installed by @tautschnig in #3789 * Improve `--jobs` UI by @carolynzech in #3790 * Update kissat to v4.0.1 by @remi-delmas-3000 in #3791 * Automatic cargo update to 2024-12-23 by @github-actions in #3792 * Bump tests/perf/s2n-quic from `0b3f892` to `a54686e` by @dependabot in #3793 * Upgrade toolchain to nightly-2024-12-18 by @zhassan-aws in #3794 * Automatic cargo update to 2024-12-30 by @github-actions in #3800 * fix: clippy by @ShoyuVanilla in #3806 * Update dependencies (02.01.2025). by @remi-delmas-3000 in #3809 * Update charon submodule by @zhassan-aws in #3801 * Upgrade toolchain to 2024-12-19 by @zhassan-aws in #3810 * Automatic cargo update to 2025-01-06 by @github-actions in #3812 * Bump tests/perf/s2n-quic from `a54686e` to `ac52a48` by @dependabot in #3813 * Generate contracts of dependencies as assertions by @carolynzech in #3802 * Fix hanging command in `std-analysis.sh` by @carolynzech in #3818 * Add UB checks for ptr_offset_from* intrinsics by @celinval in #3757 * Toolchain update 06-01-2025 by @remi-delmas-3000 in #3814 * Automatic toolchain upgrade to nightly-2025-01-07 by @github-actions in #3820 * Include manifest-path when checking if packages are in the workspace by @qinheping in #3819 ## New Contributors * @ShoyuVanilla made their first contribution in #3806 **Full Changelog**: kani-0.57.0...kani-0.58.0 --------- Co-authored-by: Celina G. Val <[email protected]>
Add a new model for
ptr_offset_from
andptr_offset_from_unsigned
intrinsics that check allocation and address order.
Resolves #3756
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.