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..03415980da48b 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -191,17 +191,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 +220,14 @@ 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 }) +} + impl CStr { /// Wraps a raw C string with a safe C string wrapper. /// @@ -735,6 +738,9 @@ 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())] 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 +778,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: @@ -1096,4 +1102,67 @@ mod verify { assert_eq!(expected_is_empty, c_str.is_empty()); assert!(c_str.is_safe()); } + + // impl ops::Index> for CStr + #[kani::proof] + #[kani::unwind(9)] + fn check_index_range_from() { + 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(); + + 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(9)] + fn check_clone_to_uninit_contract() { + 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(); + + // 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()); + } }