Implement BoundedArbitrary for boxed slices

Author: zhassan-aws

library/kani_core/src/bounded_arbitrary.rs

@@ -13,6 +13,22 @@ macro_rules! generate_bounded_arbitrary {
             fn bounded_any<const N: usize>() -> Self;
         }
 
+        impl<T: Arbitrary> BoundedArbitrary for alloc::boxed::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 = alloc::boxed::Box::<[T]>::new_uninit_slice(len);
+                for i in 0..len {
+                    b[i] = MaybeUninit::new(T::any());
+                }
+                unsafe { b.assume_init() }
+            }
+        }
+
         impl<T> BoundedArbitrary for Option<T>
         where
             T: BoundedArbitrary,

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));
+}