Contracts & Harnesses for len, is_empty, is_aligned, and is_aligned_to

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;
@@ -1301,6 +1301,7 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[stable(feature = "pointer_is_aligned", since = "1.79.0")]
     #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")]
+    #[ensures(|result: &bool| *result == (self.as_ptr() as usize % core::mem::align_of::<T>() == 0))] // Ensure the returned value is correct for alignment check
     pub const fn is_aligned(self) -> bool
     where
         T: Sized,
@@ -1416,6 +1417,7 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[unstable(feature = "pointer_is_aligned_to", issue = "96284")]
     #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")]
+    #[ensures(|result: &bool| *result == ((self.as_ptr() as *const u8) as usize % align == 0))] // Ensure the returned value is correct based on the given alignment
     pub const fn is_aligned_to(self, align: usize) -> bool {
         self.pointer.is_aligned_to(align)
     }
@@ -1471,6 +1473,7 @@ impl<T> NonNull<[T]> {
     #[rustc_const_stable(feature = "const_slice_ptr_len_nonnull", since = "1.63.0")]
     #[must_use]
     #[inline]
+    #[ensures(|result: &usize| *result >= 0)]
     pub const fn len(self) -> usize {
         self.as_ptr().len()
     }
@@ -1489,6 +1492,7 @@ impl<T> NonNull<[T]> {
     #[rustc_const_stable(feature = "const_slice_ptr_is_empty_nonnull", since = "1.79.0")]
     #[must_use]
     #[inline]
+    #[ensures(|result: &bool| *result == (self.len() == 0))]
     pub const fn is_empty(self) -> bool {
         self.len() == 0
     }
@@ -1786,6 +1790,14 @@ mod verify {
     use super::*;
     use crate::ptr::null_mut;
 
+    impl<T> kani::Arbitrary for NonNull<T> {
+        fn any() -> Self {
+            let ptr: *mut T = kani::any::<usize>() as *mut T;
+            kani::assume(!ptr.is_null());
+            NonNull::new(ptr).expect("Non-null pointer expected")
+        }
+    }
+
     // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
     #[kani::proof_for_contract(NonNull::new_unchecked)]
     pub fn non_null_check_new_unchecked() {
@@ -1803,4 +1815,80 @@ 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::len)]
+    // pub fn non_null_check_len() {
+    //     const SIZE: usize = 20000;
+    //     // Create a non-deterministic array of size SIZE
+    //     let arr: [i8; SIZE] = kani::any();  
+    //     // Get a raw pointer to the array
+    //     let raw_ptr: *const i8 = arr.as_ptr();  
+    //     // Create a NonNull slice from the raw pointer
+    //     let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) };  
+
+    //     // Perform the length check
+    //     let len = non_null_slice.len();
+    //     assert!(len == SIZE);
+    // }
+
+    #[kani::proof_for_contract(NonNull::len)]
+    pub fn non_null_check_len() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i8> = kani::any();
+        // Create a non-deterministic size using kani::any()
+        let size: usize = kani::any();
+        // Create a NonNull slice from the non-null pointer and size
+        let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) };
+
+        // Perform the length check
+        let len = non_null_slice.len();
+        assert!(len == size);
+    }
+
+    #[kani::proof_for_contract(NonNull::is_empty)]
+    pub fn non_null_check_is_empty() {
+        const SIZE: usize = 0;
+        // Create a non-deterministic array of size SIZE
+        let arr: [i8; SIZE] = kani::any();  
+        // Get a raw pointer to the array
+        let raw_ptr: *const i8 = arr.as_ptr();  
+        // Create a NonNull slice from the raw pointer
+        let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) };  
+
+        // Perform the is_empty check
+        let is_empty = non_null_slice.is_empty();
+        assert!(is_empty);
+    }
+
+    #[kani::proof_for_contract(NonNull::is_aligned)]
+    pub fn non_null_slice_is_aligned_check() {
+        // Create a non-deterministic integer
+        let mut data: i32 = kani::any();  
+        // Get a raw pointer to the integer
+        let raw_ptr: *mut i32 = &mut data;
+        // NonNull pointer to the integer
+        let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };
+
+        // Perform the alignment check
+        let result = ptr.is_aligned();
+        assert!(result);
+    }
+
+    #[kani::proof_for_contract(NonNull::is_aligned_to)]
+    pub fn non_null_check_is_aligned_to() {
+        const SIZE: usize = 10;
+        const ALIGN: usize = 4;
+        // Create a non-deterministic array of size SIZE
+        let arr: [i32; SIZE] = kani::any();  
+        // Get a raw pointer to the array
+        let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32;
+        // Randomize pointer offset within array bounds
+        let offset = kani::any_where(|x| *x <= SIZE);
+        // NonNull pointer to the random offset
+        let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() };
+
+        // Perform the alignment to check if it matches the given alignment
+        let result = ptr.is_aligned_to(ALIGN);
+        assert!(result == (ptr.as_ptr() as usize % ALIGN == 0));
+    }
 }