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.

Sign up for GitHub

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

Jump to bottom

Add UB checks for ptr_offset_from* intrinsics #3757

Draft
wants to merge 11 commits into
base: main
Choose a base branch
from
Draft

Add UB checks for ptr_offset_from* intrinsics #3757

wants to merge 11 commits into from

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Dec 5, 2024 •
edited by tautschnig
Loading

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.

@celinval
Implement bounds check on offset
ed7e698 
Still need to adjust tests
@celinval
Fix tests after enabling offset bound checks
1632b67
@celinval
Add UB checks for ptr_offset_from* intrinsics
0f027cf 
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
@carolynzech
fix tests
e321b71
@carolynzech
add test for distance offset_from UB
049c1da
@carolynzech
Add test for pointers to ZSTs
b3beba3 
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>>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@carolynzech carolynzech

Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
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
@celinval @carolynzech @tautschnig