Repository navigation
Add a loop's dead temporaries and loop-body variables to an explicit loop_modifies - #5071
Open
hung1962003 wants to merge 12 commits into
Open
hung1962003 wants to merge 12 commits into
hung1962003 wants to merge 12 commits into
Conversation
…to loop_modifies `#[kani::loop_invariant]` rewrites a `for` loop into a `while` loop, and the rewrite dropped the attributes written after the invariant, so a `#[kani::loop_modifies]` or `#[kani::loop_decreases]` written there was silently ignored. Keep them on the rewritten loop. Carrying them over exposed two problems, the first of which also affects clauses written before the invariant: - A complete `loop_modifies` clause failed the assigns check on locals that the user cannot name in the clause: the index and the pattern bindings that the `for` loop rewrite generates, the variables generated for `prev`, and the variables and temporaries declared in the loop body whose initialization the loop contract pass copies to the loop head. The pass now records these locals for each loop, by the instance of the register function that the loop latch calls, and `BodyTransformation` keeps them by the instance of the body and of the register function (new `TransformPass::take_generated_loop_modifies` with an empty default). The codegen hook of that call adds them to the assigns clause of the loop if the user wrote one. The body is not changed for this, so later passes such as the uninitialized memory checks do not instrument anything for it. The locals only exist for the loop, so writes to any other memory are still checked against the user's clause. - `replace_first_pat_by_nth_pat` assumed that the loop head is the second block after the call to `KaniIter::first`, and panicked with `not a loop head` when an expression evaluated in between needed a block of its own (e.g. `#[kani::loop_modifies(&out[0])]` written after the invariant, or `on_entry(v.len())`). It now finds the loop head in the control flow graph, redirects the uses of the first pattern in all blocks before it, and emits an error instead of panicking if the loop head cannot be found.
A variable declared before the loop that the loop writes before reading it must still fail the assigns check, and a variable declared in the loop body must still be dead after its scope. Suggested in review.
Each `#[kani::loop_invariant]` attribute of a loop added its own call to a register function. On a `while` loop, only the call of the last attribute is the loop head, so the other invariants were silently dropped: they were neither checked nor assumed. On a `for` loop, whose attributes after the invariant are now kept on the rewritten loop, a second invariant made the loop contract pass fail with "Kani could not find the loop head of this `for` loop with a loop contract". The documentation says that a loop contract is composed of one or more loop invariants. Make the first `#[kani::loop_invariant]` attribute take the other ones out of the loop and use the conjunction of all their invariants, for `while`, `loop`, `while let` and `for` loops.
A loop whose `#[kani::loop_modifies]` clause had no target got an inferred write set, so the loop could write anything: codegen only attached a clause with at least one target, and CBMC infers the write set of a loop whose assigns clause has no target. This happened with an empty clause (`#[kani::loop_modifies()]`, whose `()` binding MIR optimizations also remove), and with a clause whose targets all have zero size, since codegen drops those targets (it also did not drop a single zero-sized target, which made CBMC report pointer failures). Track whether a loop has a clause separately from its targets (`current_loop_modifies` is now an `Option`), drop a single zero-sized target as well, and when a clause has no target left (also after adding the locals that only exist for the loop), use an object that no code writes as its only target. For an empty clause, the macro now binds a reference to a zero-sized local, which MIR optimizations keep.
Codegen kept the user clause in a single slot: it was set when codegen reached the
`kani_loop_modifies` binding and taken by the next loop latch that codegen generated. The latch
of an inner loop is generated before the latch of its outer loop, so an inner loop without a
clause got the clause of its outer loop, and an inner loop with a clause replaced it, leaving the
outer loop with an inferred write set. Since the attributes of a `for` loop are now kept, an
outer clause written after the invariant of a `for` loop reached this as well. The clause of a
loop that does not iterate (e.g. `loop { break; }`), whose latch is not generated, went to the
next loop.
The loop contract pass now finds the `kani_loop_modifies` binding of each loop, by walking up
the dominator tree from the loop head and stopping at the head of another loop or at a binding
of another loop, and records it with the instance of the register function of the loop, like the
locals that only exist for the loop. Codegen keeps the targets of each clause by that instance,
and the hook of each loop takes its own clause. A binding that does not belong to a loop with a
loop invariant is not attached to any loop. The decreases clause is not changed.
The binding of a `#[kani::loop_modifies]` clause was assigned where the attribute expanded: before all the code that `#[kani::loop_invariant]` generates for the loop when the clause is written first, and right before the loop otherwise. The loop contract pass, which looks for the binding of a loop by walking up the dominator tree from the loop head, stopped at the head of any loop. So the clause was dropped, and CBMC inferred the write set of the loop, when a loop without a loop contract was in between: a loop in the iterable expression of a `for` loop or in an `on_entry` expression, with the clause written first, or a loop around the loop whose body starts with it, whose head then holds the binding. `#[kani::loop_invariant]` now takes the `#[kani::loop_modifies]` attributes of its loop and binds their targets right before the loop, after the code that it generates for the loop. A `#[kani::loop_modifies]` written before the invariant moves itself after it. The walk now also searches the head of the loop where it stops. In addition: - The targets of several `#[kani::loop_modifies]` attributes on one loop are combined. Only the attribute closest to the loop was applied. - A clause on a loop without `#[kani::loop_invariant]` is ignored with a warning. It was applied to the next loop when its own loop does not iterate. - The binding is a tuple, even for a single target. MIR optimizations merged the binding of a single variable (e.g. `#[kani::loop_modifies(p)]`) with that variable: if the variable is an argument, the clause was dropped, and codegen also skipped the writes through the variable, taking them for the binding; if it is a local, Kani panicked.
`move_storagelive_assign_to_loophead` copies the initialization of a variable declared in a loop body to the loop head, and records the variable as a local of that loop, which codegen adds to its write set. The binding of a `#[kani::loop_modifies]` clause of an inner loop is such a variable when it has a single target or no target, so it was added to the write set of the loop around it. With three nested loops, the write set of the middle loop then had a local that is not in the write set of the outer loop, since it is only declared at the head of the middle loop, and `Check assigns clause inclusion` failed for the middle loop. Codegen does not generate the assignments of the bindings, so they are not moved anymore.
… found Codegen skipped every assignment to a local whose name contains `kani_loop_modifies`, including assignments through it (e.g. `*p = ..`). Now it only skips the assignment of a binding itself, when the loop contract pass found the loop of that binding, and the pass ignores assignments through a binding. Codegen also keeps the targets of a clause by the instance of the function that contains the loop as well as the register function of the loop, as the locals of the loop are, so that a loop whose latch is not generated does not leave its clause to another function.
Codegen generated the tuple that binds the targets of a clause, and paired its fields with the operands of the tuple. The fields are in the order of the layout of the tuple, which rustc can change, e.g. a slice and two references, so a target could get the type of another one: Kani panicked on `#[kani::loop_modifies(slice_from_raw_parts_mut(a.as_mut_ptr(), 2), &i, &j)]`, and with slices of different element sizes the target of a slice covered the wrong number of bytes, which could miss a write outside of the clause. Each operand is now generated on its own. This already happened on `main` for clauses with several targets, and is more likely now that the targets of several `#[kani::loop_modifies]` attributes are combined.
An explicit `#[kani::loop_modifies]` must cover every local that the loop writes. model-checking#4947 adds the loop-only locals that Kani generates, but MIR temporaries (e.g. the scrutinee of a `match` with `return` arms) and variables of the loop body that are still live when a `return` leaves the loop cannot be named by the user, and still fail with `Check that var_N is assignable`. Add to the write set the locals that are dead at the loop head where the write set is havocked (by a MIR liveness analysis), are not storage-local to the loop, and are temporaries or declared inside the loop's span, for loops that are not nested in another contracted loop. Emit `StorageLive` for them at the latch, so that havocking an address-taken temporary whose storage the last iteration ended is not a write to a dead object. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
github-actions
Bot
added
Z-EndToEndBenchCI
Author
|
Friendly ping: this is a small follow-up to #4947 (only the last commit is new). It unblocks unbounded proofs of the provided |
This branch has not been deployed
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.
Follow-up to #4947, stacked on its branch (only the last commit is new; I will rebase once #4947 merges).
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 withCheck that var_N is assignable:matchwithreturnarms. This is the shape of the providedSearcher::next_rejectincore::str::pattern:returnleaves the loop (theirStorageDeadis outside the loop), e.g.found_charinCharSearcher::next_match.Change
This PR adds a local to an explicit write set when all of the following hold:
StorageLiveand everyStorageDeadare not all inside the natural loop. CBMC already allows writes to storage-local locals.*_failtests are unchanged.assigns clause inclusion.The PR also emits
StorageLivefor these locals at the latch, before the back jump. Without it, havocking an address-taken temporary whose storage the last iteration ended fails withdereference failure: dead object.codegen_storage_liveis factored out of theStorageLivestatement codegen for this reuse, with no behavior change.Testing
loop_modifies_match_temporary.rs(thematchscrutinee) andloop_modifies_returned_local.rs(a loop-body variable read by areturn) fail without this PR (Check that var_12 is assignable,Check that found is assignable) and pass with it.loop_modifies_returned_temporary.rscovers theStorageLiveat the latch. Its borrowed temporaryx + 0is added to the write set, and havocking it after its storage ended must not fail.tests/expected/loop-contract: all pass. Eightloop_assigns_for_*.expectedfiles are renumbered (check numbers only; no status changes).Searchermethods in verify-rust-std'score::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