Deprecate any_slice (#2789)

Deprecate kani::slice::any_slice in Kani 0.38.0 (and the related AnySlice struct), and remove it in a later version.

Motivation: The Kani library's `slice::any_slice` API is doing more harm than benefit: it is meant to provide a convenient way for users to generate non-deterministic slices, but its current implementation aims to avoid any unsoundness by making sure that for the non-deterministic slice returned by the API, accessing memory beyond the slice length is flagged as an out-of-bounds access (see #1009 for details). However, in practical scenarios, using it ends up causing memory to blowup for CBMC. Given that users may not care about this type of unsoundness, which is only possible through using a pointer dereference inside an unsafe block (see discussion in #2634). Thus, we should leave it to the user to decide the suitable method for generating slices that fits their verification needs. For example, they can use Kani's alternative API, `any_slice_of_array` that extracts a slice of a non-deterministic start and end from a given array.

library/kani/src/slice.rs

@@ -47,12 +47,17 @@ fn any_range<const LENGTH: usize>() -> (usize, usize) {
 /// let slice: kani::slice::AnySlice<u8, 5> = kani::slice::any_slice();
 /// foo(&slice); // where foo is a function that takes a slice and verifies a property about it
 /// ```
+#[deprecated(
+    since = "0.38.0",
+    note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead"
+)]
 pub struct AnySlice<T, const MAX_SLICE_LENGTH: usize> {
     layout: Layout,
     ptr: *mut T,
     slice_len: usize,
 }
 
+#[allow(deprecated)]
 impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
     fn new() -> Self
     where
@@ -103,6 +108,7 @@ impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
     }
 }
 
+#[allow(deprecated)]
 impl<T, const MAX_SLICE_LENGTH: usize> Drop for AnySlice<T, MAX_SLICE_LENGTH> {
     fn drop(&mut self) {
         if self.slice_len > 0 {
@@ -114,6 +120,7 @@ impl<T, const MAX_SLICE_LENGTH: usize> Drop for AnySlice<T, MAX_SLICE_LENGTH> {
     }
 }
 
+#[allow(deprecated)]
 impl<T, const MAX_SLICE_LENGTH: usize> Deref for AnySlice<T, MAX_SLICE_LENGTH> {
     type Target = [T];
 
@@ -122,15 +129,22 @@ impl<T, const MAX_SLICE_LENGTH: usize> Deref for AnySlice<T, MAX_SLICE_LENGTH> {
     }
 }
 
+#[allow(deprecated)]
 impl<T, const MAX_SLICE_LENGTH: usize> DerefMut for AnySlice<T, MAX_SLICE_LENGTH> {
     fn deref_mut(&mut self) -> &mut Self::Target {
         self.get_slice_mut()
     }
 }
 
+#[deprecated(
+    since = "0.38.0",
+    note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead"
+)]
+#[allow(deprecated)]
 pub fn any_slice<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH>
 where
     T: Arbitrary,
 {
+    #[allow(deprecated)]
     AnySlice::<T, MAX_SLICE_LENGTH>::new()
 }

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

@@ -2,11 +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
+// created using `kani::slice::any_slice_of_array`
 
 #[kani::proof]
 fn check_out_of_bounds() {
-    let bytes = kani::slice::any_slice::<i32, 8>();
-    let val = unsafe { *bytes.get_slice().as_ptr().offset(1) };
+    let arr: [i32; 8] = kani::any();
+    let bytes = kani::slice::any_slice_of_array(&arr);
+    let val = unsafe { *bytes.as_ptr().offset(1) };
     assert_eq!(val - val, 0);
 }

tests/expected/nondet-slice-len/expected

@@ -1,5 +1,14 @@
-Failed Checks: assertion failed: s.len() != 0
-Failed Checks: assertion failed: s.len() != 1
-Failed Checks: assertion failed: s.len() != 2
-Failed Checks: assertion failed: s.len() != 3
-Failed Checks: assertion failed: s.len() != 4
+Status: SATISFIED\
+Description: "cover condition: s.len() == 0"
+
+Status: SATISFIED\
+Description: "cover condition: s.len() == 1"
+
+Status: SATISFIED\
+Description: "cover condition: s.len() == 2"
+
+Status: SATISFIED\
+Description: "cover condition: s.len() == 3"
+
+Status: SATISFIED\
+Description: "cover condition: s.len() == 4"

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

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

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

@@ -2,12 +2,13 @@
 // 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
+// created using `kani::slice::any_slice_of_array`
 
 #[kani::proof]
 fn check_out_of_bounds() {
-    let mut bytes = kani::slice::any_slice::<u8, 5>();
-    let val = unsafe { *bytes.get_slice().as_ptr().add(4) };
+    let arr: [u8; 5] = kani::any();
+    let mut bytes = kani::slice::any_slice_of_array(&arr);
+    let val = unsafe { *bytes.as_ptr().add(4) };
     kani::assume(val != 0);
     assert_ne!(val, 0);
 }

tests/kani/NondetSlices/test2.rs

@@ -9,7 +9,8 @@ fn check(s: &[u8]) {
 
 #[kani::proof]
 fn main() {
-    // returns a slice of length between 0 and 5 with non-det content
-    let slice: kani::slice::AnySlice<u8, 5> = kani::slice::any_slice();
+    let arr: [u8; 5] = kani::any();
+    // returns a slice of length between 0 and 5
+    let slice = kani::slice::any_slice_of_array(&arr);
     check(&slice);
 }

tests/kani/NondetSlices/test3.rs

@@ -1,13 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This test uses kani::slice::any_slice of i32
+// This test uses `kani::slice::any_slice_of_array` with `i32`
 
 // kani-flags: --default-unwind 6
 
 #[kani::proof]
 fn check_any_slice_i32() {
-    let s = kani::slice::any_slice::<i32, 5>();
+    let a: [i32; 5] = kani::any();
+    let s = kani::slice::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/ui/any-slice-deprecated/expected

@@ -0,0 +1,2 @@
+warning: use of deprecated function `kani::slice::any_slice`: Use `any_slice_of_array` or `any_slice_of_array_mut` instead
+warning: use of deprecated struct `kani::slice::AnySlice`: Use `any_slice_of_array` or `any_slice_of_array_mut` instead

tests/ui/any-slice-deprecated/test.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A test that checks that Kani emits the deprecated message for `any_slice`
+//! and `AnySlice`
+
+#[kani::proof]
+fn check_any_slice_deprecated() {
+    let _s: kani::slice::AnySlice<i32, 5> = kani::slice::any_slice();
+}