From b2b321da5a19739d159a394e19784d9b7df0517b Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Tue, 29 Sep 2026 18:12:10 +0300 Subject: [PATCH 1/8] Challenge 10: verify memory safety of String functions with Kani Adds a #[cfg(kani)] mod verify to library/alloc/src/string.rs with 16 harnesses covering all 15 functions of Challenge 10. No production code is changed. - Any length (symbolic len/cap up to CBMC's object limit, loop-free): pop, remove, insert, insert_str, split_off, drain (next and drop), into_boxed_str, leak. - Any receiver length, bounded edit/match count: replace_range (<= 4 bytes removed and inserted), remove_matches (<= 4 matches, most-general Searcher). - Bounded because of current Kani limitations (documented in the PR): retain (<= 12 chars), from_utf16le/from_utf16be/from_utf16be_lossy (<= 12 bytes), from_utf16le_lossy (<= 8 bytes). Written with AI assistance. --- library/alloc/src/string.rs | 387 ++++++++++++++++++++++++++++++++++++ 1 file changed, 387 insertions(+) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 4100ee55a4c7b..6e8dc6db2909d 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3606,3 +3606,390 @@ impl From for String { c.to_string() } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + //! Challenge 10: memory safety of `String` methods that are safe abstractions over unsafe code. + //! + //! Every harness in this module is loop-free, so no `#[kani::unwind]` bound is involved: + //! strings have a symbolic length and capacity, limited only by the largest object CBMC can + //! represent under `--object-bits 12` (see `MAX_ALLOC`). This covers the functions the + //! challenge marks "(U)" (`insert_str`, `split_off`) as well as the others. + //! + //! UTF-8 validity. None of these functions reads string contents except `pop`, `remove` and + //! the `Drain` iterator, which decode exactly one char. We model a `String` as arbitrary + //! bytes; where one char is decoded we place a well-formed encoding of an arbitrary `char` + //! at that position (`with_char_at`). Every valid `String` is an instance of this model + //! (`valid prefix ++ c ++ valid suffix`, and arbitrary bytes include every valid prefix and + //! suffix), so absence of UB for the model implies it for every valid `String`. Nothing is + //! assumed about the result of the function under test. + //! + //! Panics are not UB. Documented panic conditions (index not on a char boundary, removing + //! at the end) are excluded with `kani::assume`. + use core::cell::Cell; + use core::kani; + use core::str::pattern::{Pattern, SearchStep, Searcher}; + + use crate::string::String; + use crate::vec::Vec; + + /// Largest single allocation CBMC can represent with `--object-bits 12` (the setting used by + /// `scripts/run-kani.sh`): 52 offset bits, signed. A limit of the memory model, not a bound + /// chosen for tractability (2^51 bytes = 2 PiB). + const MAX_ALLOC: usize = (1usize << 51) - 1; + + /// A `String` with symbolic length and capacity whose bytes are arbitrary + /// (fresh heap memory is nondeterministic in CBMC; no loop is executed). + fn any_string_bytes() -> String { + let cap: usize = kani::any_where(|c: &usize| *c <= MAX_ALLOC); + let len: usize = kani::any_where(|l: &usize| *l <= cap); + let mut v: Vec = Vec::with_capacity(cap); + // SAFETY (harness): `len <= capacity`; see the module comment on contents. + unsafe { v.set_len(len) }; + // SAFETY (harness): see the module comment on UTF-8 validity. + unsafe { String::from_utf8_unchecked(v) } + } + + /// `prefix ++ encode_utf8(c) ++ suffix` with arbitrary-length arbitrary-byte `prefix` and + /// `suffix` and an arbitrary `char` `c`. Returns the string, the start of `c`, and `c`. + fn with_char_at() -> (String, usize, char) { + let c: char = kani::any(); + let prefix: usize = kani::any_where(|p: &usize| *p <= MAX_ALLOC); + let suffix: usize = kani::any(); + let total = prefix.checked_add(4).and_then(|n| n.checked_add(suffix)); + kani::assume(total.is_some_and(|n| n <= MAX_ALLOC)); + let cap: usize = kani::any_where(|c: &usize| *c >= total.unwrap() && *c <= MAX_ALLOC); + let mut v: Vec = Vec::with_capacity(cap); + let c_len = c.len_utf8(); + // SAFETY (harness): `prefix + c_len + suffix <= cap`; the char's bytes are written into + // the reserved space before they become part of the vector. + unsafe { + c.encode_utf8(core::slice::from_raw_parts_mut(v.as_mut_ptr().add(prefix), c_len)); + v.set_len(prefix + c_len + suffix); + (String::from_utf8_unchecked(v), prefix, c) + } + } + + #[kani::proof] + fn check_pop() { + // Either empty, or `c` is the last char (everything before it arbitrary). + let (mut s, start, c) = with_char_at(); + let has_last_char: bool = kani::any(); + // SAFETY (harness): shrinking the length keeps a prefix of the initialized bytes. + unsafe { s.as_mut_vec().set_len(if has_last_char { start + c.len_utf8() } else { 0 }) }; + kani::cover(has_last_char && start > 64, "pop from a long string"); + let res = s.pop(); + if has_last_char { + assert!(res == Some(c)); + assert!(s.len() == start); + } else { + assert!(res.is_none()); + assert!(s.len() == 0); + } + } + + // `self[idx..]` has a panic path (`str::slice_error_fail`) that formats the error message + // with loops over the string. Under this harness that path is infeasible (`idx` is the + // start of a well-formed char), but symbolic execution would still unfold it without end. + // The unwind bound only cuts that path: unwinding assertions stay enabled, so any loop that + // is actually reachable and needs more iterations makes the proof fail. No loop is + // reachable on the verified (non-panicking) path, so input sizes stay unbounded. + #[kani::proof] + #[kani::unwind(2)] + fn check_remove() { + let (mut s, idx, c) = with_char_at(); + let len = s.len(); + kani::cover(idx > 64 && len > idx + 64, "remove in the middle of a long string"); + let res = s.remove(idx); + assert!(res == c); + assert!(s.len() == len - c.len_utf8()); + } + + #[kani::proof] + fn check_insert() { + let mut s = any_string_bytes(); + let len = s.len(); + let ch: char = kani::any(); + kani::assume(len + 4 <= MAX_ALLOC); + let idx: usize = kani::any_where(|i: &usize| *i <= len); + kani::assume(s.is_char_boundary(idx)); + kani::cover(idx > 64 && len > idx + 64, "insert in the middle of a long string"); + s.insert(idx, ch); + assert!(s.len() == len + ch.len_utf8()); + } + + #[kani::proof] + fn check_insert_str() { + let mut s = any_string_bytes(); + let t = any_string_bytes(); + let len = s.len(); + let amt = t.len(); + kani::assume(len.checked_add(amt).is_some_and(|n| n <= MAX_ALLOC)); + let idx: usize = kani::any_where(|i: &usize| *i <= len); + kani::assume(s.is_char_boundary(idx)); + kani::cover(idx > 64 && len > idx + 64 && amt > 64, "long insert in the middle"); + s.insert_str(idx, t.as_str()); + assert!(s.len() == len + amt); + } + + #[kani::proof] + fn check_split_off() { + let mut s = any_string_bytes(); + let len = s.len(); + let at: usize = kani::any_where(|a: &usize| *a <= len); + kani::assume(s.is_char_boundary(at)); + kani::cover(at > 64 && len > at + 64, "split in the middle of a long string"); + let other = s.split_off(at); + assert!(s.len() == at); + assert!(other.len() == len - at); + } + + #[kani::proof] + fn check_drain_drop() { + // Arbitrary char-boundary range; the `Drain` is dropped without being iterated. + let mut s = any_string_bytes(); + let len = s.len(); + let start: usize = kani::any_where(|x: &usize| *x <= len); + let end: usize = kani::any_where(|x: &usize| *x >= start && *x <= len); + kani::assume(s.is_char_boundary(start) && s.is_char_boundary(end)); + kani::cover(start > 64 && end > start + 64 && len > end + 64, "drain in the middle"); + drop(s.drain(start..end)); + assert!(s.len() == len - (end - start)); + } + + #[kani::proof] + fn check_drain_next() { + // The drained range starts with a well-formed char, which the iterator decodes. + let (mut s, start, c) = with_char_at(); + let len = s.len(); + let end: usize = kani::any_where(|x: &usize| *x >= start + c.len_utf8() && *x <= len); + kani::assume(s.is_char_boundary(end)); + kani::cover(start > 64 && len > end + 64, "drain and iterate in the middle"); + let mut d = s.drain(start..end); + assert!(d.next() == Some(c)); + drop(d); + assert!(s.len() == len - (end - start)); + } + + #[kani::proof] + fn check_into_boxed_str() { + let s = any_string_bytes(); + let len = s.len(); + kani::cover(len > 64 && s.capacity() > len, "shrinking a long string"); + let b = s.into_boxed_str(); + assert!(b.len() == len); + } + + #[kani::proof] + fn check_leak() { + let s = any_string_bytes(); + let len = s.len(); + kani::cover(len > 64, "long string"); + let r: &'static mut str = s.leak(); + assert!(r.len() == len); + } + + // --------------------------------------------------------------------------------------- + // replace_range / remove_matches (from the ch10-hard6 branch): arbitrary receiver length, + // bounded edit size. + // + // Every loop reachable from these two functions iterates once per *edited* byte or per + // *match* (Splice::drop's drain/fill/extend/collect loops; remove_matches' rejection-collect + // and compaction loops), never once per byte of the receiver: the receiver-sized work is the + // tail `ptr::copy`, which is loop-free. So the receiver has arbitrary length and capacity, + // and only the number of edited bytes / matches is bounded, with a matching + // `#[kani::unwind]` (an insufficient bound fails the unwinding assertion). + // --------------------------------------------------------------------------------------- + + /// Arbitrary-length receiver, symbolic range `start..end` (any position, + /// `end - start <= E`) on char boundaries, given as an arbitrary `(Bound, Bound)` pair, + /// and an arbitrary replacement of `<= E` bytes. + fn replace_range_harness() { + use core::ops::Bound; + let mut s = any_string_bytes(); + let len = s.len(); + let start: usize = kani::any_where(|a: &usize| *a <= len); + let removed: usize = kani::any_where(|n: &usize| *n <= E && *n <= len - start); + let end = start + removed; + kani::assume(s.is_char_boundary(start) && s.is_char_boundary(end)); + let bytes: [u8; E] = kani::any(); + let rl: usize = kani::any_where(|n: &usize| *n <= E); + // SAFETY (harness only): `replace_range` copies the replacement bytes and never + // decodes them, so arbitrary bytes over-approximate every `&str`. + let repl = unsafe { core::str::from_utf8_unchecked(&bytes[..rl]) }; + kani::assume(len + E <= MAX_ALLOC); + kani::cover(len > 64 && start > 0 && end < len && rl > removed, "grow in the middle"); + kani::cover(len > 64 && start > 0 && end < len && rl < removed, "shrink in the middle"); + kani::cover(len > 64 && end == len && rl > 0, "append at the end"); + // Every `RangeBounds` shape (`a..b`, `a..=b`, `a..`, `..b`, `..=b`, `..`, and + // `Excluded` starts) denoting the same byte range. + let sb = if start > 0 && kani::any() { + Bound::Excluded(start - 1) + } else if start == 0 && kani::any() { + Bound::Unbounded + } else { + Bound::Included(start) + }; + let eb = if end > 0 && kani::any() { + Bound::Included(end - 1) + } else if end == len && kani::any() { + Bound::Unbounded + } else { + Bound::Excluded(end) + }; + s.replace_range((sb, eb), repl); + assert!(s.len() == len - removed + rl); + } + + #[kani::proof] + #[kani::unwind(6)] + fn check_replace_range() { + replace_range_harness::<4>(); + } + + /// A `Pattern` whose searcher is the most general one permitted by the `unsafe trait + /// Searcher` contract that `remove_matches` relies on (its SAFETY comment): successive + /// `next_match` results are non-overlapping, in increasing order, within the haystack and on + /// UTF-8 char boundaries (empty matches allowed). Every sound `Pattern` yields one of these + /// sequences, so this covers all of them at once; the std searchers' own conformance is the + /// subject of Challenges 20/21. At most `max_matches` matches (the only bound). + struct AnyPattern<'c> { + removed: &'c Cell, + max_matches: usize, + } + + struct AnySearcher<'a, 'c> { + haystack: &'a str, + front: usize, + left: usize, + removed: &'c Cell, + } + + // SAFETY: `next_match` only returns ranges satisfying the Searcher contract (see above); + // `next` reports the rest of the haystack as a single rejection, then Done. + unsafe impl<'a, 'c> Searcher<'a> for AnySearcher<'a, 'c> { + fn haystack(&self) -> &'a str { + self.haystack + } + + fn next(&mut self) -> SearchStep { + let len = self.haystack.len(); + if self.front == len { + return SearchStep::Done; + } + let a = self.front; + self.front = len; + SearchStep::Reject(a, len) + } + + fn next_match(&mut self) -> Option<(usize, usize)> { + if self.left == 0 || kani::any() { + return None; + } + let len = self.haystack.len(); + let front = self.front; + let a: usize = kani::any_where(|a: &usize| *a >= front && *a <= len); + let b: usize = kani::any_where(|b: &usize| *b >= a && *b <= len); + kani::assume(self.haystack.is_char_boundary(a) && self.haystack.is_char_boundary(b)); + self.front = b; + self.left -= 1; + self.removed.set(self.removed.get() + (b - a)); + Some((a, b)) + } + } + + impl<'c> Pattern for AnyPattern<'c> { + type Searcher<'a> = AnySearcher<'a, 'c>; + + fn into_searcher(self, haystack: &str) -> AnySearcher<'_, 'c> { + AnySearcher { haystack, front: 0, left: self.max_matches, removed: self.removed } + } + } + + #[kani::proof] + #[kani::unwind(6)] + fn check_remove_matches() { + let mut s = any_string_bytes(); + let len = s.len(); + let removed = Cell::new(0usize); + kani::cover(len > 64, "long receiver"); + s.remove_matches(AnyPattern { removed: &removed, max_matches: 4 }); + let r = removed.get(); + assert!(s.len() == len - r); + } + + // --------------------------------------------------------------------------------------- + // BOUNDED harnesses for the remaining "(U)" functions (`retain`, `from_utf16le/be` and their + // `_lossy` variants). Their loops (the `retain` loop; `decode_utf16`/`collect`/`push` loops + // in `from_utf16*`) cannot be given loop contracts with the pinned Kani: symbolic-bound + // quantifiers are dropped by the SAT backend, calls inside loop invariants are replaced by + // nondeterministic values, `for` over `DecodeUtf16` is rejected, and contracts/stubs on + // generic trait methods are not supported. These harnesses verify the real bodies up to the + // stated sizes (the unwinding assertions make an insufficient bound fail). + // --------------------------------------------------------------------------------------- + + /// Up to `N` arbitrary chars encoded back to back into one allocation (valid UTF-8 by + /// construction; no reallocation, which keeps the harness CI-sized). + fn any_valid_string() -> String { + let chars: [char; N] = kani::any(); + let n: usize = kani::any_where(|n: &usize| *n <= N); + let mut v: Vec = Vec::with_capacity(4 * N); + let mut off = 0; + for i in 0..n { + let l = chars[i].len_utf8(); + // SAFETY (harness): `off + l <= 4 * N = capacity`. + unsafe { + chars[i].encode_utf8(core::slice::from_raw_parts_mut(v.as_mut_ptr().add(off), l)); + } + off += l; + } + // SAFETY (harness): the first `off` bytes were written above. + unsafe { v.set_len(off) }; + // SAFETY (harness): concatenation of UTF-8 encodings of chars. + unsafe { String::from_utf8_unchecked(v) } + } + + /// `retain` on any valid string of up to 12 chars (<= 48 bytes), arbitrary keep-predicate. + #[kani::proof] + #[kani::unwind(13)] + fn check_retain_bounded() { + let mut s = any_valid_string::<12>(); + let len = s.len(); + kani::cover(len > 6, "multi-byte input"); + s.retain(|_c| kani::any()); + assert!(s.len() <= len); + } + + /// An arbitrary byte slice of length `<= N` at an arbitrary (odd or even) address, so both + /// the aligned (`align_to` succeeds) and the unaligned paths, and odd lengths, are + /// exercised. Each UTF-16 code unit decodes to at most 3 UTF-8 bytes (a surrogate pair, + /// 2 units, to 4), and a trailing odd byte becomes U+FFFD (3 bytes) in the lossy variants. + macro_rules! utf16_harness { + ($name:ident, $n:literal, $unwind:literal, $lossy:literal, $call:expr) => { + #[kani::proof] + #[kani::unwind($unwind)] + fn $name() { + let arr: [u8; $n] = kani::any(); + let v = kani::slice::any_slice_of_array(&arr); + kani::cover(v.len() >= 4 && (v.as_ptr() as usize) % 2 == 1, "unaligned"); + kani::cover(v.len() >= 4 && (v.as_ptr() as usize) % 2 == 0, "aligned"); + kani::cover(v.len() % 2 == 1, "odd length"); + let max = 3 * (v.len() / 2) + if $lossy { 3 } else { 0 }; + let f: fn(&[u8]) -> Option = $call; + match f(v) { + Some(s) => assert!(s.len() <= max), + None => assert!(!$lossy), + } + } + }; + } + utf16_harness!(check_from_utf16le_bounded, 12, 13, false, |v| String::from_utf16le(v).ok()); + utf16_harness!(check_from_utf16be_bounded, 12, 13, false, |v| String::from_utf16be(v).ok()); + utf16_harness!(check_from_utf16le_lossy_bounded, 8, 9, true, |v| Some( + String::from_utf16le_lossy(v) + )); + utf16_harness!(check_from_utf16be_lossy_bounded, 12, 13, true, |v| Some( + String::from_utf16be_lossy(v) + )); +} From ef9133a41b1b8a84a644e3a88be78d996396d489 Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Tue, 29 Sep 2026 20:59:19 +0300 Subject: [PATCH 2/8] Address review: initialized valid-UTF-8 inputs, tighter searcher, accurate docs - String generators: build the buffer with vec![0u8; cap] (a zeroed allocation, still loop-free and of symbolic size) and truncate it, and in with_char_at encode an arbitrary char at an arbitrary offset. Every generated String is now initialized, valid UTF-8; before, set_len exposed uninitialized capacity as string bytes. A ptr::write_bytes fill was tried first, but it made CBMC run out of memory while Kani generated traces. - replace_range: the replacement is a checked &str (str::from_utf8, invalid input assumed away), i.e. any valid UTF-8 of <= 4 bytes. - remove_matches: AnySearcher never repeats an empty match at the same position; its doc and SAFETY comment now follow the Searcher contract. - Module doc: bounds of each harness, and the content-independence argument for the generators. Written with AI assistance. --- library/alloc/src/string.rs | 132 +++++++++++++++++++++++------------- 1 file changed, 85 insertions(+), 47 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 6e8dc6db2909d..ce74aee6cc214 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3612,18 +3612,35 @@ impl From for String { mod verify { //! Challenge 10: memory safety of `String` methods that are safe abstractions over unsafe code. //! - //! Every harness in this module is loop-free, so no `#[kani::unwind]` bound is involved: - //! strings have a symbolic length and capacity, limited only by the largest object CBMC can - //! represent under `--object-bits 12` (see `MAX_ALLOC`). This covers the functions the - //! challenge marks "(U)" (`insert_str`, `split_off`) as well as the others. + //! Bounds. Strings have a symbolic length and capacity, limited only by the largest object + //! CBMC can represent under `--object-bits 12` (see `MAX_ALLOC`), except where stated below. //! - //! UTF-8 validity. None of these functions reads string contents except `pop`, `remove` and - //! the `Drain` iterator, which decode exactly one char. We model a `String` as arbitrary - //! bytes; where one char is decoded we place a well-formed encoding of an arbitrary `char` - //! at that position (`with_char_at`). Every valid `String` is an instance of this model - //! (`valid prefix ++ c ++ valid suffix`, and arbitrary bytes include every valid prefix and - //! suffix), so absence of UB for the model implies it for every valid `String`. Nothing is - //! assumed about the result of the function under test. + //! * Unbounded: `check_insert_str` and `check_split_off` (both "unbounded" in the challenge), + //! and `check_pop`, `check_remove`, `check_insert`, `check_drain_drop`, `check_drain_next`, + //! `check_into_boxed_str`, `check_leak`. No loop is reachable on their verified paths, so + //! no unwind bound limits the input. `check_remove` has `#[kani::unwind(2)]` only to cut an + //! infeasible panic-formatting path (see the comment on it). + //! * Receiver of any length, bounded edit: `check_replace_range` (removed and inserted + //! ranges of at most 4 bytes each) and `check_remove_matches` (at most 4 matches). Their + //! loops run once per edited byte or per match, never once per receiver byte. + //! * Bounded because of tool limits: `check_retain_bounded` (strings of up to 12 chars) and + //! the `from_utf16*` harnesses (inputs of up to 12 bytes, 8 for `from_utf16le_lossy`). See + //! the comment above them. + //! + //! Every `#[kani::unwind]` bound is checked by unwinding assertions, so a bound that is too + //! small makes the proof fail instead of silently cutting executions. + //! + //! Contents. Every generated `String` is initialized, valid UTF-8. The harnesses with a + //! symbolic length use a zeroed buffer, i.e. a string of NUL chars (`any_string`), and, where a + //! function decodes a char, put the UTF-8 encoding of an arbitrary `char` at an arbitrary + //! position (`with_char_at`). This is a modeling argument, not a quantification over all + //! contents: memory safety of these functions depends only on the length, the capacity, the + //! indices, the outcome of the char-boundary checks at those indices (the harnesses assume they + //! pass; outside the one encoded char they pass at every index), and the one char that `pop`, + //! `remove` and `Drain::next` decode. Any other bytes are only copied or moved, never used for + //! control flow or address computation. So the model reaches every combination of these + //! quantities that any valid `String` can produce. Nothing is assumed about the result of the + //! function under test. //! //! Panics are not UB. Documented panic conditions (index not on a char boundary, removing //! at the end) are excluded with `kani::assume`. @@ -3639,20 +3656,20 @@ mod verify { /// chosen for tractability (2^51 bytes = 2 PiB). const MAX_ALLOC: usize = (1usize << 51) - 1; - /// A `String` with symbolic length and capacity whose bytes are arbitrary - /// (fresh heap memory is nondeterministic in CBMC; no loop is executed). - fn any_string_bytes() -> String { + /// A `String` with symbolic length and capacity whose bytes are all 0 (NUL, a one-byte + /// UTF-8 char). The buffer is a zeroed allocation (`vec![0; cap]`), so it is initialized + /// without a loop or a fill of symbolic size. See the module comment on contents. + fn any_string() -> String { let cap: usize = kani::any_where(|c: &usize| *c <= MAX_ALLOC); let len: usize = kani::any_where(|l: &usize| *l <= cap); - let mut v: Vec = Vec::with_capacity(cap); - // SAFETY (harness): `len <= capacity`; see the module comment on contents. - unsafe { v.set_len(len) }; - // SAFETY (harness): see the module comment on UTF-8 validity. + let mut v: Vec = vec![0u8; cap]; + v.truncate(len); + // SAFETY (harness): all bytes are 0, which is valid UTF-8. unsafe { String::from_utf8_unchecked(v) } } - /// `prefix ++ encode_utf8(c) ++ suffix` with arbitrary-length arbitrary-byte `prefix` and - /// `suffix` and an arbitrary `char` `c`. Returns the string, the start of `c`, and `c`. + /// `prefix ++ encode_utf8(c) ++ suffix` with an arbitrary `char` `c` and all-zero `prefix` + /// and `suffix` of arbitrary lengths. Returns the string, the start of `c`, and `c`. fn with_char_at() -> (String, usize, char) { let c: char = kani::any(); let prefix: usize = kani::any_where(|p: &usize| *p <= MAX_ALLOC); @@ -3660,15 +3677,16 @@ mod verify { let total = prefix.checked_add(4).and_then(|n| n.checked_add(suffix)); kani::assume(total.is_some_and(|n| n <= MAX_ALLOC)); let cap: usize = kani::any_where(|c: &usize| *c >= total.unwrap() && *c <= MAX_ALLOC); - let mut v: Vec = Vec::with_capacity(cap); + let mut v: Vec = vec![0u8; cap]; let c_len = c.len_utf8(); - // SAFETY (harness): `prefix + c_len + suffix <= cap`; the char's bytes are written into - // the reserved space before they become part of the vector. + // SAFETY (harness): `prefix + c_len <= cap = v.len()`, so the char's bytes are written + // inside the zeroed, initialized buffer. unsafe { c.encode_utf8(core::slice::from_raw_parts_mut(v.as_mut_ptr().add(prefix), c_len)); - v.set_len(prefix + c_len + suffix); - (String::from_utf8_unchecked(v), prefix, c) } + v.truncate(prefix + c_len + suffix); + // SAFETY (harness): zero bytes, a well-formed char encoding, zero bytes: valid UTF-8. + (unsafe { String::from_utf8_unchecked(v) }, prefix, c) } #[kani::proof] @@ -3708,7 +3726,7 @@ mod verify { #[kani::proof] fn check_insert() { - let mut s = any_string_bytes(); + let mut s = any_string(); let len = s.len(); let ch: char = kani::any(); kani::assume(len + 4 <= MAX_ALLOC); @@ -3721,8 +3739,8 @@ mod verify { #[kani::proof] fn check_insert_str() { - let mut s = any_string_bytes(); - let t = any_string_bytes(); + let mut s = any_string(); + let t = any_string(); let len = s.len(); let amt = t.len(); kani::assume(len.checked_add(amt).is_some_and(|n| n <= MAX_ALLOC)); @@ -3735,7 +3753,7 @@ mod verify { #[kani::proof] fn check_split_off() { - let mut s = any_string_bytes(); + let mut s = any_string(); let len = s.len(); let at: usize = kani::any_where(|a: &usize| *a <= len); kani::assume(s.is_char_boundary(at)); @@ -3748,7 +3766,7 @@ mod verify { #[kani::proof] fn check_drain_drop() { // Arbitrary char-boundary range; the `Drain` is dropped without being iterated. - let mut s = any_string_bytes(); + let mut s = any_string(); let len = s.len(); let start: usize = kani::any_where(|x: &usize| *x <= len); let end: usize = kani::any_where(|x: &usize| *x >= start && *x <= len); @@ -3774,7 +3792,7 @@ mod verify { #[kani::proof] fn check_into_boxed_str() { - let s = any_string_bytes(); + let s = any_string(); let len = s.len(); kani::cover(len > 64 && s.capacity() > len, "shrinking a long string"); let b = s.into_boxed_str(); @@ -3783,7 +3801,7 @@ mod verify { #[kani::proof] fn check_leak() { - let s = any_string_bytes(); + let s = any_string(); let len = s.len(); kani::cover(len > 64, "long string"); let r: &'static mut str = s.leak(); @@ -3804,10 +3822,10 @@ mod verify { /// Arbitrary-length receiver, symbolic range `start..end` (any position, /// `end - start <= E`) on char boundaries, given as an arbitrary `(Bound, Bound)` pair, - /// and an arbitrary replacement of `<= E` bytes. + /// and an arbitrary valid UTF-8 replacement of `<= E` bytes. fn replace_range_harness() { use core::ops::Bound; - let mut s = any_string_bytes(); + let mut s = any_string(); let len = s.len(); let start: usize = kani::any_where(|a: &usize| *a <= len); let removed: usize = kani::any_where(|n: &usize| *n <= E && *n <= len - start); @@ -3815,9 +3833,11 @@ mod verify { kani::assume(s.is_char_boundary(start) && s.is_char_boundary(end)); let bytes: [u8; E] = kani::any(); let rl: usize = kani::any_where(|n: &usize| *n <= E); - // SAFETY (harness only): `replace_range` copies the replacement bytes and never - // decodes them, so arbitrary bytes over-approximate every `&str`. - let repl = unsafe { core::str::from_utf8_unchecked(&bytes[..rl]) }; + // Every `&str` of at most `E` bytes (checked conversion; invalid UTF-8 is assumed away). + let Ok(repl) = core::str::from_utf8(&bytes[..rl]) else { + kani::assume(false); + return; + }; kani::assume(len + E <= MAX_ALLOC); kani::cover(len > 64 && start > 0 && end < len && rl > removed, "grow in the middle"); kani::cover(len > 64 && start > 0 && end < len && rl < removed, "shrink in the middle"); @@ -3848,12 +3868,18 @@ mod verify { replace_range_harness::<4>(); } - /// A `Pattern` whose searcher is the most general one permitted by the `unsafe trait - /// Searcher` contract that `remove_matches` relies on (its SAFETY comment): successive - /// `next_match` results are non-overlapping, in increasing order, within the haystack and on - /// UTF-8 char boundaries (empty matches allowed). Every sound `Pattern` yields one of these - /// sequences, so this covers all of them at once; the std searchers' own conformance is the - /// subject of Challenges 20/21. At most `max_matches` matches (the only bound). + /// A `Pattern` whose searcher returns an arbitrary sequence of matches allowed by the + /// `unsafe trait Searcher` contract that `remove_matches` relies on (its SAFETY comment). + /// `Searcher::next` must produce `Match`/`Reject` ranges that are adjacent, non-overlapping, + /// cover the whole haystack and lie on UTF-8 char boundaries, and `next_match` returns the + /// `Match` ranges of that stream. So successive `next_match` results `(a, b)` satisfy + /// `front <= a <= b <= haystack.len()`, where `front` is the end of the previous match (0 at + /// first), with `a` and `b` on char boundaries; the gap `front..a` is the implied `Reject`. + /// Empty matches are allowed, but never twice at the same position: that would make no + /// progress, and no std searcher does it. Every searcher that meets this contract and never + /// repeats an empty match yields one of these sequences, so this covers all of them at once; + /// the std searchers' own conformance is the subject of Challenges 20/21. At most + /// `max_matches` matches (the only bound). struct AnyPattern<'c> { removed: &'c Cell, max_matches: usize, @@ -3863,11 +3889,15 @@ mod verify { haystack: &'a str, front: usize, left: usize, + /// Position of the previous match if it was empty. + last_empty: Option, removed: &'c Cell, } - // SAFETY: `next_match` only returns ranges satisfying the Searcher contract (see above); - // `next` reports the rest of the haystack as a single rejection, then Done. + // SAFETY: `next_match` returns `Match` ranges of a stream that meets the contract of + // `Searcher::next` (see `AnyPattern`): in increasing order, non-overlapping, within the + // haystack, on char boundaries, and no empty match repeated at one position. `next` reports + // the rest of the haystack (from the end of the last match) as one `Reject`, then `Done`. unsafe impl<'a, 'c> Searcher<'a> for AnySearcher<'a, 'c> { fn haystack(&self) -> &'a str { self.haystack @@ -3892,6 +3922,8 @@ mod verify { let a: usize = kani::any_where(|a: &usize| *a >= front && *a <= len); let b: usize = kani::any_where(|b: &usize| *b >= a && *b <= len); kani::assume(self.haystack.is_char_boundary(a) && self.haystack.is_char_boundary(b)); + kani::assume(!(a == b && self.last_empty == Some(a))); + self.last_empty = if a == b { Some(a) } else { None }; self.front = b; self.left -= 1; self.removed.set(self.removed.get() + (b - a)); @@ -3903,14 +3935,20 @@ mod verify { type Searcher<'a> = AnySearcher<'a, 'c>; fn into_searcher(self, haystack: &str) -> AnySearcher<'_, 'c> { - AnySearcher { haystack, front: 0, left: self.max_matches, removed: self.removed } + AnySearcher { + haystack, + front: 0, + left: self.max_matches, + last_empty: None, + removed: self.removed, + } } } #[kani::proof] #[kani::unwind(6)] fn check_remove_matches() { - let mut s = any_string_bytes(); + let mut s = any_string(); let len = s.len(); let removed = Cell::new(0usize); kani::cover(len > 64, "long receiver"); From 277b53e4913e3fb159c6349b0d85a1f5ca7d2c17 Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Tue, 29 Sep 2026 21:47:17 +0300 Subject: [PATCH 3/8] Address review: initialize retain inputs, most-general searcher, stronger covers - any_valid_string (retain): encode the chars into a zeroed vec![0u8; 4 * N] and truncate it, instead of writing through a slice over uninitialized spare capacity. - AnySearcher: drop the assumption that an empty match never repeats at one position. The Searcher contract allows it (adjacent, zero-length ranges), so the searcher is the most-general one again; its doc and SAFETY comment now state exactly what is generated. - remove_matches: up to 5 matches (unwind 7), so the rejections Vec grows past its initial capacity of 4. - Covers: remove_matches shows a real removal leaving a long string and the 5-match case; retain shows a multi-byte char kept after a deletion (the unsafe re-encode path). - Comment fixes: check_pop SAFETY (UTF-8 validity), with_char_at capacity bound uses the char's width, panic exclusions. Written with AI assistance. --- library/alloc/src/string.rs | 110 ++++++++++++++++++++++-------------- 1 file changed, 67 insertions(+), 43 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index ce74aee6cc214..f6fd1a6c6319e 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3621,7 +3621,7 @@ mod verify { //! no unwind bound limits the input. `check_remove` has `#[kani::unwind(2)]` only to cut an //! infeasible panic-formatting path (see the comment on it). //! * Receiver of any length, bounded edit: `check_replace_range` (removed and inserted - //! ranges of at most 4 bytes each) and `check_remove_matches` (at most 4 matches). Their + //! ranges of at most 4 bytes each) and `check_remove_matches` (at most 5 matches). Their //! loops run once per edited byte or per match, never once per receiver byte. //! * Bounded because of tool limits: `check_retain_bounded` (strings of up to 12 chars) and //! the `from_utf16*` harnesses (inputs of up to 12 bytes, 8 for `from_utf16le_lossy`). See @@ -3642,8 +3642,9 @@ mod verify { //! quantities that any valid `String` can produce. Nothing is assumed about the result of the //! function under test. //! - //! Panics are not UB. Documented panic conditions (index not on a char boundary, removing - //! at the end) are excluded with `kani::assume`. + //! Panics are not UB. Documented panic conditions are excluded: an index that is not on a char + //! boundary with `kani::assume`, and `remove` at the end of the string by construction + //! (`with_char_at` always puts a char at the index that is removed). use core::cell::Cell; use core::kani; use core::str::pattern::{Pattern, SearchStep, Searcher}; @@ -3672,13 +3673,14 @@ mod verify { /// and `suffix` of arbitrary lengths. Returns the string, the start of `c`, and `c`. fn with_char_at() -> (String, usize, char) { let c: char = kani::any(); + let c_len = c.len_utf8(); let prefix: usize = kani::any_where(|p: &usize| *p <= MAX_ALLOC); let suffix: usize = kani::any(); - let total = prefix.checked_add(4).and_then(|n| n.checked_add(suffix)); + let total = prefix.checked_add(c_len).and_then(|n| n.checked_add(suffix)); kani::assume(total.is_some_and(|n| n <= MAX_ALLOC)); + // `cap >= total`, so `cap == len` is possible for chars of every width. let cap: usize = kani::any_where(|c: &usize| *c >= total.unwrap() && *c <= MAX_ALLOC); let mut v: Vec = vec![0u8; cap]; - let c_len = c.len_utf8(); // SAFETY (harness): `prefix + c_len <= cap = v.len()`, so the char's bytes are written // inside the zeroed, initialized buffer. unsafe { @@ -3691,10 +3693,12 @@ mod verify { #[kani::proof] fn check_pop() { - // Either empty, or `c` is the last char (everything before it arbitrary). + // Either empty, or `c` is the last char, after a NUL prefix of arbitrary length. let (mut s, start, c) = with_char_at(); let has_last_char: bool = kani::any(); - // SAFETY (harness): shrinking the length keeps a prefix of the initialized bytes. + // SAFETY (harness): shrinking the length keeps a prefix of the initialized bytes. The new + // length is 0 or `start + c.len_utf8()`, the end of `c`, so the kept bytes are NULs + // followed by the whole encoding of `c`: valid UTF-8. unsafe { s.as_mut_vec().set_len(if has_last_char { start + c.len_utf8() } else { 0 }) }; kani::cover(has_last_char && start > 64, "pop from a long string"); let res = s.pop(); @@ -3809,8 +3813,7 @@ mod verify { } // --------------------------------------------------------------------------------------- - // replace_range / remove_matches (from the ch10-hard6 branch): arbitrary receiver length, - // bounded edit size. + // replace_range / remove_matches: arbitrary receiver length, bounded edit size. // // Every loop reachable from these two functions iterates once per *edited* byte or per // *match* (Splice::drop's drain/fill/extend/collect loops; remove_matches' rejection-collect @@ -3870,18 +3873,22 @@ mod verify { /// A `Pattern` whose searcher returns an arbitrary sequence of matches allowed by the /// `unsafe trait Searcher` contract that `remove_matches` relies on (its SAFETY comment). - /// `Searcher::next` must produce `Match`/`Reject` ranges that are adjacent, non-overlapping, - /// cover the whole haystack and lie on UTF-8 char boundaries, and `next_match` returns the - /// `Match` ranges of that stream. So successive `next_match` results `(a, b)` satisfy - /// `front <= a <= b <= haystack.len()`, where `front` is the end of the previous match (0 at - /// first), with `a` and `b` on char boundaries; the gap `front..a` is the implied `Reject`. - /// Empty matches are allowed, but never twice at the same position: that would make no - /// progress, and no std searcher does it. Every searcher that meets this contract and never - /// repeats an empty match yields one of these sequences, so this covers all of them at once; - /// the std searchers' own conformance is the subject of Challenges 20/21. At most - /// `max_matches` matches (the only bound). + /// The docs of `Searcher::next` say: "The stream of Match and Reject values up to a Done + /// will contain index ranges that are adjacent, non-overlapping, covering the whole + /// haystack, and laying on utf8 boundaries." and "Both ranges may have zero length." + /// `next_match` returns the `Match` ranges of that stream. So the successive `next_match` + /// results `(a, b)` are exactly the sequences with `front <= a <= b <= haystack.len()`, + /// where `front` is the end of the previous match (0 at first), and `a`, `b` on char + /// boundaries; the gap `front..a` is the implied `Reject`. This searcher generates all of + /// them: matches in increasing order, non-overlapping, possibly empty, possibly an empty + /// match repeated at one position (adjacent zero-length ranges, which the contract allows; + /// `remove_matches` then copies 0 bytes), within the haystack, on char boundaries. So it + /// covers every searcher that meets the contract at once; the std searchers' own + /// conformance is the subject of Challenges 20/21. At most `max_matches` matches (the only + /// bound). struct AnyPattern<'c> { removed: &'c Cell, + matches: &'c Cell, max_matches: usize, } @@ -3889,15 +3896,16 @@ mod verify { haystack: &'a str, front: usize, left: usize, - /// Position of the previous match if it was empty. - last_empty: Option, removed: &'c Cell, + matches: &'c Cell, } - // SAFETY: `next_match` returns `Match` ranges of a stream that meets the contract of - // `Searcher::next` (see `AnyPattern`): in increasing order, non-overlapping, within the - // haystack, on char boundaries, and no empty match repeated at one position. `next` reports - // the rest of the haystack (from the end of the last match) as one `Reject`, then `Done`. + // SAFETY: `next_match` returns the `Match` ranges of a stream that meets the contract of + // `Searcher::next` (see `AnyPattern`): in increasing order, non-overlapping (possibly empty, + // and possibly an empty match repeated at one position, as the contract allows), within the + // haystack, on char boundaries; the gaps between them are the implied `Reject`s. `next` + // reports the rest of the haystack (from the end of the last match) as one `Reject`, then + // `Done`. unsafe impl<'a, 'c> Searcher<'a> for AnySearcher<'a, 'c> { fn haystack(&self) -> &'a str { self.haystack @@ -3922,11 +3930,10 @@ mod verify { let a: usize = kani::any_where(|a: &usize| *a >= front && *a <= len); let b: usize = kani::any_where(|b: &usize| *b >= a && *b <= len); kani::assume(self.haystack.is_char_boundary(a) && self.haystack.is_char_boundary(b)); - kani::assume(!(a == b && self.last_empty == Some(a))); - self.last_empty = if a == b { Some(a) } else { None }; self.front = b; self.left -= 1; self.removed.set(self.removed.get() + (b - a)); + self.matches.set(self.matches.get() + 1); Some((a, b)) } } @@ -3939,21 +3946,26 @@ mod verify { haystack, front: 0, left: self.max_matches, - last_empty: None, removed: self.removed, + matches: self.matches, } } } + /// At most 5 matches. `remove_matches` collects the gaps between matches into a + /// `Vec<(usize, usize)>` that starts with capacity 4, so the 5th match exercises its + /// reallocation. The loops run at most 6 times (5 gaps plus the tail), hence `unwind(7)`. #[kani::proof] - #[kani::unwind(6)] + #[kani::unwind(7)] fn check_remove_matches() { let mut s = any_string(); let len = s.len(); let removed = Cell::new(0usize); - kani::cover(len > 64, "long receiver"); - s.remove_matches(AnyPattern { removed: &removed, max_matches: 4 }); + let matches = Cell::new(0usize); + s.remove_matches(AnyPattern { removed: &removed, matches: &matches, max_matches: 5 }); let r = removed.get(); + kani::cover(r > 0 && s.len() > 64, "real removal, long string left"); + kani::cover(matches.get() == 5, "5 matches: the rejections Vec reallocates"); assert!(s.len() == len - r); } @@ -3967,24 +3979,22 @@ mod verify { // stated sizes (the unwinding assertions make an insufficient bound fail). // --------------------------------------------------------------------------------------- - /// Up to `N` arbitrary chars encoded back to back into one allocation (valid UTF-8 by - /// construction; no reallocation, which keeps the harness CI-sized). + /// Up to `N` arbitrary chars encoded back to back into a zeroed (initialized) buffer of + /// `4 * N` bytes, which is then truncated to the encoded length (valid UTF-8 by construction; + /// no reallocation, which keeps the harness CI-sized). fn any_valid_string() -> String { let chars: [char; N] = kani::any(); let n: usize = kani::any_where(|n: &usize| *n <= N); - let mut v: Vec = Vec::with_capacity(4 * N); + let mut v: Vec = vec![0u8; 4 * N]; let mut off = 0; for i in 0..n { let l = chars[i].len_utf8(); - // SAFETY (harness): `off + l <= 4 * N = capacity`. - unsafe { - chars[i].encode_utf8(core::slice::from_raw_parts_mut(v.as_mut_ptr().add(off), l)); - } + chars[i].encode_utf8(&mut v[off..off + l]); off += l; } - // SAFETY (harness): the first `off` bytes were written above. - unsafe { v.set_len(off) }; - // SAFETY (harness): concatenation of UTF-8 encodings of chars. + v.truncate(off); + // SAFETY (harness): `v` is exactly the concatenation of the UTF-8 encodings of + // `chars[..n]` (`truncate` drops only the unused zero bytes after them): valid UTF-8. unsafe { String::from_utf8_unchecked(v) } } @@ -3994,8 +4004,22 @@ mod verify { fn check_retain_bounded() { let mut s = any_valid_string::<12>(); let len = s.len(); - kani::cover(len > 6, "multi-byte input"); - s.retain(|_c| kani::any()); + // Observers for the cover below; they do not influence the predicate's result. + let deleted = Cell::new(false); + let kept_multibyte_after_deletion = Cell::new(false); + s.retain(|c| { + let keep: bool = kani::any(); + if !keep { + deleted.set(true); + } else if c.len_utf8() > 1 && deleted.get() { + kept_multibyte_after_deletion.set(true); + } + keep + }); + kani::cover( + kept_multibyte_after_deletion.get(), + "multi-byte char kept after a deletion (moved by the unsafe re-encode)", + ); assert!(s.len() <= len); } From d2cf8f0b2efde7d2d173ebf0c1fc444acaa1fd93 Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Wed, 30 Sep 2026 20:08:00 +0300 Subject: [PATCH 4/8] Ch10: drop all kani::assume, add should_panic harnesses, stronger covers - Replace the char-boundary assumes with assert!s: on the all-NUL strings every index up to the length is a boundary, and in check_drain_next the end lies in the NUL suffix. The Searcher of check_remove_matches asserts its boundary requirement instead of assuming it. - Express the MAX_ALLOC size limits as any_where domains of the generators (any_string_max_len, with_char_at), so the module has no kani::assume. - replace_range: build the replacement constructively (up to 4 encoded chars in a zeroed buffer) instead of from_utf8 plus assume(false); unwind bound 5 (4 iterations plus the exit test). - Share an any_bounds generator between replace_range and drain, with a cover per Bound variant; covers for the reallocation paths. - retain: assert that the new length equals the bytes of the kept chars. - from_utf16*: covers for a leading surrogate pair that decodes and a leading unpaired surrogate, assert Err for the latter in the strict variants; unwind 7 (6 code units plus the exit test), which also lets from_utf16le_lossy run on inputs of up to 12 bytes like the others. - Add should_panic harnesses for insert, insert_str, split_off, drain and replace_range at indices strictly inside a multi-byte char or past the end. - Document each unwind bound and update the module comment. --- library/alloc/src/string.rs | 385 ++++++++++++++++++++++++++---------- 1 file changed, 284 insertions(+), 101 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index f6fd1a6c6319e..abe146a6f2e1f 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3619,78 +3619,123 @@ mod verify { //! and `check_pop`, `check_remove`, `check_insert`, `check_drain_drop`, `check_drain_next`, //! `check_into_boxed_str`, `check_leak`. No loop is reachable on their verified paths, so //! no unwind bound limits the input. `check_remove` has `#[kani::unwind(2)]` only to cut an - //! infeasible panic-formatting path (see the comment on it). + //! infeasible panic-formatting path (see the comment on it). The `check_*_panics` + //! harnesses are unbounded too (`#[kani::unwind(1)]` on `check_replace_range_panics` only + //! covers loops that no input reaches, see the comment on it). //! * Receiver of any length, bounded edit: `check_replace_range` (removed and inserted //! ranges of at most 4 bytes each) and `check_remove_matches` (at most 5 matches). Their //! loops run once per edited byte or per match, never once per receiver byte. //! * Bounded because of tool limits: `check_retain_bounded` (strings of up to 12 chars) and - //! the `from_utf16*` harnesses (inputs of up to 12 bytes, 8 for `from_utf16le_lossy`). See - //! the comment above them. + //! the `from_utf16*` harnesses (inputs of up to 12 bytes). See the comment above them. //! //! Every `#[kani::unwind]` bound is checked by unwinding assertions, so a bound that is too //! small makes the proof fail instead of silently cutting executions. //! + //! Restrictions. There is no `kani::assume` in this module: every restriction of an input + //! is a `kani::any_where` domain at the point where the input is generated (sizes that fit + //! in one CBMC object, indices inside the string, the bounds above, and in the panic + //! harnesses indices without a char boundary, `any_non_boundary`). Nothing is assumed + //! about the result of a function under test. + //! //! Contents. Every generated `String` is initialized, valid UTF-8. The harnesses with a //! symbolic length use a zeroed buffer, i.e. a string of NUL chars (`any_string`), and, where a //! function decodes a char, put the UTF-8 encoding of an arbitrary `char` at an arbitrary //! position (`with_char_at`). This is a modeling argument, not a quantification over all //! contents: memory safety of these functions depends only on the length, the capacity, the - //! indices, the outcome of the char-boundary checks at those indices (the harnesses assume they - //! pass; outside the one encoded char they pass at every index), and the one char that `pop`, - //! `remove` and `Drain::next` decode. Any other bytes are only copied or moved, never used for - //! control flow or address computation. So the model reaches every combination of these - //! quantities that any valid `String` can produce. Nothing is assumed about the result of the - //! function under test. + //! indices, the outcome of the char-boundary checks at those indices, and the one char that + //! `pop`, `remove` and `Drain::next` decode. Any other bytes are only copied or moved, never + //! used for control flow or address computation. On an all-NUL string every index up to the + //! length is a char boundary, so the model reaches every combination of these quantities for + //! which the boundary checks pass; the combinations for which they fail are the panics below. //! - //! Panics are not UB. Documented panic conditions are excluded: an index that is not on a char - //! boundary with `kani::assume`, and `remove` at the end of the string by construction - //! (`with_char_at` always puts a char at the index that is removed). + //! Panics. Panics are not UB. The harnesses stay out of the documented panic conditions + //! through their input domains: indices are at most the length (an `any_where` domain), and + //! every such index of an all-NUL string is a char boundary by construction (the harnesses + //! `assert!` this before the call); `with_char_at` puts a char at the index that `remove` + //! removes. The `check_*_panics` harnesses (`#[kani::should_panic]`) show for `insert`, + //! `insert_str`, `split_off`, `drain` and `replace_range` that an index strictly inside a + //! multi-byte char, or past the end, panics. Reversed ranges and `Bound` overflow + //! (`..=usize::MAX`) are not exercised there. use core::cell::Cell; use core::kani; + use core::ops::Bound; use core::str::pattern::{Pattern, SearchStep, Searcher}; use crate::string::String; use crate::vec::Vec; - /// Largest single allocation CBMC can represent with `--object-bits 12` (the setting used by - /// `scripts/run-kani.sh`): 52 offset bits, signed. A limit of the memory model, not a bound - /// chosen for tractability (2^51 bytes = 2 PiB). + /// Largest positive offset CBMC can represent within one object with `--object-bits 12` (the + /// setting used by `scripts/run-kani.sh`): 52 offset bits, signed. A limit of the memory + /// model, not a bound chosen for tractability (2^51 bytes = 2 PiB). const MAX_ALLOC: usize = (1usize << 51) - 1; - /// A `String` with symbolic length and capacity whose bytes are all 0 (NUL, a one-byte - /// UTF-8 char). The buffer is a zeroed allocation (`vec![0; cap]`), so it is initialized - /// without a loop or a fill of symbolic size. See the module comment on contents. - fn any_string() -> String { + /// A `String` with symbolic capacity (`<= MAX_ALLOC`) and symbolic length (`<= max_len`) + /// whose bytes are all 0 (NUL, a one-byte UTF-8 char). The buffer is a zeroed allocation + /// (`vec![0; cap]`), so it is initialized without a loop or a fill of symbolic size. See the + /// module comment on contents. + fn any_string_max_len(max_len: usize) -> String { let cap: usize = kani::any_where(|c: &usize| *c <= MAX_ALLOC); - let len: usize = kani::any_where(|l: &usize| *l <= cap); + let len: usize = kani::any_where(|l: &usize| *l <= cap && *l <= max_len); let mut v: Vec = vec![0u8; cap]; v.truncate(len); // SAFETY (harness): all bytes are 0, which is valid UTF-8. unsafe { String::from_utf8_unchecked(v) } } + /// `any_string_max_len` without a limit on the length other than the capacity. + fn any_string() -> String { + any_string_max_len(MAX_ALLOC) + } + /// `prefix ++ encode_utf8(c) ++ suffix` with an arbitrary `char` `c` and all-zero `prefix` /// and `suffix` of arbitrary lengths. Returns the string, the start of `c`, and `c`. fn with_char_at() -> (String, usize, char) { let c: char = kani::any(); let c_len = c.len_utf8(); - let prefix: usize = kani::any_where(|p: &usize| *p <= MAX_ALLOC); - let suffix: usize = kani::any(); - let total = prefix.checked_add(c_len).and_then(|n| n.checked_add(suffix)); - kani::assume(total.is_some_and(|n| n <= MAX_ALLOC)); - // `cap >= total`, so `cap == len` is possible for chars of every width. - let cap: usize = kani::any_where(|c: &usize| *c >= total.unwrap() && *c <= MAX_ALLOC); + // `prefix + c_len + suffix <= MAX_ALLOC`: the string fits in one CBMC object. + let prefix: usize = kani::any_where(|p: &usize| *p <= MAX_ALLOC - c_len); + let suffix: usize = kani::any_where(|s: &usize| *s <= MAX_ALLOC - c_len - prefix); + let len = prefix + c_len + suffix; + // `cap >= len`, so `cap == len` is possible for chars of every width. + let cap: usize = kani::any_where(|k: &usize| *k >= len && *k <= MAX_ALLOC); let mut v: Vec = vec![0u8; cap]; // SAFETY (harness): `prefix + c_len <= cap = v.len()`, so the char's bytes are written // inside the zeroed, initialized buffer. unsafe { c.encode_utf8(core::slice::from_raw_parts_mut(v.as_mut_ptr().add(prefix), c_len)); } - v.truncate(prefix + c_len + suffix); + v.truncate(len); // SAFETY (harness): zero bytes, a well-formed char encoding, zero bytes: valid UTF-8. (unsafe { String::from_utf8_unchecked(v) }, prefix, c) } + /// The byte range `start..end` of a string of length `len` as an arbitrary `(Bound, Bound)` + /// pair: every `RangeBounds` shape (`a..b`, `a..=b`, `a..`, `..b`, `..=b`, `..`, and + /// `Excluded` starts) that denotes this range. + fn any_bounds(start: usize, end: usize, len: usize) -> (Bound, Bound) { + let sb = if start > 0 && kani::any() { + Bound::Excluded(start - 1) + } else if start == 0 && kani::any() { + Bound::Unbounded + } else { + Bound::Included(start) + }; + let eb = if end > 0 && kani::any() { + Bound::Included(end - 1) + } else if end == len && kani::any() { + Bound::Unbounded + } else { + Bound::Excluded(end) + }; + kani::cover(matches!(sb, Bound::Included(_)), "start bound Included"); + kani::cover(matches!(sb, Bound::Excluded(_)), "start bound Excluded"); + kani::cover(matches!(sb, Bound::Unbounded), "start bound Unbounded"); + kani::cover(matches!(eb, Bound::Included(_)), "end bound Included"); + kani::cover(matches!(eb, Bound::Excluded(_)), "end bound Excluded"); + kani::cover(matches!(eb, Bound::Unbounded), "end bound Unbounded"); + (sb, eb) + } + #[kani::proof] fn check_pop() { // Either empty, or `c` is the last char, after a NUL prefix of arbitrary length. @@ -3730,13 +3775,16 @@ mod verify { #[kani::proof] fn check_insert() { - let mut s = any_string(); + // `len + 4 <= MAX_ALLOC`: the length of the result stays within `MAX_ALLOC`. + let mut s = any_string_max_len(MAX_ALLOC - 4); let len = s.len(); let ch: char = kani::any(); - kani::assume(len + 4 <= MAX_ALLOC); let idx: usize = kani::any_where(|i: &usize| *i <= len); - kani::assume(s.is_char_boundary(idx)); + // Every index up to the length of an all-NUL string is a char boundary, so the + // documented panic is excluded by construction. Checked here, not assumed. + assert!(s.is_char_boundary(idx)); kani::cover(idx > 64 && len > idx + 64, "insert in the middle of a long string"); + kani::cover(s.capacity() == len, "full buffer: insert reallocates"); s.insert(idx, ch); assert!(s.len() == len + ch.len_utf8()); } @@ -3744,13 +3792,15 @@ mod verify { #[kani::proof] fn check_insert_str() { let mut s = any_string(); - let t = any_string(); let len = s.len(); + // `len + amt <= MAX_ALLOC`: the length of the result stays within `MAX_ALLOC`. + let t = any_string_max_len(MAX_ALLOC - len); let amt = t.len(); - kani::assume(len.checked_add(amt).is_some_and(|n| n <= MAX_ALLOC)); let idx: usize = kani::any_where(|i: &usize| *i <= len); - kani::assume(s.is_char_boundary(idx)); + // No panic by construction, as in `check_insert`. + assert!(s.is_char_boundary(idx)); kani::cover(idx > 64 && len > idx + 64 && amt > 64, "long insert in the middle"); + kani::cover(s.capacity() == len && amt > 0, "full buffer: insert_str reallocates"); s.insert_str(idx, t.as_str()); assert!(s.len() == len + amt); } @@ -3760,7 +3810,8 @@ mod verify { let mut s = any_string(); let len = s.len(); let at: usize = kani::any_where(|a: &usize| *a <= len); - kani::assume(s.is_char_boundary(at)); + // No panic by construction, as in `check_insert`. + assert!(s.is_char_boundary(at)); kani::cover(at > 64 && len > at + 64, "split in the middle of a long string"); let other = s.split_off(at); assert!(s.len() == at); @@ -3769,14 +3820,16 @@ mod verify { #[kani::proof] fn check_drain_drop() { - // Arbitrary char-boundary range; the `Drain` is dropped without being iterated. + // Arbitrary range, given in every `RangeBounds` shape; the `Drain` is dropped without + // being iterated. let mut s = any_string(); let len = s.len(); let start: usize = kani::any_where(|x: &usize| *x <= len); let end: usize = kani::any_where(|x: &usize| *x >= start && *x <= len); - kani::assume(s.is_char_boundary(start) && s.is_char_boundary(end)); + // No panic by construction, as in `check_insert`. + assert!(s.is_char_boundary(start) && s.is_char_boundary(end)); kani::cover(start > 64 && end > start + 64 && len > end + 64, "drain in the middle"); - drop(s.drain(start..end)); + drop(s.drain(any_bounds(start, end, len))); assert!(s.len() == len - (end - start)); } @@ -3786,9 +3839,11 @@ mod verify { let (mut s, start, c) = with_char_at(); let len = s.len(); let end: usize = kani::any_where(|x: &usize| *x >= start + c.len_utf8() && *x <= len); - kani::assume(s.is_char_boundary(end)); + // `start` is the start of `c`, and `end` is in the NUL suffix after `c` or at the end + // of the string: both are char boundaries by construction. Checked here, not assumed. + assert!(s.is_char_boundary(start) && s.is_char_boundary(end)); kani::cover(start > 64 && len > end + 64, "drain and iterate in the middle"); - let mut d = s.drain(start..end); + let mut d = s.drain(any_bounds(start, end, len)); assert!(d.next() == Some(c)); drop(d); assert!(s.len() == len - (end - start)); @@ -3823,50 +3878,55 @@ mod verify { // `#[kani::unwind]` (an insufficient bound fails the unwinding assertion). // --------------------------------------------------------------------------------------- + /// Every valid UTF-8 string of at most `E` bytes: up to `E` arbitrary chars encoded back to + /// back into the zeroed buffer `buf`, stopping at the first char that does not fit. A string + /// of `k` chars whose encodings fit in `E` bytes is produced when those chars come first and + /// `n = k`. The bytes are valid UTF-8 by construction; nothing is checked or assumed. + fn any_short_str(buf: &mut [u8; E]) -> &str { + let chars: [char; E] = kani::any(); + let n: usize = kani::any_where(|n: &usize| *n <= E); + let mut off = 0; + for i in 0..n { + let l = chars[i].len_utf8(); + if l > E - off { + break; + } + chars[i].encode_utf8(&mut buf[off..off + l]); + off += l; + } + // SAFETY (harness): `buf[..off]` is the concatenation of the UTF-8 encodings of whole + // chars: valid UTF-8. + unsafe { core::str::from_utf8_unchecked(&buf[..off]) } + } + /// Arbitrary-length receiver, symbolic range `start..end` (any position, /// `end - start <= E`) on char boundaries, given as an arbitrary `(Bound, Bound)` pair, /// and an arbitrary valid UTF-8 replacement of `<= E` bytes. fn replace_range_harness() { - use core::ops::Bound; - let mut s = any_string(); + // `len + E <= MAX_ALLOC`: the length of the result stays within `MAX_ALLOC`. + let mut s = any_string_max_len(MAX_ALLOC - E); let len = s.len(); let start: usize = kani::any_where(|a: &usize| *a <= len); let removed: usize = kani::any_where(|n: &usize| *n <= E && *n <= len - start); let end = start + removed; - kani::assume(s.is_char_boundary(start) && s.is_char_boundary(end)); - let bytes: [u8; E] = kani::any(); - let rl: usize = kani::any_where(|n: &usize| *n <= E); - // Every `&str` of at most `E` bytes (checked conversion; invalid UTF-8 is assumed away). - let Ok(repl) = core::str::from_utf8(&bytes[..rl]) else { - kani::assume(false); - return; - }; - kani::assume(len + E <= MAX_ALLOC); + // No panic by construction, as in `check_insert`. + assert!(s.is_char_boundary(start) && s.is_char_boundary(end)); + let mut buf = [0u8; E]; + let repl = any_short_str(&mut buf); + let rl = repl.len(); kani::cover(len > 64 && start > 0 && end < len && rl > removed, "grow in the middle"); kani::cover(len > 64 && start > 0 && end < len && rl < removed, "shrink in the middle"); kani::cover(len > 64 && end == len && rl > 0, "append at the end"); - // Every `RangeBounds` shape (`a..b`, `a..=b`, `a..`, `..b`, `..=b`, `..`, and - // `Excluded` starts) denoting the same byte range. - let sb = if start > 0 && kani::any() { - Bound::Excluded(start - 1) - } else if start == 0 && kani::any() { - Bound::Unbounded - } else { - Bound::Included(start) - }; - let eb = if end > 0 && kani::any() { - Bound::Included(end - 1) - } else if end == len && kani::any() { - Bound::Unbounded - } else { - Bound::Excluded(end) - }; - s.replace_range((sb, eb), repl); + kani::cover(s.capacity() == len && rl > removed, "full buffer, growing: reallocates"); + kani::cover(rl >= 4 && repl.as_bytes()[0] >= 0xF0, "replacement starts with a 4-byte char"); + s.replace_range(any_bounds(start, end, len), repl); assert!(s.len() == len - removed + rl); } + // `unwind(5)`: the longest loops here run at most 4 times (the chars of `any_short_str`; + // the `Splice` loops, once per removed or inserted byte), plus the exit test. #[kani::proof] - #[kani::unwind(6)] + #[kani::unwind(5)] fn check_replace_range() { replace_range_harness::<4>(); } @@ -3879,13 +3939,17 @@ mod verify { /// `next_match` returns the `Match` ranges of that stream. So the successive `next_match` /// results `(a, b)` are exactly the sequences with `front <= a <= b <= haystack.len()`, /// where `front` is the end of the previous match (0 at first), and `a`, `b` on char - /// boundaries; the gap `front..a` is the implied `Reject`. This searcher generates all of - /// them: matches in increasing order, non-overlapping, possibly empty, possibly an empty - /// match repeated at one position (adjacent zero-length ranges, which the contract allows; - /// `remove_matches` then copies 0 bytes), within the haystack, on char boundaries. So it - /// covers every searcher that meets the contract at once; the std searchers' own - /// conformance is the subject of Challenges 20/21. At most `max_matches` matches (the only - /// bound). + /// boundaries; the gap `front..a` is the implied `Reject`. + /// + /// This searcher generates every such sequence of at most `max_matches` matches (the only + /// bound) on a haystack where every index is a char boundary, which is the all-NUL receiver + /// of `check_remove_matches`: matches in increasing order, non-overlapping, possibly empty, + /// possibly an empty match repeated at one position (adjacent zero-length ranges, which the + /// contract allows; `remove_matches` then copies 0 bytes), within the haystack. The boundary + /// requirement is asserted, not assumed. On a haystack with multi-byte chars the contract + /// allows only a subset of these sequences, and `remove_matches` never reads the bytes + /// itself (it only moves them), so this covers every searcher that meets the contract at + /// once; the std searchers' own conformance is the subject of Challenges 20/21. struct AnyPattern<'c> { removed: &'c Cell, matches: &'c Cell, @@ -3903,9 +3967,9 @@ mod verify { // SAFETY: `next_match` returns the `Match` ranges of a stream that meets the contract of // `Searcher::next` (see `AnyPattern`): in increasing order, non-overlapping (possibly empty, // and possibly an empty match repeated at one position, as the contract allows), within the - // haystack, on char boundaries; the gaps between them are the implied `Reject`s. `next` - // reports the rest of the haystack (from the end of the last match) as one `Reject`, then - // `Done`. + // haystack, on char boundaries (asserted in `next_match`); the gaps between them are the + // implied `Reject`s. `next` reports the rest of the haystack (from the end of the last + // match) as one `Reject`, then `Done`. unsafe impl<'a, 'c> Searcher<'a> for AnySearcher<'a, 'c> { fn haystack(&self) -> &'a str { self.haystack @@ -3929,7 +3993,9 @@ mod verify { let front = self.front; let a: usize = kani::any_where(|a: &usize| *a >= front && *a <= len); let b: usize = kani::any_where(|b: &usize| *b >= a && *b <= len); - kani::assume(self.haystack.is_char_boundary(a) && self.haystack.is_char_boundary(b)); + // The contract's boundary requirement. Every index of the all-NUL haystack is a + // char boundary, so this holds for every pair above; checked, not assumed. + assert!(self.haystack.is_char_boundary(a) && self.haystack.is_char_boundary(b)); self.front = b; self.left -= 1; self.removed.set(self.removed.get() + (b - a)); @@ -3954,7 +4020,8 @@ mod verify { /// At most 5 matches. `remove_matches` collects the gaps between matches into a /// `Vec<(usize, usize)>` that starts with capacity 4, so the 5th match exercises its - /// reallocation. The loops run at most 6 times (5 gaps plus the tail), hence `unwind(7)`. + /// reallocation. `unwind(7)`: the loops run at most 6 times (5 gaps plus the tail), plus + /// the exit test. #[kani::proof] #[kani::unwind(7)] fn check_remove_matches() { @@ -3971,12 +4038,16 @@ mod verify { // --------------------------------------------------------------------------------------- // BOUNDED harnesses for the remaining "(U)" functions (`retain`, `from_utf16le/be` and their - // `_lossy` variants). Their loops (the `retain` loop; `decode_utf16`/`collect`/`push` loops - // in `from_utf16*`) cannot be given loop contracts with the pinned Kani: symbolic-bound - // quantifiers are dropped by the SAT backend, calls inside loop invariants are replaced by - // nondeterministic values, `for` over `DecodeUtf16` is rejected, and contracts/stubs on - // generic trait methods are not supported. These harnesses verify the real bodies up to the - // stated sizes (the unwinding assertions make an insufficient bound fail). + // `_lossy` variants). Their loops cannot be given loop contracts with the pinned Kani. + // `retain`: symbolic-bound quantifiers are dropped by the SAT backend, calls inside loop + // invariants are replaced by nondeterministic values, and the `Chars` temporary of the loop + // body cannot be named in `loop_modifies`. `from_utf16*`: the aligned `from_utf16le` path + // loops with `for` over `DecodeUtf16`, which the loop-contract macro rejects; every other + // path loops inside the generic default `Iterator::try_fold` / `fold` (via `collect`), whose + // state cannot be named in an invariant; and each of these loops pushes to a `String`, while + // loop contracts do not allow the loop body to allocate or free memory. These harnesses + // verify the real bodies up to the stated sizes (the unwinding assertions make an + // insufficient bound fail). // --------------------------------------------------------------------------------------- /// Up to `N` arbitrary chars encoded back to back into a zeroed (initialized) buffer of @@ -3999,11 +4070,14 @@ mod verify { } /// `retain` on any valid string of up to 12 chars (<= 48 bytes), arbitrary keep-predicate. + /// `unwind(13)`: the generator's loop and the `retain` loop run once per char (at most 12), + /// plus the exit test. #[kani::proof] #[kani::unwind(13)] fn check_retain_bounded() { let mut s = any_valid_string::<12>(); - let len = s.len(); + // Bytes of the chars the predicate keeps (`retain` calls it once per char, in order). + let kept = Cell::new(0usize); // Observers for the cover below; they do not influence the predicate's result. let deleted = Cell::new(false); let kept_multibyte_after_deletion = Cell::new(false); @@ -4011,8 +4085,11 @@ mod verify { let keep: bool = kani::any(); if !keep { deleted.set(true); - } else if c.len_utf8() > 1 && deleted.get() { - kept_multibyte_after_deletion.set(true); + } else { + kept.set(kept.get() + c.len_utf8()); + if c.len_utf8() > 1 && deleted.get() { + kept_multibyte_after_deletion.set(true); + } } keep }); @@ -4020,38 +4097,144 @@ mod verify { kept_multibyte_after_deletion.get(), "multi-byte char kept after a deletion (moved by the unsafe re-encode)", ); - assert!(s.len() <= len); + assert!(s.len() == kept.get()); } /// An arbitrary byte slice of length `<= N` at an arbitrary (odd or even) address, so both /// the aligned (`align_to` succeeds) and the unaligned paths, and odd lengths, are /// exercised. Each UTF-16 code unit decodes to at most 3 UTF-8 bytes (a surrogate pair, /// 2 units, to 4), and a trailing odd byte becomes U+FFFD (3 bytes) in the lossy variants. + /// An input whose first code unit (in the byte order of the function, `$be`) is a low + /// surrogate is invalid UTF-16, so the strict variants must return `Err`. The covers read + /// only the input and whether the result is `Ok`: reading the bytes of the decoded string + /// made CBMC run out of memory at these sizes. macro_rules! utf16_harness { - ($name:ident, $n:literal, $unwind:literal, $lossy:literal, $call:expr) => { + ($name:ident, $n:literal, $unwind:literal, $lossy:literal, $be:literal, $call:expr) => { #[kani::proof] #[kani::unwind($unwind)] fn $name() { let arr: [u8; $n] = kani::any(); let v = kani::slice::any_slice_of_array(&arr); + // Code unit `i` of `v`, in the byte order of the function under test. + let unit = |i: usize| { + let b = [v[2 * i], v[2 * i + 1]]; + if $be { u16::from_be_bytes(b) } else { u16::from_le_bytes(b) } + }; + let lone = v.len() >= 2 && (0xDC00..=0xDFFF).contains(&unit(0)); + let pair = v.len() >= 4 + && (0xD800..=0xDBFF).contains(&unit(0)) + && (0xDC00..=0xDFFF).contains(&unit(1)); kani::cover(v.len() >= 4 && (v.as_ptr() as usize) % 2 == 1, "unaligned"); kani::cover(v.len() >= 4 && (v.as_ptr() as usize) % 2 == 0, "aligned"); kani::cover(v.len() % 2 == 1, "odd length"); let max = 3 * (v.len() / 2) + if $lossy { 3 } else { 0 }; let f: fn(&[u8]) -> Option = $call; - match f(v) { - Some(s) => assert!(s.len() <= max), + let res = f(v); + kani::cover(pair && res.is_some(), "starts with a surrogate pair, decoded"); + kani::cover(lone && v.len() % 2 == 0, "starts with an unpaired low surrogate"); + match res { + Some(s) => { + assert!(s.len() <= max); + // Invalid UTF-16: only the lossy variants return a string. + assert!($lossy || !lone); + } None => assert!(!$lossy), } } }; } - utf16_harness!(check_from_utf16le_bounded, 12, 13, false, |v| String::from_utf16le(v).ok()); - utf16_harness!(check_from_utf16be_bounded, 12, 13, false, |v| String::from_utf16be(v).ok()); - utf16_harness!(check_from_utf16le_lossy_bounded, 8, 9, true, |v| Some( - String::from_utf16le_lossy(v) - )); - utf16_harness!(check_from_utf16be_lossy_bounded, 12, 13, true, |v| Some( - String::from_utf16be_lossy(v) - )); + // `unwind(7)`: an input of at most 12 bytes has at most 6 code units, and the decode, + // collect and push loops run at most once per code unit, plus the exit test. + utf16_harness!(check_from_utf16le_bounded, 12, 7, false, false, |v| { + String::from_utf16le(v).ok() + }); + utf16_harness!(check_from_utf16be_bounded, 12, 7, false, true, |v| { + String::from_utf16be(v).ok() + }); + utf16_harness!(check_from_utf16le_lossy_bounded, 12, 7, true, false, |v| { + Some(String::from_utf16le_lossy(v)) + }); + utf16_harness!(check_from_utf16be_lossy_bounded, 12, 7, true, true, |v| { + Some(String::from_utf16be_lossy(v)) + }); + + // --------------------------------------------------------------------------------------- + // Panic harnesses: the documented panic conditions that the harnesses above exclude do + // panic. Each takes a string from `with_char_at` and an index at which it has no char + // boundary: strictly inside its char (so the char is multi-byte), or past the end. With + // `#[kani::should_panic]`, Kani checks that a panic-class failure is reachable and that + // every failing check is of that class (assertions, including arithmetic overflow and + // out-of-bounds indexing), so no UB is reachable before the panic (Kani uses + // `panic=abort`). That the failing checks are exactly the documented panics was checked in + // the verification logs. + // `pop` has no panic condition. `remove` has no panic harness: its panic path for an index + // inside a char formats the message with loops over the string (see `check_remove`). + // --------------------------------------------------------------------------------------- + + /// An index at which the string from `with_char_at` (`c` at `start`, length `len`) has no + /// char boundary: strictly inside `c`, or past the end. + fn any_non_boundary(len: usize, start: usize, c: char) -> usize { + let c_end = start + c.len_utf8(); + let i: usize = kani::any_where(|i: &usize| (start < *i && *i < c_end) || *i > len); + kani::cover(i < len && start > 64 && len > c_end + 64, "inside a char, long string"); + kani::cover(i < len && c.len_utf8() == 4, "inside a 4-byte char"); + kani::cover(i > len, "past the end"); + i + } + + /// A range `a..b` with `a <= b` where at least one end comes from `any_non_boundary` and + /// the other end is arbitrary. + fn any_bad_range(len: usize, start: usize, c: char) -> (usize, usize) { + let bad = any_non_boundary(len, start, c); + let other: usize = kani::any(); + let (a, b) = if bad <= other { (bad, other) } else { (other, bad) }; + kani::cover(a == bad && b <= len, "start not on a char boundary, end in bounds"); + kani::cover(b == bad && b <= len, "end not on a char boundary"); + (a, b) + } + + #[kani::proof] + #[kani::should_panic] + fn check_insert_panics() { + let (mut s, start, c) = with_char_at(); + let idx = any_non_boundary(s.len(), start, c); + s.insert(idx, kani::any()); + } + + #[kani::proof] + #[kani::should_panic] + fn check_insert_str_panics() { + let (mut s, start, c) = with_char_at(); + let len = s.len(); + let idx = any_non_boundary(len, start, c); + let t = any_string_max_len(MAX_ALLOC - len); + s.insert_str(idx, t.as_str()); + } + + #[kani::proof] + #[kani::should_panic] + fn check_split_off_panics() { + let (mut s, start, c) = with_char_at(); + let at = any_non_boundary(s.len(), start, c); + let _ = s.split_off(at); + } + + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics() { + let (mut s, start, c) = with_char_at(); + let (a, b) = any_bad_range(s.len(), start, c); + drop(s.drain(a..b)); + } + + // `unwind(1)`: the `Splice` loops are reachable only after both boundary checks pass, which + // no input here does. Unwinding assertions stay on, so a reachable loop would fail. + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(1)] + fn check_replace_range_panics() { + let (mut s, start, c) = with_char_at(); + let (a, b) = any_bad_range(s.len(), start, c); + s.replace_range(a..b, ""); + } } From b3f7dc861bf505efde4aba1c8c84a44172be8609 Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Fri, 2 Oct 2026 08:30:40 +0300 Subject: [PATCH 5/8] Ch10: split each panic harness into inside-a-char and past-the-end cases A should_panic harness passes as soon as some input panics. With an index that is either inside a multi-byte char or past the end, the past-the-end inputs alone made the harnesses for insert, insert_str, split_off, drain and replace_range pass even without the char-boundary checks (reported by rajath-mk in review). Each of these harnesses is now two: one with an index strictly inside a multi-byte char (for ranges, the other end in bounds, so only a char-boundary check can panic) and one with an index past the end. --- library/alloc/src/string.rs | 125 +++++++++++++++++++++++++++--------- 1 file changed, 95 insertions(+), 30 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index abe146a6f2e1f..91797602d0c9f 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3634,7 +3634,7 @@ mod verify { //! Restrictions. There is no `kani::assume` in this module: every restriction of an input //! is a `kani::any_where` domain at the point where the input is generated (sizes that fit //! in one CBMC object, indices inside the string, the bounds above, and in the panic - //! harnesses indices without a char boundary, `any_non_boundary`). Nothing is assumed + //! harnesses indices without a char boundary, `any_inside_char` and `any_past_end`). Nothing is assumed //! about the result of a function under test. //! //! Contents. Every generated `String` is initialized, valid UTF-8. The harnesses with a @@ -3652,9 +3652,10 @@ mod verify { //! through their input domains: indices are at most the length (an `any_where` domain), and //! every such index of an all-NUL string is a char boundary by construction (the harnesses //! `assert!` this before the call); `with_char_at` puts a char at the index that `remove` - //! removes. The `check_*_panics` harnesses (`#[kani::should_panic]`) show for `insert`, - //! `insert_str`, `split_off`, `drain` and `replace_range` that an index strictly inside a - //! multi-byte char, or past the end, panics. Reversed ranges and `Bound` overflow + //! removes. The `check_*_panics_inside_char` and `check_*_panics_past_end` harnesses + //! (`#[kani::should_panic]`) show for `insert`, `insert_str`, `split_off`, `drain` and + //! `replace_range` that an index strictly inside a multi-byte char panics, and separately + //! that an index past the end panics. Reversed ranges and `Bound` overflow //! (`..=usize::MAX`) are not exercised there. use core::cell::Cell; use core::kani; @@ -4171,70 +4172,134 @@ mod verify { // inside a char formats the message with loops over the string (see `check_remove`). // --------------------------------------------------------------------------------------- - /// An index at which the string from `with_char_at` (`c` at `start`, length `len`) has no - /// char boundary: strictly inside `c`, or past the end. - fn any_non_boundary(len: usize, start: usize, c: char) -> usize { + /// An index strictly inside the encoding of `c`, which starts at byte `start`: in bounds, + /// but not a char boundary. There is none if `c` is ASCII; the covers show the other widths. + fn any_inside_char(len: usize, start: usize, c: char) -> usize { let c_end = start + c.len_utf8(); - let i: usize = kani::any_where(|i: &usize| (start < *i && *i < c_end) || *i > len); - kani::cover(i < len && start > 64 && len > c_end + 64, "inside a char, long string"); - kani::cover(i < len && c.len_utf8() == 4, "inside a 4-byte char"); - kani::cover(i > len, "past the end"); + let i: usize = kani::any_where(|i: &usize| start < *i && *i < c_end); + kani::cover(start > 64 && len > c_end + 64, "inside a char, long string"); + kani::cover(c.len_utf8() == 2, "inside a 2-byte char"); + kani::cover(c.len_utf8() == 4, "inside a 4-byte char"); i } - /// A range `a..b` with `a <= b` where at least one end comes from `any_non_boundary` and - /// the other end is arbitrary. - fn any_bad_range(len: usize, start: usize, c: char) -> (usize, usize) { - let bad = any_non_boundary(len, start, c); - let other: usize = kani::any(); + /// An index past the end of a string of length `len`. + fn any_past_end(len: usize) -> usize { + let i: usize = kani::any_where(|i: &usize| *i > len); + kani::cover(len > 64, "past the end of a long string"); + kani::cover(i == len + 1, "one past the end"); + i + } + + /// A range `a..b` with `a <= b <= len` where at least one end is inside the encoding of `c`. + /// Both ends are in bounds, so a panic can only come from a char-boundary check. + fn any_range_inside_char(len: usize, start: usize, c: char) -> (usize, usize) { + let bad = any_inside_char(len, start, c); + let other: usize = kani::any_where(|o: &usize| *o <= len); let (a, b) = if bad <= other { (bad, other) } else { (other, bad) }; - kani::cover(a == bad && b <= len, "start not on a char boundary, end in bounds"); - kani::cover(b == bad && b <= len, "end not on a char boundary"); + kani::cover(a == bad && b != bad, "only the start is inside a char"); + kani::cover(b == bad && a != bad, "only the end is inside a char"); (a, b) } + /// A range `a..b` with `a <= b` whose end is past the end of a string of length `len`. + fn any_range_past_end(len: usize) -> (usize, usize) { + let b = any_past_end(len); + let a: usize = kani::any_where(|a: &usize| *a <= b); + kani::cover(a <= len, "only the end is past the end"); + (a, b) + } + + // Each panic condition has its own harness. A `should_panic` harness passes as soon as some + // input panics, so with both kinds of index in one harness the past-the-end inputs alone + // would make it pass even without the char-boundary checks. + #[kani::proof] #[kani::should_panic] - fn check_insert_panics() { + fn check_insert_panics_inside_char() { let (mut s, start, c) = with_char_at(); - let idx = any_non_boundary(s.len(), start, c); + let idx = any_inside_char(s.len(), start, c); + s.insert(idx, kani::any()); + } + + #[kani::proof] + #[kani::should_panic] + fn check_insert_panics_past_end() { + let (mut s, _, _) = with_char_at(); + let idx = any_past_end(s.len()); s.insert(idx, kani::any()); } #[kani::proof] #[kani::should_panic] - fn check_insert_str_panics() { + fn check_insert_str_panics_inside_char() { let (mut s, start, c) = with_char_at(); let len = s.len(); - let idx = any_non_boundary(len, start, c); + let idx = any_inside_char(len, start, c); let t = any_string_max_len(MAX_ALLOC - len); s.insert_str(idx, t.as_str()); } #[kani::proof] #[kani::should_panic] - fn check_split_off_panics() { + fn check_insert_str_panics_past_end() { + let (mut s, _, _) = with_char_at(); + let len = s.len(); + let idx = any_past_end(len); + let t = any_string_max_len(MAX_ALLOC - len); + s.insert_str(idx, t.as_str()); + } + + #[kani::proof] + #[kani::should_panic] + fn check_split_off_panics_inside_char() { let (mut s, start, c) = with_char_at(); - let at = any_non_boundary(s.len(), start, c); + let at = any_inside_char(s.len(), start, c); let _ = s.split_off(at); } #[kani::proof] #[kani::should_panic] - fn check_drain_panics() { + fn check_split_off_panics_past_end() { + let (mut s, _, _) = with_char_at(); + let at = any_past_end(s.len()); + let _ = s.split_off(at); + } + + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics_inside_char() { let (mut s, start, c) = with_char_at(); - let (a, b) = any_bad_range(s.len(), start, c); + let (a, b) = any_range_inside_char(s.len(), start, c); drop(s.drain(a..b)); } - // `unwind(1)`: the `Splice` loops are reachable only after both boundary checks pass, which - // no input here does. Unwinding assertions stay on, so a reachable loop would fail. + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics_past_end() { + let (mut s, _, _) = with_char_at(); + let (a, b) = any_range_past_end(s.len()); + drop(s.drain(a..b)); + } + + // `unwind(1)` on the two `replace_range` harnesses: the `Splice` loops are reachable only + // after both boundary checks pass, which no input here does. Unwinding assertions stay on, + // so a reachable loop would fail. #[kani::proof] #[kani::should_panic] #[kani::unwind(1)] - fn check_replace_range_panics() { + fn check_replace_range_panics_inside_char() { let (mut s, start, c) = with_char_at(); - let (a, b) = any_bad_range(s.len(), start, c); + let (a, b) = any_range_inside_char(s.len(), start, c); + s.replace_range(a..b, ""); + } + + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(1)] + fn check_replace_range_panics_past_end() { + let (mut s, _, _) = with_char_at(); + let (a, b) = any_range_past_end(s.len()); s.replace_range(a..b, ""); } } From a50a5f488aac3d3a65d509fadb9eb461ee86996f Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Wed, 14 Oct 2026 03:46:18 +0300 Subject: [PATCH 6/8] Ch10: update the harnesses for current main - retain: main now has the PanicGuard version, whose drop runs debug_assert!(str::from_utf8(..).is_ok()). Under -Z loop-contracts the abstracted validator can reject valid UTF-8 with a multi-byte char. check_retain_bounded now checks the exact result (up to 5 chars) and replaces from_utf8 by from_utf8_kept, which accepts only the expected bytes. - from_utf16*: check Ok/Err and the exact length against a reference decoder (utf16_expected); big-endian inputs up to 16 bytes; comments follow the new from_utf16_units loop. - New panic harnesses: remove (inside a char, at the end, past the end), and for drain and replace_range a reversed range, ..=usize::MAX and (Excluded(usize::MAX), Unbounded). --- library/alloc/src/string.rs | 448 ++++++++++++++++++++++++++++-------- 1 file changed, 354 insertions(+), 94 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 38870bc2d65dd..98dec026d1eb3 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3690,14 +3690,16 @@ mod verify { //! and `check_pop`, `check_remove`, `check_insert`, `check_drain_drop`, `check_drain_next`, //! `check_into_boxed_str`, `check_leak`. No loop is reachable on their verified paths, so //! no unwind bound limits the input. `check_remove` has `#[kani::unwind(2)]` only to cut an - //! infeasible panic-formatting path (see the comment on it). The `check_*_panics` - //! harnesses are unbounded too (`#[kani::unwind(1)]` on `check_replace_range_panics` only - //! covers loops that no input reaches, see the comment on it). + //! infeasible panic path (see the comment on it). The `check_*_panics_*` harnesses are + //! unbounded too: `#[kani::unwind(1)]` on the `replace_range` ones only covers loops that + //! no input reaches, and `#[kani::unwind(4)]` on `check_remove_panics_inside_char` covers a + //! loop of at most 3 iterations (see the comments on them). //! * Receiver of any length, bounded edit: `check_replace_range` (removed and inserted //! ranges of at most 4 bytes each) and `check_remove_matches` (at most 5 matches). Their //! loops run once per edited byte or per match, never once per receiver byte. - //! * Bounded because of tool limits: `check_retain_bounded` (strings of up to 12 chars) and - //! the `from_utf16*` harnesses (inputs of up to 12 bytes). See the comment above them. + //! * Bounded because of tool limits: `check_retain_bounded` (strings of up to 5 chars) and + //! the `from_utf16*` harnesses (inputs of up to 12 bytes for the little-endian and 16 bytes + //! for the big-endian variants). See the comment above them. //! //! Every `#[kani::unwind]` bound is checked by unwinding assertions, so a bound that is too //! small makes the proof fail instead of silently cutting executions. @@ -3705,8 +3707,12 @@ mod verify { //! Restrictions. There is no `kani::assume` in this module: every restriction of an input //! is a `kani::any_where` domain at the point where the input is generated (sizes that fit //! in one CBMC object, indices inside the string, the bounds above, and in the panic - //! harnesses indices without a char boundary, `any_inside_char` and `any_past_end`). Nothing is assumed - //! about the result of a function under test. + //! harnesses the cause of the panic: `any_inside_char`, `any_past_end` and + //! `any_reversed_range`). Nothing is assumed about the result of a function under test. + //! + //! Stubs. One: `check_retain_bounded` replaces `core::str::from_utf8`, which `retain` calls in + //! a `debug_assert!`, with `from_utf8_kept`, which checks that the bytes are exactly the + //! chars the predicate kept (see the comment on it). No function under test is replaced. //! //! Contents. Every generated `String` is initialized, valid UTF-8. The harnesses with a //! symbolic length use a zeroed buffer, i.e. a string of NUL chars (`any_string`), and, where a @@ -3724,10 +3730,12 @@ mod verify { //! every such index of an all-NUL string is a char boundary by construction (the harnesses //! `assert!` this before the call); `with_char_at` puts a char at the index that `remove` //! removes. The `check_*_panics_inside_char` and `check_*_panics_past_end` harnesses - //! (`#[kani::should_panic]`) show for `insert`, `insert_str`, `split_off`, `drain` and - //! `replace_range` that an index strictly inside a multi-byte char panics, and separately - //! that an index past the end panics. Reversed ranges and `Bound` overflow - //! (`..=usize::MAX`) are not exercised there. + //! (`#[kani::should_panic]`) show for `insert`, `insert_str`, `split_off`, `remove`, `drain` + //! and `replace_range` that an index strictly inside a multi-byte char panics, and separately + //! that an index past the end panics. Further `should_panic` harnesses show that `remove` + //! panics at the end of the string, and that `drain` and `replace_range` panic for a reversed + //! range, for `..=usize::MAX` and for `(Excluded(usize::MAX), Unbounded)`. Each harness has a + //! single cause of panic in its input domain. use core::cell::Cell; use core::kani; use core::ops::Bound; @@ -3828,12 +3836,12 @@ mod verify { } } - // `self[idx..]` has a panic path (`str::slice_error_fail`) that formats the error message - // with loops over the string. Under this harness that path is infeasible (`idx` is the - // start of a well-formed char), but symbolic execution would still unfold it without end. - // The unwind bound only cuts that path: unwinding assertions stay enabled, so any loop that - // is actually reachable and needs more iterations makes the proof fail. No loop is - // reachable on the verified (non-panicking) path, so input sizes stay unbounded. + // `self[idx..]` has a panic path (`str::slice_error_fail_rt`) with a loop + // (`ceil_char_boundary`). Under this harness that path is infeasible (`idx` is the start of + // a well-formed char). The unwind bound only cuts that path: unwinding assertions stay + // enabled, so any loop that is actually reachable and needs more iterations makes the proof + // fail. No loop is reachable on the verified (non-panicking) path, so input sizes stay + // unbounded. #[kani::proof] #[kani::unwind(2)] fn check_remove() { @@ -4109,77 +4117,236 @@ mod verify { } // --------------------------------------------------------------------------------------- - // BOUNDED harnesses for the remaining "(U)" functions (`retain`, `from_utf16le/be` and their - // `_lossy` variants). Their loops cannot be given loop contracts with the pinned Kani. - // `retain`: symbolic-bound quantifiers are dropped by the SAT backend, calls inside loop - // invariants are replaced by nondeterministic values, and the `Chars` temporary of the loop - // body cannot be named in `loop_modifies`. `from_utf16*`: the aligned `from_utf16le` path - // loops with `for` over `DecodeUtf16`, which the loop-contract macro rejects; every other - // path loops inside the generic default `Iterator::try_fold` / `fold` (via `collect`), whose - // state cannot be named in an invariant; and each of these loops pushes to a `String`, while - // loop contracts do not allow the loop body to allocate or free memory. These harnesses - // verify the real bodies up to the stated sizes (the unwinding assertions make an - // insufficient bound fail). + // BOUNDED harnesses for the remaining "(U)" functions: `retain`, `from_utf16le/be` and their + // `_lossy` variants. With the pinned Kani their loops cannot carry loop contracts: + // * `retain` (the `PanicGuard` version) reads the unread tail with `get_unchecked` and + // `unwrap_unchecked`, so an invariant must state that the tail is still valid UTF-8 after + // the earlier moves: a quantifier over a symbolic range, which CI's SAT backend does not + // support (kani#4719). Its first loop runs over a `CharIndices`, whose state an invariant + // can only reach through method calls, which loop invariants do not support (kani#4796). + // * `from_utf16le` and `from_utf16be` loop with `for` over `DecodeUtf16` in + // `from_utf16_units`, which loop contracts do not support (kani#4907); the `_lossy` + // variants loop inside `Iterator::fold` (via `collect`), where a loop contract has no + // attach site (kani#4893). All of these loops push to a `String`, and a loop with a + // contract may not allocate (kani#3587). + // These harnesses verify the real bodies up to the stated sizes (the unwinding assertions + // make an insufficient bound fail). // --------------------------------------------------------------------------------------- - /// Up to `N` arbitrary chars encoded back to back into a zeroed (initialized) buffer of - /// `4 * N` bytes, which is then truncated to the encoded length (valid UTF-8 by construction; - /// no reallocation, which keeps the harness CI-sized). - fn any_valid_string() -> String { - let chars: [char; N] = kani::any(); - let n: usize = kani::any_where(|n: &usize| *n <= N); - let mut v: Vec = vec![0u8; 4 * N]; - let mut off = 0; - for i in 0..n { - let l = chars[i].len_utf8(); - chars[i].encode_utf8(&mut v[off..off + l]); - off += l; - } - v.truncate(off); - // SAFETY (harness): `v` is exactly the concatenation of the UTF-8 encodings of - // `chars[..n]` (`truncate` drops only the unused zero bytes after them): valid UTF-8. - unsafe { String::from_utf8_unchecked(v) } + /// `check_retain_bounded` takes strings of at most this many chars. + const RETAIN_BOUND: usize = 5; + /// Length of the byte arrays in `check_retain_bounded`. A char is stored as 4 bytes (its + /// UTF-8 encoding, then zeros), so `4 * RETAIN_BOUND` = 20 bytes are needed; 24 is that + /// rounded up to three whole `u64` words. + const RETAIN_BYTES: usize = 24; + + /// What `check_retain_bounded` expects `retain` to leave in the string: the UTF-8 encodings + /// of the chars that the predicate keeps, back to back, then zeros. The harness sets it + /// before it calls `retain`, and `from_utf8_kept` compares against it. A harness runs on a + /// single thread, so nothing else touches these statics. + static mut RETAIN_AFTER: [u8; RETAIN_BYTES] = [0; RETAIN_BYTES]; + /// The number of bytes at the start of `RETAIN_AFTER` that form the expected string. + static mut RETAIN_AFTER_LEN: usize = 0; + + /// The bytes of `v` (at most `RETAIN_BYTES` of them), then zeros up to `RETAIN_BYTES`. + fn zero_padded(v: &[u8]) -> [u8; RETAIN_BYTES] { + let mut out = [0u8; RETAIN_BYTES]; + out[..v.len()].copy_from_slice(v); + out + } + + /// Whether `a == b`, decided by comparing three `u64` words at fixed positions, so that + /// there is no loop to unwind. + fn equal_padded(a: [u8; RETAIN_BYTES], b: [u8; RETAIN_BYTES]) -> bool { + // SAFETY: `[u8; 24]` and `[u64; 3]` are the same size, and any 64 bits are a valid `u64`. + let x: [u64; 3] = unsafe { core::mem::transmute(a) }; + // SAFETY: as for `x`. + let y: [u64; 3] = unsafe { core::mem::transmute(b) }; + x[0] == y[0] && x[1] == y[1] && x[2] == y[2] + } + + /// Replaces `core::str::from_utf8` in `check_retain_bounded`. + /// + /// Once `retain` has removed a char, it ends by dropping its `PanicGuard`, and that drop runs + /// `debug_assert!(str::from_utf8(..).is_ok())` on the new contents. CI passes + /// `-Z loop-contracts`, so the real validator (`run_utf8_validation` in + /// `core/src/str/validations.rs`) is checked with its loops replaced by their invariants. + /// Those invariants do not keep the index on a char boundary, so the validator can then + /// reject valid UTF-8 that contains a multi-byte char, and the `debug_assert!` fails on + /// correct bytes. + /// + /// This stand-in accepts one input only: the bytes in `RETAIN_AFTER`. On any other input + /// it panics, which fails the harness (`alloc` cannot construct a `Utf8Error`). The accepted + /// bytes are valid UTF-8, so the real `from_utf8` returns `Ok` whenever this one does. The + /// stand-in can therefore add failures but never hide one, and it checks the exact contents, + /// not only their validity. + fn from_utf8_kept(v: &[u8]) -> Result<&str, core::str::Utf8Error> { + // SAFETY (harness): plain reads of the statics; see `RETAIN_AFTER`. + let (want, want_len) = unsafe { (RETAIN_AFTER, RETAIN_AFTER_LEN) }; + assert!( + v.len() == want_len && equal_padded(zero_padded(v), want), + "from_utf8 stand-in: bytes differ from RETAIN_AFTER" + ); + // SAFETY: `v` equals the expected bytes, which are UTF-8 encodings of chars. + Ok(unsafe { core::str::from_utf8_unchecked(v) }) } - /// `retain` on any valid string of up to 12 chars (<= 48 bytes), arbitrary keep-predicate. - /// `unwind(13)`: the generator's loop and the `retain` loop run once per char (at most 12), - /// plus the exit test. + /// Inputs: up to `RETAIN_BOUND` chars, each of them any `char`, and for every call of the + /// predicate any answer: the answer to the `i`-th call is `answers[i]`. The predicate also + /// records the char it gets in each call. After `retain` returns, the harness checks that + /// there was one call per char, in the order of the chars, and that the string now holds + /// exactly the kept chars: first its length, then its bytes. When `retain` removes a char, + /// `from_utf8_kept` also compares the bytes inside `retain`. + /// `unwind(6)`: each loop runs at most once per char (at most 5 times), plus the exit test. #[kani::proof] - #[kani::unwind(13)] + #[kani::unwind(6)] + #[kani::stub(core::str::from_utf8, from_utf8_kept)] fn check_retain_bounded() { - let mut s = any_valid_string::<12>(); - // Bytes of the chars the predicate keeps (`retain` calls it once per char, in order). - let kept = Cell::new(0usize); - // Observers for the cover below; they do not influence the predicate's result. - let deleted = Cell::new(false); - let kept_multibyte_after_deletion = Cell::new(false); - s.retain(|c| { - let keep: bool = kani::any(); - if !keep { - deleted.set(true); - } else { - kept.set(kept.get() + c.len_utf8()); - if c.len_utf8() > 1 && deleted.get() { - kept_multibyte_after_deletion.set(true); - } + let chars: [char; RETAIN_BOUND] = kani::any(); + let n: usize = kani::any_where(|n: &usize| *n <= RETAIN_BOUND); + let answers: [bool; RETAIN_BOUND] = kani::any(); + + // One pass over `chars[..n]` builds `before`, the bytes of the string, and `after`, the + // bytes that `retain` has to leave. Each char is stored as 4 bytes, its encoding and + // then zeros, at the current end; the next char starts where the encoding ends and + // overwrites the zeros. Storing whole 4-byte groups keeps the formula small. + let mut before = [0u8; RETAIN_BYTES]; + let mut before_len = 0; + let mut after = [0u8; RETAIN_BYTES]; + let mut after_len = 0; + // Facts about the moves that `retain` has to make, for the covers at the end. + let mut multibyte_kept_in_place = false; + let mut overlapping_move = false; + for i in 0..n { + let ch = chars[i]; + let mut utf8 = [0u8; 4]; + ch.encode_utf8(&mut utf8); + let width = ch.len_utf8(); + before[before_len] = utf8[0]; + before[before_len + 1] = utf8[1]; + before[before_len + 2] = utf8[2]; + before[before_len + 3] = utf8[3]; + if answers[i] { + // `retain` moves a kept char left by the number of bytes removed before it. + let shift = before_len - after_len; + multibyte_kept_in_place |= shift == 0 && width > 1; + overlapping_move |= shift > 0 && shift < width; + after[after_len] = utf8[0]; + after[after_len + 1] = utf8[1]; + after[after_len + 2] = utf8[2]; + after[after_len + 3] = utf8[3]; + after_len += width; } - keep + before_len += width; + } + // SAFETY (harness): plain writes of the statics, before `retain` runs. + unsafe { + RETAIN_AFTER = after; + RETAIN_AFTER_LEN = after_len; + } + + // The string gets its bytes in one copy of the whole array (building it char by char + // with `Vec::extend_from_slice` made CBMC run out of memory). + let mut owned = before.to_vec(); + owned.truncate(before_len); + // SAFETY (harness): `owned` holds the UTF-8 encodings of `chars[..n]`, back to back. + let mut s = unsafe { String::from_utf8_unchecked(owned) }; + + let mut calls = 0; + let mut visited = ['\0'; RETAIN_BOUND]; + s.retain(|c| { + // More than `RETAIN_BOUND` calls index past the end of `visited` and fail the harness + // here; the count check below catches any other wrong number of calls. (Indexing + // without a check first also lets CBMC cut those paths early.) + visited[calls] = c; + let answer = answers[calls]; + calls += 1; + answer }); + + assert!(calls == n, "one predicate call per char"); + for i in 0..n { + assert!(visited[i] == chars[i], "predicate calls follow the order of the chars"); + } + assert!(s.len() == after_len, "new length = total UTF-8 length of the kept chars"); + assert!( + equal_padded(zero_padded(s.as_bytes()), after), + "new bytes = encodings of the kept chars, back to back" + ); + + // Paths through `retain`: its first loop returns; its second loop starts at offset 0 or + // after a multi-byte char; it moves a char onto bytes that the char itself occupies + // (`ptr::copy` with overlapping ranges); it ends with length 0. + let removed_some = after_len < before_len; + kani::cover(n > 0 && !removed_some, "nothing rejected: the first loop returns"); + kani::cover(n > 0 && !answers[0], "first char rejected: the second loop writes from 0"); + kani::cover( + multibyte_kept_in_place && removed_some, + "rejection after a kept multi-byte char", + ); kani::cover( - kept_multibyte_after_deletion.get(), - "multi-byte char kept after a deletion (moved by the unsafe re-encode)", + overlapping_move, + "a char moves left by less than its length: overlapping copy", ); - assert!(s.len() == kept.get()); + kani::cover(n > 0 && after_len == 0, "every char rejected: the length drops to 0"); + } + + /// What `char::decode_utf16` makes of the bytes `v` read as code units (big-endian if `be`): + /// whether `v` is valid UTF-16 (an even number of bytes, every surrogate paired), and the + /// UTF-8 length of the decoded string, where each unpaired surrogate and a trailing odd + /// byte count as U+FFFD (3 bytes), as in the `_lossy` variants. `N`: the most bytes `v` can + /// have. + fn utf16_expected(v: &[u8], be: bool) -> (bool, usize) { + let units = v.len() / 2; + let mut valid = v.len() % 2 == 0; + let mut out = if v.len() % 2 == 1 { 3 } else { 0 }; + // Whether the previous code unit is a high surrogate that is still waiting for its pair. + let mut high = false; + for i in 0..N / 2 { + if i < units { + let b = [v[2 * i], v[2 * i + 1]]; + let u = if be { u16::from_be_bytes(b) } else { u16::from_le_bytes(b) }; + let is_high = (0xD800..=0xDBFF).contains(&u); + let is_low = (0xDC00..=0xDFFF).contains(&u); + if high && is_low { + // A surrogate pair: one char outside the BMP, 4 bytes. + out += 4; + high = false; + } else { + if high { + // The previous high surrogate is unpaired. + valid = false; + out += 3; + } + high = is_high; + if is_low { + valid = false; + out += 3; + } else if !is_high { + out += if u < 0x80 { + 1 + } else if u < 0x800 { + 2 + } else { + 3 + }; + } + } + } + } + if high { + valid = false; + out += 3; + } + (valid, out) } /// An arbitrary byte slice of length `<= N` at an arbitrary (odd or even) address, so both /// the aligned (`align_to` succeeds) and the unaligned paths, and odd lengths, are - /// exercised. Each UTF-16 code unit decodes to at most 3 UTF-8 bytes (a surrogate pair, - /// 2 units, to 4), and a trailing odd byte becomes U+FFFD (3 bytes) in the lossy variants. - /// An input whose first code unit (in the byte order of the function, `$be`) is a low - /// surrogate is invalid UTF-16, so the strict variants must return `Err`. The covers read - /// only the input and whether the result is `Ok`: reading the bytes of the decoded string - /// made CBMC run out of memory at these sizes. + /// exercised. The strict variants must return `Ok` exactly for valid UTF-16, and every + /// returned string must have the length that `utf16_expected` computes. The covers read + /// only the input and the result's length: reading the bytes of the decoded string made + /// CBMC run out of memory at these sizes. macro_rules! utf16_harness { ($name:ident, $n:literal, $unwind:literal, $lossy:literal, $be:literal, $call:expr) => { #[kani::proof] @@ -4187,60 +4354,61 @@ mod verify { fn $name() { let arr: [u8; $n] = kani::any(); let v = kani::slice::any_slice_of_array(&arr); + let (valid, out_len) = utf16_expected::<$n>(v, $be); // Code unit `i` of `v`, in the byte order of the function under test. let unit = |i: usize| { let b = [v[2 * i], v[2 * i + 1]]; if $be { u16::from_be_bytes(b) } else { u16::from_le_bytes(b) } }; - let lone = v.len() >= 2 && (0xDC00..=0xDFFF).contains(&unit(0)); - let pair = v.len() >= 4 - && (0xD800..=0xDBFF).contains(&unit(0)) - && (0xDC00..=0xDFFF).contains(&unit(1)); kani::cover(v.len() >= 4 && (v.as_ptr() as usize) % 2 == 1, "unaligned"); kani::cover(v.len() >= 4 && (v.as_ptr() as usize) % 2 == 0, "aligned"); kani::cover(v.len() % 2 == 1, "odd length"); - let max = 3 * (v.len() / 2) + if $lossy { 3 } else { 0 }; + kani::cover( + v.len() >= 4 + && (0xD800..=0xDBFF).contains(&unit(0)) + && (0xDC00..=0xDFFF).contains(&unit(1)), + "starts with a surrogate pair", + ); + kani::cover(!valid && v.len() % 2 == 0, "unpaired surrogate"); let f: fn(&[u8]) -> Option = $call; - let res = f(v); - kani::cover(pair && res.is_some(), "starts with a surrogate pair, decoded"); - kani::cover(lone && v.len() % 2 == 0, "starts with an unpaired low surrogate"); - match res { + match f(v) { Some(s) => { - assert!(s.len() <= max); - // Invalid UTF-16: only the lossy variants return a string. - assert!($lossy || !lone); + assert!($lossy || valid, "Ok only for valid UTF-16"); + assert!(s.len() == out_len, "the decoded string has the expected length"); } - None => assert!(!$lossy), + None => assert!(!$lossy && !valid, "Err only for invalid UTF-16"), } } }; } - // `unwind(7)`: an input of at most 12 bytes has at most 6 code units, and the decode, - // collect and push loops run at most once per code unit, plus the exit test. + // `unwind(N / 2 + 1)`: an input of at most `N` bytes has at most `N / 2` code units, and + // every loop (the decode and push loops, and the one in `utf16_expected`) runs at most once + // per code unit, plus the exit test. utf16_harness!(check_from_utf16le_bounded, 12, 7, false, false, |v| { String::from_utf16le(v).ok() }); - utf16_harness!(check_from_utf16be_bounded, 12, 7, false, true, |v| { + utf16_harness!(check_from_utf16be_bounded, 16, 9, false, true, |v| { String::from_utf16be(v).ok() }); utf16_harness!(check_from_utf16le_lossy_bounded, 12, 7, true, false, |v| { Some(String::from_utf16le_lossy(v)) }); - utf16_harness!(check_from_utf16be_lossy_bounded, 12, 7, true, true, |v| { + utf16_harness!(check_from_utf16be_lossy_bounded, 16, 9, true, true, |v| { Some(String::from_utf16be_lossy(v)) }); // --------------------------------------------------------------------------------------- // Panic harnesses: the documented panic conditions that the harnesses above exclude do - // panic. Each takes a string from `with_char_at` and an index at which it has no char + // panic. Most take a string from `with_char_at` and an index at which it has no char // boundary: strictly inside its char (so the char is multi-byte), or past the end. With // `#[kani::should_panic]`, Kani checks that a panic-class failure is reachable and that // every failing check is of that class (assertions, including arithmetic overflow and // out-of-bounds indexing), so no UB is reachable before the panic (Kani uses // `panic=abort`). That the failing checks are exactly the documented panics was checked in // the verification logs. - // `pop` has no panic condition. `remove` has no panic harness: its panic path for an index - // inside a char formats the message with loops over the string (see `check_remove`). + // `pop` has no panic condition. `drain` and `replace_range` also panic for a reversed range + // and for the two `RangeBounds` shapes whose conversion to `start..end` would overflow + // without the checks of `slice::range`; `remove` also panics at the end of the string. // --------------------------------------------------------------------------------------- /// An index strictly inside the encoding of `c`, which starts at byte `start`: in bounds, @@ -4373,4 +4541,96 @@ mod verify { let (a, b) = any_range_past_end(s.len()); s.replace_range(a..b, ""); } + + // `unwind(4)`: on this path `str::slice_error_fail_rt` finds the char around the index with + // `ceil_char_boundary`, whose loop runs at most 3 times (the next char boundary is at most + // 3 bytes away); no other loop is reachable. Unwinding assertions stay on. + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(4)] + fn check_remove_panics_inside_char() { + let (mut s, start, c) = with_char_at(); + let idx = any_inside_char(s.len(), start, c); + let _ = s.remove(idx); + } + + /// `remove(len)`: in bounds and a char boundary, but there is no char to remove. + #[kani::proof] + #[kani::should_panic] + fn check_remove_panics_at_end() { + let mut s = any_string(); + let len = s.len(); + kani::cover(len > 64, "at the end of a long string"); + let _ = s.remove(len); + } + + #[kani::proof] + #[kani::should_panic] + fn check_remove_panics_past_end() { + let (mut s, _, _) = with_char_at(); + let idx = any_past_end(s.len()); + let _ = s.remove(idx); + } + + /// A reversed range `a..b`, `b < a <= len`, of the all-NUL string `any_string`: both ends are + /// in bounds and char boundaries, so the reversal is the only cause of a panic. + fn any_reversed_range(len: usize) -> (usize, usize) { + let a: usize = kani::any_where(|a: &usize| *a > 0 && *a <= len); + let b: usize = kani::any_where(|b: &usize| *b < a); + kani::cover(len > 64 && a < len && b > 0, "reversed range inside a long string"); + (a, b) + } + + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics_reversed() { + let mut s = any_string(); + let (a, b) = any_reversed_range(s.len()); + drop(s.drain(a..b)); + } + + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(1)] + fn check_replace_range_panics_reversed() { + let mut s = any_string(); + let (a, b) = any_reversed_range(s.len()); + s.replace_range(a..b, ""); + } + + // `..=usize::MAX` (`end + 1` would overflow) and `(Excluded(usize::MAX), Unbounded)` + // (`start + 1` would overflow), one harness each. + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics_end_included_max() { + let mut s = any_string(); + kani::cover(s.len() > 64, "long string"); + drop(s.drain(..=usize::MAX)); + } + + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics_start_excluded_max() { + let mut s = any_string(); + kani::cover(s.len() > 64, "long string"); + drop(s.drain((Bound::Excluded(usize::MAX), Bound::Unbounded))); + } + + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(1)] + fn check_replace_range_panics_end_included_max() { + let mut s = any_string(); + kani::cover(s.len() > 64, "long string"); + s.replace_range(..=usize::MAX, ""); + } + + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(1)] + fn check_replace_range_panics_start_excluded_max() { + let mut s = any_string(); + kani::cover(s.len() > 64, "long string"); + s.replace_range((Bound::Excluded(usize::MAX), Bound::Unbounded), ""); + } } From 93c332f3f91174f67e3a2dd118ed545928526262 Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Wed, 14 Oct 2026 04:02:03 +0300 Subject: [PATCH 7/8] Ch10: one failing check per range panic harness drain and replace_range check a range a..b in this order: b <= len and a <= b (slice::range), then that a, and then b, is a char boundary. Split the "inside a char" harnesses into start inside, end inside and both inside, so that without the check that should fail no input of a harness panics. The past-the-end harnesses now take any start, and the reversed-range harnesses any start greater than the end, so that these domains and the valid ranges of the main harnesses cover every pair (a, b). --- library/alloc/src/string.rs | 117 +++++++++++++++++++++++++++--------- 1 file changed, 90 insertions(+), 27 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 98dec026d1eb3..4a65b9a280d7b 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3707,7 +3707,7 @@ mod verify { //! Restrictions. There is no `kani::assume` in this module: every restriction of an input //! is a `kani::any_where` domain at the point where the input is generated (sizes that fit //! in one CBMC object, indices inside the string, the bounds above, and in the panic - //! harnesses the cause of the panic: `any_inside_char`, `any_past_end` and + //! harnesses the cause of the panic, e.g. `any_inside_char`, `any_past_end` and //! `any_reversed_range`). Nothing is assumed about the result of a function under test. //! //! Stubs. One: `check_retain_bounded` replaces `core::str::from_utf8`, which `retain` calls in @@ -3729,13 +3729,13 @@ mod verify { //! through their input domains: indices are at most the length (an `any_where` domain), and //! every such index of an all-NUL string is a char boundary by construction (the harnesses //! `assert!` this before the call); `with_char_at` puts a char at the index that `remove` - //! removes. The `check_*_panics_inside_char` and `check_*_panics_past_end` harnesses - //! (`#[kani::should_panic]`) show for `insert`, `insert_str`, `split_off`, `remove`, `drain` - //! and `replace_range` that an index strictly inside a multi-byte char panics, and separately - //! that an index past the end panics. Further `should_panic` harnesses show that `remove` - //! panics at the end of the string, and that `drain` and `replace_range` panic for a reversed - //! range, for `..=usize::MAX` and for `(Excluded(usize::MAX), Unbounded)`. Each harness has a - //! single cause of panic in its input domain. + //! removes. The `#[kani::should_panic]` harnesses show for `insert`, `insert_str`, + //! `split_off` and `remove` that an index strictly inside a multi-byte char panics, and + //! separately that an index past the end panics, and that `remove` panics at the end of the + //! string. For `drain` and `replace_range` they show the same for a range with its start, + //! its end, or both inside a char, for a range whose end is past the end, for a reversed + //! range, for `..=usize::MAX` and for `(Excluded(usize::MAX), Unbounded)`. In each harness, + //! every input fails the same check of the function under test. use core::cell::Cell; use core::kani; use core::ops::Bound; @@ -4405,7 +4405,9 @@ mod verify { // every failing check is of that class (assertions, including arithmetic overflow and // out-of-bounds indexing), so no UB is reachable before the panic (Kani uses // `panic=abort`). That the failing checks are exactly the documented panics was checked in - // the verification logs. + // the verification logs. In each harness every input fails the same check (for a reversed + // range whose start is also past the length, `slice::range` reports that check with the + // message for a start out of range). // `pop` has no panic condition. `drain` and `replace_range` also panic for a reversed range // and for the two `RangeBounds` shapes whose conversion to `start..end` would overflow // without the checks of `slice::range`; `remove` also panics at the end of the string. @@ -4430,22 +4432,48 @@ mod verify { i } - /// A range `a..b` with `a <= b <= len` where at least one end is inside the encoding of `c`. - /// Both ends are in bounds, so a panic can only come from a char-boundary check. - fn any_range_inside_char(len: usize, start: usize, c: char) -> (usize, usize) { - let bad = any_inside_char(len, start, c); - let other: usize = kani::any_where(|o: &usize| *o <= len); - let (a, b) = if bad <= other { (bad, other) } else { (other, bad) }; - kani::cover(a == bad && b != bad, "only the start is inside a char"); - kani::cover(b == bad && a != bad, "only the end is inside a char"); + // For a range `a..b`, `drain` and `replace_range` check, in this order: `b <= len` and + // `a <= b` (both in `slice::range`), then that `a`, and then `b`, is a char boundary. The + // domains of `any_range_past_end`, `any_reversed_range` and the three helpers for ranges + // inside a char, together with the valid ranges of the main harnesses, split all pairs + // `(a, b)` along these checks. + + // In `with_char_at`'s string, the only indices that are not char boundaries are strictly + // inside `c`. A range `a..b`, `a <= b <= len`, that fails a boundary check has its start + // inside `c` and its end at or after the end of `c`, or its start at or before the start of + // `c` and its end inside `c`, or both ends inside `c`: one helper and harness each, so that + // without the check that should fail no input of a harness panics. + + /// A range whose start is strictly inside `c` and whose end is a char boundary. + fn any_range_start_inside_char(len: usize, start: usize, c: char) -> (usize, usize) { + let a = any_inside_char(len, start, c); + let b: usize = kani::any_where(|b: &usize| *b >= start + c.len_utf8() && *b <= len); + kani::cover(b > start + c.len_utf8(), "the end is after the char"); + (a, b) + } + + /// A range whose start is a char boundary and whose end is strictly inside `c`. + fn any_range_end_inside_char(len: usize, start: usize, c: char) -> (usize, usize) { + let b = any_inside_char(len, start, c); + let a: usize = kani::any_where(|a: &usize| *a <= start); + kani::cover(a < start, "the start is before the char"); (a, b) } - /// A range `a..b` with `a <= b` whose end is past the end of a string of length `len`. + /// A range whose two ends are strictly inside `c` (`a <= b`). + fn any_range_both_inside_char(len: usize, start: usize, c: char) -> (usize, usize) { + let a = any_inside_char(len, start, c); + let b: usize = kani::any_where(|b: &usize| *b >= a && *b < start + c.len_utf8()); + kani::cover(a < b, "two different indices inside the char"); + (a, b) + } + + /// A range `a..b` whose end is past the end of a string of length `len`, with any start. fn any_range_past_end(len: usize) -> (usize, usize) { let b = any_past_end(len); - let a: usize = kani::any_where(|a: &usize| *a <= b); + let a: usize = kani::any(); kani::cover(a <= len, "only the end is past the end"); + kani::cover(a > b, "also reversed"); (a, b) } @@ -4507,9 +4535,25 @@ mod verify { #[kani::proof] #[kani::should_panic] - fn check_drain_panics_inside_char() { + fn check_drain_panics_start_inside_char() { + let (mut s, start, c) = with_char_at(); + let (a, b) = any_range_start_inside_char(s.len(), start, c); + drop(s.drain(a..b)); + } + + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics_end_inside_char() { + let (mut s, start, c) = with_char_at(); + let (a, b) = any_range_end_inside_char(s.len(), start, c); + drop(s.drain(a..b)); + } + + #[kani::proof] + #[kani::should_panic] + fn check_drain_panics_both_inside_char() { let (mut s, start, c) = with_char_at(); - let (a, b) = any_range_inside_char(s.len(), start, c); + let (a, b) = any_range_both_inside_char(s.len(), start, c); drop(s.drain(a..b)); } @@ -4527,9 +4571,27 @@ mod verify { #[kani::proof] #[kani::should_panic] #[kani::unwind(1)] - fn check_replace_range_panics_inside_char() { + fn check_replace_range_panics_start_inside_char() { + let (mut s, start, c) = with_char_at(); + let (a, b) = any_range_start_inside_char(s.len(), start, c); + s.replace_range(a..b, ""); + } + + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(1)] + fn check_replace_range_panics_end_inside_char() { + let (mut s, start, c) = with_char_at(); + let (a, b) = any_range_end_inside_char(s.len(), start, c); + s.replace_range(a..b, ""); + } + + #[kani::proof] + #[kani::should_panic] + #[kani::unwind(1)] + fn check_replace_range_panics_both_inside_char() { let (mut s, start, c) = with_char_at(); - let (a, b) = any_range_inside_char(s.len(), start, c); + let (a, b) = any_range_both_inside_char(s.len(), start, c); s.replace_range(a..b, ""); } @@ -4572,12 +4634,13 @@ mod verify { let _ = s.remove(idx); } - /// A reversed range `a..b`, `b < a <= len`, of the all-NUL string `any_string`: both ends are - /// in bounds and char boundaries, so the reversal is the only cause of a panic. + /// A reversed range `a..b`, `b < a`, whose end is in bounds (`b <= len`) of the all-NUL + /// string `any_string`, with any start: the reversal is the only cause of a panic. fn any_reversed_range(len: usize) -> (usize, usize) { - let a: usize = kani::any_where(|a: &usize| *a > 0 && *a <= len); - let b: usize = kani::any_where(|b: &usize| *b < a); + let b: usize = kani::any_where(|b: &usize| *b <= len); + let a: usize = kani::any_where(|a: &usize| *a > b); kani::cover(len > 64 && a < len && b > 0, "reversed range inside a long string"); + kani::cover(a > len, "the start is also past the end"); (a, b) } From 89ab0d47a6413e2cef66f5a094f5f790f3b2c127 Mon Sep 17 00:00:00 2001 From: Talha-Dmr Date: Wed, 14 Oct 2026 06:07:13 +0300 Subject: [PATCH 8/8] Ch10: check the range checks of slice::range directly A should_panic harness accepts any panic. Without the range checks of slice::range, the four *_max harnesses still pass through an arithmetic overflow, and check_replace_range_panics_reversed through later checks. Add three ordinary harnesses that check that slice::try_range rejects ..=usize::MAX, (Excluded(usize::MAX), Unbounded) and every reversed range a..b with b <= len, for every len up to MAX_ALLOC. try_range returns None exactly when slice::range panics, and here an overflow is a failure. --- library/alloc/src/string.rs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 4a65b9a280d7b..580fe361e38ae 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -4696,4 +4696,32 @@ mod verify { kani::cover(s.len() > 64, "long string"); s.replace_range((Bound::Excluded(usize::MAX), Bound::Unbounded), ""); } + + // Why these three exist: `should_panic` accepts any panic. Without the range checks of + // `slice::range`, the four `*_max` harnesses above still pass, through an arithmetic + // overflow, and so does `check_replace_range_panics_reversed`, through later checks. These + // ordinary harnesses check the range checks themselves: `drain` and `replace_range` convert + // their range with `slice::range`, which panics exactly when `slice::try_range` returns + // `None` (both go through `try_into_slice_range`), and here an overflow is a failure. + #[kani::proof] + fn check_range_rejects_end_included_max() { + let len: usize = kani::any_where(|l: &usize| *l <= MAX_ALLOC); + kani::cover(len > 64, "long string"); + assert!(core::slice::try_range(..=usize::MAX, ..len).is_none()); + } + + #[kani::proof] + fn check_range_rejects_start_excluded_max() { + let len: usize = kani::any_where(|l: &usize| *l <= MAX_ALLOC); + kani::cover(len > 64, "long string"); + let r = (Bound::Excluded(usize::MAX), Bound::Unbounded); + assert!(core::slice::try_range(r, ..len).is_none()); + } + + #[kani::proof] + fn check_range_rejects_reversed() { + let len: usize = kani::any_where(|l: &usize| *l <= MAX_ALLOC); + let (a, b) = any_reversed_range(len); + assert!(core::slice::try_range(a..b, ..len).is_none()); + } }