From 1422f9d2504a897605916b11d9d29a9ebf7d42e1 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Tue, 22 Oct 2024 02:18:59 -0500
Subject: [PATCH] Update the script

---
 library/core/src/lib.rs         |  1 +
 library/core/src/str/pattern.rs | 37 +++++++++++++++++++++++++++++----
 scripts/check_kani.sh           |  2 +-
 3 files changed, 35 insertions(+), 5 deletions(-)

diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs
index 402c1e05b4400..7873a2a44c679 100644
--- a/library/core/src/lib.rs
+++ b/library/core/src/lib.rs
@@ -263,6 +263,7 @@
 #![feature(tbm_target_feature)]
 #![feature(wasm_target_feature)]
 #![feature(x86_amx_intrinsics)]
+#![cfg_attr(kani, feature(proc_macro_hygiene))]
 // tidy-alphabetical-end
 
 // allow using `core::` in intra-doc links
diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index 38943f6395ab9..4c4a220464107 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -43,8 +43,12 @@ use crate::convert::TryInto as _;
 use crate::slice::memchr;
 use crate::{cmp, fmt};
 
+use safety::{requires, ensures};
+
 #[cfg(kani)]
 use crate::kani;
+#[cfg(kani)]
+use crate::kani::mem::same_allocation;
 
 // Pattern
 
@@ -1885,6 +1889,7 @@ fn simd_contains(needle: &str, haystack: &str) -> Option<bool> {
 /// Both slices must have the same length.
 #[cfg(all(target_arch = "x86_64", target_feature = "sse2"))] // only called on x86
 #[inline]
+#[requires(x.len() == y.len())]
 unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
     debug_assert_eq!(x.len(), y.len());
     // This function is adapted from
@@ -1951,13 +1956,37 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
 pub mod verify {
+    use super::*;
+
+    pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
+        let (from, to) = any_range::<LENGTH>();
+        &arr[from..to]
+    }
+
+    /// A mutable version of the previous function
+    pub fn any_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
+        let (from, to) = any_range::<LENGTH>();
+        &mut arr[from..to]
+    }
+
+    fn any_range<const LENGTH: usize>() -> (usize, usize) {
+        let from: usize = kani::any();
+        let to: usize = kani::any();
+        kani::assume(to <= LENGTH);
+        kani::assume(from <= to);
+        (from, to)
+    }
+
     #[cfg(all(target_arch = "x86_64", target_feature = "sse2"))] // only called on x86
     #[kani::proof]
     pub fn check_small_slice_eq() {
-        let _ = Box::new(0);
         const ARR_SIZE: usize = 1000;
-        let x: [i32; ARR_SIZE] = kani::any();
-        let y: [i32; ARR_SIZE] = kani::any();
-        small_slice_eq(x, y);
+        let x: [u8; ARR_SIZE] = kani::any();
+        let y: [u8; ARR_SIZE] = kani::any();
+        let xs = any_slice_of_array(&x);
+        let ys = any_slice_of_array(&y);
+        unsafe {
+            small_slice_eq(xs, ys);
+        }
     }
 }
diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh
index c93499cb7a398..b4dbc82fa9597 100644
--- a/scripts/check_kani.sh
+++ b/scripts/check_kani.sh
@@ -44,7 +44,7 @@ cargo build-dev --release
 echo "Running tests..."
 echo
 cd "$VERIFY_RUST_STD_DIR"
-$KANI_DIR/scripts/kani verify-std -Z unstable-options $VERIFY_RUST_STD_DIR/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates
+$KANI_DIR/scripts/kani verify-std -Z unstable-options $VERIFY_RUST_STD_DIR/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates -Z loop-contracts
 
 echo "Tests completed."
 echo