Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_unchecked

library/core/src/ffi/c_str.rs

@@ -11,6 +11,7 @@ use crate::slice::memchr;
 use crate::{fmt, ops, slice, str};
 
 use crate::ub_checks::Invariant;
+use safety::{requires, ensures};
 
 #[cfg(kani)]
 use crate::kani;
@@ -432,6 +433,10 @@ impl CStr {
     #[stable(feature = "cstr_from_bytes", since = "1.10.0")]
     #[rustc_const_stable(feature = "const_cstr_unchecked", since = "1.59.0")]
     #[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
+    #[ensures(|result| result.is_safe())]
     pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr {
         const_eval_select!(
             @capture { bytes: &[u8] } -> &CStr:
@@ -755,6 +760,33 @@ impl AsRef<CStr> for CStr {
 #[unstable(feature = "cstr_internals", issue = "none")]
 #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0"))]
 #[rustc_allow_const_fn_unstable(const_eval_select)]
+// Preconditions:
+// - ptr must be non-null
+// - ptr must point to a valid null-terminated string
+// - null terminator must be within isize::MAX bytes from ptr
+#[requires(!ptr.is_null() && {
+    let mut found_null = false;
+    for i in 0..isize::MAX as usize {
+        if unsafe { *ptr.add(i) } == 0 {
+            found_null = true;
+            break;
+        }
+    }
+    found_null
+})]
+// Postconditions:
+// - Returns length before null terminator
+// - Length must be less than isize::MAX
+#[ensures(|&result| result < isize::MAX as usize && {
+    let mut valid = true;
+    for i in 0..result {
+        if unsafe { *ptr.add(i) } == 0 {
+            valid = false;
+            break;
+        }
+    }
+    valid && unsafe { *ptr.add(result) } == 0
+})]
 const unsafe fn strlen(ptr: *const c_char) -> usize {
     const_eval_select!(
         @capture { s: *const c_char = ptr } -> usize:
@@ -867,7 +899,7 @@ mod verify {
         c_str
     }
 
-    // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
+    // Proof harness for pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> 
     #[kani::proof]
     #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32
     fn check_from_bytes_until_nul() {
@@ -882,6 +914,25 @@ mod verify {
             assert!(c_str.is_safe());
         }
     }
+
+    //  pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr
+    #[kani::proof_for_contract(CStr::from_bytes_with_nul_unchecked)]
+    #[kani::unwind(33)]
+    fn check_from_bytes_with_nul_unchecked() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        // Kani assumes that the input slice is null-terminated and contains
+        // no intermediate null bytes
+        let c_str = unsafe { CStr::from_bytes_with_nul_unchecked(slice) };
+        // Kani ensures that the output CStr holds the CStr safety invariant
+
+        // Correctness check
+        let bytes = c_str.to_bytes();
+        let len = bytes.len();
+        assert_eq!(bytes, &slice[..len]);
+    }
 
     // pub const fn count_bytes(&self) -> usize
     #[kani::proof]
@@ -939,4 +990,37 @@ mod verify {
         assert_eq!(bytes, &slice[..end_idx]);
         assert!(c_str.is_safe());
     }
-}
+
+    #[kani::proof_for_contract(super::strlen)]
+    #[kani::unwind(32)]
+    fn check_strlen_contract() {
+        const MAX_SIZE: usize = 32;
+        let mut string: [u8; MAX_SIZE] = kani::any();
+        let nul_position: usize = kani::any_where(|x| *x < MAX_SIZE);
+        string[nul_position] = 0;
+
+        // Ensure no null bytes before nul_position
+        for i in 0..nul_position {
+            kani::assume(string[i] != 0);
+        }
+
+        let ptr = string.as_ptr() as *const c_char;
+
+        unsafe {
+            let len = super::strlen(ptr);
+
+            // Length must be less than isize::MAX
+            assert!(len < isize::MAX as usize);
+            // Length must equal nul_position
+            assert_eq!(len, nul_position);
+            // no null in between
+            for i in 0..len {
+                assert!(*ptr.add(i) != 0);
+            }
+            // additional checks
+            assert_eq!(*ptr.add(len), 0);
+            assert!(len <= MAX_SIZE - 1);
+        }
+    }
+}
+