From 358ade91d84869673fbaaaf6f848aa8f068f373f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 4 Jun 2024 23:55:16 +0300 Subject: [PATCH 1/2] Bump Kani version to 0.52.0 (#3224) Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.51.0"/version = "0.52.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Bump tests/perf/s2n-quic from `6dd41e0` to `bd37960` by @dependabot in https://github.com/model-checking/kani/pull/3178 * Automatic cargo update to 2024-05-13 by @github-actions in https://github.com/model-checking/kani/pull/3177 * Upgrade toolchain to 2024-04-22 by @zhassan-aws in https://github.com/model-checking/kani/pull/3171 * Upgrade toolchain to 2024-05-14 by @zhassan-aws in https://github.com/model-checking/kani/pull/3183 * Automatic toolchain upgrade to nightly-2024-05-15 by @github-actions in https://github.com/model-checking/kani/pull/3185 * Include `--check-cfg=cfg(kani)` in the rust flags to avoid a warning about an unknown `cfg`. by @zhassan-aws in https://github.com/model-checking/kani/pull/3187 * Automatic toolchain upgrade to nightly-2024-05-16 by @github-actions in https://github.com/model-checking/kani/pull/3189 * Perform cargo update because of yanked libc version by @zhassan-aws in https://github.com/model-checking/kani/pull/3192 * Automatic toolchain upgrade to nightly-2024-05-17 by @github-actions in https://github.com/model-checking/kani/pull/3191 * Automatic cargo update to 2024-05-20 by @github-actions in https://github.com/model-checking/kani/pull/3195 * Bump tests/perf/s2n-quic from `bd37960` to `f5d9d74` by @dependabot in https://github.com/model-checking/kani/pull/3196 * New section about linter configuraton checking in the doc. by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3198 * Automatic cargo update to 2024-05-27 by @github-actions in https://github.com/model-checking/kani/pull/3201 * Bump tests/perf/s2n-quic from `f5d9d74` to `d03cc47` by @dependabot in https://github.com/model-checking/kani/pull/3202 * Update Rust toolchain from nightly-2024-05-17 to nightly-2024-05-23 by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3199 * Fix `{,e}println!()` by @GrigorenkoPV in https://github.com/model-checking/kani/pull/3209 * Contracts for a few core functions by @celinval in https://github.com/model-checking/kani/pull/3107 * Don't crash benchcomp when rounding non-numeric values by @karkhaz in https://github.com/model-checking/kani/pull/3211 * Update Rust toolchain nightly-2024-05-24 by @qinheping in https://github.com/model-checking/kani/pull/3212 * Upgrade Rust toolchain nightly-2024-05-27 by @qinheping in https://github.com/model-checking/kani/pull/3215 * Automatic toolchain upgrade to nightly-2024-05-28 by @github-actions in https://github.com/model-checking/kani/pull/3217 * Automatic cargo update to 2024-06-03 by @github-actions in https://github.com/model-checking/kani/pull/3220 * Bump tests/perf/s2n-quic from `d03cc47` to `d90729d` by @dependabot in https://github.com/model-checking/kani/pull/3222 * Add simple API for shadow memory by @zhassan-aws in https://github.com/model-checking/kani/pull/3200 ## New Contributors * @GrigorenkoPV made their first contribution in https://github.com/model-checking/kani/pull/3209 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.51.0...kani-0.52.0 --- CHANGELOG.md | 13 ++++++++++++- Cargo.lock | 18 +++++++++--------- Cargo.toml | 2 +- cprover_bindings/Cargo.toml | 2 +- kani-compiler/Cargo.toml | 2 +- kani-driver/Cargo.toml | 2 +- kani_metadata/Cargo.toml | 2 +- library/kani/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 11 files changed, 30 insertions(+), 19 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7fc4cac54063..9b4acbb284aa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,9 +4,20 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. -## [0.51.0] +## [0.52.0] ## What's Changed +* New section about linter configuraton checking in the doc by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3198 +* Fix `{,e}println!()` by @GrigorenkoPV in https://github.com/model-checking/kani/pull/3209 +* Contracts for a few core functions by @celinval in https://github.com/model-checking/kani/pull/3107 +* Add simple API for shadow memory by @zhassan-aws in https://github.com/model-checking/kani/pull/3200 +* Upgrade Rust toolchain to 2024-05-28 by @zhassan-aws @remi-delmas-3000 @qinheping + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.51.0...kani-0.52.0 + +## [0.51.0] + +### What's Changed * Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in https://github.com/model-checking/kani/pull/3134 * Remove `kani::Arbitrary` from the `modifies` contract instrumentation by @feliperodri in https://github.com/model-checking/kani/pull/3169 diff --git a/Cargo.lock b/Cargo.lock index f1ee88cafeed..dc15890341c3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -92,7 +92,7 @@ checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" [[package]] name = "build-kani" -version = "0.51.0" +version = "0.52.0" dependencies = [ "anyhow", "cargo_metadata", @@ -228,7 +228,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.51.0" +version = "0.52.0" dependencies = [ "lazy_static", "linear-map", @@ -405,14 +405,14 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "kani" -version = "0.51.0" +version = "0.52.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.51.0" +version = "0.52.0" dependencies = [ "clap", "cprover_bindings", @@ -433,7 +433,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.51.0" +version = "0.52.0" dependencies = [ "anyhow", "cargo_metadata", @@ -461,7 +461,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.51.0" +version = "0.52.0" dependencies = [ "anyhow", "home", @@ -470,7 +470,7 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.51.0" +version = "0.52.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -480,7 +480,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.51.0" +version = "0.52.0" dependencies = [ "clap", "cprover_bindings", @@ -985,7 +985,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" [[package]] name = "std" -version = "0.51.0" +version = "0.52.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 24812a157ae5..bd3c7f3336c2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.51.0" +version = "0.52.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 844accd3914b..b98b09c68a58 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.51.0" +version = "0.52.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 7315ff224bd8..2ef273802028 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.51.0" +version = "0.52.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 6b25fe02a263..2263e39792e2 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.51.0" +version = "0.52.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 645ed4da5fd2..f9d701018367 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.51.0" +version = "0.52.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 4b158e41daa0..c0f783e65315 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.51.0" +version = "0.52.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 0f9dda7136ad..e915fdc64a75 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.51.0" +version = "0.52.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index b83c9d3dcba0..fcc2739dc606 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.51.0" +version = "0.52.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 21ad6be2a4b0..30c2807aa323 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.51.0" +version = "0.52.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" From ab56b9d96308be5acba4865577abb9450518ed9a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 4 Jun 2024 15:17:12 -0700 Subject: [PATCH 2/2] Add `kani_core` library placeholder and build logic (#3227) While at it, I also added a `--skip-libs` to skip rebuilding the Kani libraries and standard library at every `cargo build-dev` execution. We usually only need to rebuild the libraries when we make changes to them or when we update the Rust toolchain. Rebuilding them can be quite time consuming when you are making changes to Kani. Towards #3226 #3153 Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- Cargo.lock | 7 ++++ Cargo.toml | 1 + library/kani_core/Cargo.toml | 11 +++++++ library/kani_core/src/lib.rs | 5 +++ library/kani_macros/Cargo.toml | 5 ++- tools/build-kani/src/main.rs | 8 ++++- tools/build-kani/src/parser.rs | 4 +++ tools/build-kani/src/sysroot.rs | 58 +++++++++++++++++++++++---------- 8 files changed, 79 insertions(+), 20 deletions(-) create mode 100644 library/kani_core/Cargo.toml create mode 100644 library/kani_core/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index dc15890341c3..7b2857e1c7ba 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -468,6 +468,13 @@ dependencies = [ "os_info", ] +[[package]] +name = "kani_core" +version = "0.51.0" +dependencies = [ + "kani_macros", +] + [[package]] name = "kani_macros" version = "0.52.0" diff --git a/Cargo.toml b/Cargo.toml index bd3c7f3336c2..e4ff44f42ddc 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -43,6 +43,7 @@ members = [ "kani-driver", "kani-compiler", "kani_metadata", + "library/kani_core", ] # This indicates what package to e.g. build with 'cargo build' without --workspace diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml new file mode 100644 index 000000000000..ad96017a2a28 --- /dev/null +++ b/library/kani_core/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "kani_core" +version = "0.51.0" +edition = "2021" +license = "MIT OR Apache-2.0" +publish = false + +[dependencies] +kani_macros = { path = "../kani_macros", features = ["no_core"] } \ No newline at end of file diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs new file mode 100644 index 000000000000..00b5efbe719c --- /dev/null +++ b/library/kani_core/src/lib.rs @@ -0,0 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This is placeholder for the new `kani_core` library. +#![feature(no_core)] diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index e915fdc64a75..dbe2126d0458 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -19,4 +19,7 @@ syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] } [package.metadata.rust-analyzer] # This package uses rustc crates. -rustc_private=true +rustc_private = true + +[features] +no_core = [] \ No newline at end of file diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index f65d52e03fd1..3f1bc26cfbbb 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -19,7 +19,13 @@ fn main() -> Result<()> { let args = parser::ArgParser::parse(); match args.subcommand { - parser::Commands::BuildDev(build_parser) => build_lib(&build_bin(&build_parser.args)?), + parser::Commands::BuildDev(build_parser) => { + let bin_folder = &build_bin(&build_parser.args)?; + if !build_parser.skip_libs { + build_lib(&bin_folder)?; + } + Ok(()) + } parser::Commands::Bundle(bundle_parser) => { let version_string = bundle_parser.version; let kani_string = format!("kani-{version_string}"); diff --git a/tools/build-kani/src/parser.rs b/tools/build-kani/src/parser.rs index 3f9dfa0a1d42..718cbb00bcb4 100644 --- a/tools/build-kani/src/parser.rs +++ b/tools/build-kani/src/parser.rs @@ -17,6 +17,10 @@ pub struct BuildDevParser { /// Arguments to be passed down to cargo when building cargo binaries. #[clap(value_name = "ARG", allow_hyphen_values = true)] pub args: Vec, + /// Do not re-build Kani libraries. Only use this if you know there has been no changes to Kani + /// libraries or the underlying Rust compiler. + #[clap(long)] + pub skip_libs: bool, } #[derive(Args, Debug, Eq, PartialEq)] diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index b831ed0d63a8..f3ece1ee006a 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -55,18 +55,29 @@ pub fn kani_playback_lib() -> PathBuf { path_buf!(kani_sysroot(), "playback/lib") } +/// Returns the path to where Kani libraries for no_core is kept. +pub fn kani_no_core_lib() -> PathBuf { + path_buf!(kani_sysroot(), "no_core/lib") +} + /// Returns the path to where Kani's pre-compiled binaries are stored. fn kani_sysroot_bin() -> PathBuf { path_buf!(kani_sysroot(), "bin") } +/// Returns the build target +fn build_target() -> &'static str { + env!("TARGET") +} + /// Build the `lib/` folder and `lib-playback/` for the new sysroot. /// - The `lib/` folder contains the sysroot for verification. /// - The `lib-playback/` folder contains the sysroot used for playback. pub fn build_lib(bin_folder: &Path) -> Result<()> { let compiler_path = bin_folder.join("kani-compiler"); build_verification_lib(&compiler_path)?; - build_playback_lib(&compiler_path) + build_playback_lib(&compiler_path)?; + build_no_core_lib(&compiler_path) } /// Build the `lib/` folder for the new sysroot used during verification. @@ -75,7 +86,9 @@ fn build_verification_lib(compiler_path: &Path) -> Result<()> { let extra_args = ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""]; let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std"]; - build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args) + let packages = ["std", "kani", "kani_macros"]; + let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &compiler_args)?; + copy_artifacts(&artifacts, &kani_sysroot_lib(), true) } /// Build the `lib-playback/` folder that will be used during counter example playback. @@ -83,26 +96,30 @@ fn build_verification_lib(compiler_path: &Path) -> Result<()> { fn build_playback_lib(compiler_path: &Path) -> Result<()> { let extra_args = ["--features=std/concrete_playback,kani/concrete_playback", "-Z", "build-std=std,test"]; - build_kani_lib(compiler_path, &kani_playback_lib(), &extra_args, &[]) + let packages = ["std", "kani", "kani_macros"]; + let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &[])?; + copy_artifacts(&artifacts, &kani_playback_lib(), true) +} + +/// 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 packages = ["kani_core", "kani_macros"]; + let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &[])?; + copy_artifacts(&artifacts, &kani_no_core_lib(), false) } fn build_kani_lib( compiler_path: &Path, - output_path: &Path, + packages: &[&str], extra_cargo_args: &[&str], extra_rustc_args: &[&str], -) -> Result<()> { +) -> Result> { // Run cargo build with -Z build-std - let target = env!("TARGET"); + let target = build_target(); let target_dir = env!("KANI_BUILD_LIBS"); let args = [ "build", - "-p", - "std", - "-p", - "kani", - "-p", - "kani_macros", "-Z", "unstable-options", "--target-dir", @@ -137,6 +154,7 @@ fn build_kani_lib( .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join("\x1f")) .env("RUSTC", compiler_path) .args(args) + .args(packages.iter().copied().flat_map(|pkg| ["-p", pkg])) .args(extra_cargo_args) .stdout(Stdio::piped()) .spawn() @@ -152,20 +170,24 @@ fn build_kani_lib( } // Create sysroot folder hierarchy. - copy_artifacts(&artifacts, output_path, target) + Ok(artifacts) } /// Copy all the artifacts to their correct place to generate a valid sysroot. -fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, target: &str) -> Result<()> { - // Create sysroot folder hierarchy. +fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, copy_std: bool) -> Result<()> { + // Create sysroot folder. sysroot_lib.exists().then(|| fs::remove_dir_all(sysroot_lib)); - let std_path = path_buf!(&sysroot_lib, "rustlib", target, "lib"); - fs::create_dir_all(&std_path).expect(&format!("Failed to create {std_path:?}")); + fs::create_dir_all(sysroot_lib)?; // Copy Kani libraries into sysroot top folder. copy_libs(&artifacts, &sysroot_lib, &is_kani_lib); + // Copy standard libraries into rustlib//lib/ folder. - copy_libs(&artifacts, &std_path, &is_std_lib); + if copy_std { + let std_path = path_buf!(&sysroot_lib, "rustlib", build_target(), "lib"); + fs::create_dir_all(&std_path).expect(&format!("Failed to create {std_path:?}")); + copy_libs(&artifacts, &std_path, &is_std_lib); + } Ok(()) }