Contracts & Harnesses for add, addr, and align_offset (#105)

Towards #53

## Changes
Three function contracts & four harnesses:
- added contract and harness for `non_null::add`
- added contract and harness for `non_null::addr`
- added contract and harnesses for `non_null::align_offset`, including
both positive and negative harness that triggers panic. The ensures
clause for `align_offset` is referenced from
[`align_offset`](https://github.com/model-checking/verify-rust-std/pull/69/files)
in `library/core/src/ptr/mod.rs`.


## Revalidation
To revalidate the verification results, run `kani verify-std -Z
unstable-options "path/to/library" -Z function-contracts -Z
mem-predicates --harness ptr::non_null::verify`. This will run all six
harnesses in the module. All default checks should pass:
```
SUMMARY:
 ** 0 of 1556 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.28004378s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.
```
### :exclamation: Warning
Running the above command with the default installed cargo kani will
result in compilation error due to the latest merged from
[PR#91](#91).
Detailed errors are commented under that PR. This issue is waiting to be
resolved.

## TODO:

- Use `Layout` to create dynamically sized arrays in place of fixed size
array in harnesses. This approach currently has errors and is documented
in
[discussion](#104).
- Verify multiple data types: these will be added in future PR.
- Add `requires` clause in contract to constrain `count` to be within
object memory size: there is a current
[issue](#99)
with using `ub_checks::can_write` to get the object size. A workaround
is implemented in the harness.

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: Carolyn Zech <[email protected]>

Author: QinyuanWu

library/core/src/ptr/non_null.rs

@@ -294,6 +294,7 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[inline]
     #[stable(feature = "strict_provenance", since = "CURRENT_RUSTC_VERSION")]
+    #[ensures(|result| result.get() == self.as_ptr() as *const() as usize)]
     pub fn addr(self) -> NonZero<usize> {
         // SAFETY: The pointer is guaranteed by the type to be non-null,
         // meaning that the address will be non-zero.
@@ -567,6 +568,11 @@ 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() 
+        && 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)))]
+    #[ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(count as isize))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1208,6 +1214,36 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_unstable(feature = "const_align_offset", issue = "90962")]
+    #[ensures(|result| {
+        // Post-condition reference: https://github.com/model-checking/verify-rust-std/pull/69/files
+        let stride = crate::mem::size_of::<T>();
+        // ZSTs
+        if stride == 0 {
+            if self.pointer.addr() % align == 0 { 
+                return *result == 0;
+            } else { 
+                return *result == usize::MAX;
+            }
+        }
+        // In this case, the pointer cannot be aligned
+        if (align % stride == 0) && (self.pointer.addr() % stride != 0) {
+            return *result == usize::MAX;
+        }
+        // Checking if the answer should indeed be usize::MAX when align % stride != 0
+        // 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 we reach this case, either:
+        //  - align % stride == 0 and self.pointer.addr() % stride == 0, so it is definitely possible to align the pointer
+        //  - align % stride != 0 and result != usize::MAX, so align_offset is claiming that it's possible to align the pointer
+        // Check that applying the returned result does indeed produce an aligned address
+        let product = usize::wrapping_mul(*result, stride);
+        let new_addr = usize::wrapping_add(product, self.pointer.addr());
+        *result != usize::MAX && new_addr % align == 0
+    })]
     pub const fn align_offset(self, align: usize) -> usize
     where
         T: Sized,
@@ -1811,6 +1847,7 @@ impl<T: ?Sized> From<&T> for NonNull<T> {
 mod verify {
     use super::*;
     use crate::ptr::null_mut;
+    use kani::PointerGenerator;
 
     // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
     #[kani::proof_for_contract(NonNull::new_unchecked)]
@@ -1821,12 +1858,64 @@ mod verify {
         }
     }
 
-    // pub const unsafe fn new(ptr: *mut T) -> Option<Self>
+    // pub const fn new(ptr: *mut T) -> Option<Self>
     #[kani::proof_for_contract(NonNull::new)]
     pub fn non_null_check_new() {
         let mut x: i32 = kani::any();
         let xptr = &mut x;
         let maybe_null_ptr =  if kani::any() { xptr as *mut i32 } else { null_mut() };
         let _ = NonNull::new(maybe_null_ptr);
     }
+
+    // pub const unsafe fn add(self, count: usize) -> Self
+    #[kani::proof_for_contract(NonNull::add)]
+    pub fn non_null_check_add() {
+        const SIZE: usize = 100000;
+        let mut generator = PointerGenerator::<100000>::new();
+        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();  
+        
+        unsafe {
+            let result = ptr.add(count);
+        }
+    }
+
+    // pub fn addr(self) -> NonZero<usize>
+    #[kani::proof_for_contract(NonNull::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; };
+        let address = nonnull_xptr.addr();
+    }
+
+    // pub fn align_offset(self, align: usize) -> usize
+    #[kani::proof_for_contract(NonNull::align_offset)]
+    pub fn non_null_check_align_offset() {
+        // 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());
+        nonnull_xptr.align_offset(align);
+    }
+
+    // pub fn align_offset(self, align: usize) -> usize
+    #[kani::should_panic]
+    #[kani::proof_for_contract(NonNull::align_offset)]
+    pub fn non_null_check_align_offset_negative() {
+        // Create NonNull pointer
+        let x = kani::any::<usize>() as *mut i8;
+        let Some(nonnull_xptr) = NonNull::new(x) else { return; };
+
+        // 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);
+    }
 }