Challenge 13: Kani contracts for CStr

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).

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<ops::RangeFrom<usize>> 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<usize>) -> &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<CStr> 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<ops::RangeFrom<usize>> 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<u8>; 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());
+    }
 }