Update toolchain to nightly-2026-09-22 - #4833
Merged
feliperodri merged 5 commits intoSep 23, 2026
Merged
Conversation
The automation has been stuck since nightly-2026-08-22, so this jumps a
month at once (rustc 1303417c4).
The one non-mechanical change: rustc now enables the next-generation trait
solver by default, and that solver cannot handle `generic_const_exprs`.
rustc silently reverts to the old solver for a crate that enables the
feature, but Kani's library enables it and *exposes* it in
`kani::pointer_generator`'s return type, so crates Kani compiles -- which do
not enable the feature -- could no longer call it (E0284). Pass
`-Znext-solver=coherence`, the same escape hatch rustc uses, for every crate
we compile.
Also fixes a codegen bug the new toolchain exposed: when a projection is
unsupported, `codegen_place_ref_stable` returned a stub typed as the place
rather than as a reference to it, so the caller assigned a value to a
pointer-typed local and Kani panicked. The derived `PartialEq` for
`CoroutineState<u8, !>` reaches that path now.
Mechanical adaptations:
- `box` patterns removed
- `rustc_public::abi::ValueAbi` -> `ValueRepr`, `LayoutShape::abi` ->
`value_repr`
- `span_bug!` moved from `rustc_middle` to `rustc_span`
- `RegionExt` gone; `Region::new_early_param` is inherent now
- `CrateType` moved to the new `rustc_structures` crate
- `target_config` takes `&EarlySession` and gained `has_reliable_f16b`
- `Body::function_coverage_info` split into `coverage_mir_info`
- `Diag::emit` no longer returns `ErrorGuaranteed`; use `emit_err`
- new `Float::F16B` and `ProjectionElem::PhantomDeref` variants
- the `test` crate's `TestList` borrows a slice of references and
`DynTestFn` holds an `Arc<dyn Fn>`
Test updates follow upstream changes: `derive(Eq)` no longer emits
`assert_fields_are_eq` for fieldless types (one fewer autoharness candidate
in the autoderive probes), and the `sinf`/`cosf` float intrinsics were
removed, so those tests go through `f32::cos()` and friends.
Resolves model-checking#4774
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
The LLBC backend retains the removed CrateType import path and will fail its configured CI build.
Get a fresh assessment by requesting another Copilot review.
Review effort: Balanced
Findings: 1
Open (1)
What changed in this PR
Updates Kani to nightly-2026-09-22 and adapts compiler integration to upstream API changes.
Changes:
- Updates rustc APIs, compiletest integration, and test expectations.
- Temporarily pins the legacy trait solver for
pointer_generator. - Corrects unsupported place-reference stub typing.
| File | Description |
|---|---|
rust-toolchain.toml |
Updates the nightly toolchain. |
kani-driver/src/call_single_file.rs |
Adds the temporary solver flag. |
kani-compiler/src/main.rs |
Updates compiler feature and crate imports. |
kani-compiler/src/kani_middle/transform/check_values.rs |
Migrates layout APIs. |
kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs |
Migrates layout APIs. |
kani-compiler/src/kani_middle/stubbing/mod.rs |
Removes obsolete trait import. |
kani-compiler/src/kani_middle/points_to/points_to_graph.rs |
Handles phantom dereferences. |
kani-compiler/src/kani_middle/attributes.rs |
Updates diagnostic emission. |
kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs |
Updates span_bug import. |
kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs |
Adapts backend configuration APIs. |
kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs |
Handles the new bfloat16 variant. |
kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs |
Replaces removed box patterns. |
kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs |
Migrates layout representation APIs. |
kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs |
Corrects unsupported reference stub types. |
kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs |
Updates coverage metadata access. |
tools/compiletest/src/main.rs |
Adapts to the new test harness API. |
tests/script-based-pre/autoderive_arbitrary_structs/structs.expected |
Updates generated harness expectations. |
tests/script-based-pre/autoderive_arbitrary_enums/enums.expected |
Updates generated harness expectations. |
tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs |
Tests f64::sin. |
tests/kani/Intrinsics/Math/Trigonometry/sinf32.rs |
Tests f32::sin. |
tests/kani/Intrinsics/Math/Trigonometry/cosf64.rs |
Tests f64::cos. |
tests/kani/Intrinsics/Math/Trigonometry/cosf32.rs |
Tests f32::cos. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Neither shows up in a default `cargo build-dev`: `codegen_aeneas_llbc` is behind the `llbc` feature, and clippy had cached the `place.rs` result from before the projection change removed its last use of `unwrap_or_return_codegen_unimplemented!`. - drop the now-unused macro import in `codegen/place.rs` - take `CrateType` from `rustc_structures` in the LLBC backend too - extend `scripts/charon-patch.diff`: `box` patterns were removed, so drop the feature gate and rewrite Charon's three uses. The patch already moves Charon to edition 2024, so the `inline_local_panic_functions` site can use a let chain. `kani-llbc-regression.sh` passes (10/10), and both clippy invocations from `format-check.yml` are clean on a forced full re-lint.
`cargo test -p kani --features concrete_playback` failed in CI: doctests are compiled by rustdoc rather than through Kani's driver, so they never see the `-Znext-solver=coherence` that `base_rustc_flags` passes, and the three `PointerGenerator` doctests that call `kani::pointer_generator` hit the same E0284 as any other crate would. Set it via `rustdocflags` instead of adding `#![feature(generic_const_exprs)]` to the examples: users calling `pointer_generator` do not need that feature, so putting it in the docs would be misleading. Tracked for removal alongside the flag itself in model-checking#4832.
rustc reworked coverage instrumentation in this window (every file under
`rustc_mir_transform/src/coverage/` changed), and the regions it emits are
tighter: closing braces, `} else {` and comment lines no longer carry line
counts of their own, and the region marked uncovered inside the unreachable
`if` in `coverage/assert` now spans just the assertion rather than the whole
block.
Kani's side is a straight rename -- the new `Body::coverage_mir_info` has the
same fields the old `function_coverage_info` did, `mappings` included -- so
these are rustc's regions, not lost ones. Uncovered code is still reported as
uncovered in every one of these tests, which is what they exist to check.
`coverage` is 20/20 and `cargo-coverage` 2/2 with the regenerated files.
rajath-mk
approved these changes
Sep 23, 2026
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Sep 23, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.

The nightly toolchain automation has been stuck since nightly-2026-08-22 (#4774), so this jumps a month at once, to nightly-2026-09-22 (rustc
1303417c4). Most of the diff is API churn, but one change deserves a decision rather than a rubber stamp, so I've put it first.The part worth arguing about
rustc now enables the next-generation trait solver by default (rust-lang/rust#160619), and that solver does not support
generic_const_exprs(rust-lang/rust#160895). rustc silently reverts to the old solver for any crate that enables the feature itself — which is whylibrary/kanistill builds. But Kani exposes the feature in a public signature:A crate being verified does not enable the feature, so it gets the new solver and cannot call that function:
I checked that this is upstream behaviour rather than something we do wrong, by reproducing it in two plain crates outside Kani: one enabling
generic_const_exprsand exposing such a signature, one calling it. The caller fails identically, and-Znext-solver=coherenceon the caller fixes it.So this PR passes
-Znext-solver=coherenceinbase_rustc_flags, covering the single-file, cargo and playback flows — the same escape hatch rustc applies for itself. It is a stopgap and I don't want it to become permanent: verified code is now type-checked by the solver rustc is walking away from, so Kani can in principle accept or reject a program differently fromcargo build. Filed as #4832 (high priority) to reimplementpointer_generatorwithout a computed const in its signature and drop the flag. If you would rather reshape that API here instead of bumping first, say so and I'll do that.A codegen bug the bump uncovered
tests/kani/Coroutines/main.rsstarted ICEing:The cause is older than this bump: on an unsupported projection,
codegen_place_ref_stablereturned a stub typed as the place rather than as a reference to it, so the caller assigned a value into a pointer-typed local. The new toolchain reaches that path through the derivedPartialEqforCoroutineState<u8, !>, whose uninhabited variant's field cannot be projected. With the stub given the reference's type, it degrades the way it always should have: an unsupported construct in code CBMC proves unreachable, and the harness verifies. That the projection is reported as "unsupported" rather than "unreachable" is itself wrong, tracked separately in #4831.Mechanical adaptations
boxpatterns removedrustc_public::abi::ValueAbi→ValueRepr,LayoutShape::abi→value_reprspan_bug!moved out ofrustc_middlerustc_spanRegionExtgoneRegion::new_early_paramis inherent nowCrateTypemoved to the newrustc_structurescrateextern cratetarget_configtakes&EarlySession, gainedhas_reliable_f16bfalse— CBMC has no bfloat16Body::function_coverage_infosplitcoverage_mir_info, which carries the mappingsDiag::emitno longer returnsErrorGuaranteedemit_errFloat::F16Bunimplemented!—f16bis a library type with notcx.typesentry and no CBMC equivalentProjectionElem::PhantomDereftestcrate'sTestListborrows a slice of references;DynTestFnholds anArc<dyn Fn>boxpatterns removed in Charon tooscripts/charon-patch.diffextended to drop the feature gate and rewrite its three uses (the patch already moves Charon to edition 2024, so one site can use a let chain)Test expectations, and the upstream change behind each
derive(Eq)no longer emitsassert_fields_are_eqfor fieldless types. I confirmed this by expanding a fieldless and a field-carrying type on both toolchains. Autoharness therefore has one fewer candidate in the autoderive probes (enums 9 → 8, structs 17 → 16); the table column widths shift with the longest row, so those expected files are regenerated rather than hand-edited.rustc_mir_transform/src/coverage/changed), so the regions it emits are tighter: closing braces,} else {and comment lines no longer carry line counts of their own, and the uncovered region inside the unreachableifincoverage/assertnow spans just the assertion rather than the whole block. Kani's side is a straight rename — the newBody::coverage_mir_infocarries the same fields,mappingsincluded — so these are rustc's regions rather than lost ones, and uncovered code is still reported as uncovered in every one of these tests.std::intrinsics::{sinf,cosf}{32,64}were removed upstream. The four trig tests now go throughf32::cos()and friends, which still exercise the same CBMC model — both the range bounds andcos(0.0) == 1.0still hold. Kani'sIntrinsic::{SinF32, CosF64, …}arms are now unreachable dead code; I left them alone rather than widen this PR, happy to strip them if you prefer.What I ran
kani-fmt.sh --check, both clippy invocations fromformat-check.yml, the unit tests, and every applicable compiletest suite with--force-rerun(without which compiletest silently reports unchanged tests as ignored): kani 610/610, expected 478/478, ui 152/152, script-based-pre 75/75, plus cargo-kani, cargo-ui, std-checks, kani-fixme, firecracker, prusti, smack, json-handler, kani-docs — all green.kani-llbc-regression.shpasses too (10/10), with the extended Charon patch, andcoverage20/20 pluscargo-coverage2/2 —cbmc-viewerturned out to be installed here after all.Two things bit me that are worth knowing if you hit them: clippy caches per-crate results, so a passing incremental run can hide a warning in a file you changed earlier (that is the
place.rsunused import in the second commit) — a forced full re-lint is the only honest check. Same shape for compiletest, which reports unchanged tests asignoredrather than re-running them.What I could not run locally: the firecracker codegen check (submodule) and
verify-std, and my CBMC is 6.10.0 against the pinned 6.11.0 — CI covers those.Resolves #4774
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.