diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 04f84821660f..c2b445b5899f 100644 --- a/kani-driver/src/args/mod.rs +++ b/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, /// 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, @@ -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] diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs index aa6cd7e4018d..0de51862b7d8 100644 --- a/library/kani/src/concrete_playback.rs +++ b/library/kani/src/concrete_playback.rs @@ -40,6 +40,11 @@ pub fn concrete_playback_run(mut local_concrete_vals: Vec>, pro }); } +/// Iterate over `any_raw_internal` since CBMC produces assignment per element. +pub(crate) unsafe fn any_raw_array() -> [T; N] { + [(); N].map(|_| crate::any_raw_internal::()) +} + /// 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. diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index b0a190f89cf2..046c6e7a0667 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -249,26 +249,19 @@ pub fn any_where 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 { +unsafe fn any_raw_internal() -> T { any_raw::() } /// 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; N] { +unsafe fn any_raw_array() -> [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; N] { - [(); N].map(|_| any_raw_internal::()) -} +use concrete_playback::{any_raw_array, any_raw_internal}; /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 7cfb649b11a0..ab5213af9b6c 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -34,7 +34,7 @@ macro_rules! generate_arbitrary { unsafe { crate::kani::any_raw_internal::() } } fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } + unsafe { crate::kani::any_raw_aray::<[Self; MAX_ARRAY_LENGTH]>() } } } }; diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 016c805e8f8e..9baba1abe886 100644 --- a/library/kani_core/src/lib.rs +++ b/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 { - any_raw_inner::() + unsafe fn any_raw_internal() -> T { + any_raw::() } + /// 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 { - concrete_playback::any_raw_internal::() + #[cfg(not(feature = "concrete_playback"))] + unsafe fn any_raw_array() -> [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 { + fn any_raw() -> T { kani_intrinsic() } diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 91454c4b65e7..3a24bf15241e 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/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 {