Move any_slice_from_array to kani_core

library/kani/src/lib.rs

@@ -29,7 +29,6 @@ mod concrete_playback;
 pub mod futures;
 pub mod invariant;
 pub mod shadow;
-pub mod slice;
 pub mod vec;
 
 mod models;

library/kani_core/src/arbitrary.rs

@@ -9,6 +9,7 @@
 //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.
 
 mod pointer;
+mod slice;
 
 #[macro_export]
 #[allow(clippy::crate_in_macro_def)]
@@ -188,6 +189,10 @@ macro_rules! generate_arbitrary {
         mod arbitrary_ptr {
             kani_core::ptr_generator!();
         }
+
+        pub mod slice {
+            kani_core::slice_generator!();
+        }
     };
 }
 

library/kani_core/src/arbitrary/slice.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This macro generates the logic required to generate slice with arbitrary contents and length.
+#[allow(clippy::crate_in_macro_def)]
+#[macro_export]
+macro_rules! slice_generator {
+    () => {
+        use crate::kani;
+
+        /// Given an array `arr` of length `LENGTH`, this function returns a **valid**
+        /// slice of `arr` with non-deterministic start and end points.  This is useful
+        /// in situations where one wants to verify that all possible slices of a given
+        /// array satisfy some property.
+        ///
+        /// # Example:
+        ///
+        /// ```no_run
+        /// # fn foo(_: &[i32]) {}
+        /// let arr = [1, 2, 3];
+        /// let slice = kani::slice::any_slice_of_array(&arr);
+        /// foo(slice); // where foo is a function that takes a slice and verifies a property about it
+        /// ```
+        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)
+        }
+    };
+}