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

Contracts and Harnesses for <*mut T>::add, sub and offset #113

Merged
merged 32 commits into from
Nov 27, 2024
Merged
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
9a8993d
added common codes for all proof of contracts
xsxszab Oct 7, 2024
55950bb
implemented integer type proof for contract for fn add, sub and offset
xsxszab Oct 7, 2024
ce13e8f
Merge branch 'main' into verify/ptr_mut
stogaru Oct 9, 2024
3682858
Adds proofs for tuple types
stogaru Oct 9, 2024
a6d4d62
Renames harnesses
stogaru Oct 9, 2024
dec8c30
Added unit type proofs for mut ptr
MayureshJoshi25 Oct 9, 2024
2be7639
Merge pull request #8 from stogaru/verify/ptr_mut_unit_types
stogaru Oct 11, 2024
75179dc
Merge branch 'verify/ptr_mut' into verify/ptr_mut_integer_types
xsxszab Oct 11, 2024
34c670e
Merge pull request #6 from stogaru/verify/ptr_mut_integer_types
xsxszab Oct 11, 2024
66c956e
Merge branch 'verify/ptr_mut' into verify/ptr_mut_composite
stogaru Oct 11, 2024
d9b8c65
Merge pull request #7 from stogaru/verify/ptr_mut_composite
stogaru Oct 11, 2024
0faac46
Combined macros
stogaru Oct 11, 2024
82345de
Fixes a typo
stogaru Oct 12, 2024
656209b
Removes an unnecessary attribute
stogaru Oct 12, 2024
46e839c
Merge pull request #9 from stogaru/verify/ptr_mut_combined
stogaru Oct 12, 2024
96a8a2e
refactored function contracts for add, sub and offset using the same_…
xsxszab Oct 23, 2024
852e96f
merged macros for add, sub and offset
xsxszab Oct 23, 2024
04bd61e
updated function contracts and proof for contracts for add(), sub() a…
xsxszab Oct 24, 2024
7557fc5
added support for unit type pointers
xsxszab Oct 31, 2024
76b2311
updated function contracts, removed unnecessary kani::assmue
xsxszab Nov 6, 2024
cb6a177
added comments to function contracts
xsxszab Nov 6, 2024
6385d4a
Merge pull request #12 from stogaru/verify/ptr_mut_refactor_harness
xsxszab Nov 7, 2024
a079a7a
added comments for magic numbers
xsxszab Nov 7, 2024
214f84d
Merge branch 'main' into verify/ptr_mut
stogaru Nov 7, 2024
51ded41
updated proofs using pointer generator
xsxszab Nov 15, 2024
fb6215e
fixed typos in comments
xsxszab Nov 15, 2024
f229fd9
rustfmt formatting
xsxszab Nov 15, 2024
20fffa3
reverse unnecessary rustfmt formatting
xsxszab Nov 15, 2024
b9054a8
temporary disabled check_mut_add_u8 test
xsxszab Nov 16, 2024
b528b0e
Clarified preconditions with additional notes
xsxszab Nov 27, 2024
9b90b23
added tracking issue info for the pointer generator bug
xsxszab Nov 27, 2024
b3b0620
Merge branch 'main' into verify/ptr_mut
tautschnig Nov 27, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
177 changes: 177 additions & 0 deletions library/core/src/ptr/mut_ptr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less};
use crate::intrinsics::const_eval_select;
use crate::mem::SizedTypeProperties;
use crate::slice::{self, SliceIndex};
use safety::{ensures, requires};

#[cfg(kani)]
use crate::kani;

impl<T: ?Sized> *mut T {
/// Returns `true` if the pointer is null.
Expand Down Expand Up @@ -400,6 +404,22 @@ impl<T: ?Sized> *mut T {
#[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
// Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
// These conditions are not verified as part of the preconditions.
#[requires(
// Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
// Precondition 2: adding the computed offset to `self` does not cause overflow
(self as isize).checked_add((count * core::mem::size_of::<T>() as isize)).is_some() &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
// Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object,
// restricting `count` to prevent crossing allocation boundaries.
((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count))))
)]
feliperodri marked this conversation as resolved.
Show resolved Hide resolved
// Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
// Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
// verifying that the result remains within the same allocation as `self`.
#[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
pub const unsafe fn offset(self, count: isize) -> *mut T
where
T: Sized,
Expand Down Expand Up @@ -998,6 +1018,23 @@ impl<T: ?Sized> *mut T {
#[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
// Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
// These conditions are not verified as part of the preconditions.
#[requires(
// Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
count.checked_mul(core::mem::size_of::<T>()).is_some() &&
count * core::mem::size_of::<T>() <= isize::MAX as usize &&
// Precondition 2: adding the computed offset to `self` does not cause overflow
(self as isize).checked_add((count * core::mem::size_of::<T>()) as isize).is_some() &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
// Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object,
// restricting `count` to prevent crossing allocation boundaries.
((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count))))
)]
// Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
// Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
// verifying that the result remains within the same allocation as `self`.
#[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
pub const unsafe fn add(self, count: usize) -> Self
where
T: Sized,
Expand Down Expand Up @@ -1107,6 +1144,23 @@ impl<T: ?Sized> *mut T {
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))]
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
// Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
// These conditions are not verified as part of the preconditions.
#[requires(
// Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
count.checked_mul(core::mem::size_of::<T>()).is_some() &&
count * core::mem::size_of::<T>() <= isize::MAX as usize &&
// Precondition 2: subtracting the computed offset from `self` does not cause overflow
(self as isize).checked_sub((count * core::mem::size_of::<T>()) as isize).is_some() &&
// Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
// Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object,
// restricting `count` to prevent crossing allocation boundaries.
((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count))))
)]
// Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
// Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
// verifying that the result remains within the same allocation as `self`.
#[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
pub const unsafe fn sub(self, count: usize) -> Self
where
T: Sized,
Expand Down Expand Up @@ -2302,3 +2356,126 @@ impl<T: ?Sized> PartialOrd for *mut T {
*self >= *other
}
}

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use crate::kani;

/// This macro generates proofs for contracts on `add`, `sub`, and `offset`
/// operations for pointers to integer, composite, and unit types.
/// - `$type`: Specifies the pointee type.
/// - `$proof_name`: Specifies the name of the generated proof for contract.
macro_rules! generate_mut_arithmetic_harness {
($type:ty, $proof_name:ident, add) => {
#[kani::proof_for_contract(<*mut $type>::add)]
pub fn $proof_name() {
// 200 bytes are large enough to cover all pointee types used for testing
const BUF_SIZE: usize = 200;
let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
let test_ptr: *mut $type = generator.any_in_bounds().ptr;
let count: usize = kani::any();
unsafe {
test_ptr.add(count);
}
}
};
($type:ty, $proof_name:ident, sub) => {
#[kani::proof_for_contract(<*mut $type>::sub)]
pub fn $proof_name() {
// 200 bytes are large enough to cover all pointee types used for testing
const BUF_SIZE: usize = 200;
let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
let test_ptr: *mut $type = generator.any_in_bounds().ptr;
let count: usize = kani::any();
unsafe {
test_ptr.sub(count);
}
}
};
($type:ty, $proof_name:ident, offset) => {
#[kani::proof_for_contract(<*mut $type>::offset)]
pub fn $proof_name() {
// 200 bytes are large enough to cover all pointee types used for testing
const BUF_SIZE: usize = 200;
let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
let test_ptr: *mut $type = generator.any_in_bounds().ptr;
let count: isize = kani::any();
unsafe {
test_ptr.offset(count);
}
}
};
}

// <*mut T>:: add() integer types verification
generate_mut_arithmetic_harness!(i8, check_mut_add_i8, add);
generate_mut_arithmetic_harness!(i16, check_mut_add_i16, add);
generate_mut_arithmetic_harness!(i32, check_mut_add_i32, add);
generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add);
generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add);
generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add);
// Due to a bug of kani this test case is malfunctioning for now.
// Tracking issue: https://github.com/model-checking/kani/issues/3743
// generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add);
generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add);
generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add);
generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add);
generate_mut_arithmetic_harness!(u128, check_mut_add_u128, add);
generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add);

// <*mut T>:: add() unit type verification
generate_mut_arithmetic_harness!((), check_mut_add_unit, add);

// <*mut T>:: add() composite types verification
generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add);
generate_mut_arithmetic_harness!((f64, bool), check_mut_add_tuple_2, add);
generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_add_tuple_3, add);
generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add);

// <*mut T>:: sub() integer types verification
generate_mut_arithmetic_harness!(i8, check_mut_sub_i8, sub);
generate_mut_arithmetic_harness!(i16, check_mut_sub_i16, sub);
generate_mut_arithmetic_harness!(i32, check_mut_sub_i32, sub);
generate_mut_arithmetic_harness!(i64, check_mut_sub_i64, sub);
generate_mut_arithmetic_harness!(i128, check_mut_sub_i128, sub);
generate_mut_arithmetic_harness!(isize, check_mut_sub_isize, sub);
generate_mut_arithmetic_harness!(u8, check_mut_sub_u8, sub);
generate_mut_arithmetic_harness!(u16, check_mut_sub_u16, sub);
generate_mut_arithmetic_harness!(u32, check_mut_sub_u32, sub);
generate_mut_arithmetic_harness!(u64, check_mut_sub_u64, sub);
generate_mut_arithmetic_harness!(u128, check_mut_sub_u128, sub);
generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub);

// <*mut T>:: sub() unit type verification
generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);

// <*mut T>:: sub() composite types verification
generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub);
generate_mut_arithmetic_harness!((f64, bool), check_mut_sub_tuple_2, sub);
generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub);
generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub);

// fn <*mut T>::offset() integer types verification
generate_mut_arithmetic_harness!(i8, check_mut_offset_i8, offset);
generate_mut_arithmetic_harness!(i16, check_mut_offset_i16, offset);
generate_mut_arithmetic_harness!(i32, check_mut_offset_i32, offset);
generate_mut_arithmetic_harness!(i64, check_mut_offset_i64, offset);
generate_mut_arithmetic_harness!(i128, check_mut_offset_i128, offset);
generate_mut_arithmetic_harness!(isize, check_mut_offset_isize, offset);
generate_mut_arithmetic_harness!(u8, check_mut_offset_u8, offset);
generate_mut_arithmetic_harness!(u16, check_mut_offset_u16, offset);
generate_mut_arithmetic_harness!(u32, check_mut_offset_u32, offset);
generate_mut_arithmetic_harness!(u64, check_mut_offset_u64, offset);
generate_mut_arithmetic_harness!(u128, check_mut_offset_u128, offset);
generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset);

// fn <*mut T>::offset() unit type verification
generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);

// fn <*mut T>::offset() composite type verification
generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset);
generate_mut_arithmetic_harness!((f64, bool), check_mut_offset_tuple_2, offset);
generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_offset_tuple_3, offset);
generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4, offset);
}
Loading