From eeb5fe74629355ba2612416c8ad05aa31bcb2fb4 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Tue, 11 Jun 2024 00:45:28 -0400 Subject: [PATCH] Add intrinsics and Arbitrary support for no_core (#3230) ### Approach So far The approach so far has been to shift the `kani` library's functionality to `kani_core` instead, which has no dependencies of its own. By moving these API functions to macros, we delay the compilation of these to when Kani is invoked. Tested by using the regression tests added @celinval in https://github.com/model-checking/kani/pull/3236 using the new `verify-std` subcommand. ### Running Kani To test Kani itself, we injected a proof inside the core library by making these changes. ``` rust #[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"); } } ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val --- Cargo.lock | 2 +- .../codegen_cprover_gotoc/codegen/contract.rs | 1 + kani-driver/src/args_toml.rs | 2 +- library/kani/build.rs | 7 + library/kani_core/Cargo.toml | 9 +- library/kani_core/src/arbitrary.rs | 168 +++++++++++ library/kani_core/src/lib.rs | 283 +++++++++++++++++- .../src/sysroot/contracts/shared.rs | 3 + .../verify_std_cmd/verify_std.expected | 10 +- .../verify_std_cmd/verify_std.sh | 55 +--- tools/build-kani/src/sysroot.rs | 2 +- 11 files changed, 490 insertions(+), 52 deletions(-) create mode 100644 library/kani/build.rs create mode 100644 library/kani_core/src/arbitrary.rs 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)