diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 68bcd0c1a3d84..714104930dd5a 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1035,8 +1035,14 @@ impl NonNull { /// [`ptr::copy`]: crate::ptr::copy() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr()))] #[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::()).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))] pub const unsafe fn copy_to(self, dest: NonNull, count: usize) where T: Sized, @@ -1055,8 +1061,15 @@ impl NonNull { /// [`ptr::copy_nonoverlapping`]: crate::ptr::copy_nonoverlapping() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr()))] #[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::()).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::()))] + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) + && ub_checks::can_dereference(dest.as_ptr() as *const u8))] pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull, count: usize) where T: Sized, @@ -1075,8 +1088,14 @@ impl NonNull { /// [`ptr::copy`]: crate::ptr::copy() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr()))] #[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::()).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))] pub const unsafe fn copy_from(self, src: NonNull, count: usize) where T: Sized, @@ -1095,8 +1114,15 @@ impl NonNull { /// [`ptr::copy_nonoverlapping`]: crate::ptr::copy_nonoverlapping() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr()))] #[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::()).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::()))] + #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) + && ub_checks::can_dereference(self.as_ptr() as *const u8))] pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull, count: usize) where T: Sized, @@ -2538,4 +2564,62 @@ mod verify { let _ = ptr.byte_offset_from(origin); } } + + #[kani::proof_for_contract(NonNull::::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::().ptr; + let dest_ptr = generator.any_in_bounds::().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::::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::().ptr; + let dest_ptr = generator.any_in_bounds::().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::::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::().ptr; + let dest_ptr = generator.any_in_bounds::().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::::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::().ptr; + let dest_ptr = generator.any_in_bounds::().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);} + } }