From 4ba2f628044de53649ed7776e533e6d9cf79fa5e Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 16 Oct 2024 11:23:19 -0700 Subject: [PATCH 01/14] verification for as_mut() --- library/core/src/ptr/non_null.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915dbf..7517e2dbc315d 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)] @@ -406,6 +407,10 @@ impl NonNull { #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] #[must_use] #[inline(always)] + // verify that `self` meets all the requirements for a mutable reference + #[requires(ub_checks::can_dereference(self))] + // 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. @@ -1803,4 +1808,14 @@ 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(); + let mut ptr = NonNull::new(x as *mut i32).unwrap(); + + unsafe { + let result = ptr.as_mut(); + } + } } From 0069da04d5276e7f28e0aa2b70d0fb4e5abcbb0e Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 16 Oct 2024 14:07:46 -0700 Subject: [PATCH 02/14] verification for as_ref() --- library/core/src/ptr/non_null.rs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 7517e2dbc315d..aa292ba45ee8b 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -369,6 +369,8 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_as_ref", since = "1.73.0")] #[must_use] #[inline(always)] + #[requires(ub_checks::can_dereference(self))] // Ensure pointer is valid for shared reference + #[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. @@ -1818,4 +1820,14 @@ mod verify { 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(); + let ptr = NonNull::new(x as *mut i32).unwrap(); + + unsafe { + let _ = ptr.as_ref(); + } + } } From dde0808c55e30ca7be23806b9920fe770d553bdc Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 16 Oct 2024 15:30:50 -0700 Subject: [PATCH 03/14] verification for as_uninit_ref() --- library/core/src/ptr/non_null.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index aa292ba45ee8b..06c09bb720c68 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -140,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. @@ -1830,4 +1832,17 @@ mod verify { let _ = ptr.as_ref(); } } + + #[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(); + } + } } From 6a49d068be876bd5d7cf2dc4524bf9bd7f6ee65c Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 16 Oct 2024 15:45:29 -0700 Subject: [PATCH 04/14] verification for as_uninit_mut() --- library/core/src/ptr/non_null.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 06c09bb720c68..306192915bbf7 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -166,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. @@ -1833,12 +1835,25 @@ mod verify { } } + #[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 mut uninit: MaybeUninit = MaybeUninit::uninit(); let ptr = NonNull::new(uninit.as_mut_ptr()).unwrap(); unsafe { From a0c6fed7b7da4620a256edebe7b06c1df2e6db2e Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 23 Oct 2024 16:36:57 -0700 Subject: [PATCH 05/14] verification for as_uninit_slice() --- library/core/src/ptr/non_null.rs | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 306192915bbf7..03de9a14b414c 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1584,6 +1584,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()) } @@ -1857,7 +1861,23 @@ mod verify { let ptr = NonNull::new(uninit.as_mut_ptr()).unwrap(); unsafe { - let uninit_ref = ptr.as_uninit_ref(); + 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 arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let ptr = NonNull::slice_from_raw_parts( + NonNull::new(arr.as_ptr()).unwrap(), + SIZE, + ); + + unsafe { + let _ = ptr.as_uninit_slice(); } } } From 673d861cd87cb7b406441b6454d504b437067b95 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 23 Oct 2024 17:33:17 -0700 Subject: [PATCH 06/14] verification for as_uninit_slice_mut() --- library/core/src/ptr/non_null.rs | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 03de9a14b414c..46048e36419cc 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1870,9 +1870,9 @@ mod verify { use core::mem::MaybeUninit; const SIZE: usize = 100000; - let arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let mut arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); let ptr = NonNull::slice_from_raw_parts( - NonNull::new(arr.as_ptr()).unwrap(), + NonNull::new(arr.as_mut_ptr()).unwrap(), SIZE, ); @@ -1880,4 +1880,20 @@ mod verify { 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(); + } + } } From 7c34873f322e2649b131d6151a398b4ab5212630 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 23 Oct 2024 17:33:26 -0700 Subject: [PATCH 07/14] verification for as_uninit_slice_mut() --- library/core/src/ptr/non_null.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 46048e36419cc..fac3b001aa6a2 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1653,6 +1653,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()) } @@ -1681,6 +1686,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]>, From b8aa51bb0d09446131e5bb78fce061ef59716043 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 24 Oct 2024 21:50:48 -0700 Subject: [PATCH 08/14] fix error for NonNull::get_unchecked_mut --- library/core/src/ptr/non_null.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index fac3b001aa6a2..77803cfadbc20 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -373,7 +373,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_as_ref", since = "1.73.0")] #[must_use] #[inline(always)] - #[requires(ub_checks::can_dereference(self))] // Ensure pointer is valid for shared reference + #[requires(ub_checks::can_dereference(self) == true)] // Ensure pointer is valid for shared reference #[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 @@ -1903,4 +1903,19 @@ mod verify { 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); + } + } } From 16d5a067d1acb039de8a886924e3048cef316f53 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 24 Oct 2024 22:36:43 -0700 Subject: [PATCH 09/14] fix failures for as_ref and as_mut --- library/core/src/ptr/non_null.rs | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 77803cfadbc20..bfb93500f1281 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -373,7 +373,6 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_as_ref", since = "1.73.0")] #[must_use] #[inline(always)] - #[requires(ub_checks::can_dereference(self) == true)] // Ensure pointer is valid for shared reference #[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 @@ -413,8 +412,6 @@ impl NonNull { #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] #[must_use] #[inline(always)] - // verify that `self` meets all the requirements for a mutable reference - #[requires(ub_checks::can_dereference(self))] // 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 { @@ -1829,20 +1826,22 @@ mod verify { #[kani::proof_for_contract(NonNull::as_mut)] pub fn non_null_check_as_mut() { let mut x: i32 = kani::any(); - let mut ptr = NonNull::new(x as *mut i32).unwrap(); - - unsafe { - let result = ptr.as_mut(); + 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(); - let ptr = NonNull::new(x as *mut i32).unwrap(); - - unsafe { - let _ = ptr.as_ref(); + 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(); + } } } From dd5c8702a81721955bc2893f0d0945d114c222b6 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 12 Nov 2024 23:59:43 -0800 Subject: [PATCH 10/14] update contracts --- library/core/src/ptr/non_null.rs | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index bfb93500f1281..6cef7cd9ce0b2 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,7 +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}; +use crate::ub_checks; #[cfg(kani)] @@ -373,6 +373,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_as_ref", since = "1.73.0")] #[must_use] #[inline(always)] + #[kani::requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure input is convertible to a reference #[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 @@ -412,6 +413,7 @@ impl NonNull { #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")] #[must_use] #[inline(always)] + #[kani::requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // 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 { @@ -1583,7 +1585,7 @@ impl NonNull<[T]> { #[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]| result.len() == self.len())] // Length check #[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`. @@ -1652,7 +1654,6 @@ impl NonNull<[T]> { #[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] { @@ -1683,8 +1684,9 @@ 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 + #[requires( + ub_checks::can_dereference(self.as_ptr()) // Ensure self can be dereferenced + )] pub unsafe fn get_unchecked_mut(self, index: I) -> NonNull where I: SliceIndex<[T]>, @@ -1827,7 +1829,6 @@ mod verify { 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(); } @@ -1838,7 +1839,6 @@ mod verify { 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(); } @@ -1912,9 +1912,14 @@ mod verify { NonNull::new(raw_ptr).unwrap(), ARR_SIZE, ); - let index = kani::any_where(|x| *x < ARR_SIZE - 1); + let lower = kani::any_where(|x| *x < ARR_SIZE); + let upper = kani::any_where(|x| *x < ARR_SIZE && *x >= lower); unsafe { - let _ = ptr.get_unchecked_mut(index..index + 1); + // NOTE: The `index` parameter cannot be used in the function contracts without being moved. + // Since `SliceIndex` does not guarantee that `index` implements `Clone` or `Copy`. To ensure 'index' is only used once, + // we put the in-bound check in proof harness as a workaround + kani::assume(ptr.as_ref().get(lower..upper).is_some()); + let _ = ptr.get_unchecked_mut(lower..upper); } } } From d30ec58261bec47f1a18049cdae97300ae08536f Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 13 Nov 2024 00:06:25 -0800 Subject: [PATCH 11/14] comment --- library/core/src/ptr/non_null.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 6cef7cd9ce0b2..f9fcf470ab846 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1916,8 +1916,10 @@ mod verify { let upper = kani::any_where(|x| *x < ARR_SIZE && *x >= lower); unsafe { // NOTE: The `index` parameter cannot be used in the function contracts without being moved. - // Since `SliceIndex` does not guarantee that `index` implements `Clone` or `Copy`. To ensure 'index' is only used once, - // we put the in-bound check in proof harness as a workaround + // Since the `SliceIndex` trait does not guarantee that `index` implements `Clone` or `Copy`, + // it cannot be reused after being consumed in the precondition. To comply with Rust's ownership + // rules and ensure `index` is only used once, the in-bounds check is moved to the proof harness + // as a workaround. kani::assume(ptr.as_ref().get(lower..upper).is_some()); let _ = ptr.get_unchecked_mut(lower..upper); } From bd44fb9840cf0b2cdef000923621b58e712e509f Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 13 Nov 2024 14:06:06 -0800 Subject: [PATCH 12/14] add in-bound check --- library/core/src/ptr/non_null.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index f9fcf470ab846..28bc25207d26e 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1585,6 +1585,7 @@ impl NonNull<[T]> { #[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 + #[requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_add(self.len() * core::mem::size_of::()) as *const()))] // Ensure the slice is contained within a single allocation #[ensures(|result: &&[MaybeUninit]| result.len() == self.len())] // Length check #[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] { @@ -1654,6 +1655,7 @@ impl NonNull<[T]> { #[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 + #[requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_add(self.len() * core::mem::size_of::()) as *const()))] // Ensure the slice is contained within a single 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] { @@ -1684,9 +1686,7 @@ impl NonNull<[T]> { /// ``` #[unstable(feature = "slice_ptr_get", issue = "74265")] #[inline] - #[requires( - ub_checks::can_dereference(self.as_ptr()) // Ensure self can be dereferenced - )] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self can be dereferenced pub unsafe fn get_unchecked_mut(self, index: I) -> NonNull where I: SliceIndex<[T]>, From f9bbf69959d071b03886633feac7ea8feaf256d8 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 14 Nov 2024 19:49:44 -0800 Subject: [PATCH 13/14] create slice with any_slice_of_array --- 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 52013145142ed..3983a98c9d76c 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1939,10 +1939,11 @@ mod verify { use core::mem::MaybeUninit; const SIZE: usize = 100000; - let mut arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let slice: &[MaybeUninit] = kani::slice::any_slice_of_array(&arr); let ptr = NonNull::slice_from_raw_parts( - NonNull::new(arr.as_mut_ptr()).unwrap(), - SIZE, + NonNull::new(slice.as_ptr() as *mut MaybeUninit).unwrap(), + slice.len(), ); unsafe { @@ -1956,8 +1957,9 @@ mod verify { const SIZE: usize = 100000; let mut arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let slice: &[MaybeUninit] = kani::slice::any_slice_of_array(&mut arr); let ptr = NonNull::slice_from_raw_parts( - NonNull::new(arr.as_mut_ptr()).unwrap(), + NonNull::new(slice.as_ptr() as *mut MaybeUninit).unwrap(), SIZE, ); From b7ff33c0889965016ab7acc9a88cacc7bc09c7e0 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 14 Nov 2024 21:08:15 -0800 Subject: [PATCH 14/14] fix compile errors --- 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 3983a98c9d76c..0075b2d19f46c 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -389,7 +389,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_as_ref", since = "1.73.0")] #[must_use] #[inline(always)] - #[kani::requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure input is convertible to a reference + #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure input is convertible to a reference #[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 @@ -429,7 +429,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_ptr_as_ref", since = "1.83.0")] #[must_use] #[inline(always)] - #[kani::requires(ub_checks::can_dereference(self.as_ptr() as *const()))] + #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // 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 {