[hung1962003]

Follow-up to #4947 (merged), rebased onto main: one commit.

Problem

With an explicit #[kani::loop_modifies], CBMC requires every local the loop writes to be in the write set. #4947 adds the loop-only locals that Kani generates. Two more kinds of locals cannot be named by the user, and loops that use them still fail with Check that var_N is assignable:

1. MIR temporaries, e.g. the scrutinee of a match with return arms. This is the shape of the provided Searcher::next_reject in core::str::pattern:

   loop {
       match self.next() {
           SearchStep::Reject(a, b) => return Some((a, b)),
           SearchStep::Done => return None,
           _ => continue,
       }
   }

2. Variables declared in the loop body that are still live when a return leaves the loop (their StorageDead is outside the loop), e.g. found_char in CharSearcher::next_match.

Change

This PR adds a local to an explicit write set when all of the following hold:

• It is dead at the loop head where the write set is havocked (the target of the new latch), according to a small backward MIR liveness analysis. So havocking it cannot change a value that the loop reads.
• It is not storage-local to the loop, i.e. its StorageLive and every StorageDead are not all inside the natural loop. CBMC already allows writes to storage-local locals.
• It is a temporary, or a variable declared inside the loop's source: within the spans of the user code of the loop's MIR blocks, in the same file (code from macro expansions, including the code #[kani::loop_invariant] generates, is left out). A variable declared before the loop must still be named, which keeps Keep loop attributes on rewritten for loops and add loop-only locals to loop_modifies #4947's policy; the *_fail tests are unchanged.
• Its loop cannot be entered again, i.e. it is not inside another loop, with a contract or without (its entry block is not on a cycle). Otherwise the write set that CBMC infers for the outer loop fails assigns clause inclusion, and a new entry could havoc a local whose storage a path that left the loop ended.

The PR also emits StorageLive for these locals at the latch, before the back jump. Without it, havocking an address-taken temporary whose storage the last iteration ended fails with dereference failure: dead object. codegen_storage_live is factored out of the StorageLive statement codegen for this reuse, with no behavior change.

Testing

• loop_modifies_match_temporary.rs (the match scrutinee) and loop_modifies_returned_local.rs (a loop-body variable read by a return) fail without this PR (Check that var_12 is assignable, Check that found is assignable) and pass with it.
• loop_modifies_returned_temporary.rs covers the StorageLive at the latch. Its borrowed temporary x + 0 is added to the write set, and havocking it after its storage ended must not fail.
• loop_modifies_returned_local_while_let.rs: the same as loop_modifies_returned_local.rs for a while let and a let chain, whose loops #[kani::loop_invariant] rewrites; both fail Check that found is assignable without the span change.
• loop_modifies_returned_local_dangling.rs: an invariant that reads an added loop-body variable through a pointer after its storage ended still fails with dereference failure: dead object, despite the StorageLive at the latch.
• tests/expected/loop-contract: all pass. Eight loop_assigns_for_*.expected files are renumbered (check numbers only; no status changes).
• With this PR, the provided Searcher methods in verify-rust-std's core::str::pattern (Challenge 20) verify unbounded on unmodified bodies with the bundled CBMC 6.11.0 (Challenge 20: Unbounded proofs for the char Searchers of str::pattern verify-rust-std#740).

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

🤖 Generated with Claude Code

[hung1962003]

Friendly ping: this is a small follow-up to #4947 (only the last commit is new). It unblocks unbounded proofs of the provided Searcher methods in verify-rust-std (model-checking/verify-rust-std#740, Challenge 20), whose loops match on a call result and return from the loop. I am happy to rebase onto main once #4947 merges, or to split the StorageLive change into its own PR if that is easier to review. @feliperodri @tautschnig

[feliperodri]

@hung1962003 can you rebase this PR?

[Copilot]

🟡 Changes recommended

Lifetime resets can mask dangling-pointer errors, and source-coordinate matching can wrongly permit writes outside a modifies clause; loop-form and re-entry regressions also remain unresolved.

4 open issues

• Havocing locals can make dangling escaped pointers appear live · New
• Line/column ranges can include unrelated macro or include locals · New
• Repeated loop entry can havoc dead borrowed temporaries · New
• Rewritten loop spans can omit returned body locals · New

What changed in this PR

Extends Kani’s explicit loop_modifies handling to include eligible dead temporaries and loop-body variables, building on #4947 to support loops with early returns.

Changes:

• Adds MIR liveness and storage analysis to identify locals eligible for automatic write-set inclusion.
• Reuses storage-lifetime code generation at loop latches to support havoc of added locals.
• Adds three regression tests and updates eight expected-output check numbers without changing their expected statuses.

File	Description
tests/​expected/​loop-contract/​loop_modifies_returned_temporary.rs	Tests havoc of a borrowed temporary whose storage ended.
tests/​expected/​loop-contract/​loop_modifies_returned_temporary.expected	Expects successful verification.
tests/​expected/​loop-contract/​loop_modifies_returned_local.rs	Tests a loop-body local used by an early return.
tests/​expected/​loop-contract/​loop_modifies_returned_local.expected	Expects successful verification.
tests/​expected/​loop-contract/​loop_modifies_match_temporary.rs	Tests a match scrutinee with returning arms.
tests/​expected/​loop-contract/​loop_modifies_match_temporary.expected	Expects successful verification.
tests/​expected/​loop-contract/​loop_assigns_for_vec.expected	Renumbers an assigns check.
tests/​expected/​loop-contract/​loop_assigns_for_ref.expected	Renumbers an assigns check.
tests/​expected/​loop-contract/​loop_assigns_for_ref_fail.expected	Renumbers an expected failing check.
tests/​expected/​loop-contract/​loop_assigns_for_ptr.expected	Renumbers assigns checks.
tests/​expected/​loop-contract/​loop_assigns_for_ptr_fail.expected	Renumbers an expected failing check.
tests/​expected/​loop-contract/​loop_assigns_for_fat_ptr.expected	Renumbers assigns checks.
tests/​expected/​loop-contract/​loop_assigns_for_fat_ptr_fail.expected	Renumbers an expected failing check.
tests/​expected/​loop-contract/​loop_assigns_for_empty_slice_fail.expected	Renumbers an expected failing check.
kani-compiler/​src/​kani_middle/​transform/​loop_contracts.rs	Identifies additional locals for explicit write sets.
kani-compiler/​src/​codegen_cprover_gotoc/​overrides/​hooks.rs	Emits storage-live operations before loop back jumps.
kani-compiler/​src/​codegen_cprover_gotoc/​codegen/​statement.rs	Extracts reusable StorageLive code generation.

_{Review effort: Balanced}

[hung1962003]

A pointer to such a local that the loop writes must itself be in the write set, so it is havocked at the head, and the step case still flags the read. 9510ceb adds loop_modifies_returned_local_dangling.rs: the invariant reads an added loop-body variable through a pointer after its storage ended, and Kani still reports dereference failure: dead object there. The comment above the StorageLive now says this.

[feliperodri]

The dangling-pointer test covers a pointer the loop names (&p in loop_modifies). Two cases it doesn't:

1. The pointer is stored through a pre-loop pointer the user doesn't name, e.g. *q = &t where q is set before the loop and never written in it.
2. The pointer is kept in a struct field or Option that the loop writes, but whose root local isn't in the clause.

Either one with the invariant reading through the pointer should fail with dead object. If it can't happen, a short comment saying why would settle it.

[feliperodri]

Approving. This unblocks unbounded proofs of loops that match on a call and return from the
loop, a common shape in core (Challenge 20's Searcher methods). Users can't name the
temporaries involved in loop_modifies, so without this change those loops have no workaround.

Soundness: adding a local to a loop's write set only makes CBMC havoc more at the loop head. That
can cause spurious failures, never a false proof, so the liveness filter is about precision, not
soundness. I looked hardest at the StorageLive emitted at the latch, because it clears the
dead-object marker one step early. It only affects the checks between the latch and the back edge
(invariant and assigns), and a pointer to such a local is havocked at the head anyway. So I don't
see a way to get a false "verified" from it. A comment in the code saying so would help the next
reader (inline).

What I ran, on the PR rebased onto main (c5e65fd):

• tests/expected/loop-contract and the other loop tests: 93 passed, 4 ignored. tests/kani loop
  tests: 6 passed. kani-fmt --check and clippy -D warnings on kani-compiler are clean.
• The new tests on main without the compiler change: loop_modifies_match_temporary and
  loop_modifies_returned_local fail with the "assignable" errors from the description.
  loop_modifies_returned_temporary passes on main, because the temporary isn't added at all.
  With the PR minus only the latch StorageLive, it fails with dereference failure: dead object. So each test guards the part it's meant to.
• A probe where the loop invariant reads, through a pointer, a loop-body variable whose storage
  ended (p = &t in the body, then *p in the invariant). Kani still reports dead object on it,
  along with failures from the havocked pointer.

Not run: verify-rust-std#740 (Challenge 20), macOS, and the full regression suite.

The judgment call worth a maintainer's look is the two heuristics that position-match the loop:

• the loop's line/column range, parsed from the register function's name;
• block-index ranges for written and nested, while the new code computes the natural loop.

Both fail safe (the local isn't added, or a spurious failure), but they're the most likely things
to break with a toolchain or macro change.

Good work on:

• the description, which states each condition and why it's there;
• tests that each fail for the right reason;
• factoring codegen_storage_live out instead of duplicating it.

[feliperodri]

@hung1962003 can you also address all Copilot's comments before we merge it?

[hung1962003]

@feliperodri I addressed all the comments, yours and Copilot's, in 9510ceb (replies inline). In short: the loop's source now comes from the spans of its MIR blocks instead of the register function's name (this also fixes while let and let chains, with a new test), the written locals use the natural loop, and loops that can be entered again get nothing added, which covers both the nested case and Copilot's re-entry case. A new test checks that a dangling read in the invariant still fails. tests/expected/loop-contract: 92 passed, 0 failed; tests/kani Loop: 6 passed; fmt and clippy clean. The PR description is updated to match.

[feliperodri]

Thanks for the thorough replies. Three small things, all non-blocking.

Also: 8 .expected files changed, but the PR says the *_fail tests are unchanged. Can you list each changed output and say why it moved? That's the easiest way for us to check it's expected.

[feliperodri]

This shadows declared_in_loop (the set on the line above). It works, but it's easy to misread. Rename the set to declared and keep the closure name.

[feliperodri]

This loops over every local of the function, for every loop that gets a new latch. On big functions with many loops that adds up. Could we iterate the written set instead? It's already small, and the other filters still apply.

[feliperodri]

Body::new copies every block and local just to call statement_location. On big MIR bodies that's a lot of copying. Could these helpers take the existing body instead?