From 7a6f1a445066c7c6720cd0583cf1cf56f6646955 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 8 Aug 2024 21:07:32 -0400 Subject: [PATCH] Bump Kani version to 0.54.0 (#3430) ## 0.54.0 ### Major Changes * We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts. * We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros. * We enabled support for concrete playback for harness that contains stubs or function contracts. * We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs. ### Breaking Changes * The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default. ## What's Changed * Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in https://github.com/model-checking/kani/pull/3332 * Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323 * Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295 * Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344 * Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348 * Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283 * Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305 * Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373 * Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995 * Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270 * Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389 * Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120 * Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363 * Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001 * Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999 * Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002 * Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000 * Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417 * Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374 * Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333 * Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426 * Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri ## New Contributors * @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Signed-off-by: Felipe R. Monteiro --- CHANGELOG.md | 40 ++++++++++++++++++++++++++++++++++ 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 +- 12 files changed, 60 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 47ae290853a3..d36def1a45f1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,46 @@ 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.54.0] + +### Major Changes +* We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts. +* We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros. +* We enabled support for concrete playback for harness that contains stubs or function contracts. +* We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs. + +### Breaking Changes +* The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default. + +## What's Changed +* Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in https://github.com/model-checking/kani/pull/3332 +* Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323 +* Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295 +* Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344 +* Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348 +* Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283 +* Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305 +* Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373 +* Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995 +* Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270 +* Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389 +* Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120 +* Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363 +* Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001 +* Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999 +* Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002 +* Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000 +* Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417 +* Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374 +* Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333 +* Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426 +* Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri + +## New Contributors +* @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0 + ## [0.53.0] ### Major Changes diff --git a/Cargo.lock b/Cargo.lock index 52250d2468c8..12c28c49c1bf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" [[package]] name = "build-kani" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "cargo_metadata", @@ -234,7 +234,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.53.0" +version = "0.54.0" dependencies = [ "lazy_static", "linear-map", @@ -432,7 +432,7 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "kani" -version = "0.53.0" +version = "0.54.0" dependencies = [ "kani_core", "kani_macros", @@ -440,7 +440,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.53.0" +version = "0.54.0" dependencies = [ "clap", "cprover_bindings", @@ -461,7 +461,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "cargo_metadata", @@ -489,7 +489,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "home", @@ -498,14 +498,14 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.53.0" +version = "0.54.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.53.0" +version = "0.54.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -515,7 +515,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.53.0" +version = "0.54.0" dependencies = [ "clap", "cprover_bindings", @@ -1034,7 +1034,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" [[package]] name = "std" -version = "0.53.0" +version = "0.54.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 68b5bcc20ff3..f2301983fcb4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.53.0" +version = "0.54.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 aced9e5b9b65..c53ffb207fcf 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 23389c156302..24ed00f54338 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index d58d686d7d43..c57ec8e8e2f2 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.53.0" +version = "0.54.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 816752a58e03..de91900d6d9c 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 1fba7875672a..7d7ced8ee0b7 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.53.0" +version = "0.54.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 5388dcfb9427..8928992c3f16 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.53.0" +version = "0.54.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 42eb37a56584..475e2978df91 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.53.0" +version = "0.54.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index ae70767f6781..9f0d09b0d7bb 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.53.0" +version = "0.54.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 7c8e6eef122a..cd2985e4ad68 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.53.0" +version = "0.54.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"