Challenge 20: Unbounded proofs for the char Searchers of str::pattern

library/core/src/ffi/c_str.rs

@@ -1149,7 +1149,12 @@ mod verify {
     }
 
     // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr
+    // The stub: this harness reaches `CharSearcher::next_match` only through
+    // panic formatting, where it never runs. Its loop contract would make Kani
+    // apply loop contracts here, and CBMC 6.11 then rejects the loop of its
+    // built-in `strlen` (fixed by diffblue/cbmc#9164).
     #[kani::proof_for_contract(CStr::from_ptr)]
+    #[kani::stub(<crate::str::pattern::CharSearcher as crate::str::pattern::Searcher>::next_match, any_match)]
     #[kani::unwind(33)]
     fn check_from_ptr_contract() {
         const MAX_SIZE: usize = 32;
@@ -1161,6 +1166,14 @@ mod verify {
         }
     }
 
+    // `'a: 'a` makes `'a` early-bound, like the lifetime of the impl.
+    fn any_match<'a>(_: &mut crate::str::pattern::CharSearcher<'a>) -> Option<(usize, usize)>
+    where
+        'a: 'a,
+    {
+        kani::any()
+    }
+
     // pub const fn is_empty(&self) -> bool
     #[kani::proof]
     #[kani::unwind(33)]

library/core/src/slice/iter.rs

@@ -168,6 +168,23 @@ impl<T> AsRef<[T]> for Iter<'_, T> {
     }
 }
 
+#[cfg(kani)]
+impl<T> Iter<'_, T> {
+    /// `(ptr, end_or_len)`, read without calls, for the proofs in
+    /// `str::pattern`.
+    pub(crate) fn kani_raw_parts(&self) -> (*const T, *const T) {
+        // SAFETY: `NonNull<T>` is a transparent `*const T`.
+        (unsafe { mem::transmute::<NonNull<T>, *const T>(self.ptr) }, self.end_or_len)
+    }
+
+    /// The same, for the loop invariants in `str::pattern`: a loop invariant
+    /// must not call a function that other code also calls.
+    pub(crate) fn kani_loop_raw_parts(&self) -> (*const T, *const T) {
+        // SAFETY: `NonNull<T>` is a transparent `*const T`.
+        (unsafe { mem::transmute::<NonNull<T>, *const T>(self.ptr) }, self.end_or_len)
+    }
+}
+
 #[unstable(feature = "ub_checks", issue = "none")]
 impl<T> Invariant for Iter<'_, T> {
     /// An iterator can be safely used if its pointer can be read for its current length.