Add loop contracts and harness for Slice::partition_dedup_by

Author: qinheping

library/core/src/lib.rs

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

library/core/src/slice/mod.rs

@@ -15,6 +15,11 @@ use crate::simd::{self, Simd};
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{fmt, hint, ptr, slice};
 
+use safety::{requires, ensures};
+
+#[cfg(kani)]
+use crate::kani;
+
 #[unstable(
     feature = "slice_internals",
     issue = "none",
@@ -3362,6 +3367,7 @@ impl<T> [T] {
         // thus `next_read > next_write - 1` is too.
         unsafe {
             // Avoid bounds checks by using raw pointers.
+            #[cfg_attr(kani, kani::loop_invariant(next_read <= len && next_read >= next_write && next_write >= 1))]
             while next_read < len {
                 let ptr_read = ptr.add(next_read);
                 let prev_ptr_write = ptr.add(next_write - 1);
@@ -4912,3 +4918,38 @@ impl<const N: usize> fmt::Display for GetManyMutError<N> {
         fmt::Display::fmt("an index is out of bounds or appeared multiple times in the array", f)
     }
 }
+
+#[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)
+    }
+
+    #[kani::proof]
+    pub fn check_partition_dedup_by() {
+        const ARR_SIZE: usize = 1000;
+        let mut x: [u8; ARR_SIZE] = kani::any();
+        let xs = any_slice_of_array_mut(&mut x);
+        unsafe {
+            xs.partition_dedup_by(|a, b| a == 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