Skip to content

Conversation

@celinval
Copy link
Contributor

@celinval celinval commented Dec 5, 2024

Add a new model for ptr_offset_from and ptr_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.

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.
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Dec 5, 2024
@tautschnig tautschnig marked this pull request as ready for review December 13, 2024 10:14
@tautschnig tautschnig requested a review from a team as a code owner December 13, 2024 10:14
@tautschnig tautschnig marked this pull request as draft December 13, 2024 10:46
@carolynzech carolynzech self-assigned this Dec 13, 2024
Carolyn Zech added 3 commits December 13, 2024 12:06
Moved the ZST check above the check for the same pointer, since the function panics for all ZST pointers
@carolynzech
Copy link
Contributor

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. Vec<Vec<T>>.
Minimal reproducer (based on perf/vec/vec/src/main.rs:

#[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:

Check 87: kani::rustc_intrinsics::ptr_offset_from::<std::vec::Vec<i32>>.safety_check.3
- Status: FAILURE
- Description: "Expected the distance between the pointers, in bytes, to be a multiple of the size of `T`"
- Location: ../../../../library/kani/src/lib.rs:54:1 in function kani::rustc_intrinsics::ptr_offset_from::<std::vec::Vec<i32>>

and adjust test to use byte_offset_from
@celinval
Copy link
Contributor Author

celinval commented Jan 4, 2025

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. Vec<Vec<T>>. Minimal reproducer (based on perf/vec/vec/src/main.rs:

#[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:

Check 87: kani::rustc_intrinsics::ptr_offset_from::<std::vec::Vec<i32>>.safety_check.3
- Status: FAILURE
- Description: "Expected the distance between the pointers, in bytes, to be a multiple of the size of `T`"
- Location: ../../../../library/kani/src/lib.rs:54:1 in function kani::rustc_intrinsics::ptr_offset_from::<std::vec::Vec<i32>>

I'm investigating this issue. It seems that the failure occurs inside size_hint of vec::IntoIter which is called by the drop implementation.

@celinval
Copy link
Contributor Author

celinval commented Jan 4, 2025

My bad... I confused size and alignment. Only the second is a power of two. 😊

@celinval celinval marked this pull request as ready for review January 6, 2025 18:28
@celinval celinval force-pushed the issue-3756-offset-from branch from 7a72f0e to 509c6af Compare January 8, 2025 23:27
@celinval celinval added this pull request to the merge queue Jan 9, 2025
Merged via the queue into model-checking:main with commit 4d477f6 Jan 9, 2025
27 of 28 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Jan 11, 2025
## 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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Kani does not detect UB for ptr_offset_from and ptr_offset_from_unsigned

3 participants