Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 7 commits into
base: main
Choose a base branch
from
Open

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

Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
8e6b212
Add safety preconditions to alloc/src/collections/binary_heap/mod.rs
tautschnig Oct 17, 2024
7e7b50b
Add safety dependency to alloc and std crates
tautschnig Oct 17, 2024
806ea2a
fixup! Add safety dependency to alloc and std crates
tautschnig Oct 17, 2024
c2b65cf
fixup! Add safety dependency to alloc and std crates
tautschnig Oct 17, 2024
2ca4ee7
Fix harnesses
tautschnig Oct 17, 2024
027385a
Add annotations required by Kani
tautschnig Oct 18, 2024
6582e1d
Merge remote-tracking branch 'origin/main' into bedrock-library/alloc…
tautschnig Dec 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 69 additions & 0 deletions library/alloc/src/collections/binary_heap/mod.rs
View file
Open in desktop
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do these function require self to be safe?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are you asking whether there are requirements that the object is in some sort of sane state? I would believe so, but why would we ever permit for that not to be the case?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that we shouldn't, but we do.

Conceptually, internal functions can temporary break the safety invariants of the types.

Original file line number Diff line number Diff line change
Expand Up @@ -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, ManuallyDrop, swap};
Expand Down Expand Up @@ -675,6 +680,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
/// # Safety
///
/// The caller must guarantee that `pos < self.len()`.
#[requires(pos < self.len())]
#[cfg_attr(kani, kani::modifies(self.data.as_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()
Expand Down Expand Up @@ -704,6 +711,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
/// # Safety
///
/// The caller must guarantee that `pos < end <= self.len()`.
#[requires(pos < end && end <= self.len())]
#[cfg_attr(kani, kani::modifies(self.data.as_ptr()))]
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) };
Expand Down Expand Up @@ -744,6 +753,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
/// # Safety
///
/// The caller must guarantee that `pos < self.len()`.
#[requires(pos < self.len())]
#[cfg_attr(kani, kani::modifies(self.data.as_ptr()))]
unsafe fn sift_down(&mut self, pos: usize) {
let len = self.len();
// SAFETY: pos < len is guaranteed by the caller and
Expand All @@ -760,6 +771,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
/// # Safety
///
/// The caller must guarantee that `pos < self.len()`.
#[requires(pos < self.len())]
#[cfg_attr(kani, kani::modifies(self.data.as_ptr()))]
unsafe fn sift_down_to_bottom(&mut self, mut pos: usize) {
let end = self.len();
let start = pos;
Expand Down Expand Up @@ -1901,3 +1914,59 @@ 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::*;

// TODO: Kani reports as failing property "Only a single top-level call", which does not
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what exactly is the error?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Following up on this: can you extend the TODO to say what function it's complaining about for the single top-level call?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise, this PR LGTM, but I am curious if we can do a bit of debugging on this harness before merging it as a TODO. If we really get stuck, I'll approve.

// obviously make sense. Requires investigation.
// // unsafe fn sift_up(&mut self, start: usize, pos: usize) -> usize
// #[kani::proof_for_contract(BinaryHeap<T, A>::sift_up)]
// #[kani::unwind(1)]
// 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)]
#[kani::unwind(1)]
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)]
#[kani::unwind(1)]
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)]
#[kani::unwind(1)]
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());
}
}
}
Loading