From 10cfee891b1c363cc092e87111ce3b882574a549 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Sun, 8 Feb 2026 13:17:20 +1100 Subject: [PATCH 1/6] Verify safety of CStr CloneToUninit and Index (Challenge 13) Add the final 2 verification harnesses to complete Challenge 13: - check_clone_to_uninit: Verifies the unsafe CloneToUninit impl for CStr correctly copies all bytes (including NUL terminator) and produces a valid CStr at the destination. Includes safety contract on clone_to_uninit requiring non-null dest pointer. - check_index_from: Verifies ops::Index> for CStr produces a valid CStr that maintains the safety invariant and matches the expected tail of the original bytes. Both harnesses are bounded (MAX_SIZE=16/32) with appropriate unwind limits and verify the CStr is_safe() invariant holds. --- library/core/src/clone.rs | 4 +++ library/core/src/ffi/c_str.rs | 55 +++++++++++++++++++++++++++++++++++ 2 files changed, 59 insertions(+) diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs index 7f2a40f753fa6..39f7b1b3b09f5 100644 --- a/library/core/src/clone.rs +++ b/library/core/src/clone.rs @@ -37,6 +37,9 @@ #![stable(feature = "rust1", since = "1.0.0")] use crate::marker::{Destruct, PointeeSized}; +#[cfg(kani)] +use crate::kani; +use safety::requires; mod uninit; @@ -544,6 +547,7 @@ unsafe impl CloneToUninit for str { #[unstable(feature = "clone_to_uninit", issue = "126799")] unsafe impl CloneToUninit for crate::ffi::CStr { #[cfg_attr(debug_assertions, track_caller)] + #[requires(!dest.is_null())] unsafe fn clone_to_uninit(&self, dest: *mut u8) { // SAFETY: For now, CStr is just a #[repr(trasnsparent)] [c_char] with some invariants. // And we can cast [c_char] to [u8] on all supported platforms (see: to_bytes_with_nul). diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 715d0d8db4025..7a09f9b8beb52 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -875,6 +875,7 @@ impl FusedIterator for Bytes<'_> {} #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; + use crate::clone::CloneToUninit; // Helper function fn arbitrary_cstr(slice: &[u8]) -> &CStr { @@ -1096,4 +1097,58 @@ mod verify { assert_eq!(expected_is_empty, c_str.is_empty()); assert!(c_str.is_safe()); } + + // ops::Index> for CStr + #[kani::proof] + #[kani::unwind(33)] + fn check_index_from() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); + + let bytes_with_nul = c_str.to_bytes_with_nul(); + let idx: usize = kani::any(); + kani::assume(idx < bytes_with_nul.len()); + + let indexed = &c_str[idx..]; + assert!(indexed.is_safe()); + // The indexed result should correspond to the tail of the original bytes + assert_eq!(indexed.to_bytes_with_nul(), &bytes_with_nul[idx..]); + } + + // CloneToUninit for CStr + #[kani::proof] + #[kani::unwind(17)] + fn check_clone_to_uninit() { + const MAX_SIZE: usize = 16; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); + + let bytes_with_nul = c_str.to_bytes_with_nul(); + let len = bytes_with_nul.len(); + + // Allocate destination buffer + let mut buf = [core::mem::MaybeUninit::::uninit(); MAX_SIZE]; + let dest = buf.as_mut_ptr() as *mut u8; + + // Call the unsafe clone_to_uninit + unsafe { + c_str.clone_to_uninit(dest); + } + + // Verify the cloned bytes match the original + unsafe { + for i in 0..len { + assert_eq!(*dest.add(i), bytes_with_nul[i]); + } + } + + // Verify we can reconstruct a valid CStr from the cloned data + let cloned_slice = unsafe { core::slice::from_raw_parts(dest, len) }; + let cloned_cstr = CStr::from_bytes_with_nul(cloned_slice); + assert!(cloned_cstr.is_ok()); + assert!(cloned_cstr.unwrap().is_safe()); + } } From a0b5f8f0446ba84117f46e4997d16f36b3fd8039 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Wed, 11 Feb 2026 12:16:59 +1100 Subject: [PATCH 2/6] Apply upstream rustfmt formatting via check_rustc.sh --bless --- library/core/src/clone.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs index 39f7b1b3b09f5..a2bd21ef32844 100644 --- a/library/core/src/clone.rs +++ b/library/core/src/clone.rs @@ -36,10 +36,11 @@ #![stable(feature = "rust1", since = "1.0.0")] -use crate::marker::{Destruct, PointeeSized}; +use safety::requires; + #[cfg(kani)] use crate::kani; -use safety::requires; +use crate::marker::{Destruct, PointeeSized}; mod uninit; From f0e50490eab1553f02d4e8afeab49f90afb74c89 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Sun, 22 Feb 2026 07:11:17 +1100 Subject: [PATCH 3/6] Fix check_clone_to_uninit CBMC timeout: reduce size and remove byte loop The harness was timing out (10 min CBMC limit) due to expensive symbolic pointer arithmetic in clone_to_uninit combined with a symbolic-length verification loop. Fix: reduce MAX_SIZE from 16 to 8 bytes (sufficient to cover empty, single-char, and multi-char C strings) and remove the byte-by-byte verification loop (the CStr reconstruction check still validates the safety invariant). --- library/core/src/ffi/c_str.rs | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 7a09f9b8beb52..ad620412244d5 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1118,34 +1118,29 @@ mod verify { } // CloneToUninit for CStr + // MAX_SIZE is kept small to avoid CBMC timeout: the symbolic pointer + // arithmetic in clone_to_uninit is expensive; 8 bytes is sufficient to + // cover empty, single-char, and multi-char C strings. #[kani::proof] - #[kani::unwind(17)] + #[kani::unwind(9)] fn check_clone_to_uninit() { - const MAX_SIZE: usize = 16; + const MAX_SIZE: usize = 8; let string: [u8; MAX_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array(&string); let c_str = arbitrary_cstr(slice); - let bytes_with_nul = c_str.to_bytes_with_nul(); - let len = bytes_with_nul.len(); + let len = c_str.to_bytes_with_nul().len(); - // Allocate destination buffer + // Allocate destination buffer (len <= MAX_SIZE since slice.len() <= MAX_SIZE) let mut buf = [core::mem::MaybeUninit::::uninit(); MAX_SIZE]; let dest = buf.as_mut_ptr() as *mut u8; - // Call the unsafe clone_to_uninit + // Safety: dest is non-null (stack allocation), valid for len writes unsafe { c_str.clone_to_uninit(dest); } - // Verify the cloned bytes match the original - unsafe { - for i in 0..len { - assert_eq!(*dest.add(i), bytes_with_nul[i]); - } - } - - // Verify we can reconstruct a valid CStr from the cloned data + // Verify the cloned bytes form a valid CStr let cloned_slice = unsafe { core::slice::from_raw_parts(dest, len) }; let cloned_cstr = CStr::from_bytes_with_nul(cloned_slice); assert!(cloned_cstr.is_ok()); From ac63dd9154529c56ff368f85076df4369a6eec62 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Thu, 2 Apr 2026 11:39:56 +1100 Subject: [PATCH 4/6] Fix CStr clone_to_uninit harness soundness and typo Address review feedback: - Use initialized buffer to avoid UB from reading uninitialized memory - Assert exact byte-for-byte match with source - Document full safety contract requirements - Fix typo: trasnsparent -> transparent --- library/core/src/clone.rs | 4 +++- library/core/src/ffi/c_str.rs | 16 +++++++++++----- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs index a2bd21ef32844..29923926df734 100644 --- a/library/core/src/clone.rs +++ b/library/core/src/clone.rs @@ -548,9 +548,11 @@ unsafe impl CloneToUninit for str { #[unstable(feature = "clone_to_uninit", issue = "126799")] unsafe impl CloneToUninit for crate::ffi::CStr { #[cfg_attr(debug_assertions, track_caller)] + // Safety contract: dest must be non-null, valid for size_of_val(self) writes, + // and properly aligned (u8 alignment is always satisfied for non-null pointers). #[requires(!dest.is_null())] unsafe fn clone_to_uninit(&self, dest: *mut u8) { - // SAFETY: For now, CStr is just a #[repr(trasnsparent)] [c_char] with some invariants. + // SAFETY: For now, CStr is just a #[repr(transparent)] [c_char] with some invariants. // And we can cast [c_char] to [u8] on all supported platforms (see: to_bytes_with_nul). // The pointer metadata properly preserves the length (so NUL is also copied). // See: `cstr_metadata_is_length_with_nul` in tests. diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index ad620412244d5..d3cdcdd7efd25 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1131,11 +1131,13 @@ mod verify { let len = c_str.to_bytes_with_nul().len(); - // Allocate destination buffer (len <= MAX_SIZE since slice.len() <= MAX_SIZE) - let mut buf = [core::mem::MaybeUninit::::uninit(); MAX_SIZE]; - let dest = buf.as_mut_ptr() as *mut u8; + // Use an initialized buffer to avoid UB from reading uninitialized + // memory if clone_to_uninit were buggy and failed to write all bytes. + let mut buf = [0u8; MAX_SIZE]; + let dest = buf.as_mut_ptr(); - // Safety: dest is non-null (stack allocation), valid for len writes + // Safety: dest is non-null (stack allocation), valid for len writes, + // properly aligned (u8 has alignment 1) unsafe { c_str.clone_to_uninit(dest); } @@ -1144,6 +1146,10 @@ mod verify { let cloned_slice = unsafe { core::slice::from_raw_parts(dest, len) }; let cloned_cstr = CStr::from_bytes_with_nul(cloned_slice); assert!(cloned_cstr.is_ok()); - assert!(cloned_cstr.unwrap().is_safe()); + let cloned = cloned_cstr.unwrap(); + assert!(cloned.is_safe()); + + // Verify exact byte-for-byte match with source (including NUL terminator) + assert_eq!(cloned.to_bytes_with_nul(), c_str.to_bytes_with_nul()); } } From a9b65999a5627eb3c84229c8fac0e24e98614f6b Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Tue, 18 Aug 2026 21:50:36 +1000 Subject: [PATCH 5/6] Strengthen clone_to_uninit contract and verify it with proof_for_contract Per review on #543: - The CloneToUninit for CStr contract now uses the repo's memory predicates: requires can_write(slice_from_raw_parts_mut(dest, size_of_val(self))) plus a matching kani::modifies clause, replacing the weaker !dest.is_null() (which can_write subsumes). - New check_clone_to_uninit_contract harness: #[kani::proof_for_contract(CStr::clone_to_uninit)] with a deliberately uninitialized MaybeUninit destination, following the existing contract harness pattern in c_str.rs. The functional byte-for-byte check stays in check_clone_to_uninit. - Branch merged with current main: the previously pinned Kani 0.65 miscompiles contracts attached to this trait impl method (builtin memcpy assigns-check failure); the current pin (0.67, d4df833) verifies the impl contract directly. Local verification with the pinned Kani and CI flags: full ffi::c_str::verify suite passes, 15 of 15 harnesses. Co-Authored-By: Claude Fable 5 --- library/core/src/clone.rs | 15 ++++++++++++--- library/core/src/ffi/c_str.rs | 23 +++++++++++++++++++++++ 2 files changed, 35 insertions(+), 3 deletions(-) diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs index 025ecc0ede6ca..b605b71806558 100644 --- a/library/core/src/clone.rs +++ b/library/core/src/clone.rs @@ -580,9 +580,18 @@ unsafe impl CloneToUninit for str { #[unstable(feature = "clone_to_uninit", issue = "126799")] unsafe impl CloneToUninit for crate::ffi::CStr { #[cfg_attr(debug_assertions, track_caller)] - // Safety contract: dest must be non-null, valid for size_of_val(self) writes, - // and properly aligned (u8 alignment is always satisfied for non-null pointers). - #[requires(!dest.is_null())] + // Safety contract: `dest` must be valid for writes of `size_of_val(self)` + // bytes (the whole string including its NUL terminator) and properly + // aligned. `can_write` checks non-null, single-allocation bounds, and + // alignment (trivial for u8), matching the pointer contracts in + // `core::ptr` (e.g. `NonNull::write_bytes`); it subsumes the previous + // `!dest.is_null()`. The body writes exactly `size_of_val(self)` bytes + // through `dest`, which the modifies clause captures. Verified by + // `check_clone_to_uninit_contract` in ffi/c_str.rs. + #[requires(crate::ub_checks::can_write( + crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self)) + ))] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))))] unsafe fn clone_to_uninit(&self, dest: *mut u8) { // SAFETY: For now, CStr is just a #[repr(transparent)] [c_char] with some invariants. // And we can cast [c_char] to [u8] on all supported platforms (see: to_bytes_with_nul). diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index b85c76166c6cd..3f95e1ed5e2f7 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1152,4 +1152,27 @@ mod verify { // Verify exact byte-for-byte match with source (including NUL terminator) assert_eq!(cloned.to_bytes_with_nul(), c_str.to_bytes_with_nul()); } + + // Contract harness for `CloneToUninit for CStr` (Challenge 13, + // criterion 4): checks that the impl's `#[requires]` (dest valid for + // writes of `size_of_val(self)` bytes) and modifies clause rule out UB + // in the real body, following the pattern of the other contract + // harnesses in this file (`check_from_bytes_with_nul_unchecked`, + // `check_from_ptr`). The destination buffer is deliberately + // uninitialized: the contract only claims validity for writes, so the + // harness must not rely on `dest`'s contents. The functional + // (byte-for-byte) check stays in `check_clone_to_uninit` above. + #[kani::proof_for_contract(CStr::clone_to_uninit)] + #[kani::unwind(17)] + fn check_clone_to_uninit_contract() { + const MAX_SIZE: usize = 16; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); + + // Buffer of MAX_SIZE >= size_of_val(c_str) bytes, so the contract's + // `can_write` precondition is satisfiable for every generated length. + let mut dest = [crate::mem::MaybeUninit::::uninit(); MAX_SIZE]; + unsafe { crate::clone::CloneToUninit::clone_to_uninit(c_str, dest.as_mut_ptr().cast::()) }; + } } From 5cfc4487e6b8cbc41fdfd73f7393ab0d094aecd5 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Wed, 19 Aug 2026 06:44:08 +1000 Subject: [PATCH 6/6] Apply rustfmt formatting to contract attributes Co-Authored-By: Claude Fable 5 --- library/core/src/clone.rs | 12 ++++++++---- library/core/src/ffi/c_str.rs | 4 +++- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs index b605b71806558..b363c85bb9921 100644 --- a/library/core/src/clone.rs +++ b/library/core/src/clone.rs @@ -588,10 +588,14 @@ unsafe impl CloneToUninit for crate::ffi::CStr { // `!dest.is_null()`. The body writes exactly `size_of_val(self)` bytes // through `dest`, which the modifies clause captures. Verified by // `check_clone_to_uninit_contract` in ffi/c_str.rs. - #[requires(crate::ub_checks::can_write( - crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self)) - ))] - #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))))] + #[requires(crate::ub_checks::can_write(crate::ptr::slice_from_raw_parts_mut( + dest, + crate::mem::size_of_val(self) + )))] + #[cfg_attr( + kani, + kani::modifies(crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self))) + )] unsafe fn clone_to_uninit(&self, dest: *mut u8) { // SAFETY: For now, CStr is just a #[repr(transparent)] [c_char] with some invariants. // And we can cast [c_char] to [u8] on all supported platforms (see: to_bytes_with_nul). diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 3f95e1ed5e2f7..b4ffae79f7494 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1173,6 +1173,8 @@ mod verify { // Buffer of MAX_SIZE >= size_of_val(c_str) bytes, so the contract's // `can_write` precondition is satisfiable for every generated length. let mut dest = [crate::mem::MaybeUninit::::uninit(); MAX_SIZE]; - unsafe { crate::clone::CloneToUninit::clone_to_uninit(c_str, dest.as_mut_ptr().cast::()) }; + unsafe { + crate::clone::CloneToUninit::clone_to_uninit(c_str, dest.as_mut_ptr().cast::()) + }; } }