Contracts and harnesses for ptr::Unique

library/core/src/ptr/unique.rs

@@ -1,8 +1,12 @@
+use safety::{ensures, requires};
 use crate::fmt;
 use crate::marker::{PhantomData, Unsize};
 use crate::ops::{CoerceUnsized, DispatchFromDyn};
 use crate::ptr::NonNull;
 
+#[cfg(kani)]
+use crate::kani;
+
 /// A wrapper around a raw non-null `*mut T` that indicates that the possessor
 /// of this wrapper owns the referent. Useful for building abstractions like
 /// `Box<T>`, `Vec<T>`, `String`, and `HashMap<K, V>`.
@@ -84,13 +88,17 @@ impl<T: ?Sized> Unique<T> {
     ///
     /// `ptr` must be non-null.
     #[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 { Unique { pointer: NonNull::new_unchecked(ptr), _marker: PhantomData } }
     }
 
     /// Creates a new `Unique` if `ptr` is non-null.
     #[inline]
+    #[ensures(|result| result.is_none() == ptr.is_null())]
+    #[ensures(|result| result.is_none() || result.unwrap().as_ptr() == ptr)]
     pub const fn new(ptr: *mut T) -> Option<Self> {
         if let Some(pointer) = NonNull::new(ptr) {
             Some(Unique { pointer, _marker: PhantomData })
@@ -102,13 +110,15 @@ impl<T: ?Sized> Unique<T> {
     /// Acquires the underlying `*mut` pointer.
     #[must_use = "`self` will be dropped if the result is not used"]
     #[inline]
+    #[ensures(|result| !result.is_null())]
     pub const fn as_ptr(self) -> *mut T {
         self.pointer.as_ptr()
     }
 
     /// Acquires the underlying `*mut` pointer.
     #[must_use = "`self` will be dropped if the result is not used"]
     #[inline]
+    #[ensures(|result| result.as_ptr() == self.pointer.as_ptr())]
     pub const fn as_non_null_ptr(self) -> NonNull<T> {
         self.pointer
     }
@@ -201,3 +211,82 @@ impl<T: ?Sized> From<NonNull<T>> for Unique<T> {
         Unique { pointer, _marker: PhantomData }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
+    #[kani::proof_for_contract(Unique::new_unchecked)]
+    pub fn check_new_unchecked() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let _ = Unique::new_unchecked(xptr as *mut i32);
+        }
+    }
+
+    // pub const fn new(ptr: *mut T) -> Option<Self>
+    #[kani::proof_for_contract(Unique::new)]
+    pub fn check_new() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        let _ = Unique::new(xptr as *mut i32);
+    }
+
+    // pub const fn as_ptr(self) -> *mut T
+    #[kani::proof_for_contract(Unique::as_ptr)]
+    pub fn check_as_ptr() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let unique = Unique::new_unchecked(xptr as *mut i32);
+            assert_eq!(unique.as_ptr(), xptr as *mut i32);
+        }
+    }
+
+    // pub const fn as_non_null_ptr(self) -> NonNull<T>
+    #[kani::proof_for_contract(Unique::as_non_null_ptr)]
+    pub fn check_as_non_null_ptr() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let unique = Unique::new_unchecked(xptr as *mut i32);
+            let _ = unique.as_non_null_ptr();
+        }
+    }
+
+    // pub const unsafe fn as_ref(&self) -> &T
+    #[kani::proof]
+    pub fn check_as_ref() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let unique = Unique::new_unchecked(xptr as *mut i32);
+            assert_eq!(*unique.as_ref(), x);
+        }
+    }
+
+    // pub const unsafe fn as_mut(&mut self) -> &mut T
+    #[kani::proof]
+    pub fn check_as_mut() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let mut unique = Unique::new_unchecked(xptr as *mut i32);
+            assert_eq!(*unique.as_mut(), x);
+        }
+    }
+
+    // pub const fn cast<U>(self) -> Unique<U>
+    #[kani::proof_for_contract(Unique::cast<U>)]
+    pub fn check_cast<U>() {
+        let mut x : i32 = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let unique = Unique::new_unchecked(xptr as *mut i32);
+            assert_eq!(*unique.cast::<u32>().as_ref(), x as u32);
+        }
+    }
+}