diff --git a/library/core/src/str/iter.rs b/library/core/src/str/iter.rs index 472ce896a059f..41df47042d67f 100644 --- a/library/core/src/str/iter.rs +++ b/library/core/src/str/iter.rs @@ -1641,3 +1641,992 @@ macro_rules! escape_types_impls { } escape_types_impls!(EscapeDebug, EscapeDefault, EscapeUnicode); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use super::super::pattern::verify::{ + any_char_searcher, cs_finger, cs_finger_back, cs_needle, type_invariant_cs, + }; + use super::super::validations::{utf8_char_width, utf8_is_cont_byte}; + use super::*; + + // ================================================================= + // Challenge 22: verify safety of str iter functions. + // + // Every harness runs the real, unmodified iterator code; no product + // code path is compiled out under Kani. The proofs are unbounded in + // the two dimensions the challenge cares about: + // + // - String length. The haystack is a symbolic-length slice of an + // arbitrary byte array constrained to valid UTF-8 by a loop-free + // byte-table predicate (`any_utf8` below); every valid + // UTF-8 string of at most HAY_MAX bytes — contents, length and + // character widths all symbolic — is one input. HAY_MAX is the + // size of the symbolic backing allocation, a CBMC memory-model + // parameter (as `ARR_SIZE` in + // `str::validations::verify::check_run_utf8_validation`); no loop + // is unwound to it. + // - Iterator state. Following the Challenge 20 methodology, each + // iterator type has a type invariant `C`; a base-case harness + // shows the constructors establish `C`, and every method harness + // starts from an *arbitrary* `C`-satisfying state (a superset of + // the states any call sequence reaches), runs the method, asserts + // the safety facts the unsafe blocks rely on (`str::get_unchecked` + // only checks bounds, so char-boundary-ness of every produced + // index and slice is asserted explicitly) and re-asserts `C`. + // + // The pattern searchers. The `SplitInternal`/`MatchesInternal`/ + // `MatchIndicesInternal` bodies contain no loops; every loop they can + // reach is inside `CharSearcher::next_match`/`next_match_back` + // (`str::pattern`). Challenge 22 assumption 2 allows assuming the + // safety and functional correctness of everything in `pattern.rs`; + // these harnesses assume strictly less than that: the two methods are + // replaced (`#[kani::stub_verified]`) by their *function contract*, + // which is the `Searcher` trait's documented guarantee (indices on + // char boundaries) plus the struct's documented finger invariant, is + // attached to the real, byte-identical method bodies, and is checked + // against those bodies by `pattern::verify::verify_cs_next_match`/ + // `verify_cs_next_match_back` (`#[kani::proof_for_contract]`). Under + // `stub_verified` each call site asserts the contract's precondition + // (`C` for the searcher) and assumes its postcondition; nothing about + // boundaries is `kani::assume`d by these harnesses. Lifting the + // searcher loops themselves with loop contracts is not possible with + // the pinned Kani: the slice comparison inside them lowers to CBMC's + // builtin `memcmp`, whose locals fail the loop-contract assigns check, + // and neither the `compare_bytes` intrinsic ("invalid stub: function + // does not have a body") nor `<[u8] as PartialEq>::eq` ("unable to + // find implementation ... for [u8]") can be stubbed around it. The + // contract proofs in `pattern::verify` therefore keep Challenge 20's + // bounded haystack; that bound is the one accepted limitation of + // this suite and it lives entirely inside Challenge 20's scope. + // + // `Chars::advance_by` is the only target function with loops. Its + // harness is unbounded in string length and bounded only in the + // advance count `n` (`ADVANCE_MAX`); every unwind bound derives from + // `ADVANCE_MAX` and the constant chunk size, never from the string + // length. See `check_chars_advance_by` for why loop contracts cannot + // be applied to those loops with the pinned Kani. + // + // Harness-writing rules (both consequences of CI's `-Z loop-contracts`): + // never filter inputs through `from_utf8` (its loop invariants make + // the result unreliable), and never reach a `#[safety::loop_invariant]` + // (`from_utf8`, `is_ascii`, `chars().count()`, ...) from a harness, + // which silently switches it into loop-contract mode. Equality of + // string slices is checked by pointer and length (`same_str`) rather + // than `==`, which lowers to `memcmp` over the whole slice. + // ================================================================= + + /// Maximum haystack length in bytes: the size of the symbolic backing + /// allocation, not a loop bound (see the module comment). Haystack + /// lengths range over `0..=HAY_MAX`; 256 keeps every harness within + /// a few minutes under CI's flags (at 1000 the loop-free harnesses + /// take about 2 minutes each run alone, ~11x the time at 256, and + /// `check_chars_advance_by` did not finish within an hour). + // TODO: HAY_MAX can be much larger with cbmc argument `--arrays-uf-always` + const HAY_MAX: usize = 256; + /// Size of the backing array behind a `HAY_MAX`-byte haystack. + const HAY_ARR: usize = HAY_MAX + PAD; + + // ------------------------------------------------------------------ + // Symbolic-length UTF-8 inputs: a self-contained copy of the + // byte-table input model also used by the Challenge 21 proofs (#538), + // so this module depends only on the Challenge 20 contracts. + // ------------------------------------------------------------------ + + /// Extra bytes past the maximum length so the byte-table predicates + /// may read up to four bytes after any index `< MAX` without leaving + /// the backing array. + const PAD: usize = 4; + + /// The byte-table definition of "`arr[..len]` is valid UTF-8", as two + /// facts local to a 4-byte window and quantified over every index of + /// the backing array (`i >= len` positions are vacuous): + /// + /// - U-lead: every non-continuation byte at `i` is a valid leading + /// byte (`<0x80`, `0xC2..=0xDF`, `0xE0..=0xEF`, `0xF0..=0xF4`) of + /// width `w`, its `w - 1` continuation bytes are present (with the + /// second-byte restrictions for `E0`/`ED`/`F0`/`F4`: no overlong + /// forms, no surrogates, nothing above U+10FFFF), `i + w <= len`, + /// and the byte at `i + w` is a leading byte or the end of the + /// string. + /// - U-cover: every byte lies within three bytes after a + /// non-continuation byte (at `i = 0`: the first byte leads). + /// + /// Both are properties of every valid UTF-8 string, so assuming them + /// is sound; together they are equivalent to `from_utf8(..).is_ok()` + /// (U-cover at 0 starts the parse on a leading byte, U-lead makes + /// each step a valid sequence that lands on the next leading byte or + /// exactly on `len`), which justifies `from_utf8_unchecked` in + /// `any_utf8`. `from_utf8` itself is not used as the filter because + /// under CI's `-Z loop-contracts` the invariants in + /// `run_utf8_validation` abstract its loops and its result no longer + /// constrains the bytes. + /// + /// The quantifier bodies are deliberately branch-free (bitwise `&`/`|`, + /// indicator arithmetic, no helper calls, no nested closures): CBMC + /// instantiates a quantifier body as one expression, and control flow + /// or statement expressions inside it are rejected or blow up + /// instrumentation. Every read stays inside the backing array because + /// of `PAD`. + fn utf8_local(arr: &[u8; N], len: usize) -> bool { + let p = arr.as_ptr(); + let lead = crate::forall!(|i in (0, N - PAD)| unsafe { + let i: usize = i; + let b0 = *p.wrapping_add(i); + let b1 = *p.wrapping_add(i.wrapping_add(1)); + let b2 = *p.wrapping_add(i.wrapping_add(2)); + let b3 = *p.wrapping_add(i.wrapping_add(3)); + let c0 = (b0 as i8) < -64; + let c1 = (b1 as i8) < -64; + let c2 = (b2 as i8) < -64; + let c3 = (b3 as i8) < -64; + // width of the sequence led by b0 (0: not a valid leading byte) + let w: usize = (b0 < 0x80) as usize + + (((b0 >= 0xC2) & (b0 < 0xE0)) as usize) * 2 + + (((b0 >= 0xE0) & (b0 < 0xF0)) as usize) * 3 + + (((b0 >= 0xF0) & (b0 < 0xF5)) as usize) * 4; + let cw = (*p.wrapping_add(i.wrapping_add(w)) as i8) < -64; + let sec = ((b0 != 0xE0) | (b1 >= 0xA0)) + & ((b0 != 0xED) | (b1 < 0xA0)) + & ((b0 != 0xF0) | (b1 >= 0x90)) + & ((b0 != 0xF4) | (b1 < 0x90)); + (i >= len) + | c0 + | ((w != 0) + & (i.wrapping_add(w) <= len) + & ((w < 2) | (c1 & sec)) + & ((w < 3) | c2) + & ((w < 4) | c3) + & ((i.wrapping_add(w) == len) | !cw)) + }); + let cover = crate::forall!(|i in (0, N - PAD)| unsafe { + let i: usize = i; + (i >= len) + | ((*p.wrapping_add(i) as i8) >= -64) + | ((i >= 1) & ((*p.wrapping_add(i.saturating_sub(1)) as i8) >= -64)) + | ((i >= 2) & ((*p.wrapping_add(i.saturating_sub(2)) as i8) >= -64)) + | ((i >= 3) & ((*p.wrapping_add(i.saturating_sub(3)) as i8) >= -64)) + }); + lead && cover + } + + /// An arbitrary valid UTF-8 string of symbolic length `0..=N - PAD` + /// backed by a caller-owned array of arbitrary content. + fn any_utf8(arr: &[u8; N]) -> &str { + let len: usize = kani::any(); + kani::assume(len <= N - PAD); + kani::assume(utf8_local(arr, len)); + // SAFETY: `utf8_local` is the byte-table definition of UTF-8 + // validity (see its documentation). + unsafe { crate::str::from_utf8_unchecked(&arr[..len]) } + } + + /// An arbitrary haystack: a valid UTF-8 string of symbolic length + /// `0..=N - PAD` (contents, length and character widths symbolic), + /// via the byte-table input model `utf8_local`/`any_utf8` above (see + /// `utf8_local` for why `from_utf8` cannot be the filter). + fn any_haystack(arr: &[u8; N]) -> &str { + let s = any_utf8(arr); + kani::cover(s.len() == N - PAD, "a haystack of the maximum length"); + s + } + + /// Identity of two string slices (same address and length). Used + /// instead of `==`, which lowers to `memcmp` over the whole slice. + fn same_str(a: &str, b: &str) -> bool { + a.as_ptr() == b.as_ptr() && a.len() == b.len() + } + + /// Byte offset of `sub` inside `s`; `sub` must be a subslice of `s`. + fn offset_in(s: &str, sub: &str) -> usize { + sub.as_ptr().addr() - s.as_ptr().addr() + } + + /// An arbitrary in-bounds char-boundary window `k..m` of `s`. + fn any_window(s: &str) -> (usize, usize) { + let k: usize = kani::any(); + let m: usize = kani::any(); + kani::assume(k <= m && m <= s.len()); + kani::assume(s.is_char_boundary(k) && s.is_char_boundary(m)); + (k, m) + } + + /// The window `k..m` of `s` as returned by `any_window`. + fn window(s: &str, k: usize, m: usize) -> &str { + // SAFETY: `any_window` assumed `k <= m <= s.len()` and that both + // are char boundaries. + unsafe { s.get_unchecked(k..m) } + } + + // ------------------------------------------------------------------ + // Chars + // + // Type invariant: the iterator's bytes are a char-boundary window of + // a valid UTF-8 string (the `str` invariant `Chars` documents). Every + // state reachable by `next`/`next_back`/`advance_by` from `s.chars()` + // is such a window, and every window is reachable as + // `s[k..m].chars()`, so the harnesses start from an arbitrary window. + // ------------------------------------------------------------------ + + /// `Chars::next`: the real `next_code_point` (whose + /// `char::from_u32_unchecked` result Kani checks for validity) on an + /// arbitrary window; the consumed prefix is one whole character. + #[kani::proof] + pub fn check_chars_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut it = w.chars(); + match it.next() { + Some(c) => { + let rest = it.as_str(); + assert!(rest.len() + c.len_utf8() == w.len()); + assert!(offset_in(s, rest) == k + c.len_utf8()); + assert!(s.is_char_boundary(k + c.len_utf8())); + kani::cover(c.len_utf8() == 1, "1-byte char consumed"); + kani::cover(c.len_utf8() == 2, "2-byte char consumed"); + kani::cover(c.len_utf8() == 3, "3-byte char consumed"); + kani::cover(c.len_utf8() == 4, "4-byte char consumed"); + } + None => { + assert!(w.is_empty()); + kani::cover(true, "empty window"); + } + } + } + + /// `Chars::next_back`: the real `next_code_point_reverse` on an + /// arbitrary window; the consumed suffix is one whole character. + #[kani::proof] + pub fn check_chars_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut it = w.chars(); + match it.next_back() { + Some(c) => { + let rest = it.as_str(); + assert!(rest.len() + c.len_utf8() == w.len()); + assert!(offset_in(s, rest) == k); + assert!(s.is_char_boundary(m - c.len_utf8())); + kani::cover(c.len_utf8() == 1, "1-byte char consumed"); + kani::cover(c.len_utf8() == 2, "2-byte char consumed"); + kani::cover(c.len_utf8() == 3, "3-byte char consumed"); + kani::cover(c.len_utf8() == 4, "4-byte char consumed"); + } + None => { + assert!(w.is_empty()); + kani::cover(true, "empty window"); + } + } + } + + /// `Chars::as_str` (`from_utf8_unchecked` over the iterator's bytes) + /// on an arbitrary window, and again after consuming from both ends. + #[kani::proof] + pub fn check_chars_as_str() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut it = w.chars(); + assert!(same_str(it.as_str(), w)); + let front = it.next().map_or(0, char::len_utf8); + let back = it.next_back().map_or(0, char::len_utf8); + let rest = it.as_str(); + assert!(offset_in(s, rest) == k + front); + assert!(rest.len() + front + back == w.len()); + assert!(s.is_char_boundary(k + front) && s.is_char_boundary(m - back)); + kani::cover(front > 0 && back > 0, "consumed from both ends"); + } + + /// Advance-count bound of `check_chars_advance_by`, the per-character + /// path of `Chars::advance_by` (counts below `CHUNK_SIZE` never enter + /// the chunk-skip phase). + const ADVANCE_MAX: usize = 8; + /// Backing-array size of `check_chars_advance_by`. Its per-character + /// loop is unwound, so unlike the loop-free harnesses its memory use + /// grows with the array (measured peak RSS: 4.8 GB at HAY_MAX, 1.8 GB + /// at 128); 128 keeps it inside the budget of CI's macOS runners. + /// Like HAY_MAX it is the size of the symbolic backing allocation, + /// not a loop bound. + const ADVANCE_HAY_MAX: usize = 128; + const ADVANCE_ARR: usize = ADVANCE_HAY_MAX + PAD; + /// Advance-count range of `check_chars_advance_by_chunked`, the + /// chunk-skip path: at least 33 so the chunk-skip loop body runs (it + /// runs while more than 32 characters remain to be skipped and a full + /// 32-byte chunk is available), at most 40 so it runs exactly once (a + /// 32-byte chunk of valid UTF-8 holds at least 8 characters, so + /// afterwards at most 32 remain and the guard fails). + const CHUNKED_MIN: usize = 33; + const CHUNKED_MAX: usize = 40; + /// String length of `check_chars_advance_by_chunked`: one full 32-byte + /// chunk plus a 16-byte tail. The length is a compile-time constant + /// (the contents are fully symbolic) because CBMC only drops the + /// unrolled copies of the chunk-skip loop when the chunk iterator's + /// end is known at unwinding time: each copy of that loop body reads + /// a whole chunk at a symbolic offset and runs two 32-iteration + /// loops, and with a symbolic string length -- or a symbolic start of + /// a fixed-length window -- the 33 copies the unwind bound implies + /// exceed 11 GB of RSS (measured). So the chunk-skip path is verified for every + /// 48-byte string; the per-character path (`check_chars_advance_by`) + /// for arbitrary windows of strings of arbitrary length. + const CHUNKED_WINDOW: usize = 48; + const _: () = assert!(ADVANCE_MAX <= WALK_MAX && CHUNKED_MAX <= WALK_MAX); + /// Number of unrolled steps in `walk`. + const WALK_MAX: usize = 40; + + /// Reference for `advance_by`: the position reached by skipping up to + /// `n <= WALK_MAX` characters from `off` (never past `m`) and the + /// number of characters skipped. Loop-free: `WALK_MAX` unrolled + /// conditional `utf8_char_width` steps, so it adds nothing to the + /// harness's unwind bound. + fn walk(bytes: &[u8], off: usize, m: usize, n: usize) -> (usize, usize) { + let mut off = off; + let mut steps = 0; + macro_rules! step { + () => { + if steps < n && off < m { + off += utf8_char_width(bytes[off]); + steps += 1; + } + }; + } + macro_rules! steps8 { + () => { + step!(); + step!(); + step!(); + step!(); + step!(); + step!(); + step!(); + step!(); + }; + } + // WALK_MAX = 5 * 8 steps + steps8!(); + steps8!(); + steps8!(); + steps8!(); + steps8!(); + (off, steps) + } + + /// Shared body of the two `advance_by` harnesses: the real + /// `Chars::advance_by` on the window `k..m` of `s` for the advance + /// count `n`, checked against `walk`. The remainder must start exactly + /// where the walk ends (and so on a char boundary); `Ok` iff `n` + /// characters were available, otherwise `Err(n - characters)`. + fn check_advance_by(s: &str, k: usize, m: usize, n: usize) -> (usize, usize) { + let bytes = s.as_bytes(); + let (off, steps) = walk(bytes, k, m, n); + + let mut it = window(s, k, m).chars(); + let res = it.advance_by(n); + let rest = it.as_str(); + assert!(offset_in(s, rest) == off); + assert!(rest.len() == m - off); + assert!(s.is_char_boundary(off)); + match res { + Ok(()) => { + assert!(steps == n); + kani::cover(n > 0, "advanced by a nonzero count"); + } + Err(rem) => { + assert!(off == m); + assert!(rem.get() == n - steps); + kani::cover(true, "ran out of characters"); + } + } + (off, steps) + } + + /// `Chars::advance_by`, per-character path: the real per-character + /// loop on an arbitrary window of a string of arbitrary length, for + /// counts up to `ADVANCE_MAX`. The unwind bound follows from + /// `ADVANCE_MAX` alone (the loop decrements `remainder` each + /// iteration); the string length plays no part in it. + /// + /// Loop contracts are not used on `advance_by`'s loops because, with + /// the pinned Kani, the invariant of a loop that advances a + /// `slice::Iter` through a method call cannot be stated: loop-modifies + /// inference misses fields written by callees (Kani reference, loop + /// contracts, limitations), and after the iterator is havocked its + /// `len()`/`as_slice()` trip the same-allocation check in Kani's + /// `ptr_offset_from` model before an invariant could re-pin it. + #[kani::proof] + #[kani::unwind(9)] + pub fn check_chars_advance_by() { + let arr: [u8; ADVANCE_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let n: usize = kani::any(); + kani::assume(n <= ADVANCE_MAX); + let (off, _) = check_advance_by(s, k, m, n); + kani::cover(n > 0 && off - k == 4 * n, "skipped only 4-byte characters"); + } + + /// `Chars::advance_by`, chunk-skip path: the real chunk-skip loop (its + /// body runs exactly once for these counts, see `CHUNKED_MAX`), the + /// trailing-continuation loop and the per-character loop, on a + /// `CHUNKED_WINDOW`-byte string of arbitrary contents. The unwind + /// bound is 34: the two loops over a chunk run 32 times, the + /// per-character loop at most 16 times (the bytes left after the + /// chunk), the trailing-continuation loop at most 3 (a character has + /// at most 3 continuation bytes); CBMC's unwinding assertions check + /// these counts rather than assume them. + #[kani::proof] + #[kani::unwind(34)] + pub fn check_chars_advance_by_chunked() { + let arr: [u8; CHUNKED_WINDOW + PAD] = kani::any(); + kani::assume(utf8_local(&arr, CHUNKED_WINDOW)); + // SAFETY: `utf8_local` is the byte-table definition of UTF-8 + // validity of `arr[..CHUNKED_WINDOW]` (see its documentation). + let s = unsafe { from_utf8_unchecked(&arr[..CHUNKED_WINDOW]) }; + let bytes = s.as_bytes(); + let n: usize = kani::any(); + kani::assume(CHUNKED_MIN <= n && n <= CHUNKED_MAX); + check_advance_by(s, 0, CHUNKED_WINDOW, n); + kani::cover( + utf8_is_cont_byte(bytes[32]), + "trailing-continuation loop skipped a byte after the chunk", + ); + kani::cover( + bytes[0] >= 0xF0 + && bytes[4] >= 0xF0 + && bytes[8] >= 0xF0 + && bytes[12] >= 0xF0 + && bytes[16] >= 0xF0 + && bytes[20] >= 0xF0 + && bytes[24] >= 0xF0 + && bytes[28] >= 0xF0, + "chunk of eight 4-byte characters (the fewest a chunk can hold)", + ); + kani::cover(bytes[0] < 0x80 && bytes[31] < 0x80, "chunk starting and ending in ASCII"); + } + + // ------------------------------------------------------------------ + // SplitInternal<'_, char> + // + // Type invariant `C`: the searcher satisfies its own invariant, the + // unconsumed range `start..end` is a char-boundary range of the + // haystack, and the searcher's fingers lie within it + // (`start <= finger` and `finger_back <= end`). The constructors + // establish it (`check_split_constructors_establish_invariant`); every + // reachable state in fact has `start == finger`, and `finger_back == + // end` except after `next_back_inclusive` (which leaves `end` at the + // match end while `finger_back` is at its start), so the arbitrary + // `C`-states below are a superset of the reachable ones. + // ------------------------------------------------------------------ + + /// Type invariant `C` of `SplitInternal<'_, char>`. + fn split_invariant(it: &SplitInternal<'_, char>) -> bool { + let h = it.matcher.haystack(); + type_invariant_cs(&it.matcher) + && it.start <= cs_finger(&it.matcher) + && cs_finger_back(&it.matcher) <= it.end + && it.end <= h.len() + && h.is_char_boundary(it.start) + && h.is_char_boundary(it.end) + } + + /// An arbitrary `C`-satisfying `SplitInternal` over `s` with a + /// symbolic `char` pattern and symbolic flags. + fn any_split(s: &str) -> SplitInternal<'_, char> { + let it = SplitInternal { + start: kani::any(), + end: kani::any(), + matcher: any_char_searcher(s), + allow_trailing_empty: kani::any(), + finished: kani::any(), + }; + kani::assume(split_invariant(&it)); + it + } + + /// Snapshot of the parts of a `SplitInternal` state that a method must + /// leave alone, checked after the call. + struct SplitFrame { + start: usize, + end: usize, + finger: usize, + finger_back: usize, + needle: char, + } + + fn split_frame(it: &SplitInternal<'_, char>) -> SplitFrame { + SplitFrame { + start: it.start, + end: it.end, + finger: cs_finger(&it.matcher), + finger_back: cs_finger_back(&it.matcher), + needle: cs_needle(&it.matcher), + } + } + + /// `part` is the char-boundary range `lo..hi` of `s` (by address). + fn assert_is_range(s: &str, part: &str, lo: usize, hi: usize) { + assert!(offset_in(s, part) == lo); + assert!(lo + part.len() == hi); + assert!(hi <= s.len()); + assert!(s.is_char_boundary(lo) && s.is_char_boundary(hi)); + } + + /// Criterion 1: `split`, `split_terminator` and `split_inclusive` + /// establish `C`. + #[kani::proof] + pub fn check_split_constructors_establish_invariant() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let p: char = kani::any(); + let a = s.split(p).0; + assert!(split_invariant(&a) && a.start == 0 && a.end == s.len() && !a.finished); + let b = s.split_terminator(p).0; + assert!(split_invariant(&b) && b.start == 0 && b.end == s.len() && !b.finished); + let c = s.split_inclusive(p).0; + assert!(split_invariant(&c) && c.start == 0 && c.end == s.len() && !c.finished); + } + + /// `SplitInternal::next` from an arbitrary `C`-state: the fragment is + /// `start..a` for the match `a..b` the searcher contract returns, the + /// new `start` is `b`, and on exhaustion `get_end` yields + /// `start..end` at most once. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_split_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + match it.next() { + Some(part) => { + assert!(!finished); + if it.finished { + assert_is_range(s, part, f.start, f.end); + assert!(it.start == f.start); + kani::cover(true, "next: trailing fragment from get_end"); + } else { + let a = f.start + part.len(); + assert_is_range(s, part, f.start, a); + assert!(a >= f.finger); + assert!(it.start == a + f.needle.len_utf8()); + assert!(it.start == cs_finger(&it.matcher)); + kani::cover(part.is_empty(), "next: empty fragment between adjacent matches"); + kani::cover(!part.is_empty(), "next: nonempty fragment"); + } + } + None => { + assert!(it.finished); + kani::cover(finished, "next: already finished"); + kani::cover(!finished, "next: exhausted without a trailing fragment"); + } + } + assert!(split_invariant(&it)); + assert!(it.end == f.end); + assert!(cs_finger_back(&it.matcher) == f.finger_back); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::next_inclusive` from an arbitrary `C`-state: the + /// fragment is `start..b` and the new `start` is `b`. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_split_next_inclusive() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + match it.next_inclusive() { + Some(part) => { + assert!(!finished); + if it.finished { + assert_is_range(s, part, f.start, f.end); + assert!(it.start == f.start); + kani::cover(true, "next_inclusive: trailing fragment from get_end"); + } else { + let b = f.start + part.len(); + assert_is_range(s, part, f.start, b); + assert!(part.len() >= f.needle.len_utf8()); + assert!(it.start == b); + assert!(it.start == cs_finger(&it.matcher)); + kani::cover( + part.len() == f.needle.len_utf8(), + "next_inclusive: fragment is just the separator", + ); + kani::cover( + part.len() > f.needle.len_utf8(), + "next_inclusive: fragment with content before the separator", + ); + } + } + None => { + assert!(it.finished); + kani::cover(finished, "next_inclusive: already finished"); + kani::cover(!finished, "next_inclusive: exhausted without a trailing fragment"); + } + } + assert!(split_invariant(&it)); + assert!(it.end == f.end); + assert!(cs_finger_back(&it.matcher) == f.finger_back); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::next_back` from an arbitrary `C`-state, including + /// the `allow_trailing_empty == false` path that first calls itself + /// to drop an empty trailing fragment: every fragment is a + /// char-boundary sub-range of the unconsumed range, `end` only + /// decreases, and `start` is untouched. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_split_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + let trailing = it.allow_trailing_empty; + match it.next_back() { + Some(part) => { + assert!(!finished); + let lo = offset_in(s, part); + let hi = lo + part.len(); + assert!(f.start <= lo && hi <= f.end); + assert!(s.is_char_boundary(lo) && s.is_char_boundary(hi)); + if it.finished { + // the final fragment `start..end` (of the range as it + // was when the searcher ran out of matches) + assert!(lo == f.start); + kani::cover(true, "next_back: final fragment"); + } else { + // `b..end` for a match `a..b` at or after `finger`; + // `end` becomes `a` + assert!(lo > f.finger); + assert!(it.end == cs_finger_back(&it.matcher)); + assert!(it.end + f.needle.len_utf8() == lo); + kani::cover(part.is_empty(), "next_back: empty fragment"); + kani::cover(!part.is_empty(), "next_back: nonempty fragment"); + } + kani::cover( + !trailing && !part.is_empty(), + "next_back: fragment returned with allow_trailing_empty == false", + ); + } + None => { + assert!(it.finished); + kani::cover(finished, "next_back: already finished"); + kani::cover( + !finished && !trailing, + "next_back: only an empty trailing fragment remained", + ); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start); + assert!(it.end <= f.end); + assert!(cs_finger(&it.matcher) == f.finger); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::next_back_inclusive` from an arbitrary `C`-state: + /// as `next_back`, but `end` becomes the match end `b` (so + /// `finger_back < end` afterwards, which `C` allows). + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_split_next_back_inclusive() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + let trailing = it.allow_trailing_empty; + match it.next_back_inclusive() { + Some(part) => { + assert!(!finished); + let lo = offset_in(s, part); + let hi = lo + part.len(); + assert!(f.start <= lo && hi <= f.end); + assert!(s.is_char_boundary(lo) && s.is_char_boundary(hi)); + if it.finished { + assert!(lo == f.start); + kani::cover(true, "next_back_inclusive: final fragment"); + } else { + assert!(it.end == lo); + assert!(cs_finger_back(&it.matcher) + f.needle.len_utf8() == lo); + kani::cover(part.is_empty(), "next_back_inclusive: empty fragment"); + kani::cover(!part.is_empty(), "next_back_inclusive: nonempty fragment"); + } + kani::cover( + !trailing && !part.is_empty(), + "next_back_inclusive: fragment returned with allow_trailing_empty == false", + ); + } + None => { + assert!(it.finished); + kani::cover(finished, "next_back_inclusive: already finished"); + kani::cover( + !finished && !trailing, + "next_back_inclusive: only an empty trailing fragment remained", + ); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start); + assert!(it.end <= f.end); + assert!(cs_finger(&it.matcher) == f.finger); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::get_end` from an arbitrary `C`-state, called + /// directly: on an unfinished iterator it finishes it and returns + /// `start..end` iff a trailing empty fragment is allowed or the range + /// is nonempty; on a finished one it is a no-op returning `None`. + #[kani::proof] + pub fn check_split_get_end() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + let trailing = it.allow_trailing_empty; + let res = it.get_end(); + assert!(it.finished); + match res { + Some(part) => { + assert!(!finished); + assert!(trailing || f.end > f.start); + assert_is_range(s, part, f.start, f.end); + kani::cover( + trailing && part.is_empty(), + "get_end: empty trailing fragment allowed", + ); + kani::cover( + !trailing && !part.is_empty(), + "get_end: nonempty fragment, trailing empty disallowed", + ); + } + None => { + assert!(finished || (!trailing && f.end == f.start)); + kani::cover(finished, "get_end: already finished"); + kani::cover(!finished, "get_end: empty trailing fragment suppressed"); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start && it.end == f.end); + assert!(cs_finger(&it.matcher) == f.finger && cs_finger_back(&it.matcher) == f.finger_back); + } + + /// `SplitInternal::remainder` from an arbitrary `C`-state: `None` iff + /// finished, else `start..end`; the state is untouched. + #[kani::proof] + pub fn check_split_remainder() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let it = any_split(s); + let f = split_frame(&it); + match it.remainder() { + Some(rem) => { + assert!(!it.finished); + assert_is_range(s, rem, f.start, f.end); + kani::cover(rem.is_empty(), "remainder: empty"); + kani::cover(!rem.is_empty(), "remainder: nonempty"); + } + None => { + assert!(it.finished); + kani::cover(true, "remainder: finished"); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start && it.end == f.end); + } + + // ------------------------------------------------------------------ + // MatchIndicesInternal / MatchesInternal + // + // Type invariant: the wrapped searcher satisfies its own invariant + // (nothing else is stored). Arbitrary `C`-states are produced by + // `any_char_searcher`. + // ------------------------------------------------------------------ + + /// `MatchIndicesInternal::next`: the returned index is the match + /// start, a char boundary, and the slice is the match. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_match_indices_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchIndicesInternal<'_, char> = MatchIndicesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next() { + Some((i, m)) => { + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger(&it.0) == i + m.len()); + kani::cover(m.len() > 1, "match_indices next: multibyte match"); + kani::cover(i > 0, "match_indices next: match after the start"); + } + None => { + assert!(cs_finger(&it.0) == finger_back); + kani::cover(true, "match_indices next: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger_back(&it.0) == finger_back && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + /// `MatchIndicesInternal::next_back`: as `next`, searching backwards. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_match_indices_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchIndicesInternal<'_, char> = MatchIndicesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next_back() { + Some((i, m)) => { + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger_back(&it.0) == i); + kani::cover(m.len() > 1, "match_indices next_back: multibyte match"); + kani::cover( + i + m.len() < finger_back, + "match_indices next_back: match before the end", + ); + } + None => { + assert!(cs_finger_back(&it.0) == finger); + kani::cover(true, "match_indices next_back: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger(&it.0) == finger && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + /// `MatchesInternal::next`: the returned slice is the match. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_matches_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchesInternal<'_, char> = MatchesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next() { + Some(m) => { + let i = offset_in(s, m); + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger(&it.0) == i + m.len()); + kani::cover(m.len() > 1, "matches next: multibyte match"); + } + None => { + assert!(cs_finger(&it.0) == finger_back); + kani::cover(true, "matches next: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger_back(&it.0) == finger_back && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + /// `MatchesInternal::next_back`: as `next`, searching backwards. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_matches_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchesInternal<'_, char> = MatchesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next_back() { + Some(m) => { + let i = offset_in(s, m); + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger_back(&it.0) == i); + kani::cover(m.len() > 1, "matches next_back: multibyte match"); + } + None => { + assert!(cs_finger_back(&it.0) == finger); + kani::cover(true, "matches next_back: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger(&it.0) == finger && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + // ------------------------------------------------------------------ + // SplitAsciiWhitespace + // + // Type invariant: the inner `slice::Split`'s unconsumed slice `v` is a + // char-boundary window of the string. `split_ascii_whitespace` + // starts with the whole string; each `next` (`next_back`) cuts `v` + // after (before) an ASCII-whitespace byte, which is a one-byte + // character, so every reachable `v` is such a window, and every + // window is one `C`-state. + // ------------------------------------------------------------------ + + /// `SplitAsciiWhitespace::remainder` (`from_utf8_unchecked` over `v`) + /// on the fresh iterator and on an arbitrary `C`-state. + #[kani::proof] + pub fn check_split_ascii_whitespace_remainder() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = s.split_ascii_whitespace(); + assert!(it.remainder().is_some_and(|rem| same_str(rem, s))); + let (k, m) = any_window(s); + it.inner.iter.iter.v = window(s, k, m).as_bytes(); + it.inner.iter.iter.finished = kani::any(); + match it.remainder() { + Some(rem) => { + assert!(!it.inner.iter.iter.finished); + assert_is_range(s, rem, k, m); + kani::cover(!rem.is_empty(), "split_ascii_whitespace remainder: nonempty"); + } + None => { + assert!(it.inner.iter.iter.finished); + kani::cover(true, "split_ascii_whitespace remainder: finished"); + } + } + } + + // ------------------------------------------------------------------ + // Bytes + // ------------------------------------------------------------------ + + /// Contract harness for `Bytes::__iterator_get_unchecked`: its + /// `#[requires(idx < self.0.len())]` rules out UB in the body, for a + /// `Bytes` over any window of a string of arbitrary length. Under + /// CI's `--no-assert-contracts` a contract is only checked by a + /// `proof_for_contract` harness. + #[kani::proof_for_contract(Bytes::__iterator_get_unchecked)] + pub fn check_bytes_iterator_get_unchecked() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut bytes = w.bytes(); + let idx: usize = kani::any(); + let b = unsafe { bytes.__iterator_get_unchecked(idx) }; + assert!(b == w.as_bytes()[idx]); + kani::cover(idx > 0, "bytes get_unchecked: index past the start"); + } +} diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index ee6fd26ca0bfe..84613a05bf143 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -38,13 +38,14 @@ issue = "27721" )] -// Must match the `cfg` on `small_slice_eq`, the only user of these attributes. +// Must match the `cfg` on `small_slice_eq`, the only user of `loop_invariant`. #[cfg(any( all(target_arch = "x86_64", any(kani, target_feature = "sse2")), all(target_arch = "loongarch64", target_feature = "lsx"), all(target_arch = "aarch64", target_feature = "neon") ))] -use safety::{loop_invariant, requires}; +use safety::loop_invariant; +use safety::{ensures, requires}; use crate::cmp::Ordering; use crate::convert::TryInto as _; @@ -441,6 +442,30 @@ unsafe impl<'a> Searcher<'a> for CharSearcher<'a> { } } #[inline] + // Kani contract (a runtime no-op). `requires` restates the safety + // invariant documented on `CharSearcher`: both fingers are in-bounds + // char boundaries of the haystack (`into_searcher` establishes it and + // every method preserves it; see `verify`). `ensures` restates the + // `Searcher` guarantee this method gives its callers: a returned + // range is a needle-width range on char boundaries, at or after the + // finger on entry and within `finger_back`, and `finger` is left at + // its end; `None` leaves `finger` at `finger_back`. Only `finger` is + // written. Checked against this body by `verify::verify_cs_next_match`. + #[requires(self.finger <= self.finger_back + && self.finger_back <= self.haystack.len() + && self.haystack.is_char_boundary(self.finger) + && self.haystack.is_char_boundary(self.finger_back))] + #[ensures(|result| match *result { + Some((a, b)) => old(self.finger) <= a + && a < b + && b == self.finger + && b <= self.finger_back + && b - a == self.utf8_size() + && self.haystack.is_char_boundary(a) + && self.haystack.is_char_boundary(b), + None => self.finger == self.finger_back, + })] + #[cfg_attr(kani, kani::modifies(&self.finger))] fn next_match(&mut self) -> Option<(usize, usize)> { loop { // get the haystack after the last character found @@ -508,6 +533,26 @@ unsafe impl<'a> ReverseSearcher<'a> for CharSearcher<'a> { } } #[inline] + // Kani contract (a runtime no-op); see `next_match`. A returned range + // is a needle-width range on char boundaries, at or before the + // `finger_back` on entry and at or after `finger`, and `finger_back` + // is left at its start; `None` leaves `finger_back` at `finger`. Only + // `finger_back` is written. Checked by `verify::verify_cs_next_match_back`. + #[requires(self.finger <= self.finger_back + && self.finger_back <= self.haystack.len() + && self.haystack.is_char_boundary(self.finger) + && self.haystack.is_char_boundary(self.finger_back))] + #[ensures(|result| match *result { + Some((a, b)) => a == self.finger_back + && a < b + && b - a == self.utf8_size() + && b <= old(self.finger_back) + && self.finger <= a + && self.haystack.is_char_boundary(a) + && self.haystack.is_char_boundary(b), + None => self.finger_back == self.finger, + })] + #[cfg_attr(kani, kani::modifies(&self.finger_back))] fn next_match_back(&mut self) -> Option<(usize, usize)> { let haystack = self.haystack.as_bytes(); loop { @@ -2140,4 +2185,581 @@ pub mod verify { true ); } + + // ================================================================== + // Challenge 20: verify safety of char-related Searcher methods + // + // For each searcher type we define a type invariant `C` and prove the + // challenge's three criteria against the real, unmodified method + // bodies: + // 1. `into_searcher` establishes `C` (base-case harnesses); + // 2. `C` implies the Searcher safety property: every returned index + // pair lies on UTF-8 char boundaries (asserted on the values the + // real methods return); + // 3. every method preserves `C` (inductive-step harnesses that admit + // an arbitrary `C`-satisfying state — not just reachable ones — + // then run the real method and re-assert `C`). + // + // Accepted limitation: bounded haystack length. + // + // The challenge asks for proofs over haystacks of arbitrary size. + // These proofs are bounded in exactly one dimension: the haystack is + // at most `HAYSTACK_BYTES` bytes long, and every harness that runs a + // search loop carries the matching `#[kani::unwind]` bound. Within + // that bound the proofs are exhaustive: + // - every haystack: contents and length are symbolic, so every + // valid UTF-8 string of at most HAYSTACK_BYTES bytes, with every + // combination of the four UTF-8 width classes that fits, is one + // symbolic input; + // - every needle: an arbitrary `char` (`CharSearcher`) or + // `[char; 2]` (`MultiCharEqSearcher` and the wrappers); + // - every searcher state: the inductive-step harnesses start from + // an arbitrary `C`-satisfying state, a superset of the states any + // call sequence reaches, so they are unbounded in the number of + // calls made before the one under verification. + // + // Why HAYSTACK_BYTES = 5. A 4-byte (maximum-width) character plus one + // neighbour is the smallest haystack in which every case the search + // loops distinguish is reachable: every needle width; a memchr hit on + // a continuation byte that is *not* the end of the needle, which + // leaves `finger` mid-character for the next iteration (the + // `EA 81 81` case discussed in `CharSearcher::next_match`); a match + // preceded by such a false hit (a multi-iteration loop); the needle + // partially overlapping the end of the search window; and "found + // nothing". The `kani::cover`s in the harnesses witness that these + // arms execute. + // + // Why the unwind bounds are sound. Every iteration of every loop + // under verification moves a cursor by at least one byte + // (`finger += index + 1` / `finger_back = index` in the memchr loops; + // `next`/`next_back` consume one whole character in the trait + // defaults), so over a haystack of at most HAYSTACK_BYTES bytes a + // loop runs at most HAYSTACK_BYTES + 1 iterations and the bound + // HAYSTACK_BYTES + 2 unwinds it completely. Kani checks this: a bound + // that is too small fails the unwinding assertion rather than + // silently truncating the proof. + // + // Why the bound is not lifted with loop contracts. Four of the loops + // under verification are the generic `Searcher`/`ReverseSearcher` + // trait defaults (`next_match`, `next_reject`, `next_match_back`, + // `next_reject_back`), which loop over `self.next()`/`next_back()`. + // A loop invariant strong enough to re-enter `self.next()` safely + // must state the concrete searcher's `C`, which a generic trait body + // cannot name without changing shipped trait code. The unbounded + // argument for those loops is the inductive-step harnesses on + // `next`/`next_back` (the per-iteration lemma the loops need: one + // step from any `C`-state returns a boundary-valid range and + // re-establishes `C`) together with the bounded end-to-end harnesses + // that run the real default bodies. The two remaining loops, + // `CharSearcher::next_match`/`next_match_back`, are unwound within + // the same bound. Lifting it with a `#[safety::loop_invariant]` on + // those two loops was tried with the pinned Kani (branch + // `c20-loop-contracts-experiment` on the author's fork): with the + // invariant `finger <= finger_back && finger_back <= haystack.len()`, + // a symbolic-length haystack over a 16-byte backing array, and + // loop-free first/last-occurrence specifications of memchr/memrchr, + // every boundary assertion, the loop invariant and `C` verify in + // about 10 s per direction -- but the proofs cannot be merged: the + // slice comparison `slice == &self.utf8_encoded[..]` lowers to + // CBMC's builtin `memcmp`, whose internal locals are linked in after + // Kani's loop-modifies inference and so fail the loop-contract + // assigns check (four spurious "is assignable" failures per harness, + // nothing else). The comparison cannot be stubbed around it: the + // pinned Kani rejects a stub of the `compare_bytes` intrinsic + // ("invalid stub: function does not have a body, but is not an + // extern function") and cannot name the blanket `PartialEq` impl for + // `[u8]` (`<[u8] as crate::cmp::PartialEq<[u8]>>::eq`: "unable to + // find implementation of associated function `cmp::PartialEq::eq` + // for [u8]"), and an explicit `kani::loop_modifies` clause fails on + // the loop-body locals Kani hoists. That is a tool limitation to + // report upstream; the bounded proofs here are the shipped evidence. + // + // Contracts. `CharSearcher::next_match` and `next_match_back` carry + // their `Searcher` contract as `#[requires]`/`#[ensures]` attributes + // (runtime no-ops): the precondition is `C`, and the postcondition + // is the guarantee callers rely on -- a returned range is a + // needle-width range on char boundaries, at or after the finger on + // entry (at or before the `finger_back` on entry), and that finger + // is left at the range's end (start); `None` leaves the two fingers + // equal; nothing but that finger is written. `verify_cs_next_match` + // and `verify_cs_next_match_back` are the `#[kani::proof_for_contract]` + // harnesses that check the contract against the real bodies (within + // the bound above). This is what lets the `str` iterators (Challenge + // 22, `str::iter::verify`) compose with the searchers through + // `#[kani::stub_verified]` rather than assume anything about them. + // ================================================================== + + /// Maximum haystack length in bytes — the one accepted bound of these + /// proofs (see the section comment). 5 fits a 4-byte (maximum-width) + /// character plus a neighbour, so every UTF-8 width class and every + /// arm of the search loops is reachable. Every loop under + /// verification advances a cursor by at least one byte per iteration, + /// so an unwind bound of `HAYSTACK_BYTES + 2` (the `#[kani::unwind]` + /// literals below are at least that) unwinds it completely: at most + /// HAYSTACK_BYTES + 1 iterations, plus one for the unwinding + /// assertion. + const HAYSTACK_BYTES: usize = 5; + + /// An arbitrary UTF-8 string of 0..=N bytes written into a + /// caller-owned buffer, built constructively as a concatenation of + /// up to N symbolic `char`s — every valid UTF-8 string of at most N + /// bytes is reachable, multibyte characters included. Constructive + /// generation is used instead of filtering `kani::any()` bytes + /// through `from_utf8`, because under CI's `-Z loop-contracts` the + /// loop invariants inside `run_utf8_validation` abstract the + /// validator's loops, making its *functional* result unreliable as + /// a filter (and the constructive form is cheaper for the solver). + fn symbolic_str(buf: &mut [u8; N]) -> &str { + let mut len = 0usize; + let mut i = 0; + while i < N { + if kani::any() { + let c: char = kani::any(); + let w = c.len_utf8(); + if len + w <= N { + c.encode_utf8(&mut buf[len..]); + len += w; + } + } + i += 1; + } + // SAFETY: `buf[..len]` is a concatenation of UTF-8 encodings of + // `char`s, hence valid UTF-8 by construction. + unsafe { crate::str::from_utf8_unchecked(&buf[..len]) } + } + + // ------------------------------------------------------------------ + // Stub for memrchr. + // + // Challenge 20 allows assuming "the safety and functional correctness + // of all functions in the slice module", which covers + // `core::slice::memchr::{memchr,memrchr}`. Since #628, `memchr` under + // `cfg(kani)` is already the byte-by-byte scan `memchr_naive` + // (`library/core/src/slice/memchr.rs`), so `verify_cs_next_match` + // runs the real `cfg(kani)` path and needs no stub. `memrchr` has no + // `cfg(kani)` path (it wraps `memrchr_aligned`'s `align_to` word + // scan), so, following the stub pattern accepted in PR #544, + // `stub_memrchr` is a *semantically identical implementation* of the + // last-occurrence contract — no nondeterminism, no `kani::assume` — + // replacing only the optimized word-at-a-time scan, which CBMC + // unwinds poorly. The harness's unwind bound fully unwinds the linear + // scan, so the proof remains exhaustive. It is applied per-harness, + // only where the real call graph reaches memrchr + // (`CharSearcher::next_match_back`). + // ------------------------------------------------------------------ + + fn stub_memrchr(x: u8, text: &[u8]) -> Option { + let mut i = text.len(); + while i > 0 { + i -= 1; + if text[i] == x { + return Some(i); + } + } + None + } + + // ------------------------------------------------------------------ + // CharSearcher + // ------------------------------------------------------------------ + + /// Type invariant `C` for `CharSearcher` (the condition of challenge + /// criterion 2): both fingers are in-bounds char boundaries of the + /// haystack in the right order, and the needle metadata is the true + /// UTF-8 encoding of the needle. (Inside `next_match`/`next_match_back` + /// the fingers may transiently leave boundaries — the documented + /// mid-loop state — but every public method must restore `C` on exit, + /// which is exactly what these harnesses check.) + pub fn type_invariant_cs(s: &CharSearcher<'_>) -> bool { + let mut enc = [0u8; 4]; + let enc_len = s.needle.encode_utf8(&mut enc).len(); + s.finger <= s.finger_back + && s.finger_back <= s.haystack.len() + && s.haystack.is_char_boundary(s.finger) + && s.haystack.is_char_boundary(s.finger_back) + && s.utf8_size() == enc_len + // byte-wise rather than `==` on the slices, which lowers to + // CBMC's `memcmp` loop and would force an unwind bound on + // every harness that states `C` (`enc_len >= 1` always) + && s.utf8_encoded[0] == enc[0] + && (enc_len < 2 || s.utf8_encoded[1] == enc[1]) + && (enc_len < 3 || s.utf8_encoded[2] == enc[2]) + && (enc_len < 4 || s.utf8_encoded[3] == enc[3]) + } + + /// An arbitrary `CharSearcher` state satisfying `C` — the induction + /// hypothesis for the step harnesses. This covers every + /// `C`-satisfying state, a superset of the states reachable by call + /// sequences from `into_searcher` (whose base case is + /// `verify_cs_into_searcher`). + pub fn any_char_searcher(haystack: &str) -> CharSearcher<'_> { + let needle: char = kani::any(); + let mut utf8_encoded = [0u8; 4]; + let utf8_size = needle.encode_utf8(&mut utf8_encoded).len() as u8; + let finger: usize = kani::any(); + let finger_back: usize = kani::any(); + kani::assume(finger <= finger_back && finger_back <= haystack.len()); + kani::assume(haystack.is_char_boundary(finger)); + kani::assume(haystack.is_char_boundary(finger_back)); + CharSearcher { haystack, finger, finger_back, needle, utf8_size, utf8_encoded } + } + + /// Criterion 2's safety property for a returned index pair. + pub fn assert_valid_range(haystack: &str, a: usize, b: usize) { + assert!(a <= b && b <= haystack.len()); + assert!(haystack.is_char_boundary(a)); + assert!(haystack.is_char_boundary(b)); + } + + /// `CharSearcher::finger`, for invariants stated outside this module + /// (the fields are private to `str::pattern`). + pub fn cs_finger(s: &CharSearcher<'_>) -> usize { + s.finger + } + + /// `CharSearcher::finger_back`, for invariants stated outside this module. + pub fn cs_finger_back(s: &CharSearcher<'_>) -> usize { + s.finger_back + } + + /// `CharSearcher::needle`, for invariants stated outside this module. + pub fn cs_needle(s: &CharSearcher<'_>) -> char { + s.needle + } + + /// Criterion 1: `char::into_searcher` establishes `C`. + #[kani::proof] + #[kani::unwind(8)] + pub fn verify_cs_into_searcher() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let needle: char = kani::any(); + let searcher = needle.into_searcher(haystack); + assert!(type_invariant_cs(&searcher)); + assert!(searcher.finger == 0); + assert!(searcher.finger_back == haystack.len()); + } + + /// Criteria 2+3 for the real `CharSearcher::next`. + #[kani::proof] + #[kani::unwind(8)] + pub fn verify_cs_next() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "next returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "next returned Done"), + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for the real `CharSearcher::next_back`. + #[kani::proof] + #[kani::unwind(8)] + pub fn verify_cs_next_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next_back() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "next_back returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "next_back returned Done"), + } + assert!(type_invariant_cs(&s)); + } + + /// Contract proof for the real `CharSearcher::next_match` (the memchr + /// loop; under `cfg(kani)` core's `memchr` is the byte-by-byte scan + /// `memchr_naive` since #628, so it runs unstubbed) and criteria 2+3 + /// for it: Kani assumes + /// the `#[requires]` (which `any_char_searcher` establishes anyway), + /// checks the `#[ensures]` and the write set on return, and the body + /// re-asserts the boundary property and `C`. Every loop iteration + /// advances `finger` by at least one byte, so the unwind bound fully + /// unwinds the search. + #[kani::proof_for_contract(CharSearcher::next_match)] + #[kani::unwind(7)] + pub fn verify_cs_next_match() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next_match() { + Some((a, b)) => { + assert_valid_range(haystack, a, b); + assert!(b - a == s.utf8_size()); + kani::cover(true, "next_match found the needle"); + } + None => kani::cover(true, "next_match found nothing"), + } + assert!(type_invariant_cs(&s)); + } + + /// Contract proof for the real `CharSearcher::next_match_back` (the + /// memrchr loop, with memrchr replaced by the semantically identical + /// `stub_memrchr`) and criteria 2+3 for it, as `verify_cs_next_match`. + /// Every iteration decreases `finger_back` by at least one byte. + #[kani::proof_for_contract(CharSearcher::next_match_back)] + #[kani::unwind(7)] + #[kani::stub(crate::slice::memchr::memrchr, stub_memrchr)] + pub fn verify_cs_next_match_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next_match_back() { + Some((a, b)) => { + assert_valid_range(haystack, a, b); + assert!(b - a == s.utf8_size()); + kani::cover(true, "next_match_back found the needle"); + } + None => kani::cover(true, "next_match_back found nothing"), + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for `CharSearcher::next_reject` — the real trait + /// default, looping over the real `next()`. Each `next()` consumes at + /// least one byte, so the unwind bound fully unwinds the loop. + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_cs_next_reject() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + if let Some((a, b)) = s.next_reject() { + assert_valid_range(haystack, a, b); + kani::cover(true, "next_reject returned a range"); + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for `CharSearcher::next_reject_back` — the real trait + /// default over the real `next_back()`. + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_cs_next_reject_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + if let Some((a, b)) = s.next_reject_back() { + assert_valid_range(haystack, a, b); + kani::cover(true, "next_reject_back returned a range"); + } + assert!(type_invariant_cs(&s)); + } + + /// From-creation run to `Done`: every step of the real `next()` on a + /// freshly created searcher yields boundary-valid ranges and + /// preserves `C` (criteria 1+2+3 composed). + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_cs_search_to_done() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let needle: char = kani::any(); + let mut s = needle.into_searcher(haystack); + loop { + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b) + } + SearchStep::Done => break, + } + assert!(type_invariant_cs(&s)); + } + kani::cover(true, "searched the whole haystack"); + } + + // ------------------------------------------------------------------ + // MultiCharEqSearcher (and its four delegating wrapper searchers) + // ------------------------------------------------------------------ + + /// Type invariant `C` for `MultiCharEqSearcher`: the `CharIndices` + /// iterator views exactly the haystack subrange + /// `[front, front + rem)`, and both endpoints are char boundaries. + /// This is what makes the real `next`/`next_back` (and the trait + /// defaults built on them) return boundary-valid indices: `next()` + /// yields `front` and `next_back()` yields `front + rem` positions, + /// and `Chars`/`CharIndices` step through whole characters. + fn type_invariant_mces(s: &MultiCharEqSearcher<'_, C>) -> bool { + let front = s.char_indices.front_offset; + let rem = s.char_indices.iter.iter.len(); + front + rem <= s.haystack.len() + && s.haystack.is_char_boundary(front) + && s.haystack.is_char_boundary(front + rem) + && s.char_indices.iter.iter.as_slice().as_ptr().addr() + == s.haystack.as_ptr().addr() + front + } + + /// An arbitrary `C`-satisfying `MultiCharEqSearcher` state — the + /// induction hypothesis for the step harnesses. `char_eq.matches` is + /// a pure, safe predicate, so the safety argument is independent of + /// the concrete `MultiCharEq` instantiation; harnesses use + /// `[char; 2]`. + fn any_mces(haystack: &str) -> MultiCharEqSearcher<'_, [char; 2]> { + let k: usize = kani::any(); + let j: usize = kani::any(); + kani::assume(k <= j && j <= haystack.len()); + kani::assume(haystack.is_char_boundary(k)); + kani::assume(haystack.is_char_boundary(j)); + // SAFETY: k <= j <= len and both are char boundaries (assumed + // above); get_unchecked avoids dragging the slice-error panic + // machinery into the CBMC formula. + let sub = unsafe { haystack.get_unchecked(k..j) }; + let char_indices = crate::str::CharIndices { front_offset: k, iter: sub.chars() }; + let char_eq: [char; 2] = kani::any(); + MultiCharEqSearcher { char_eq, haystack, char_indices } + } + + /// Criterion 1: `into_searcher` establishes `C` for + /// `MultiCharEqSearcher`. + #[kani::proof] + pub fn verify_mces_into_searcher() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let chars: [char; 2] = kani::any(); + let searcher = MultiCharEqPattern(chars).into_searcher(haystack); + assert!(type_invariant_mces(&searcher)); + } + + /// Criteria 2+3 for the real `MultiCharEqSearcher::next`. + #[kani::proof] + pub fn verify_mces_next() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "mces next returned Done"), + } + assert!(type_invariant_mces(&s)); + } + + /// Criteria 2+3 for the real `MultiCharEqSearcher::next_back`. + #[kani::proof] + pub fn verify_mces_next_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + match s.next_back() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_back returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "mces next_back returned Done"), + } + assert!(type_invariant_mces(&s)); + } + + /// Criteria 2+3 for the four trait defaults on `MultiCharEqSearcher` + /// (`next_match`, `next_reject`, `next_match_back`, + /// `next_reject_back`) — the real default loops over the real + /// `next`/`next_back`. Each iteration consumes at least one byte. + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_match() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_match() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_match returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_reject() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_reject() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_reject returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_match_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_match_back() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_match_back returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_reject_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_reject_back() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_reject_back returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + /// The four remaining challenge searcher types + /// (`CharArraySearcher`, `CharArrayRefSearcher`, `CharSliceSearcher`, + /// `CharPredicateSearcher`) are `pattern_methods!` newtype delegations + /// to `MultiCharEqSearcher`, so their invariant is the wrapped + /// searcher's `C` and all six methods delegate to the code verified + /// above. These harnesses check the delegation itself end-to-end for + /// the array wrapper (the other three wrappers expand from the same + /// macro with a different `MultiCharEq` instance; `matches` is a pure + /// safe predicate in all four). + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_char_array_searcher_delegation() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let chars: [char; 2] = kani::any(); + let mut s = chars.into_searcher(haystack); + assert!(type_invariant_mces(&s.0)); + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b) + } + SearchStep::Done => {} + } + if let Some((a, b)) = s.next_match() { + assert_valid_range(haystack, a, b); + } + assert!(type_invariant_mces(&s.0)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_char_array_searcher_delegation_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let chars: [char; 2] = kani::any(); + let mut s = chars.into_searcher(haystack); + match s.next_back() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b) + } + SearchStep::Done => {} + } + if let Some((a, b)) = s.next_match_back() { + assert_valid_range(haystack, a, b); + } + assert!(type_invariant_mces(&s.0)); + } }