CStr : Proof for from_ptr with contract (#204)

Towards #150 Similar PR Ref : #193 Annotates and verifies the safety contracts for the unsafe function : `from_ptr` - `core::ffi::c_str` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Yenyun035 <[email protected]> Co-authored-by: Yenyun035 <[email protected]>
model-checking · Dec 11, 2024 · 9058f0b · 9058f0b
1 parent 4698b88
commit 9058f0b
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 2 deletions.
diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
@@ -9,8 +9,11 @@ use crate::marker::PhantomData;
 use crate::ptr::NonNull;
 use crate::slice::memchr;
 use crate::{fmt, ops, slice, str};
+use safety::{requires, ensures};
 
 use crate::ub_checks::Invariant;
+#[allow(unused_imports)]
+use crate::ub_checks::can_dereference;
 
 #[cfg(kani)]
 use crate::kani;
@@ -229,6 +232,25 @@ impl Invariant for &CStr {
     }
 }
 
+// Helper function
+#[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.
     ///
@@ -296,6 +318,8 @@ impl CStr {
     #[must_use]
     #[stable(feature = "rust1", since = "1.0.0")]
     #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")]
+    #[requires(!ptr.is_null() && is_null_terminated(ptr))]
+    #[ensures(|result: &&CStr| result.is_safe())]
     pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr {
         // SAFETY: The caller has provided a pointer that points to a valid C
         // string with a NUL terminator less than `isize::MAX` from `ptr`.
@@ -1017,6 +1041,16 @@ mod verify {
         assert_eq!(bytes, &slice[..end_idx]);
         assert!(c_str.is_safe());
     }
+
+    #[kani::proof_for_contract(CStr::from_ptr)]
+    #[kani::unwind(33)]
+    fn check_from_ptr_contract() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let ptr = string.as_ptr() as *const c_char;
+
+        unsafe { CStr::from_ptr(ptr); }
+    }
 
     #[kani::proof]
     #[kani::unwind(33)]

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
@@ -215,13 +215,13 @@ main() {
             -Z mem-predicates \
             -Z loop-contracts \
             -Z float-lib \
-            --output-format=terse \
+            -Z c-ffi \
             $command_args \
             --enable-unstable \
             --cbmc-args --object-bits 12
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
-        "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std --format markdown
+        "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format markdown
     fi
 }