From bcdedb8611dee9347ec3a750c10c2c8d79ebf09c Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Sat, 5 Oct 2024 00:13:31 -0700 Subject: [PATCH 01/15] verification for byte_add, byte_offset, and byte_offset_from --- library/core/src/ptr/non_null.rs | 74 ++++++++++++++++++++++++++++++++ 1 file changed, 74 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915db..37dc25b77a46 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -502,6 +502,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(!origin.as_ptr().is_null())] + #[ensures( + |result: &isize| + *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) + )] pub const unsafe fn byte_offset(self, count: isize) -> Self { // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has // the same safety contract. @@ -579,6 +584,11 @@ impl NonNull { #[rustc_allow_const_fn_unstable(set_ptr_value)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(!self.as_ptr().is_null())] + #[ensures( + |result: &NonNull| + (result.as_ptr() as *const () as usize) == ((self.as_ptr() as *const () as usize) + count) + )] pub const unsafe fn byte_add(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same // safety contract. @@ -783,6 +793,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(!origin.as_ptr().is_null())] + #[ensures( + |result: &isize| + *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) + )] pub const unsafe fn byte_offset_from(self, origin: NonNull) -> isize { // SAFETY: the caller must uphold the safety contract for `byte_offset_from`. unsafe { self.pointer.byte_offset_from(origin.pointer) } @@ -1803,4 +1818,63 @@ 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::byte_add)] + pub fn non_null_byte_add_proof() { + const ARR_SIZE: usize = 100000; + let arr: [i32; ARR_SIZE] = kani::any(); + let offset = kani::any_where(|x| *x <= ARR_SIZE); + let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; + let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + let count: usize = kani::any(); + + kani::assume(count < usize::MAX); + kani::assume(count.checked_mul(mem::size_of::()).is_some()); + kani::assume(count * mem::size_of::() <= (isize::MAX as usize)); + kani::assume(count < ARR_SIZE - offset); + + unsafe { + let result = ptr.byte_add(count); + } + } + + #[kani::proof_for_contract(NonNull::byte_offset)] + pub fn non_null_byte_offset_proof() { + const ARR_SIZE: usize = 100000; + let arr: [i32; ARR_SIZE] = kani::any(); + let offset = kani::any_where(|x| *x <= ARR_SIZE); + let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; + let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + let count: isize = kani::any(); + + kani::assume(count >= isize::MIN); + kani::assume(count <= isize::MAX); + kani::assume(count.checked_mul(mem::size_of::() as isize).is_some()); + kani::assume(count * (mem::size_of::() as isize) <= (isize::MAX as isize)); + kani::assume((offset as isize + count) < (ARR_SIZE as isize)); + + unsafe { + let result = ptr.byte_offset(count); + } + } + + #[kani::proof_for_contract(NonNull::byte_offset_from)] + pub fn non_null_byte_offset_from_proof() { + const ARR_SIZE: usize = 100000; + let arr: [i32; ARR_SIZE] = kani::any(); + + // Randomly generate offsets for the pointers + let offset = kani::any_where(|x| *x < ARR_SIZE); + let origin_offset = kani::any_where(|x| *x < ARR_SIZE); + + let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; + let origin_ptr: *mut i32 = arr.as_ptr() as *mut i32; + + let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + let origin = unsafe { NonNull::new(origin_ptr.add(origin_offset)).unwrap() }; + + unsafe { + let result = ptr.byte_offset_from(origin); + } + } } From 009c561f7fbe83d0995650a860c60965ee6cbe2a Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 23 Oct 2024 14:59:32 -0700 Subject: [PATCH 02/15] remove redundant requires and add TODO --- 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 37dc25b77a46..89c1d70bad0f 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -502,7 +502,7 @@ 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(!origin.as_ptr().is_null())] + // TODO: add a require to check whether two pointer points to the same allocated object with `same_allocation` #[ensures( |result: &isize| *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) @@ -584,7 +584,7 @@ impl NonNull { #[rustc_allow_const_fn_unstable(set_ptr_value)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] - #[requires(!self.as_ptr().is_null())] + // TODO: add a require to check whether two pointer points to the same allocated object with `same_allocation` #[ensures( |result: &NonNull| (result.as_ptr() as *const () as usize) == ((self.as_ptr() as *const () as usize) + count) @@ -793,7 +793,7 @@ 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(!origin.as_ptr().is_null())] + // TODO: add a require to check whether two pointer points to the same allocated object with `same_allocation` #[ensures( |result: &isize| *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) From 3a986c54eec5d6a6984d41b232ff095e5b38ef2a Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 23 Oct 2024 18:23:45 -0700 Subject: [PATCH 03/15] fix error for byte_offset() --- library/core/src/ptr/non_null.rs | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 89c1d70bad0f..5cc47aad0084 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -503,10 +503,15 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] // TODO: add a require to check whether two pointer points to the same allocated object with `same_allocation` - #[ensures( - |result: &isize| - *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) - )] + #[ensures(|result: &Self| { + if (count >= 0) { + let offset_ptr = self.as_ptr().byte_add(count as usize) as *mut T; + result.as_ptr() == offset_ptr + } else { + let offset_ptr = self.as_ptr().byte_sub(-count as usize) as *mut T; + result.as_ptr() == offset_ptr + } + })] pub const unsafe fn byte_offset(self, count: isize) -> Self { // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has // the same safety contract. @@ -1800,6 +1805,7 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; + use crate::mem; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1864,8 +1870,8 @@ mod verify { let arr: [i32; ARR_SIZE] = kani::any(); // Randomly generate offsets for the pointers - let offset = kani::any_where(|x| *x < ARR_SIZE); - let origin_offset = kani::any_where(|x| *x < ARR_SIZE); + let offset = kani::any_where(|x| *x <= ARR_SIZE); + let origin_offset = kani::any_where(|x| *x <= ARR_SIZE); let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; let origin_ptr: *mut i32 = arr.as_ptr() as *mut i32; From fff0e6a13139239f17cf1e9b5f1f6e2220b41681 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 31 Oct 2024 22:58:48 -0700 Subject: [PATCH 04/15] add contracts with same_allocation --- library/core/src/ptr/non_null.rs | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 5cc47aad0084..23b3c6f2349f 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -502,8 +502,14 @@ 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")] - // TODO: add a require to check whether two pointer points to the same allocated object with `same_allocation` - #[ensures(|result: &Self| { + #[kani::requires( + if (count >= 0) { + kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_add(count as usize) as *const()) + } else { + kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_sub(-count as usize) as *const()) + } + )] + #[kani::ensures(|result: &Self| { if (count >= 0) { let offset_ptr = self.as_ptr().byte_add(count as usize) as *mut T; result.as_ptr() == offset_ptr @@ -589,8 +595,11 @@ impl NonNull { #[rustc_allow_const_fn_unstable(set_ptr_value)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] - // TODO: add a require to check whether two pointer points to the same allocated object with `same_allocation` - #[ensures( + #[kani::requires(kani::mem::same_allocation( + self.as_ptr() as *const(), + ((self.as_ptr() as *const () as usize) + count) as *const() + ))] + #[kani::ensures( |result: &NonNull| (result.as_ptr() as *const () as usize) == ((self.as_ptr() as *const () as usize) + count) )] @@ -798,8 +807,8 @@ 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")] - // TODO: add a require to check whether two pointer points to the same allocated object with `same_allocation` - #[ensures( + #[kani::requires(kani::mem::same_allocation(self.as_ptr() as *const(), origin.as_ptr() as *const()))] + #[kani::ensures( |result: &isize| *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) )] @@ -1837,7 +1846,6 @@ mod verify { kani::assume(count < usize::MAX); kani::assume(count.checked_mul(mem::size_of::()).is_some()); kani::assume(count * mem::size_of::() <= (isize::MAX as usize)); - kani::assume(count < ARR_SIZE - offset); unsafe { let result = ptr.byte_add(count); @@ -1857,8 +1865,6 @@ mod verify { kani::assume(count <= isize::MAX); kani::assume(count.checked_mul(mem::size_of::() as isize).is_some()); kani::assume(count * (mem::size_of::() as isize) <= (isize::MAX as isize)); - kani::assume((offset as isize + count) < (ARR_SIZE as isize)); - unsafe { let result = ptr.byte_offset(count); } From 7ce2d89b8c54e876c905485d89b2609c552c1366 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 4 Nov 2024 16:03:36 -0800 Subject: [PATCH 05/15] simplify contract for byte_offset --- library/core/src/ptr/non_null.rs | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 23b3c6f2349f..4f489254efd2 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -502,22 +502,8 @@ 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")] - #[kani::requires( - if (count >= 0) { - kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_add(count as usize) as *const()) - } else { - kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_sub(-count as usize) as *const()) - } - )] - #[kani::ensures(|result: &Self| { - if (count >= 0) { - let offset_ptr = self.as_ptr().byte_add(count as usize) as *mut T; - result.as_ptr() == offset_ptr - } else { - let offset_ptr = self.as_ptr().byte_sub(-count as usize) as *mut T; - result.as_ptr() == offset_ptr - } - })] + #[kani::requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const()))] + #[kani::ensures(|result: &Self| result.as_ptr() == self.as_ptr().byte_offset(count))] pub const unsafe fn byte_offset(self, count: isize) -> Self { // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has // the same safety contract. From 459a692ff7f275ba51526132c0364673d211c7c2 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 4 Nov 2024 16:42:50 -0800 Subject: [PATCH 06/15] refactor proof harness with pointer generator for byte_offset_from --- library/core/src/ptr/non_null.rs | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4f489254efd2..d42250708364 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1858,21 +1858,28 @@ mod verify { #[kani::proof_for_contract(NonNull::byte_offset_from)] pub fn non_null_byte_offset_from_proof() { - const ARR_SIZE: usize = 100000; - let arr: [i32; ARR_SIZE] = kani::any(); + use kani::PointerGenerator; + const SIZE: usize = mem::size_of::(); + let mut generator1 = PointerGenerator::::new(); + let mut generator2 = PointerGenerator::::new(); - // Randomly generate offsets for the pointers - let offset = kani::any_where(|x| *x <= ARR_SIZE); - let origin_offset = kani::any_where(|x| *x <= ARR_SIZE); + 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 raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; - let origin_ptr: *mut i32 = arr.as_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 = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; - let origin = unsafe { NonNull::new(origin_ptr.add(origin_offset)).unwrap() }; + let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() }; + let origin_nonnull = unsafe { NonNull::new(origin).unwrap() }; unsafe { - let result = ptr.byte_offset_from(origin); + let result = ptr_nonnull.byte_offset_from(origin_nonnull); } } } From 670adefdb7f5133be0f5b05bfaea639a2f358bb6 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 7 Nov 2024 20:32:58 -0800 Subject: [PATCH 07/15] update code based on comments --- library/core/src/ptr/non_null.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index d42250708364..2f6780c39f42 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1829,7 +1829,6 @@ mod verify { let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; let count: usize = kani::any(); - kani::assume(count < usize::MAX); kani::assume(count.checked_mul(mem::size_of::()).is_some()); kani::assume(count * mem::size_of::() <= (isize::MAX as usize)); @@ -1847,8 +1846,6 @@ mod verify { let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; let count: isize = kani::any(); - kani::assume(count >= isize::MIN); - kani::assume(count <= isize::MAX); kani::assume(count.checked_mul(mem::size_of::() as isize).is_some()); kani::assume(count * (mem::size_of::() as isize) <= (isize::MAX as isize)); unsafe { @@ -1859,7 +1856,7 @@ mod verify { #[kani::proof_for_contract(NonNull::byte_offset_from)] pub fn non_null_byte_offset_from_proof() { use kani::PointerGenerator; - const SIZE: usize = mem::size_of::(); + const SIZE: usize = mem::size_of::() * 10; let mut generator1 = PointerGenerator::::new(); let mut generator2 = PointerGenerator::::new(); From e6c6795374bb7ef098ab16206d8e52388d285c8b Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 12 Nov 2024 23:20:49 -0800 Subject: [PATCH 08/15] update contracts --- library/core/src/ptr/non_null.rs | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 2f6780c39f42..8d042c30a6da 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -502,7 +502,12 @@ 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")] - #[kani::requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const()))] + #[kani::requires( + count <= isize::MAX && + count <= isize::MIN && + (self.as_ptr().addr() as isize).checked_add(count).is_some() && + kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const()) + )] #[kani::ensures(|result: &Self| result.as_ptr() == self.as_ptr().byte_offset(count))] pub const unsafe fn byte_offset(self, count: isize) -> Self { // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has @@ -581,13 +586,14 @@ impl NonNull { #[rustc_allow_const_fn_unstable(set_ptr_value)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] - #[kani::requires(kani::mem::same_allocation( - self.as_ptr() as *const(), - ((self.as_ptr() as *const () as usize) + count) as *const() - ))] + #[kani::requires( + count <= (isize::MAX as usize) && + self.as_ptr().addr().checked_add(count).is_some() && + kani::mem::same_allocation(self.as_ptr() as *const(),((self.as_ptr().addr()) + count) as *const()) + )] #[kani::ensures( |result: &NonNull| - (result.as_ptr() as *const () as usize) == ((self.as_ptr() as *const () as usize) + count) + result.as_ptr().addr() == (self.as_ptr().addr() + count) )] pub const unsafe fn byte_add(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same @@ -1801,6 +1807,7 @@ mod verify { use super::*; use crate::ptr::null_mut; use crate::mem; + use kani::PointerGenerator; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1829,9 +1836,6 @@ mod verify { let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; let count: usize = kani::any(); - kani::assume(count.checked_mul(mem::size_of::()).is_some()); - kani::assume(count * mem::size_of::() <= (isize::MAX as usize)); - unsafe { let result = ptr.byte_add(count); } @@ -1846,8 +1850,6 @@ mod verify { let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; let count: isize = kani::any(); - kani::assume(count.checked_mul(mem::size_of::() as isize).is_some()); - kani::assume(count * (mem::size_of::() as isize) <= (isize::MAX as isize)); unsafe { let result = ptr.byte_offset(count); } @@ -1855,7 +1857,6 @@ mod verify { #[kani::proof_for_contract(NonNull::byte_offset_from)] pub fn non_null_byte_offset_from_proof() { - use kani::PointerGenerator; const SIZE: usize = mem::size_of::() * 10; let mut generator1 = PointerGenerator::::new(); let mut generator2 = PointerGenerator::::new(); From 293d9c88c6bcd4e8202ca20d6b569f805293f408 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 13 Nov 2024 14:24:32 -0800 Subject: [PATCH 09/15] remove unnecessary preconditions --- library/core/src/ptr/non_null.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 8d042c30a6da..0b9bfcb26d6e 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -503,8 +503,6 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[kani::requires( - count <= isize::MAX && - count <= isize::MIN && (self.as_ptr().addr() as isize).checked_add(count).is_some() && kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const()) )] @@ -587,7 +585,6 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[kani::requires( - count <= (isize::MAX as usize) && self.as_ptr().addr().checked_add(count).is_some() && kani::mem::same_allocation(self.as_ptr() as *const(),((self.as_ptr().addr()) + count) as *const()) )] From 40b3833e66ad0aa7d271bb39c3a19b7e8ce23323 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Wed, 13 Nov 2024 19:44:02 -0800 Subject: [PATCH 10/15] fix comment issues --- library/core/src/ptr/non_null.rs | 35 ++++++++++++++++---------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 0b9bfcb26d6e..6da30620300e 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -502,11 +502,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")] - #[kani::requires( + #[requires( (self.as_ptr().addr() as isize).checked_add(count).is_some() && kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const()) )] - #[kani::ensures(|result: &Self| result.as_ptr() == self.as_ptr().byte_offset(count))] + #[ensures(|result: &Self| result.as_ptr() == self.as_ptr().wrapping_byte_offset(count))] pub const unsafe fn byte_offset(self, count: isize) -> Self { // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has // the same safety contract. @@ -584,11 +584,12 @@ impl NonNull { #[rustc_allow_const_fn_unstable(set_ptr_value)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] - #[kani::requires( + #[requires( + count <= (isize::MAX as usize) && self.as_ptr().addr().checked_add(count).is_some() && kani::mem::same_allocation(self.as_ptr() as *const(),((self.as_ptr().addr()) + count) as *const()) )] - #[kani::ensures( + #[ensures( |result: &NonNull| result.as_ptr().addr() == (self.as_ptr().addr() + count) )] @@ -796,8 +797,8 @@ 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")] - #[kani::requires(kani::mem::same_allocation(self.as_ptr() as *const(), origin.as_ptr() as *const()))] - #[kani::ensures( + #[requires(kani::mem::same_allocation(self.as_ptr() as *const(), origin.as_ptr() as *const()))] + #[ensures( |result: &isize| *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) )] @@ -1826,35 +1827,35 @@ mod verify { #[kani::proof_for_contract(NonNull::byte_add)] pub fn non_null_byte_add_proof() { - const ARR_SIZE: usize = 100000; - let arr: [i32; ARR_SIZE] = kani::any(); - let offset = kani::any_where(|x| *x <= ARR_SIZE); - let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; - let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + const ARR_SIZE: usize = mem::size_of::() * 1000; + let mut generator = PointerGenerator::::new(); + let count: usize = kani::any(); + let raw_ptr: *mut i32 = generator.any_in_bounds().ptr as *mut i32; unsafe { + let ptr = NonNull::new(raw_ptr).unwrap(); let result = ptr.byte_add(count); } } #[kani::proof_for_contract(NonNull::byte_offset)] pub fn non_null_byte_offset_proof() { - const ARR_SIZE: usize = 100000; - let arr: [i32; ARR_SIZE] = kani::any(); - let offset = kani::any_where(|x| *x <= ARR_SIZE); - let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; - let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + const ARR_SIZE: usize = mem::size_of::() * 1000; + let mut generator = PointerGenerator::::new(); + let count: isize = kani::any(); + let raw_ptr: *mut i32 = generator.any_in_bounds().ptr as *mut i32; unsafe { + let ptr = NonNull::new(raw_ptr).unwrap(); let result = ptr.byte_offset(count); } } #[kani::proof_for_contract(NonNull::byte_offset_from)] pub fn non_null_byte_offset_from_proof() { - const SIZE: usize = mem::size_of::() * 10; + const SIZE: usize = mem::size_of::() * 1000; let mut generator1 = PointerGenerator::::new(); let mut generator2 = PointerGenerator::::new(); From 16bf41929344f6c96c5b1e907c54242f414731db Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Fri, 15 Nov 2024 14:18:00 -0800 Subject: [PATCH 11/15] adjust the usage of pointer generator --- library/core/src/ptr/non_null.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index fc47f811264c..140a587d14f5 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -2173,11 +2173,7 @@ mod verify { let mut generator1 = PointerGenerator::::new(); let mut generator2 = 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 ptr: *mut i32 = generator1.any_in_bounds().ptr as *mut i32; let origin: *mut i32 = if kani::any() { generator1.any_in_bounds().ptr as *mut i32 From 8451bcb4fee20ae0aad030c8f635a6910c590aba Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Fri, 15 Nov 2024 14:42:19 -0800 Subject: [PATCH 12/15] unify contracts --- 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 140a587d14f5..87d6cbb86ab9 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -531,7 +531,7 @@ impl NonNull { #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires( (self.as_ptr().addr() as isize).checked_add(count).is_some() && - kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_offset(count) as *const()) + kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_byte_offset(count)) )] #[ensures(|result: &Self| result.as_ptr() == self.as_ptr().wrapping_byte_offset(count))] pub const unsafe fn byte_offset(self, count: isize) -> Self { @@ -618,11 +618,11 @@ impl NonNull { #[requires( count <= (isize::MAX as usize) && self.as_ptr().addr().checked_add(count).is_some() && - kani::mem::same_allocation(self.as_ptr() as *const(),((self.as_ptr().addr()) + count) as *const()) + kani::mem::same_allocation(self.as_ptr(),self.as_ptr().wrapping_byte_add(count)) )] #[ensures( |result: &NonNull| - result.as_ptr().addr() == (self.as_ptr().addr() + count) + result.as_ptr() == self.as_ptr().wrapping_byte_add(count) )] pub const unsafe fn byte_add(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same From 98a196a6cf0d7e9ac78859ef65a36ffff15e98f9 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Fri, 15 Nov 2024 16:07:49 -0800 Subject: [PATCH 13/15] fix overflow fail case --- library/core/src/ptr/non_null.rs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 87d6cbb86ab9..5b8787b93a6b 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -616,13 +616,8 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires( - count <= (isize::MAX as usize) && - self.as_ptr().addr().checked_add(count).is_some() && - kani::mem::same_allocation(self.as_ptr(),self.as_ptr().wrapping_byte_add(count)) - )] - #[ensures( - |result: &NonNull| - result.as_ptr() == self.as_ptr().wrapping_byte_add(count) + count <= (isize::MAX as usize) - self.as_ptr().addr() && // Ensure the offset doesn't overflow + kani::mem::same_allocation(self.as_ptr(),self.as_ptr().wrapping_byte_add(count)) // Ensure the offset is within the same allocation )] pub const unsafe fn byte_add(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same From 7c7ae14e7e31011210379a96253fbdecb6f265b2 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 2 Dec 2024 15:46:43 -0800 Subject: [PATCH 14/15] dangling pointer verification --- library/core/src/ptr/non_null.rs | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 932b1d325fe7..4e61b6ec8561 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -620,7 +620,7 @@ impl NonNull { #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires( count <= (isize::MAX as usize) - self.as_ptr().addr() && // Ensure the offset doesn't overflow - kani::mem::same_allocation(self.as_ptr(),self.as_ptr().wrapping_byte_add(count)) // Ensure the offset is within the same allocation + (count == 0 || kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_byte_add(count))) // Ensure the offset is within the same allocation )] pub const unsafe fn byte_add(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same @@ -835,7 +835,10 @@ 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() as *const(), origin.as_ptr() as *const()))] + #[requires( + self.as_ptr().addr() == origin.as_ptr().addr() || + kani::mem::same_allocation(self.as_ptr() as *const(), origin.as_ptr() as *const()) + )] #[ensures( |result: &isize| *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8) @@ -2503,6 +2506,14 @@ mod verify { } } + #[kani::proof_for_contract(NonNull::byte_add)] + pub fn non_null_byte_add_dangling_proof() { + let ptr = NonNull::::dangling(); + unsafe { + let _ = ptr.byte_add(0); + } + } + #[kani::proof_for_contract(NonNull::byte_offset)] pub fn non_null_byte_offset_proof() { const ARR_SIZE: usize = mem::size_of::() * 1000; @@ -2538,4 +2549,13 @@ mod verify { let result = ptr_nonnull.byte_offset_from(origin_nonnull); } } + + #[kani::proof_for_contract(NonNull::byte_offset_from)] + pub fn non_null_byte_offset_from_dangling_proof() { + let origin = NonNull::::dangling(); + let ptr = origin; + unsafe { + let _ = ptr.byte_offset_from(origin); + } + } } From 0f1c6d3821e8a1983ad212ec1e5d6a538c2ca4dc Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 2 Dec 2024 22:20:51 -0800 Subject: [PATCH 15/15] comment --- library/core/src/ptr/non_null.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 7575d5a1c247..60e1ef93bc47 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -2321,6 +2321,8 @@ mod verify { #[kani::proof_for_contract(NonNull::byte_add)] pub fn non_null_byte_add_proof() { + // Make size as 1000 to ensure the array is large enough to cover various senarios + // while maintaining a reasonable proof runtime const ARR_SIZE: usize = mem::size_of::() * 1000; let mut generator = PointerGenerator::::new();