Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_unchecked

library/core/src/ffi/c_str.rs

@@ -10,6 +10,7 @@ use crate::slice::memchr;
 use crate::{fmt, intrinsics, ops, slice, str};
 
 use crate::ub_checks::Invariant;
+use safety::{requires, ensures};
 
 #[cfg(kani)]
 use crate::kani;
@@ -431,6 +432,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 {
         #[inline]
         fn rt_impl(bytes: &[u8]) -> &CStr {
@@ -860,7 +865,7 @@ impl FusedIterator for Bytes<'_> {}
 mod verify {
     use super::*;
 
-    // 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() {
@@ -875,4 +880,82 @@ mod verify {
             assert!(c_str.is_safe());
         }
     }
-}
+
+    // Stub implementation for strlen: https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html
+    #[cfg(kani)]
+    unsafe fn stub_strlen(s: *const c_char) -> usize {
+        let mut len = 0;
+        unsafe {
+            while *s.add(len) != 0 {
+                len += 1;
+            }
+        }
+        len
+    }
+
+    // Proof harness for pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr
+    #[cfg(kani)]
+    #[kani::proof]
+    #[kani::unwind(33)] 
+    #[kani::stub(strlen, stub_strlen)]
+    fn check_from_ptr() {
+        const MAX_SIZE: usize = 32;
+        //generating an arbitrary byte array with a max size
+        let mut string: [u8; MAX_SIZE] = kani::any();
+        // need At least one nul terminator is present within the array
+        let nul_position: usize = kani::any_where(|x| *x >= 0 && *x < MAX_SIZE);
+        string[nul_position] = 0;
+        // Make sure that there are no other nul bytes before `nul_position`
+        for i in 0..nul_position {
+            kani::assume(string[i] != 0);
+        }
+        // start from the beginning of the string
+        let ptr = string.as_ptr().cast::<c_char>();
+        let c_str = unsafe { CStr::from_ptr(ptr) };
+        // Compute the expected length up to the nul terminator
+        let len = unsafe { strlen(ptr) };
+        // Check that `c_str` has the correct length
+        assert_eq!(c_str.to_bytes().len(), len);
+        assert!(c_str.is_safe());
+    }
+
+    // Proof harness for const unsafe fn strlen(ptr: *const c_char) -> usize
+    #[cfg(kani)]
+    #[kani::proof]
+    #[kani::unwind(32)]
+    #[kani::stub(strlen, stub_strlen)]
+    fn check_strlen() {
+        const MAX_SIZE: usize = 32;
+        let mut string: [u8; MAX_SIZE] = kani::any();
+        let nul_position: usize = kani::any_where(|x| *x >= 0 && *x < MAX_SIZE);
+        string[nul_position] = 0;
+        // Make sure that there are no other nul bytes before `nul_position`
+        for i in 0..nul_position {
+            kani::assume(string[i] != 0);
+        }
+        let ptr = string.as_ptr().cast::<c_char>();
+        // Call strlen with the pointer
+        let len = unsafe { strlen(ptr) };
+        // Check that len matches the expected position of the nul terminator
+        assert_eq!(len, nul_position);
+    }
+
+    //  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]);
+    }
+}