add quantifiers to loop invariant

Author: thanhnguyen-aws

library/core/src/slice/memchr.rs

@@ -36,7 +36,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)`.
-    #[safety::loop_invariant(true)]
+    #[safety::loop_invariant(i <= text.len() && kani::forall!(|j in (0,i)| unsafe {*text.as_ptr().wrapping_add(j)} != x))]
     while i < text.len() {
         if text[i] == x {
             return Some(i);
@@ -79,7 +79,8 @@ const fn memchr_aligned(x: u8, text: &[u8]) -> Option<usize> {
 
             // search the body of the text
             let repeated_x = usize::repeat_u8(x);
-            #[safety::loop_invariant(len >= 2 * USIZE_BYTES && offset <= len)]
+            #[safety::loop_invariant(len >= 2 * USIZE_BYTES && offset <= len &&
+                kani::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.
@@ -170,22 +171,21 @@ pub mod verify {
     use crate::kani;
 
     #[kani::proof]
+    #[kani::solver(cvc5)]
     #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     pub fn check_memchr_naive() {
-        const ARR_SIZE: usize = 1000;
+        const ARR_SIZE: usize = 64;
         let x: u8 = kani::any();
-        let a: [u8; ARR_SIZE] = kani::any();
-        let text = kani::slice::any_slice_of_array(&a);
-        let _result = memchr_naive(x, text);
+        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 = 1000;
+        const ARR_SIZE: usize = 64;
         let x: u8 = kani::any();
-        let a: [u8; ARR_SIZE] = kani::any();
-        let text = kani::slice::any_slice_of_array(&a);
-        let _result = memrchr(x, text);
+        let text: [u8; ARR_SIZE] = kani::any();
+        let _result = memrchr(x, &text);
     }
 }