Contract and harness for copy_to, copy_to_nonoverlapping, copy_from, and copy_from_nonoverlapping

library/core/src/ptr/non_null.rs

@@ -1021,6 +1021,12 @@ 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 = "const_intrinsic_copy", since = "1.83.0")]
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
+        && ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr())
+        && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()))]
+    #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8)
+        && ub_checks::can_dereference(dest.as_ptr() as *const u8))]
+    #[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr())]
     pub const unsafe fn copy_to(self, dest: NonNull<T>, count: usize)
     where
         T: Sized,
@@ -1041,6 +1047,13 @@ 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 = "const_intrinsic_copy", since = "1.83.0")]
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
+        && ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr())
+        && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr())
+        && ub_checks::maybe_is_nonoverlapping(self.as_ptr() as *const (), dest.as_ptr() as *const (), count, core::mem::size_of::<T>()))]
+        #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8)
+        && ub_checks::can_dereference(dest.as_ptr() as *const u8))]
+    #[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr())]
     pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull<T>, count: usize)
     where
         T: Sized,
@@ -1061,6 +1074,12 @@ 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 = "const_intrinsic_copy", since = "1.83.0")]
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
+        && ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr())
+        && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()))]
+    #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8)
+        && ub_checks::can_dereference(self.as_ptr() as *const u8))]
+    #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())]
     pub const unsafe fn copy_from(self, src: NonNull<T>, count: usize)
     where
         T: Sized,
@@ -1081,6 +1100,13 @@ 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 = "const_intrinsic_copy", since = "1.83.0")]
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).map_or_else(|| false, |size| size <= isize::MAX as usize)
+        && ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr())
+        && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr())
+        && ub_checks::maybe_is_nonoverlapping(src.as_ptr() as *const (), self.as_ptr() as *const (), count, core::mem::size_of::<T>()))]
+    #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8)
+        && ub_checks::can_dereference(self.as_ptr() as *const u8))]
+    #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())]
     pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull<T>, count: usize)
     where
         T: Sized,
@@ -2475,4 +2501,62 @@ mod verify {
             let _ = ptr.byte_offset_from(origin);
         }
     }
+
+    #[kani::proof_for_contract(NonNull::<T>::copy_to)]
+    pub fn non_null_check_copy_to() {
+        // PointerGenerator instance
+        let mut generator = PointerGenerator::<16>::new();
+        // Generate arbitrary pointers for src and dest
+        let src_ptr = generator.any_in_bounds::<i32>().ptr;
+        let dest_ptr = generator.any_in_bounds::<i32>().ptr;
+         // Wrap the raw pointers in NonNull
+        let src = NonNull::new(src_ptr).unwrap();
+        let dest = NonNull::new(dest_ptr).unwrap();
+        // Generate an arbitrary count using kani::any
+        let count: usize = kani::any();
+        unsafe { src.copy_to(dest, count);}
+    }
+
+    #[kani::proof_for_contract(NonNull::<T>::copy_from)]
+    pub fn non_null_check_copy_from() {
+       // PointerGenerator instance
+       let mut generator = PointerGenerator::<16>::new();
+       // Generate arbitrary pointers for src and dest
+       let src_ptr = generator.any_in_bounds::<i32>().ptr;
+       let dest_ptr = generator.any_in_bounds::<i32>().ptr;
+        // Wrap the raw pointers in NonNull
+       let src = NonNull::new(src_ptr).unwrap();
+       let dest = NonNull::new(dest_ptr).unwrap();
+       // Generate an arbitrary count using kani::any
+       let count: usize = kani::any();
+       unsafe { src.copy_from(dest, count);}
+    }
+    #[kani::proof_for_contract(NonNull::<T>::copy_to_nonoverlapping)]
+    pub fn non_null_check_copy_to_nonoverlapping() {
+       // PointerGenerator instance
+       let mut generator = PointerGenerator::<16>::new();
+       // Generate arbitrary pointers for src and dest
+       let src_ptr = generator.any_in_bounds::<i32>().ptr;
+       let dest_ptr = generator.any_in_bounds::<i32>().ptr;
+        // Wrap the raw pointers in NonNull
+       let src = NonNull::new(src_ptr).unwrap();
+       let dest = NonNull::new(dest_ptr).unwrap();
+       // Generate an arbitrary count using kani::any
+       let count: usize = kani::any();
+       unsafe { src.copy_to_nonoverlapping(dest, count);}
+    }
+    #[kani::proof_for_contract(NonNull::<T>::copy_from_nonoverlapping)]
+    pub fn non_null_check_copy_from_nonoverlapping() {
+         // PointerGenerator instance
+         let mut generator = PointerGenerator::<16>::new();
+         // Generate arbitrary pointers for src and dest
+         let src_ptr = generator.any_in_bounds::<i32>().ptr;
+         let dest_ptr = generator.any_in_bounds::<i32>().ptr;
+          // Wrap the raw pointers in NonNull
+         let src = NonNull::new(src_ptr).unwrap();
+         let dest = NonNull::new(dest_ptr).unwrap();
+         // Generate an arbitrary count using kani::any
+         let count: usize = kani::any();
+         unsafe { src.copy_from_nonoverlapping(dest, count);}
+    }
 }