Contracts & Harnesses for swap, replace, and drop_in_place

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;
@@ -1009,6 +1009,7 @@ impl<T: ?Sized> NonNull<T> {
     /// [`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))]
     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()) }
@@ -1100,6 +1101,10 @@ impl<T: ?Sized> NonNull<T> {
     /// [`ptr::replace`]: crate::ptr::replace()
     #[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::<T>() == false)]  // No drop should occur
     pub unsafe fn replace(self, src: T) -> T
     where
         T: Sized,
@@ -1118,6 +1123,9 @@ impl<T: ?Sized> NonNull<T> {
     #[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())]
+    #[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<T>)
     where
         T: Sized,
@@ -1803,4 +1811,54 @@ 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();
+        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().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)
+            }
+        }
+    }
+
+    #[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().is_aligned());
+            unsafe {
+                ptr.drop_in_place();
+            }
+        }
+    }
+
+    #[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);
+        }
+    }
 }