Add loop contracts and harness for slice::is_ascii (#157)

Author: qinheping

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.addr() >= start.addr() + offset_to_aligned
+                            && byte_pos == word_ptr.addr() - start.addr())]
     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 much larger 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);
+            }
+        }
+    }
+}