Merge branch 'main' into verify/ptr_const_byte_offset_from

stogaru · web-flow · commit 1d0fb7573d21 · 2024-11-27T14:48:21.000-08:00
diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml
@@ -16,5 +16,7 @@ members = [
     "robdockins",
     "HuStmpHrrr",
     "Eh2406",
-    "jswrenn"
+    "jswrenn",
+    "havelund",
+    "jorajeev"
 ]
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
@@ -405,6 +405,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,
@@ -1013,6 +1029,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,
@@ -1122,6 +1155,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,
@@ -2506,5 +2556,121 @@ pub mod verify {
     generate_mut_byte_offset_from_slice_harness!(i64, check_mut_byte_offset_from_i64_slice);
     generate_mut_byte_offset_from_slice_harness!(i128, check_mut_byte_offset_from_i128_slice);
     generate_mut_byte_offset_from_slice_harness!(isize, check_mut_byte_offset_from_isize_slice);
-    
+
+    /// 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);
 }
diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
@@ -665,6 +665,12 @@ impl<T: ?Sized> NonNull<T> {
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
     #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))]
+    #[requires(
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize && 
+        kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_sub(count))
+    )]
+    #[ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(-(count as isize)))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -794,6 +800,11 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires( 
+        (kani::mem::same_allocation(self.as_ptr(), origin.as_ptr()) && 
+        ((self.as_ptr().addr() - origin.as_ptr().addr()) % core::mem::size_of::<T>() == 0))
+    )] // Ensure both pointers meet safety conditions for offset_from
+    #[ensures(|result: &isize| *result == (self.as_ptr() as isize - origin.as_ptr() as isize) / core::mem::size_of::<T>() as isize)]
     pub const unsafe fn offset_from(self, origin: NonNull<T>) -> isize
     where
         T: Sized,
@@ -887,6 +898,13 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[unstable(feature = "ptr_sub_ptr", issue = "95892")]
     #[rustc_const_unstable(feature = "const_ptr_sub_ptr", issue = "95892")]
+    #[requires(
+        self.as_ptr().addr().checked_sub(subtracted.as_ptr().addr()).is_some() &&
+        kani::mem::same_allocation(self.as_ptr(), subtracted.as_ptr()) &&
+        (self.as_ptr().addr()) >= (subtracted.as_ptr().addr()) &&
+        (self.as_ptr().addr() - subtracted.as_ptr().addr()) % core::mem::size_of::<T>() == 0
+    )]
+    #[ensures(|result: &usize| *result == self.as_ptr().offset_from(subtracted.as_ptr()) as usize)]
     pub const unsafe fn sub_ptr(self, subtracted: NonNull<T>) -> usize
     where
         T: Sized,
@@ -2386,4 +2404,73 @@ mod verify {
         // Perform the alignment check
         let result = non_null_ptr.is_aligned_to(align);
     }
+
+    #[kani::proof_for_contract(NonNull::sub)]
+    pub fn non_null_check_sub() {
+        const SIZE: usize = 10000;
+        let mut generator = kani::PointerGenerator::<SIZE>::new();
+        // Get a raw pointer from the generator within bounds
+        let raw_ptr: *mut i32 = generator.any_in_bounds().ptr;
+        // Create a non-null pointer from the raw pointer
+        let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };
+        // Create a non-deterministic count value
+        let count: usize = kani::any();
+
+        unsafe {
+            let result = ptr.sub(count);
+        }
+    }
+    
+    #[kani::proof_for_contract(NonNull::sub_ptr)]
+    pub fn non_null_check_sub_ptr() {
+        const SIZE: usize = core::mem::size_of::<i32>() * 1000;
+        let mut generator1 = kani::PointerGenerator::<SIZE>::new();
+        let mut generator2 = kani::PointerGenerator::<SIZE>::new();
+
+        let ptr: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let origin: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() };
+        let origin_nonnull = unsafe { NonNull::new(origin).unwrap() };
+
+        unsafe {
+            let distance = ptr_nonnull.sub_ptr(origin_nonnull);
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::offset_from)]
+    #[kani::should_panic]
+    pub fn non_null_check_offset_from() {
+        const SIZE: usize = core::mem::size_of::<i32>() * 1000;
+        let mut generator1 = kani::PointerGenerator::<SIZE>::new();
+        let mut generator2 = kani::PointerGenerator::<SIZE>::new();
+
+        let ptr: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let origin: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() };
+        let origin_nonnull = unsafe { NonNull::new(origin).unwrap() };
+
+        unsafe {
+            let distance = ptr_nonnull.offset_from(origin_nonnull);
+        }
+    }
 }

Original file line number	Diff line number	Diff line change
`@@ -16,5 +16,7 @@ members = [`
`16`	`16`	`"robdockins",`
`17`	`17`	`"HuStmpHrrr",`
`18`	`18`	`"Eh2406",`
`19`		`- "jswrenn"`
	`19`	`+ "jswrenn",`
	`20`	`+ "havelund",`
	`21`	`+ "jorajeev"`
`20`	`22`	`]`