Add missing functionalities to kani_core (#3384)

  - Add Arbitrary for array
  - Add Arbitrary for tuples
  - Add missing changes from modifies slices (#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>(),)*)
  }
  }
- };
+ }
 }