Skip to content

Commit

Permalink
Contracts and Harnesses for <*mut T>::add, sub and offset (#113)
Browse files Browse the repository at this point in the history 
Towards #76 

### Changes
* Adds contracts for `<*mut T>::add`, `<*mut T>::sub` and `<*mut
T>::offset`
* Adds proofs for contracts of the above functions verifying the pointee
types:
  * All integer types
  * Tuples (composite type)
  * Unit Type
* Defines a macro for add and sub and another for offset.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Yifei Wang <[email protected]>
Co-authored-by: MayureshJoshi25 <[email protected]>
Co-authored-by: Yifei Wang <[email protected]>
  • Loading branch information
@stogaru @xsxszab @MayureshJoshi25
4 people authored Nov 27, 2024
1 parent 716c6af commit 014965a
Showing 1 changed file with 177 additions and 0 deletions.
177 changes: 177 additions & 0 deletions library/core/src/ptr/mut_ptr.rs
View file
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`
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))))
)]
// 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);
}

0 comments on commit 014965a

Please sign in to comment.