From f5fda455aacb2b79051b611879d2a96a38316316 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 19 Jul 2026 13:38:42 +0000 Subject: [PATCH 1/2] Fix loop-contract transform for post-#145513 deref temporaries 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 --- .../kani_middle/transform/loop_contracts.rs | 38 +++++++++++--- .../for_loop_ref_pattern.expected | 8 +++ .../loop-contract/for_loop_ref_pattern.rs | 50 +++++++++++++++++++ 3 files changed, 88 insertions(+), 8 deletions(-) create mode 100644 tests/expected/loop-contract/for_loop_ref_pattern.expected create mode 100644 tests/expected/loop-contract/for_loop_ref_pattern.rs diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 8ce1b819ac8d..70932fab6d1e 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -301,10 +301,20 @@ impl LoopContractPass { let mut firstprj_nthprj: HashMap = HashMap::new(); firstprj_nthprj.insert(firstvar, nthvar); + // Only user variables (pattern bindings) are paired up with their nthpat + // counterparts. Compiler-generated temporaries (e.g. the deref temporaries + // that destructuring patterns like `&x` introduce) must not be paired: + // their assignments are kept in place (with the rvalue redirected to + // nthvar) so that later statements reading them remain well-defined. + // Note: before rust-lang/rust#145513 such temporaries were assigned via + // `Rvalue::CopyForDeref` and thus never matched the `Rvalue::Use` pattern + // below; nowadays they are plain `Rvalue::Use(Operand::Copy)` assignments. + let user_vars = self.get_user_defined_variables(body); for fstmt in firstprj_stmts_copy.iter() { if let StatementKind::Assign(fprjplace, frval) = &fstmt.kind && let Rvalue::Use(Operand::Copy(firstpatplace)) = frval && firstpatplace.local == firstvar + && user_vars.contains(&fprjplace.local) { let firstprj = fprjplace.local; for istmt in nthprj_stmts_copy.iter() { @@ -342,17 +352,29 @@ impl LoopContractPass { match frval { Rvalue::Use(Operand::Copy(firstpatplace)) => { if firstpatplace.local == firstvar { - let nthprj = firstprj_nthprj.get(&fprjplace.local).unwrap(); let mut nthpatplace = firstpatplace.clone(); nthpatplace.local = nthvar; let newrval = Rvalue::Use(Operand::Copy(nthpatplace)); - new_stmt.kind = StatementKind::Assign( - Place { - local: *nthprj, - projection: fprjplace.projection.clone(), - }, - newrval, - ); + if let Some(nthprj) = firstprj_nthprj.get(&fprjplace.local) { + // A user pattern binding: redirect the assignment to + // the corresponding nthpat projection variable. + new_stmt.kind = StatementKind::Assign( + Place { + local: *nthprj, + projection: fprjplace.projection.clone(), + }, + newrval, + ); + } else { + // A compiler-generated temporary (e.g. a deref + // temporary, `Rvalue::CopyForDeref` before + // rust-lang/rust#145513): keep the assigned place and + // only redirect the rvalue to read from nthvar, so + // that following statements dereferencing the + // temporary keep working. + new_stmt.kind = + StatementKind::Assign(fprjplace.clone(), newrval); + } } } Rvalue::CopyForDeref(firstpatplace) => { diff --git a/tests/expected/loop-contract/for_loop_ref_pattern.expected b/tests/expected/loop-contract/for_loop_ref_pattern.expected new file mode 100644 index 000000000000..1c474d41cc79 --- /dev/null +++ b/tests/expected/loop-contract/for_loop_ref_pattern.expected @@ -0,0 +1,8 @@ +lookup.loop_invariant_base.1\ + - Status: SUCCESS\ + - Description: "Check invariant before entry for loop lookup.0" + + - Status: SUCCESS\ + - Description: "assertion failed: n <= 2" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/for_loop_ref_pattern.rs b/tests/expected/loop-contract/for_loop_ref_pattern.rs new file mode 100644 index 000000000000..f6f2f3151bd8 --- /dev/null +++ b/tests/expected/loop-contract/for_loop_ref_pattern.rs @@ -0,0 +1,50 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check for-loop invariant for a loop whose pattern destructures the +//! iterator element through a reference, e.g. `for (i, &p) in ...`. +//! Such patterns introduce compiler-generated deref temporaries in the +//! pattern-binding block. Those temporaries used to be assigned via +//! `Rvalue::CopyForDeref`, which rust-lang/rust#145513 turned into plain +//! copies, and the loop-contract transformation has to keep their +//! assignments in place instead of treating them like pattern bindings +//! (see https://github.com/model-checking/kani/issues/4658). +//! This is a regression test for the spurious "dereference failure" +//! checks Kani used to emit for this pattern; it is modelled after +//! `number_of_digits_decimal_left_shift` in the Rust standard library. + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +const TABLE: [u8; 16] = [5, 2, 5, 1, 2, 5, 6, 2, 5, 3, 1, 2, 5, 1, 5, 6]; + +fn lookup(digits: &[u8; 16], num_digits: usize, a: usize, b: usize) -> usize { + let num_new_digits: usize = 2; + let pow5 = &TABLE[a..]; + + #[kani::loop_invariant(num_new_digits > 1)] + for (i, &p5) in pow5.iter().enumerate().take(b - a) { + if i >= num_digits { + return num_new_digits - 1; + } else if digits[i] == p5 { + continue; + } else if digits[i] < p5 { + return num_new_digits - 1; + } else { + return num_new_digits; + } + } + num_new_digits +} + +#[kani::proof] +fn check_ref_pattern_deref_temp() { + let digits: [u8; 16] = kani::any(); + let num_digits: usize = kani::any_where(|x| *x <= 16); + let a: usize = kani::any_where(|x| *x < 8); + let b: usize = kani::any_where(|x| *x >= a && *x <= 16); + let n = lookup(&digits, num_digits, a, b); + assert!(n <= 2); +} From 01d41169a3ca5f7d6e5e65dfdb9993593f058a47 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 21 Jul 2026 18:59:18 +0000 Subject: [PATCH 2/2] Add check-name header to second expected block 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 --- tests/expected/loop-contract/for_loop_ref_pattern.expected | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/expected/loop-contract/for_loop_ref_pattern.expected b/tests/expected/loop-contract/for_loop_ref_pattern.expected index 1c474d41cc79..89aecbbeea58 100644 --- a/tests/expected/loop-contract/for_loop_ref_pattern.expected +++ b/tests/expected/loop-contract/for_loop_ref_pattern.expected @@ -2,6 +2,7 @@ lookup.loop_invariant_base.1\ - Status: SUCCESS\ - Description: "Check invariant before entry for loop lookup.0" +check_ref_pattern_deref_temp.assertion.1\ - Status: SUCCESS\ - Description: "assertion failed: n <= 2"