Implement BoundedArbitrary for boxed slices

library/kani/src/bounded_arbitrary.rs

@@ -5,6 +5,22 @@
 
 use kani::{Arbitrary, BoundedArbitrary};
 
+impl<T: Arbitrary> BoundedArbitrary for Box<[T]> {
+    fn bounded_any<const N: usize>() -> Self {
+        let len: usize = kani::any_where(|l| *l <= N);
+        // The following is equivalent to:
+        // ```
+        // (0..len).map(|_| T::any()).collect()
+        // ```
+        // but leads to more efficient verification
+        let mut b = Box::<[T]>::new_uninit_slice(len);
+        for i in 0..len {
+            b[i] = std::mem::MaybeUninit::new(T::any());
+        }
+        unsafe { b.assume_init() }
+    }
+}
+
 // This implementation overlaps with `kani::any_vec` in `kani/library/kani/src/vec.rs`.
 // This issue `https://github.com/model-checking/kani/issues/4027` tracks deprecating
 // `kani::any_vec` in favor of this implementation.

tests/expected/derive-bounded-arbitrary/boxed_slice.expected

@@ -0,0 +1,5 @@
+Checking harness check_my_boxed_array...
+
+ ** 6 of 6 cover properties satisfied
+
+VERIFICATION:- SUCCESSFUL

tests/expected/derive-bounded-arbitrary/boxed_slice.rs

@@ -0,0 +1,37 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that derive BoundedArbitrary macro works on boxed slices, e.g. `Box<[u16]>`
+
+extern crate kani;
+use kani::BoundedArbitrary;
+
+#[derive(BoundedArbitrary)]
+#[allow(unused)]
+struct StructWithBoxedSlice {
+    x: i32,
+    #[bounded]
+    a: Box<[u16]>,
+}
+
+fn first(s: &[u16]) -> Option<u16> {
+    if s.len() > 0 { Some(s[0]) } else { None }
+}
+
+fn tenth(s: &[u16]) -> Option<u16> {
+    if s.len() >= 10 { Some(s[9]) } else { None }
+}
+
+#[kani::proof]
+#[kani::unwind(11)]
+fn check_my_boxed_array() {
+    let swbs: StructWithBoxedSlice = kani::bounded_any::<_, 10>();
+    let f = first(&swbs.a);
+    kani::cover!(f.is_none());
+    kani::cover!(f == Some(1));
+    kani::cover!(f == Some(42));
+    let t = tenth(&swbs.a);
+    kani::cover!(t.is_none());
+    kani::cover!(t == Some(15));
+    kani::cover!(t == Some(987));
+}