Skip to content

Challenge 10: Verify memory safety of String functions #571

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Samuelsills wants to merge 2 commits into
base: main
Choose a base branch
from
+126 −0
Open

Challenge 10: Verify memory safety of String functions #571

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b5eb2c2
Challenge 10: Verify memory safety of String functions
Samuelsills Mar 26, 2026
cef17fd
Fix formatting: add blank line between use groups
Samuelsills Mar 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
126 changes: 126 additions & 0 deletions library/alloc/src/string.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3488,3 +3488,129 @@ impl From<char> for String {
c.to_string()
}
}

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use core::kani;

use crate::string::String;

#[kani::proof]
fn verify_pop() {
let mut s = String::from("hello");
let c = s.pop();
assert!(c == Some('o'));
assert!(s.len() == 4);
}

#[kani::proof]
fn verify_remove() {
let mut s = String::from("hello");
let c = s.remove(0);
assert!(c == 'h');
assert!(s.len() == 4);
}

#[kani::proof]
fn verify_insert() {
let mut s = String::from("ello");
s.insert(0, 'h');
assert!(s.len() == 5);
Comment on lines +3501 to +3519
Copy link

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

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

The harnesses use fixed, hard-coded inputs (e.g., "hello", constant indices/ranges), so Kani only explores a single execution path per method. That doesn’t meaningfully verify memory safety across the input space (e.g., varying lengths, capacities, UTF-8 boundaries, and index/range preconditions). Consider generating nondeterministic inputs with kani::any/kani::Arbitrary and constraining them with kani::assume/any_where (e.g., idx < s.len() and s.is_char_boundary(idx)), so the proof actually covers the cases these APIs must handle.

Suggested change
let mut s = String::from("hello");
let c = s.pop();
assert!(c == Some('o'));
assert!(s.len() == 4);
}
#[kani::proof]
fn verify_remove() {
let mut s = String::from("hello");
let c = s.remove(0);
assert!(c == 'h');
assert!(s.len() == 4);
}
#[kani::proof]
fn verify_insert() {
let mut s = String::from("ello");
s.insert(0, 'h');
assert!(s.len() == 5);
// Nondeterministic string to explore both empty and non-empty cases.
let mut s: String = kani::any();
let old_len = s.len();
let c = s.pop();
match c {
Some(ch) => {
// Removing a character decreases the length by its UTF-8 byte width.
assert!(s.len() == old_len - ch.len_utf8());
}
None => {
// Popping from an empty string leaves the length unchanged.
assert!(s.len() == old_len);
}
}
}
#[kani::proof]
fn verify_remove() {
// Nondeterministic string and index, constrained to remove a valid char.
let mut s: String = kani::any();
let idx: usize = kani::any();
// `remove` requires that `idx` is in-bounds and a char boundary.
kani::assume(idx < s.len());
kani::assume(s.is_char_boundary(idx));
let old_len = s.len();
let c = s.remove(idx);
// Removing a character decreases the length by its UTF-8 byte width.
assert!(s.len() == old_len - c.len_utf8());
}
#[kani::proof]
fn verify_insert() {
// Nondeterministic string, insertion index, and character.
let mut s: String = kani::any();
let idx: usize = kani::any();
let ch: char = kani::any();
// `insert` requires that `idx` is at a char boundary and within bounds.
kani::assume(idx <= s.len());
kani::assume(s.is_char_boundary(idx));
let old_len = s.len();
s.insert(idx, ch);
// Inserting a character increases the length by its UTF-8 byte width.
assert!(s.len() == old_len + ch.len_utf8());

Copilot uses AI. Check for mistakes.
}

#[kani::proof]
fn verify_insert_str() {
let mut s = String::from("world");
s.insert_str(0, "hello ");
assert!(s.len() == 11);
}

#[kani::proof]
fn verify_split_off() {
let mut s = String::from("hello");
let s2 = s.split_off(2);
assert!(s.len() == 2);
assert!(s2.len() == 3);
}

#[kani::proof]
fn verify_drain() {
let mut s = String::from("hello");
let d: String = s.drain(1..3).collect();
assert!(d.len() == 2);
assert!(s.len() == 3);
}

#[kani::proof]
fn verify_replace_range() {
let mut s = String::from("hello");
s.replace_range(1..3, "a");
assert!(s.len() == 4);
}

#[kani::proof]
fn verify_into_boxed_str() {
let s = String::from("hello");
let b: crate::boxed::Box<str> = s.into_boxed_str();
assert!(b.len() == 5);
}

#[kani::proof]
fn verify_leak() {
let s = String::from("hello");
let leaked: &'static mut str = s.leak();
assert!(leaked.len() == 5);
unsafe {
drop(crate::boxed::Box::from_raw(leaked as *mut str));
}
Comment on lines +3564 to +3566
Copy link

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

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

String::leak explicitly may retain unused capacity (allocation size can be larger than leaked.len()). Reconstructing a Box<str> from the leaked &mut str and dropping it can deallocate with the wrong layout (based on len rather than the original capacity), which is undefined behavior. For this proof harness, avoid trying to free the leaked allocation; just let it leak (or use a different cleanup strategy that preserves the original allocation layout).

Suggested change
unsafe {
drop(crate::boxed::Box::from_raw(leaked as *mut str));
}

Copilot uses AI. Check for mistakes.
}

#[kani::proof]
#[kani::unwind(3)]
fn verify_from_utf16le() {
let bytes: [u8; 4] = [0x68, 0x00, 0x69, 0x00];
let result = String::from_utf16le(&bytes);
assert!(result.is_ok());
}

#[kani::proof]
#[kani::unwind(3)]
fn verify_from_utf16le_lossy() {
let bytes: [u8; 4] = [0x68, 0x00, 0x69, 0x00];
let s = String::from_utf16le_lossy(&bytes);
assert!(s.len() >= 2);
}

#[kani::proof]
#[kani::unwind(3)]
fn verify_from_utf16be() {
let bytes: [u8; 4] = [0x00, 0x68, 0x00, 0x69];
let result = String::from_utf16be(&bytes);
assert!(result.is_ok());
}

#[kani::proof]
#[kani::unwind(3)]
fn verify_from_utf16be_lossy() {
let bytes: [u8; 4] = [0x00, 0x68, 0x00, 0x69];
let s = String::from_utf16be_lossy(&bytes);
assert!(s.len() >= 2);
}

#[kani::proof]
#[kani::unwind(7)]
fn verify_retain() {
let mut s = String::from("hello");
s.retain(|c| c != 'l');
assert!(s.len() == 3);
}

#[kani::proof]
#[kani::unwind(7)]
fn verify_remove_matches() {
let mut s = String::from("abcabc");
s.remove_matches('a');
assert!(s.len() == 4);
}
}
Loading