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,11 @@ macro_rules! generate_arbitrary {
         mod arbitrary_ptr {
             kani_core::ptr_generator!();
         }
+
+        pub use self::arbitrary_slice::*;
+        mod arbitrary_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::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)
+        }
+    };
+}

library/kani_core/src/lib.rs

@@ -146,7 +146,7 @@ macro_rules! kani_intrinsics {
         /// # use crate::kani;
         /// #
         /// # let array: [u8; 10]  = kani::any();
-        /// # let slice = kani::slice::any_slice_of_array(&array);
+        /// # let slice = kani::any_slice_of_array(&array);
         /// kani::cover(slice.len() == 0, "The slice may have a length of 0");
         /// ```
         ///

tests/expected/nondet-slice-i32-oob/main.rs

@@ -2,12 +2,12 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // This test checks that Kani reports out-of-bound accesses on a non-det slice
-// created using `kani::slice::any_slice_of_array`
+// created using `kani::any_slice_of_array`
 
 #[kani::proof]
 fn check_out_of_bounds() {
     let arr: [i32; 8] = kani::any();
-    let bytes = kani::slice::any_slice_of_array(&arr);
+    let bytes = kani::any_slice_of_array(&arr);
     let val = unsafe { *bytes.as_ptr().offset(1) };
     assert_eq!(val - val, 0);
 }

tests/expected/nondet-slice-len/main.rs

@@ -1,13 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This test checks that non-det slices created using `kani::slice::any_slice_of_array`
+// This test checks that non-det slices created using `kani::any_slice_of_array`
 // assume any length up the specified maximum
 
 #[kani::proof]
 fn check_possible_slice_lengths() {
     let arr: [i32; 4] = kani::any();
-    let s = kani::slice::any_slice_of_array(&arr);
+    let s = kani::any_slice_of_array(&arr);
     kani::cover!(s.len() == 0);
     kani::cover!(s.len() == 1);
     kani::cover!(s.len() == 2);

tests/expected/nondet-slice-u8-oob/main.rs

@@ -2,12 +2,12 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // This test checks that Kani reports out-of-bound accesses on a non-det slice
-// created using `kani::slice::any_slice_of_array`
+// created using `kani::any_slice_of_array`
 
 #[kani::proof]
 fn check_out_of_bounds() {
     let arr: [u8; 5] = kani::any();
-    let mut bytes = kani::slice::any_slice_of_array(&arr);
+    let mut bytes = kani::any_slice_of_array(&arr);
     let val = unsafe { *bytes.as_ptr().add(4) };
     kani::assume(val != 0);
     assert_ne!(val, 0);

tests/kani/NondetSlices/test1.rs

@@ -20,6 +20,6 @@ fn main() {
     let arr = [1, 2, 3];
     // The slice returned can be any of the following:
     // {[], [1], [2], [3], [1, 2], [2, 3], [1, 2, 3]}
-    let slice = kani::slice::any_slice_of_array(&arr);
+    let slice = kani::any_slice_of_array(&arr);
     check(slice);
 }

tests/kani/NondetSlices/test2.rs

@@ -11,6 +11,6 @@ fn check(s: &[u8]) {
 fn main() {
     let arr: [u8; 5] = kani::any();
     // returns a slice of length between 0 and 5
-    let slice = kani::slice::any_slice_of_array(&arr);
+    let slice = kani::any_slice_of_array(&arr);
     check(&slice);
 }

tests/kani/NondetSlices/test3.rs

@@ -1,14 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This test uses `kani::slice::any_slice_of_array` with `i32`
+// This test uses `kani::any_slice_of_array` with `i32`
 
 // kani-flags: --default-unwind 6
 
 #[kani::proof]
 fn check_any_slice_i32() {
     let a: [i32; 5] = kani::any();
-    let s = kani::slice::any_slice_of_array(&a);
+    let s = kani::any_slice_of_array(&a);
     s.iter().for_each(|x| kani::assume(*x < 10 && *x > -20));
     let sum = s.iter().fold(0, |acc, x| acc + x);
     assert!(sum <= 45); // 9 * 5

tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs

@@ -20,7 +20,7 @@ pub mod slices_check {
     #[kani::stub(<[MyStruct]>::len, stub_len_is_10)]
     pub fn check_stub_len_is_10() {
         let input: [MyStruct; 5] = kani::any();
-        let slice = kani::slice::any_slice_of_array(&input);
+        let slice = kani::any_slice_of_array(&input);
         assert_eq!(slice.len(), 10);
     }
 }