Contracts & Harnesses for non_null::new and non_null::new_unchecked

library/core/src/ptr/non_null.rs

@@ -1,3 +1,4 @@
+use super::*;
 use crate::cmp::Ordering;
 use crate::marker::Unsize;
 use crate::mem::{MaybeUninit, SizedTypeProperties};
@@ -8,6 +9,10 @@ use crate::ptr::Unique;
 use crate::slice::{self, SliceIndex};
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{fmt, hash, intrinsics, ptr};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 
 /// `*mut T` but non-zero and [covariant].
 ///
@@ -192,6 +197,8 @@ impl<T: ?Sized> NonNull<T> {
     #[stable(feature = "nonnull", since = "1.25.0")]
     #[rustc_const_stable(feature = "const_nonnull_new_unchecked", since = "1.25.0")]
     #[inline]
+    #[requires(!ptr.is_null())]
+    #[ensures(|result| result.as_ptr() == ptr)]
     pub const unsafe fn new_unchecked(ptr: *mut T) -> Self {
         // SAFETY: the caller must guarantee that `ptr` is non-null.
         unsafe {
@@ -221,6 +228,8 @@ impl<T: ?Sized> NonNull<T> {
     #[stable(feature = "nonnull", since = "1.25.0")]
     #[rustc_const_unstable(feature = "const_nonnull_new", issue = "93235")]
     #[inline]
+    #[ensures(|result| result.is_some() == !ptr.is_null())]
+    #[ensures(|result| result.is_none() || result.expect("ptr is null!").as_ptr() == ptr)]
     pub const fn new(ptr: *mut T) -> Option<Self> {
         if !ptr.is_null() {
             // SAFETY: The pointer is already checked and is not null
@@ -1770,3 +1779,30 @@ impl<T: ?Sized> From<&T> for NonNull<T> {
         unsafe { NonNull { pointer: reference as *const T } }
     }
 }
+
+//#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
+    #[kani::proof_for_contract(NonNull::new_unchecked)]
+    pub fn non_null_check_new_unchecked() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let _ = NonNull::new_unchecked(xptr as *mut i32);
+        }
+    }
+
+    // pub const unsafe 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;
+        unsafe {
+            let nonnull_ptr = NonNull::new(xptr as *mut i32);
+            let null_ptr = NonNull::<u32>::new(null_mut());
+            assert!(null_ptr.is_none());
+        }
+    }
+}