From c886c81642b1a4b3fdb981bd35d20a23eb9fd864 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 2 Jul 2024 21:10:33 +0000 Subject: [PATCH 1/4] Bump Kani version to 0.53.0 --- Cargo.lock | 20 ++++++++++---------- 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_core/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 11 files changed, 20 insertions(+), 20 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 89e393db8b46..cf47e75b0562 100644 --- 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 index 641cbaf961be..1b4933c5bdcf 100644 --- 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 index 63dfbf6781cd..aced9e5b9b65 100644 --- 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 index 05002ed1eb27..23389c156302 100644 --- 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 index 2263e39792e2..d58d686d7d43 100644 --- 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_metadata/Cargo.toml b/kani_metadata/Cargo.toml index f9d701018367..816752a58e03 100644 --- 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 index c0f783e65315..91fee3dabf30 100644 --- 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 index 6f5230c6d19b..ec12209f0e08 100644 --- 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 index e0c79a39c105..5917c322729e 100644 --- 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 index fcc2739dc606..ae70767f6781 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.52.0" +version = "0.53.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 30c2807aa323..7c8e6eef122a 100644 --- 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" From 8deff656396e35e1d1c44e2a5bffbf2150f3e0ab Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 2 Jul 2024 21:52:31 +0000 Subject: [PATCH 2/4] Edit release notes --- CHANGELOG.md | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b4acbb284aa..1d760bc6db6a 100644 --- 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 the next release once remaining performance issues have been resolved. + +### What's Changed + +* Add `kani_core` library placeholder and build logic by @celinval in https://github.com/model-checking/kani/pull/3227 +* 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 +* Fix a few issues with std verification 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 a few more issues with the std library by @celinval in https://github.com/model-checking/kani/pull/3261 +* Fix typed_swap for ZSTs by @tautschnig in https://github.com/model-checking/kani/pull/3256 +* Remove further uses of Location::none by @tautschnig in https://github.com/model-checking/kani/pull/3253 +* 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 +* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278 +* 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 +* C library: declare malloc by @tautschnig in https://github.com/model-checking/kani/pull/3296 +* 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 From aab5ddafaa52a5664c4b66ff20418909d6a49230 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 2 Jul 2024 23:15:37 +0000 Subject: [PATCH 3/4] Address comments --- CHANGELOG.md | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d760bc6db6a..390f7130153e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,11 +8,14 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ### 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 the next release once remaining performance issues have been resolved. +* 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 ### What's Changed -* Add `kani_core` library placeholder and build logic by @celinval in https://github.com/model-checking/kani/pull/3227 * 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 @@ -23,18 +26,14 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from * 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 -* Fix a few issues with std verification by @celinval in https://github.com/model-checking/kani/pull/3255 +* 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 a few more issues with the std library by @celinval in https://github.com/model-checking/kani/pull/3261 * Fix typed_swap for ZSTs by @tautschnig in https://github.com/model-checking/kani/pull/3256 -* Remove further uses of Location::none by @tautschnig in https://github.com/model-checking/kani/pull/3253 * 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 -* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278 * 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 -* C library: declare malloc by @tautschnig in https://github.com/model-checking/kani/pull/3296 * 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 From ae3f0a1ab9b637139cceb6897039327e4af2f6c3 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 3 Jul 2024 14:07:06 +0000 Subject: [PATCH 4/4] Add newly merged PR to notes --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 390f7130153e..47ae290853a3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ### 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