From c841a12bf045cc71cc2a181a6f80b0ac06125a88 Mon Sep 17 00:00:00 2001
From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com>
Date: Wed, 4 Dec 2024 17:20:13 -0800
Subject: [PATCH] Contract and harness for as_ptr, cast, as_mut_ptr, and
 as_non_null_ptr (#126)

### Description

This PR includes contracts and proof harnesses for the four APIs as_ptr,
cast, as_mut_ptr, and as_non_null_ptr which are part of the NonNull
library in Rust.

### Changes Overview:

Covered APIs:
NonNull::as_ptr: Acquires the underlying *mut pointer
NonNull::cast: Casts to a pointer of another type
NonNull:: as_mut_ptr:  Returns raw pointer to array's buffer
NonNull::as_non_null_ptr:  Returns a non-null pointer to slice's buffer

Proof harness:
non_null_check_as_ptr
non_null_check_cast
non_null_check_as_mut_ptr
non_null_check_as_non_null_ptr

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 four
harnesses in the module. All default checks should pass:

```
SUMMARY:
 ** 0 of 128 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.8232234s

Complete - 4 successfully verified harnesses, 0 failures, 4 total.

```
Towards issue #53

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 <88045115+zhassan-aws@users.noreply.github.com>
Co-authored-by: Zyad Hassan <zyadh@amazon.com>
Co-authored-by: Michael Tautschnig <mt@debian.org>
Co-authored-by: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com>
---
 library/core/src/ptr/non_null.rs | 44 ++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index c347d8b82c4ac..4174377a84408 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -353,6 +353,8 @@ impl<T: ?Sized> NonNull<T> {
     #[rustc_never_returns_null_ptr]
     #[must_use]
     #[inline(always)]
+    //Ensures address of resulting pointer is same as original
+    #[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
     pub const fn as_ptr(self) -> *mut T {
         self.pointer as *mut T
     }
@@ -454,6 +456,8 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use = "this returns the result of the operation, \
                   without modifying the original"]
     #[inline]
+    // Address preservation
+    #[ensures(|result: &NonNull<U>| result.as_ptr().addr() == self.as_ptr().addr())]
     pub const fn cast<U>(self) -> NonNull<U> {
         // SAFETY: `self` is a `NonNull` pointer which is necessarily non-null
         unsafe { NonNull { pointer: self.as_ptr() as *mut U } }
@@ -1470,6 +1474,8 @@ impl<T> NonNull<[T]> {
     #[inline]
     #[must_use]
     #[unstable(feature = "slice_ptr_get", issue = "74265")]
+    // Address preservation
+    #[ensures(|result: &NonNull<T>| result.as_ptr().addr() == self.as_ptr().addr())]
     pub const fn as_non_null_ptr(self) -> NonNull<T> {
         self.cast()
     }
@@ -1489,6 +1495,8 @@ impl<T> NonNull<[T]> {
     #[must_use]
     #[unstable(feature = "slice_ptr_get", issue = "74265")]
     #[rustc_never_returns_null_ptr]
+    // Address preservation
+    #[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
     pub const fn as_mut_ptr(self) -> *mut T {
         self.as_non_null_ptr().as_ptr()
     }
@@ -2186,6 +2194,42 @@ mod verify {
         }
     }
 
+    #[kani::proof_for_contract(NonNull::as_ptr)]
+    pub fn non_null_check_as_ptr() {
+        // Create a non-null pointer to a random value
+        let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
+        if let Some(ptr) = NonNull::new(non_null_ptr) {
+            let result = ptr.as_ptr();
+        }
+    
+    }
+    
+    #[kani::proof_for_contract(NonNull::<[T]>::as_mut_ptr)]
+    pub fn non_null_check_as_mut_ptr() {
+        const ARR_LEN: usize = 100;
+        let mut values: [i32; ARR_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array_mut(&mut values);
+        let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap();
+        let result = non_null_ptr.as_mut_ptr();
+    }
+    #[kani::proof_for_contract(NonNull::<T>::cast)]
+    pub fn non_null_check_cast() {
+        // Create a non-null pointer to a random value
+        let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
+        if let Some(ptr) = NonNull::new(non_null_ptr) {
+            let result: NonNull<u8> = ptr.cast();
+        }
+    }
+    
+    #[kani::proof_for_contract(NonNull::<[T]>::as_non_null_ptr)]
+    pub fn non_null_check_as_non_null_ptr() {
+        const ARR_LEN: usize = 100;
+        let mut values: [i32; ARR_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array_mut(&mut values);
+        let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap();
+        let result = non_null_ptr.as_non_null_ptr();
+     } 
+  
     #[kani::proof]
     pub fn non_null_check_len() {
         // Create a non-deterministic NonNull pointer using kani::any()