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().addr() % core::mem::align_of::<T>() == 0))]
     pub const fn is_aligned(self) -> bool
     where
         T: Sized,
@@ -1416,6 +1417,8 @@ 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")]
+    #[requires(align.is_power_of_two())]
+    #[ensures(|result: &bool| *result == (self.as_ptr().addr() % 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)
     }
@@ -1786,6 +1789,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 +1814,71 @@ mod verify {
         let maybe_null_ptr =  if kani::any() { xptr as *mut i32 } else { null_mut() };
         let _ = NonNull::new(maybe_null_ptr);
     }
+
+    #[kani::proof]
+    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]> = NonNull::slice_from_raw_parts(non_null_ptr, size);
+
+        // Perform the length check
+        let len = non_null_slice.len();
+        assert!(len == size);
+    }
+
+    #[kani::proof]
+    pub fn non_null_check_is_empty() {
+        // 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(), constrained to zero
+        let size: usize = 0;
+
+        // 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 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 NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned();
+
+    }
+
+    #[kani::proof_for_contract(NonNull::is_aligned_to)]
+    pub fn non_null_check_is_aligned_to() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Create a non-deterministic alignment using kani::any()
+        let align: usize = kani::any();
+        kani::assume(align > 0); // Ensure alignment is greater than zero
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned_to(align);
+
+    }
+
+    #[kani::proof]
+    #[kani::should_panic] // Add this if we expect a panic when the alignment is invalid
+    pub fn non_null_check_is_aligned_to_no_power_two() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Create a non-deterministic alignment value using kani::any()
+        let align: usize = kani::any();
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned_to(align);
+
+    }
 }