Skip to content

Update toolchain to nightly-2026-09-22 - #4833

Merged
feliperodri merged 5 commits into
model-checking:mainfrom
feliperodri:toolchain-2026-09-22
Sep 23, 2026
Merged

feliperodri merged 5 commits into
model-checking:mainfrom
feliperodri:toolchain-2026-09-22

Conversation

@feliperodri

@feliperodri feliperodri commented Sep 23, 2026 •

Copy link
Copy Markdown
Member

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 why library/kani still builds. But Kani exposes the feature in a public signature:

pub fn pointer_generator<T, const NUM_ELTS: usize>()
-> PointerGenerator<{ core::mem::size_of::<T>() * NUM_ELTS }>

A crate being verified does not enable the feature, so it gets the new solver and cannot call that function:

error[E0284]: type annotations needed
    = note: cannot satisfy `kani::pointer_generator<T, NUM_ELTS>::{constant#0} == _`

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_exprs and exposing such a signature, one calling it. The caller fails identically, and -Znext-solver=coherence on the caller fixes it.

So this PR passes -Znext-solver=coherence in base_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 from cargo build. Filed as #4832 (high priority) to reimplement pointer_generator without 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.rs started ICEing:

assertion `left == right` failed: Error: assign statement with unequal types
  lhs Pointer { typ: StructTag("tag-Never") } rhs StructTag("tag-Never")

The cause is older than this bump: on an unsupported projection, codegen_place_ref_stable returned 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 derived PartialEq for CoroutineState<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

Change Adaptation
box patterns removed match the pointer, then look through it
rustc_public::abi::ValueAbi → ValueRepr, LayoutShape::abi → value_repr rename
span_bug! moved out of rustc_middle import from rustc_span
RegionExt gone Region::new_early_param is inherent now
CrateType moved to the new rustc_structures crate new extern crate
target_config takes &EarlySession, gained has_reliable_f16b false — CBMC has no bfloat16
Body::function_coverage_info split use coverage_mir_info, which carries the mappings
Diag::emit no longer returns ErrorGuaranteed emit_err
new Float::F16B unimplemented! — f16b is a library type with no tcx.types entry and no CBMC equivalent
new ProjectionElem::PhantomDeref treated as a dereference in the points-to analysis (rust-lang/rust#159103)
the test crate's TestList borrows a slice of references; DynTestFn holds an Arc<dyn Fn> compiletest updated; the closure clones the config it used to move
box patterns removed in Charon too scripts/charon-patch.diff extended 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 emits assert_fields_are_eq for 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 reworked coverage instrumentation (every file under 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 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 carries the same fields, mappings included — 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 through f32::cos() and friends, which still exercise the same CBMC model — both the range bounds and cos(0.0) == 1.0 still hold. Kani's Intrinsic::{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 from format-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.sh passes too (10/10), with the extended Charon patch, and coverage 20/20 plus cargo-coverage 2/2 — cbmc-viewer turned 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.rs unused import in the second commit) — a forced full re-lint is the only honest check. Same shape for compiletest, which reports unchanged tests as ignored rather 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.

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

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.

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 High severity

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.

Comment thread kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
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.
@feliperodri
feliperodri added this pull request to the merge queue Sep 23, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Sep 23, 2026
@feliperodri
feliperodri added this pull request to the merge queue Sep 23, 2026
Merged via the queue into model-checking:main with commit b35a446 Sep 23, 2026
34 checks passed
@feliperodri
feliperodri deleted the toolchain-2026-09-22 branch September 23, 2026 22:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

[I] Refactoring / Clean Up Refactoring or cleaning up of existing code 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-08-22 failed

3 participants