CStr Safety invariant & Harnesses for from_bytes_until_nul

library/core/src/ffi/c_str.rs

@@ -9,6 +9,12 @@ use crate::ptr::NonNull;
 use crate::slice::memchr;
 use crate::{fmt, intrinsics, ops, slice, str};
 
+// use safety::{requires, ensures};
+use crate::ub_checks::Invariant;
+
+#[cfg(kani)]
+use crate::kani;
+
 // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link
 //   depends on where the item is being documented. however, since this is libcore, we can't
 //   actually reference libstd or liballoc in intra-doc links. so, the best we can do is remove the
@@ -207,6 +213,23 @@ impl fmt::Display for FromBytesWithNulError {
     }
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl Invariant for &CStr {
+    fn is_safe(&self) -> bool {
+        let bytes: &[c_char] = &self.inner;
+        let len = bytes.len();
+
+        // An empty CStr should has a null byte.
+        // A valid CStr should end with a null-terminator and contains
+        // no intermediate null bytes.
+        if bytes.is_empty() || bytes[len - 1] != 0 || bytes[..len-1].contains(&0) {
+            return false;
+        }
+
+        true
+    }
+}
+
 impl CStr {
     /// Wraps a raw C string with a safe C string wrapper.
     ///
@@ -833,3 +856,26 @@ impl Iterator for Bytes<'_> {
 
 #[unstable(feature = "cstr_bytes", issue = "112115")]
 impl FusedIterator for Bytes<'_> {}
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
+    #[kani::proof]
+    #[kani::unwind(16)] // 7.3 seconds when 16; 33.1 seconds when 32
+    fn check_from_bytes_until_nul() {
+        const MAX_SIZE: usize = 16;
+        let string: [u8; MAX_SIZE] = kani::any();
+        // Covers the case of a single null byte at the end, no null bytes, as
+        // well as intermediate null bytes
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        let result = CStr::from_bytes_until_nul(slice);
+        if result.is_ok() {
+            let c_str = result.unwrap();
+            assert!(c_str.is_safe());
+        }
+    }
+}