Contracts and Harnesses for <*const T>::add, sub and offset

library/core/src/ptr/const_ptr.rs

@@ -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> *const T {
     /// Returns `true` if the pointer is null.
@@ -405,6 +409,20 @@ impl<T: ?Sized> *const 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
+    #[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, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *const T
     where
         T: Sized,
@@ -918,6 +936,21 @@ impl<T: ?Sized> *const 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
+    #[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, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1027,6 +1060,21 @@ impl<T: ?Sized> *const 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
+    #[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, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -1899,3 +1947,219 @@ impl<T: ?Sized> PartialOrd for *const T {
         *self >= *other
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use crate::kani;
+    use core::mem;
+    // Constant for array size used in all tests, for performance reason
+    const ARRAY_SIZE: usize = 5;
+
+    /// This macro generates verification harnesses for the `offset`, `add`, and `sub`
+    /// pointer operations for a slice type and function name.
+    /// - `$ty`: The type of the array (e.g., i32, u32, tuples).
+    /// - `$offset_fn`: The function name for the `offset` operation.
+    /// - `$add_fn`: The function name for the `add` operation.
+    /// - `$sub_fn`: The function name for the `sub` operation.
+    macro_rules! generate_slice_harnesses {
+        ($ty:ty, $offset_fn:ident, $add_fn:ident, $sub_fn:ident) => {
+            // Generates a harness for the `offset` operation
+            #[kani::proof_for_contract(<*const $ty>::offset)]
+            fn $offset_fn() {
+                let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *const $ty = arr.as_ptr();
+                let offset: usize = kani::any();
+                let count: isize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset);                
+                unsafe {
+                    ptr_with_offset.offset(count);
+                }
+            }
+
+            // Generates a harness for the `add` operation
+            #[kani::proof_for_contract(<*const $ty>::add)]
+            fn $add_fn() {
+                let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *const $ty = arr.as_ptr();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset);                
+                unsafe {
+                    ptr_with_offset.add(count);
+                }
+            }
+
+            // Generates a harness for the `sub` operation
+            #[kani::proof_for_contract(<*const $ty>::sub)]
+            fn $sub_fn() {
+                let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *const $ty = arr.as_ptr();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset);                
+                unsafe {
+                    ptr_with_offset.sub(count);
+                }
+            }
+        };
+    }
+
+    // Generate slice harnesses for various types (offset, add, sub)
+    generate_slice_harnesses!(i8, check_const_offset_slice_i8, check_const_add_slice_i8, check_const_sub_slice_i8);
+    generate_slice_harnesses!(i16, check_const_offset_slice_i16, check_const_add_slice_i16, check_const_sub_slice_i16);
+    generate_slice_harnesses!(i32, check_const_offset_slice_i32, check_const_add_slice_i32, check_const_sub_slice_i32);
+    generate_slice_harnesses!(i64, check_const_offset_slice_i64, check_const_add_slice_i64, check_const_sub_slice_i64);
+    generate_slice_harnesses!(i128, check_const_offset_slice_i128, check_const_add_slice_i128, check_const_sub_slice_i128);
+    generate_slice_harnesses!(isize, check_const_offset_slice_isize, check_const_add_slice_isize, check_const_sub_slice_isize);
+    generate_slice_harnesses!(u8, check_const_offset_slice_u8, check_const_add_slice_u8, check_const_sub_slice_u8);
+    generate_slice_harnesses!(u16, check_const_offset_slice_u16, check_const_add_slice_u16, check_const_sub_slice_u16);
+    generate_slice_harnesses!(u32, check_const_offset_slice_u32, check_const_add_slice_u32, check_const_sub_slice_u32);
+    generate_slice_harnesses!(u64, check_const_offset_slice_u64, check_const_add_slice_u64, check_const_sub_slice_u64);
+    generate_slice_harnesses!(u128, check_const_offset_slice_u128, check_const_add_slice_u128, check_const_sub_slice_u128);
+    generate_slice_harnesses!(usize, check_const_offset_slice_usize, check_const_add_slice_usize, check_const_sub_slice_usize);
+
+    // Generate slice harnesses for tuples (offset, add, sub)
+    generate_slice_harnesses!(
+        (i8, i8),
+        check_const_offset_slice_tuple_1,
+        check_const_add_slice_tuple_1,
+        check_const_sub_slice_tuple_1
+    );    
+    generate_slice_harnesses!(
+        (f64, bool),
+        check_const_offset_slice_tuple_2,
+        check_const_add_slice_tuple_2,
+        check_const_sub_slice_tuple_2
+    );
+    generate_slice_harnesses!(
+        (i32, f64, bool),
+        check_const_offset_slice_tuple_3,
+        check_const_add_slice_tuple_3,
+        check_const_sub_slice_tuple_3
+    );
+    generate_slice_harnesses!(
+        (i8, u16, i32, u64, isize),
+        check_const_offset_slice_tuple_4,
+        check_const_add_slice_tuple_4,
+        check_const_sub_slice_tuple_4
+    );
+
+    /// 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_const_arithmetic_harness {
+        ($type:ty, $proof_name:ident, add) => {
+            #[kani::proof_for_contract(<*const $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: *const $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(<*const $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: *const $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(<*const $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: *const $type = generator.any_in_bounds().ptr;
+                let count: isize = kani::any();
+                unsafe {
+                    test_ptr.offset(count);
+                }
+            }
+        };
+    }
+
+    // <*const T>:: add() integer types verification
+    generate_const_arithmetic_harness!(i8, check_const_add_i8, add);
+    generate_const_arithmetic_harness!(i16, check_const_add_i16, add);
+    generate_const_arithmetic_harness!(i32, check_const_add_i32, add);
+    generate_const_arithmetic_harness!(i64, check_const_add_i64, add);
+    generate_const_arithmetic_harness!(i128, check_const_add_i128, add);
+    generate_const_arithmetic_harness!(isize, check_const_add_isize, add);
+    generate_const_arithmetic_harness!(u8, check_const_add_u8, add);
+    generate_const_arithmetic_harness!(u16, check_const_add_u16, add);
+    generate_const_arithmetic_harness!(u32, check_const_add_u32, add);
+    generate_const_arithmetic_harness!(u64, check_const_add_u64, add);
+    generate_const_arithmetic_harness!(u128, check_const_add_u128, add);
+    generate_const_arithmetic_harness!(usize, check_const_add_usize, add);   
+
+    // <*const T>:: add() unit type verification
+    generate_const_arithmetic_harness!((), check_const_add_unit, add);
+
+    // <*const T>:: add() composite types verification
+    generate_const_arithmetic_harness!((i8, i8), check_const_add_tuple_1, add);
+    generate_const_arithmetic_harness!((f64, bool), check_const_add_tuple_2, add);
+    generate_const_arithmetic_harness!((i32, f64, bool), check_const_add_tuple_3, add);
+    generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_add_tuple_4, add);
+
+    // <*const T>:: sub() integer types verification
+    generate_const_arithmetic_harness!(i8, check_const_sub_i8, sub);
+    generate_const_arithmetic_harness!(i16, check_const_sub_i16, sub);
+    generate_const_arithmetic_harness!(i32, check_const_sub_i32, sub);
+    generate_const_arithmetic_harness!(i64, check_const_sub_i64, sub);
+    generate_const_arithmetic_harness!(i128, check_const_sub_i128, sub);
+    generate_const_arithmetic_harness!(isize, check_const_sub_isize, sub);
+    generate_const_arithmetic_harness!(u8, check_const_sub_u8, sub);
+    generate_const_arithmetic_harness!(u16, check_const_sub_u16, sub);
+    generate_const_arithmetic_harness!(u32, check_const_sub_u32, sub);
+    generate_const_arithmetic_harness!(u64, check_const_sub_u64, sub);
+    generate_const_arithmetic_harness!(u128, check_const_sub_u128, sub);
+    generate_const_arithmetic_harness!(usize, check_const_sub_usize, sub);
+
+    // <*const T>:: sub() unit type verification
+    generate_const_arithmetic_harness!((), check_const_sub_unit, sub);
+
+    // <*const T>:: sub() composite types verification
+    generate_const_arithmetic_harness!((i8, i8), check_const_sub_tuple_1, sub);
+    generate_const_arithmetic_harness!((f64, bool), check_const_sub_tuple_2, sub);
+    generate_const_arithmetic_harness!((i32, f64, bool), check_const_sub_tuple_3, sub);
+    generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_sub_tuple_4, sub); 
+
+    // fn <*const T>::offset() integer types verification
+    generate_const_arithmetic_harness!(i8, check_const_offset_i8, offset);
+    generate_const_arithmetic_harness!(i16, check_const_offset_i16, offset);
+    generate_const_arithmetic_harness!(i32, check_const_offset_i32, offset);
+    generate_const_arithmetic_harness!(i64, check_const_offset_i64, offset);
+    generate_const_arithmetic_harness!(i128, check_const_offset_i128, offset);
+    generate_const_arithmetic_harness!(isize, check_const_offset_isize, offset);
+    generate_const_arithmetic_harness!(u8, check_const_offset_u8, offset);
+    generate_const_arithmetic_harness!(u16, check_const_offset_u16, offset);
+    generate_const_arithmetic_harness!(u32, check_const_offset_u32, offset);
+    generate_const_arithmetic_harness!(u64, check_const_offset_u64, offset);
+    generate_const_arithmetic_harness!(u128, check_const_offset_u128, offset);
+    generate_const_arithmetic_harness!(usize, check_const_offset_usize, offset);
+
+    // fn <*const T>::offset() unit type verification
+    generate_const_arithmetic_harness!((), check_const_offset_unit, offset);
+
+    // fn <*const T>::offset() composite type verification
+    generate_const_arithmetic_harness!((i8, i8), check_const_offset_tuple_1, offset);
+    generate_const_arithmetic_harness!((f64, bool), check_const_offset_tuple_2, offset);
+    generate_const_arithmetic_harness!((i32, f64, bool), check_const_offset_tuple_3, offset);
+    generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_offset_tuple_4, offset);
+}