diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915dbf..bfb93500f1281 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,6 +9,7 @@ use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; +use crate::{ub_checks}; #[cfg(kani)] @@ -139,6 +140,8 @@ impl NonNull { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure the pointer is valid to create a reference. + #[ensures(|result: &&MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure returned reference points to the correct memory location. pub const unsafe fn as_uninit_ref<'a>(self) -> &'a MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -163,6 +166,8 @@ impl NonNull { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure pointer is valid to create a mutable reference. + #[ensures(|result: &&mut MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure the returned reference points to the correct memory. pub const unsafe fn as_uninit_mut<'a>(self) -> &'a mut MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -368,6 +373,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_as_ref", since = "1.73.0")] #[must_use] #[inline(always)] + #[ensures(|result: &&T| core::ptr::eq(*result, self.as_ptr()))] // Ensure returned reference matches pointer pub const unsafe fn as_ref<'a>(&self) -> &'a T { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -406,6 +412,8 @@ impl NonNull { #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] #[must_use] #[inline(always)] + // verify result (a mutable reference) is still associated with the same memory address as the raw pointer stored in self + #[ensures(|result: &&mut T| core::ptr::eq(*result, self.as_ptr()))] pub const unsafe fn as_mut<'a>(&mut self) -> &'a mut T { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a mutable reference. @@ -1573,6 +1581,10 @@ impl NonNull<[T]> { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] + #[requires(self.as_ptr().cast::().align_offset(core::mem::align_of::()) == 0)] // Ensure the pointer is properly aligned + #[requires(self.len().checked_mul(core::mem::size_of::()).is_some() && self.len() * core::mem::size_of::() <= isize::MAX as usize)] // Ensure the slice size does not exceed isize::MAX + // TODO: add a require to check the slice belong to same allocated object with `same_allocation` + #[ensures(|result: &&[MaybeUninit]| core::ptr::eq(result.as_ptr(), self.cast().as_ptr()))] // Ensure the memory addresses match. pub const unsafe fn as_uninit_slice<'a>(self) -> &'a [MaybeUninit] { // SAFETY: the caller must uphold the safety contract for `as_uninit_slice`. unsafe { slice::from_raw_parts(self.cast().as_ptr(), self.len()) } @@ -1638,6 +1650,11 @@ impl NonNull<[T]> { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] + #[requires(self.as_ptr().cast::().align_offset(core::mem::align_of::()) == 0)] // Ensure the pointer is properly aligned + #[requires(self.len().checked_mul(core::mem::size_of::()).is_some() && self.len() * core::mem::size_of::() <= isize::MAX as usize)] // Ensure the slice size does not exceed isize::MAX + // TODO: add a require to check the slice belong to same allocated object with `same_allocation` + #[ensures(|result: &&mut [MaybeUninit]| result.len() == self.len())] // Length check + #[ensures(|result: &&mut [MaybeUninit]| core::ptr::eq(result.as_ptr(), self.cast().as_ptr()))] // Address check pub const unsafe fn as_uninit_slice_mut<'a>(self) -> &'a mut [MaybeUninit] { // SAFETY: the caller must uphold the safety contract for `as_uninit_slice_mut`. unsafe { slice::from_raw_parts_mut(self.cast().as_ptr(), self.len()) } @@ -1666,6 +1683,8 @@ impl NonNull<[T]> { /// ``` #[unstable(feature = "slice_ptr_get", issue = "74265")] #[inline] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is dereferenceable + #[ensures(|result: &NonNull| result.as_ptr() as *mut () != core::ptr::null_mut())] // Ensure valid non-null pointer pub unsafe fn get_unchecked_mut(self, index: I) -> NonNull where I: SliceIndex<[T]>, @@ -1803,4 +1822,99 @@ mod verify { let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } + + #[kani::proof_for_contract(NonNull::as_mut)] + pub fn non_null_check_as_mut() { + let mut x: i32 = kani::any(); + if let Some(mut ptr) = NonNull::new(&mut x as *mut i32) { + kani::assume(ptr.as_ptr().align_offset(core::mem::align_of::()) == 0); + unsafe { + let result = ptr.as_mut(); + } + } + } + + #[kani::proof_for_contract(NonNull::as_ref)] + pub fn non_null_check_as_ref() { + let mut x: i32 = kani::any(); + if let Some(ptr) = NonNull::new(&mut x as *mut i32) { + kani::assume(ptr.as_ptr().align_offset(core::mem::align_of::()) == 0); + unsafe { + let _ = ptr.as_ref(); + } + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_mut)] + pub fn non_null_check_as_uninit_mut() { + use core::mem::MaybeUninit; + + // Create an uninitialized MaybeUninit value + let mut uninit: MaybeUninit = MaybeUninit::uninit(); + let mut ptr = NonNull::new(uninit.as_mut_ptr()).unwrap(); + + unsafe { + let _ = ptr.as_uninit_mut(); + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_ref)] + pub fn non_null_check_as_uninit_ref() { + use core::mem::MaybeUninit; + + // Create an uninitialized MaybeUninit value + let mut uninit: MaybeUninit = MaybeUninit::uninit(); + let ptr = NonNull::new(uninit.as_mut_ptr()).unwrap(); + + unsafe { + let uninit_ref = ptr.as_uninit_ref(); + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_slice)] + pub fn non_null_check_as_uninit_slice() { + use core::mem::MaybeUninit; + + const SIZE: usize = 100000; + let mut arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let ptr = NonNull::slice_from_raw_parts( + NonNull::new(arr.as_mut_ptr()).unwrap(), + SIZE, + ); + + unsafe { + let _ = ptr.as_uninit_slice(); + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_slice_mut)] + pub fn non_null_check_as_uninit_slice_mut() { + use core::mem::MaybeUninit; + + const SIZE: usize = 100000; + let mut arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let ptr = NonNull::slice_from_raw_parts( + NonNull::new(arr.as_mut_ptr()).unwrap(), + SIZE, + ); + + unsafe { + let _ = ptr.as_uninit_slice_mut(); + } + } + + #[kani::proof_for_contract(NonNull::get_unchecked_mut)] + pub fn non_null_check_get_unchecked_mut() { + const ARR_SIZE: usize = 100000; + let mut arr: [i32; ARR_SIZE] = kani::any(); + let raw_ptr = arr.as_mut_ptr(); + let ptr = NonNull::slice_from_raw_parts( + NonNull::new(raw_ptr).unwrap(), + ARR_SIZE, + ); + let index = kani::any_where(|x| *x < ARR_SIZE - 1); + unsafe { + let _ = ptr.get_unchecked_mut(index..index + 1); + } + } }