Skip to content

Conversation

zhassan-aws
Copy link
Contributor

Relevant upstream changes:

rust-lang/rust#120675: An intrinsic Symbol is now wrapped in a IntrinsicDef struct, so the relevant part of the code needed to be updated.
rust-lang/rust#121464: The second argument of the create_wrapper_file function changed from a vector to a string.
rust-lang/rust#121662: NullOp::DebugAssertions was renamed to NullOp::UbCheck and it now has data (currently unused by Kani)
rust-lang/rust#121728: Introduces F16 and F128, so needed to add stubs for them
rust-lang/rust#121969: parse_sess was renamed to psess, so updated the relevant code.
rust-lang/rust#122059: The is_val_statically_known intrinsic is now used in some core::fmt code, so had to handle it in (codegen'ed to false).
rust-lang/rust#122233: This added a new retag_box_to_raw intrinsic. This is an operation that is primarily relevant for stacked borrows. For Kani, we just return the pointer.

Resolves #3057

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@zhassan-aws zhassan-aws requested a review from a team as a code owner March 11, 2024 21:54
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Mar 11, 2024
@zhassan-aws zhassan-aws force-pushed the toolchain-2024-03-11 branch from 477fe78 to 0a371ce Compare March 11, 2024 21:58
@zhassan-aws
Copy link
Contributor Author

I ran the main test that has failed the performance regressions (s2n-quic/quic/s2n-quic-core/sync::spsc::tests::alloc_test) 3 times locally with and without the changes, and while there is some slowdown, it's within an acceptable percentage (~9%):
With the toolchain upgrade:

Verification Time: 70.934296s
Verification Time: 70.673645s
Verification Time: 70.516945s

Without the toolchain upgrade:

Verification Time: 64.85171s
Verification Time: 64.96482s
Verification Time: 65.115456s

@celinval celinval merged commit e7a4d83 into model-checking:main Mar 12, 2024
zhassan-aws added a commit that referenced this pull request Mar 13, 2024
These are the original release notes for the reference:

## What's Changed
* Automatic cargo update to 2024-02-26 by @github-actions in
#3043
* Upgrade rust toolchain to 2024-02-17 by @celinval in
#3040
* Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in
#3049
* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in
#3047
* Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in
#3048
* Update s2n-quic submodule by @zhassan-aws in
#3050
* Update s2n-quic submodule weekly through dependabot by @zhassan-aws in
#3053
* Retrieve info for recursion tracker reliably by @feliperodri in
#3045
* Automatic cargo update to 2024-03-04 by @github-actions in
#3055
* Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in
#3052
* Add `--use-local-toolchain` to Kani setup by @jaisnan in
#3056
* Replace internal reverse_postorder by a stable one by @celinval in
#3064
* Add option to override `--crate-name` from `kani` by @adpaco-aws in
#3054
* cargo update and fix macos CI by @zhassan-aws in
#3067
* Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in
#3066
* Upgrade toolchain to 2024-03-11 by @zhassan-aws in
#3071
* Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in
#3063


**Full Changelog**:
kani-0.47.0...kani-0.48.0
@zhassan-aws zhassan-aws deleted the toolchain-2024-03-11 branch June 27, 2024 22:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Toolchain upgrade to nightly-2024-03-02 failed
2 participants