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 {