Make the harness running in CI

model-checking · Oct 24, 2024 · 365d85c · 365d85c
1 parent 1422f9d
commit 365d85c
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 9 deletions.
diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
@@ -1887,7 +1887,7 @@ fn simd_contains(needle: &str, haystack: &str) -> Option<bool> {
 /// # Safety
 ///
 /// Both slices must have the same length.
-#[cfg(all(target_arch = "x86_64", target_feature = "sse2"))] // only called on x86
+#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] // only called on x86
 #[inline]
 #[requires(x.len() == y.len())]
 unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
@@ -1958,17 +1958,13 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
 pub mod verify {
     use super::*;
 
+    // Copied from https://github.com/model-checking/kani/blob/main/library/kani/src/slice.rs
+    // should be removed when these functions are moved to `kani_core`
     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();
@@ -1977,14 +1973,16 @@ pub mod verify {
         (from, to)
     }
 
-    #[cfg(all(target_arch = "x86_64", target_feature = "sse2"))] // only called on x86
+    #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
     #[kani::proof]
+    #[kani::unwind(4)]
     pub fn check_small_slice_eq() {
         const ARR_SIZE: usize = 1000;
         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);
+        kani::assume(xs.len() == ys.len());
         unsafe {
             small_slice_eq(xs, ys);
         }

diff --git 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 -Z loop-contracts
+$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 --enable-unstable --cbmc-args --object-bits 8
 
 echo "Tests completed."
 echo