Skip to content

Upgrade Rust toolchain to nightly-2026-03-01 - #4712

Open
feliperodri wants to merge 1 commit into
model-checking:mainfrom
feliperodri:upgrade-toolchain-2026-03-01
Open

Upgrade Rust toolchain to nightly-2026-03-01#4712
feliperodri wants to merge 1 commit into
model-checking:mainfrom
feliperodri:upgrade-toolchain-2026-03-01

Conversation

@feliperodri

Copy link
Copy Markdown
Member

Advance from nightly-2026-02-18 to nightly-2026-03-01. Several source changes are required to track rustc and rustc_public API changes.

  • Rvalue::ShallowInitBox was removed. Box::new is now lowered as an ordinary library call rather than a box-expression that produced this variant, so exchange_malloc/ShallowInitBox no longer exist in either rustc_public or internal MIR. Remove the now-unmatchable arms in analysis, points-to, check_values, body visitor, internal_mir, the gotoc rvalue codegen, and the llbc backend. Box/Vec/dyn codegen still verifies.

  • IntoQueryParam<DefId> no longer has a blanket impl for &DefId; only the owned type implements it. Dereference &DefId to the Copy DefId at the generics_of, coerce_unsized_info, def_kind, def_path_str, and associated_item_def_ids call sites.

  • VariantDef::idx is now private with no accessor. variants_iter yields variants in declaration order, so reconstruct the VariantIdx from the enumeration index via VariantIdx::to_val in the automatic Arbitrary pass, the Option builders, and the llbc backend.

  • CrateDefItems was removed; its associated_items method is now inherent on TraitDef/ImplDef. Drop the unused import.

  • rustc_driver::default_translator was removed and JsonEmitter::new no longer takes a translator argument. Drop both.

  • TyCtxt::get_all_attrs is now #[deprecated] in favor of rustc_hir::find_attr!, which only matches parsed built-in attributes. Kani inspects unparsed kanitool::* tool attributes, so get_all_attrs remains the correct API; add scoped #[allow(deprecated)] with a comment.

  • Fix new clippy lints on pre-existing code that CI's -D warnings now rejects: an if-in-match guard, iterating a map's keys, an explicit loop counter, and a redundant .into_iter().

Test fixtures:

  • tests/cargo-kani/vecdeque-cve: the rustc_allow_const_fn_unstable feature gate was removed (the #[rustc_allow_const_fn_unstable] attribute still works under rustc_attrs). Drop the #![feature(...)] line.
  • tests/ui/unsupported-annotation: rustc reworded E0433 from "failed to resolve: could not find" to "cannot find".

The charon submodule is left unchanged. It builds against this nightly once scripts/charon-patch.diff is applied, which the llbc CI job already does; cargo build-dev --features cprover --features llbc and ./scripts/kani-llbc-regression.sh (9/9) both pass with the patch applied.

Resolves #4703 and #4707

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

@feliperodri
feliperodri requested a review from a team as a code owner August 4, 2026 02:02
@github-actions github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 4, 2026
@feliperodri feliperodri added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Aug 4, 2026
@feliperodri
feliperodri requested a review from Copilot August 4, 2026 02:12

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🟡 Human review recommended

It upgrades the pinned nightly and touches multiple compiler-internals-facing translation paths (MIR transforms and both backends), which warrants final human verification despite the changes being mostly mechanical.

Pull request overview

Updates Kani’s Rust nightly toolchain to nightly-2026-03-01 and applies the corresponding mechanical source/test adjustments needed to track upstream rustc / rustc_public API and lint changes (notably removal of Rvalue::ShallowInitBox, IntoQueryParam<DefId> reference behavior changes, and VariantDef::idx privacy).

Changes:

  • Bump toolchain to nightly-2026-03-01 and update UI / cargo-kani test fixtures for upstream diagnostic/feature-gate changes.
  • Remove now-unreachable ShallowInitBox handling across MIR transforms and codegen paths.
  • Adapt to API changes around DefId query parameters and variant indexing by reconstructing VariantIdx from enumeration order; address newly-enforced Clippy warnings.
File summaries
File Description
rust-toolchain.toml Bumps pinned nightly from 2026-02-18 to 2026-03-01.
kani-driver/src/list/collect_metadata.rs Removes redundant .into_iter() to satisfy linting / idiomatic iteration.
kani-driver/src/cbmc_property_renderer.rs Reworks property indexing to avoid an explicit loop counter (Clippy).
kani-compiler/src/session.rs Updates JSON emitter construction after default_translator / signature changes.
kani-compiler/src/kani_middle/transform/kani_intrinsics.rs Reconstructs VariantIdx via enumeration index (since VariantDef::idx is private).
kani-compiler/src/kani_middle/transform/internal_mir.rs Drops internal MIR conversion for removed Rvalue::ShallowInitBox.
kani-compiler/src/kani_middle/transform/check_values.rs Removes unreachable ShallowInitBox visitor handling.
kani-compiler/src/kani_middle/transform/body.rs Removes unreachable ShallowInitBox operand visitation.
kani-compiler/src/kani_middle/transform/automatic.rs Reconstructs VariantIdx for enum/struct Arbitrary generation; updates helper signature accordingly.
kani-compiler/src/kani_middle/resolve.rs Adjusts imports and dereferences &DefId at query call sites; drops removed CrateDefItems.
kani-compiler/src/kani_middle/points_to/points_to_analysis.rs Removes unreachable ShallowInitBox handling in points-to analysis match.
kani-compiler/src/kani_middle/coercion.rs Dereferences &DefId at coerce_unsized_info call site.
kani-compiler/src/kani_middle/attributes.rs Adds scoped #[allow(deprecated)] for get_all_attrs (tool attrs), derefs &DefId, and fixes map-key iteration lint.
kani-compiler/src/kani_middle/analysis.rs Removes unreachable ShallowInitBox key classification.
kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs Refactors match arm to satisfy Clippy (if-in-match guard).
kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs Removes ShallowInitBox rvalue codegen path (no longer produced).
kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs Reconstructs VariantIdx during variant translation and removes ShallowInitBox TODO arm.
tests/cargo-kani/vecdeque-cve/src/harness.rs Removes obsolete #![feature(rustc_allow_const_fn_unstable)] gate from fixture.
tests/ui/unsupported-annotation/expected Updates expected diagnostic wording to match new rustc E0433 message.
Review details
  • Files reviewed: 19/19 changed files
  • Comments generated: 0
  • Review effort level: Lite

We're testing this review assessment. Please use 👍 or 👎 to tell us if it's correct.

Advance from nightly-2026-02-18 to nightly-2026-03-01. Several source
changes are required to track rustc and rustc_public API changes.

- `Rvalue::ShallowInitBox` was removed. `Box::new` is now lowered as an
  ordinary library call rather than a box-expression that produced this
  variant, so `exchange_malloc`/`ShallowInitBox` no longer exist in either
  `rustc_public` or internal MIR. Remove the now-unmatchable arms in
  analysis, points-to, check_values, body visitor, internal_mir, the gotoc
  rvalue codegen, and the llbc backend. Box/Vec/dyn codegen still verifies.

- `IntoQueryParam<DefId>` no longer has a blanket impl for `&DefId`; only the
  owned type implements it. Dereference `&DefId` to the `Copy` `DefId` at the
  `generics_of`, `coerce_unsized_info`, `def_kind`, `def_path_str`, and
  `associated_item_def_ids` call sites.

- `VariantDef::idx` is now private with no accessor. `variants_iter` yields
  variants in declaration order, so reconstruct the `VariantIdx` from the
  enumeration index via `VariantIdx::to_val` in the automatic Arbitrary pass,
  the Option builders, and the llbc backend.

- `CrateDefItems` was removed; its `associated_items` method is now inherent
  on `TraitDef`/`ImplDef`. Drop the unused import.

- `rustc_driver::default_translator` was removed and `JsonEmitter::new` no
  longer takes a translator argument. Drop both.

- `TyCtxt::get_all_attrs` is now `#[deprecated]` in favor of
  `rustc_hir::find_attr!`, which only matches parsed built-in attributes.
  Kani inspects unparsed `kanitool::*` tool attributes, so `get_all_attrs`
  remains the correct API; add scoped `#[allow(deprecated)]` with a comment.

- Fix new clippy lints on pre-existing code that CI's `-D warnings` now
  rejects: an `if`-in-`match` guard, iterating a map's keys, an explicit
  loop counter, and a redundant `.into_iter()`.

Test fixtures:
- `tests/cargo-kani/vecdeque-cve`: the `rustc_allow_const_fn_unstable`
  feature gate was removed (the `#[rustc_allow_const_fn_unstable]` attribute
  still works under `rustc_attrs`). Drop the `#![feature(...)]` line.
- `tests/ui/unsupported-annotation`: rustc reworded E0433 from
  "failed to resolve: could not find" to "cannot find".
- `tests/script-based-pre/autoderive_arbitrary_{enums,structs}`: `Eq` gained
  an `assert_fields_are_eq` method, and `derive(Eq)` now emits that instead of
  `assert_receiver_is_total_eq`. Update the autoharness tables (the shorter
  name also re-pads the surrounding ASCII borders). All verification verdicts
  are unchanged.

The `charon` submodule is left unchanged. It builds against this nightly
once `scripts/charon-patch.diff` is applied, which the llbc CI job already
does; `cargo build-dev --features cprover --features llbc` and
`./scripts/kani-llbc-regression.sh` (9/9) both pass with the patch applied.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

[C] Internal Tracks some internal work. I.e.: Users should not be affected. Z-CompilerBenchCI Tag a PR to run benchmark CI 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-2026-02-16 failed

2 participants