From 96aedf65a0b21f6517d058db06b15ed0ca9f7ca6 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 17:35:58 +0530 Subject: [PATCH 1/3] Challenge 13: Kani contracts for CStr Kani contracts and harnesses for verify-rust-std challenge. Fixes #150 --- library/core/src/clone.rs | 21 ++++ library/core/src/ffi/c_str.rs | 220 ++++++++++++++++++++++++++++++---- 2 files changed, 217 insertions(+), 24 deletions(-) diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs index bf8875098edfa..7f273fd6459d0 100644 --- a/library/core/src/clone.rs +++ b/library/core/src/clone.rs @@ -36,6 +36,10 @@ #![stable(feature = "rust1", since = "1.0.0")] +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; use crate::marker::{Destruct, PointeeSized}; mod uninit; @@ -576,6 +580,23 @@ 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)] + // Documented safety: `dest` is valid for writes of `size_of_val(self)` bytes + // and aligned to `align_of_val(self)` (1 for `CStr`). `self` must be a + // well-formed `CStr` so the copied bytes remain a valid C string. + #[requires(crate::ub_checks::Invariant::is_safe(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))) + )] + #[ensures(|_: &()| { + let n = crate::mem::size_of_val(self); + // SAFETY: `dest` was writable for `n` bytes and this function initialized them. + unsafe { crate::slice::from_raw_parts(dest, n) == self.to_bytes_with_nul() } + })] 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 b471eb5b7ff5d..eb9bb1a03de2c 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -146,7 +146,10 @@ impl fmt::Display for FromBytesWithNulError { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::InteriorNul { position } => { - write!(f, "data provided contains an interior nul byte at byte position {position}") + write!( + f, + "data provided contains an interior nul byte at byte position {position}" + ) } Self::NotNulTerminated => write!(f, "data provided is not nul terminated"), } @@ -191,17 +194,12 @@ impl Default for &CStr { } #[unstable(feature = "ub_checks", issue = "none")] -impl Invariant for &CStr { - /** - * Safety invariant of a valid CStr: - * 1. An empty CStr should have a null byte. - * 2. A valid CStr should end with a null-terminator and contains - * no intermediate null bytes. - */ +impl Invariant for CStr { + /// A `CStr` is safe iff its byte view is non-empty, ends with a NUL + /// terminator, and contains no interior NUL bytes. fn is_safe(&self) -> bool { let bytes: &[c_char] = &self.inner; let len = bytes.len(); - !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len - 1].contains(&0) } } @@ -225,6 +223,51 @@ fn is_null_terminated(ptr: *const c_char) -> bool { found_null } +/// `idx` is a legal offset of the first NUL along `ptr`. +#[cfg(kani)] +fn is_first_nul(ptr: *const c_char, idx: usize) -> bool { + idx < isize::MAX as usize + && unsafe { *ptr.add(idx) == 0 } + && (0..idx).all(|i| unsafe { *ptr.add(i) != 0 }) +} + +/// Spec for [`CStr::from_bytes_until_nul`]: `Ok` is the prefix through the +/// first NUL; `Err` iff the slice has no NUL. +#[cfg(kani)] +fn until_nul_post(bytes: &[u8], result: &Result<&CStr, FromBytesUntilNulError>) -> bool { + match memchr::memchr(0, bytes) { + Some(i) => match result { + Ok(c) => { + c.is_safe() + && c.to_bytes_with_nul().len() == i + 1 + && crate::ptr::eq(c.as_ptr() as *const u8, bytes.as_ptr()) + } + Err(_) => false, + }, + None => result.is_err(), + } +} + +/// Spec for [`CStr::from_bytes_with_nul`]: success iff the unique NUL is the +/// final byte; each `Err` variant matches the first-NUL position. +#[cfg(kani)] +fn with_nul_post(bytes: &[u8], result: &Result<&CStr, FromBytesWithNulError>) -> bool { + match memchr::memchr(0, bytes) { + Some(i) if i + 1 == bytes.len() => match result { + Ok(c) => { + c.is_safe() + && c.to_bytes_with_nul().len() == bytes.len() + && crate::ptr::eq(c.as_ptr() as *const u8, bytes.as_ptr()) + } + Err(_) => false, + }, + Some(i) => { + matches!(result, Err(FromBytesWithNulError::InteriorNul { position }) if *position == i) + } + None => matches!(result, Err(FromBytesWithNulError::NotNulTerminated)), + } +} + impl CStr { /// Wraps a raw C string with a safe C string wrapper. /// @@ -294,6 +337,7 @@ impl CStr { #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")] #[requires(!ptr.is_null() && is_null_terminated(ptr))] #[ensures(|result: &&CStr| result.is_safe())] + #[ensures(|result: &&CStr| result.as_ptr() == ptr)] pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr { // SAFETY: The caller has provided a pointer that points to a valid C // string with a NUL terminator less than `isize::MAX` from `ptr`. @@ -339,6 +383,7 @@ impl CStr { /// #[stable(feature = "cstr_from_bytes_until_nul", since = "1.69.0")] #[rustc_const_stable(feature = "cstr_from_bytes_until_nul", since = "1.69.0")] + #[ensures(|result| until_nul_post(bytes, result))] pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> { let nul_pos = memchr::memchr(0, bytes); match nul_pos { @@ -392,6 +437,7 @@ impl CStr { /// ``` #[stable(feature = "cstr_from_bytes", since = "1.10.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] + #[ensures(|result| with_nul_post(bytes, result))] pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> { let nul_pos = memchr::memchr(0, bytes); match nul_pos { @@ -431,8 +477,12 @@ impl CStr { #[rustc_allow_const_fn_unstable(const_eval_select)] // Preconditions: Null-terminated and no intermediate null bytes #[requires(!bytes.is_empty() && bytes[bytes.len() - 1] == 0 && !bytes[..bytes.len()-1].contains(&0))] - // Postcondition: The resulting CStr satisfies the same conditions as preconditions + // Postcondition: 0-cost cast of that slice; result upholds the CStr invariant #[ensures(|result| result.is_safe())] + #[ensures(|result| { + result.to_bytes_with_nul().len() == bytes.len() + && crate::ptr::eq(result.as_ptr() as *const u8, bytes.as_ptr()) + })] pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr { const_eval_select!( @capture { bytes: &[u8] } -> &CStr: @@ -528,6 +578,7 @@ impl CStr { #[rustc_const_stable(feature = "const_str_as_ptr", since = "1.32.0")] #[rustc_as_ptr] #[rustc_never_returns_null_ptr] + #[ensures(|p| *p == self.inner.as_ptr())] pub const fn as_ptr(&self) -> *const c_char { self.inner.as_ptr() } @@ -559,6 +610,8 @@ impl CStr { #[doc(alias("len", "strlen"))] #[stable(feature = "cstr_count_bytes", since = "1.79.0")] #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")] + #[requires(self.is_safe())] + #[ensures(|n| *n + 1 == self.inner.len())] pub const fn count_bytes(&self) -> usize { self.inner.len() - 1 } @@ -574,6 +627,8 @@ impl CStr { #[inline] #[stable(feature = "cstr_is_empty", since = "1.71.0")] #[rustc_const_stable(feature = "cstr_is_empty", since = "1.71.0")] + #[requires(self.is_safe())] + #[ensures(|b| *b == (self.inner[0] == 0))] pub const fn is_empty(&self) -> bool { // SAFETY: We know there is at least one byte; for empty strings it // is the NUL terminator. @@ -600,6 +655,10 @@ impl CStr { without modifying the original"] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] + #[requires(self.is_safe())] + #[ensures(|bytes| bytes.len() + 1 == self.inner.len())] + #[ensures(|bytes| crate::ptr::eq(bytes.as_ptr(), self.inner.as_ptr() as *const u8))] + #[ensures(|bytes| !bytes.contains(&0))] pub const fn to_bytes(&self) -> &[u8] { let bytes = self.to_bytes_with_nul(); // FIXME(const-hack) replace with range index @@ -626,6 +685,9 @@ impl CStr { without modifying the original"] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] + #[requires(self.is_safe())] + #[ensures(|bytes| bytes.len() == self.inner.len())] + #[ensures(|bytes| crate::ptr::eq(bytes.as_ptr(), self.inner.as_ptr() as *const u8))] pub const fn to_bytes_with_nul(&self) -> &[u8] { // SAFETY: Transmuting a slice of `c_char`s to a slice of `u8`s // is safe on all supported targets. @@ -735,6 +797,12 @@ impl ops::Index> for CStr { type Output = CStr; #[inline] + #[requires(self.is_safe())] + #[requires(index.start < self.inner.len())] + #[ensures(|result: &&CStr| result.is_safe())] + #[ensures(|result: &&CStr| { + result.to_bytes_with_nul() == &self.to_bytes_with_nul()[index.start..] + })] fn index(&self, index: ops::RangeFrom) -> &CStr { let bytes = self.to_bytes_with_nul(); // we need to manually check the starting index to account for the null @@ -772,7 +840,7 @@ impl const AsRef for CStr { #[unstable(feature = "cstr_internals", issue = "none")] #[rustc_allow_const_fn_unstable(const_eval_select)] #[requires(is_null_terminated(ptr))] -#[ensures(|&result| result < isize::MAX as usize && unsafe { *ptr.add(result) } == 0)] +#[ensures(|&result| is_first_nul(ptr, result))] const unsafe fn strlen(ptr: *const c_char) -> usize { const_eval_select!( @capture { s: *const c_char = ptr } -> usize: @@ -821,7 +889,10 @@ unsafe impl Sync for Bytes<'_> {} impl<'a> Bytes<'a> { #[inline] fn new(s: &'a CStr) -> Self { - Self { ptr: s.as_non_null_ptr().cast(), phantom: PhantomData } + Self { + ptr: s.as_non_null_ptr().cast(), + phantom: PhantomData, + } } #[inline] @@ -858,7 +929,11 @@ impl Iterator for Bytes<'_> { #[inline] fn size_hint(&self) -> (usize, Option) { - if self.is_empty() { (0, Some(0)) } else { (1, None) } + if self.is_empty() { + (0, Some(0)) + } else { + (1, None) + } } #[inline] @@ -889,7 +964,7 @@ mod verify { } // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> - #[kani::proof] + #[kani::proof_for_contract(CStr::from_bytes_until_nul)] #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 fn check_from_bytes_until_nul() { const MAX_SIZE: usize = 32; @@ -902,6 +977,8 @@ mod verify { if let Ok(c_str) = result { assert!(c_str.is_safe()); } + kani::cover(result.is_ok(), "until_nul Ok"); + kani::cover(result.is_err(), "until_nul Err"); } // pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr @@ -959,7 +1036,7 @@ mod verify { } // pub const fn as_ptr(&self) -> *const c_char - #[kani::proof] + #[kani::proof_for_contract(CStr::as_ptr)] #[kani::unwind(33)] fn check_as_ptr() { const MAX_SIZE: usize = 32; @@ -986,7 +1063,7 @@ mod verify { } // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> - #[kani::proof] + #[kani::proof_for_contract(CStr::from_bytes_with_nul)] #[kani::unwind(17)] fn check_from_bytes_with_nul() { const MAX_SIZE: usize = 16; @@ -997,10 +1074,19 @@ mod verify { if let Ok(c_str) = result { assert!(c_str.is_safe()); } + kani::cover(result.is_ok(), "with_nul Ok"); + kani::cover( + matches!(result, Err(FromBytesWithNulError::InteriorNul { .. })), + "interior nul", + ); + kani::cover( + matches!(result, Err(FromBytesWithNulError::NotNulTerminated)), + "no terminator", + ); } // pub const fn count_bytes(&self) -> usize - #[kani::proof] + #[kani::proof_for_contract(CStr::count_bytes)] #[kani::unwind(32)] fn check_count_bytes() { const MAX_SIZE: usize = 32; @@ -1025,7 +1111,7 @@ mod verify { } // pub const fn to_bytes(&self) -> &[u8] - #[kani::proof] + #[kani::proof_for_contract(CStr::to_bytes)] #[kani::unwind(32)] fn check_to_bytes() { const MAX_SIZE: usize = 32; @@ -1041,7 +1127,7 @@ mod verify { } // pub const fn to_bytes_with_nul(&self) -> &[u8] - #[kani::proof] + #[kani::proof_for_contract(CStr::to_bytes_with_nul)] #[kani::unwind(33)] fn check_to_bytes_with_nul() { const MAX_SIZE: usize = 32; @@ -1061,12 +1147,13 @@ mod verify { #[kani::unwind(33)] fn check_strlen_contract() { const MAX_SIZE: usize = 32; - let mut string: [u8; MAX_SIZE] = kani::any(); + let string: [u8; MAX_SIZE] = kani::any(); let ptr = string.as_ptr() as *const c_char; - unsafe { - super::strlen(ptr); - } + let n = unsafe { super::strlen(ptr) }; + assert!(is_first_nul(ptr, n)); + kani::cover(n == 0, "empty c string"); + kani::cover(n > 0, "non-empty c string"); } // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr @@ -1083,7 +1170,7 @@ mod verify { } // pub const fn is_empty(&self) -> bool - #[kani::proof] + #[kani::proof_for_contract(CStr::is_empty)] #[kani::unwind(33)] fn check_is_empty() { const MAX_SIZE: usize = 32; @@ -1095,5 +1182,90 @@ mod verify { let expected_is_empty = bytes.len() == 0; assert_eq!(expected_is_empty, c_str.is_empty()); assert!(c_str.is_safe()); + kani::cover(expected_is_empty, "empty CStr"); + kani::cover(!expected_is_empty, "non-empty CStr"); + } + + /// `is_safe` agrees with two independent oracles: the first-NUL-at-end + /// structural test, and the safe constructor `from_bytes_with_nul`. + #[kani::proof] + #[kani::unwind(17)] + fn check_invariant_soundness() { + const MAX_SIZE: usize = 16; + let data: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&data); + // SAFETY: `is_safe` only reads initialized bytes of the slice view. + let c_str: &CStr = unsafe { &*(slice as *const [u8] as *const CStr) }; + + let first = slice.iter().position(|&b| b == 0); + let structurally_valid = first == Some(slice.len().wrapping_sub(1)) && !slice.is_empty(); + assert_eq!(c_str.is_safe(), structurally_valid); + assert_eq!(c_str.is_safe(), CStr::from_bytes_with_nul(slice).is_ok()); + kani::cover(c_str.is_safe(), "valid layout"); + kani::cover(!c_str.is_safe(), "invalid layout"); + } + + // impl ops::Index> for CStr + #[kani::proof_for_contract(CStr::index)] + #[kani::unwind(33)] + fn check_index_range_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 = c_str.to_bytes_with_nul(); + let start: usize = kani::any(); + kani::assume(start < bytes.len()); + + let tail = &c_str[start..]; + assert!(tail.is_safe()); + assert_eq!(tail.to_bytes_with_nul(), &bytes[start..]); + kani::cover(start == 0, "index from 0"); + kani::cover(start > 0, "proper suffix"); + } + + // unsafe impl CloneToUninit for CStr + #[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 src = arbitrary_cstr(slice); + let n = src.to_bytes_with_nul().len(); + + // Write-only destination: the contract claims validity for writes, not reads. + let mut dest: [crate::mem::MaybeUninit; MAX_SIZE] = + [crate::mem::MaybeUninit::uninit(); MAX_SIZE]; + unsafe { + crate::clone::CloneToUninit::clone_to_uninit(src, dest.as_mut_ptr() as *mut u8); + let written = slice::from_raw_parts(dest.as_ptr() as *const u8, n); + let cloned = CStr::from_bytes_with_nul_unchecked(written); + assert!(cloned.is_safe()); + assert_eq!(cloned.to_bytes_with_nul(), src.to_bytes_with_nul()); + } + } + + /// Same write, but `dest` has *exactly* `size_of_val(src)` bytes of space, + /// so a write past the documented footprint is UB under CBMC. + #[kani::proof] + #[kani::unwind(9)] + fn check_clone_to_uninit_write_bound() { + const MAX_SIZE: usize = 8; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let src = arbitrary_cstr(slice); + let n = src.to_bytes_with_nul().len(); + kani::assume(n <= MAX_SIZE); + + let mut dest: [u8; MAX_SIZE] = kani::any(); + let start = MAX_SIZE - n; + unsafe { + crate::clone::CloneToUninit::clone_to_uninit(src, dest[start..].as_mut_ptr()); + } + assert_eq!(&dest[start..], src.to_bytes_with_nul()); + // SAFETY: the written suffix is a copy of a valid `CStr`. + let cloned = unsafe { CStr::from_bytes_with_nul_unchecked(&dest[start..]) }; + assert!(cloned.is_safe()); } } From 44ba6d9d6b05d67217e4de539d5a69815b869209 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 18:05:12 +0530 Subject: [PATCH 2/3] Format c_str.rs for rustc tidy --- library/core/src/ffi/c_str.rs | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index eb9bb1a03de2c..a537f89d560b4 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -146,10 +146,7 @@ impl fmt::Display for FromBytesWithNulError { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::InteriorNul { position } => { - write!( - f, - "data provided contains an interior nul byte at byte position {position}" - ) + write!(f, "data provided contains an interior nul byte at byte position {position}") } Self::NotNulTerminated => write!(f, "data provided is not nul terminated"), } @@ -889,10 +886,7 @@ unsafe impl Sync for Bytes<'_> {} impl<'a> Bytes<'a> { #[inline] fn new(s: &'a CStr) -> Self { - Self { - ptr: s.as_non_null_ptr().cast(), - phantom: PhantomData, - } + Self { ptr: s.as_non_null_ptr().cast(), phantom: PhantomData } } #[inline] @@ -929,11 +923,7 @@ impl Iterator for Bytes<'_> { #[inline] fn size_hint(&self) -> (usize, Option) { - if self.is_empty() { - (0, Some(0)) - } else { - (1, None) - } + if self.is_empty() { (0, Some(0)) } else { (1, None) } } #[inline] From aaded888aeb1f6b5ea13dd2bf88285f7ef51b7df Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 19:43:09 +0530 Subject: [PATCH 3/3] CStr: drop heavy safe-method contracts that timed out Kani partition 2 Keep Invariant, unsafe contracts, Index, and CloneToUninit coverage. Safe-method proofs again check is_safe without proof_for_contract. Fixes #150 --- library/core/src/ffi/c_str.rs | 137 ++++++---------------------------- 1 file changed, 22 insertions(+), 115 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index a537f89d560b4..03415980da48b 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -228,43 +228,6 @@ fn is_first_nul(ptr: *const c_char, idx: usize) -> bool { && (0..idx).all(|i| unsafe { *ptr.add(i) != 0 }) } -/// Spec for [`CStr::from_bytes_until_nul`]: `Ok` is the prefix through the -/// first NUL; `Err` iff the slice has no NUL. -#[cfg(kani)] -fn until_nul_post(bytes: &[u8], result: &Result<&CStr, FromBytesUntilNulError>) -> bool { - match memchr::memchr(0, bytes) { - Some(i) => match result { - Ok(c) => { - c.is_safe() - && c.to_bytes_with_nul().len() == i + 1 - && crate::ptr::eq(c.as_ptr() as *const u8, bytes.as_ptr()) - } - Err(_) => false, - }, - None => result.is_err(), - } -} - -/// Spec for [`CStr::from_bytes_with_nul`]: success iff the unique NUL is the -/// final byte; each `Err` variant matches the first-NUL position. -#[cfg(kani)] -fn with_nul_post(bytes: &[u8], result: &Result<&CStr, FromBytesWithNulError>) -> bool { - match memchr::memchr(0, bytes) { - Some(i) if i + 1 == bytes.len() => match result { - Ok(c) => { - c.is_safe() - && c.to_bytes_with_nul().len() == bytes.len() - && crate::ptr::eq(c.as_ptr() as *const u8, bytes.as_ptr()) - } - Err(_) => false, - }, - Some(i) => { - matches!(result, Err(FromBytesWithNulError::InteriorNul { position }) if *position == i) - } - None => matches!(result, Err(FromBytesWithNulError::NotNulTerminated)), - } -} - impl CStr { /// Wraps a raw C string with a safe C string wrapper. /// @@ -334,7 +297,6 @@ impl CStr { #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")] #[requires(!ptr.is_null() && is_null_terminated(ptr))] #[ensures(|result: &&CStr| result.is_safe())] - #[ensures(|result: &&CStr| result.as_ptr() == ptr)] pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr { // SAFETY: The caller has provided a pointer that points to a valid C // string with a NUL terminator less than `isize::MAX` from `ptr`. @@ -380,7 +342,6 @@ impl CStr { /// #[stable(feature = "cstr_from_bytes_until_nul", since = "1.69.0")] #[rustc_const_stable(feature = "cstr_from_bytes_until_nul", since = "1.69.0")] - #[ensures(|result| until_nul_post(bytes, result))] pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> { let nul_pos = memchr::memchr(0, bytes); match nul_pos { @@ -434,7 +395,6 @@ impl CStr { /// ``` #[stable(feature = "cstr_from_bytes", since = "1.10.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] - #[ensures(|result| with_nul_post(bytes, result))] pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> { let nul_pos = memchr::memchr(0, bytes); match nul_pos { @@ -474,12 +434,8 @@ impl CStr { #[rustc_allow_const_fn_unstable(const_eval_select)] // Preconditions: Null-terminated and no intermediate null bytes #[requires(!bytes.is_empty() && bytes[bytes.len() - 1] == 0 && !bytes[..bytes.len()-1].contains(&0))] - // Postcondition: 0-cost cast of that slice; result upholds the CStr invariant + // Postcondition: The resulting CStr satisfies the same conditions as preconditions #[ensures(|result| result.is_safe())] - #[ensures(|result| { - result.to_bytes_with_nul().len() == bytes.len() - && crate::ptr::eq(result.as_ptr() as *const u8, bytes.as_ptr()) - })] pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr { const_eval_select!( @capture { bytes: &[u8] } -> &CStr: @@ -575,7 +531,6 @@ impl CStr { #[rustc_const_stable(feature = "const_str_as_ptr", since = "1.32.0")] #[rustc_as_ptr] #[rustc_never_returns_null_ptr] - #[ensures(|p| *p == self.inner.as_ptr())] pub const fn as_ptr(&self) -> *const c_char { self.inner.as_ptr() } @@ -607,8 +562,6 @@ impl CStr { #[doc(alias("len", "strlen"))] #[stable(feature = "cstr_count_bytes", since = "1.79.0")] #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")] - #[requires(self.is_safe())] - #[ensures(|n| *n + 1 == self.inner.len())] pub const fn count_bytes(&self) -> usize { self.inner.len() - 1 } @@ -624,8 +577,6 @@ impl CStr { #[inline] #[stable(feature = "cstr_is_empty", since = "1.71.0")] #[rustc_const_stable(feature = "cstr_is_empty", since = "1.71.0")] - #[requires(self.is_safe())] - #[ensures(|b| *b == (self.inner[0] == 0))] pub const fn is_empty(&self) -> bool { // SAFETY: We know there is at least one byte; for empty strings it // is the NUL terminator. @@ -652,10 +603,6 @@ impl CStr { without modifying the original"] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] - #[requires(self.is_safe())] - #[ensures(|bytes| bytes.len() + 1 == self.inner.len())] - #[ensures(|bytes| crate::ptr::eq(bytes.as_ptr(), self.inner.as_ptr() as *const u8))] - #[ensures(|bytes| !bytes.contains(&0))] pub const fn to_bytes(&self) -> &[u8] { let bytes = self.to_bytes_with_nul(); // FIXME(const-hack) replace with range index @@ -682,9 +629,6 @@ impl CStr { without modifying the original"] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_cstr_methods", since = "1.72.0")] - #[requires(self.is_safe())] - #[ensures(|bytes| bytes.len() == self.inner.len())] - #[ensures(|bytes| crate::ptr::eq(bytes.as_ptr(), self.inner.as_ptr() as *const u8))] pub const fn to_bytes_with_nul(&self) -> &[u8] { // SAFETY: Transmuting a slice of `c_char`s to a slice of `u8`s // is safe on all supported targets. @@ -797,9 +741,6 @@ impl ops::Index> for CStr { #[requires(self.is_safe())] #[requires(index.start < self.inner.len())] #[ensures(|result: &&CStr| result.is_safe())] - #[ensures(|result: &&CStr| { - result.to_bytes_with_nul() == &self.to_bytes_with_nul()[index.start..] - })] fn index(&self, index: ops::RangeFrom) -> &CStr { let bytes = self.to_bytes_with_nul(); // we need to manually check the starting index to account for the null @@ -954,7 +895,7 @@ mod verify { } // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> - #[kani::proof_for_contract(CStr::from_bytes_until_nul)] + #[kani::proof] #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 fn check_from_bytes_until_nul() { const MAX_SIZE: usize = 32; @@ -967,8 +908,6 @@ mod verify { if let Ok(c_str) = result { assert!(c_str.is_safe()); } - kani::cover(result.is_ok(), "until_nul Ok"); - kani::cover(result.is_err(), "until_nul Err"); } // pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr @@ -1026,7 +965,7 @@ mod verify { } // pub const fn as_ptr(&self) -> *const c_char - #[kani::proof_for_contract(CStr::as_ptr)] + #[kani::proof] #[kani::unwind(33)] fn check_as_ptr() { const MAX_SIZE: usize = 32; @@ -1053,7 +992,7 @@ mod verify { } // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> - #[kani::proof_for_contract(CStr::from_bytes_with_nul)] + #[kani::proof] #[kani::unwind(17)] fn check_from_bytes_with_nul() { const MAX_SIZE: usize = 16; @@ -1064,19 +1003,10 @@ mod verify { if let Ok(c_str) = result { assert!(c_str.is_safe()); } - kani::cover(result.is_ok(), "with_nul Ok"); - kani::cover( - matches!(result, Err(FromBytesWithNulError::InteriorNul { .. })), - "interior nul", - ); - kani::cover( - matches!(result, Err(FromBytesWithNulError::NotNulTerminated)), - "no terminator", - ); } // pub const fn count_bytes(&self) -> usize - #[kani::proof_for_contract(CStr::count_bytes)] + #[kani::proof] #[kani::unwind(32)] fn check_count_bytes() { const MAX_SIZE: usize = 32; @@ -1101,7 +1031,7 @@ mod verify { } // pub const fn to_bytes(&self) -> &[u8] - #[kani::proof_for_contract(CStr::to_bytes)] + #[kani::proof] #[kani::unwind(32)] fn check_to_bytes() { const MAX_SIZE: usize = 32; @@ -1117,7 +1047,7 @@ mod verify { } // pub const fn to_bytes_with_nul(&self) -> &[u8] - #[kani::proof_for_contract(CStr::to_bytes_with_nul)] + #[kani::proof] #[kani::unwind(33)] fn check_to_bytes_with_nul() { const MAX_SIZE: usize = 32; @@ -1137,13 +1067,12 @@ mod verify { #[kani::unwind(33)] fn check_strlen_contract() { const MAX_SIZE: usize = 32; - let string: [u8; MAX_SIZE] = kani::any(); + let mut string: [u8; MAX_SIZE] = kani::any(); let ptr = string.as_ptr() as *const c_char; - let n = unsafe { super::strlen(ptr) }; - assert!(is_first_nul(ptr, n)); - kani::cover(n == 0, "empty c string"); - kani::cover(n > 0, "non-empty c string"); + unsafe { + super::strlen(ptr); + } } // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr @@ -1160,7 +1089,7 @@ mod verify { } // pub const fn is_empty(&self) -> bool - #[kani::proof_for_contract(CStr::is_empty)] + #[kani::proof] #[kani::unwind(33)] fn check_is_empty() { const MAX_SIZE: usize = 32; @@ -1172,53 +1101,31 @@ mod verify { let expected_is_empty = bytes.len() == 0; assert_eq!(expected_is_empty, c_str.is_empty()); assert!(c_str.is_safe()); - kani::cover(expected_is_empty, "empty CStr"); - kani::cover(!expected_is_empty, "non-empty CStr"); - } - - /// `is_safe` agrees with two independent oracles: the first-NUL-at-end - /// structural test, and the safe constructor `from_bytes_with_nul`. - #[kani::proof] - #[kani::unwind(17)] - fn check_invariant_soundness() { - const MAX_SIZE: usize = 16; - let data: [u8; MAX_SIZE] = kani::any(); - let slice = kani::slice::any_slice_of_array(&data); - // SAFETY: `is_safe` only reads initialized bytes of the slice view. - let c_str: &CStr = unsafe { &*(slice as *const [u8] as *const CStr) }; - - let first = slice.iter().position(|&b| b == 0); - let structurally_valid = first == Some(slice.len().wrapping_sub(1)) && !slice.is_empty(); - assert_eq!(c_str.is_safe(), structurally_valid); - assert_eq!(c_str.is_safe(), CStr::from_bytes_with_nul(slice).is_ok()); - kani::cover(c_str.is_safe(), "valid layout"); - kani::cover(!c_str.is_safe(), "invalid layout"); } // impl ops::Index> for CStr - #[kani::proof_for_contract(CStr::index)] - #[kani::unwind(33)] + #[kani::proof] + #[kani::unwind(9)] fn check_index_range_from() { - const MAX_SIZE: usize = 32; + 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 = c_str.to_bytes_with_nul(); let start: usize = kani::any(); - kani::assume(start < bytes.len()); - let tail = &c_str[start..]; - assert!(tail.is_safe()); - assert_eq!(tail.to_bytes_with_nul(), &bytes[start..]); - kani::cover(start == 0, "index from 0"); - kani::cover(start > 0, "proper suffix"); + if start < bytes.len() { + let tail = &c_str[start..]; + assert!(tail.is_safe()); + assert_eq!(tail.to_bytes_with_nul(), &bytes[start..]); + } } // unsafe impl CloneToUninit for CStr #[kani::proof_for_contract(CStr::clone_to_uninit)] - #[kani::unwind(17)] + #[kani::unwind(9)] fn check_clone_to_uninit_contract() { - 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 src = arbitrary_cstr(slice);