Merge branch 'main' into nondet-meminit

model-checking · Jul 3, 2024 · 8e7eac1 · 8e7eac1
2 parents 0723510 + fcc9d8b
commit 8e7eac1
Show file tree

Hide file tree

Showing 23 changed files with 86 additions and 70 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,6 +4,44 @@ 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.53.0]
+
+### Major Changes
+* The `--visualize` option is being deprecated and will be removed in a future release. Consider using the `--concrete-playback` option instead.
+* The `-Z ptr-to-ref-cast-checks` option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in a future release once remaining performance issues have been resolved.
+* The `-Z uninit-checks` option is being introduced to check memory initialization. The feature is currently behind an unstable flag and also requires the `-Z ghost-state` option.
+
+### Breaking Changes
+* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278
+* Remove deprecated `--enable-stubbing` by @celinval in https://github.com/model-checking/kani/pull/3309
+
+### What's Changed
+
+* Change ensures into closures by @pi314mm in https://github.com/model-checking/kani/pull/3207
+* (Re)introduce `Invariant` trait by @adpaco-aws in https://github.com/model-checking/kani/pull/3190
+* Remove empty box creation from contracts impl by @celinval in https://github.com/model-checking/kani/pull/3233
+* Add a new verify-std subcommand to Kani by @celinval in https://github.com/model-checking/kani/pull/3231
+* Inject pointer validity check when casting raw pointers to references by @artemagvanian in https://github.com/model-checking/kani/pull/3221
+* Do not turn trivially diverging loops into assume(false) by @tautschnig in https://github.com/model-checking/kani/pull/3223
+* Fix "unused mut" warnings created by generated code. by @jsalzbergedu in https://github.com/model-checking/kani/pull/3247
+* Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in https://github.com/model-checking/kani/pull/3245
+* Use cfg=kani_host for host crates by @tautschnig in https://github.com/model-checking/kani/pull/3244
+* Add intrinsics and Arbitrary support for no_core by @jaisnan in https://github.com/model-checking/kani/pull/3230
+* Contracts: Avoid attribute duplication and `const` function generation for constant function by @celinval in https://github.com/model-checking/kani/pull/3255
+* Fix contract of constant fn with effect feature by @celinval in https://github.com/model-checking/kani/pull/3259
+* Fix typed_swap for ZSTs by @tautschnig in https://github.com/model-checking/kani/pull/3256
+* Add a `#[derive(Invariant)]` macro by @adpaco-aws in https://github.com/model-checking/kani/pull/3250
+* Contracts: History Expressions via "old" monad by @pi314mm in https://github.com/model-checking/kani/pull/3232
+* Function Contracts: remove instances of _renamed by @pi314mm in https://github.com/model-checking/kani/pull/3274
+* Deprecate `--visualize` in favor of concrete playback by @celinval in https://github.com/model-checking/kani/pull/3281
+* Fix operand in fat pointer comparison by @pi314mm in https://github.com/model-checking/kani/pull/3297
+* Function Contracts: Closure Type Inference by @pi314mm in https://github.com/model-checking/kani/pull/3307
+* Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in https://github.com/model-checking/kani/pull/3306
+* Towards Proving Memory Initialization by @artemagvanian in https://github.com/model-checking/kani/pull/3264
+* Rust toolchain upgraded to `nightly-2024-07-01` by @tautschnig @celinval @jaisnan @adpaco-aws
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.52.0...kani-0.53.0
+
 ## [0.52.0]
 
 ## What's Changed

diff --git a/Cargo.lock b/Cargo.lock
@@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "build-kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -228,7 +228,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -405,14 +405,14 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -433,7 +433,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -461,7 +461,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "anyhow",
  "home",
@@ -470,14 +470,14 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -487,7 +487,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -992,7 +992,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.52.0"
+version = "0.53.0"
 dependencies = [
  "kani",
 ]

diff --git a/Cargo.toml b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.52.0"
+version = "0.53.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
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.52.0"
+version = "0.53.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.52.0"
+version = "0.53.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.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
@@ -282,17 +282,6 @@ pub struct VerificationArgs {
  #[arg(long)]
  pub randomize_layout: Option<Option<u64>>,
 
- /// Enable the stubbing of functions and methods.
- // TODO: Stubbing should in principle work with concrete playback.
- // <https://github.com/model-checking/kani/issues/1842>
- #[arg(
- long,
- hide_short_help = true,
- requires("enable_unstable"),
- conflicts_with("concrete_playback")
- )]
- enable_stubbing: bool,
-
  /// Enable Kani coverage output alongside verification result
  #[arg(long, hide_short_help = true)]
  pub coverage: bool,
@@ -345,8 +334,7 @@ impl VerificationArgs {
 
  /// Is experimental stubbing enabled?
  pub fn is_stubbing_enabled(&self) -> bool {
- self.enable_stubbing
- || self.common_args.unstable_features.contains(UnstableFeature::Stubbing)
+ self.common_args.unstable_features.contains(UnstableFeature::Stubbing)
  || self.is_function_contracts_enabled()
  }
 }
@@ -579,6 +567,13 @@ impl ValidateArgs for VerificationArgs {
  --output-format=old.",
  ));
  }
+ if self.concrete_playback.is_some() && self.is_stubbing_enabled() {
+ // Concrete playback currently does not work with contracts or stubbing.
+ return Err(Error::raw(
+ ErrorKind::ArgumentConflict,
+ "Conflicting options: --concrete-playback isn't compatible with stubbing.",
+ ));
+ }
  if self.concrete_playback.is_some() && self.jobs() != Some(1) {
  // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called.
  return Err(Error::raw(
@@ -606,10 +601,6 @@ impl ValidateArgs for VerificationArgs {
  }
  }
 
- if self.enable_stubbing {
- print_deprecated(&self.common_args, "--enable-stubbing", "-Z stubbing");
- }
-
  if self.concrete_playback.is_some()
  && !self.common_args.unstable_features.contains(UnstableFeature::ConcretePlayback)
  {
@@ -880,14 +871,18 @@ mod tests {
 
  #[test]
  fn check_enable_stubbing() {
- check_unstable_flag!("--enable-stubbing --harness foo", enable_stubbing);
+ let res = parse_unstable_disabled("--harness foo").unwrap();
+ assert!(!res.verify_opts.is_stubbing_enabled());
 
- check_unstable_flag!("--enable-stubbing", enable_stubbing);
+ let res = parse_unstable_disabled("--harness foo -Z stubbing").unwrap();
+ assert!(res.verify_opts.is_stubbing_enabled());
 
- // `--enable-stubbing` cannot be called with `--concrete-playback`
- let err =
- parse_unstable_enabled("--enable-stubbing --harness foo --concrete-playback=print")
- .unwrap_err();
+ // `-Z stubbing` cannot be called with `--concrete-playback`
+ let res = parse_unstable_disabled(
+ "--harness foo --concrete-playback=print -Z concrete-playback -Z stubbing",
+ )
+ .unwrap();
+ let err = res.validate().unwrap_err();
  assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
  }
 

diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.52.0"
+version = "0.53.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.52.0"
+version = "0.53.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
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_core"
-version = "0.52.0"
+version = "0.53.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
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

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.52.0"
+version = "0.53.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

diff --git a/tests/cargo-ui/stubbing-flag/src/main.rs b/tests/cargo-ui/stubbing-flag/src/main.rs
@@ -1,7 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-//! This tests that the `--enable-stubbing` and `--harness` arguments flow from `kani-driver` to `kani-compiler`.
+//! This tests that enabling stubbing and using `--harness` arguments flow from
+//! `kani-driver` to `kani-compiler`.
 
 #[kani::proof]
 fn main() {}
diff --git a/tests/expected/function-stubbing-no-harness/main.rs b/tests/expected/function-stubbing-no-harness/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness foo --enable-unstable --enable-stubbing
+// kani-flags: --harness foo -Z stubbing
 //
 //! This tests whether we detect missing harnesses during stubbing.
 

diff --git a/tests/expected/stubbing-ambiguous-path/main.rs b/tests/expected/stubbing-ambiguous-path/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests that we raise an error if a path in a `kani::stub` attribute can
 //! resolve to multiple functions.

diff --git a/tests/ui/function-stubbing-error/main.rs b/tests/ui/function-stubbing-error/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests whether we detect syntactically misformed `kani::stub` annotations.
 

diff --git a/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs b/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs
diff --git a/tests/ui/stubbing/deprecated-enable-stable/expected b/tests/ui/stubbing/deprecated-enable-stable/expected
diff --git a/tests/ui/stubbing/invalid-path/invalid.rs b/tests/ui/stubbing/invalid-path/invalid.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness invalid_stub --enable-unstable --enable-stubbing
+// kani-flags: --harness invalid_stub -Z stubbing
 
 pub mod mod_a {
  use crate::mod_b::noop;

diff --git a/tests/ui/stubbing/stubbing-flag/main.rs b/tests/ui/stubbing/stubbing-flag/main.rs
@@ -1,9 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
-//! This tests that the `--enable-stubbing` and `--harness` arguments flow from `kani-driver` to `kani-compiler`.
+//! This tests that enabling stubbing and `--harness` argument flow from `kani-driver` to `kani-compiler`.
 
 #[kani::proof]
 fn main() {}
diff --git a/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs b/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests that we catch trait mismatches between the stub and the original
 //! function/method. In particular, this tests the case when the program is

diff --git a/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs b/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests that we catch type mismatches between the stub and the original
 //! function/method.

diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.52.0"
+version = "0.53.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"