Fix unit tests and apply changes to kani_core

kani-driver/src/args/mod.rs

@@ -137,10 +137,10 @@ pub struct VerificationArgs {
  /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code.
  /// This option does not work with `--output-format old`.
  #[arg(
- long,
- conflicts_with_all(& ["visualize"]),
- ignore_case = true,
- value_enum
+  long,
+  conflicts_with_all(& ["visualize"]),
+  ignore_case = true,
+  value_enum
  )]
  pub concrete_playback: Option<ConcretePlaybackMode>,
  /// Keep temporary files generated throughout Kani process. This is already the default
@@ -210,10 +210,10 @@ pub struct VerificationArgs {
  /// Pass through directly to CBMC; must be the last flag.
  /// This feature is unstable and it requires `--enable_unstable` to be used
  #[arg(
- long,
- allow_hyphen_values = true,
- requires("enable_unstable"),
- num_args(0..)
+  long,
+  allow_hyphen_values = true,
+  requires("enable_unstable"),
+  num_args(0..)
  )]
  // consumes everything
  pub cbmc_args: Vec<OsString>,
@@ -870,13 +870,13 @@ mod tests {
  let res = parse_unstable_disabled("--harness foo -Z stubbing").unwrap();
  assert!(res.verify_opts.is_stubbing_enabled());
 
- // `-Z stubbing` cannot be called with `--concrete-playback`
+ // `-Z stubbing` can now be called with concrete playback.
  let res = parse_unstable_disabled(
  "--harness foo --concrete-playback=print -Z concrete-playback -Z stubbing",
  )
  .unwrap();
- let err = res.validate().unwrap_err();
- assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
+ // Note that `res.validate()` fails because input file does not exist.
+ assert!(matches!(res.verify_opts.validate(), Ok(())));
  }
 
  #[test]

library/kani/src/concrete_playback.rs

@@ -40,6 +40,11 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
  });
 }
 
+/// Iterate over `any_raw_internal` since CBMC produces assignment per element.
+pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+ [(); N].map(|_| crate::any_raw_internal::<T>())
+}
+
 /// Concrete playback implementation of
 /// kani::any_raw_internal. Because CBMC does not bother putting in
 /// Zero-Sized Types, those are defaulted to an empty vector.

library/kani/src/lib.rs

@@ -249,26 +249,19 @@ 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: Copy>() -> T {
+unsafe fn any_raw_internal<T: Copy>() -> T {
  any_raw::<T>()
 }
 
 /// This is the same as [any_raw_internal] for verification flow, but not for concrete playback.
 #[inline(never)]
 #[cfg(not(feature = "concrete_playback"))]
-pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
  any_raw::<[T; N]>()
 }
 
 #[cfg(feature = "concrete_playback")]
-use concrete_playback::any_raw_internal;
-
-/// Iterate over `any_raw_internal` since CBMC produces assignment per element.
-#[inline(never)]
-#[cfg(feature = "concrete_playback")]
-pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
- [(); N].map(|_| any_raw_internal::<T>())
-}
+use concrete_playback::{any_raw_array, any_raw_internal};
 
 /// This low-level function returns nondet bytes of size T.
 #[rustc_diagnostic_item = "KaniAnyRaw"]

library/kani_core/src/arbitrary.rs

@@ -34,7 +34,7 @@ macro_rules! generate_arbitrary {
  unsafe { crate::kani::any_raw_internal::<Self>() }
  }
  fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
- unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() }
+ unsafe { crate::kani::any_raw_aray::<[Self; MAX_ARRAY_LENGTH]>() }
  }
  }
  };

library/kani_core/src/lib.rs

@@ -248,21 +248,25 @@ macro_rules! kani_intrinsics {
  /// 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: Copy>() -> T {
- any_raw_inner::<T>()
+ unsafe fn any_raw_internal<T: Copy>() -> T {
+ any_raw::<T>()
  }
 
+ /// This is the same as [any_raw_internal] for verification flow, but not for concrete playback.
  #[inline(never)]
- #[cfg(feature = "concrete_playback")]
- pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
- concrete_playback::any_raw_internal::<T>()
+ #[cfg(not(feature = "concrete_playback"))]
+ unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+ any_raw::<[T; N]>()
  }
 
+ #[cfg(feature = "concrete_playback")]
+ use concrete_playback::{any_raw_array, any_raw_internal};
+
  /// This low-level function returns nondet bytes of size T.
  #[rustc_diagnostic_item = "KaniAnyRaw"]
  #[inline(never)]
  #[allow(dead_code)]
- pub fn any_raw_inner<T: Copy>() -> T {
+ fn any_raw<T: Copy>() -> T {
  kani_intrinsic()
  }
 

tests/script-based-pre/verify_std_cmd/verify_std.sh

@@ -29,7 +29,7 @@ mod verify {
  use core::kani;
  #[kani::proof]
  fn check_non_zero() {
- let orig: u32 = kani::any_raw_inner();
+ let orig: u32 = kani::any();
  if let Some(val) = core::num::NonZeroU32::new(orig) {
  assert!(orig == val.into());
  } else {