From 52fcc6cc747779c31ba41593b0d0777043540264 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Mon, 28 Oct 2024 22:04:30 -0500
Subject: [PATCH] Move any_slice_from_array to kani_core (#3646)

Move `any_slice_from_array` to `kani_core` so that we can call them in
verify-rust-std (an example harness in
https://github.com/model-checking/verify-rust-std/pull/122).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 library/kani/src/lib.rs                  |  1 -
 library/kani/src/slice.rs                | 35 -------------------
 library/kani_core/src/arbitrary.rs       |  5 +++
 library/kani_core/src/arbitrary/slice.rs | 43 ++++++++++++++++++++++++
 4 files changed, 48 insertions(+), 36 deletions(-)
 delete mode 100644 library/kani/src/slice.rs
 create mode 100644 library/kani_core/src/arbitrary/slice.rs

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 053af760067b..75b83fd3bc76 100644
--- a/library/kani/src/lib.rs
+++ b/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;
diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs
deleted file mode 100644
index c419a881fa55..000000000000
--- a/library/kani/src/slice.rs
+++ /dev/null
@@ -1,35 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::{any, assume};
-
-/// 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 = any();
-    let to: usize = any();
-    assume(to <= LENGTH);
-    assume(from <= to);
-    (from, to)
-}
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index 1dc30feca566..90a2ae5e4c82 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/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!();
+        }
     };
 }
 
diff --git a/library/kani_core/src/arbitrary/slice.rs b/library/kani_core/src/arbitrary/slice.rs
new file mode 100644
index 000000000000..5d6841c2f0c7
--- /dev/null
+++ b/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)
+        }
+    };
+}