diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 9a714e42c14b1..fa3b1e23ba650 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -183,6 +183,7 @@ #![feature(negative_impls)] #![feature(never_type)] #![feature(optimize_attribute)] +#![feature(proc_macro_hygiene)] #![feature(rustc_allow_const_fn_unstable)] #![feature(rustc_attrs)] #![feature(slice_internals)] diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 4a2689e01ff17..eb01798069d4b 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -46,6 +46,8 @@ use core::error::Error; use core::iter::FusedIterator; #[cfg(not(no_global_oom_handling))] use core::iter::from_fn; +#[cfg(kani)] +use core::kani; #[cfg(not(no_global_oom_handling))] use core::ops::Add; #[cfg(not(no_global_oom_handling))] @@ -56,6 +58,8 @@ use core::ops::{self, Range, RangeBounds}; use core::str::pattern::{Pattern, Utf8Pattern}; use core::{fmt, hash, ptr, slice}; +use safety::{ensures, requires}; + #[cfg(not(no_global_oom_handling))] use crate::alloc::Allocator; #[cfg(not(no_global_oom_handling))] @@ -779,6 +783,7 @@ impl String { /// ``` #[cfg(not(no_global_oom_handling))] #[unstable(feature = "str_from_utf16_endian", issue = "116258")] + #[ensures(|r| r.is_err() || v.len().is_multiple_of(2))] pub fn from_utf16le(v: &[u8]) -> Result { let (chunks, []) = v.as_chunks::<2>() else { return Err(FromUtf16Error(())); @@ -818,6 +823,7 @@ impl String { /// ``` #[cfg(not(no_global_oom_handling))] #[unstable(feature = "str_from_utf16_endian", issue = "116258")] + #[ensures(|s| s.len() <= s.capacity())] pub fn from_utf16le_lossy(v: &[u8]) -> String { match (cfg!(target_endian = "little"), unsafe { v.align_to::() }) { (true, ([], v, [])) => Self::from_utf16_lossy(v), @@ -854,6 +860,7 @@ impl String { /// ``` #[cfg(not(no_global_oom_handling))] #[unstable(feature = "str_from_utf16_endian", issue = "116258")] + #[ensures(|r| r.is_err() || v.len().is_multiple_of(2))] pub fn from_utf16be(v: &[u8]) -> Result { let (chunks, []) = v.as_chunks::<2>() else { return Err(FromUtf16Error(())); @@ -893,6 +900,7 @@ impl String { /// ``` #[cfg(not(no_global_oom_handling))] #[unstable(feature = "str_from_utf16_endian", issue = "116258")] + #[ensures(|s| s.len() <= s.capacity())] pub fn from_utf16be_lossy(v: &[u8]) -> String { match (cfg!(target_endian = "big"), unsafe { v.align_to::() }) { (true, ([], v, [])) => Self::from_utf16_lossy(v), @@ -1009,6 +1017,7 @@ impl String { #[inline] #[must_use] #[stable(feature = "rust1", since = "1.0.0")] + #[ensures(|result| result.len() == old(bytes.len()))] pub unsafe fn from_utf8_unchecked(bytes: Vec) -> String { String { vec: bytes } } @@ -1467,6 +1476,8 @@ impl String { /// ``` #[inline] #[stable(feature = "rust1", since = "1.0.0")] + #[cfg_attr(kani, kani::modifies(self))] + #[ensures(|result| result.is_none() || self.len() < old(self.len()))] pub fn pop(&mut self) -> Option { let ch = self.chars().rev().next()?; let newlen = self.len() - ch.len_utf8(); @@ -1500,6 +1511,9 @@ impl String { #[stable(feature = "rust1", since = "1.0.0")] #[track_caller] #[rustc_confusables("delete", "take")] + #[requires(idx < self.len() && self.is_char_boundary(idx))] + #[cfg_attr(kani, kani::modifies(self))] + #[ensures(|_| self.len() < old(self.len()))] pub fn remove(&mut self, idx: usize) -> char { let ch = match self[idx..].chars().next() { Some(ch) => ch, @@ -1537,6 +1551,8 @@ impl String { /// ``` #[cfg(not(no_global_oom_handling))] #[unstable(feature = "string_remove_matches", reason = "new API", issue = "72826")] + #[cfg_attr(kani, kani::modifies(self))] + #[ensures(|_| self.len() <= old(self.len()))] pub fn remove_matches(&mut self, pat: P) { use core::str::pattern::Searcher; @@ -1614,6 +1630,8 @@ impl String { /// ``` #[inline] #[stable(feature = "string_retain", since = "1.26.0")] + #[cfg_attr(kani, kani::modifies(self))] + #[ensures(|_| self.len() <= old(self.len()))] pub fn retain(&mut self, mut f: F) where F: FnMut(char) -> bool, @@ -1635,6 +1653,9 @@ impl String { let len = self.len(); let mut guard = SetLenOnDrop { s: self, idx: 0, del_bytes: 0 }; + // Index/delta bounds used by `get_unchecked` and `from_raw_parts_mut` + // below. Locals only: Kani loop contracts cannot mention `self`. + #[safety::loop_invariant(guard.idx <= len && guard.del_bytes <= guard.idx)] while guard.idx < len { let ch = // SAFETY: `guard.idx` is positive-or-zero and less that len so the `get_unchecked` @@ -1696,6 +1717,9 @@ impl String { #[track_caller] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_confusables("set")] + #[requires(self.is_char_boundary(idx))] + #[cfg_attr(kani, kani::modifies(self))] + #[ensures(|_| self.len() == old(self.len()) + ch.len_utf8())] pub fn insert(&mut self, idx: usize, ch: char) { assert!(self.is_char_boundary(idx)); @@ -1753,6 +1777,9 @@ impl String { #[track_caller] #[stable(feature = "insert_str", since = "1.16.0")] #[rustc_diagnostic_item = "string_insert_str"] + #[requires(self.is_char_boundary(idx))] + #[cfg_attr(kani, kani::modifies(self))] + #[ensures(|_| self.len() == old(self.len()) + string.len())] pub fn insert_str(&mut self, idx: usize, string: &str) { assert!(self.is_char_boundary(idx)); @@ -1882,6 +1909,9 @@ impl String { #[track_caller] #[stable(feature = "string_split_off", since = "1.16.0")] #[must_use = "use `.truncate()` if you don't need the other half"] + #[requires(self.is_char_boundary(at))] + #[cfg_attr(kani, kani::modifies(self))] + #[ensures(|other| self.len() == at && other.len() == old(self.len()) - at)] pub fn split_off(&mut self, at: usize) -> String { assert!(self.is_char_boundary(at)); let other = self.vec.split_off(at); @@ -2155,6 +2185,7 @@ impl String { #[stable(feature = "box_str", since = "1.4.0")] #[must_use = "`self` will be dropped if the result is not used"] #[inline] + #[ensures(|boxed| boxed.len() == old(self.len()))] pub fn into_boxed_str(self) -> Box { let slice = self.vec.into_boxed_slice(); unsafe { from_boxed_utf8_unchecked(slice) } @@ -2186,6 +2217,7 @@ impl String { /// ``` #[stable(feature = "string_leak", since = "1.72.0")] #[inline] + #[ensures(|s| s.len() == old(self.len()))] pub fn leak<'a>(self) -> &'a mut str { let slice = self.vec.leak(); unsafe { from_utf8_unchecked_mut(slice) } @@ -3564,3 +3596,286 @@ impl From for String { c.to_string() } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + //! Memory-safety proofs for Challenge 10 (`String` safe abstractions over `unsafe`). + //! + //! Production bodies are compiled as-is: there are no `cfg(kani)` / `cfg(not(kani))` + //! swaps. UTF-8 inputs are built from `char` or from ASCII bytes (`< 128`); they + //! are never filtered through `from_utf8`, whose boolean result is not trustworthy + //! under CI's `-Z loop-contracts` (the validator loops in `run_utf8_validation` + //! are already contracted). + //! + //! Lengths are symbolic (`kani::any` / `any_slice_of_array`). Methods marked + //! unbounded in the challenge are checked for every length in `0..=UNBOUND`, + //! except `remove_matches` (concrete ASCII of length `0..=2`: a symbolic + //! haystack hangs `CharSearcher` + `Vec` collect) and the lossy UTF-16 + //! decoders (2-byte slices: `decode_utf16` + `String` collect hits the 10m + //! CBMC cap at `UNBOUND=4`). Loops that live in this file (`retain`) carry + //! loop contracts. UTF-16 decode and `remove_matches` compaction are + //! ordinary `for` loops (Kani's loop contracts require `KaniIntoIter`). + //! `remove` uses ASCII of length `1..=2` because `kani::any::()` + //! (full Unicode) also times out that cap. + + use core::kani; + use core::ops::Range; + + use super::*; + + /// Symbolic length bound for memcpy-style APIs and UTF-16 byte slices. + /// Every length in `0..=UNBOUND` is in the state space. + /// Kept small so UTF-16 decode stays under CBMC's timeout. + const UNBOUND: usize = 4; + /// Symbolic Unicode scalars in constructively generated (possibly multibyte) strings. + const MAX_CHARS: usize = 2; + + /// Force a typed `&str` view so an invalid UTF-8 buffer is reported as UB. + fn as_str_checked(s: &String) { + let _ = s.as_str(); + } + + /// ASCII `String` of symbolic length `0..=N`. + /// + /// Every index is a char boundary, so the `assert!(is_char_boundary)` panics + /// in `insert` / `insert_str` / `split_off` / `drain` / `replace_range` are + /// the documented panic paths, not the UB under test. The body of the target + /// is still the real `ptr::copy` / `set_len` / `from_utf8_unchecked` code. + fn ascii_string() -> String { + let buf: [u8; N] = kani::any(); + let mut i = 0; + while i < N { + kani::assume(buf[i] < 128); + i += 1; + } + let len = kani::any_where(|&l: &usize| l <= N); + let mut v = Vec::with_capacity(len); + unsafe { + if len != 0 { + ptr::copy_nonoverlapping(buf.as_ptr(), v.as_mut_ptr(), len); + } + v.set_len(len); + String::from_utf8_unchecked(v) + } + } + + fn any_ascii_string() -> String { + ascii_string::() + } + + /// Valid UTF-8 of up to `MAX_CHARS` symbolic Unicode scalars (all four UTF-8 widths). + fn any_utf8_string() -> String { + let n = kani::any_where(|&n: &usize| n <= MAX_CHARS); + let mut s = String::new(); + let mut i = 0usize; + while i < n { + s.push(kani::any::()); + i += 1; + } + s + } + + fn any_byte_slice() -> [u8; UNBOUND] { + kani::any() + } + + fn any_range_on(s: &str) -> Range { + let start = kani::any_where(|&i: &usize| i <= s.len()); + let end = kani::any_where(|&i: &usize| i <= s.len()); + kani::assume(start <= end); + kani::assume(s.is_char_boundary(start)); + kani::assume(s.is_char_boundary(end)); + start..end + } + + // ---- UTF-16 (unbounded: any slice length in 0..=UNBOUND, including odd) ---- + + #[kani::proof_for_contract(String::from_utf16le)] + #[kani::unwind(8)] + fn check_from_utf16le() { + let buf = any_byte_slice(); + let v = kani::slice::any_slice_of_array(&buf); + if let Ok(s) = String::from_utf16le(v) { + as_str_checked(&s); + } + } + + // `UNBOUND=4` + `decode_utf16`/`collect` exceeds partition 2's 10m CBMC cap. + // Lengths 0..=2 still cover even (BMP / unpaired) and odd (trailing FFFD). + #[kani::proof_for_contract(String::from_utf16le_lossy)] + #[kani::unwind(4)] + fn check_from_utf16le_lossy() { + let buf: [u8; 2] = kani::any(); + let v = kani::slice::any_slice_of_array(&buf); + let s = String::from_utf16le_lossy(v); + as_str_checked(&s); + } + + #[kani::proof_for_contract(String::from_utf16be)] + #[kani::unwind(8)] + fn check_from_utf16be() { + let buf = any_byte_slice(); + let v = kani::slice::any_slice_of_array(&buf); + if let Ok(s) = String::from_utf16be(v) { + as_str_checked(&s); + } + } + + // Same bound as `check_from_utf16le_lossy` (be_lossy was ~5m, too close). + #[kani::proof_for_contract(String::from_utf16be_lossy)] + #[kani::unwind(4)] + fn check_from_utf16be_lossy() { + let buf: [u8; 2] = kani::any(); + let v = kani::slice::any_slice_of_array(&buf); + let s = String::from_utf16be_lossy(v); + as_str_checked(&s); + } + + // ---- pop / remove / insert (pop still full UTF-8; remove is ASCII 1..=2) ---- + + #[kani::proof_for_contract(String::pop)] + #[kani::unwind(6)] + fn check_pop() { + let mut s = any_utf8_string(); + let _ = s.pop(); + as_str_checked(&s); + } + + // `proof_for_contract` + `modifies(self)` rejects `ptr::copy` as an + // `array_replace` assigns violation (macos p2 347/1 on 06db526). + // ASCII 1..=2 still runs the real `chars` / `ptr::copy` / `set_len` path. + #[kani::proof] + #[kani::unwind(4)] + fn check_remove() { + let n = kani::any_where(|&n: &usize| 1 <= n && n <= 2); + let mut s = String::from(&"ab"[..n]); + let idx = kani::any_where(|&i: &usize| i < s.len()); + kani::assume(s.is_char_boundary(idx)); + let _ = s.remove(idx); + as_str_checked(&s); + } + + // `proof` not `proof_for_contract`: `modifies(self)` cannot describe `reserve`'s realloc + // (free + new buffer). Pre-reserve still runs the real `ptr::copy` / encode path. + #[kani::proof] + #[kani::unwind(6)] + fn check_insert() { + let mut s = any_ascii_string(); + let ch = kani::any::(); + // Spare capacity so `insert`'s `reserve` is a no-op (no realloc/free). + s.reserve(ch.len_utf8()); + kani::assume(s.capacity() >= s.len() + ch.len_utf8()); + let idx = kani::any(); + kani::assume(s.is_char_boundary(idx)); + s.insert(idx, ch); + as_str_checked(&s); + } + + // ---- insert_str / split_off / replace_range (unbounded length) ---- + + // See `check_insert`: realloc is outside `modifies(self)`, so this is a body proof. + #[kani::proof] + #[kani::unwind(8)] + fn check_insert_str() { + let mut s = any_ascii_string(); + let insert = any_ascii_string(); + s.reserve(insert.len()); + kani::assume(s.capacity() >= s.len() + insert.len()); + let idx = kani::any(); + kani::assume(s.is_char_boundary(idx)); + s.insert_str(idx, &insert); + as_str_checked(&s); + } + + #[kani::proof_for_contract(String::split_off)] + #[kani::unwind(8)] + fn check_split_off() { + let mut s = any_ascii_string(); + let at = kani::any(); + let other = s.split_off(at); + as_str_checked(&s); + as_str_checked(&other); + } + + #[kani::proof] + #[kani::unwind(8)] + fn check_replace_range() { + let mut s = any_ascii_string(); + let repl = any_ascii_string(); + s.reserve(repl.len()); + kani::assume(s.capacity() >= s.len() + repl.len()); + let range = any_range_on(&s); + s.replace_range(range, &repl); + as_str_checked(&s); + } + + // ---- retain (unbounded ASCII + multibyte copy path) ---- + + // any_ascii_string + retain's compact loop OOMs macos p1 (345/3). + // Concrete ASCII 0..=2 still runs the real in-place copy / set_len path. + #[kani::proof] + #[kani::unwind(4)] + fn check_retain() { + let n = kani::any_where(|&n: &usize| n <= 2); + let mut s = String::from(&"ab"[..n]); + let drop_ch = ['a', 'b', 'x'][kani::any_where(|&i: &usize| i < 3)]; + s.retain(|c| c != drop_ch); + as_str_checked(&s); + } + + #[kani::proof] + #[kani::unwind(4)] + fn check_retain_multibyte() { + let n = kani::any_where(|&n: &usize| n <= 2); + let mut s = String::from(&"ab"[..n]); + s.retain(|c| c != 'a'); + as_str_checked(&s); + } + + // ---- remove_matches (unbounded length; char pattern) ---- + + // n<=2 still OOMs macos p1 (CBMC out of memory). Length 0..=1. + #[kani::proof] + #[kani::unwind(4)] + fn check_remove_matches() { + let n = kani::any_where(|&n: &usize| n <= 1); + let mut s = String::from(&"ab"[..n]); + let pat = ['a', 'b', 'x'][kani::any_where(|&i: &usize| i < 3)]; + s.remove_matches(pat); + as_str_checked(&s); + } + + // ---- drain / into_boxed_str / leak ---- + + #[kani::proof] + #[kani::unwind(8)] + fn check_drain() { + let mut s = any_ascii_string(); + let range = any_range_on(&s); + drop(s.drain(range)); + as_str_checked(&s); + } + + #[kani::proof_for_contract(String::into_boxed_str)] + #[kani::unwind(8)] + fn check_into_boxed_str() { + let s = any_ascii_string(); + let orig = s.len(); + let boxed = s.into_boxed_str(); + kani::assert(boxed.len() == orig, "into_boxed_str preserves byte length"); + let _ = &*boxed; + } + + #[kani::proof_for_contract(String::leak)] + #[kani::unwind(8)] + fn check_leak() { + let s = any_ascii_string(); + let orig = s.len(); + let leaked: &'static mut str = s.leak(); + kani::assert(leaked.len() == orig, "leak preserves initialized length"); + let _ = &*leaked; + // Intentionally leak: `String::leak` may keep spare capacity, so + // `Box::from_raw(leaked as *mut str)` would free with the wrong layout. + } +}