Skip to content

Upgrade Rust toolchain to nightly-2026-02-14 - #4683

Merged
feliperodri merged 2 commits into
model-checking:mainfrom
tautschnig:toolchain-2026-02-14-pr
Jul 29, 2026
Merged

Upgrade Rust toolchain to nightly-2026-02-14#4683
feliperodri merged 2 commits into
model-checking:mainfrom
tautschnig:toolchain-2026-02-14-pr

Conversation

@tautschnig

@tautschnig tautschnig commented Jul 28, 2026

Copy link
Copy Markdown
Member

Advance from nightly-2026-02-12 to nightly-2026-02-14. One source change is required (first needed at nightly-2026-02-13); 02-14 then also passes with no further changes.

nightly-2026-02-13 introduces ty::PatternKind::NotNull (used by NonNull), which rustc_public cannot yet convert to its stable representation, so calling the stable Ty::kind() on such a pattern type panics (not yet implemented). Kani's -Z valid-value-checks pass walks every reachable type and hit this.

Detect pattern types via the internal representation (where inspecting the kind is always safe) and derive their validity from the scalar valid_range in their layout ABI, which already captures both range and non-null constraints, instead of matching on the stable kind. Thread tcx through ty_validity_per_offset, try_from_ty, and assignment_check_points for the internal check.

Additionally, two script-based-pre tests regress on this nightly and are addressed here:

  • std_codegen: std itself now uses pattern-typed NonNull, so Kani cannot codegen std at all in this toolchain window — the rustc_public conversion for PatternKind::NotNull is todo!() until it was implemented upstream on nightly-2026-04-29, and it is hit from reachability and codegen paths that cannot work around an unrepresentable type. The test is disabled via the fixme path convention (directory renamed to std_codegen_fixme), with a comment in its config.yml stating that it should be re-enabled once the toolchain reaches nightly-2026-04-29. Note for reviewers: this suspends std-codegen coverage until the toolchain upgrade reaches that nightly.

  • ambiguous_crate: cargo reworded its ambiguous-package-specification error. The expected output is trimmed to the durable lines of the new wording (the current wording contains an upstream typo, "specificationm", which is deliberately not matched so the eventual upstream fix does not break the test again).

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

@tautschnig
tautschnig requested a review from a team as a code owner July 28, 2026 13:32
Copilot AI review requested due to automatic review settings July 28, 2026 13:32
@github-actions github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Jul 28, 2026

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.

Pull request overview

Updates Kani’s Rust nightly toolchain and adjusts the -Z valid-value-checks instrumentation to avoid panicking when encountering newly introduced rustc pattern types (e.g., ty::PatternKind::NotNull used by NonNull) that rustc_public cannot yet convert to its stable Ty::kind() representation.

Changes:

  • Bump toolchain from nightly-2026-02-12 to nightly-2026-02-14.
  • Thread TyCtxt through the valid-value intrinsic generation and validity-walking helpers.
  • Detect pattern types via the internal representation and avoid calling stable Ty::kind() on them during validity analysis.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File Description
rust-toolchain.toml Advances the pinned nightly toolchain version.
kani-compiler/src/kani_middle/transform/kani_intrinsics.rs Passes tcx through valid-value intrinsic generation to support internal pattern-type detection.
kani-compiler/src/kani_middle/transform/check_values.rs Updates validity-range extraction and validity traversal to safely handle pattern types using internal APIs.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread kani-compiler/src/kani_middle/transform/check_values.rs Outdated
Advance from nightly-2026-02-12 to nightly-2026-02-14. One source change is
required (first needed at nightly-2026-02-13); 02-14 then also passes with no
further changes.

nightly-2026-02-13 introduces `ty::PatternKind::NotNull` (used by `NonNull`),
which `rustc_public` cannot yet convert to its stable representation, so calling
the stable `Ty::kind()` on such a pattern type panics (`not yet implemented`).
Kani's `-Z valid-value-checks` pass walks every reachable type and hit this.
Detect pattern types via the internal representation (where inspecting the kind
is safe) and skip them there.

Two script-based-pre tests regress on this nightly and are addressed here:

- std_codegen: std itself now uses pattern-typed `NonNull`, so Kani cannot
  codegen std at all in this toolchain window (rustc_public's conversion is
  `todo!()` until it was implemented upstream on nightly-2026-04-29). The test
  is disabled via the `fixme` path convention with a comment saying when to
  re-enable it.

- ambiguous_crate: cargo reworded the ambiguous-package-specification error;
  the expected output is trimmed to the durable lines of the new wording.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig
tautschnig force-pushed the toolchain-2026-02-14-pr branch from 2dc53c3 to 76c3672 Compare July 28, 2026 19:25
Address review feedback: the early return for pattern types relied on their
validity being fully captured by the scalar valid_range in the layout ABI,
without enforcing that assumption or handling the one case where it does not
hold.

- Pattern types over `char` are now rejected with an unsupported-value error:
  char's validity is two intervals around the surrogate gap, which a single
  scalar range cannot express, and the char special case in `try_from_ty` is
  skipped for pattern types.
- For all other bases, assert that the pattern type has a scalar ABI, which is
  what makes returning only the scalar range requirement complete (integer
  bases add no requirements of their own; the NotNull constraint is part of
  the range).
- Turn the now-unreachable `RigidTy::Pat` traversal arm into an explicit
  `unreachable!` and document why the early-return path fully replaces it.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@feliperodri
feliperodri added this pull request to the merge queue Jul 29, 2026
Merged via the queue into model-checking:main with commit 45dba15 Jul 29, 2026
46 of 50 checks passed
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