Upgrade Rust toolchain to nightly-2026-06-01 by feliperodri · Pull Request #4760 · model-checking/kani

feliperodri · 2026-08-25T17:52:48Z

Description

Bumps rust-toolchain.toml from nightly-2026-05-01 to nightly-2026-06-01. Four upstream changes drive most of this.

1. `Retag` moved onto `Rvalue::Use`

StatementKind::Retag and RetagKind are gone; Rvalue::Use now carries a WithRetag flag instead:

Use(Operand, WithRetag),

Kani never modelled retags (they are Stacked-Borrows/Miri only), so the statement arms are dropped, the flag is ignored when reading a Use, and synthesized Uses pass WithRetag::No. internal_mir's RetagKind conversion becomes a WithRetag one.

2. `Variants::Multiple` stores a `VariantLayout`, not a `LayoutData`

The new type carries only per-field offsets — no FieldsShape (so no field order) and no alignment. Variant layouts now come from Layout::for_variant, which is what rustc_codegen_ssa does and which restores the field order. A new variant_layout helper is used by both the type side (codegen_enum_cases) and the value side (codegen_aggregate), so the goto struct's components and the operands initializing them cannot disagree.

That change bit back: for_variant reports the enum's align for a variant (align: parent.align), which over-pads every variant and inflates the enum. check_vtable_size caught it as an ICE on tests/cargo-kani/iss2857 (48 vs 55 bytes). So codegen_struct_fields/codegen_alignment_padding now take the align explicitly, and a variant's own align is computed as the maximum of its fields' aligns — which is what the per-variant LayoutData used to carry.

3. `rustc_layout_scalar_valid_range_start`/`_end` were removed

Replaced by pattern types, the same move core::num::niche_types made. The tests that define ranged scalar newtypes are converted to std::pat::pattern_type!.

This narrows the layout-niche feature added in #4716: a pattern type is not an ADT and has no Arbitrary implementation, so can_derive_arbitrary cannot synthesize a struct that has one as a field, and locally-defined ranged types are now skipped rather than harnessed. The assumption still works end to end through std::time::Duration (the motivating case from the #3832 triage), and tests/script-based-pre/autoharness_niche pins both halves so the reduced reach is asserted by a test rather than silent. Tracked in #4758 with a concrete fix sketch.

4. New `Rvalue::Reborrow`

User-definable reborrowing of ADTs via CoerceShared. It is documented as a bitwise copy today, but the same docs anticipate it changing memory layout, so codegen reports it as an unsupported construct rather than silently modelling it as a copy. The points-to analysis treats it as pointing wherever its place does.

Assorted API changes

Change	Site
`CodegenBackend` moved `CrateInfo` from `codegen_crate` to `join_codegen`	both backends' `compiler_interface.rs`
`rustc_data_structures::stable_hasher` renamed to `stable_hash`; `HashStable`/`hash_stable` to `StableHash`/`stable_hash`	`reachability.rs`
The `normalize` callback of `ptr_metadata_ty{,_or_tail}` now takes `Unnormalized`	`typ.rs`
More `FieldDef::ty` and `instantiate*` sites need `.skip_normalization()`	`typ.rs`, `intrinsics.rs`
`TagEncoding::Niche`'s `niche_variants` is the lang `RangeInclusive` (public `start`/`last` fields, not methods)	`rvalue.rs`, `statement.rs`
New `useless_borrows_in_formatting` clippy lint	11 sites across the workspace

Test change worth calling out

vtable_size_align_drop no longer asserts the exact identity of the vtable's drop pointer. Traced with Kani's debug logging: the drop-glue shim is now core::ptr::drop_glue::<T> rather than core::ptr::drop_in_place::<T>, and drop_glue is not nameable from source. It checks the slot is populated instead; the size and align fields the test is named for are unchanged. This weakens the test — it no longer checks the slot holds the drop glue for the right type — so it is tracked in #4759 with options for restoring that coverage.

Both of these failures were confirmed to be genuine nightly-2026-06-01 regressions rather than pre-existing fragility, by rebuilding the parent commit against nightly-2026-05-01, where both pass.

`drop_in_place` now takes a reference to reach the drop glue

Related to the same rename: core::ptr::drop_in_place used to be the drop lang item, with its body replaced wholesale by the compiler. It is now a wrapper that calls the new drop_glue lang item through &mut *to_drop, and creating that reference asserts the pointee is aligned and valid — so dropping through a raw pointer carries a precondition it did not before.

That surfaced in expected/loop-contract/loop_assigns_for_vec.rs, whose loop_modifies havocs the word holding v.len() while the invariant only constrains i; the drop after the loop then sees an unconstrained length. Strengthening the invariant with v.len() == i * 3 + 3 is rejected (Rust intrinsic assumption failed), so expressing what the drop needs looks like a loop-contracts limitation rather than something this PR can fix. The test is renamed loop_assigns_for_vec_fixme.rs with the analysis recorded in the file, tracked in #4761. Verified that Vec's internal layout is unchanged, so the test's hard-coded .add(2) offset for len is still correct.

Two contract tests that deliberately pin a total check count needed their numbers updated: capture_load_checks_elided 36 → 34 and capture_load_user_deref_pass 60 → 58 (two checks in read_answer's own body became unreachable). In both cases the assertion the test actually exists for still holds — no user-facing pointer_dereference group came back in the first, and the pinned {closure#3}::{closure#0}.pointer_dereference.1 - Status: SUCCESS is still present in the second — so the counts were updated with a note in each test explaining that the total is plumbing-sensitive and what it still guards against.

Testing

Local, macOS aarch64, CBMC 6.10.0 (cbmc-6.9.0-214-g45436eea34), all re-run after rebasing onto current main (which now includes #4717, whose new Rvalue::Use construction site also needed the WithRetag argument):

Suite	Result
`kani`	607 passed, 0 failed, 23 ignored
`cargo-kani`	71 passed, 0 failed
`script-based-pre`	68 passed, 0 failed, 1 ignored
`std-checks`	5 passed, 0 failed
`cargo-ui`	30 passed, 0 failed
`coverage`	20 passed, 0 failed
`ui`	151 passed, 2 failed — both the `cadical` tests, see below
`expected`	474 passed, 0 failed, 16 fixme/ignored
`prusti` / `smack` / `kani-docs` / `json-handler` / `cargo-coverage` / `firecracker`	8 / 40 / 13 / 5 / 2 / 0 passed, 0 failed

Other gates, all clean:

cargo build-dev
cargo build-dev -- --features cprover --features llbc
cargo clippy --workspace --tests and RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace
./scripts/kani-fmt.sh --check
RUSTFLAGS="-D warnings" cargo build --no-default-features --features cprover
Unit tests: cprover_bindings, kani-compiler, kani-driver, kani_metadata, kani --features concrete_playback, kani_macros

Environment caveat: this CBMC build has no cadical, so ui/solver-{attribute,option}/cadical fail locally on output text only ("The specified solver, 'cadical', is not available"), and expected/shadow/slices/slice_split is very slow under the MiniSat fallback. Both are expected to be clean on CI.

Towards #4758, #4759, #4761.

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

Four upstream changes drive most of this. **Retag moved onto `Rvalue::Use`.** `StatementKind::Retag` and `RetagKind` are gone; `Rvalue::Use` now carries a `WithRetag` flag instead. Kani never modelled retags (they are Stacked-Borrows/Miri only), so the statement arms are dropped, the flag is ignored when reading a `Use`, and synthesized `Use`s pass `WithRetag::No`. `internal_mir`'s `RetagKind` conversion becomes a `WithRetag` one. **`Variants::Multiple` stores a `VariantLayout`, not a `LayoutData`.** The new type carries only per-field offsets -- no `FieldsShape` (so no field order) and no alignment. Variant layouts now come from `Layout::for_variant`, which is what `rustc_codegen_ssa` does and restores the field order; a new `variant_layout` helper is used by both the type side (`codegen_enum_cases`) and the value side (`codegen_aggregate`) so the goto struct's components and the operands initializing them cannot disagree. `for_variant` reports the *enum's* align for a variant (`align: parent.align`), which would over-pad every variant and inflate the enum -- caught by `check_vtable_size` on `tests/cargo-kani/iss2857` (48 vs 55 bytes). So `codegen_struct_fields`/`codegen_alignment_padding` now take the align explicitly, and a variant's own align is computed as the maximum of its fields' aligns, which is what the per-variant `LayoutData` used to carry. **`rustc_layout_scalar_valid_range_start`/`_end` were removed** in favour of pattern types, the same move `core::num::niche_types` made. The tests that define ranged scalar newtypes are converted to `std::pat::pattern_type!`. Note the consequence for autoharness: a pattern type is not an ADT and has no `Arbitrary` implementation, so `can_derive_arbitrary` cannot synthesize a struct that has one as a field, and locally-defined ranged types are now skipped rather than harnessed. The niche assumption added in model-checking#4716 is still exercised end to end through `std::time::Duration`; `tests/script-based-pre/autoharness_niche` pins both halves so the reduced reach is asserted rather than silent. **New `Rvalue::Reborrow`** (user-definable reborrowing of ADTs via `CoerceShared`). It is documented as a bitwise copy today, but the same docs anticipate it changing memory layout, so codegen reports it as an unsupported construct rather than silently modelling it as a copy. The points-to analysis treats it as pointing wherever its place does. Also adapts to: the `CodegenBackend` trait moving `CrateInfo` from `codegen_crate` to `join_codegen` (both backends), `rustc_data_structures:: stable_hasher` being renamed to `stable_hash` with `HashStable`/`hash_stable` becoming `StableHash`/`stable_hash`, the `normalize` callback of `ptr_metadata_ty{,_or_tail}` now taking `Unnormalized`, more `FieldDef::ty` and `instantiate*` sites needing `.skip_normalization()`, `TagEncoding::Niche`'s `niche_variants` becoming the lang `RangeInclusive` (public `start`/`last` fields), and the new `useless_borrows_in_formatting` clippy lint. The `vtable_size_align_drop` test no longer asserts the exact identity of the vtable's drop pointer: the drop-glue shim is now `core::ptr::drop_glue::<T>` rather than `core::ptr::drop_in_place::<T>`, and `drop_glue` is not nameable from source. It checks the slot is populated instead; the size and align fields that the test is named for are unchanged.

feliperodri · 2026-08-25T22:16:07Z

The next upgrade, nightly-2026-07-01, is up as a draft in #4764 stacked on this one. It is much smaller (no verification behaviour changed and no test needed adjusting) and should be reviewed once this lands.

…del-checking#4766) ## Description `cargo_build` hardcoded the compiler output directory as `target/kani/<triple>/debug/deps`, and `cargo_project` then canonicalized it. That layout is cargo's to choose, and **cargo 1.99 changes it**: artifacts no longer share `debug/deps` — each package gets its own `debug/build/PKG/HASH/out/` — so `debug/deps` is never created and the canonicalize fails: ``` error: No such file or directory (os error 2) ``` Artifact *discovery* was already layout-agnostic: `map_kani_artifact` derives every path from the `filenames` that cargo reports. The hardcoded directory was the only thing tying the driver to the old layout. This PR: - Derives `CargoOutputs::outdir` from the discovered artifacts instead of assuming a path. - Drops the `canonicalize` in `cargo_project`. An artifact path is canonical already (`Artifact::try_new` canonicalizes), and the no-artifacts fallback names a directory cargo had no reason to create — canonicalizing it turns a benign case into a hard error. - Makes two tests layout-agnostic: `check-output` searches the target directory for its `--gen-c` output, and `cargo_playback_opts` asserts only the *file name* of the executable whose path cargo itself reports. Note that with cargo 1.99 a multi-package build no longer has a single output directory. `outdir` names one of them; it feeds only the `output_dir` field of the `-Z unstable-options` JSON frontend, and previously named a directory that under 1.99 does not exist at all. The doc comment says so explicitly. The layout change, confirmed locally on nightly-2026-08-01 (cargo 1.99.0-nightly): ``` # cargo 1.97 target/kani/<triple>/debug/deps/<pkg>-<hash>.kani-metadata.json # cargo 1.99 -- one directory per package, no debug/deps at all target/kani/<triple>/debug/build/<pkg>/<hash>/out/<pkg>-<hash>.kani-metadata.json ``` ## Why this is a standalone PR This unblocks the toolchain upgrade chain. It has no dependency on any toolchain bump and is behaviour-preserving on the current toolchain, so it can land on its own. The intended order is model-checking#4760 (2026-06-01) → model-checking#4764 (2026-07-01) → this PR → the 2026-08-01 bump, which is blocked on it. ## Testing **On the current toolchain (nightly-2026-05-01, cargo 1.97 — old layout):** - `cargo-kani`: 71 passed, 0 failed - `script-based-pre`: 70 passed, 2 failed — both failures (`cargo_autoharness_filter`, `cargo_autoharness_slices`) reproduce on unmodified `main` and are unrelated to this change - `cargo test -p kani-driver`: 93 passed - `./scripts/kani-fmt.sh --check`, `cargo clippy --workspace --tests -- -D warnings`, `RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings`: clean **Cherry-picked onto the local 2026-08-01 branch (cargo 1.99 — new layout), which is where the bug bites:** | Suite | Before | After | |---|---|---| | `cargo-kani` | 68 failed | **71 passed, 0 failed** | | `script-based-pre` | 11 failed | **68 passed, 0 failed** | - Was this change tested? **Yes** - Is this a breaking change? **No** By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

### Description Bumps `rust-toolchain.toml` from `nightly-2026-07-01` to `nightly-2026-08-01`, the first 1.99 nightly. 91 compile errors came with it. #### 1. `Statement`/`Terminator` carry a `SourceInfo`, not a bare `Span` (78 of the 91 errors) ```rust // nightly-2026-07-01 pub struct Statement<'tcx> { pub source_info: SourceInfo, .. } // Terminator: span only // nightly-2026-08-01 -- both carry SourceInfo (span + source scope) ``` A new helper in `transform/body.rs` keeps the choice of scope in one documented place rather than spreading a bare `scope: 0` across ~78 sites: ```rust /// The `SourceInfo` for a statement or terminator that Kani synthesizes at `span`. /// /// As of nightly-2026-08-01 `Statement` and `Terminator` carry a `SourceInfo` (span plus source /// scope) instead of a bare `Span`. Kani-synthesized MIR does not belong to any inlined scope, so /// it uses the outermost one -- scope 0, which `Body::new` always allocates. pub fn synthetic_source_info(span: Span) -> SourceInfo { SourceInfo { span, scope: 0 } } ``` Reads become `.source_info.span`. #### 2. `predicates_of` became `clauses_of` Returns `GenericClauses` (`parent` + `clauses`) instead of `GenericPredicates` (`parent` + `predicates`). Same shape and same `instantiate`, so this is a rename at four call sites — three in `codegen_units.rs` from model-checking#4706/model-checking#4718, one in the LLBC backend. #### 3. `ty::FnDef`'s generic args are bound Three `Instance::{try,expect}_resolve` call sites need `.skip_binder()`. #### 4. `ValueAbi::ScalarPair` became a struct variant With a new `b_offset` field. #### 5. Two new enum variants - `AssertMessage::NullReferenceConstructed` — handled like `NullPointerDereference`: same property class, description taken from `rustc_public` rather than hardcoded. - `InstanceKind::LlvmIntrinsic` — codegens like any other item, and has no Rust body for reachability to collect. Plus `LocalModDefId` renamed to `LocalModId`, and `Region::new_early_param` moving to the `RegionExt` extension trait. ### Test changes (5 files) **`std::intrinsics::{size_of,align_of}` are now comptime fns** and cannot be called at runtime, which affected four tests: - `tests/kani/DynTrait/{nested_boxes,vtable_size_align_drop}.rs` used `size_of` incidentally, to compare a vtable field against a type's size — switched to `std::mem::size_of`. - `tests/kani/Intrinsics/ConstEval/{size_of,align_of}.rs` exist to check the intrinsics themselves, so each call is bound to a `const` — which is what that directory is about, and the only way now legal. **`expected/issue-3571` — a genuine behaviour change worth flagging.** Constructing a null reference (`&*(0 as *const u32)`) used to report `null pointer dereference occurred`; rustc now distinguishes constructing a null reference from dereferencing a null pointer and reports `null reference produced`. rustc also emits a new `misaligned pointer to reference cast` check at the same site. The UB is still caught and the harness still fails — only the wording is more precise — so the expectation follows rustc's message rather than pinning the old one. No other test needed adjusting, and no verification behaviour changed. ### Testing Local, macOS aarch64, CBMC 6.10.0 (`cbmc-6.9.0-214-g45436eea34`), on the stack rebased onto current `main` (which now includes model-checking#4760): | Suite | Result | |---|---| | `kani` | **607 passed, 0 failed** | | `cargo-kani` | **71 passed, 0 failed** | | `cargo-ui` | **30 passed, 0 failed** | | `expected` | 471 passed, 2 failed — see below | | `ui` | 151 passed, 2 failed — environmental, see below | Also clean: both the CPROVER and LLBC builds, `cargo clippy --workspace --tests -- -D warnings`, `RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings`, and `./scripts/kani-fmt.sh --check`. The two `expected` failures were run before the fix above and are accounted for: - `expected/issue-3571` — the null-reference wording change; **fixed in this PR**, verified passing. - `expected/shadow/slices/slice_split` — I interrupted this one to let the suite finish. It is **not** an 08-01 regression: I timed it on the 07-01 branch as a control and it is equally slow there (>20 min in CBMC's SAT solver on both), so it is a slow test on this machine rather than anything this upgrade introduced. CI covers it. The two `ui` failures are `solver-attribute/cadical` and `solver-option/cadical`, both expecting `Solving with CaDiCaL`. My local CBMC build reports `The specified solver, 'cadical', is not available. The default solver will be used instead.` — a missing solver in my environment, independent of the Rust toolchain. - Was this change tested? **Yes** - Is this a breaking change? **No** By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

feliperodri requested review from a team as code owners August 25, 2026 17:52

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 25, 2026

This was referenced Aug 25, 2026

Autoharness: generate values for pattern-type fields, restoring layout-niche coverage for user-defined ranged types #4758

Open

vtable_size_align_drop no longer checks the drop slot holds the right type's drop glue #4759

Open

feliperodri force-pushed the toolchain-2026-06-01 branch from 2ae175e to 8189db1 Compare August 25, 2026 18:14

feliperodri mentioned this pull request Aug 25, 2026

loop_modifies over a Vec no longer establishes drop_in_place's new reference-creation precondition #4761

Open

feliperodri force-pushed the toolchain-2026-06-01 branch 2 times, most recently from 08a421d to fa20876 Compare August 25, 2026 19:17

feliperodri force-pushed the toolchain-2026-06-01 branch from fa20876 to 110a309 Compare August 25, 2026 21:06

feliperodri enabled auto-merge August 25, 2026 21:13

feliperodri assigned celinval and rajath-mk Aug 25, 2026

feliperodri mentioned this pull request Aug 25, 2026

Upgrade Rust toolchain to nightly-2026-07-01 #4764

Merged

rajath-mk approved these changes Aug 26, 2026

View reviewed changes

feliperodri added this pull request to the merge queue Aug 26, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 26, 2026

feliperodri added this pull request to the merge queue Aug 26, 2026

feliperodri unassigned celinval and rajath-mk Aug 26, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 26, 2026

feliperodri added this pull request to the merge queue Aug 26, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 26, 2026

feliperodri added 2 commits August 26, 2026 17:28

Merge branch 'main' into toolchain-2026-06-01

aa368bc

Add WithRetag argument to Rvalue::Use sites merged from main

439db28

feliperodri enabled auto-merge August 26, 2026 22:14

feliperodri added this pull request to the merge queue Aug 26, 2026

feliperodri mentioned this pull request Aug 26, 2026

Derive the cargo output directory from cargo's reported artifacts #4766

Merged

Merged via the queue into model-checking:main with commit 1b88be0 Aug 26, 2026
34 checks passed

feliperodri deleted the toolchain-2026-06-01 branch August 26, 2026 23:46

feliperodri mentioned this pull request Aug 27, 2026

Upgrade Rust toolchain to nightly-2026-08-01 #4767

Merged

Navigation Menu

Uh oh!

Upgrade Rust toolchain to nightly-2026-06-01 - #4760

Upgrade Rust toolchain to nightly-2026-06-01#4760
feliperodri merged 3 commits into
model-checking:mainfrom
feliperodri:toolchain-2026-06-01

feliperodri commented Aug 25, 2026 •

edited

Loading

Uh oh!

feliperodri commented Aug 25, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

feliperodri commented Aug 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

1. Retag moved onto Rvalue::Use

2. Variants::Multiple stores a VariantLayout, not a LayoutData

3. rustc_layout_scalar_valid_range_start/_end were removed

4. New Rvalue::Reborrow

Assorted API changes

Test change worth calling out

drop_in_place now takes a reference to reach the drop glue

Testing

Uh oh!

feliperodri commented Aug 25, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

feliperodri commented Aug 25, 2026 •

edited

Loading

1. `Retag` moved onto `Rvalue::Use`

2. `Variants::Multiple` stores a `VariantLayout`, not a `LayoutData`

3. `rustc_layout_scalar_valid_range_start`/`_end` were removed

4. New `Rvalue::Reborrow`

`drop_in_place` now takes a reference to reach the drop glue