Harnesses verifying slice types for add, sub and offset

library/core/src/ptr/mut_ptr.rs

@@ -404,8 +404,10 @@ 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() &&
@@ -1018,6 +1020,7 @@ 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(
@@ -1033,7 +1036,7 @@ impl<T: ?Sized> *mut T {
     )]
     // 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`.
+    // 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
@@ -1144,8 +1147,10 @@ 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() &&
@@ -1159,7 +1164,8 @@ impl<T: ?Sized> *mut T {
     )]
     // 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`.
+    // 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
@@ -2361,6 +2367,80 @@ impl<T: ?Sized> PartialOrd for *mut T {
 #[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.
+    macro_rules! generate_mut_slice_harnesses {
+        ($ty:ty, $offset_fn:ident, $add_fn:ident, $sub_fn:ident) => {
+            // Generates a harness for the `offset` operation
+            #[kani::proof_for_contract(<*mut $ty>::offset)]
+            fn $offset_fn() {
+                let mut arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *mut $ty = arr.as_mut_ptr();
+                let offset: usize = kani::any();
+                let count: isize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset);                
+                unsafe {
+                    ptr_with_offset.offset(count);
+                }
+            }
+
+            // Generates a harness for the `add` operation
+            #[kani::proof_for_contract(<*mut $ty>::add)]
+            fn $add_fn() {
+                let mut arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *mut $ty = arr.as_mut_ptr();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset);                
+                unsafe {
+                    ptr_with_offset.add(count);
+                }
+            }
+
+            // Generates a harness for the `sub` operation
+            #[kani::proof_for_contract(<*mut $ty>::sub)]
+            fn $sub_fn() {
+                let mut arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *mut $ty = arr.as_mut_ptr();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset);                
+                unsafe {
+                    ptr_with_offset.sub(count);
+                }
+            }
+        };
+    }
+
+    // Generate pointer harnesses for various types (offset, add, sub)
+    generate_mut_slice_harnesses!(i8, check_mut_offset_slice_i8, check_mut_add_slice_i8, check_mut_sub_slice_i8);
+    generate_mut_slice_harnesses!(i16, check_mut_offset_slice_i16, check_mut_add_slice_i16, check_mut_sub_slice_i16);
+    generate_mut_slice_harnesses!(i32, check_mut_offset_slice_i32, check_mut_add_slice_i32, check_mut_sub_slice_i32);
+    generate_mut_slice_harnesses!(i64, check_mut_offset_slice_i64, check_mut_add_slice_i64, check_mut_sub_slice_i64);
+    generate_mut_slice_harnesses!(i128, check_mut_offset_slice_i128, check_mut_add_slice_i128, check_mut_sub_slice_i128);
+    generate_mut_slice_harnesses!(isize, check_mut_offset_slice_isize, check_mut_add_slice_isize, check_mut_sub_slice_isize);
+    generate_mut_slice_harnesses!(u8, check_mut_offset_slice_u8, check_mut_add_slice_u8, check_mut_sub_slice_u8);
+    generate_mut_slice_harnesses!(u16, check_mut_offset_slice_u16, check_mut_add_slice_u16, check_mut_sub_slice_u16);
+    generate_mut_slice_harnesses!(u32, check_mut_offset_slice_u32, check_mut_add_slice_u32, check_mut_sub_slice_u32);
+    generate_mut_slice_harnesses!(u64, check_mut_offset_slice_u64, check_mut_add_slice_u64, check_mut_sub_slice_u64);
+    generate_mut_slice_harnesses!(u128, check_mut_offset_slice_u128, check_mut_add_slice_u128, check_mut_sub_slice_u128);
+    generate_mut_slice_harnesses!(usize, check_mut_offset_slice_usize, check_mut_add_slice_usize, check_mut_sub_slice_usize);
+
+    // Generate pointer harnesses for tuples (offset, add, sub)
+    generate_mut_slice_harnesses!((i8, i8), check_mut_offset_slice_tuple_1, check_mut_add_slice_tuple_1, check_mut_sub_slice_tuple_1);
+    generate_mut_slice_harnesses!((f64, bool), check_mut_offset_slice_tuple_2, check_mut_add_slice_tuple_2, check_mut_sub_slice_tuple_2);
+    generate_mut_slice_harnesses!((i32, f64, bool), check_mut_offset_slice_tuple_3, check_mut_add_slice_tuple_3, check_mut_sub_slice_tuple_3);
+    generate_mut_slice_harnesses!((i8, u16, i32, u64, isize), check_mut_offset_slice_tuple_4, check_mut_add_slice_tuple_4, check_mut_sub_slice_tuple_4);
+
+
+    // generate proof for contracts for integer type, composite type and unit type pointers
 
     /// This macro generates proofs for contracts on `add`, `sub`, and `offset`
     /// operations for pointers to integer, composite, and unit types.
@@ -2370,6 +2450,17 @@ mod verify {
         ($type:ty, $proof_name:ident, add) => {
             #[kani::proof_for_contract(<*mut $type>::add)]
             pub fn $proof_name() {
+                let mut test_val: $type = kani::any::<$type>();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();                
+                let test_ptr: *mut $type = &mut test_val;
+
+                // For integer, composite, and unit types, 1 is the largest offset that
+                // keeps `ptr_with_offset` within bounds.
+                kani::assume(offset <= 1); 
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                   
+                unsafe {
+                    ptr_with_offset.add(count);
                 // 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();
@@ -2383,6 +2474,17 @@ mod verify {
         ($type:ty, $proof_name:ident, sub) => {
             #[kani::proof_for_contract(<*mut $type>::sub)]
             pub fn $proof_name() {
+                let mut test_val: $type = kani::any::<$type>();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();
+                let test_ptr: *mut $type = &mut test_val;
+
+                // For integer, composite, and unit types, 1 is the largest offset that
+                // keeps `ptr_with_offset` within bounds.
+                kani::assume(offset <= 1);
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);
+                unsafe {
+                    ptr_with_offset.sub(count);
                 // 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();
@@ -2396,6 +2498,17 @@ mod verify {
         ($type:ty, $proof_name:ident, offset) => {
             #[kani::proof_for_contract(<*mut $type>::offset)]
             pub fn $proof_name() {
+                let mut test_val: $type = kani::any::<$type>();
+                let offset: usize = kani::any();
+                let count: isize = kani::any();
+                let test_ptr: *mut $type = &mut test_val;
+
+                // For integer, composite, and unit types, 1 is the largest offset that
+                // keeps `ptr_with_offset` within bounds.
+                kani::assume(offset <= 1);
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                
+                unsafe {
+                    ptr_with_offset.offset(count);
                 // 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();
@@ -2415,13 +2528,15 @@ mod verify {
     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);
+    generate_mut_arithmetic_harness!(u8, check_mut_add_u8, 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);   
     generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add);
 
     // <*mut T>:: add() unit type verification
@@ -2454,6 +2569,7 @@ mod verify {
     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); 
     generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub);
 
     // fn <*mut T>::offset() integer types verification