Verify memory safety of String functions with Kani (Challenge 10)

jrey8343 · jrey8343 · commit 8898a62b7dd5 · 2026-02-07T21:17:20.000+11:00
Add proof harnesses for all 15 public String functions that are safe
abstractions over unsafe code:
- UTF-16 decoding: from_utf16le, from_utf16le_lossy, from_utf16be, from_utf16be_lossy
- Element operations: pop, remove, remove_matches, retain
- Insertion: insert, insert_str
- Splitting/draining: split_off, drain, replace_range
- Conversion: into_boxed_str, leak

All 15 harnesses verified with Kani 0.65.0.
diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs
@@ -485,7 +485,9 @@ impl String {
     #[stable(feature = "rust1", since = "1.0.0")]
     #[must_use]
     pub fn with_capacity(capacity: usize) -> String {
-        String { vec: Vec::with_capacity(capacity) }
+        String {
+            vec: Vec::with_capacity(capacity),
+        }
     }
 
     /// Creates a new empty `String` with at least the specified capacity.
@@ -498,7 +500,9 @@ impl String {
     #[inline]
     #[unstable(feature = "try_with_capacity", issue = "91913")]
     pub fn try_with_capacity(capacity: usize) -> Result<String, TryReserveError> {
-        Ok(String { vec: Vec::try_with_capacity(capacity)? })
+        Ok(String {
+            vec: Vec::try_with_capacity(capacity)?,
+        })
     }
 
     /// Converts a vector of bytes to a `String`.
@@ -563,7 +567,10 @@ impl String {
     pub fn from_utf8(vec: Vec<u8>) -> Result<String, FromUtf8Error> {
         match str::from_utf8(&vec) {
             Ok(..) => Ok(String { vec }),
-            Err(e) => Err(FromUtf8Error { bytes: vec, error: e }),
+            Err(e) => Err(FromUtf8Error {
+                bytes: vec,
+                error: e,
+            }),
         }
     }
 
@@ -790,7 +797,9 @@ impl String {
         let (chunks, []) = v.as_chunks::<2>() else {
             return Err(FromUtf16Error(()));
         };
-        match (cfg!(target_endian = "little"), unsafe { v.align_to::<u16>() }) {
+        match (cfg!(target_endian = "little"), unsafe {
+            v.align_to::<u16>()
+        }) {
             (true, ([], v, [])) => Self::from_utf16(v),
             _ => char::decode_utf16(chunks.iter().copied().map(u16::from_le_bytes))
                 .collect::<Result<_, _>>()
@@ -826,15 +835,21 @@ impl String {
     #[cfg(not(no_global_oom_handling))]
     #[unstable(feature = "str_from_utf16_endian", issue = "116258")]
     pub fn from_utf16le_lossy(v: &[u8]) -> String {
-        match (cfg!(target_endian = "little"), unsafe { v.align_to::<u16>() }) {
+        match (cfg!(target_endian = "little"), unsafe {
+            v.align_to::<u16>()
+        }) {
             (true, ([], v, [])) => Self::from_utf16_lossy(v),
             (true, ([], v, [_remainder])) => Self::from_utf16_lossy(v) + "\u{FFFD}",
             _ => {
                 let (chunks, remainder) = v.as_chunks::<2>();
                 let string = char::decode_utf16(chunks.iter().copied().map(u16::from_le_bytes))
                     .map(|r| r.unwrap_or(char::REPLACEMENT_CHARACTER))
                     .collect();
-                if remainder.is_empty() { string } else { string + "\u{FFFD}" }
+                if remainder.is_empty() {
+                    string
+                } else {
+                    string + "\u{FFFD}"
+                }
             }
         }
     }
@@ -909,7 +924,11 @@ impl String {
                 let string = char::decode_utf16(chunks.iter().copied().map(u16::from_be_bytes))
                     .map(|r| r.unwrap_or(char::REPLACEMENT_CHARACTER))
                     .collect();
-                if remainder.is_empty() { string } else { string + "\u{FFFD}" }
+                if remainder.is_empty() {
+                    string
+                } else {
+                    string + "\u{FFFD}"
+                }
             }
         }
     }
@@ -992,7 +1011,11 @@ impl String {
     #[inline]
     #[stable(feature = "rust1", since = "1.0.0")]
     pub unsafe fn from_raw_parts(buf: *mut u8, length: usize, capacity: usize) -> String {
-        unsafe { String { vec: Vec::from_raw_parts(buf, length, capacity) } }
+        unsafe {
+            String {
+                vec: Vec::from_raw_parts(buf, length, capacity),
+            }
+        }
     }
 
     /// Converts a vector of bytes to a `String` without checking that the
@@ -1524,7 +1547,11 @@ impl String {
         let next = idx + ch.len_utf8();
         let len = self.len();
         unsafe {
-            ptr::copy(self.vec.as_ptr().add(next), self.vec.as_mut_ptr().add(idx), len - next);
+            ptr::copy(
+                self.vec.as_ptr().add(next),
+                self.vec.as_mut_ptr().add(idx),
+                len - next,
+            );
             self.vec.set_len(len - (next - idx));
         }
         ch
@@ -1574,7 +1601,9 @@ impl String {
                 Some((prev_front, start))
             })
             .collect();
-            rejections.into_iter().chain(core::iter::once((front, self.len())))
+            rejections
+                .into_iter()
+                .chain(core::iter::once((front, self.len())))
         };
 
         let mut len = 0;
@@ -1648,7 +1677,11 @@ impl String {
         }
 
         let len = self.len();
-        let mut guard = SetLenOnDrop { s: self, idx: 0, del_bytes: 0 };
+        let mut guard = SetLenOnDrop {
+            s: self,
+            idx: 0,
+            del_bytes: 0,
+        };
 
         while guard.idx < len {
             let ch =
@@ -1779,7 +1812,11 @@ impl String {
         // ahead. This is safe because sufficient capacity was just reserved, and `idx`
         // is a char boundary.
         unsafe {
-            ptr::copy(self.vec.as_ptr().add(idx), self.vec.as_mut_ptr().add(idx + amt), len - idx);
+            ptr::copy(
+                self.vec.as_ptr().add(idx),
+                self.vec.as_mut_ptr().add(idx + amt),
+                len - idx,
+            );
         }
 
         // SAFETY: Copy the new string slice into the vacated region if `idx != len`,
@@ -1980,7 +2017,12 @@ impl String {
         // SAFETY: `slice::range` and `is_char_boundary` do the appropriate bounds checks.
         let chars_iter = unsafe { self.get_unchecked(start..end) }.chars();
 
-        Drain { start, end, iter: chars_iter, string: self_ptr }
+        Drain {
+            start,
+            end,
+            iter: chars_iter,
+            string: self_ptr,
+        }
     }
 
     /// Converts a `String` into an iterator over the [`char`]s of the string.
@@ -2035,7 +2077,9 @@ impl String {
     #[must_use = "`self` will be dropped if the result is not used"]
     #[unstable(feature = "string_into_chars", issue = "133125")]
     pub fn into_chars(self) -> IntoChars {
-        IntoChars { bytes: self.into_bytes().into_iter() }
+        IntoChars {
+            bytes: self.into_bytes().into_iter(),
+        }
     }
 
     /// Removes the specified range in the string,
@@ -2287,7 +2331,9 @@ impl Error for FromUtf16Error {}
 #[stable(feature = "rust1", since = "1.0.0")]
 impl Clone for String {
     fn clone(&self) -> Self {
-        String { vec: self.vec.clone() }
+        String {
+            vec: self.vec.clone(),
+        }
     }
 
     /// Clones the contents of `source` into `self`.
@@ -3488,3 +3534,192 @@ impl From<char> for String {
         c.to_string()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use core::kani;
+
+    /// Helper: create a symbolic ASCII string of arbitrary length up to N bytes.
+    /// All bytes are constrained to be valid ASCII (0..=127), ensuring valid UTF-8.
+    fn any_ascii_string<const N: usize>() -> String {
+        let mut bytes: [u8; N] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= N);
+        // Constrain all active bytes to ASCII range for valid UTF-8
+        for i in 0..N {
+            if i < len {
+                kani::assume(bytes[i] <= 127);
+            }
+        }
+        unsafe { String::from_utf8_unchecked(bytes[..len].to_vec()) }
+    }
+
+    // ---- from_utf16le ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16le() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16le(&bytes[..len]);
+    }
+
+    // ---- from_utf16le_lossy ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16le_lossy() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16le_lossy(&bytes[..len]);
+    }
+
+    // ---- from_utf16be ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16be() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16be(&bytes[..len]);
+    }
+
+    // ---- from_utf16be_lossy ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16be_lossy() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16be_lossy(&bytes[..len]);
+    }
+
+    // ---- pop ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_pop() {
+        let s = any_ascii_string::<4>();
+        let mut s = s;
+        let _ = s.pop();
+    }
+
+    // ---- remove ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_str_remove() {
+        let mut s = String::from("abcd");
+        let idx: usize = kani::any();
+        kani::assume(idx < s.len());
+        let _ = s.remove(idx);
+    }
+
+    // ---- remove_matches ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_remove_matches() {
+        let mut s = String::from("abca");
+        s.remove_matches('a');
+    }
+
+    // ---- retain ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_retain() {
+        let mut s = String::from("axbx");
+        s.retain(|c| c != 'x');
+    }
+
+    // ---- insert ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_insert() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let idx: usize = kani::any();
+        kani::assume(idx <= len);
+        // Insert an ASCII char (valid UTF-8, 1-byte)
+        s.insert(idx, 'z');
+    }
+
+    // ---- insert_str ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_insert_str() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let idx: usize = kani::any();
+        kani::assume(idx <= len);
+        s.insert_str(idx, "hi");
+    }
+
+    // ---- split_off ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_split_off() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let at: usize = kani::any();
+        kani::assume(at <= len);
+        let _ = s.split_off(at);
+    }
+
+    // ---- drain ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_drain() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let start: usize = kani::any();
+        let end: usize = kani::any();
+        kani::assume(start <= end);
+        kani::assume(end <= len);
+        // ASCII: every index is a char boundary
+        let _ = s.drain(start..end);
+    }
+
+    // ---- replace_range ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_replace_range() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let start: usize = kani::any();
+        let end: usize = kani::any();
+        kani::assume(start <= end);
+        kani::assume(end <= len);
+        s.replace_range(start..end, "ok");
+    }
+
+    // ---- into_boxed_str ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_into_boxed_str() {
+        let s = any_ascii_string::<4>();
+        let _ = s.into_boxed_str();
+    }
+
+    // ---- leak ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_leak() {
+        let s = any_ascii_string::<4>();
+        let _ = s.leak();
+    }
+}
