-
Notifications
You must be signed in to change notification settings - Fork 97
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Bump Kani version to 0.57.0 #3777
base: main
Are you sure you want to change the base?
Conversation
Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.56.0"/version = "0.57.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Remove the overflow checks for wrapping_offset by @zhassan-aws in model-checking#3589 * `kani-cov`: A coverage tool for Kani by @adpaco-aws in model-checking#3121 * Automatic toolchain upgrade to nightly-2024-10-04 by @github-actions in model-checking#3570 * Automatic toolchain upgrade to nightly-2024-10-05 by @github-actions in model-checking#3591 * Automatic toolchain upgrade to nightly-2024-10-06 by @github-actions in model-checking#3592 * Exclude Charon from workspace by @zhassan-aws in model-checking#3580 * Support fully-qualified --package arguments by @celinval in model-checking#3593 * Automatic toolchain upgrade to nightly-2024-10-07 by @github-actions in model-checking#3595 * Automatic toolchain upgrade to nightly-2024-10-08 by @github-actions in model-checking#3597 * Automatic cargo update to 2024-10-14 by @github-actions in model-checking#3598 * Bump tests/perf/s2n-quic from `17171ec` to `7752afb` by @dependabot in model-checking#3601 * Automatic toolchain upgrade to nightly-2024-10-09 by @github-actions in model-checking#3600 * Automatic toolchain upgrade to nightly-2024-10-10 by @github-actions in model-checking#3602 * Automatic toolchain upgrade to nightly-2024-10-11 by @github-actions in model-checking#3603 * Loop Contracts Annotation for While-Loop by @qinheping in model-checking#3151 * Automatic toolchain upgrade to nightly-2024-10-12 by @github-actions in model-checking#3604 * Update toolchain to 2024-10-15 by @zhassan-aws in model-checking#3605 * Automatic toolchain upgrade to nightly-2024-10-16 by @github-actions in model-checking#3607 * Implement proper function pointer handling for validity checks by @celinval in model-checking#3606 * Update toolchain to 2024-10-17 by @zhassan-aws in model-checking#3610 * Add fn that checks pointers point to same allocation by @celinval in model-checking#3583 * Automatic toolchain upgrade to nightly-2024-10-18 by @github-actions in model-checking#3613 * [aeneas] Preserve variable names by @zhassan-aws in model-checking#3560 * [Breaking change] Make `kani::check` private by @celinval in model-checking#3614 * Emit an error when proof_for_contract function is not found by @zhassan-aws in model-checking#3609 * Automatic toolchain upgrade to nightly-2024-10-19 by @github-actions in model-checking#3617 * Automatic toolchain upgrade to nightly-2024-10-20 by @github-actions in model-checking#3619 * Update test small_slice_eq by @qinheping in model-checking#3618 * Automatic toolchain upgrade to nightly-2024-10-21 by @github-actions in model-checking#3621 * Automatic cargo update to 2024-10-21 by @github-actions in model-checking#3622 * Bump tests/perf/s2n-quic from `7752afb` to `cd0314b` by @dependabot in model-checking#3625 * Update coverage flag in docs by @zhassan-aws in model-checking#3626 * Automatic toolchain upgrade to nightly-2024-10-22 by @github-actions in model-checking#3628 * Automatic toolchain upgrade to nightly-2024-10-23 by @github-actions in model-checking#3635 * Remove dead Option layer from run_piped by @zhassan-aws in model-checking#3634 * Add `free(0)` to codegen of loop contracts by @qinheping in model-checking#3637 * [Lean] Rename user-facing options from Aeneas to Lean by @zhassan-aws in model-checking#3630 * Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in model-checking#3636 * Automatic toolchain upgrade to nightly-2024-10-24 by @github-actions in model-checking#3639 * Add regular & fixme tests for function contracts by @celinval in model-checking#3371 * Call `goto-instrument` with `DFCC` only once by @qinheping in model-checking#3642 * Build and include `kani-cov` in the bundle by @adpaco-aws in model-checking#3641 * Fix loop contracts transformation when loops in branching by @qinheping in model-checking#3640 * Update toolchain to 10/25 by @carolynzech in model-checking#3648 * Automatic toolchain upgrade to nightly-2024-10-26 by @github-actions in model-checking#3651 * Automatic toolchain upgrade to nightly-2024-10-27 by @github-actions in model-checking#3652 * Bump tests/perf/s2n-quic from `cd0314b` to `ed9db08` by @dependabot in model-checking#3655 * Automatic cargo update to 2024-10-28 by @github-actions in model-checking#3654 * Automatic toolchain upgrade to nightly-2024-10-28 by @github-actions in model-checking#3653 * Reduce the number of object bits for refcell test by @zhassan-aws in model-checking#3656 * Move any_slice_from_array to kani_core by @qinheping in model-checking#3646 * Upgrade toolchain to 2024-10-29 by @zhassan-aws in model-checking#3658 * Add a timeout option by @zhassan-aws in model-checking#3649 * Upgrade toolchain to 2024-10-30 by @tautschnig in model-checking#3661 * Upgrade Rust toolchain to 2024-10-31 by @zhassan-aws in model-checking#3668 * Upgrade toolchain to 2024-11-01 by @tautschnig in model-checking#3671 * Automatic toolchain upgrade to nightly-2024-11-02 by @github-actions in model-checking#3673 * Implement `Arbitrary` for `Range*` by @c410-f3r in model-checking#3666 * Automatic toolchain upgrade to nightly-2024-11-03 by @github-actions in model-checking#3674 * codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in model-checking#3675 * Automatic cargo update to 2024-11-04 by @github-actions in model-checking#3677 * Bump tests/perf/s2n-quic from `192de7d` to `65d55a4` by @dependabot in model-checking#3678 * Update dependencies following Audit workflow failure. by @remi-delmas-3000 in model-checking#3680 * Harness output individual files by @Alexander-Aghili in model-checking#3360 * Update Charon submodule to 2024-11-04 by @zhassan-aws in model-checking#3686 * Add support for float_to_int_unchecked by @zhassan-aws in model-checking#3660 * Change `same_allocation` to accept wide pointers by @celinval in model-checking#3684 * Automatic upgrade of CBMC from 6.3.1 to 6.4.0 by @github-actions in model-checking#3689 * Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in model-checking#3692 * Update cbmc-viewer to 3.10 by @remi-delmas-3000 in model-checking#3683 * Apply loop contracts only if there exists some usage by @qinheping in model-checking#3694 * Remove symtab json support by @celinval in model-checking#3695 * Remove CBMC viewer and visualize option by @zhassan-aws in model-checking#3699 * Ignore derivative in Cargo deny by @qinheping in model-checking#3708 * Upgrade Rust toolchain to 2024-11-08 by @zhassan-aws in model-checking#3703 * Automatic cargo update to 2024-11-11 by @github-actions in model-checking#3704 * Update verify-std-check workflow to enable loop contracts by @qinheping in model-checking#3705 * Automatic toolchain upgrade to nightly-2024-11-09 by @github-actions in model-checking#3709 * Bump tests/perf/s2n-quic from `65d55a4` to `cb41b35` by @dependabot in model-checking#3706 * Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in model-checking#3701 * Upgrade toolchain to nightly-2024-11-11 by @qinheping in model-checking#3710 * Automatic toolchain upgrade to nightly-2024-11-12 by @github-actions in model-checking#3713 * Update charon submodule by @zhassan-aws in model-checking#3716 * Revert "Ignore derivative in Cargo deny" by @qinheping in model-checking#3712 * Upgrade toolchain to nightly-2024-11-13 by @qinheping in model-checking#3715 * Automatic toolchain upgrade to nightly-2024-11-14 by @github-actions in model-checking#3719 * Automatic toolchain upgrade to nightly-2024-11-15 by @github-actions in model-checking#3720 * Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in model-checking#3644 * Improve Kani handling of function markers by @celinval in model-checking#3718 * Automatic toolchain upgrade to nightly-2024-11-16 by @github-actions in model-checking#3722 * Automatic toolchain upgrade to nightly-2024-11-17 by @github-actions in model-checking#3724 * Automatic cargo update to 2024-11-18 by @github-actions in model-checking#3723 * Bump tests/perf/s2n-quic from `cb41b35` to `4c3ba69` by @dependabot in model-checking#3725 * Automatic toolchain upgrade to nightly-2024-11-18 by @github-actions in model-checking#3727 * Enable contracts for const generic functions by @qinheping in model-checking#3726 * List Subcommand Improvements by @carolynzech in model-checking#3729 * Automatic toolchain upgrade to nightly-2024-11-19 by @github-actions in model-checking#3730 * add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in model-checking#3721 * Fix issues with how we compute DST size by @celinval in model-checking#3687 * Bump tests/perf/s2n-quic from `4c3ba69` to `c84ba19` by @dependabot in model-checking#3736 * Fix size and alignment computation for intrinsics by @celinval in model-checking#3734 * Automatic cargo update to 2024-11-25 by @github-actions in model-checking#3735 * Cleanup a few internal compiler deps by @celinval in model-checking#3739 * Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in model-checking#3742 * Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in model-checking#3744 * Update toolchain to nightly-2024-11-26 by @celinval in model-checking#3740 * Automatic upgrade of CBMC from 6.4.0 to 6.4.1 by @github-actions in model-checking#3748 * Automatic cargo update to 2024-12-02 by @github-actions in model-checking#3749 * Update download-artifact, upload-artifact and checkout to v4 by @thanhnguyen-aws in model-checking#3745 * Bump tests/perf/s2n-quic from `c84ba19` to `96d2e22` by @dependabot in model-checking#3750 * Upgrade toolchain to 2024-11-27 by @tautschnig in model-checking#3751 * Upgrade toolchain to 2024-11-28 by @tautschnig in model-checking#3753 * Setup/CI: cleanup Ubuntu 18.04 and cbmc-viewer left-overs and enable 24.04 by @tautschnig in model-checking#3758 * Automatic cargo update to 2024-12-09 by @github-actions in model-checking#3766 * Bump tests/perf/s2n-quic from `96d2e22` to `e4a2365` by @dependabot in model-checking#3767 * Upgrade toolchain to 2024-12-09 by @carolynzech in model-checking#3768 * Add out of bounds check for `offset` intrinsics by @celinval in model-checking#3755 * Upgrade toolchain to 2024-12-12 by @carolynzech in model-checking#3774 * Automatic toolchain upgrade to nightly-2024-12-13 by @github-actions in model-checking#3775 ## New Contributors * @c410-f3r made their first contribution in model-checking#3666 * @workingjubilee made their first contribution in model-checking#3675 * @Alexander-Aghili made their first contribution in model-checking#3360 * @AlgebraicWolf made their first contribution in model-checking#3692 * @thanhnguyen-aws made their first contribution in model-checking#3721 **Full Changelog**: model-checking/kani@kani-0.56.0...kani-0.57.0
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure exactly what our protocol is w.r.t release notes: whether we only delete the toolchain/dependency upgrades and leave the rest, or try to prune further. I made suggestions based on the latter approach, but I do not feel strongly about any of these, so feel free to take or leave them.
Thanks for handling the release this week!
* [aeneas] Preserve variable names by @zhassan-aws in https://github.com/model-checking/kani/pull/3560 | ||
* Emit an error when proof_for_contract function is not found by @zhassan-aws in https://github.com/model-checking/kani/pull/3609 | ||
* [Lean] Rename user-facing options from Aeneas to Lean by @zhassan-aws in https://github.com/model-checking/kani/pull/3630 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we pick one of [aeneas] or [Lean]? (Maybe just [Lean], given the rename)?
### New Contributors | ||
* @c410-f3r made their first contribution in https://github.com/model-checking/kani/pull/3666 | ||
* @workingjubilee made their first contribution in https://github.com/model-checking/kani/pull/3675 | ||
* @Alexander-Aghili made their first contribution in https://github.com/model-checking/kani/pull/3360 | ||
* @AlgebraicWolf made their first contribution in https://github.com/model-checking/kani/pull/3692 | ||
* @thanhnguyen-aws made their first contribution in https://github.com/model-checking/kani/pull/3721 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### New Contributors | |
* @c410-f3r made their first contribution in https://github.com/model-checking/kani/pull/3666 | |
* @workingjubilee made their first contribution in https://github.com/model-checking/kani/pull/3675 | |
* @Alexander-Aghili made their first contribution in https://github.com/model-checking/kani/pull/3360 | |
* @AlgebraicWolf made their first contribution in https://github.com/model-checking/kani/pull/3692 | |
* @thanhnguyen-aws made their first contribution in https://github.com/model-checking/kani/pull/3721 |
IIRC we don't do first-time contributors.
* codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in https://github.com/model-checking/kani/pull/3675 | ||
* Update dependencies following Audit workflow failure. by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3680 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in https://github.com/model-checking/kani/pull/3675 | |
* Update dependencies following Audit workflow failure. by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3680 |
Suggesting we delete changes that don't affect the user experience
* add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3721 | ||
* Fix issues with how we compute DST size by @celinval in https://github.com/model-checking/kani/pull/3687 | ||
* Fix size and alignment computation for intrinsics by @celinval in https://github.com/model-checking/kani/pull/3734 | ||
* Cleanup a few internal compiler deps by @celinval in https://github.com/model-checking/kani/pull/3739 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* Cleanup a few internal compiler deps by @celinval in https://github.com/model-checking/kani/pull/3739 |
* Apply loop contracts only if there exists some usage by @qinheping in https://github.com/model-checking/kani/pull/3694 | ||
* Update verify-std-check workflow to enable loop contracts by @qinheping in https://github.com/model-checking/kani/pull/3705 | ||
* Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in https://github.com/model-checking/kani/pull/3701 | ||
* Revert "Ignore derivative in Cargo deny" by @qinheping in https://github.com/model-checking/kani/pull/3712 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* Revert "Ignore derivative in Cargo deny" by @qinheping in https://github.com/model-checking/kani/pull/3712 |
|
||
* Automatic upgrade of CBMC from 6.3.1 to 6.4.1 | ||
* Rust toolchain upgraded to nightly-2024-12-13 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
* Automatic upgrade of CBMC from 6.3.1 to 6.4.1 | |
* Rust toolchain upgraded to nightly-2024-12-13 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig |
@@ -4,6 +4,63 @@ 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.57.0] | |||
|
|||
### Major/Breaking Changes |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we separate the "Major" and "Breaking" changes? We haven't been consistent in previous releases (some mixed them, and some combined them). But it's more convenient for the reader to have them separated.
* Implement `Arbitrary` for `Range*` by @c410-f3r in https://github.com/model-checking/kani/pull/3666 | ||
* codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in https://github.com/model-checking/kani/pull/3675 | ||
* Update dependencies following Audit workflow failure. by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3680 | ||
* Harness output individual files by @Alexander-Aghili in https://github.com/model-checking/kani/pull/3360 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this should be moved to the "Major Changes" section.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
All four of them? I suggested deleting the middle two since they're just backend changes.
(I agree about the last one, could go either way on the first).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, just pointing to the Harness output one.
* Change `same_allocation` to accept wide pointers by @celinval in https://github.com/model-checking/kani/pull/3684 | ||
* Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in https://github.com/model-checking/kani/pull/3692 | ||
* Apply loop contracts only if there exists some usage by @qinheping in https://github.com/model-checking/kani/pull/3694 | ||
* Update verify-std-check workflow to enable loop contracts by @qinheping in https://github.com/model-checking/kani/pull/3705 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This doesn't have any user impact.
* Fix size and alignment computation for intrinsics by @celinval in https://github.com/model-checking/kani/pull/3734 | ||
* Cleanup a few internal compiler deps by @celinval in https://github.com/model-checking/kani/pull/3739 | ||
* Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in https://github.com/model-checking/kani/pull/3742 | ||
* Setup/CI: cleanup Ubuntu 18.04 and cbmc-viewer left-overs and enable 24.04 by @tautschnig in https://github.com/model-checking/kani/pull/3758 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe move this to "Major Changes" and just rename it to "Add support for Ubuntu 24.04"?
* Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in https://github.com/model-checking/kani/pull/3742 | ||
* Setup/CI: cleanup Ubuntu 18.04 and cbmc-viewer left-overs and enable 24.04 by @tautschnig in https://github.com/model-checking/kani/pull/3758 | ||
* Add out of bounds check for `offset` intrinsics by @celinval in https://github.com/model-checking/kani/pull/3755 | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Updated version in all
Cargo.toml
files (viafind . -name Cargo.toml -exec sed -i 's/version = "0.56.0"/version = "0.57.0"/' {} \;
) and rancargo build-dev
to haveCargo.lock
files updated.GitHub generated release notes:
What's Changed
kani-cov
: A coverage tool for Kani by @adpaco-aws inkani-cov
: A coverage tool for Kani #312117171ec
to7752afb
by @dependabot in Bump tests/perf/s2n-quic from17171ec
to7752afb
#3601kani::check
private by @celinval in [Breaking change] Makekani::check
private #36147752afb
tocd0314b
by @dependabot in Bump tests/perf/s2n-quic from7752afb
tocd0314b
#3625free(0)
to codegen of loop contracts by @qinheping in Addfree(0)
to codegen of loop contracts #3637goto-instrument
withDFCC
only once by @qinheping in Callgoto-instrument
withDFCC
only once #3642kani-cov
in the bundle by @adpaco-aws in Build and includekani-cov
in the bundle #3641cd0314b
toed9db08
by @dependabot in Bump tests/perf/s2n-quic fromcd0314b
toed9db08
#3655Arbitrary
forRange*
by @c410-f3r in ImplementArbitrary
forRange*
#3666192de7d
to65d55a4
by @dependabot in Bump tests/perf/s2n-quic from192de7d
to65d55a4
#3678same_allocation
to accept wide pointers by @celinval in Changesame_allocation
to accept wide pointers #3684Arbitrary
for enums with a single variant by @AlgebraicWolf in DeriveArbitrary
for enums with a single variant #369265d55a4
tocb41b35
by @dependabot in Bump tests/perf/s2n-quic from65d55a4
tocb41b35
#3706cb41b35
to4c3ba69
by @dependabot in Bump tests/perf/s2n-quic fromcb41b35
to4c3ba69
#37254c3ba69
toc84ba19
by @dependabot in Bump tests/perf/s2n-quic from4c3ba69
toc84ba19
#3736c84ba19
to96d2e22
by @dependabot in Bump tests/perf/s2n-quic fromc84ba19
to96d2e22
#375096d2e22
toe4a2365
by @dependabot in Bump tests/perf/s2n-quic from96d2e22
toe4a2365
#3767offset
intrinsics by @celinval in Add out of bounds check foroffset
intrinsics #3755New Contributors
Arbitrary
forRange*
#3666Arbitrary
for enums with a single variant #3692Full Changelog: kani-0.56.0...kani-0.57.0
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.