diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index a83cebe76609e..6c11ebfeb3691 100644 --- 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/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 93dd351b02958..2e4fcbcafe6cf 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -9,6 +9,11 @@ use crate::ptr::NonNull; use crate::slice::memchr; use crate::{fmt, intrinsics, ops, slice, str}; +use crate::ub_checks::Invariant; + +#[cfg(kani)] +use crate::kani; + // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link // depends on where the item is being documented. however, since this is libcore, we can't // actually reference libstd or liballoc in intra-doc links. so, the best we can do is remove the @@ -207,6 +212,22 @@ impl fmt::Display for FromBytesWithNulError { } } +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for &CStr { + /** + * Safety invariant of a valid CStr: + * 1. An empty CStr should have a null byte. + * 2. A valid CStr should end with a null-terminator and contains + * no intermediate null bytes. + */ + fn is_safe(&self) -> bool { + let bytes: &[c_char] = &self.inner; + let len = bytes.len(); + + !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0) + } +} + impl CStr { /// Wraps a raw C string with a safe C string wrapper. /// @@ -833,3 +854,91 @@ impl Iterator for Bytes<'_> { #[unstable(feature = "cstr_bytes", issue = "112115")] impl FusedIterator for Bytes<'_> {} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Helper function + fn arbitrary_cstr(slice: &[u8]) -> &CStr { + let result = CStr::from_bytes_until_nul(&slice); + kani::assume(result.is_ok()); + let c_str = result.unwrap(); + assert!(c_str.is_safe()); + c_str + } + + // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + #[kani::proof] + #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 + fn check_from_bytes_until_nul() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + // Covers the case of a single null byte at the end, no null bytes, as + // well as intermediate null bytes + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if let Ok(c_str) = result { + assert!(c_str.is_safe()); + } + } + + // pub const fn count_bytes(&self) -> usize + #[kani::proof] + #[kani::unwind(32)] + fn check_count_bytes() { + const MAX_SIZE: usize = 32; + let mut bytes: [u8; MAX_SIZE] = kani::any(); + + // Non-deterministically generate a length within the valid range [0, MAX_SIZE] + let mut len: usize = kani::any_where(|&x| x < MAX_SIZE); + + // If a null byte exists before the generated length + // adjust len to its position + if let Some(pos) = bytes[..len].iter().position(|&x| x == 0) { + len = pos; + } else { + // If no null byte, insert one at the chosen length + bytes[len] = 0; + } + + let c_str = CStr::from_bytes_until_nul(&bytes).unwrap(); + // Verify that count_bytes matches the adjusted length + assert_eq!(c_str.count_bytes(), len); + assert!(c_str.is_safe()); + } + + // pub const fn to_bytes(&self) -> &[u8] + #[kani::proof] + #[kani::unwind(32)] + fn check_to_bytes() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); + + let bytes = c_str.to_bytes(); + let end_idx = bytes.len(); + // Comparison does not include the null byte + assert_eq!(bytes, &slice[..end_idx]); + assert!(c_str.is_safe()); + } + + // pub const fn to_bytes_with_nul(&self) -> &[u8] + #[kani::proof] + #[kani::unwind(33)] + fn check_to_bytes_with_nul() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); + + let bytes = c_str.to_bytes_with_nul(); + let end_idx = bytes.len(); + // Comparison includes the null byte + assert_eq!(bytes, &slice[..end_idx]); + assert!(c_str.is_safe()); + } +} \ No newline at end of file diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 7aa6a309a06b5..34ab472735915 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; use crate::mem::SizedTypeProperties; use crate::slice::{self, SliceIndex}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; impl *mut T { /// Returns `true` if the pointer is null. @@ -400,6 +404,22 @@ impl *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::()` does not overflow `isize` + count.checked_mul(core::mem::size_of::() 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::() as isize)).is_some() && + // Precondition 3: If `T` is a unit type (`size_of::() == 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::() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count)))) + )] + // Postcondition: If `T` is a unit type (`size_of::() == 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::() == 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, @@ -998,6 +1018,23 @@ impl *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::()` does not overflow `isize` + count.checked_mul(core::mem::size_of::()).is_some() && + count * core::mem::size_of::() <= 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::()) as isize).is_some() && + // Precondition 3: If `T` is a unit type (`size_of::() == 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::() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count)))) + )] + // Postcondition: If `T` is a unit type (`size_of::() == 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::() == 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, @@ -1107,6 +1144,23 @@ impl *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::()` does not overflow `isize` + count.checked_mul(core::mem::size_of::()).is_some() && + count * core::mem::size_of::() <= 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::()) as isize).is_some() && + // Precondition 3: If `T` is a unit type (`size_of::() == 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::() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count)))) + )] + // Postcondition: If `T` is a unit type (`size_of::() == 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::() == 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, @@ -2302,3 +2356,126 @@ impl PartialOrd for *mut T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + + /// 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::::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::::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::::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 index aa224db211933..42ea9d75896d3 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())) } @@ -661,6 +665,12 @@ impl NonNull { #[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::()).is_some() && + count * core::mem::size_of::() <= isize::MAX as usize && + kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_sub(count)) + )] + #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(-(count as isize)))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -790,6 +800,11 @@ impl NonNull { #[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::() == 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::() as isize)] pub const unsafe fn offset_from(self, origin: NonNull) -> isize where T: Sized, @@ -883,6 +898,13 @@ impl NonNull { #[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::() == 0 + )] + #[ensures(|result: &usize| *result == self.as_ptr().offset_from(subtracted.as_ptr()) as usize)] pub const unsafe fn sub_ptr(self, subtracted: NonNull) -> usize where T: Sized, @@ -1536,6 +1558,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 +1909,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 +2074,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(); @@ -2256,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::::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::() * 1000; + let mut generator1 = kani::PointerGenerator::::new(); + let mut generator2 = kani::PointerGenerator::::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::() * 1000; + let mut generator1 = kani::PointerGenerator::::new(); + let mut generator2 = kani::PointerGenerator::::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); + } + } }