From b205735729b843059657905860b74aea5018313f Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 24 Oct 2024 21:42:00 -0700 Subject: [PATCH 01/15] fix error for NonNull::replace --- library/core/src/ptr/non_null.rs | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915dbf..ed8a3375308b8 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}; #[cfg(kani)] use crate::kani; @@ -1100,6 +1100,9 @@ impl NonNull { /// [`ptr::replace`]: crate::ptr::replace() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(!self.as_ptr().is_null())] // Pointer must not be null or some cases will fail + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure valid pointer + #[kani::ensures(|ret: &T| core::mem::needs_drop::() == false)] // No drop should occur pub unsafe fn replace(self, src: T) -> T where T: Sized, @@ -1803,4 +1806,20 @@ 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::replace)] + pub fn non_null_check_replace() { + let mut x: i32 = kani::any(); + let mut y: i32 = kani::any(); + + let origin_ptr = NonNull::new(x as *mut i32).unwrap(); + unsafe { + let captured_original = ptr::read(origin_ptr.as_ptr()); + let replaced = origin_ptr.replace(y); + let after_replace = ptr::read(origin_ptr.as_ptr()); + + kani::assume(replaced == x); + kani::assume(after_replace == y) + } + } } From ce4ff30c11873f1a32ac067c65b889fcf9bea126 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 28 Oct 2024 17:28:35 -0700 Subject: [PATCH 02/15] checkpoint --- library/core/src/ptr/non_null.rs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index ed8a3375308b8..19e19a6e2de47 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1822,4 +1822,15 @@ mod verify { kani::assume(after_replace == y) } } + + #[kani::proof_for_contract(NonNull::drop_in_place)] + pub fn non_null_check_drop_in_place() { + 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 { + ptr.drop_in_place(); + } + } + } } From 8ab7dce918d71c1f0950056511a09bf2a10c1221 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 29 Oct 2024 22:08:47 -0700 Subject: [PATCH 03/15] contract for drop_in_place --- library/core/src/ptr/non_null.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 19e19a6e2de47..2c07187793b0b 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1009,6 +1009,7 @@ impl NonNull { /// [`ptr::drop_in_place`]: crate::ptr::drop_in_place() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] + #[ensures(|result| ub_checks::can_dereference(result))] pub unsafe fn drop_in_place(self) { // SAFETY: the caller must uphold the safety contract for `drop_in_place`. unsafe { ptr::drop_in_place(self.as_ptr()) } From 1b6f50d0c1a7fdb98836a1ac81a201febfed373c Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 29 Oct 2024 22:50:47 -0700 Subject: [PATCH 04/15] complete condition for replace() --- library/core/src/ptr/non_null.rs | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 2c07187793b0b..d4bf21413f708 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1101,8 +1101,8 @@ impl NonNull { /// [`ptr::replace`]: crate::ptr::replace() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] - #[requires(!self.as_ptr().is_null())] // Pointer must not be null or some cases will fail #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure valid pointer + #[requires(ub_checks::can_dereference(&src))] // Ensure valid source #[kani::ensures(|ret: &T| core::mem::needs_drop::() == false)] // No drop should occur pub unsafe fn replace(self, src: T) -> T where @@ -1812,15 +1812,18 @@ mod verify { pub fn non_null_check_replace() { let mut x: i32 = kani::any(); let mut y: i32 = kani::any(); + kani::assume((&y as *const i32) != core::ptr::null()); - let origin_ptr = NonNull::new(x as *mut i32).unwrap(); - unsafe { - let captured_original = ptr::read(origin_ptr.as_ptr()); - let replaced = origin_ptr.replace(y); - let after_replace = ptr::read(origin_ptr.as_ptr()); + if let Some(origin_ptr) = NonNull::new(&mut x as *mut i32) { + kani::assume(origin_ptr.as_ptr().align_offset(core::mem::align_of::()) == 0); + unsafe { + let captured_original = ptr::read(origin_ptr.as_ptr()); + let replaced = origin_ptr.replace(y); + let after_replace = ptr::read(origin_ptr.as_ptr()); - kani::assume(replaced == x); - kani::assume(after_replace == y) + kani::assume(replaced == x); + kani::assume(after_replace == y) + } } } From 355520878b0ad585e92d1f63c371a3199b409b57 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 29 Oct 2024 23:16:19 -0700 Subject: [PATCH 05/15] basic verification for swap() --- library/core/src/ptr/non_null.rs | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index d4bf21413f708..82adf9f3ca7f5 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1122,6 +1122,11 @@ impl NonNull { #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_swap", issue = "83163")] + #[requires(self.as_ptr() != with.as_ptr())] + #[requires(self.as_ptr().align_offset(core::mem::align_of::()) == 0)] + #[requires(with.as_ptr().align_offset(core::mem::align_of::()) == 0)] + #[requires(ub_checks::can_dereference(self.as_ptr()))] + #[requires(ub_checks::can_dereference(with.as_ptr()))] pub const unsafe fn swap(self, with: NonNull) where T: Sized, @@ -1837,4 +1842,24 @@ mod verify { } } } + + #[kani::proof_for_contract(NonNull::swap)] + pub fn non_null_check_swap() { + let mut a: i32 = kani::any(); + let mut b: i32 = kani::any(); + + let ptr_a = NonNull::new(&mut a as *mut i32).unwrap(); + let ptr_b = NonNull::new(&mut b as *mut i32).unwrap(); + + unsafe { + let old_a = ptr::read(ptr_a.as_ptr()); + let old_b = ptr::read(ptr_b.as_ptr()); + ptr_a.swap(ptr_b); + // Verify that the values have been swapped. + let new_a = ptr::read(ptr_a.as_ptr()); + let new_b = ptr::read(ptr_b.as_ptr()); + kani::assume(old_a == new_b); + kani::assume(old_b == new_a); + } + } } From 9606e2ed2650de9911abde92a18ae59353948b69 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 31 Oct 2024 22:23:28 -0700 Subject: [PATCH 06/15] add modifies to apis --- library/core/src/ptr/non_null.rs | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 82adf9f3ca7f5..f02158e374d7c 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1009,7 +1009,7 @@ impl NonNull { /// [`ptr::drop_in_place`]: crate::ptr::drop_in_place() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] - #[ensures(|result| ub_checks::can_dereference(result))] + #[kani::ensures(|result| ub_checks::can_dereference(result))] pub unsafe fn drop_in_place(self) { // SAFETY: the caller must uphold the safety contract for `drop_in_place`. unsafe { ptr::drop_in_place(self.as_ptr()) } @@ -1101,8 +1101,9 @@ impl NonNull { /// [`ptr::replace`]: crate::ptr::replace() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] - #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure valid pointer - #[requires(ub_checks::can_dereference(&src))] // Ensure valid source + #[kani::modifies(self.as_ptr())] + #[kani::requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure valid pointer + #[kani::requires(ub_checks::can_dereference(&src))] // Ensure valid source #[kani::ensures(|ret: &T| core::mem::needs_drop::() == false)] // No drop should occur pub unsafe fn replace(self, src: T) -> T where @@ -1122,11 +1123,9 @@ impl NonNull { #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_swap", issue = "83163")] - #[requires(self.as_ptr() != with.as_ptr())] - #[requires(self.as_ptr().align_offset(core::mem::align_of::()) == 0)] - #[requires(with.as_ptr().align_offset(core::mem::align_of::()) == 0)] - #[requires(ub_checks::can_dereference(self.as_ptr()))] - #[requires(ub_checks::can_dereference(with.as_ptr()))] + #[kani::modifies(self.as_ptr(), with.as_ptr())] + #[kani::requires(ub_checks::can_dereference(self.as_ptr()))] + #[kani::requires(ub_checks::can_dereference(with.as_ptr()))] pub const unsafe fn swap(self, with: NonNull) where T: Sized, @@ -1820,7 +1819,7 @@ mod verify { kani::assume((&y as *const i32) != core::ptr::null()); if let Some(origin_ptr) = NonNull::new(&mut x as *mut i32) { - kani::assume(origin_ptr.as_ptr().align_offset(core::mem::align_of::()) == 0); + kani::assume(origin_ptr.as_ptr().is_aligned()); unsafe { let captured_original = ptr::read(origin_ptr.as_ptr()); let replaced = origin_ptr.replace(y); @@ -1836,7 +1835,7 @@ mod verify { pub fn non_null_check_drop_in_place() { 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); + kani::assume(ptr.as_ptr().is_aligned()); unsafe { ptr.drop_in_place(); } From e4fb14bf2bed9edba25d8a7f92ae581c8c6f6050 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 11 Nov 2024 19:58:32 -0800 Subject: [PATCH 07/15] update function contracts --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index f02158e374d7c..c4772546f9fb6 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)] use crate::kani; From 0202bcfbfa42c09a7067304b5cd2c7325c29bdbf Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 11 Nov 2024 19:58:50 -0800 Subject: [PATCH 08/15] update function contracts --- library/core/src/ptr/non_null.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index c4772546f9fb6..9f9d4ff96f2d5 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1009,7 +1009,8 @@ impl NonNull { /// [`ptr::drop_in_place`]: crate::ptr::drop_in_place() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] - #[kani::ensures(|result| ub_checks::can_dereference(result))] + #[kani::requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure self is aligned, initialized, and valid for read + #[kani::requires(ub_checks::can_write(self.as_ptr() as *mut()))] // Ensure self is valid for write pub unsafe fn drop_in_place(self) { // SAFETY: the caller must uphold the safety contract for `drop_in_place`. unsafe { ptr::drop_in_place(self.as_ptr()) } @@ -1102,9 +1103,8 @@ impl NonNull { #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[kani::modifies(self.as_ptr())] - #[kani::requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure valid pointer - #[kani::requires(ub_checks::can_dereference(&src))] // Ensure valid source - #[kani::ensures(|ret: &T| core::mem::needs_drop::() == false)] // No drop should occur + #[kani::requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is aligned, initialized, and valid for read + #[kani::requires(ub_checks::can_write(self.as_ptr()))] // Ensure self is valid for write pub unsafe fn replace(self, src: T) -> T where T: Sized, @@ -1124,8 +1124,8 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_swap", issue = "83163")] #[kani::modifies(self.as_ptr(), with.as_ptr())] - #[kani::requires(ub_checks::can_dereference(self.as_ptr()))] - #[kani::requires(ub_checks::can_dereference(with.as_ptr()))] + #[kani::requires(ub_checks::can_dereference(self.as_ptr()) && ub_checks::can_write(self.as_ptr()))] + #[kani::requires(ub_checks::can_dereference(with.as_ptr()) && ub_checks::can_write(with.as_ptr()))] pub const unsafe fn swap(self, with: NonNull) where T: Sized, From 7c5c0e895e2f5152b64a1cf40c395b5a9cd36598 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Mon, 11 Nov 2024 21:02:26 -0800 Subject: [PATCH 09/15] replace unnecessary assume with assert --- library/core/src/ptr/non_null.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 9f9d4ff96f2d5..23feffa79efd7 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1819,14 +1819,15 @@ mod verify { kani::assume((&y as *const i32) != core::ptr::null()); if let Some(origin_ptr) = NonNull::new(&mut x as *mut i32) { + // let origin_ptr = NonNull::new(x as *mut i32).unwrap(); kani::assume(origin_ptr.as_ptr().is_aligned()); unsafe { let captured_original = ptr::read(origin_ptr.as_ptr()); let replaced = origin_ptr.replace(y); let after_replace = ptr::read(origin_ptr.as_ptr()); - kani::assume(replaced == x); - kani::assume(after_replace == y) + assert_eq!(captured_original, replaced); + assert_eq!(after_replace, y) } } } @@ -1857,8 +1858,8 @@ mod verify { // Verify that the values have been swapped. let new_a = ptr::read(ptr_a.as_ptr()); let new_b = ptr::read(ptr_b.as_ptr()); - kani::assume(old_a == new_b); - kani::assume(old_b == new_a); + assert_eq!(old_a, new_b); + assert_eq!(old_b, new_a); } } } From 02a7130ff0ab2d657570af031fdae244586688af Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 12 Nov 2024 16:20:29 -0800 Subject: [PATCH 10/15] remove some redundant condition --- library/core/src/ptr/non_null.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 23feffa79efd7..64d0d7b929a4f 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1816,7 +1816,6 @@ mod verify { pub fn non_null_check_replace() { let mut x: i32 = kani::any(); let mut y: i32 = kani::any(); - kani::assume((&y as *const i32) != core::ptr::null()); if let Some(origin_ptr) = NonNull::new(&mut x as *mut i32) { // let origin_ptr = NonNull::new(x as *mut i32).unwrap(); @@ -1836,7 +1835,6 @@ mod verify { pub fn non_null_check_drop_in_place() { let mut x: i32 = kani::any(); if let Some(ptr) = NonNull::new(&mut x as *mut i32) { - kani::assume(ptr.as_ptr().is_aligned()); unsafe { ptr.drop_in_place(); } From 93df6a43f6c686610f1288ab08f1774a826eaac5 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 12 Nov 2024 16:23:10 -0800 Subject: [PATCH 11/15] remove some redundant condition --- library/core/src/ptr/non_null.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 64d0d7b929a4f..67929cabb907c 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1819,7 +1819,6 @@ mod verify { if let Some(origin_ptr) = NonNull::new(&mut x as *mut i32) { // let origin_ptr = NonNull::new(x as *mut i32).unwrap(); - kani::assume(origin_ptr.as_ptr().is_aligned()); unsafe { let captured_original = ptr::read(origin_ptr.as_ptr()); let replaced = origin_ptr.replace(y); From 69428d646613d5ad91bedc6a9d4880b167622376 Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Thu, 14 Nov 2024 20:31:12 -0800 Subject: [PATCH 12/15] adjust ptr created based on comment --- library/core/src/ptr/non_null.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index c196e70a0eee1..a183ca3c5d030 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1932,8 +1932,8 @@ mod verify { let mut x: i32 = kani::any(); let mut y: i32 = kani::any(); - if let Some(origin_ptr) = NonNull::new(&mut x as *mut i32) { - // let origin_ptr = NonNull::new(x as *mut i32).unwrap(); + if let nonnull_origin_ptr = NonNull::new(&mut x as *mut i32) { + let origin_ptr = nonnull_origin_ptr.unwrap(); unsafe { let captured_original = ptr::read(origin_ptr.as_ptr()); let replaced = origin_ptr.replace(y); @@ -1948,7 +1948,8 @@ mod verify { #[kani::proof_for_contract(NonNull::drop_in_place)] pub fn non_null_check_drop_in_place() { let mut x: i32 = kani::any(); - if let Some(ptr) = NonNull::new(&mut x as *mut i32) { + if let nonnull_ptr = NonNull::new(&mut x as *mut i32) { + let ptr = nonnull_ptr.unwrap(); unsafe { ptr.drop_in_place(); } From c00fc7125736c9cebe322df46196753a0cc5611d Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Fri, 15 Nov 2024 10:51:35 -0800 Subject: [PATCH 13/15] update proof harness --- library/core/src/ptr/non_null.rs | 35 ++++++++++++++++++-------------- 1 file changed, 20 insertions(+), 15 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index a183ca3c5d030..e0df1c4dafb87 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1932,28 +1932,33 @@ mod verify { let mut x: i32 = kani::any(); let mut y: i32 = kani::any(); - if let nonnull_origin_ptr = NonNull::new(&mut x as *mut i32) { - let origin_ptr = nonnull_origin_ptr.unwrap(); - unsafe { - let captured_original = ptr::read(origin_ptr.as_ptr()); - let replaced = origin_ptr.replace(y); - let after_replace = ptr::read(origin_ptr.as_ptr()); - - assert_eq!(captured_original, replaced); - assert_eq!(after_replace, y) - } + let origin_ptr = NonNull::new(&mut x as *mut i32).unwrap(); + unsafe { + let captured_original = ptr::read(origin_ptr.as_ptr()); + let replaced = origin_ptr.replace(y); + let after_replace = ptr::read(origin_ptr.as_ptr()); + + assert_eq!(captured_original, replaced); + assert_eq!(after_replace, y) } } #[kani::proof_for_contract(NonNull::drop_in_place)] pub fn non_null_check_drop_in_place() { - let mut x: i32 = kani::any(); - if let nonnull_ptr = NonNull::new(&mut x as *mut i32) { - let ptr = nonnull_ptr.unwrap(); - unsafe { - ptr.drop_in_place(); + struct Droppable { + value: i32, + } + + impl Drop for Droppable { + fn drop(&mut self) { } } + + let mut droppable = Droppable { value: kani::any() }; + let ptr = NonNull::new(&mut droppable as *mut Droppable).unwrap(); + unsafe { + ptr.drop_in_place(); + } } #[kani::proof_for_contract(NonNull::swap)] From 91b4300a77ff23ead732cea95234eb77901b4a7a Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Fri, 15 Nov 2024 11:19:41 -0800 Subject: [PATCH 14/15] use safty requires and ensures --- library/core/src/ptr/non_null.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4ad7b0dda1cfb..c8e07d2639bca 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1051,8 +1051,8 @@ impl NonNull { /// [`ptr::drop_in_place`]: crate::ptr::drop_in_place() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] - #[kani::requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure self is aligned, initialized, and valid for read - #[kani::requires(ub_checks::can_write(self.as_ptr() as *mut()))] // Ensure self is valid for write + #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure self is aligned, initialized, and valid for read + #[requires(ub_checks::can_write(self.as_ptr() as *mut()))] // Ensure self is valid for write pub unsafe fn drop_in_place(self) { // SAFETY: the caller must uphold the safety contract for `drop_in_place`. unsafe { ptr::drop_in_place(self.as_ptr()) } @@ -1145,8 +1145,8 @@ impl NonNull { #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[kani::modifies(self.as_ptr())] - #[kani::requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is aligned, initialized, and valid for read - #[kani::requires(ub_checks::can_write(self.as_ptr()))] // Ensure self is valid for write + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is aligned, initialized, and valid for read + #[requires(ub_checks::can_write(self.as_ptr()))] // Ensure self is valid for write pub unsafe fn replace(self, src: T) -> T where T: Sized, @@ -1166,8 +1166,8 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_swap", issue = "83163")] #[kani::modifies(self.as_ptr(), with.as_ptr())] - #[kani::requires(ub_checks::can_dereference(self.as_ptr()) && ub_checks::can_write(self.as_ptr()))] - #[kani::requires(ub_checks::can_dereference(with.as_ptr()) && ub_checks::can_write(with.as_ptr()))] + #[requires(ub_checks::can_dereference(self.as_ptr()) && ub_checks::can_write(self.as_ptr()))] + #[requires(ub_checks::can_dereference(with.as_ptr()) && ub_checks::can_write(with.as_ptr()))] pub const unsafe fn swap(self, with: NonNull) where T: Sized, From 40491cccd2cf9a4ef444e7548e7f10a217e51dbe Mon Sep 17 00:00:00 2001 From: Daniel Tu Date: Tue, 19 Nov 2024 15:18:00 -0800 Subject: [PATCH 15/15] 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 180e62cb66970..4834c8009ec44 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1152,7 +1152,7 @@ impl NonNull { /// [`ptr::replace`]: crate::ptr::replace() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] - #[kani::modifies(self.as_ptr())] + #[cfg_attr(kani, kani::modifies(self.as_ptr()))] #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is aligned, initialized, and valid for read #[requires(ub_checks::can_write(self.as_ptr()))] // Ensure self is valid for write pub unsafe fn replace(self, src: T) -> T @@ -1173,7 +1173,7 @@ impl NonNull { #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_swap", issue = "83163")] - #[kani::modifies(self.as_ptr(), with.as_ptr())] + #[cfg_attr(kani, kani::modifies(self.as_ptr(), with.as_ptr()))] #[requires(ub_checks::can_dereference(self.as_ptr()) && ub_checks::can_write(self.as_ptr()))] #[requires(ub_checks::can_dereference(with.as_ptr()) && ub_checks::can_write(with.as_ptr()))] pub const unsafe fn swap(self, with: NonNull)