Add loop contracts and harness for Utf8Chunk::next

Author: qinheping

library/core/src/lib.rs

@@ -230,6 +230,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
+#![feature(proc_macro_hygiene)]
 // tidy-alphabetical-end
 //
 // Target features:

library/core/src/str/lossy.rs

@@ -4,6 +4,9 @@ use crate::fmt;
 use crate::fmt::{Formatter, Write};
 use crate::iter::FusedIterator;
 
+#[cfg(kani)]
+use crate::kani;
+
 impl [u8] {
     /// Creates an iterator over the contiguous valid UTF-8 ranges of this
     /// slice, and the non-UTF-8 fragments in between.
@@ -204,6 +207,11 @@ impl<'a> Iterator for Utf8Chunks<'a> {
 
         let mut i = 0;
         let mut valid_up_to = 0;
+        // TODO: remove `LEN` and use `self.source.len()` directly once
+        // fix the issue that Kani loop contracts doesn't support `self`.
+        #[cfg(kani)]
+        let LEN = self.source.len();
+        #[safety::loop_invariant(i <= LEN && valid_up_to == i)]
         while i < self.source.len() {
             // SAFETY: `i < self.source.len()` per previous line.
             // For some reason the following are both significantly slower:
@@ -296,3 +304,22 @@ impl fmt::Debug for Utf8Chunks<'_> {
         f.debug_struct("Utf8Chunks").field("source", &self.debug()).finish()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use super::*;
+
+    #[kani::proof]
+    pub fn check_next() {
+        // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument
+        // `--arrays-uf-always`
+        const ARR_SIZE: usize = 1000;
+        let mut x: [u8; ARR_SIZE] = kani::any();
+        let mut xs = kani::slice::any_slice_of_array_mut(&mut x);
+        let mut chunks = xs.utf8_chunks();
+        unsafe {
+            chunks.next();
+        }
+    }
+}

scripts/run-kani.sh

@@ -183,7 +183,7 @@ main() {
 
     echo "Running Kani verify-std command..."
 
-    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
+    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12
 }
 
 main

tool_config/kani-version.toml

@@ -2,4 +2,4 @@
 # incompatible with the verify-std repo.
 
 [kani]
-commit = "2565ef65767a696f1d519b42621b4e502e8970d0"
+commit = "8400296f5280be4f99820129bc66447e8dff63f4"