From d3fb92de908173f2b4ddd4679afbdb7001c8fe2e Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Mon, 21 Oct 2024 22:45:26 -0400 Subject: [PATCH 1/9] draft for pointer creation & init APIs --- library/core/src/ptr/non_null.rs | 127 +++++++++++++++++++++++++++++++ 1 file changed, 127 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915dbf..9c98b6365e69e 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -111,6 +111,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: mem::align_of() returns a non-zero usize which is then casted // to a *mut T. Therefore, `ptr` is not null and the conditions for @@ -248,6 +249,8 @@ impl NonNull { #[unstable(feature = "ptr_metadata", issue = "81513")] #[rustc_const_unstable(feature = "ptr_metadata", issue = "81513")] #[inline] + //TODO: Do we want requires for different types? + #[ensures(|result| !result.pointer.is_null())] pub const fn from_raw_parts( data_pointer: NonNull<()>, metadata: ::Metadata, @@ -266,6 +269,7 @@ impl NonNull { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|(data_ptr, metadata)| self == NonNull::from_raw_parts(*data_ptr, *metadata))] pub const fn to_raw_parts(self) -> (NonNull<()>, ::Metadata) { (self.cast(), super::metadata(self.as_ptr())) } @@ -1443,10 +1447,17 @@ impl NonNull<[T]> { /// /// (Note that this example artificially demonstrates a use of this method, /// but `let slice = NonNull::from(&x[..]);` would be a better way to write code like this.) + // Safety: https://doc.rust-lang.org/std/slice/fn.from_raw_parts.html #[stable(feature = "nonnull_slice_from_raw_parts", since = "1.70.0")] #[rustc_const_unstable(feature = "const_slice_from_raw_parts_mut", issue = "67456")] #[must_use] #[inline] + //TODO: The entire memory range of this slice must be contained within a single allocated object(same_allocation?) which means must be valid for reads for len * mem::size_of::() many bytes + #[requires(data.pointer.is_aligned() + && len as isize * core::mem::size_of::() as isize <= isize::MAX + && (len as isize).checked_mul(core::mem::size_of::() as isize).is_some() + && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::() as isize).is_some())] // adding len * core::mem::size_of::() to data must not “wrap around” the address space + #[ensures(|result| !result.pointer.is_null())] //TODO: &data[..len] == result.as_ref() preserve content 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)) } @@ -1786,6 +1797,20 @@ mod verify { use super::*; use crate::ptr::null_mut; + trait SampleTrait { + fn get_value(&self) -> i32; + } + + struct SampleStruct { + value: i32, + } + + impl SampleTrait for SampleStruct { + fn get_value(&self) -> i32 { + self.value + } + } + // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] pub fn non_null_check_new_unchecked() { @@ -1803,4 +1828,106 @@ mod verify { let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } + + // 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(); + } +/* + // pub const fn from_raw_parts(data_pointer: NonNull<()>, metadata: ::Metadata,) -> NonNull + #[kani::proof_for_contract(NonNull::from_raw_parts)] + 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 = &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 + // Safety: https://doc.rust-lang.org/std/slice/fn.from_raw_parts.html + let nonnull_slice = NonNull::<[i8]>::from_raw_parts(arr_slice_raw_ptr, arr_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 preserve" ); + } + + // 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)] + pub fn non_null_check_slice_from_raw_parts() { + const arr_len: usize = 10; + // 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 preserve" ); + } + } + + // 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::<()>(); + //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); + let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object); +/* + 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"); + } + } +*/ + } } From 90f7b4b7feea0276652ca890dfa2739585a89d9b Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Fri, 25 Oct 2024 13:06:52 -0400 Subject: [PATCH 2/9] kani pointer compare bug fixed, using same_allocation, trait eq failure --- library/core/src/ptr/non_null.rs | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 9c98b6365e69e..78b9999389b76 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -269,6 +269,7 @@ 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())] //TODO: kani bug #[ensures(|(data_ptr, metadata)| self == NonNull::from_raw_parts(*data_ptr, *metadata))] pub const fn to_raw_parts(self) -> (NonNull<()>, ::Metadata) { (self.cast(), super::metadata(self.as_ptr())) @@ -1452,12 +1453,12 @@ impl NonNull<[T]> { #[rustc_const_unstable(feature = "const_slice_from_raw_parts_mut", issue = "67456")] #[must_use] #[inline] - //TODO: The entire memory range of this slice must be contained within a single allocated object(same_allocation?) which means must be valid for reads for len * mem::size_of::() many bytes #[requires(data.pointer.is_aligned() && len as isize * core::mem::size_of::() as isize <= isize::MAX && (len as isize).checked_mul(core::mem::size_of::() as isize).is_some() - && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::() as isize).is_some())] // adding len * core::mem::size_of::() to data must not “wrap around” the address space - #[ensures(|result| !result.pointer.is_null())] //TODO: &data[..len] == result.as_ref() preserve content + && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::() as isize).is_some() // adding len must not “wrap around” the address space + && unsafe { kani::mem::same_allocation(data.pointer, data.pointer.add(len)) })] + #[ensures(|result| !result.pointer.is_null())] //TODO: &data[..len] == result.as_ref() preserve content(question) 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)) } @@ -1848,8 +1849,11 @@ mod verify { let ptr_isize = NonNull::::dangling(); // unit type let ptr_unit = NonNull::<()>::dangling(); + // trait object + // let ptr_unit = NonNull::::dangling(); question: trait is unsized + // question: slice?? } -/* + // pub const fn from_raw_parts(data_pointer: NonNull<()>, metadata: ::Metadata,) -> NonNull #[kani::proof_for_contract(NonNull::from_raw_parts)] pub fn non_null_check_from_raw_parts() { @@ -1886,9 +1890,10 @@ mod verify { } } -*/ + // pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self #[kani::proof_for_contract(NonNull::slice_from_raw_parts)] + #[kani::unwind(11)] pub fn non_null_check_slice_from_raw_parts() { const arr_len: usize = 10; // Create a non-deterministic array @@ -1906,6 +1911,7 @@ mod verify { } } + // 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() { @@ -1914,20 +1920,19 @@ mod verify { 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::<()>(); - //let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); + 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); -/* + 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"); } } -*/ - } +//Question: pointer offset with integer without creating an array } From e5a7f149ffd29f882d705cc7ab1ef2070b53c1db Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Mon, 28 Oct 2024 11:11:44 -0400 Subject: [PATCH 3/9] add zero_len_slice in dangling, failed eq check in to_raw_parts --- library/core/src/ptr/non_null.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 78b9999389b76..b34ada19c59bd 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1797,6 +1797,7 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; + // use crate::boxed::Box; // failed to import trait SampleTrait { fn get_value(&self) -> i32; @@ -1850,8 +1851,9 @@ mod verify { // unit type let ptr_unit = NonNull::<()>::dangling(); // trait object - // let ptr_unit = NonNull::::dangling(); question: trait is unsized - // question: slice?? + // let ptr_trait = NonNull::>::dangling(); // failed to import Box + // 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 @@ -1931,8 +1933,8 @@ mod verify { 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"); + //kani::assert( trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), "trait method and member must correctly preserve"); // TODO: failed checks: partial eq + kani::assert( trait_object as *const dyn ptr::non_null::verify::SampleTrait == nonnull_trait_object.as_ptr(), "trait method and member must correctly preserve"); } } -//Question: pointer offset with integer without creating an array } From 13e669531e0b5ab6edd6ca0af7158f138a6e858f Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Thu, 7 Nov 2024 11:51:07 -0800 Subject: [PATCH 4/9] resolve partial eq --- library/core/src/ptr/non_null.rs | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index b34ada19c59bd..3b65525d2515a 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -249,7 +249,6 @@ impl NonNull { #[unstable(feature = "ptr_metadata", issue = "81513")] #[rustc_const_unstable(feature = "ptr_metadata", issue = "81513")] #[inline] - //TODO: Do we want requires for different types? #[ensures(|result| !result.pointer.is_null())] pub const fn from_raw_parts( data_pointer: NonNull<()>, @@ -269,8 +268,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())] //TODO: kani bug - #[ensures(|(data_ptr, metadata)| self == NonNull::from_raw_parts(*data_ptr, *metadata))] + #[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())) } @@ -1458,7 +1457,7 @@ impl NonNull<[T]> { && (len as isize).checked_mul(core::mem::size_of::() as isize).is_some() && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::() as isize).is_some() // adding len must not “wrap around” the address space && unsafe { kani::mem::same_allocation(data.pointer, data.pointer.add(len)) })] - #[ensures(|result| !result.pointer.is_null())] //TODO: &data[..len] == result.as_ref() preserve content(question) + #[ensures(|result| !result.pointer.is_null())] //TODO: compare byte by byte between data and result uptill len * size_of::() 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)) } @@ -1850,8 +1849,6 @@ mod verify { let ptr_isize = NonNull::::dangling(); // unit type let ptr_unit = NonNull::<()>::dangling(); - // trait object - // let ptr_trait = NonNull::>::dangling(); // failed to import Box // zero length slice from dangling unit pointer let zero_len_slice = NonNull::slice_from_raw_parts(ptr_unit, 0); } @@ -1867,7 +1864,6 @@ mod verify { // 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 - // Safety: https://doc.rust-lang.org/std/slice/fn.from_raw_parts.html let nonnull_slice = NonNull::<[i8]>::from_raw_parts(arr_slice_raw_ptr, arr_len); // Ensure slice content is preserved, runtime at this step is proportional to arr_len unsafe { @@ -1929,12 +1925,7 @@ mod verify { // 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); - - 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"); // TODO: failed checks: partial eq - kani::assert( trait_object as *const dyn ptr::non_null::verify::SampleTrait == nonnull_trait_object.as_ptr(), "trait method and member must correctly preserve"); - } + let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object); } + } From e408f24571687d7c154f739364ec11c429157961 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Tue, 12 Nov 2024 22:20:32 -0800 Subject: [PATCH 5/9] address PR comments --- library/core/src/ptr/non_null.rs | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 3b65525d2515a..fb2fa632a3998 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -7,7 +7,7 @@ use crate::pin::PinCoerceUnsized; use crate::ptr::Unique; use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; -use crate::{fmt, hash, intrinsics, ptr}; +use crate::{fmt, hash, intrinsics, ptr, ub_checks}; use safety::{ensures, requires}; @@ -1453,10 +1453,11 @@ impl NonNull<[T]> { #[must_use] #[inline] #[requires(data.pointer.is_aligned() - && len as isize * core::mem::size_of::() as isize <= isize::MAX + //&& len as isize * core::mem::size_of::() as isize <= isize::MAX && (len as isize).checked_mul(core::mem::size_of::() as isize).is_some() && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::() as isize).is_some() // adding len must not “wrap around” the address space - && unsafe { kani::mem::same_allocation(data.pointer, data.pointer.add(len)) })] + && unsafe { kani::mem::same_allocation(data.pointer, data.pointer.add(len)) + && ub_checks::can_dereference(data.pointer) })] #[ensures(|result| !result.pointer.is_null())] //TODO: compare byte by byte between data and result uptill len * size_of::() pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self { // SAFETY: `data` is a `NonNull` pointer which is necessarily non-null @@ -1857,15 +1858,15 @@ mod verify { #[kani::proof_for_contract(NonNull::from_raw_parts)] pub fn non_null_check_from_raw_parts() { - const arr_len: usize = 100; + const ARR_LEN: usize = 10000; // Create a non-deterministic array and its slice - let arr: [i8; arr_len] = kani::any(); + let arr: [i8; ARR_LEN] = kani::any(); let arr_slice = &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_len); - // Ensure slice content is preserved, runtime at this step is proportional to arr_len + let nonnull_slice = NonNull::<[i8]>::from_raw_parts(arr_slice_raw_ptr, ARR_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 preserve" ); } @@ -1893,17 +1894,17 @@ mod verify { #[kani::proof_for_contract(NonNull::slice_from_raw_parts)] #[kani::unwind(11)] pub fn non_null_check_slice_from_raw_parts() { - const arr_len: usize = 10; + const ARR_LEN: usize = 10000; // Create a non-deterministic array - let mut arr: [i8; arr_len] = kani::any(); + 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); + 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 + // 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 preserve" ); } From 27f3f6ca88748f2213a12c5c897db6887987714e Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 13 Nov 2024 22:46:22 -0800 Subject: [PATCH 6/9] address PR comments --- library/core/src/ptr/non_null.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 52b7e2ac2ed84..02c9f12de7f99 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1918,9 +1918,9 @@ mod verify { // pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self #[kani::proof_for_contract(NonNull::slice_from_raw_parts)] - #[kani::unwind(11)] + #[kani::unwind(1001)] pub fn non_null_check_slice_from_raw_parts() { - const ARR_LEN: usize = 10000; + 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 From 113e2570564828be257049e1ec21a53e73fa57b1 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Fri, 15 Nov 2024 11:31:13 -0800 Subject: [PATCH 7/9] address PR comments --- library/core/src/ptr/non_null.rs | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 02c9f12de7f99..5c1e20cb43579 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1482,7 +1482,6 @@ impl NonNull<[T]> { #[must_use] #[inline] #[requires(data.pointer.is_aligned() - //&& len as isize * core::mem::size_of::() as isize <= isize::MAX && (len as isize).checked_mul(core::mem::size_of::() as isize).is_some() && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::() as isize).is_some() // adding len must not “wrap around” the address space && unsafe { kani::mem::same_allocation(data.pointer, data.pointer.add(len)) @@ -1823,7 +1822,6 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; - // use crate::boxed::Box; // failed to import trait SampleTrait { fn get_value(&self) -> i32; @@ -1882,21 +1880,28 @@ mod verify { // 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 = 10000; + const ARR_LEN: usize = 100; // Create a non-deterministic array and its slice let arr: [i8; ARR_LEN] = kani::any(); - let arr_slice = &arr[..]; + 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_LEN); + 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 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; @@ -1913,7 +1918,6 @@ mod verify { // 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 @@ -1934,6 +1938,10 @@ mod verify { unsafe { kani::assert( &arr[..slice_len] == nonnull_slice.as_ref(), "slice content must 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); } From b0ea3035dee0056b8cb99082d5818fbc9b5f8c1e Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 20 Nov 2024 17:54:48 -0800 Subject: [PATCH 8/9] address PR comments, add correctness clause for slice_from_raw_parts --- library/core/src/ptr/non_null.rs | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index c0390cc811b62..e620ed4fb7a7b 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1515,17 +1515,13 @@ impl NonNull<[T]> { /// /// (Note that this example artificially demonstrates a use of this method, /// but `let slice = NonNull::from(&x[..]);` would be a better way to write code like this.) - // Safety: https://doc.rust-lang.org/std/slice/fn.from_raw_parts.html #[stable(feature = "nonnull_slice_from_raw_parts", since = "1.70.0")] #[rustc_const_stable(feature = "const_slice_from_raw_parts_mut", since = "1.83.0")] #[must_use] #[inline] - #[requires(data.pointer.is_aligned() - && (len as isize).checked_mul(core::mem::size_of::() as isize).is_some() - && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::() as isize).is_some() // adding len must not “wrap around” the address space - && unsafe { kani::mem::same_allocation(data.pointer, data.pointer.add(len)) - && ub_checks::can_dereference(data.pointer) })] - #[ensures(|result| !result.pointer.is_null())] //TODO: compare byte by byte between data and result uptill len * size_of::() + #[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)) } @@ -2057,7 +2053,7 @@ mod verify { 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 preserve" ); + kani::assert(arr_slice == nonnull_slice.as_ref(), "slice content must be preserve"); } // zero-length dangling pointer example @@ -2101,7 +2097,7 @@ mod verify { 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 preserve" ); + 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) From 37d210e4277695ad03171fe4e461d324e369c49d Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 25 Nov 2024 13:19:06 -0800 Subject: [PATCH 9/9] Minor fixes --- library/core/src/ptr/non_null.rs | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index d4d8521d82a94..915473ee027f0 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -7,11 +7,13 @@ use crate::pin::PinCoerceUnsized; use crate::ptr::Unique; use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; -use crate::{fmt, hash, intrinsics, ptr, ub_checks}; +use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; +#[cfg(kani)] +use crate::ub_checks; /// `*mut T` but non-zero and [covariant]. /// @@ -1538,7 +1540,7 @@ 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() + #[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 { @@ -1892,17 +1894,17 @@ mod verify { 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; @@ -2086,7 +2088,7 @@ mod verify { 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(); + 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 @@ -2127,7 +2129,7 @@ mod verify { // 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(); + 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(); @@ -2143,7 +2145,7 @@ mod verify { //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() { @@ -2159,7 +2161,7 @@ mod verify { // 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); + let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object); }