Upgrade Rust toolchain to 2025-12-31#4624
Merged
tautschnig merged 9 commits intoJul 9, 2026
Merged
Conversation
Relevant upstream PR: - rust-lang/rust#148602 (misc coercion cleanups and handle safety correctly) Resolves: model-checking#4623
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This PR upgrades Kani’s pinned Rust nightly toolchain to nightly-2025-12-16 and applies the minimal source updates needed to stay compatible with upstream rustc MIR changes (notably PointerCoercion::ReifyFnPointer now carrying a safety value).
Changes:
- Bump
rust-toolchain.tomlfromnightly-2025-12-05tonightly-2025-12-16. - Update StableMIR → internal rustc MIR conversion to pass through the new
ReifyFnPointer(safety)payload. - Adjust pattern matches in reachability collection and CPROVER codegen to account for the new
ReifyFnPointer(_)shape.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| rust-toolchain.toml | Updates the pinned nightly toolchain version to 2025-12-16. |
| kani-compiler/src/kani_middle/transform/internal_mir.rs | Converts ReifyFnPointer(safety) into the corresponding rustc internal PointerCoercion with safety preserved. |
| kani-compiler/src/kani_middle/reachability.rs | Updates MIR pattern matching for ReifyFnPointer(_) during mono-item collection. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | Updates codegen pattern matching for ReifyFnPointer(_) in pointer-cast handling. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
feliperodri
approved these changes
Jul 8, 2026
rust-lang/rust#149401 fixed rustc_public's `Instance::name()` (and `CrateItem::name()`) to return the true absolute path, which now includes the crate name for *local* items too (e.g. `my_crate::my_fn` instead of `my_fn`, and `<my_crate::T as my_crate::Tr>::m` instead of `<T as Tr>::m`). Kani feeds these names into user-facing output ("Checking harness ...", "Verification failed for - ...", stubbing diagnostics) and into CBMC symbol pretty-names ("in function ..."), so the bump to nightly-2025-12-16 made ~160 `expected` tests fail on the newly crate-qualified names. Add `strip_local_crate_prefix` (and the `readable_name` wrapper) in kani_middle, which removes the local crate name at each path-component *qualifier* position (start, or after a delimiter such as `<`, `,`, ` `), while preserving continuation segments after `::` so a module/item that shares the crate's name (e.g. crate `main` with `fn main`) is not over-stripped. Non-local paths (`std::...`) are unaffected. Apply it at the harness pretty-name, function/static symbol pretty-name, current-function readable name, and the two stubbing diagnostics. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
rust-lang/rust#148717 ("Point at span within local macros even when error happens in nested external macro") changed how macro-originated errors are rendered, so the E0080 const-eval error for `PointerGenerator::<0>` now points at different spans and adds a "this error originates in the macro ..." note. Replace the brittle consecutive-line block with the stable, essential lines (the E0080 message, the failing const, the instantiation note, and the offending call), which still assert the misuse fails to compile while being robust to future diagnostic reformatting. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The contract-recursion tests (e.g. generic_infinity_recursion, gcd_rec_simple_pass) regressed on nightly-2025-12-16: the recursive-call precondition was spuriously falsifiable. Root cause is the same rust-lang/rust#149401 name change: `find_recursion_tracker` builds the `--nondet-static-exclude` value from `static_item.name()`, which is now crate-qualified (`t::foo::{closure#0}::REENTRY`). CBMC matches that value against the static's crate-relative pretty name, so the qualified value no longer matches, `REENTRY` is not excluded from `--nondet-static`, and the recursion tracker is havocked to a nondet value. With `REENTRY` nondet the top-level contract call can take the REPLACE path (which *asserts* the precondition) instead of the CHECK path (which *assumes* it), so the precondition fails on a nondet input. Strip the local crate prefix here too (matching `readable_name`), restoring the match. Verified: the full `expected` suite is green again. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Adapt kani-compiler to the rustc/rustc_public API changes in this window: - rust-lang/rust#148766 (mir-const-runtime-checks): `Rvalue::NullaryOp` and `NullOp` were removed; `SizeOf`/`AlignOf`/`OffsetOf` become `mir::ConstValue` and the `ub_checks`/`contract_checks`/`overflow_checks` flags move to a new `Operand::RuntimeChecks(RuntimeChecks)`. Drop the `NullaryOp` match arms and handle `Operand::RuntimeChecks` everywhere `Operand` is matched (codegen it to `false`, as the old `NullOp::RuntimeChecks` was; treat it as a no-op in the points-to / uninit / MIR-internalization visitors). - rust-lang/rust#150116: `FieldsShape::Arbitrary::memory_index` renamed to `in_memory_order` (Kani only uses its length). - New `ValueAbi::ScalableVector` variant handled in the valid-value analysis. - rust-lang/rust#6d6068f6c5b (stabilize annotate-snippet): `HumanReadableErrorType` became a struct `{ short, unicode }` instead of an enum with a `Default` variant. Main suites pass on 12-31: expected (458), ui (144), kani (589), 0 failures. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Extend the rust-lang/rust#149401 crate-prefix stripping (`strip_local_crate_prefix` / `readable_name`) to the stubbing validation error messages that still emitted crate-qualified item names, which broke the `ui` stubbing tests: the arity- and generic-parameter-mismatch errors, the trait-mismatch ("cannot be stubbed by") error, the "does not have a body" resolution notes, and the "stub verified target ... does not have a corresponding proof_for_contract harness" error. The `ui` suite is green again (144 passed, 0 failed). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Three follow-ups from the nightly-2025-12-31 bump surfaced by CI: - clippy `result_large_err` on `ensure_non_empty_span`: the `Err` type is rustc's `SpanSnippetError`, which grew and now trips the lint. `#[allow]` it (we can't shrink an upstream type). - LLBC backend (`--features llbc`, not built in the default job): its `translate_operand` needs an arm for the new `Operand::RuntimeChecks` (rust-lang/rust#148766); left as `todo!()` like the backend's other unmodeled cases. - The stub-cycle error ("Stub configuration for harness `..` has a cycle") also embedded a crate-qualified harness name (rust-lang/rust#149401); strip it, fixing cargo-kani/stubbing-double-extern-path. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
rust-lang/rust#149401 made `name()` crate-qualify local items, which broke the autoharness and `list` features: - metadata.rs: the automatic-contract-harness lookup matched the (now crate-relative) harness `target_fn` against the fully-qualified `ContractedFunction.function`, panicking on the `.unwrap()`. Store all contract/harness names crate-relative so display and lookup are consistent. - codegen_units.rs: strip the crate prefix from the autoharness `chosen` and `skipped` function names (the `Selected Function` list column), and from the autoharness filter name, which #149401 had made doubly crate-qualified (`crate::crate::fn`). Fixes the script-based-pre autoharness/list/autoderive regression tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The updated std (nightly-2025-12-31) exercises `unsized_fn_params` in alloc,
e.g. `impl SpecExtendStr for [&str] { fn spec_extend_into(self, ...) }`, which
takes an unsized `self: [&str]` by value. Kani codegened such arguments as their
bare unsized type, which lowers to an incomplete `FlexibleArray`; that cannot be
a function parameter (`as_parameter` asserts `can_be_lvalue`) and drops the
length/vtable metadata, causing an ICE while codegenning the standard library.
Represent unsized-by-value arguments as fat pointers instead (matching the ABI):
- fn_typ: parameter type is the fat pointer (`codegen_ty_ref_stable`).
- codegen_declare_variables + codegen_local: declare/emit the arg local as a fat
pointer, keyed off the new `is_unsized_by_value_arg` helper (which uses the
`arg_count` now tracked in `CurrentFnCtx`).
- codegen_place_stable: model the base local as `*(&local)` by applying a `Deref`
projection, reusing the existing fat-pointer projection logic so reads,
indexing, and `&self` recover the data pointer and metadata.
- codegen_place_ref_stable: `&self` returns the fat pointer directly.
- codegen_operand_stable: pass the fat pointer for slice/str/dyn operands so
callers forward the metadata too.
Adds tests/kani/UnsizedFnParams/unsized_by_value_args.rs covering slice and str
by-value self. Fixes the script-based-pre std_codegen regression.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
changed the title
Merged
via the queue into
model-checking:main
with commit Jul 9, 2026
89aa585
32 of 34 checks passed
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.
Upgrade the toolchain to
nightly-2025-12-31and adapt Kani to the correspondingrustc/rustc_publicchanges:name()functions for local defs in rustc_public rust-lang/rust#149401):name()now qualifies localitems with the crate name. Add a
strip_local_crate_prefixhelper and keepharness/function/static pretty names, the recursion-tracker
--nondet-static-exclude, stubbing diagnostics, and the autoharness/listoutput crate-relative; fix the automatic contract-harness lookup accordingly.
Rvalue::NullaryOp/NullOpwere removed and the
ub/contract/overflowchecks moved toOperand::RuntimeChecks; update the CPROVER and LLBC codegen and the relatedanalyses.
unsized_fn_params: the updated std passes unsized values by value (e.g.impl … for [&str]). Represent unsized-by-value arguments as fat pointers sothey codegen instead of triggering an ICE (test under
tests/kani/UnsizedFnParams).FieldsShape::…::in_memory_order(layout: Store inverse memory index inFieldsShape::Arbitraryrust-lang/rust#150116),the new
ValueAbi::ScalableVectorvariant, theHumanReadableErrorTypestructform, coercion/safety cleanups (misc coercion cleanups and handle safety correctly rust-lang/rust#148602), a refreshed
pointer_generator_errorexpected file, and aclippy::result_large_errallow.Resolves: #4623
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.