Fix loop-contract transform for post-#145513 deref temporaries#4659
Open
tautschnig wants to merge 3 commits into
Open
Fix loop-contract transform for post-#145513 deref temporaries#4659tautschnig wants to merge 3 commits into
tautschnig wants to merge 3 commits into
Conversation
rust-lang/rust#145513 (first shipped in nightly-2025-10-13) removed `Rvalue::CopyForDeref` from runtime MIR: the compiler-generated deref temporaries that destructuring patterns like `for (i, &p) in ...` introduce are now assigned via plain `Rvalue::Use(Operand::Copy)`. `replace_first_pat_by_nth_pat` distinguished pattern bindings from deref temporaries purely by rvalue kind: `Use(Copy)` assignments sourced from the firstpat variable were paired up with their nthpat counterparts and had their assignment redirected to the nthpat projection local, while `CopyForDeref` assignments kept their left-hand side and only had the rvalue re-pointed at the nthpat variable. With the new MIR shape, deref temporaries took the first path: their assignment was redirected to the nthpat temporary, leaving the original temporary uninitialized, and the subsequent dereference of that temporary produced spurious "dereference failure" checks, e.g.: Failed Checks: dereference failure: pointer NULL File: "library/core/src/num/dec2flt/decimal_seq.rs", line 398, in num::dec2flt::decimal_seq::number_of_digits_decimal_left_shift Fix this by pairing up only user variables (pattern bindings, as per var_debug_info) in the firstprj-to-nthprj map, and by handling unmapped `Use(Copy)` assignments sourced from firstpat exactly like the old `CopyForDeref` case: keep the assigned place and only redirect the rvalue to the nthpat variable, so later statements dereferencing the temporary remain well-defined. The `CopyForDeref` arm is kept for defensiveness even though current runtime MIR no longer produces it. Add a regression test modelled after `number_of_digits_decimal_left_shift` from the Rust standard library, where verify-rust-std first hit the regression. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This PR updates Kani’s loop-contract MIR transformation to handle the post-rust-lang/rust#145513 MIR shape where compiler-generated deref temporaries are assigned via plain Rvalue::Use(Operand::Copy) instead of Rvalue::CopyForDeref. The change prevents those deref temporaries from being misclassified as pattern bindings during the firstpat→nthpat rewrite, avoiding spurious dereference-failure checks (regression tracked as #4658).
Changes:
- Restrict firstprj→nthprj pairing to user-defined variables (identified via
var_debug_info) and treat unmappedUse(Copy)assignments sourced fromfirstvarlike the historicalCopyForDerefpath (keep LHS, redirect RHS). - Keep the
CopyForDerefarm as a defensive fallback. - Add a new expected-test regression covering
for (i, &p) in ...ref-pattern loops and its corresponding.expectedoutput.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
kani-compiler/src/kani_middle/transform/loop_contracts.rs |
Fixes the firstpat→nthpat rewrite logic to avoid mis-rewriting compiler deref temporaries as pattern bindings. |
tests/expected/loop-contract/for_loop_ref_pattern.rs |
Adds a regression test exercising ref-pattern destructuring in for loops under -Z loop-contracts. |
tests/expected/loop-contract/for_loop_ref_pattern.expected |
Adds expected-output patterns for the new regression test. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
added a commit
to model-checking/verify-rust-std
that referenced
this pull request
Jul 19, 2026
The Kani version this PR moves to (d4df833c8) is pinned to toolchain nightly-2025-11-25, which includes rust-lang#145513: deref temporaries are no longer assigned via `Rvalue::CopyForDeref` in runtime MIR. Kani's loop-contract instrumentation relies on that rvalue kind to recognize such temporaries in `for` loops whose pattern destructures the iterator element through a reference, like the for (i, &p5) in pow5.iter().enumerate().take(pow5_b - pow5_a) loop in number_of_digits_decimal_left_shift, and now emits spurious dereference failures for them, which failed the check_left_shift and check_number_of_digits_decimal_left_shift harnesses in CI: Failed Checks: dereference failure: pointer NULL File: "library/core/src/num/dec2flt/decimal_seq.rs", line 398 Reported as model-checking/kani#4658, fix proposed in model-checking/kani#4659. Until that fix is part of the pinned Kani version, disable the loop invariant on this loop and bound the two affected harnesses with #[kani::unwind(44)] instead: the loop runs at most pow5_b - pow5_a <= 42 iterations for the reachable TABLE entries, and the unwinding assertion proves that bound. Verified locally with the pinned Kani commit: all four decimal_seq harnesses pass (check_number_of_digits_decimal_left_shift 198s, check_left_shift 250s, check_round + check_right_shift 4s), which is slower than the loop-contract proofs (~20s each) but well within CI budgets. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
feliperodri
approved these changes
Jul 21, 2026
Address review feedback: all other loop-contract expected files precede each '- Status' line with the property name, so match that convention rather than relying on the (unique) description alone. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.
rust-lang/rust#145513 (first shipped in nightly-2025-10-13) removed
Rvalue::CopyForDereffrom runtime MIR: the compiler-generated deref temporaries that destructuring patterns likefor (i, &p) in ...introduce are now assigned via plainRvalue::Use(Operand::Copy).replace_first_pat_by_nth_patdistinguished pattern bindings from deref temporaries purely by rvalue kind, so with the new MIR shape a deref temporary is treated like a pattern binding: its assignment is redirected to the nthpat temporary, leaving the firstpat temporary uninitialized, and the subsequent dereference of that temporary yields spurious "dereference failure" checks (see #4658 for the full analysis). This is what currently breaks thenum::dec2flt::decimal_seqproofs in model-checking/verify-rust-std#530.The fix pairs up only user variables (pattern bindings, as identified via
var_debug_info) in the firstprj→nthprj map, and handles unmappedUse(Copy)assignments sourced from the firstpat variable exactly like the oldCopyForDerefcase: keep the assigned place, only re-point the rvalue at the nthpat variable. TheCopyForDerefmatch arm is kept for defensiveness.Manual testing performed:
tests/expected/loop-contract/for_loop_ref_pattern.rs(modelled afternumber_of_digits_decimal_left_shiftfrom the Rust standard library) fails before the fix with 6 spurious dereference failures and passes with it.expectedsuite: 404 passed / 1 failed — the failure (shadow/unsupported_num_objects) is pre-existing and also fails on unmodifiedmain(unsupported__rust_alloc_error_handlerforeign function).decimal_seq_verify::check_left_shift,decimal_seq_verify::check_number_of_digits_decimal_left_shift) verify successfully.Resolves #4658
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.