Upgrade Rust toolchain to nightly-2026-08-21 by feliperodri · Pull Request #4768 · model-checking/kani

feliperodri · 2026-08-27T04:12:13Z

Important

Draft: do not review until #4764, #4766 and #4767 are merged.

This is the last link in a four-PR chain, so its diff currently contains the other three:

Commit	What	Lands from
`f22ed96ea`	Upgrade to `nightly-2026-07-01`	#4764
`15da7c42e`	Derive the cargo output directory from cargo's reported artifacts	#4766
`b0062be2c`	Upgrade to `nightly-2026-08-01`	#4767
`80ae6726c`	Upgrade to `nightly-2026-08-21`	this PR — review only this commit

Once the other three land this rebases down to the single nightly-2026-08-21 commit.

Dependencies and merge order

#4760  nightly-2026-06-01   ✅ merged
  └─ #4764  nightly-2026-07-01     ← ready (MERGEABLE, no longer draft)
       └─ #4766  cargo target layout   ← CI green
            └─ #4767  nightly-2026-08-01   ← draft, gated on #4766
                 └─ THIS PR  nightly-2026-08-21

Each link is a genuine dependency, not just sequencing:

Derive the cargo output directory from cargo's reported artifacts #4766 is a hard blocker for everything from 08-01 on. cargo 1.99 changed the layout under target/; without that fix the whole cargo-based flow fails with error: No such file or directory (os error 2).
Upgrade Rust toolchain to nightly-2026-07-01 #4764 and Upgrade Rust toolchain to nightly-2026-08-01 #4767 are sequential toolchain bumps. Skipping them would fold three upgrades into one review, and each carries distinct API adaptations.

Note that two commits in this stack picked up extra call sites from main while I rebased: #4726 landed code using EarlyBinder::bind(value) and tcx.predicates_of(..).predicates, which the 07-01 and 08-01 upgrades respectively replace. I folded each fix into the commit that owns that API change rather than into this one, so every commit in the stack still builds on its own (verified individually — see Testing). #4764 and #4767 will need the same one-line additions when they are rebased on current main.

Description

nightly-2026-08-21 is the first 1.100 nightly. Only 14 compile errors came with it — a much smaller upgrade than 08-01's 91 — but one runtime change broke the entire sysroot. That one first:

1. The sysroot needs `-Zembed-metadata=yes`

Cargo builds Kani's library/std and library/kani with metadata embedding off, so the rlib holds only a metadata stub and the full .rmeta is left behind in the build directory. Kani copies just the rlib into its sysroot and later compiles against it standalone, so every verification failed:

error: only metadata stub found for `rlib` dependency `std`
       please provide path to the corresponding .rmeta file with full metadata

That took out 534 of 607 kani tests. The symptom was visible in the artifacts — the sysroot's libstd.rlib was 1024 bytes, and ar t showed nothing but a stub:

$ ar t target/kani/lib/libstd.rlib
__.SYMDEF
lib.rmeta          # 440 bytes -- the stub
lib.rmeta-link

Asking for full metadata in the sysroot build keeps those rlibs self-contained (they grow to 32 KB / 596 KB) and takes the failures from 534 to 2.

2. Mechanical API adaptations

Change	Adaptation
`LangItem` moved from `rustc_hir` to `rustc_hir::attrs::lang_items`	3 imports, matching the path the compiler itself uses
`CodegenBackend::join_codegen` gained `Option<&IncrCompSession>`	added in both backends
`Analysis::apply_primary_terminator_effect` no longer returns `TerminatorEdges`	the framework computes them itself; drop the return value and the now-unused `'mir` lifetime
`BackendRepr::SimdVector`'s lane count is `BackendLaneCount` (a `NonZero<u16>`), not `u64`	`codegen_vector` calls `as_u64()`
`TargetConfig`'s `target_features` + `unstable_target_features` → one `internal_target_features: UnordSet<Symbol>`	also removes the `FIXME do unstable_target_features properly`, since there is no longer an unstable list
`TyCtxt` no longer implements `rustc_hir_pretty::PpAnn`	the impl is on `&dyn HirTyCtxt`, which `TyCtxt` does implement, so `syn_attr` coerces through it
`evaluate_obligations_error_on_ambiguity` returns a `TraitErrors` enum, not a vector	the emptiness check becomes `no_errors()`
`LocalModDefId` renamed `LocalModId`	rename

3. `fn_abi_of_instance` now refuses LLVM intrinsics

fn_abi_adjust_for_abi asserts that the ABI is not Unadjusted. InstanceKind::LlvmIntrinsic already existed on nightly-2026-08-01 — where computing an ABI for one was still allowed, so codegen could treat it as an ordinary item — but on 1.100 that aborts the compiler:

assertion `left != right` failed: fn_abi_of_instance should not be called on LLVM intrinsics

There is no way to obtain a FnAbi for one: the assert sits in the shared fn_abi_new_uncached, so deriving it from the signature trips it too. Without an ABI Kani cannot codegen the call or even its arguments, and it has no model for LLVM intrinsics anyway, so codegen_funcall now reports the call as an unsupported construct (#4770) before touching the ABI:

call to LLVM intrinsic `llvm.aarch64.neon.uqadd.i64` is not currently supported by Kani.
Please post your example at https://github.com/model-checking/kani/issues/4770

This preserves the earlier behaviour. Before 1.100 these were foreign items (DefKind::Fn declarations in stdarch's extern "unadjusted" blocks), so they went through Kani's FFI shim, which raised an equivalent unsupported-construct check. As then, reaching one fails verification and code that never reaches one still verifies.

4. New `CastKind::BoxDerefTransmute`

An elaborated Box deref that turns the inner pointer into a raw one. Its documentation calls it a regular transmute that is additionally UB if the input is not valid as a Box<T>, and states that backends may treat it as a plain transmute. So codegen and the value checks group it with Transmute (as cranelift does) — Kani checks pointer validity separately at the deref itself. The stable-to-internal conversion maps it faithfully rather than collapsing it to Transmute, because MIR validation distinguishes the two (Cannot BoxDerefTransmute to non-pointer type).

Worth a reviewer's eye: the extra "input not valid as Box<T>" UB is not separately modelled. If we want a dedicated check there, that is a follow-up rather than part of a toolchain bump.

Test changes (3 files)

atomic_load and atomic_store gained a VOLATILE: bool const parameter. Each call passes false, matching what the ordinary atomic types in core pass, and borrows their /* VOLATILE */ annotation so the bare bool reads clearly:

atomic_store::<_, { AtomicOrdering::SeqCst }, /* VOLATILE */ false>(ptr_a1, 0);

I checked every atomic intrinsic signature rather than only the ones the suites happened to flag — no other atomic intrinsic changed (cxchg, cxchgweak, xchg, xadd, xsub, and, nand, or, xor, max, min, umin, umax, fence, singlethreadfence are all unchanged). This matters because 27 of the 29 Intrinsics/Atomic tests are fixme-ignored, so the compiler never type-checks them.

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 (3c3008001):

Suite	Result
`kani`	607 passed, 0 failed (matches the 08-01 baseline exactly)
`cargo-kani`	71 passed, 0 failed
`cargo-ui`	30 passed, 0 failed
`expected`	472 passed, 0 real failures — see below
`ui`	150 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.

Each commit in the stack was checked out and built individually to confirm the rebase left no commit broken.

The LLVM-intrinsic abort was caught by CI on kani/SizeAndAlignOfDst/main_assert.rs, which passes vacuously on macOS (its body is #[cfg(not(target_os = "macos"))]) and so could not reproduce on my machine. I reproduced the same abort locally with a targeted probe instead, confirmed the identical assertion, and confirmed the fix resolves it:

#[kani::proof]
fn check_scalar_saturating_add() {
    use std::arch::aarch64::vqaddd_u64;   // -> llvm.aarch64.neon.uqadd.i64
    let (x, y): (u64, u64) = (kani::any(), kani::any());
    let _ = unsafe { vqaddd_u64(x, y) };
}

Before the fix: signal: 6 (SIGABRT) with fn_abi_of_instance should not be called on LLVM intrinsics. After: the unsupported-construct check shown above.

Two caveats, stated rather than omitted:

expected/shadow/slices/slice_split is unverified locally. It spends >20 minutes in CBMC's SAT solver and I interrupted it. It is not a regression from this upgrade or from 08-01: I timed it on the 07-01 branch as a control and it is equally slow there. CI covers it.
The two ui failures are solver-attribute/cadical and solver-option/cadical, both expecting Solving with CaDiCaL. My local CBMC reports The specified solver, 'cadical', is not available — a missing solver in my environment, independent of the Rust toolchain, and failing identically on 08-01.
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.

A much smaller upgrade than the previous two: no verification behaviour changed, and no test needed adjusting. **`FieldDef` moved to the `crate_def_with_ty!` macro.** Its inherent `ty()` and `ty_with_args()` are now provided by the `CrateDefType` trait, so the 17 call sites just need that trait in scope. This is a pure import change -- the semantics are identical (both still resolve to `def_ty`/`def_ty_with_args`). **`EarlyBinder::bind` takes the interner.** `bind(value)` becomes `bind(tcx, value)` at five sites. **`Terminator` gained MIR-level attributes** (`attributes: ThinVec<AttributeKind>`). The stable representation has no equivalent, and Kani-synthesized terminators carry none, so `internal_mir` passes an empty vector. **`TerminatorKind::Drop` lost `async_fut`**, so that field is dropped from the `internal_mir` conversion. **Work products are an `UnordMap`, not an `FxIndexMap`**, in `CodegenBackend::join_codegen`'s return type (both backends). Full regression run is clean on the first attempt: kani 607/607, cargo-kani 71/71, expected, script-based-pre 68/68, std-checks, cargo-ui, coverage, prusti, smack, kani-docs, json-handler, cargo-coverage, all unit tests, both `-D warnings` clippy gates, the `-D warnings` build, fmt, and the LLBC build.

`cargo_build` hardcoded the compiler output directory as `target/kani/<triple>/debug/deps`, and `cargo_project` then canonicalized it -- so any layout that does not match becomes `error: No such file or directory (os error 2)`. That layout is cargo's to choose, and cargo 1.99 changes it: artifacts no longer share `debug/deps`, each package getting its own `debug/build/PKG/HASH/out/` instead. Artifact discovery was already layout-agnostic (`map_kani_artifact` derives every path from the `filenames` cargo reports), so the hardcoded directory was the only thing tying the driver to the old layout. Derive it from the discovered artifacts instead, and drop the canonicalization: an artifact path is canonical already, and the no-artifacts fallback names a directory cargo had no reason to create. Two tests hardcoded the same layout and are now 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 reports.

nightly-2026-08-01 is the first 1.99 nightly, and 91 compile errors came with it. `Statement`/`Terminator` carry a `SourceInfo`, not a bare `Span` (78 of the 91 errors). A new `synthetic_source_info(span)` helper in `transform/body.rs` documents the choice of the outermost source scope (scope 0, which `Body::new` always allocates) for MIR Kani synthesizes; reads become `.source_info.span`. `predicates_of` became `clauses_of`, returning `GenericClauses` (`parent` + `clauses`) instead of `GenericPredicates` (`parent` + `predicates`). Same shape and same `instantiate`, so this is a rename at the four call sites -- three in `codegen_units.rs` from model-checking#4706/model-checking#4718, one in the LLBC backend. `ty::FnDef`'s generic args are bound, so three `Instance::{try,expect}_resolve` call sites need `.skip_binder()`. `ValueAbi::ScalarPair` became a struct variant with a new `b_offset` field. Two new enum variants: `AssertMessage::NullReferenceConstructed`, handled like `NullPointerDereference` (same property class, description from rustc_public); and `InstanceKind::LlvmIntrinsic`, which codegens like any other item and has no Rust body for reachability to collect. That new variant is why `expected/issue-3571` needed updating. Constructing a null reference (`&*(0 as *const u32)`) used to report "null pointer dereference occurred"; rustc now distinguishes the two and reports "null reference produced". 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. Also adapts to `LocalModDefId` being renamed `LocalModId` and `Region::new_early_param` moving to the `RegionExt` extension trait. Four tests needed adjusting because `std::intrinsics::{size_of,align_of}` are now comptime fns and cannot be called at runtime. The two `DynTrait` tests used `size_of` incidentally, to compare a vtable field against a type's size, so they use `std::mem::size_of`. The two `Intrinsics/ConstEval` tests 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. cargo 1.99 also ships with this nightly and changed the layout under `target/`, which broke the whole cargo-based flow. That fix is not part of this commit: it stands on its own, applies to the current toolchain, and is under review separately.

nightly-2026-08-21 is the first 1.100 nightly. Only 14 compile errors came with it, but one runtime change broke the whole sysroot; see the last item. `LangItem` moved from `rustc_hir` to `rustc_hir::attrs::lang_items`, which is the path the compiler itself now uses. Three import sites. `CodegenBackend::join_codegen` gained an `Option<&IncrCompSession>` parameter, added to both backends. `Analysis::apply_primary_terminator_effect` no longer returns `TerminatorEdges` -- the dataflow framework computes them itself -- so `points_to_analysis` drops the return value and the now-unused `'mir` lifetime. `BackendRepr::SimdVector`'s lane count is a `BackendLaneCount` (a `NonZero<u16>`) rather than a bare `u64`, so `codegen_vector` calls `as_u64()`. `TargetConfig`'s separate `target_features` and `unstable_target_features` `Vec<Symbol>` lists became a single `internal_target_features: UnordSet<Symbol>`. This also removes the `FIXME do unstable_target_features properly`, since there is no longer an unstable list to populate. `TyCtxt` no longer implements `rustc_hir_pretty::PpAnn`; the impl is on `&dyn HirTyCtxt`, which `TyCtxt` does implement, so `syn_attr` coerces through that. `evaluate_obligations_error_on_ambiguity` returns a `TraitErrors` enum instead of a vector, so the emptiness check becomes `no_errors()`. `CastKind::BoxDerefTransmute` is new: an elaborated `Box` deref that turns the inner pointer into a raw one. Its documentation describes it as a regular transmute that is additionally UB if the input is not valid as a `Box<T>`, and says backends may treat it as a plain transmute, so codegen and the value checks group it with `Transmute` -- Kani checks pointer validity separately at the deref. The stable-to-internal conversion maps it faithfully rather than collapsing it to `Transmute`, because MIR validation distinguishes the two. `fn_abi_of_instance` now refuses LLVM intrinsics -- `fn_abi_adjust_for_abi` asserts that the ABI is not `Unadjusted`. `InstanceKind::LlvmIntrinsic` already existed on nightly-2026-08-01, where computing an ABI for one was still allowed, so codegen could treat it as an ordinary item; on 1.100 that aborts the compiler: assertion `left != right` failed: fn_abi_of_instance should not be called on LLVM intrinsics There is no way to get a `FnAbi` for one -- the assert sits in the shared `fn_abi_new_uncached`, so deriving it from the signature trips it too -- and without an ABI Kani cannot codegen the call or even its arguments. Kani has no model for LLVM intrinsics either, so `codegen_funcall` now reports the call as an unsupported construct (model-checking#4770) before touching the ABI. Before 1.100 these were foreign items and went through the FFI shim, which raised an equivalent unsupported-construct check, so this keeps the earlier behaviour: reaching one fails verification, and code that never reaches one still verifies. Also adapts to `LocalModDefId` being renamed `LocalModId`. Finally, the sysroot build now passes `-Zembed-metadata=yes`. Cargo builds these libraries with metadata embedding off, which leaves the rlib holding only a metadata stub and the full `.rmeta` behind in the build directory. Kani copies just the rlib into its sysroot and later compiles against it on its own, so every verification failed with error: only metadata stub found for `rlib` dependency `std` please provide path to the corresponding .rmeta file with full metadata which took out 534 of 607 `kani` tests. Asking for full metadata keeps the sysroot self-contained. Three tests needed adjusting: the `atomic_load` and `atomic_store` intrinsics gained a `VOLATILE: bool` const parameter. Each call passes `false`, matching what the ordinary atomic types in `core` pass, and borrows their `/* VOLATILE */` annotation so the bare bool reads clearly. No other atomic intrinsic changed.

feliperodri added 3 commits August 27, 2026 00:00

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

feliperodri force-pushed the toolchain-2026-08-21 branch from 56f1b5d to 80ae672 Compare August 27, 2026 04:46

Navigation Menu

Uh oh!

Upgrade Rust toolchain to nightly-2026-08-21 - #4768

Upgrade Rust toolchain to nightly-2026-08-21#4768
feliperodri wants to merge 4 commits into
model-checking:mainfrom
feliperodri:toolchain-2026-08-21

feliperodri commented Aug 27, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

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

Uh oh!

Dependencies and merge order

Description

1. The sysroot needs -Zembed-metadata=yes

2. Mechanical API adaptations

3. fn_abi_of_instance now refuses LLVM intrinsics

4. New CastKind::BoxDerefTransmute

Test changes (3 files)

Testing

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

feliperodri commented Aug 27, 2026 •

edited

Loading

1. The sysroot needs `-Zembed-metadata=yes`

3. `fn_abi_of_instance` now refuses LLVM intrinsics

4. New `CastKind::BoxDerefTransmute`