Add loop contracts and harness for Slice::is_ascii

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/slice/ascii.rs

@@ -5,6 +5,9 @@ use core::ascii::EscapeDefault;
 use crate::fmt::{self, Write};
 use crate::{ascii, iter, mem, ops};
 
+#[cfg(kani)]
+use crate::kani;
+
 #[cfg(not(test))]
 impl [u8] {
     /// Checks if all bytes in this slice are within the ASCII range.
@@ -398,6 +401,10 @@ const fn is_ascii(s: &[u8]) -> bool {
     // Read subsequent words until the last aligned word, excluding the last
     // aligned word by itself to be done in tail check later, to ensure that
     // tail is always one `usize` at most to extra branch `byte_pos == len`.
+    #[safety::loop_invariant(byte_pos <= len 
+                            && byte_pos >= offset_to_aligned
+                            && word_ptr as usize >= start as usize + offset_to_aligned
+                            && (byte_pos - offset_to_aligned) == (word_ptr as usize - start as usize - offset_to_aligned))]
     while byte_pos < len - USIZE_SIZE {
         // Sanity check that the read is in bounds
         debug_assert!(byte_pos + USIZE_SIZE <= len);
@@ -432,3 +439,28 @@ const fn is_ascii(s: &[u8]) -> bool {
 
     !contains_nonascii(last_word)
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use super::*;
+
+    #[kani::proof]
+    #[kani::unwind(8)]
+    pub fn check_is_ascii() {
+        if kani::any() {
+            // 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);
+            is_ascii(xs);
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const u8;
+            kani::assume(ptr.is_aligned());
+            unsafe{
+                assert_eq!(is_ascii(crate::slice::from_raw_parts(ptr, 0)), true);
+            }
+        }
+    }
+}

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"