Merge remote-tracking branch 'origin/main' into toolchain-2024-06-04-…

…manual
tautschnig · Jun 5, 2024 · 836a5ee · 836a5ee
2 parents 741b401 + ab56b9d
commit 836a5ee
Show file tree

Hide file tree

Showing 16 changed files with 109 additions and 39 deletions.
diff --git 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
@@ -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,16 +461,23 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.51.0"
+version = "0.52.0"
 dependencies = [
  "anyhow",
  "home",
  "os_info",
 ]
 
 [[package]]
-name = "kani_macros"
+name = "kani_core"
 version = "0.51.0"
+dependencies = [
+ "kani_macros",
+]
+
+[[package]]
+name = "kani_macros"
+version = "0.52.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -480,7 +487,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.51.0"
+version = "0.52.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -985,7 +992,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.51.0"
+version = "0.52.0"
 dependencies = [
  "kani",
 ]

diff --git 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"
@@ -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/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
@@ -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
@@ -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
@@ -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
@@ -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_core/Cargo.toml 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"] }
diff --git a/library/kani_core/src/lib.rs 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
@@ -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
@@ -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 = []
diff --git 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
@@ -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"

diff --git 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
@@ -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<String>,
+    /// 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
@@ -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,34 +86,40 @@ 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.
 /// This will include Kani's libraries compiled with `concrete-playback` feature enabled.
 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<Vec<Artifact>> {
     // 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/<target>/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(())
 }