diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index aa224db211933..915473ee027f0 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -112,6 +112,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_dangling", since = "1.36.0")] #[must_use] #[inline] + #[ensures(|result| !result.pointer.is_null() && result.pointer.is_aligned())] pub const fn dangling() -> Self { // SAFETY: ptr::dangling_mut() returns a non-null well-aligned pointer. unsafe { @@ -269,6 +270,7 @@ impl NonNull { #[unstable(feature = "ptr_metadata", issue = "81513")] #[rustc_const_unstable(feature = "ptr_metadata", issue = "81513")] #[inline] + #[ensures(|result| !result.pointer.is_null())] pub const fn from_raw_parts( data_pointer: NonNull<()>, metadata: ::Metadata, @@ -287,6 +289,8 @@ impl NonNull { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|(data_ptr, metadata)| !data_ptr.as_ptr().is_null())] + #[ensures(|(data_ptr, metadata)| self.as_ptr() as *const () == data_ptr.as_ptr() as *const ())] pub const fn to_raw_parts(self) -> (NonNull<()>, ::Metadata) { (self.cast(), super::metadata(self.as_ptr())) } @@ -1536,6 +1540,9 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_from_raw_parts_mut", since = "1.83.0")] #[must_use] #[inline] + #[ensures(|result| !result.pointer.is_null() + && result.pointer as *const T == data.pointer + && unsafe { result.as_ref() }.len() == len)] pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self { // SAFETY: `data` is a `NonNull` pointer which is necessarily non-null unsafe { Self::new_unchecked(super::slice_from_raw_parts_mut(data.as_ptr(), len)) } @@ -1884,6 +1891,20 @@ mod verify { use crate::ptr::null_mut; use kani::PointerGenerator; + trait SampleTrait { + fn get_value(&self) -> i32; + } + + struct SampleStruct { + value: i32, + } + + impl SampleTrait for SampleStruct { + fn get_value(&self) -> i32 { + self.value + } + } + impl kani::Arbitrary for NonNull { fn any() -> Self { let ptr: *mut T = kani::any::() as *mut T; @@ -2035,6 +2056,115 @@ mod verify { let offset = nonnull_xptr.align_offset(invalid_align); } + // pub const fn dangling() -> Self + #[kani::proof_for_contract(NonNull::dangling)] + pub fn non_null_check_dangling() { + // unsigned integer types + let ptr_u8 = NonNull::::dangling(); + let ptr_u16 = NonNull::::dangling(); + let ptr_u32 = NonNull::::dangling(); + let ptr_u64 = NonNull::::dangling(); + let ptr_u128 = NonNull::::dangling(); + let ptr_usize = NonNull::::dangling(); + // signed integer types + let ptr_i8 = NonNull::::dangling(); + let ptr_i16 = NonNull::::dangling(); + let ptr_i32 = NonNull::::dangling(); + let ptr_i64 = NonNull::::dangling(); + let ptr_i128 = NonNull::::dangling(); + let ptr_isize = NonNull::::dangling(); + // unit type + let ptr_unit = NonNull::<()>::dangling(); + // zero length slice from dangling unit pointer + let zero_len_slice = NonNull::slice_from_raw_parts(ptr_unit, 0); + } + + // pub const fn from_raw_parts(data_pointer: NonNull<()>, metadata: ::Metadata,) -> NonNull + #[kani::proof_for_contract(NonNull::from_raw_parts)] + #[kani::unwind(101)] + pub fn non_null_check_from_raw_parts() { + const ARR_LEN: usize = 100; + // Create a non-deterministic array and its slice + let arr: [i8; ARR_LEN] = kani::any(); + let arr_slice = kani::slice::any_slice_of_array(&arr); + // Get a raw NonNull pointer to the start of the slice + let arr_slice_raw_ptr = NonNull::new(arr_slice.as_ptr() as *mut ()).unwrap(); + // Create NonNull pointer from the start pointer and the length of the slice + let nonnull_slice = NonNull::<[i8]>::from_raw_parts(arr_slice_raw_ptr, arr_slice.len()); + // Ensure slice content is preserved, runtime at this step is proportional to ARR_LEN + unsafe { + kani::assert(arr_slice == nonnull_slice.as_ref(), "slice content must be preserve"); + } + + // zero-length dangling pointer example + let dangling_ptr = NonNull::<()>::dangling(); + let zero_length = NonNull::<[()]>::from_raw_parts(dangling_ptr, 0); + } + + #[kani::proof_for_contract(NonNull::from_raw_parts)] + pub fn non_null_check_from_raw_part_trait() { + // Create a SampleTrait object from SampleStruct + let sample_struct = SampleStruct { value: kani::any() }; + let trait_object: &dyn SampleTrait = &sample_struct; + + // Get the raw data pointer and metadata for the trait object + let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); + // Safety: For trait objects, the metadata must come from a pointer to the same underlying erased type + let metadata = core::ptr::metadata(trait_object); + + // Create NonNull from the data pointer and metadata + let nonnull_trait_object: NonNull = NonNull::from_raw_parts(trait_ptr, metadata); + + unsafe { + // Ensure trait method and member is preserved + kani::assert( trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), "trait method and member must correctly preserve"); + } + } + + // pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self + #[kani::proof_for_contract(NonNull::slice_from_raw_parts)] + #[kani::unwind(1001)] + pub fn non_null_check_slice_from_raw_parts() { + const ARR_LEN: usize = 1000; + // Create a non-deterministic array + let mut arr: [i8; ARR_LEN] = kani::any(); + // Get a raw NonNull pointer to the start of the slice + let arr_raw_ptr = NonNull::new(arr.as_mut_ptr()).unwrap(); + // Create NonNull slice from the start pointer and ends at random slice_len + // Safety: https://doc.rust-lang.org/std/slice/fn.from_raw_parts.html + let slice_len: usize = kani::any(); + kani::assume(slice_len <= ARR_LEN); + let nonnull_slice = NonNull::<[i8]>::slice_from_raw_parts(arr_raw_ptr, slice_len); + // Ensure slice content is preserved, runtime at this step is proportional to ARR_LEN + unsafe { + kani::assert(&arr[..slice_len] == nonnull_slice.as_ref(), "slice content must be preserve"); + } + + // TODO: zero-length example blocked by kani issue [#3670](https://github.com/model-checking/kani/issues/3670) + //let dangling_ptr = NonNull::<()>::dangling(); + //let zero_length = NonNull::<[()]>::slice_from_raw_parts(dangling_ptr, 0); + } + + + // pub const fn to_raw_parts(self) -> (NonNull<()>, ::Metadata) + #[kani::proof_for_contract(NonNull::to_raw_parts)] + pub fn non_null_check_to_raw_parts() { + // Create a SampleTrait object from SampleStruct + let sample_struct = SampleStruct { value: kani::any() }; + let trait_object: &dyn SampleTrait = &sample_struct; + + // Get the raw data pointer and metadata for the trait object + let trait_ptr = NonNull::from(trait_object).cast::<()>(); //both have eq failure + //let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); //Question: what's the difference + // Safety: For trait objects, the metadata must come from a pointer to the same underlying erased type + let metadata = core::ptr::metadata(trait_object); + + // Create NonNull from the data pointer and metadata + let nonnull_trait_object: NonNull = NonNull::from_raw_parts(trait_ptr, metadata); + let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object); + } + + #[kani::proof_for_contract(NonNull::as_mut)] pub fn non_null_check_as_mut() { let mut x: i32 = kani::any();