From 0c2a9f7ed858428f2ce3d1a81ebe61fb3f3cf665 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Thu, 5 Jun 2025 17:01:12 -0700 Subject: [PATCH 1/2] Setting the appropriate target when running autoharness-analyzer from run-kani.sh --- scripts/run-kani.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 6fb4b926ffda5..389e811a5c9ab 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -351,7 +351,9 @@ main() { --cbmc-args --object-bits 12 # remove metadata file for Kani-generated "dummy" crate that we won't # get scanner data for - rm target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/dummy-* + local target=$(find "target/kani_verify_std/target/" -mindepth 1 \ + -type d -exec test -e '{}'/debug/deps/ \; -print) + rm $target/debug/deps/dummy-* echo "Running Kani's std-analysis command..." pushd scripts/kani-std-analysis ./std-analysis.sh $build_dir @@ -359,11 +361,9 @@ main() { echo "Running autoharness-analyzer command..." pushd scripts/autoharness_analyzer cargo run -- --per-crate \ - ../../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ - /tmp/std_lib_analysis/results/ + ../../$target/debug/deps/ /tmp/std_lib_analysis/results/ cargo run -- --per-crate --unsafe-fns-only \ - ../../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ - /tmp/std_lib_analysis/results/ + ../../$target/debug/deps/ /tmp/std_lib_analysis/results/ popd fi } From 06225875fd2d6b5f3be8ae8c4a221cb91fc382a2 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Thu, 19 Jun 2025 18:40:18 -0700 Subject: [PATCH 2/2] Contracts for binary_heap::mod.rs. --- .../alloc/src/collections/binary_heap/mod.rs | 57 +++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/library/alloc/src/collections/binary_heap/mod.rs b/library/alloc/src/collections/binary_heap/mod.rs index 63828b482b9a9..f0e9aa399ff8e 100644 --- a/library/alloc/src/collections/binary_heap/mod.rs +++ b/library/alloc/src/collections/binary_heap/mod.rs @@ -143,6 +143,11 @@ #![allow(missing_docs)] #![stable(feature = "rust1", since = "1.0.0")] +use safety::{ensures,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, ManuallyDrop, swap}; @@ -742,6 +747,8 @@ impl BinaryHeap { /// The caller must guarantee that `pos < self.len()`. /// /// Returns the new position of the element. + #[requires(pos < self.len())] + #[cfg_attr(kani, kani::modifies(self.data.as_mut_ptr()))] 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() @@ -773,6 +780,8 @@ impl BinaryHeap { /// # Safety /// /// The caller must guarantee that `pos < end <= self.len()`. + #[requires(pos < end && end <= self.len())] + #[cfg_attr(kani, kani::modifies(self.data.as_mut_ptr()))] unsafe fn sift_down_range(&mut self, pos: usize, end: usize) -> usize { // SAFETY: The caller guarantees that pos < end <= self.len(). let mut hole = unsafe { Hole::new(&mut self.data, pos) }; @@ -815,6 +824,8 @@ impl BinaryHeap { /// # Safety /// /// The caller must guarantee that `pos < self.len()`. + #[requires(pos < self.len())] + #[cfg_attr(kani, kani::modifies(self.data.as_mut_ptr()))] unsafe fn sift_down(&mut self, pos: usize) -> usize { let len = self.len(); // SAFETY: pos < len is guaranteed by the caller and @@ -831,6 +842,8 @@ impl BinaryHeap { /// # Safety /// /// The caller must guarantee that `pos < self.len()`. + #[requires(pos < self.len())] + #[cfg_attr(kani, kani::modifies(self.data.as_mut_ptr()))] unsafe fn sift_down_to_bottom(&mut self, mut pos: usize) { let end = self.len(); let start = pos; @@ -1440,6 +1453,7 @@ impl<'a, T> Hole<'a, T> { /// /// Unsafe because pos must be within the data slice. #[inline] + #[requires(pos < data.len())] unsafe fn new(data: &'a mut [T], pos: usize) -> Self { debug_assert!(pos < data.len()); // SAFE: pos should be inside the slice @@ -1462,6 +1476,8 @@ impl<'a, T> Hole<'a, T> { /// /// Unsafe because index must be within the data slice and not equal to pos. #[inline] + #[requires(index != self.pos)] + #[requires(index < self.data.len())] unsafe fn get(&self, index: usize) -> &T { debug_assert!(index != self.pos); debug_assert!(index < self.data.len()); @@ -1472,6 +1488,9 @@ impl<'a, T> Hole<'a, T> { /// /// Unsafe because index must be within the data slice and not equal to pos. #[inline] + #[requires(index != self.pos)] + #[requires(index < self.data.len())] + #[cfg_attr(kani, kani::modifies(self.data.as_mut_ptr()))] unsafe fn move_to(&mut self, index: usize) { debug_assert!(index != self.pos); debug_assert!(index < self.data.len()); @@ -1973,3 +1992,41 @@ impl<'a, T: 'a + Ord + Copy, A: Allocator> Extend<&'a T> for BinaryHeap { self.reserve(additional); } } + +#[cfg(kani)] +mod verify { + use super::*; + + #[kani::proof_for_contract(BinaryHeap::sift_down)] + #[kani::unwind(3)] + fn verify_sift_down() { + // Create an arbitrary size for the heap + let size: usize = kani::any(); + kani::assume(size > 0); // Need at least one element since pos < self.len() + kani::assume(size <= 2); // Reasonable bound for verification + + // Create a BinaryHeap with arbitrary elements + let mut heap = BinaryHeap::new(); + for _ in 0..size { + heap.data.push(kani::any::()); + } + + // Create arbitrary pos value + let pos: usize = kani::any(); + + // Ensure precondition: pos < self.len() + kani::assume(pos < heap.len()); + + // Store initial heap length to verify it doesn't change + let initial_len = heap.len(); + + // Call the function under test + // SAFETY: We've ensured pos < heap.len() + let new_pos = unsafe { heap.sift_down(pos) }; + + // Verify postconditions + assert_eq!(heap.len(), initial_len); // Length should remain unchanged + assert!(new_pos >= pos); // Element can only move down (to higher index) + assert!(new_pos < heap.len()); // Element stays within valid bounds + } +} \ No newline at end of file