Merge branch 'main' into challenge/select

library/core/src/ptr/alignment.rs

@@ -1,4 +1,4 @@
-use safety::requires;
+use safety::{ensures, requires};
 use crate::num::NonZero;
 #[cfg(debug_assertions)]
 use crate::ub_checks::assert_unsafe_precondition;
@@ -48,6 +48,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(mem::align_of::<T>().is_power_of_two())]
+    #[ensures(|result| result.as_usize().is_power_of_two())]
     pub const fn of<T>() -> Self {
         // SAFETY: rustc ensures that type alignment is always a power of two.
         unsafe { Alignment::new_unchecked(mem::align_of::<T>()) }
@@ -60,6 +62,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| align.is_power_of_two() == result.is_some())]
+    #[ensures(|result| result.is_none() || result.unwrap().as_usize() == align)]
     pub const fn new(align: usize) -> Option<Self> {
         if align.is_power_of_two() {
             // SAFETY: Just checked it only has one bit set
@@ -80,8 +84,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
-    #[requires(align > 0)]
-    #[requires((align & (align - 1)) == 0)]
+    #[requires(align > 0 && (align & (align - 1)) == 0)]
+    #[ensures(|result| result.as_usize() == align)]
+    #[ensures(|result| result.as_usize().is_power_of_two())]
     pub const unsafe fn new_unchecked(align: usize) -> Self {
         #[cfg(debug_assertions)]
         assert_unsafe_precondition!(
@@ -99,6 +104,7 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| result.is_power_of_two())]
     pub const fn as_usize(self) -> usize {
         self.0 as usize
     }
@@ -107,6 +113,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| result.get().is_power_of_two())]
+    #[ensures(|result| result.get() == self.as_usize())]
     pub const fn as_nonzero(self) -> NonZero<usize> {
         // SAFETY: All the discriminants are non-zero.
         unsafe { NonZero::new_unchecked(self.as_usize()) }
@@ -128,6 +136,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(self.as_usize().is_power_of_two())]
+    #[ensures(|result| (*result as usize) < mem::size_of::<usize>() * 8)]
+    #[ensures(|result| 1usize << *result == self.as_usize())]
     pub const fn log2(self) -> u32 {
         self.as_nonzero().trailing_zeros()
     }
@@ -158,6 +169,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| *result > 0)]
+    #[ensures(|result| *result == !(self.as_usize() -1))]
+    #[ensures(|result| self.as_usize() & *result == self.as_usize())]
     pub const fn mask(self) -> usize {
         // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
         !(unsafe { self.as_usize().unchecked_sub(1) })
@@ -370,3 +384,68 @@ enum AlignmentEnum {
     _Align1Shl62 = 1 << 62,
     _Align1Shl63 = 1 << 63,
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    impl kani::Arbitrary for Alignment {
+        fn any() -> Self {
+            let align = kani::any_where(|a: &usize| a.is_power_of_two());
+            unsafe { mem::transmute::<usize, Alignment>(align) }
+        }
+    }
+
+    // pub const fn of<T>() -> Self
+    #[kani::proof_for_contract(Alignment::of)]
+    pub fn check_of_i32() {
+        let _ = Alignment::of::<i32>();
+    }
+
+    // pub const fn new(align: usize) -> Option<Self>
+    #[kani::proof_for_contract(Alignment::new)]
+    pub fn check_new() {
+        let a = kani::any::<usize>();
+        let _ = Alignment::new(a);
+    }
+
+    // pub const unsafe fn new_unchecked(align: usize) -> Self
+    #[kani::proof_for_contract(Alignment::new_unchecked)]
+    pub fn check_new_unchecked() {
+        let a = kani::any::<usize>();
+        unsafe {
+            let _ = Alignment::new_unchecked(a);
+        }
+    }
+
+    // pub const fn as_usize(self) -> usize
+    #[kani::proof_for_contract(Alignment::as_usize)]
+    pub fn check_as_usize() {
+        let a = kani::any::<usize>();
+        if let Some(alignment) = Alignment::new(a) {
+            assert_eq!(alignment.as_usize(), a);
+        }
+    }
+
+    // pub const fn as_nonzero(self) -> NonZero<usize>
+    #[kani::proof_for_contract(Alignment::as_nonzero)]
+    pub fn check_as_nonzero() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.as_nonzero();
+    }
+
+    // pub const fn log2(self) -> u32
+    #[kani::proof_for_contract(Alignment::log2)]
+    pub fn check_log2() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.log2();
+    }
+
+    // pub const fn mask(self) -> usize
+    #[kani::proof_for_contract(Alignment::mask)]
+    pub fn check_mask() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.mask();
+    }
+}

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);
+        }
+    }
+}