Skip to content

Add loop contracts and harness for BinaryHeap::sift_up - #129

Closed
qinheping wants to merge 3 commits into
model-checking:mainfrom
qinheping:sift_up
Closed

Add loop contracts and harness for BinaryHeap::sift_up#129
qinheping wants to merge 3 commits into
model-checking:mainfrom
qinheping:sift_up

Conversation

@qinheping

@qinhepingqinheping commented Oct 22, 2024

Copy link
Copy Markdown

This proof is blocked as CBMC couldn't infer the loop modifies hole.pos. We need to add support of loop modifies or improve CBMC's inference algorithm.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@qinhepingqinheping changed the title Add loop contracts and harness for BinaryHeap::sift_upAdd loop contracts and harness for BinaryHeap::sift_upOct 22, 2024
tautschnig
tautschnig reviewed Oct 22, 2024
View reviewed changes
Comment threadlibrary/alloc/src/collections/binary_heap/mod.rs Outdated
@tautschnig

tautschnig commented Oct 22, 2024

Copy link
Copy Markdown
Member

This proof is blocked as CBMC couldn't infer the loop modifies hole.pos. We need to add support of loop modifies or improve CBMC's inference algorithm.

Would adding a kani::modifies for the containing function do the trick? At least in CBMC we inherit the assigns set from the encompassing context if there isn't one. See https://github.com/model-checking/verify-rust-std/pull/120/files (which covers the very same file, but doesn't use loop invariants so is way more limited).

tautschnig
tautschnig reviewed Oct 22, 2024
View reviewed changes
Comment threadlibrary/alloc/Cargo.toml
tautschnig
tautschnig reviewed Oct 22, 2024
View reviewed changes
Comment threadlibrary/alloc/src/lib.rs
celinval
celinval reviewed Oct 23, 2024
View reviewed changes
Comment threadlibrary/alloc/src/collections/binary_heap/mod.rs
// SAFETY: The caller guarantees that pos < self.len()
let mut hole = unsafe { Hole::new(&mut self.data, pos) };

#[cfg_attr(kani, kani::loop_invariant(hole.pos() <= pos))]

@celinvalcelinvalOct 23, 2024

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Can you please loop invariants to the safety crate for now and use that instead?

@qinhepingqinheping mentioned this pull request Feb 3, 2025
Closed
@qinheping

qinheping commented Feb 3, 2025

Copy link
Copy Markdown
Author

Will be unblocked with model-checking/kani#3871

Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnigtautschnigtautschnig left review comments
+1 more reviewer
@celinvalcelinvalcelinval left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

@qinhepingqinheping

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@qinheping@tautschnig@celinval