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,16 @@ 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 } }
  }
 
  /// 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);
+ }
+ }
+}