Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_unchecked

library/core/src/ffi/c_str.rs

@@ -11,6 +11,8 @@ use crate::slice::memchr;
 use crate::{fmt, ops, slice, str};
 
 use crate::ub_checks::Invariant;
+use crate::ub_checks::can_dereference;
+use safety::{requires, ensures};
 
 #[cfg(kani)]
 use crate::kani;
@@ -229,6 +231,24 @@ impl Invariant for &CStr {
     }
 }
 
+#[cfg(kani)]
+#[requires(!ptr.is_null())]
+fn is_null_terminated(ptr: *const c_char) -> bool {
+    let mut next = ptr;
+    let mut found_null = false;
+    while can_dereference(next) {
+        if unsafe { *next == 0 } {
+            found_null = true;
+            break;
+        }
+        next = next.wrapping_add(1);
+    }
+    if (next.addr() - ptr.addr()) >= isize::MAX as usize {
+        return false;
+    }
+    found_null
+}
+
 impl CStr {
     /// Wraps a raw C string with a safe C string wrapper.
     ///
@@ -432,6 +452,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 +779,8 @@ 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)]
+#[requires(is_null_terminated(ptr))]
+#[ensures(|&result| result < isize::MAX as usize && unsafe { *ptr.add(result) } == 0)]
 const unsafe fn strlen(ptr: *const c_char) -> usize {
     const_eval_select!(
         @capture { s: *const c_char = ptr } -> usize:
@@ -870,7 +896,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() {
@@ -886,6 +912,25 @@ mod verify {
         }
     }
 
+    //  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 fn bytes(&self) -> Bytes<'_>
     #[kani::proof]
     #[kani::unwind(32)]
@@ -1017,6 +1062,17 @@ mod verify {
         assert_eq!(bytes, &slice[..end_idx]);
         assert!(c_str.is_safe());
     }
+
+    // const unsafe fn strlen(ptr: *const c_char) -> usize
+    #[kani::proof_for_contract(super::strlen)]
+    #[kani::unwind(33)]
+    fn check_strlen_contract() {
+        const MAX_SIZE: usize = 32;
+        let mut string: [u8; MAX_SIZE] = kani::any();
+        let ptr = string.as_ptr() as *const c_char;
+
+        unsafe { super::strlen(ptr); }
+    }
 
     #[kani::proof]
     #[kani::unwind(33)]
@@ -1030,5 +1086,5 @@ mod verify {
         let expected_is_empty = bytes.len() == 0;
         assert_eq!(expected_is_empty, c_str.is_empty());
         assert!(c_str.is_safe());
-  }
+    }
 }