diff --git a/Cargo.lock b/Cargo.lock index 31eac9d1663e..bf34011c5f04 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -470,7 +470,7 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.51.0" +version = "0.52.0" dependencies = [ "kani_macros", ] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index a720d1457606..7edd64438728 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -47,6 +47,7 @@ impl<'tcx> GotocCtx<'tcx> { } _ => None, }); + let recursion_tracker_def = recursion_tracker .next() .expect("There should be at least one recursion tracker (REENTRY) in scope"); diff --git a/kani-driver/src/args_toml.rs b/kani-driver/src/args_toml.rs index b9e994b38fec..37b38a425597 100644 --- a/kani-driver/src/args_toml.rs +++ b/kani-driver/src/args_toml.rs @@ -315,6 +315,6 @@ mod tests { #[test] fn check_unstable_entry_invalid() { let name = String::from("feature"); - assert!(matches!(unstable_entry(&name, &Value::String("".to_string())), Err(_))); + assert!(unstable_entry(&name, &Value::String("".to_string())).is_err()); } } diff --git a/library/kani/build.rs b/library/kani/build.rs new file mode 100644 index 000000000000..c094cc0254c6 --- /dev/null +++ b/library/kani/build.rs @@ -0,0 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn main() { + // Make sure `kani_sysroot` is a recognized config + println!("cargo::rustc-check-cfg=cfg(kani_sysroot)"); +} diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index ad96017a2a28..6f5230c6d19b 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -1,11 +1,16 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "kani_core" -version = "0.51.0" +version = "0.52.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false +description = "Define core constructs to use with Kani" [dependencies] -kani_macros = { path = "../kani_macros", features = ["no_core"] } \ No newline at end of file +kani_macros = { path = "../kani_macros", features = ["no_core"] } + +[features] +no_core=["kani_macros/no_core"] diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs new file mode 100644 index 000000000000..e7ac4dc81508 --- /dev/null +++ b/library/kani_core/src/arbitrary.rs @@ -0,0 +1,168 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This macro generates implementations of the `Arbitrary` trait for various types. The `Arbitrary` trait defines +//! methods for generating arbitrary (unconstrained) values of the implementing type. +//! trivial_arbitrary and nonzero_arbitrary are implementations of Arbitrary for types that can be represented +//! by an unconstrained symbolic value of their size (e.g., `u8`, `u16`, `u32`, etc.). +//! +//! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary. +#[macro_export] +macro_rules! generate_arbitrary { + ($core:path) => { + use core_path::marker::{PhantomData, PhantomPinned}; + use $core as core_path; + + pub trait Arbitrary + where + 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]>()]:, + { + [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) + } + } + + /// The given type can be represented by an unconstrained symbolic value of size_of::. + macro_rules! trivial_arbitrary { + ( $type: ty ) => { + impl Arbitrary for $type { + #[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::() }>() } + } + // 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]>() }, + >() + } + } + } + }; + } + + macro_rules! nonzero_arbitrary { + ( $type: ty, $base: ty ) => { + use core_path::num::*; + impl Arbitrary for $type { + #[inline(always)] + fn any() -> Self { + let val = <$base>::any(); + assume(val != 0); + unsafe { <$type>::new_unchecked(val) } + } + } + }; + } + + // Generate trivial arbitrary values + trivial_arbitrary!(u8); + trivial_arbitrary!(u16); + trivial_arbitrary!(u32); + trivial_arbitrary!(u64); + trivial_arbitrary!(u128); + trivial_arbitrary!(usize); + + trivial_arbitrary!(i8); + trivial_arbitrary!(i16); + trivial_arbitrary!(i32); + trivial_arbitrary!(i64); + trivial_arbitrary!(i128); + trivial_arbitrary!(isize); + + nonzero_arbitrary!(NonZeroU8, u8); + nonzero_arbitrary!(NonZeroU16, u16); + nonzero_arbitrary!(NonZeroU32, u32); + nonzero_arbitrary!(NonZeroU64, u64); + nonzero_arbitrary!(NonZeroU128, u128); + nonzero_arbitrary!(NonZeroUsize, usize); + + nonzero_arbitrary!(NonZeroI8, i8); + nonzero_arbitrary!(NonZeroI16, i16); + nonzero_arbitrary!(NonZeroI32, i32); + nonzero_arbitrary!(NonZeroI64, i64); + nonzero_arbitrary!(NonZeroI128, i128); + nonzero_arbitrary!(NonZeroIsize, isize); + + // Implement arbitrary for non-trivial types + impl Arbitrary for bool { + #[inline(always)] + fn any() -> Self { + let byte = u8::any(); + assume(byte < 2); + byte == 1 + } + } + + /// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] + /// Ref: + impl Arbitrary for char { + #[inline(always)] + fn any() -> Self { + // Generate an arbitrary u32 and constrain it to make it a valid representation of char. + + let val = u32::any(); + assume(val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val)); + unsafe { char::from_u32_unchecked(val) } + } + } + + impl Arbitrary for Option + where + T: Arbitrary, + { + fn any() -> Self { + if bool::any() { Some(T::any()) } else { None } + } + } + + impl Arbitrary for Result + where + T: Arbitrary, + E: Arbitrary, + { + fn any() -> Self { + if bool::any() { Ok(T::any()) } else { Err(E::any()) } + } + } + + impl Arbitrary for PhantomData { + fn any() -> Self { + PhantomData + } + } + + impl Arbitrary for PhantomPinned { + fn any() -> Self { + PhantomPinned + } + } + + #[cfg(kani_sysroot)] + impl Arbitrary for [T; N] + where + T: Arbitrary, + [(); core_path::mem::size_of::<[T; N]>()]:, + { + fn any() -> Self { + T::any_array() + } + } + }; +} diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index a5cd40d71e92..c31e964eeb0a 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -1,8 +1,289 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! This crate is a macro_only crate. It is designed to be used in `no_core` and `no_std` +//! environment. +//! +//! It will contain macros that generate core components of Kani. +//! +//! For regular usage, the kani library will invoke these macros to generate its components as if +//! they were declared in that library. +//! +//! For `no_core` and `no_std` crates, they will have to directly invoke those macros inside a +//! `kani` module in order to generate all the required components. +//! I.e., the components will be part of the crate being compiled. +//! +//! Note that any crate level attribute should be added by kani_driver as RUSTC_FLAGS. +//! E.g.: `register_tool(kanitool)` -//! This is placeholder for the new `kani_core` library. #![feature(no_core)] #![no_core] +mod arbitrary; + pub use kani_macros::*; + +/// Users should only need to invoke this. +/// +/// Options are: +/// - `kani`: Add definitions needed for Kani library. +/// - `core`: Define a `kani` module inside `core` crate. +/// - `std`: TODO: Define a `kani` module inside `std` crate. Users must define kani inside core. +#[macro_export] +macro_rules! kani_lib { + (core) => { + #[cfg(kani)] + #[unstable(feature = "kani", issue = "none")] + pub mod kani { + pub use kani_core::{ensures, proof, proof_for_contract, requires, should_panic}; + kani_core::kani_intrinsics!(); + kani_core::generate_arbitrary!(core); + } + }; + + (kani) => { + pub use kani_core::*; + kani_core::kani_intrinsics!(); + kani_core::generate_arbitrary!(std); + }; +} + +/// Kani intrinsics contains the public APIs used by users to verify their harnesses. +/// This macro is a part of kani_core as that allows us to verify even libraries that are no_core +/// 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. +#[macro_export] +macro_rules! kani_intrinsics { + () => { + /// Creates an assumption that will be valid after this statement run. Note that the assumption + /// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the + /// program will exit successfully. + /// + /// # Example: + /// + /// The code snippet below should never panic. + /// + /// ```rust + /// let i : i32 = kani::any(); + /// kani::assume(i > 10); + /// if i < 0 { + /// panic!("This will never panic"); + /// } + /// ``` + /// + /// The following code may panic though: + /// + /// ```rust + /// let i : i32 = kani::any(); + /// assert!(i < 0, "This may panic and verification should fail."); + /// kani::assume(i > 10); + /// ``` + #[inline(never)] + #[rustc_diagnostic_item = "KaniAssume"] + #[cfg(not(feature = "concrete_playback"))] + pub fn assume(cond: bool) { + let _ = cond; + } + + #[inline(never)] + #[rustc_diagnostic_item = "KaniAssume"] + #[cfg(feature = "concrete_playback")] + pub fn assume(cond: bool) { + assert!(cond, "`kani::assume` should always hold"); + } + + /// Creates an assertion of the specified condition and message. + /// + /// # Example: + /// + /// ```rust + /// let x: bool = kani::any(); + /// let y = !x; + /// kani::assert(x || y, "ORing a boolean variable with its negation must be true") + /// ``` + #[cfg(not(feature = "concrete_playback"))] + #[inline(never)] + #[rustc_diagnostic_item = "KaniAssert"] + pub const fn assert(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; + } + + #[cfg(feature = "concrete_playback")] + #[inline(never)] + #[rustc_diagnostic_item = "KaniAssert"] + pub const fn assert(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); + } + + /// Creates a cover property with the specified condition and message. + /// + /// # Example: + /// + /// ```rust + /// kani::cover(slice.len() == 0, "The slice may have a length of 0"); + /// ``` + /// + /// A cover property checks if there is at least one execution that satisfies + /// the specified condition at the location in which the function is called. + /// + /// Cover properties are reported as: + /// - SATISFIED: if Kani found an execution that satisfies the condition + /// - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied + /// - UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE) + /// + /// This function is called by the [`cover!`] macro. The macro is more + /// convenient to use. + /// + #[inline(never)] + #[rustc_diagnostic_item = "KaniCover"] + pub const fn cover(_cond: bool, _msg: &'static str) {} + + /// This creates an symbolic *valid* value of type `T`. You can assign the return value of this + /// function to a variable that you want to make symbolic. + /// + /// # Example: + /// + /// In the snippet below, we are verifying the behavior of the function `fn_under_verification` + /// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero. + /// + /// ```rust + /// let inputA = kani::any::(); + /// fn_under_verification(inputA); + /// ``` + /// + /// Note: This is a safe construct and can only be used with types that implement the `Arbitrary` + /// trait. The Arbitrary trait is used to build a symbolic value that represents all possible + /// valid values for type `T`. + #[rustc_diagnostic_item = "KaniAny"] + #[inline(always)] + pub fn any() -> T { + T::any() + } + + /// This function is only used for function contract instrumentation. + /// It behaves exaclty like `kani::any()`, except it will check for the trait bounds + /// at compilation time. It allows us to avoid type checking errors while using function + /// contracts only for verification. + #[rustc_diagnostic_item = "KaniAnyModifies"] + #[inline(never)] + #[doc(hidden)] + pub fn any_modifies() -> 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!() + } + + /// This creates a symbolic *valid* value of type `T`. + /// The value is constrained to be a value accepted by the predicate passed to the filter. + /// You can assign the return value of this function to a variable that you want to make symbolic. + /// + /// # Example: + /// + /// In the snippet below, we are verifying the behavior of the function `fn_under_verification` + /// under all possible `u8` input values between 0 and 12. + /// + /// ```rust + /// let inputA: u8 = kani::any_where(|x| *x < 12); + /// fn_under_verification(inputA); + /// ``` + /// + /// Note: This is a safe construct and can only be used with types that implement the `Arbitrary` + /// trait. The Arbitrary trait is used to build a symbolic value that represents all possible + /// valid values for type `T`. + #[inline(always)] + pub fn any_where bool>(f: F) -> T { + let result = T::any(); + assume(f(&result)); + result + } + + /// This function creates a symbolic value of type `T`. This may result in an invalid value. + /// + /// # Safety + /// + /// This function is unsafe and it may represent invalid `T` values which can lead to many + /// undesirable undefined behaviors. Because of that, this function can only be used + /// internally when we can guarantee that the type T has no restriction regarding its bit level + /// representation. + /// + /// This function is also used to find concrete values in the CBMC output trace + /// and return those concrete values in concrete playback mode. + /// + /// 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::() + } + + #[inline(never)] + #[cfg(feature = "concrete_playback")] + 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 { + kani_intrinsic() + } + + /// Function used to generate panic with a static message as this is the only one currently + /// 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 + /// overrides, but not the other way around. + #[inline(never)] + #[rustc_diagnostic_item = "KaniPanic"] + #[doc(hidden)] + pub const fn panic(message: &'static str) -> ! { + panic!("{}", message) + } + + /// An empty body that can be used to define Kani intrinsic functions. + /// + /// A Kani intrinsic is a function that is interpreted by Kani compiler. + /// While we could use `unreachable!()` or `panic!()` as the body of a kani intrinsic + /// function, both cause Kani to produce a warning since we don't support caller location. + /// (see https://github.com/model-checking/kani/issues/2010). + /// + /// This function is dead, since its caller is always handled via a hook anyway, + /// so we just need to put a body that rustc does not complain about. + /// An infinite loop works out nicely. + fn kani_intrinsic() -> T { + #[allow(clippy::empty_loop)] + loop {} + } + + pub mod internal { + /// A way to break the ownerhip rules. Only used by contracts where we can + /// guarantee it is done safely. + #[inline(never)] + #[doc(hidden)] + #[rustc_diagnostic_item = "KaniUntrackedDeref"] + pub fn untracked_deref(_: &T) -> T { + todo!() + } + + /// CBMC contracts currently has a limitation where `free` has to be in scope. + /// However, if there is no dynamic allocation in the harness, slicing removes `free` from the + /// scope. + /// + /// Thus, this function will basically translate into: + /// ```c + /// // This is a no-op. + /// free(NULL); + /// ``` + #[inline(never)] + #[doc(hidden)] + #[rustc_diagnostic_item = "KaniInitContracts"] + pub fn init_contracts() {} + } + }; +} diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index b0d323b12ca3..3bef8b68f688 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -82,7 +82,10 @@ pub fn make_unsafe_argument_copies( let arg_values = renaming_map.keys(); ( quote!(#(let #arg_names = kani::internal::untracked_deref(&#arg_values);)*), + #[cfg(not(feature = "no_core"))] quote!(#(std::mem::forget(#also_arg_names);)*), + #[cfg(feature = "no_core")] + quote!(#(core::mem::forget(#also_arg_names);)*), ) } 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 028e8949815f..449148c5d904 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -1,14 +1,12 @@ [TEST] Run kani verify-std -Checking harness kani::check_stub... -VERIFICATION:- SUCCESSFUL -Checking harness kani::check_success... +Checking harness verify::dummy_proof... VERIFICATION:- SUCCESSFUL -Checking harness kani::check_panic... -VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) +Checking harness verify::harness... +VERIFICATION:- SUCCESSFUL Checking harness num::verify::check_non_zero... VERIFICATION:- SUCCESSFUL -Complete - 4 successfully verified harnesses, 0 failures, 4 total. +Complete - 3 successfully verified harnesses, 0 failures, 3 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 cc960ee2bfaf..9897a036dd22 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -23,51 +23,26 @@ cp -r "${STD_PATH}" "${TMP_DIR}" # Insert a small harness in one of the standard library modules. CORE_CODE=' #[cfg(kani)] -#[unstable(feature = "kani", issue = "none")] -pub mod kani { - pub use kani_core::proof; - - #[rustc_diagnostic_item = "KaniAnyRaw"] - #[inline(never)] - pub fn any_raw_inner() -> T { - loop {} - } +kani_core::kani_lib!(core); - #[inline(never)] - #[rustc_diagnostic_item = "KaniAssert"] - pub const fn assert(cond: bool, msg: &'\''static str) { - let _ = cond; - let _ = msg; - } - - #[kani_core::proof] - #[kani_core::should_panic] - fn check_panic() { - let num: u8 = any_raw_inner(); - assert!(num != 0, "Found zero"); - } - - #[kani_core::proof] - fn check_success() { - let orig: u8 = any_raw_inner(); - let mid = orig as i8; - let new = mid as u8; - assert!(orig == new, "Conversion round trip works"); - } +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use crate::kani; - pub fn assert_true(cond: bool) { - assert!(cond) + #[kani::proof] + pub fn harness() { + kani::assert(true, "yay"); } - pub fn assert_false(cond: bool) { - assert!(!cond) + #[kani::proof_for_contract(fake_function)] + fn dummy_proof() { + fake_function(true); } - #[kani_core::proof] - #[kani_core::stub(assert_true, assert_false)] - fn check_stub() { - // Check this is in fact asserting false. - assert_true(false) + #[kani::requires(x == true)] + fn fake_function(x: bool) -> bool { + x } } ' @@ -100,7 +75,7 @@ cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs echo "[TEST] Run kani verify-std" export RUST_BACKTRACE=1 -kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z stubbing +kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing # Cleanup rm -r ${TMP_DIR} diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index f3ece1ee006a..ffd08fa7eda0 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -103,7 +103,7 @@ fn build_playback_lib(compiler_path: &Path) -> Result<()> { /// Build the no core library folder that will be used during std verification. fn build_no_core_lib(compiler_path: &Path) -> Result<()> { - let extra_args = ["--features=kani_macros/no_core"]; + let extra_args = ["--features=kani_macros/no_core", "--features=kani_core/no_core"]; let packages = ["kani_core", "kani_macros"]; let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &[])?; copy_artifacts(&artifacts, &kani_no_core_lib(), false)