Contracts & Harnesses for write_volatile

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)]
@@ -1064,6 +1065,8 @@ impl<T: ?Sized> NonNull<T> {
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[kani::modifies(self.as_ptr())]
+    #[requires(ub_checks::can_write(self.as_ptr()))]
     pub unsafe fn write_volatile(self, val: T)
     where
         T: Sized,
@@ -1803,4 +1806,28 @@ 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::write_volatile)]
+    pub fn non_null_check_write_volatile() {
+        // Create a pointer generator for a single integer
+        let mut generator = kani::PointerGenerator::<4>::new();
+
+        // Get a raw pointer from the generator
+        let raw_ptr: *mut i32 = generator.any_in_bounds().ptr;
+
+        // Create a non-null pointer from the raw pointer
+        let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };
+
+        // Create a non-deterministic value to write
+        let new_value: i32 = kani::any();
+
+        unsafe {
+            // Perform the volatile write operation
+            ptr.write_volatile(new_value);
+
+            // Read back the value and assert it's correct
+            assert_eq!(ptr.as_ptr().read_volatile(), new_value);
+        }
+    }
+
 }