Loop invariants and harnesses for memchr functions

library/core/src/slice/memchr.rs

@@ -1,7 +1,11 @@
 // Original implementation taken from rust-memchr.
 // Copyright 2015 Andrew Gallant, bluss and Nicolas Koch
 
+#[cfg(kani)]
+use crate::forall;
 use crate::intrinsics::const_eval_select;
+#[cfg(kani)]
+use crate::kani;
 
 const LO_USIZE: usize = usize::repeat_u8(0x01);
 const HI_USIZE: usize = usize::repeat_u8(0x80);
@@ -36,6 +40,7 @@ const fn memchr_naive(x: u8, text: &[u8]) -> Option<usize> {
     let mut i = 0;
 
     // FIXME(const-hack): Replace with `text.iter().pos(|c| *c == x)`.
+    #[cfg_attr(kani, kani::loop_invariant(i <= text.len() && forall!(|j in (0,i)| unsafe {*text.as_ptr().wrapping_add(j)} != x)))]
     while i < text.len() {
         if text[i] == x {
             return Some(i);
@@ -78,6 +83,8 @@ const fn memchr_aligned(x: u8, text: &[u8]) -> Option<usize> {
 
             // search the body of the text
             let repeated_x = usize::repeat_u8(x);
+            #[cfg_attr(kani, kani::loop_invariant(len >= 2 * USIZE_BYTES && offset <= len &&
+                forall!(|j in (0,offset)| unsafe {*text.as_ptr().wrapping_add(j)} != x)))]
             while offset <= len - 2 * USIZE_BYTES {
                 // SAFETY: the while's predicate guarantees a distance of at least 2 * usize_bytes
                 // between the offset and the end of the slice.
@@ -139,6 +146,7 @@ pub fn memrchr(x: u8, text: &[u8]) -> Option<usize> {
     let repeated_x = usize::repeat_u8(x);
     let chunk_bytes = size_of::<Chunk>();
 
+    #[cfg_attr(kani, kani::loop_invariant(true))]
     while offset > min_aligned_offset {
         // SAFETY: offset starts at len - suffix.len(), as long as it is greater than
         // min_aligned_offset (prefix.len()) the remaining distance is at least 2 * chunk_bytes.
@@ -159,3 +167,28 @@ pub fn memrchr(x: u8, text: &[u8]) -> Option<usize> {
     // Find the byte before the point the body loop stopped.
     text[..offset].iter().rposition(|elt| *elt == x)
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use super::*;
+
+    #[kani::proof]
+    #[kani::solver(cvc5)]
+    #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
+    pub fn check_memchr_naive() {
+        const ARR_SIZE: usize = 64;
+        let x: u8 = kani::any();
+        let text: [u8; ARR_SIZE] = kani::any();
+        let _result = memchr_naive(x, &text);
+    }
+
+    #[kani::proof]
+    #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
+    pub fn check_memchr() {
+        const ARR_SIZE: usize = 64;
+        let x: u8 = kani::any();
+        let text: [u8; ARR_SIZE] = kani::any();
+        let _result = memrchr(x, &text);
+    }
+}

scripts/run-kani.sh

@@ -84,7 +84,7 @@ REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
 # Unstable arguments to pass to Kani
-unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts"
+unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers"
 
 # Variables used for parallel harness verification
 # When we say "parallel," we mean two dimensions of parallelization: