Skip to content
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

Merged
merged 16 commits into from
Jan 9, 2025

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-BenchCI 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
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
library/kani_core/src/models.rs Outdated Show resolved Hide resolved
tests/expected/offset-from-zst/main.rs Outdated Show resolved Hide resolved
@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-BenchCI 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