From b18698f0e01b9d7d678a0ced8c2553a8d56e7767 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 10:58:31 -0700 Subject: [PATCH] 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 | 24 +---- library/kani/src/concrete_playback.rs | 12 +-- library/kani/src/lib.rs | 17 ++-- library/kani/src/vec.rs | 2 - library/kani_core/src/arbitrary.rs | 70 ++++++++------ library/kani_core/src/lib.rs | 93 +++++++++++++------ .../verify_std_cmd/verify_core.rs | 75 +++++++++++++++ .../verify_std_cmd/verify_std.expected | 8 +- .../verify_std_cmd/verify_std.sh | 42 +-------- 9 files changed, 209 insertions(+), 134 deletions(-) create mode 100644 tests/script-based-pre/verify_std_cmd/verify_core.rs diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 424ca2485d57..ef6e2ef23dd4 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -16,12 +16,7 @@ where Self: Sized, { fn any() -> Self; - fn any_array() -> [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() -> [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::() }>() } + unsafe { crate::any_raw_internal::() } } - fn any_array() -> [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() -> [Self; MAX_ARRAY_LENGTH] { + unsafe { crate::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } } } }; @@ -128,7 +113,6 @@ nonzero_arbitrary!(NonZeroIsize, isize); impl Arbitrary for [T; N] where T: Arbitrary, - [(); std::mem::size_of::<[T; N]>()]:, { fn any() -> Self { T::any_array() diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs index 711b9b005624..aa6cd7e4018d 100644 --- a/library/kani/src/concrete_playback.rs +++ b/library/kani/src/concrete_playback.rs @@ -47,19 +47,17 @@ pub fn concrete_playback_run(mut local_concrete_vals: Vec>, 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 { +pub(crate) unsafe fn any_raw_internal() -> T { + let sz = size_of::(); let mut next_concrete_val: Vec = 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) } } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 7487cc26b186..3cf46bd7af07 100644 --- a/library/kani/src/lib.rs +++ b/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(_: Vec>, _: 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 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 { +pub(crate) unsafe fn any_raw_internal() -> T { any_raw_inner::() } #[inline(never)] #[cfg(feature = "concrete_playback")] -pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() +pub(crate) unsafe fn any_raw_internal() -> T { + concrete_playback::any_raw_internal::() } /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] #[inline(never)] #[allow(dead_code)] -fn any_raw_inner() -> T { +fn any_raw_inner() -> T { kani_intrinsic() } diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs index 626d152f02d4..a3ec05a9c953 100644 --- a/library/kani/src/vec.rs +++ b/library/kani/src/vec.rs @@ -6,7 +6,6 @@ use crate::{any, any_where, Arbitrary}; pub fn any_vec() -> Vec 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() -> Vec 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) diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index a8271ad758cf..7cfb649b11a0 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/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() -> [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() -> [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::() }>() } + unsafe { crate::kani::any_raw_internal::() } } - // Disable this for standard library since we cannot enable generic constant expr. - #[cfg(kani_sysroot)] - fn any_array() -> [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() -> [Self; MAX_ARRAY_LENGTH] { + unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } } } }; @@ -134,6 +117,15 @@ macro_rules! generate_arbitrary { } } + impl Arbitrary for [T; N] + where + T: Arbitrary, + { + fn any() -> Self { + T::any_array::() + } + } + impl Arbitrary for Option where T: Arbitrary, @@ -165,15 +157,33 @@ macro_rules! generate_arbitrary { } } - #[cfg(kani_sysroot)] - impl 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>(),)*) } } - }; + } } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index a07ba7ca8ec4..016c805e8f8e 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -60,6 +60,7 @@ macro_rules! kani_lib { /// such as core in rust's std library itself. /// /// TODO: Use this inside kani library so that we dont have to maintain two copies of the same intrinsics. +#[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! kani_intrinsics { ($core:tt) => { @@ -180,7 +181,7 @@ macro_rules! kani_intrinsics { /// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero. /// /// ```rust - /// let inputA = kani::any::(); + /// let inputA = kani::any::(); /// fn_under_verification(inputA); /// ``` /// @@ -247,21 +248,21 @@ 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 { + pub(crate) unsafe fn any_raw_internal() -> T { any_raw_inner::() } #[inline(never)] #[cfg(feature = "concrete_playback")] - pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() + pub(crate) unsafe fn any_raw_internal() -> T { + concrete_playback::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 { + pub fn any_raw_inner() -> T { kani_intrinsic() } @@ -269,7 +270,7 @@ macro_rules! kani_intrinsics { /// supported by Kani display. /// /// During verification this will get replaced by `assert(false)`. For concrete executions, we just - /// invoke the regular `std::panic!()` function. This function is used by our standard library + /// invoke the regular `core::panic!()` function. This function is used by our standard library /// overrides, but not the other way around. #[inline(never)] #[rustc_diagnostic_item = "KaniPanic"] @@ -294,6 +295,8 @@ macro_rules! kani_intrinsics { } pub mod internal { + use crate::kani::Arbitrary; + use core::ptr; /// Helper trait for code generation for `modifies` contracts. /// @@ -301,7 +304,7 @@ macro_rules! kani_intrinsics { #[doc(hidden)] pub trait Pointer<'a> { /// Type of the pointed-to data - type Inner; + type Inner: ?Sized; /// Used for checking assigns contracts where we pass immutable references to the function. /// @@ -309,56 +312,52 @@ macro_rules! kani_intrinsics { /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; - /// used for havocking on replecement of a `modifies` clause. - unsafe fn assignable(self) -> &'a mut Self::Inner; + unsafe fn assignable(self) -> *mut Self::Inner; } - impl<'a, 'b, T> Pointer<'a> for &'b T { + impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - $core::mem::transmute(*self) + core::mem::transmute(*self) } - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self as *const T) + unsafe fn assignable(self) -> *mut Self::Inner { + core::mem::transmute(self as *const T) } } - impl<'a, 'b, T> Pointer<'a> for &'b mut T { + impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { type Inner = T; #[allow(clippy::transmute_ptr_to_ref)] unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - $core::mem::transmute::<_, &&'a T>(self) + core::mem::transmute::<_, &&'a T>(self) } - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + self as *mut T } } - impl<'a, T> Pointer<'a> for *const T { + impl<'a, T: ?Sized> Pointer<'a> for *const T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T } - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + core::mem::transmute(self) } } - impl<'a, T> Pointer<'a> for *mut T { + impl<'a, T: ?Sized> Pointer<'a> for *mut T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T } - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + self } } @@ -391,6 +390,48 @@ macro_rules! kani_intrinsics { pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) } + + /// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. + /// Only for use within function contracts and will not be replaced if the recursive or function stub + /// replace contracts are not used. + #[rustc_diagnostic_item = "KaniWriteAny"] + #[inline(never)] + #[doc(hidden)] + pub unsafe fn write_any(_pointer: *mut T) { + // This function should not be reacheable. + // Users must include `#[kani::recursion]` in any function contracts for recursive functions; + // otherwise, this might not be properly instantiate. We mark this as unreachable to make + // sure Kani doesn't report any false positives. + unreachable!() + } + + /// Fill in a slice with kani::any. + /// Intended as a post compilation replacement for write_any + #[rustc_diagnostic_item = "KaniWriteAnySlice"] + #[inline(always)] + pub unsafe fn write_any_slice(slice: *mut [T]) { + (*slice).fill_with(T::any) + } + + /// Fill in a pointer with kani::any. + /// Intended as a post compilation replacement for write_any + #[rustc_diagnostic_item = "KaniWriteAnySlim"] + #[inline(always)] + pub unsafe fn write_any_slim(pointer: *mut T) { + ptr::write(pointer, T::any()) + } + + /// Fill in a str with kani::any. + /// Intended as a post compilation replacement for write_any. + /// Not yet implemented + #[rustc_diagnostic_item = "KaniWriteAnyStr"] + #[inline(always)] + pub unsafe fn write_any_str(_s: *mut str) { + //TODO: strings introduce new UB + //(*s).as_bytes_mut().fill_with(u8::any) + //TODO: String validation + unimplemented!("Kani does not support creating arbitrary `str`") + } } }; } diff --git a/tests/script-based-pre/verify_std_cmd/verify_core.rs b/tests/script-based-pre/verify_std_cmd/verify_core.rs new file mode 100644 index 000000000000..28cf113a9210 --- /dev/null +++ b/tests/script-based-pre/verify_std_cmd/verify_core.rs @@ -0,0 +1,75 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +/// Dummy code that gets injected into `core` for basic tests for `verify-std` subcommand. +#[cfg(kani)] +kani_core::kani_lib!(core); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use crate::kani; + use core::num::NonZeroU8; + + #[kani::proof] + pub fn harness() { + kani::assert(true, "yay"); + } + + #[kani::proof_for_contract(fake_function)] + fn dummy_proof() { + fake_function(true); + } + + /// Add a `rustc_diagnostic_item` to ensure this works. + /// See for more details. + #[kani::requires(x == true)] + #[rustc_diagnostic_item = "fake_function"] + fn fake_function(x: bool) -> bool { + x + } + + #[kani::proof_for_contract(dummy_read)] + fn check_dummy_read() { + let val: char = kani::any(); + assert_eq!(unsafe { dummy_read(&val) }, val); + } + + /// Ensure we can verify constant functions. + #[kani::requires(kani::mem::can_dereference(ptr))] + #[rustc_diagnostic_item = "dummy_read"] + const unsafe fn dummy_read(ptr: *const T) -> T { + *ptr + } + + #[kani::proof_for_contract(swap_tuple)] + fn check_swap_tuple() { + let initial: (char, NonZeroU8) = kani::any(); + let _swapped = swap_tuple(initial); + } + + #[kani::ensures(| result | result.0 == second && result.1 == first)] + fn swap_tuple((first, second): (char, NonZeroU8)) -> (NonZeroU8, char) { + (second, first) + } + + #[kani::proof_for_contract(add_one)] + fn check_add_one() { + let mut initial: [u32; 4] = kani::any(); + unsafe { add_one(&mut initial) }; + } + + /// Function with a more elaborated contract that uses `old` and `modifies`. + #[kani::modifies(inout)] + #[kani::requires(kani::mem::can_dereference(inout) + && unsafe { inout.as_ref_unchecked().iter().all(| i | * i < u32::MAX) })] + #[kani::requires(kani::mem::can_write(inout))] + #[kani::ensures(| result | { + let (orig, i) = old({ + let i = kani::any_where(| i: & usize | * i < unsafe { inout.len() }); + (unsafe { inout.as_ref_unchecked()[i] }, i)}); + unsafe { inout.as_ref_unchecked()[i] > orig } + })] + unsafe fn add_one(inout: *mut [u32]) { + inout.as_mut_unchecked().iter_mut().for_each(|e| *e += 1) + } +} diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index aa30da375dd3..22e8fb2e6375 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -9,7 +9,13 @@ VERIFICATION:- SUCCESSFUL Checking harness verify::check_dummy_read... VERIFICATION:- SUCCESSFUL +Checking harness verify::check_add_one... +VERIFICATION:- SUCCESSFUL + +Checking harness verify::check_swap_tuple... +VERIFICATION:- SUCCESSFUL + Checking harness num::verify::check_non_zero... VERIFICATION:- SUCCESSFUL -Complete - 4 successfully verified harnesses, 0 failures, 4 total. +Complete - 6 successfully verified harnesses, 0 failures, 6 total. 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 3253ad29756e..91454c4b65e7 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -21,47 +21,7 @@ STD_PATH="${SYSROOT}/lib/rustlib/src/rust/library" cp -r "${STD_PATH}" "${TMP_DIR}" # Insert a small harness in one of the standard library modules. -CORE_CODE=' -#[cfg(kani)] -kani_core::kani_lib!(core); - -#[cfg(kani)] -#[unstable(feature = "kani", issue = "none")] -pub mod verify { - use crate::kani; - - #[kani::proof] - pub fn harness() { - kani::assert(true, "yay"); - } - - #[kani::proof_for_contract(fake_function)] - fn dummy_proof() { - fake_function(true); - } - - /// Add a `rustc_diagnostic_item` to ensure this works. - /// See for more details. - #[kani::requires(x == true)] - #[rustc_diagnostic_item = "fake_function"] - fn fake_function(x: bool) -> bool { - x - } - - #[kani::proof_for_contract(dummy_read)] - fn check_dummy_read() { - let val: char = kani::any(); - assert_eq!(unsafe { dummy_read(&val) }, val); - } - - /// Ensure we can verify constant functions. - #[kani::requires(kani::mem::can_dereference(ptr))] - #[rustc_diagnostic_item = "dummy_read"] - const unsafe fn dummy_read(ptr: *const T) -> T { - *ptr - } -} -' +CORE_CODE=$(cat verify_core.rs) STD_CODE=' #[cfg(kani)]