[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 span. 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 is not nested in another contracted loop. Otherwise the write set that CBMC infers for the outer loop fails assigns clause inclusion.

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.
• 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}

[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]

Suggestion: declared_in_loop recovers the loop's span by parsing the
_<line>_<col>_<line>_<col> suffix of the register function's name, then compares line and
column only, without the file. Two things can go wrong:

• Coupling: this ties the compiler to the macro's naming format, and the format changes silently.
• Files: a variable whose span is in another file (from a macro expansion) can fall inside the
  numeric range and be added without the user naming it. That relaxes Keep loop attributes on rewritten for loops and add loop-only locals to loop_modifies #4947's rule that variables
  declared before the loop must be named.

Neither is unsound; the variable is just havocked when it shouldn't need to be. Could this use the
span of the loop's MIR instead, for example the span of the register call or of the latch
terminator? That carries the file and needs no parsing.

[feliperodri]

Suggestion: nested, and written at line 1493 (loop_head + 1..=*loop_latch), infer the
loop's blocks from block indices, while this PR adds natural_loop, which computes them. MIR
block order doesn't guarantee that a loop's blocks are contiguous or that a nested loop's indices
fall inside its parent's. If they don't:

• written can miss a write, and then the loop fails with "assignable" as before;
• nested can misclassify a loop, and then it fails "assigns clause inclusion".

Both are spurious failures, not soundness problems. Using natural_loop for both would make the
three checks agree. If that's out of scope, a comment noting the assumption would do.

Question: do the existing loop_modifies_nested* tests fail if the nested filter is
removed? If not, a test where an inner contracted loop has a match temporary with a return
arm would pin the reason for the filter.

[feliperodri]

Nit: "A loop can havoc a local that is not live at its head: no value of it reaches the loop
body" holds for direct reads only. A read through a pointer to the local isn't seen. For example,
a temporary without storage markers, borrowed in one iteration and read through the pointer in the
next. Havocking it then is still sound, because it over-approximates, but it can cause a spurious
failure. It would help to say that the analysis ignores indirect reads and why that's safe.

[feliperodri]

FYI: for readers of this thread. This marks the storage live at the end of the iteration, one
step before the program would. Between this point and the back edge, CBMC only checks the
invariant (and the assigns clause). A dangling read of such a local in the invariant would lose its
dead-object check on the base-case path. But a pointer to it must be in the write set, so it's
havocked at the head, and the step case flags the dereference anyway. Worth one sentence in the
comment above, so the next person doesn't have to redo this reasoning.

[feliperodri]

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