Add safety preconditions to alloc/src/collections/binary_heap/mod.rs

library/alloc/Cargo.toml

@@ -11,6 +11,7 @@ edition = "2021"
 [dependencies]
 core = { path = "../core" }
 compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] }
+safety = { path = "../contracts/safety" }
 
 [dev-dependencies]
 rand = { version = "0.8.5", default-features = false, features = ["alloc"] }

library/alloc/src/collections/binary_heap/mod.rs

@@ -143,6 +143,11 @@
 #![allow(missing_docs)]
 #![stable(feature = "rust1", since = "1.0.0")]
 
+use safety::requires;
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+use core::kani;
+
 use core::alloc::Allocator;
 use core::iter::{FusedIterator, InPlaceIterable, SourceIter, TrustedFused, TrustedLen};
 use core::mem::{self, swap, ManuallyDrop};
@@ -672,6 +677,7 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < self.len()`.
+    #[requires(pos < self.len())]
     unsafe fn sift_up(&mut self, start: usize, pos: usize) -> usize {
         // Take out the value at `pos` and create a hole.
         // SAFETY: The caller guarantees that pos < self.len()
@@ -701,6 +707,7 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < end <= self.len()`.
+    #[requires(pos < end && end <= self.len())]
     unsafe fn sift_down_range(&mut self, pos: usize, end: usize) {
         // SAFETY: The caller guarantees that pos < end <= self.len().
         let mut hole = unsafe { Hole::new(&mut self.data, pos) };
@@ -741,6 +748,7 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < self.len()`.
+    #[requires(pos < self.len())]
     unsafe fn sift_down(&mut self, pos: usize) {
         let len = self.len();
         // SAFETY: pos < len is guaranteed by the caller and
@@ -757,6 +765,7 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < self.len()`.
+    #[requires(pos < self.len())]
     unsafe fn sift_down_to_bottom(&mut self, mut pos: usize) {
         let end = self.len();
         let start = pos;
@@ -1897,3 +1906,53 @@ impl<'a, T: 'a + Ord + Copy, A: Allocator> Extend<&'a T> for BinaryHeap<T, A> {
         self.reserve(additional);
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    // unsafe fn sift_up(&mut self, start: usize, pos: usize) -> usize
+    #[kani::proof_for_contract(BinaryHeap<T, A>::sift_up)]
+    pub fn check_sift_up() {
+        // TODO: this isn't exactly an arbitrary heap
+        let mut heap = BinaryHeap::new_in(Global);
+        heap.push(kani::any::<usize>());
+        unsafe {
+            let _ = heap.sift_up(kani::any(), kani::any());
+        }
+    }
+
+    // unsafe fn sift_down_range(&mut self, pos: usize, end: usize)
+    #[kani::proof_for_contract(BinaryHeap<T, A>::sift_down_range)]
+    pub fn check_sift_down_range() {
+        // TODO: this isn't exactly an arbitrary heap
+        let mut heap = BinaryHeap::new_in(Global);
+        heap.push(kani::any::<usize>());
+        unsafe {
+            let _ = heap.sift_down_range(kani::any(), kani::any());
+        }
+    }
+
+    // unsafe fn sift_down(&mut self, pos: usize)
+    #[kani::proof_for_contract(BinaryHeap<T, A>::sift_down)]
+    pub fn check_sift_down() {
+        // TODO: this isn't exactly an arbitrary heap
+        let mut heap = BinaryHeap::new_in(Global);
+        heap.push(kani::any::<usize>());
+        unsafe {
+            let _ = heap.sift_down(kani::any());
+        }
+    }
+
+    // unsafe fn sift_down_to_bottom(&mut self, mut pos: usize)
+    #[kani::proof_for_contract(BinaryHeap<T, A>::sift_down_to_bottom)]
+    pub fn check_sift_down_to_bottom() {
+        // TODO: this isn't exactly an arbitrary heap
+        let mut heap = BinaryHeap::new_in(Global);
+        heap.push(kani::any::<usize>());
+        unsafe {
+            let _ = heap.sift_down_to_bottom(kani::any());
+        }
+    }
+}

library/alloc/src/lib.rs

@@ -91,6 +91,7 @@
 //
 // Library features:
 // tidy-alphabetical-start
+#![cfg_attr(kani, feature(kani))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
 #![feature(alloc_layout_extra)]

library/std/Cargo.toml

@@ -26,6 +26,7 @@ hashbrown = { version = "0.14", default-features = false, features = [
 std_detect = { path = "../stdarch/crates/std_detect", default-features = false, features = [
     'rustc-dep-of-std',
 ] }
+safety = { path = "../contracts/safety" }
 
 # Dependencies of the `backtrace` crate
 rustc-demangle = { version = "0.1.24", features = ['rustc-dep-of-std'] }

library/std/src/lib.rs

@@ -269,6 +269,7 @@
 #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))]
 #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))]
 #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))]
+#![cfg_attr(kani, feature(kani))]
 //
 // Language features:
 // tidy-alphabetical-start