Skip to content

iter: add kani proof for next_unchecked (#280) #501

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

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

iter: add kani proof for next_unchecked (#280) #501

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
30 changes: 29 additions & 1 deletion library/core/src/iter/traits/unchecked_iterator.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ pub(crate) trait UncheckedIterator: TrustedLen {
/// point you might want to implement this manually instead.
#[unstable(feature = "trusted_len_next_unchecked", issue = "37572")]
#[inline]
#[requires(self.size_hint().0 > 0)]
#[requires(self.size_hint().0 != 0 && self.size_hint().1 != Some(0))]
#[cfg_attr(kani, kani::modifies(self))]
unsafe fn next_unchecked(&mut self) -> Self::Item {
let opt = self.next();
Expand All @@ -40,3 +40,31 @@ pub(crate) trait UncheckedIterator: TrustedLen {
unsafe { opt.unwrap_unchecked() }
}
}

#[cfg(kani)]
#[kani::proof]
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
#[kani::proof]
#[kani::proof_for_contract(UncheckedIterator::next_unchecked)]

so that Kani actually uses the requires clause.

Copy link
Author

Choose a reason for hiding this comment

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

This does not work:

error: The function specified in the `proof_for_contract` attribute, `UncheckedIterator::next_unchecked`, is not reachable from the harness `verify_next_unchecked`.
  --> /home/user/src/rust/library/core/src/iter/traits/unchecked_iterator.rs:46:1
   |
46 | fn verify_next_unchecked() {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = help: Make sure that `verify_next_unchecked` calls `UncheckedIterator::next_unchecked`

error: could not compile `core` (lib) due to 1 previous error; 1 warning emitted
warning: build failed, waiting for other jobs to finish...
error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.

Copy link
Member

Choose a reason for hiding this comment

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

Ah, sorry, would kani::proof_for_contract(iter::traits::unchecked_iterator::UncheckedIterator::next_unchecked) work?

Copy link
Author

Choose a reason for hiding this comment

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

No, same error.

fn verify_next_unchecked() {
const N: usize = 1024;

let arr: [u8; N] = [kani::any(); N];

let idx = kani::any::<usize>() % (N - 1);

let mut it = arr[..=idx].iter();

let (lo, hi) = it.size_hint();

kani::assume(lo != 0);
kani::assume(hi != Some(0));

let _ = unsafe { it.next_unchecked() };

let mut it = arr[idx..].iter();

let (lo, hi) = it.size_hint();

kani::assume(lo != 0);
kani::assume(hi != Some(0));

let _ = unsafe { it.next_unchecked() };
}
Loading