From 6c2610dd649c3e0ed5ba13d7dcbdba1349d3bbb1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 30 Jul 2024 11:54:51 +0000
Subject: [PATCH] Contracts and harnesses for `ptr::Unique`

---
 library/core/src/ptr/unique.rs | 97 ++++++++++++++++++++++++++++++++++
 1 file changed, 97 insertions(+)

diff --git a/library/core/src/ptr/unique.rs b/library/core/src/ptr/unique.rs
index b74d691e45427..4f350b0eb1d1b 100644
--- a/library/core/src/ptr/unique.rs
+++ b/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,6 +88,7 @@ impl<T: ?Sized> Unique<T> {
     ///
     /// `ptr` must be non-null.
     #[inline]
+    #[requires(!ptr.is_null())]
     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 } }
@@ -91,6 +96,8 @@ impl<T: ?Sized> Unique<T> {
 
     /// Creates a new `Unique` if `ptr` is non-null.
     #[inline]
+    #[ensures(|result| result.is_none() == result.unwrap().as_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,6 +109,7 @@ 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()
     }
@@ -201,3 +209,92 @@ 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 = 42;
+        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 new(ptr: *mut T) -> Option<Self>
+    #[kani::proof_for_contract(Unique::new)]
+    pub fn check_new() {
+        let mut x : i32 = 42;
+        let xptr = &mut x;
+
+        if let Some(unique) = Unique::new(xptr as *mut i32) {
+            assert_eq!(unique.as_ptr(), 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 = 42;
+        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]
+    pub fn check_as_non_null_ptr() {
+        let mut x : i32 = 42;
+        let xptr = &mut x;
+
+        unsafe {
+            let unique = Unique::new_unchecked(xptr as *mut i32);
+            assert_eq!(unique.as_non_null_ptr().as_ptr(), xptr as *mut i32);
+        }
+    }
+
+    // pub const unsafe fn as_ref(&self) -> &T
+    #[kani::proof]
+    pub fn check_as_ref() {
+        let mut x : i32 = 42;
+        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 = 42;
+        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 = 42;
+        let xptr = &mut x;
+
+        unsafe {
+            let unique = Unique::new_unchecked(xptr as *mut i32);
+            assert_eq!(*unique.cast::<u32>().as_ref(), x as u32);
+        }
+    }
+}