Skip to content

Challenge 20: Unbounded proofs for the char Searchers of str::pattern #740

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
hung1962003 wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Challenge 20: Unbounded proofs for the char Searchers of str::pattern #740

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
3053231
Challenge 20: unbounded proofs for the char Searchers of str::pattern
hung1962003 Oct 27, 2026
f610507
Challenge 20: speed up the char Searcher proofs
hung1962003 Oct 27, 2026
de65496
Challenge 20: havoc the MultiCharEq cursor as words
hung1962003 Oct 27, 2026
c6a42ee
Challenge 20: simplify the slice model and the pattern state hook
hung1962003 Oct 28, 2026
080960b
Keep check_from_ptr_contract off loop-contract mode
hung1962003 Oct 28, 2026
d686f3e
Challenge 20: decode with one iterator write, model Iter::len
hung1962003 Oct 28, 2026
e86cb4f
Challenge 20: shorten the proofs, decode without `?`
hung1962003 Oct 28, 2026
85f21af
Challenge 20: address review comments
hung1962003 Nov 3, 2026
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
13 changes: 13 additions & 0 deletions library/core/src/ffi/c_str.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1149,7 +1149,12 @@ mod verify {
}

// pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr
// The stub: this harness reaches `CharSearcher::next_match` only through
// panic formatting, where it never runs. Its loop contract would make Kani
// apply loop contracts here, and CBMC 6.11 then rejects the loop of its
// built-in `strlen` (fixed by diffblue/cbmc#9164).
#[kani::proof_for_contract(CStr::from_ptr)]
#[kani::stub(<crate::str::pattern::CharSearcher as crate::str::pattern::Searcher>::next_match, any_match)]

@feliperodri feliperodri Nov 3, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Question: this works around CBMC 6.11 rejecting the built-in strlen loop once loop contracts are enabled (diffblue/cbmc#9164). Could you open a tracking issue so the stub, and the slice::iter raw-parts helpers, are removed once Kani ships a CBMC with that fix?

@hung1962003 hung1962003 Nov 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

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

Opened #748. It tracks the strlen stub (diffblue/cbmc#9164) and also Iter::kani_loop_raw_parts, which depends on model-checking/kani#4796 rather than on the CBMC fix. kani_raw_parts stays, since the invariants need the private fields of Iter.

#[kani::unwind(33)]
fn check_from_ptr_contract() {
const MAX_SIZE: usize = 32;
Expand All @@ -1161,6 +1166,14 @@ mod verify {
}
}

// `'a: 'a` makes `'a` early-bound, like the lifetime of the impl.
fn any_match<'a>(_: &mut crate::str::pattern::CharSearcher<'a>) -> Option<(usize, usize)>
where
'a: 'a,
{
kani::any()
}

// pub const fn is_empty(&self) -> bool
#[kani::proof]
#[kani::unwind(33)]
Expand Down
17 changes: 17 additions & 0 deletions library/core/src/slice/iter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,23 @@ impl<T> AsRef<[T]> for Iter<'_, T> {
}
}

#[cfg(kani)]
impl<T> Iter<'_, T> {
/// `(ptr, end_or_len)`, read without calls, for the proofs in
/// `str::pattern`.
pub(crate) fn kani_raw_parts(&self) -> (*const T, *const T) {
// SAFETY: `NonNull<T>` is a transparent `*const T`.
(unsafe { mem::transmute::<NonNull<T>, *const T>(self.ptr) }, self.end_or_len)
}

/// The same, for the loop invariants in `str::pattern`: a loop invariant
/// must not call a function that other code also calls.
pub(crate) fn kani_loop_raw_parts(&self) -> (*const T, *const T) {
// SAFETY: `NonNull<T>` is a transparent `*const T`.
(unsafe { mem::transmute::<NonNull<T>, *const T>(self.ptr) }, self.end_or_len)
}
}

#[unstable(feature = "ub_checks", issue = "none")]
impl<T> Invariant for Iter<'_, T> {
/// An iterator can be safely used if its pointer can be read for its current length.
Expand Down
Loading
Loading