Skip to content

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

Merged
feliperodri merged 3 commits into
model-checking:mainfrom
feliperodri:toolchain-2026-06-01
Aug 26, 2026
Merged

feliperodri merged 3 commits into
model-checking:mainfrom
feliperodri:toolchain-2026-06-01

Conversation

@feliperodri

@feliperodri feliperodri commented Aug 25, 2026 •

Copy link
Copy Markdown
Member

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

Copy link
Copy Markdown
Member Author

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.

@feliperodri
feliperodri added this pull request to the merge queue Aug 26, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 26, 2026
@feliperodri
feliperodri added this pull request to the merge queue Aug 26, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 26, 2026
@feliperodri
feliperodri added this pull request to the merge queue Aug 26, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 26, 2026
@feliperodri
feliperodri enabled auto-merge August 26, 2026 22:14
@feliperodri
feliperodri added this pull request to the merge queue Aug 26, 2026
Merged via the queue into model-checking:main with commit 1b88be0 Aug 26, 2026
34 checks passed
@feliperodri
feliperodri deleted the toolchain-2026-06-01 branch August 26, 2026 23:46
feliperodri added a commit to feliperodri/kani that referenced this pull request Aug 27, 2026
…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.
feliperodri added a commit to feliperodri/kani that referenced this pull request Aug 28, 2026
### 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 added a commit to ivmat/kani that referenced this pull request Sep 24, 2026
## Problem

Since `nightly-2026-04-01`, `NonNull<T>` wraps a `pattern_type!(*const T
is !null)` instead of a bare `*const T`. Since `nightly-2026-06-01`
(model-checking#4760), `rustc_layout_scalar_valid_range_start/end` attributes were
replaced by pattern types more broadly. Autoharness does not recognize
`RigidTy::Pat` — any function whose signature involves a pattern type
(directly or through a struct field) is skipped with "Missing Arbitrary
implementation".

## Solution

**`can_derive_arbitrary` (`mod.rs`)** — recognize `RigidTy::Pat` in both
the struct-field iteration loop and the top-level type match, delegating
to a new helper `pat_base_is_derivable`. Raw-pointer bases (NonNull<T>'s
field) are not supported: the pointee storage would be a local of the
synthesized any() and dangle on return. NonNull is a follow-up PR.

**`call_kani_any_for_ty` (`automatic.rs`)** — generate a value of the
base type, constrain it via assume_scalar_niche, then transmute —
assuming first keeps it valid under -Z valid-value-checks.

## Tests

**Updated `autoharness_niche`**: `Month`, `Schedule`, `PosI8`, and
`check_monthly::<Month>` move from skipped to verified (10/10 functions
pass), satisfying the acceptance criteria in model-checking#4758.

**New `autoharness_pattern_type`**: an integer pattern type as a struct
field and as a top-level argument, run with -Z valid-value-checks.

Resolves model-checking#4758

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

---------

Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>
kasimte pushed a commit to kasimte/kani that referenced this pull request Sep 30, 2026
… length (model-checking#4896)

The nightly-2026-06-01 upgrade (model-checking#4760) disabled
`tests/expected/loop-contract/loop_assigns_for_vec.rs` (renamed to
`loop_assigns_for_vec_fixme`, tracked in model-checking#4761): dropping `v` after the
loop now creates a reference to it, which requires the loop contract to
establish the vector's length, and the natural invariant `v.len() == i *
3 + 3` is rejected ("Rust intrinsic assumption failed").

The length word can instead be read through the same raw pointer the
test's `loop_modifies` clause already uses (`(&v as *const Vec<u8> as
*const usize).add(2)`). With that invariant the test passes again with
its original expected output, so this restores the loop-contract
coverage for `Vec`. The file now documents why the invariant takes this
form.

Manually checked that the test is not vacuous: adding `assert!(v.len()
== 12 && i == 3)` after the loop verifies, while `assert!(v.len() ==
11)` fails.

model-checking#4761 remains open for the `v.len()` form of the invariant.

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

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

3 participants