Upgrade Rust toolchain to nightly-2024-03-29 #3116

feliperodri · 2024-03-29T16:31:14Z

Resolves #3115.

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 <felisous@amazon.com>

feliperodri · 2024-03-29T16:33:11Z

There are two test cases failing for lack of support for typed_swap. Here are the test cases:

failures:
    [kani] kani/FunctionAbstractions/mem_swap.rs
    [kani] kani/Vectors/any/sorting.rs

Here is the error message:

Failed Checks: typed_swap is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-03-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", line 731, in std::mem::swap::<u32>

@celinval should we open a GitHub issue to track the support for typed_swap and address it on a separate PR, or should we implement it on this one?

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

kani-compiler/src/kani_middle/mod.rs

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

zhassan-aws

Thanks. Regarding typed_swap, I suspect that it'll occur in real code, so I would prefer if we handle it in this PR.

kani-compiler/src/kani_middle/transform/body.rs

zhassan-aws · 2024-03-29T18:50:20Z

For example, the s2n-quic-core regression is failing (likely due to typed_swap): https://github.com/model-checking/kani/actions/runs/8484198509/job/23246699235?pr=3116#step:5:81

celinval · 2024-04-01T20:33:24Z

I agree with @zhassan-aws that this will need to be addressed in this PR.

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

…4-03-29

tools/bookrunner/src/litani.rs

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

kani-compiler/src/kani_middle/mod.rs

tools/bookrunner/src/litani.rs

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

kani-compiler/src/kani_middle/mod.rs

zhassan-aws

LGTM. Thanks!

…4-03-29

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version = "0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in #3081 * Disable removal of storage markers by @zhassan-aws in #3083 * Automatic cargo update to 2024-03-18 by @github-actions in #3086 * Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in #3087 * Upgrade toolchain to nightly-2024-03-15 by @celinval in #3084 * Add optional scatterplot to benchcomp output by @tautschnig in #3077 * Benchcomp scatterplots: quote axis labels by @tautschnig in #3097 * Expand ${var} in benchcomp variant `env` by @karkhaz in #3090 * Add test for #3099 by @zhassan-aws in #3100 * Automatic cargo update to 2024-03-25 by @github-actions in #3103 * Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in #3104 * Implement validity checks by @celinval in #3085 * Add `benchcomp filter` command by @karkhaz in #3105 * Add CI test for --use-local-toolchain by @jaisnan in #3074 * Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in #3102 * Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in #3114 * Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in #3118 * Allow modifies clause for verification only by @feliperodri in #3098 * Automatic cargo update to 2024-04-01 by @github-actions in #3117 * Automatic cargo update to 2024-04-04 by @github-actions in #3122 * Remove bookrunner by @tautschnig in #3123 * Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in #3116 * Remove unnecessary build step for some workflows by @zhassan-aws in #3124 * Ensure storage markers are kept in std code by @zhassan-aws in #3080 **Full Changelog**: kani-0.48.0...kani-0.49.0

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version = "0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in model-checking#3081 * Disable removal of storage markers by @zhassan-aws in model-checking#3083 * Automatic cargo update to 2024-03-18 by @github-actions in model-checking#3086 * Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in model-checking#3087 * Upgrade toolchain to nightly-2024-03-15 by @celinval in model-checking#3084 * Add optional scatterplot to benchcomp output by @tautschnig in model-checking#3077 * Benchcomp scatterplots: quote axis labels by @tautschnig in model-checking#3097 * Expand ${var} in benchcomp variant `env` by @karkhaz in model-checking#3090 * Add test for model-checking#3099 by @zhassan-aws in model-checking#3100 * Automatic cargo update to 2024-03-25 by @github-actions in model-checking#3103 * Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in model-checking#3104 * Implement validity checks by @celinval in model-checking#3085 * Add `benchcomp filter` command by @karkhaz in model-checking#3105 * Add CI test for --use-local-toolchain by @jaisnan in model-checking#3074 * Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in model-checking#3102 * Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in model-checking#3114 * Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in model-checking#3118 * Allow modifies clause for verification only by @feliperodri in model-checking#3098 * Automatic cargo update to 2024-04-01 by @github-actions in model-checking#3117 * Automatic cargo update to 2024-04-04 by @github-actions in model-checking#3122 * Remove bookrunner by @tautschnig in model-checking#3123 * Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in model-checking#3116 * Remove unnecessary build step for some workflows by @zhassan-aws in model-checking#3124 * Ensure storage markers are kept in std code by @zhassan-aws in model-checking#3080 **Full Changelog**: model-checking/kani@kani-0.48.0...kani-0.49.0

feliperodri added 5 commits March 29, 2024 16:25

Upgrade Rust toolchain to nightly-2024-03-29

c89426c

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Correctly use NullOp::UbChecks

6e33108

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Update calls to ty::RawPtr

7d69cab

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Remove use of pretty_ty

0e52fed

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Add #[allow(dead_code)] to avoid spurious warnings

fdf28f6

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri requested a review from a team as a code owner March 29, 2024 16:31

github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Mar 29, 2024

zhassan-aws reviewed Mar 29, 2024

View reviewed changes

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs Outdated Show resolved Hide resolved

kani-compiler/src/kani_middle/mod.rs Outdated Show resolved Hide resolved

Remove dead code

cd134a8

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri requested a review from zhassan-aws March 29, 2024 18:19

zhassan-aws reviewed Mar 29, 2024

View reviewed changes

kani-compiler/src/kani_middle/transform/body.rs Outdated Show resolved Hide resolved

tautschnig self-assigned this Apr 1, 2024

tautschnig and others added 7 commits April 4, 2024 11:33

Update kani-compiler/src/kani_middle/transform/body.rs

851362e

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

fixup! Update kani-compiler/src/kani_middle/transform/body.rs

f93193c

Implement typed_swap intrinsic

31c549d

Merge remote-tracking branch 'origin/main' into toolchain-upgrade-202…

20e1e17

…4-03-29

fixup! Remove use of pretty_ty

c270426

Add #[allow(dead_code)] to keep clippy happy

1b4a535

fixup! fixup! Update kani-compiler/src/kani_middle/transform/body.rs

3077014

tautschnig removed their assignment Apr 4, 2024

feliperodri commented Apr 4, 2024

View reviewed changes

tools/bookrunner/src/litani.rs Outdated Show resolved Hide resolved

Merge branch 'main' into toolchain-upgrade-2024-03-29

85f0818

adpaco-aws reviewed Apr 4, 2024

View reviewed changes

adpaco-aws approved these changes Apr 4, 2024

View reviewed changes

zhassan-aws approved these changes Apr 4, 2024

View reviewed changes

tautschnig added 2 commits April 5, 2024 10:17

Add test for typed_swap

d4abc03

Add typed_swap to documentation

fc083d6

tautschnig added 5 commits April 5, 2024 10:17

fixup! Add test for typed_swap

7344be8

typed_swap: use x, y

518fd07

Check types

4dc6be4

Restore start/end column fields

50d34e6

Merge remote-tracking branch 'origin/main' into toolchain-upgrade-202…

1573607

…4-03-29

tautschnig enabled auto-merge (squash) April 5, 2024 10:20

tautschnig merged commit a589e57 into model-checking:main Apr 5, 2024
23 checks passed

tautschnig mentioned this pull request Apr 5, 2024

Bump Kani version to 0.49.0 #3126

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Upgrade Rust toolchain to nightly-2024-03-29 #3116

Upgrade Rust toolchain to nightly-2024-03-29 #3116

feliperodri commented Mar 29, 2024

feliperodri commented Mar 29, 2024

zhassan-aws left a comment

zhassan-aws commented Mar 29, 2024

celinval commented Apr 1, 2024

zhassan-aws left a comment

Upgrade Rust toolchain to nightly-2024-03-29 #3116

Upgrade Rust toolchain to nightly-2024-03-29 #3116

Conversation

feliperodri commented Mar 29, 2024

feliperodri commented Mar 29, 2024

zhassan-aws left a comment

Choose a reason for hiding this comment

zhassan-aws commented Mar 29, 2024

celinval commented Apr 1, 2024

zhassan-aws left a comment

Choose a reason for hiding this comment