Contracts & Harnesses for NonNull::read, NonNull::read_volatile, …

…`NonNull::read_unaligned` (model-checking#156)

Towards model-checking#52 

Contracts & Harnesses for `NonNull::read`, `NonNull::read_volatile`,
`NonNull::read_unaligned`
### Discussion
For the ensures clause in the contract for `NonNull::read`, I could not
directly compare the value pointed by self and result due to unsized and
lack of PartialEq implementation, and the comparison is currently moved
to the harness.
### Verification
Successful verification:
```
SUMMARY:
 ** 0 of 141 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.1760525s

Complete - 5 successfully verified harnesses, 0 failures, 5 total.
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <zyadh@amazon.com>

library/core/src/ptr/non_null.rs

@@ -13,6 +13,8 @@ use safety::{ensures, requires};
 
 #[cfg(kani)]
 use crate::kani;
+#[cfg(kani)]
+use crate::ub_checks;
 
 /// `*mut T` but non-zero and [covariant].
 ///
@@ -568,7 +570,7 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use = "returns a new pointer rather than modifying its argument"]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
-    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some() 
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some()
         && count * core::mem::size_of::<T>() <= isize::MAX as usize
         && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::<T>() as isize).is_some() // check wrapping add
         && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))]
@@ -910,6 +912,7 @@ impl<T: ?Sized> NonNull<T> {
     #[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(ub_checks::can_dereference(self.pointer))]
     pub const unsafe fn read(self) -> T
     where
         T: Sized,
@@ -931,6 +934,7 @@ impl<T: ?Sized> NonNull<T> {
     #[inline]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires(ub_checks::can_dereference(self.pointer))]
     pub unsafe fn read_volatile(self) -> T
     where
         T: Sized,
@@ -951,6 +955,7 @@ impl<T: ?Sized> NonNull<T> {
     #[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(ub_checks::can_read_unaligned(self.pointer))]
     pub const unsafe fn read_unaligned(self) -> T
     where
         T: Sized,
@@ -1219,9 +1224,9 @@ impl<T: ?Sized> NonNull<T> {
         let stride = crate::mem::size_of::<T>();
         // ZSTs
         if stride == 0 {
-            if self.pointer.addr() % align == 0 { 
+            if self.pointer.addr() % align == 0 {
                 return *result == 0;
-            } else { 
+            } else {
                 return *result == usize::MAX;
             }
         }
@@ -1233,8 +1238,8 @@ impl<T: ?Sized> NonNull<T> {
         // requires computing gcd(a, stride), which is too expensive without
         // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html).
         // This should be updated once quantifiers are available.
-        if (align % stride != 0 && *result == usize::MAX) { 
-            return true; 
+        if (align % stride != 0 && *result == usize::MAX) {
+            return true;
         }
         // If we reach this case, either:
         //  - align % stride == 0 and self.pointer.addr() % stride == 0, so it is definitely possible to align the pointer
@@ -1867,6 +1872,79 @@ mod verify {
         let _ = NonNull::new(maybe_null_ptr);
     }
 
+    // pub const unsafe fn read(self) -> T where T: Sized
+    #[kani::proof_for_contract(NonNull::read)]
+    pub fn non_null_check_read() {
+        let ptr_u8: *mut u8 = &mut kani::any();
+        let nonnull_ptr_u8 = NonNull::new(ptr_u8).unwrap();
+        unsafe {
+            let result = nonnull_ptr_u8.read();
+            kani::assert(*ptr_u8 == result, "read returns the correct value");
+        }
+
+        // array example
+        const ARR_LEN: usize = 10000;
+        let mut generator = PointerGenerator::<ARR_LEN>::new();
+        let raw_ptr: *mut i8 = generator.any_in_bounds().ptr;
+        let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap()};
+        unsafe {
+            let result = nonnull_ptr.read();
+            kani::assert( *nonnull_ptr.as_ptr() == result, "read returns the correct value");
+        }
+    }
+
+    // pub unsafe fn read_volatile(self) -> T where T: Sized
+    #[kani::proof_for_contract(NonNull::read_volatile)]
+    pub fn non_null_check_read_volatile() {
+        let ptr_u8: *mut u8 = &mut kani::any();
+        let nonnull_ptr_u8 = NonNull::new(ptr_u8).unwrap();
+        unsafe {
+            let result = nonnull_ptr_u8.read_volatile();
+            kani::assert(*ptr_u8 == result, "read returns the correct value");
+        }
+
+        // array example
+        const ARR_LEN: usize = 10000;
+        let mut generator = PointerGenerator::<ARR_LEN>::new();
+        let raw_ptr: *mut i8 = generator.any_in_bounds().ptr;
+        let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap()};
+        unsafe {
+            let result = nonnull_ptr.read_volatile();
+            kani::assert( *nonnull_ptr.as_ptr() == result, "read returns the correct value");
+        }
+    }
+
+    #[repr(packed, C)]
+    struct Packed {
+        _padding: u8,
+        unaligned: u32,
+    }
+
+    // pub const unsafe fn read_unaligned(self) -> T where T: Sized
+    #[kani::proof_for_contract(NonNull::read_unaligned)]
+    pub fn non_null_check_read_unaligned() {
+        // unaligned pointer
+        let mut generator = PointerGenerator::<10000>::new();
+        let unaligned_ptr: *mut u8 = generator.any_in_bounds().ptr;
+        let unaligned_nonnull_ptr = NonNull::new(unaligned_ptr).unwrap();
+        unsafe {
+            let result = unaligned_nonnull_ptr.read_unaligned();
+            kani::assert( *unaligned_nonnull_ptr.as_ptr() == result, "read returns the correct value");
+        }
+
+        // read an unaligned value from a packed struct
+        let unaligned_value: u32 = kani::any();
+        let packed = Packed {
+            _padding: kani::any::<u8>(),
+            unaligned: unaligned_value,
+        };
+
+        let unaligned_ptr = ptr::addr_of!(packed.unaligned);
+        let nonnull_packed_ptr = NonNull::new(unaligned_ptr as *mut u32).unwrap();
+        let v = unsafe { nonnull_packed_ptr.read_unaligned() };
+        assert_eq!(v, unaligned_value);
+    }
+
     // pub const unsafe fn add(self, count: usize) -> Self
     #[kani::proof_for_contract(NonNull::add)]
     pub fn non_null_check_add() {
@@ -1875,16 +1953,16 @@ mod verify {
         let raw_ptr: *mut i8 = generator.any_in_bounds().ptr;
         let ptr = unsafe { NonNull::new(raw_ptr).unwrap()};
         // Create a non-deterministic count value
-        let count: usize = kani::any();  
-        
+        let count: usize = kani::any();
+
         unsafe {
             let result = ptr.add(count);
         }
     }
 
     // pub fn addr(self) -> NonZero<usize>
     #[kani::proof_for_contract(NonNull::addr)]
-    pub fn non_null_check_addr() {  
+    pub fn non_null_check_addr() {
         // Create NonNull pointer & get pointer address
         let x = kani::any::<usize>() as *mut i32;
         let Some(nonnull_xptr) = NonNull::new(x) else { return; };
@@ -1897,7 +1975,7 @@ mod verify {
         // Create NonNull pointer
         let x = kani::any::<usize>() as *mut i32;
         let Some(nonnull_xptr) = NonNull::new(x) else { return; };
-    
+
         // Call align_offset with valid align value
         let align: usize = kani::any();
         kani::assume(align.is_power_of_two());
@@ -1914,7 +1992,7 @@ mod verify {
 
         // Generate align value that is not necessarily a power of two
         let invalid_align: usize = kani::any();
-    
+
         // Trigger panic
         let offset = nonnull_xptr.align_offset(invalid_align);
     }