Create Arbitrary::any_array()

library/kani/src/arbitrary.rs

@@ -3,15 +3,27 @@
 
 //! This module introduces the Arbitrary trait as well as implementation for primitive types and
 //! other std containers.
+
 use std::{
     marker::{PhantomData, PhantomPinned},
     num::*,
 };
 
 /// This trait should be used to generate symbolic variables that represent any valid value of
 /// its type.
-pub trait Arbitrary {
+pub trait Arbitrary
+where
+    Self: Sized,
+{
     fn any() -> Self;
+    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
+    // the requirement defined in the where clause must appear on the `impl`'s method `any_array`
+    // but also on the corresponding trait's method
+    where
+        [(); std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:,
+    {
+        [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
+    }
 }
 
 /// The given type can be represented by an unconstrained symbolic value of size_of::<T>.
@@ -20,8 +32,21 @@ macro_rules! trivial_arbitrary {
         impl Arbitrary for $type {
             #[inline(always)]
             fn any() -> Self {
-                // This size_of call does not use generic_const_exprs feature. It's inside a macro, and $type isn't generic.
-                unsafe { crate::any_raw_internal::<$type, { std::mem::size_of::<$type>() }>() }
+                // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.
+                unsafe { crate::any_raw_internal::<Self, { std::mem::size_of::<Self>() }>() }
+            }
+            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
+            where
+                // `generic_const_exprs` requires all potential errors to be reflected in the signature/header.
+                // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail.
+                [(); { std::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:,
+            {
+                unsafe {
+                    crate::any_raw_internal::<
+                        [Self; MAX_ARRAY_LENGTH],
+                        { std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() },
+                    >()
+                }
             }
         }
     };
@@ -99,9 +124,10 @@ nonzero_arbitrary!(NonZeroIsize, isize);
 impl<T, const N: usize> Arbitrary for [T; N]
 where
     T: Arbitrary,
+    [(); std::mem::size_of::<[T; N]>()]:,
 {
     fn any() -> Self {
-        [(); N].map(|_| T::any())
+        T::any_array()
     }
 }
 

library/kani/src/lib.rs

@@ -3,6 +3,9 @@
 
 // Used for rustc_diagnostic_item.
 #![feature(rustc_attrs)]
+// This is required for the optimized version of `any_array()`
+#![feature(generic_const_exprs)]
+#![allow(incomplete_features)]
 
 pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]

library/kani/src/vec.rs

@@ -6,6 +6,7 @@ use crate::{any, assume, Arbitrary};
 pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
 where
     T: Arbitrary,
+    [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:,
 {
     let mut v = exact_vec::<T, MAX_LENGTH>();
     let real_length: usize = any();
@@ -19,6 +20,7 @@ where
 pub fn exact_vec<T, const EXACT_LENGTH: usize>() -> Vec<T>
 where
     T: Arbitrary,
+    [(); std::mem::size_of::<[T; EXACT_LENGTH]>()]:,
 {
     let boxed_array: Box<[T; EXACT_LENGTH]> = Box::new(any());
     <[T]>::into_vec(boxed_array)

tests/expected/object-bits/insufficient/main.rs

@@ -7,6 +7,9 @@
 
 #[kani::proof]
 fn main() {
-    let arr: [i32; 100] = kani::any();
-    assert_eq!(arr[0], arr[99]);
+    let mut arr: [i32; 100] = kani::Arbitrary::any_array();
+    for i in 0..30 {
+        arr[i] = kani::any();
+    }
+    assert!(arr[0] > arr[0] - arr[99]);
 }