Harnesses verifying slice types for add, sub and offset (#179)

Towards #76


## Changes
### Contracts Added:

- Added contracts for <*mut T>::add, <*mut T>::sub, and <*mut T>::offset
operations for raw pointers to slices.
### Proofs Implemented:

- Added proofs for the above contracts, verifying safety for the
following slice pointee types using arrays:
 - All integer types (i8, i16, i32, etc.).
 - Tuples (composite types) (e.g., (i8, i8), (i32, f64, bool)).
 - Unit type (()).
 
### Macro Definitions:
- Introduced macros to simplify and automate harness generation:
 - One macro for add and sub operations on slices.
 - Another macro for offset operations on slices.
 
### Array-Based Implementation for Slice Verification:
- Arrays are used as a proxy for slices (as slices do not have a known
length at compile time) to enable proper bounds checking and assumptions
during verification.

Author: szlee118

library/core/src/ptr/mut_ptr.rs

@@ -2242,6 +2242,82 @@ impl<T: ?Sized> PartialOrd for *mut T {
 mod verify {
     use crate::kani;
     use core::mem;
+
+    // Chosen for simplicity and sufficient size to test edge cases effectively
+    // Represents the number of elements in the slice or array being tested.
+    // Doesn't need to be large because all possible values for the slice are explored, 
+    // including edge cases like pointers at the start, middle, and end of the slice. 
+    // Symbolic execution generalizes across all possible elements, regardless of the actual array size.
+    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);
+
     use kani::PointerGenerator;
 
     /// This macro generates a single verification harness for the `offset`, `add`, or `sub`