Add missing functionalities to kani_core (model-checking#3384)

  - Add Arbitrary for array
  - Add Arbitrary for tuples
  - Add missing changes from modifies slices (model-checking#3295)

Note that for adding `any_array` I had to cleanup the unnecessary usage
of constant parameters from `kani::any_raw`.

library/kani/src/arbitrary.rs

@@ -16,12 +16,7 @@ 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]>()]:,
-    {
+    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
         [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
     }
 }
@@ -33,20 +28,10 @@ macro_rules! trivial_arbitrary {
             #[inline(always)]
             fn any() -> Self {
                 // 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>() }>() }
+                unsafe { crate::any_raw_internal::<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]>() },
-                    >()
-                }
+            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
+                unsafe { crate::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() }
             }
         }
     };
@@ -128,7 +113,6 @@ 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 {
         T::any_array()

library/kani/src/concrete_playback.rs

@@ -47,19 +47,17 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
 /// # Safety
 ///
 /// The semantics of this function require that SIZE_T equals the size of type T.
-pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
+    let sz = size_of::<T>();
     let mut next_concrete_val: Vec<u8> = Vec::new();
     CONCRETE_VALS.with(|glob_concrete_vals| {
         let mut_ref_glob_concrete_vals = &mut *glob_concrete_vals.borrow_mut();
-        next_concrete_val = if SIZE_T > 0 {
+        next_concrete_val = if sz > 0 {
             mut_ref_glob_concrete_vals.pop().expect("Not enough det vals found")
         } else {
             vec![]
         };
     });
-    let next_concrete_val_len = next_concrete_val.len();
-    let bytes_t: [u8; SIZE_T] = next_concrete_val.try_into().expect(&format!(
-        "Expected {SIZE_T} bytes instead of {next_concrete_val_len} bytes in the following det vals vec"
-    ));
-    std::mem::transmute_copy::<[u8; SIZE_T], T>(&bytes_t)
+    assert_eq!(next_concrete_val.len(), sz, "Expected {sz} bytes in the following det vals vec");
+    unsafe { *(next_concrete_val.as_ptr() as *mut T) }
 }

library/kani/src/lib.rs

@@ -7,11 +7,10 @@
 // Used for rustc_diagnostic_item.
 // Note: We could use a kanitool attribute instead.
 #![feature(rustc_attrs)]
-// This is required for the optimized version of `any_array()`
-#![feature(generic_const_exprs)]
-#![allow(incomplete_features)]
 // Used to model simd.
 #![feature(repr_simd)]
+#![feature(generic_const_exprs)]
+#![allow(incomplete_features)]
 // Features used for tests only.
 #![cfg_attr(test, feature(core_intrinsics, portable_simd))]
 // Required for `rustc_diagnostic_item` and `core_intrinsics`
@@ -21,6 +20,9 @@
 #![feature(f16)]
 #![feature(f128)]
 
+// Allow us to use `kani::` to access crate features.
+extern crate self as kani;
+
 pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]
 mod concrete_playback;
@@ -48,6 +50,7 @@ pub use invariant::Invariant;
 pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
     unreachable!("Concrete playback does not work during verification")
 }
+
 pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin};
 
 /// Creates an assumption that will be valid after this statement run. Note that the assumption
@@ -246,21 +249,21 @@ pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
 /// Note that SIZE_T must be equal the size of type T in bytes.
 #[inline(never)]
 #[cfg(not(feature = "concrete_playback"))]
-pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
     any_raw_inner::<T>()
 }
 
 #[inline(never)]
 #[cfg(feature = "concrete_playback")]
-pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
-    concrete_playback::any_raw_internal::<T, SIZE_T>()
+pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
+    concrete_playback::any_raw_internal::<T>()
 }
 
 /// This low-level function returns nondet bytes of size T.
 #[rustc_diagnostic_item = "KaniAnyRaw"]
 #[inline(never)]
 #[allow(dead_code)]
-fn any_raw_inner<T>() -> T {
+fn any_raw_inner<T: Copy>() -> T {
     kani_intrinsic()
 }
 

library/kani/src/vec.rs

@@ -6,7 +6,6 @@ use crate::{any, any_where, Arbitrary};
 pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
 where
     T: Arbitrary,
-    [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:,
 {
     let real_length: usize = any_where(|sz| *sz <= MAX_LENGTH);
     match real_length {
@@ -26,7 +25,6 @@ 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)

library/kani_core/src/arbitrary.rs

@@ -8,6 +8,7 @@
 //!
 //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.
 #[macro_export]
+#[allow(clippy::crate_in_macro_def)]
 macro_rules! generate_arbitrary {
     ($core:path) => {
         use core_path::marker::{PhantomData, PhantomPinned};
@@ -18,13 +19,7 @@ macro_rules! generate_arbitrary {
             Self: Sized,
         {
             fn any() -> Self;
-            #[cfg(kani_sysroot)]
-            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
-                [(); core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:,
-            {
+            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
                 [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
             }
         }
@@ -36,22 +31,10 @@ macro_rules! generate_arbitrary {
                     #[inline(always)]
                     fn any() -> Self {
                         // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.
-                        unsafe { any_raw_internal::<Self, { core_path::mem::size_of::<Self>() }>() }
+                        unsafe { crate::kani::any_raw_internal::<Self>() }
                     }
-                    // Disable this for standard library since we cannot enable generic constant expr.
-                    #[cfg(kani_sysroot)]
-                    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.
-                        [(); { core_path::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:,
-                    {
-                        unsafe {
-                            any_raw_internal::<
-                                [Self; MAX_ARRAY_LENGTH],
-                                { core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() },
-                            >()
-                        }
+                    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
+                        unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() }
                     }
                 }
             };
@@ -134,6 +117,15 @@ macro_rules! generate_arbitrary {
             }
         }
 
+        impl<T, const N: usize> Arbitrary for [T; N]
+        where
+            T: Arbitrary,
+        {
+            fn any() -> Self {
+                T::any_array::<N>()
+            }
+        }
+
         impl<T> Arbitrary for Option<T>
         where
             T: Arbitrary,
@@ -165,15 +157,33 @@ macro_rules! generate_arbitrary {
             }
         }
 
-        #[cfg(kani_sysroot)]
-        impl<T, const N: usize> Arbitrary for [T; N]
-        where
-            T: Arbitrary,
-            [(); core_path::mem::size_of::<[T; N]>()]:,
-        {
+        arbitrary_tuple!(A);
+        arbitrary_tuple!(A, B);
+        arbitrary_tuple!(A, B, C);
+        arbitrary_tuple!(A, B, C, D);
+        arbitrary_tuple!(A, B, C, D, E);
+        arbitrary_tuple!(A, B, C, D, E, F);
+        arbitrary_tuple!(A, B, C, D, E, F, G);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K, L);
+    };
+}
+
+/// This macro implements `kani::Arbitrary` on a tuple whose elements
+/// already implement `kani::Arbitrary` by running `kani::any()` on
+/// each index of the tuple.
+#[allow(clippy::crate_in_macro_def)]
+#[macro_export]
+macro_rules! arbitrary_tuple {
+    ($($type:ident),*) => {
+        impl<$($type : Arbitrary),*>  Arbitrary for ($($type,)*) {
+            #[inline(always)]
             fn any() -> Self {
-                T::any_array()
+                ($(crate::kani::any::<$type>(),)*)
             }
         }
-    };
+    }
 }