Repository navigation
Check #[kani::loop_decreases] clauses whose measure is a variable - #4946
Merged
feliperodri merged 3 commits intoOct 22, 2026
Merged
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Copilot review overview
🔵 Needs a closer look
It changes soundness-sensitive compiler transformations and CBMC annotation generation across nested control-flow scenarios.
Review effort: Balanced
Findings: None
What changed in this PR
Fixes loop-decreases checking so variable, field, and dereference measures are correctly evaluated and attached to their intended loops.
Changes:
- Preserves decreases bindings through MIR optimization and serializes measures correctly for CBMC.
- Associates clauses with loop heads per function, including nested loops and quantifiers.
- Expands regression coverage and documents unsupported precomputed measures.
| File | Description |
|---|---|
tests/expected/loop-contract/simple_while_loop_decreases.expected |
Requires a successful decreases check. |
tests/expected/loop-contract/loop_loop_decreases.expected |
Requires a successful loop decreases check. |
tests/expected/loop-contract/fixme_decreases_struct_field.rs |
Removes the obsolete failing field test. |
tests/expected/loop-contract/fixme_decreases_struct_field.expected |
Removes obsolete expected failure output. |
tests/expected/loop-contract/decreases_with_old.expected |
Validates decreases checking with old values. |
tests/expected/loop-contract/decreases_with_function_contract.expected |
Validates decreases with function contracts. |
tests/expected/loop-contract/decreases_variable.rs |
Tests variable, for, prev, and dereference measures. |
tests/expected/loop-contract/decreases_variable.expected |
Requires successful checks for those measures. |
tests/expected/loop-contract/decreases_struct_field.rs |
Tests correct and incorrect field measures. |
tests/expected/loop-contract/decreases_struct_field.expected |
Validates field-measure results. |
tests/expected/loop-contract/decreases_no_invariant.rs |
Tests ignored unattached clauses. |
tests/expected/loop-contract/decreases_no_invariant.expected |
Requires the warning and successful harnesses. |
tests/expected/loop-contract/decreases_nested_loops.rs |
Exercises nested-loop clause association. |
tests/expected/loop-contract/decreases_nested_loops.expected |
Validates each nested loop’s result. |
tests/expected/loop-contract/decreases_nested_loops_quantifier.rs |
Tests per-function state during quantifier codegen. |
tests/expected/loop-contract/decreases_nested_loops_quantifier.expected |
Requires the outer-loop failure. |
tests/expected/loop-contract/decreases_mir_opt_level.rs |
Tests binding preservation under MIR optimization. |
tests/expected/loop-contract/decreases_mir_opt_level.expected |
Validates optimized-MIR outcomes. |
tests/expected/loop-contract/decreases_loop_max.expected |
Requires the generated decreases property. |
tests/expected/loop-contract/decreases_fail_wrong_measure.rs |
Isolates increasing variable measures. |
tests/expected/loop-contract/decreases_fail_wrong_measure.expected |
Requires both decreases failures. |
tests/expected/loop-contract/decreases_fail_unsupported_measure.rs |
Tests unsupported precomputed measures. |
tests/expected/loop-contract/decreases_fail_unsupported_measure.expected |
Requires conservative failures. |
tests/expected/loop-contract/decreases_fail_stale_measure.rs |
Isolates an unchanged measure failure. |
tests/expected/loop-contract/decreases_fail_stale_measure.expected |
Requires the specific decreases failure. |
tests/expected/loop-contract/decreases_fail_constant_measure.rs |
Tests literal and constant measures. |
tests/expected/loop-contract/decreases_fail_constant_measure.expected |
Requires constant-measure failures. |
tests/expected/loop-contract/decreases_expr.expected |
Requires the decreases property. |
library/kani_macros/src/sysroot/loop_contracts/mod.rs |
Keeps generated bindings in optimized MIR. |
kani-compiler/src/kani_middle/transform/loop_contracts.rs |
Prevents movement of decreases bindings. |
kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs |
Retrieves clauses by loop head. |
kani-compiler/src/codegen_cprover_gotoc/context/mod.rs |
Exports the decreases state type. |
kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs |
Removes global decreases state. |
kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs |
Adds per-function clause tracking. |
kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs |
Records live or conservative measures. |
kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs |
Discovers loop heads and reports unattached clauses. |
kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs |
Associates pending clauses with loop heads. |
docs/src/reference/experimental/loop-contracts.md |
Corrects behavior and limitations documentation. |
cprover_bindings/src/irep/to_irep.rs |
Encodes the measure as one annotation operand. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
feliperodri
requested changes
Oct 5, 2026
feliperodri
left a comment
feliperodri
left a comment
Member
There was a problem hiding this comment.
Thanks for tracking this down to the irep encoding. The fix itself is right; I'm requesting changes for one autoharness issue, below.
On main, a #[kani::loop_decreases] clause whose measure is a variable, a call or a constant produces no decreases check, so a measure that increases, stays equal or wraps still gets VERIFICATION:- SUCCESSFUL. That covers most of the decreases tests and every shape I tried with loop, while let, for, prev, closures and nested loops. With this PR, measures that are variables, fields or dereferences of variables are checked at each iteration. Everything else (checked arithmetic, casts, indexing, calls, if, constants) falls back to the binding, so the check fails, and I agree with failing there rather than passing.
What I ran: the new and updated .expected files against a main build (all 16 fail there and pass here), the loop-contract expected tests and the ui suite on the PR merged with current main, the three lint gates, and about 60 probe harnesses comparing main and the PR (variables, fields, derefs, calls, casts, tuples, every loop form, prev/on_entry, nested and sequential loops, closures, -Zmir-opt-level=0..4). Each wrong measure fails on the decreases check alone. I did not rerun the full regression suites (CI is green on the head) or test on macOS.
Before merge: autoharness treats kani_keep_loop_decreases_binding as a user function and generates a harness for it (inline, with a fn_marker fix I tested). The rest is non-blocking: a compile-time warning when the measure falls back to the binding, a docs bullet that looks stale now, and a couple of test cases.
Two things outside this PR's scope: a for loop with #[kani::loop_decreases] written after #[kani::loop_invariant] still drops the clause without a warning (#4929, which #4947 handles), and kani::index isn't substituted inside a decreases clause. This PR and #4947 will conflict in hooks.rs and goto_ctx.rs, so whichever lands second needs a rebase.
CBMC takes the operands of the `#spec_decreases` irep as the components of the measure, as the C front end encodes `__CPROVER_decreases(e1, ..., en)`. Kani emitted the measure itself, so a measure without operands (a variable, a field, a constant) produced no decreases check, and for other measures CBMC used their operands as the measure (e.g. the operand of a cast). Emit the measure as the only operand. This exposes other issues, which this change also fixes: - If the measure is a variable that is assigned only once, copy propagation merges the `kani_loop_decreases` binding into that variable. Codegen then took the definition of the variable for the binding: it dropped the assignment and used its right-hand side as the measure. If the measure is a constant, the binding is removed. The macro now passes a reference to the binding to a function, so that MIR optimizations (also at `-Zmir-opt-level=2`) keep its assignment, and codegen recognizes the binding by its exact name. - Codegen takes the measure from the right-hand side of the assignment to the binding, which CBMC evaluates before and after each iteration. That is only the measure if the right-hand side reads user variables and arguments, and not temporaries that hold values from before the loop (e.g. the index in `a[i]`), and if it is the only assignment to the binding (not an `if` expression or a call). Otherwise, the measure is now the value of the binding, so that the check fails instead of checking part of the measure, or nothing. - Codegen attached a clause to the next loop latch that it generated, so the clause of an outer loop was checked on an inner loop, and the clause of a loop without a loop invariant on a later loop, possibly of another function. A clause is now attached to the first loop head generated after its binding, and the loop latch takes the clause of its head. This state is kept per function, since codegen may generate a quantifier closure while it generates a function. The loop contract pass no longer copies the binding to the head of an enclosing loop. Kani warns about a clause that is not attached to a loop with a loop invariant. Resolves model-checking#4942
…binding helper from autoharness - Mark `kani_keep_loop_decreases_binding` with a `kanitool::fn_marker`, so that autoharness does not generate a harness for it. Add a script-based test that runs autoharness on a function with a decreases clause and checks that only that function is verified. - When the measure of a decreases clause is computed once, before the loop (checked arithmetic, casts, indexing, calls, `if` expressions, constants), warn at the clause that the decreases check will fail even if the measure decreases, and point to model-checking#4585. The warning is emitted once per clause. - Drop the known-bug entry about combining `loop_decreases` with `loop_modifies`: the fixme test failed because of its `5 - i` measure. Turn it into a regular test with a variable measure. - Add test cases: a `while let` loop with the decreases clause after the loop invariant, with a correct and an increasing measure, a measure that wraps around, and a correct `4 - i` measure, which fails with the warning.
Talha-Dmr
force-pushed
the
fix-loop-decreases-plain-var
branch
from
October 6, 2026 09:06
882a3a4 to
3041eb9
Compare
feliperodri
approved these changes
Oct 21, 2026
feliperodri
left a comment
feliperodri
left a comment
Member
There was a problem hiding this comment.
Thanks for working through all of these. I checked each one on the head merged with current main: the autoharness test fails without the marker and passes with it, the new warning shows up once per clause (also for a generic function used at two types) and never for a variable measure, the while let and wrapping-measure cases fail only on the decreases check, and decreases_with_modifies.rs verifies. I also reran my probes from the first round; the results are unchanged apart from the fixes. The loop-contract expected tests and the lint gates pass, and CI is green.
The remaining gap I know of, a for loop with the decreases clause after the invariant, is #4929, which #4947 handles. The two PRs still conflict in hooks.rs and goto_ctx.rs, so whichever lands second needs a rebase.
v3risec
pushed a commit
to v3risec/kani
that referenced
this pull request
Nov 3, 2026
…to loop_modifies (model-checking#4947) ### Description Follow-up to model-checking#4930, which kept the label of rewritten `for` loops but left their attributes for a separate PR (see the review there). `#[kani::loop_invariant]` rewrites a `for` loop into a `while` loop (`transform_for_to_loop`). The rewrite dropped the attributes written after the invariant, so a `#[kani::loop_modifies]` or `#[kani::loop_decreases]` written there was silently ignored. This PR keeps them on the rewritten loop, as model-checking#4930 does for `while let` loops. As found in the review of model-checking#4930, carrying the attributes over made two programs that verify on `main` fail. This PR fixes both: 1. **A complete `loop_modifies` clause failed the assigns check** on locals that the user cannot name in the clause. This already happened on `main` when the clause is written before the invariant, and for `while` loops (model-checking#4906, model-checking#4940). With an explicit clause, CBMC checks every write in the loop to a local that is also used outside of it. The loop contract transformation creates such locals: - the index (`kani_index_...`) and the pattern bindings that the `for` loop rewrite generates (after `replace_first_pat_by_nth_pat` merges the first and the nth pattern, the bindings are assigned before the loop and in each iteration), and the temporary that holds the item for patterns such as `(i, j)`, `&x` or `_`; - the variables generated for `prev(..)`; - the variables and temporaries declared in the loop body whose initialization the pass copies to the loop head (`move_storagelive_assign_to_loophead` and `move_storagelive_call_to_loophead`), e.g. `var_14`, `var_15` and `var_16` in model-checking#4906. The loop contract pass now records these locals for each loop, keyed by the instance of the register function that the new loop latch calls. This instance is unique to the loop, and it is the instance that the codegen hook of that call (`LoopInvariantRegister`) receives. The pass hands the locals to `BodyTransformation` through a new `TransformPass::take_generated_loop_modifies` method (empty by default), which keeps them by the instance of the transformed body and of the register function, and the hook adds them to the assigns clause of the loop if the user wrote one. Without a user clause, CBMC still infers the clause. The body itself is not changed for this, so the passes that run after the loop contract pass (e.g. the uninitialized memory checks) do not instrument anything for it, and nothing depends on the name of a binding that MIR optimizations could remove (as happens to `kani_loop_decreases` in model-checking#4942). The index and `prev` variables are found by their generated names, which start with the id of the loop; they are borrowed by the loop invariant closure or assigned in the loop, so they are not optimized away. This does not let the loop write to memory outside the user's clause: every added local only exists for the loop (it is generated by the rewrite or declared in the loop body), so the user could not name it in the clause anyway. Adding a local to the write set only allows writes to that local's own storage. A write through a pointer stored in such a local, or a write to any variable declared before the loop, is still checked against the user's clause (see `for_loop_modifies_fail.rs` and `loop_modifies_not_added_fail.rs` below). 2. **A clause whose expression needs a basic block of its own crashed the compiler** with `not a loop head`, e.g. `#[kani::loop_modifies(&out[0])]` written after the invariant (the bounds check of `out[0]`). `replace_first_pat_by_nth_pat` assumed that the loop head is the second block after the call to `KaniIter::first`. The same crash already happens on `main` for an `on_entry` expression that calls a function in a `for` loop invariant, e.g. `on_entry(v.len())`. The pass now finds the loop head in the control flow graph (the first loop head reachable from that call whose body calls `KaniIter::nth`), redirects the uses of the first pattern (reads, borrows and index operands) in all blocks before it, not only the borrows in the loop head, and emits a compile error instead of panicking if no loop head is found. **Each `loop_modifies` clause now goes to its own loop.** Codegen used to keep 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. With nested loops, the latch of the inner loop is generated before the latch of the outer loop, so an outer clause written after the invariant of a `for` loop now went to the inner loop, which made programs that verify on `main` fail. This already happened on `main` with the clause written before the invariant, and with `while` loops: an inner loop without a clause got the clause of the outer loop, and an inner loop with a clause replaced it, so the outer loop got an inferred write set and its writes were not checked. Likewise, the clause of a loop that does not iterate (e.g. `loop { break; }`), whose latch is never generated, went to the next loop. Now: - `#[kani::loop_invariant]` 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 (the `on_entry` variables, the initialization of a `for` loop, the first iteration for `prev`). A `#[kani::loop_modifies]` written before the invariant leaves itself on the loop as `#[kanitool::loop_modifies]`, for the invariant to take. Both macros recognize these attributes by the last segment of their path, so that re-exports such as `kani_core::loop_invariant` work. - The loop contract pass finds the binding of each loop by walking up the dominator tree from the loop head, stopping at the head of another loop with a loop contract and at a binding of another loop. Loops without a contract do not stop the walk: one can be between the binding and the loop (in a `#[kani::loop_decreases]` expression), and the binding of a loop that is the first statement in the body of a `loop` is in the head of that `loop`. The pass records the binding with the instance of the register function of the loop, like the locals above. Codegen keeps the targets of each clause by that instance and the instance of the function, and the hook of each loop takes its own clause. - Codegen only skips the assignment of a binding that the pass attached to a loop. It used to skip every assignment to a local whose name contains `kani_loop_modifies`, including writes through it. - The bindings are not copied to the head of an enclosing loop (`move_storagelive_assign_to_loophead`) anymore. That added them to the write set of the enclosing loop, which failed `Check assigns clause inclusion` with three nested loops. The decreases clause is not changed here (see model-checking#4946). **Other `loop_modifies` changes that come with the new binding.** They can change the result of a program: - The targets of several `#[kani::loop_modifies]` attributes on one loop are combined. Only the attribute closest to the loop used to be applied. - A `#[kani::loop_modifies]` on a loop without `#[kani::loop_invariant]` is ignored with a warning, as model-checking#4946 does for a decreases clause. It used to be applied to the next loop with a loop invariant. - The binding is a tuple, even for a single target. MIR optimizations merged the binding of a clause whose only target is a variable (e.g. `#[kani::loop_modifies(p)]` with a raw pointer `p`, or `t` with `t: &mut u8`) with that variable, which then had the name of the binding. When the variable is an argument, the clause was dropped (the case from the review of this PR), and codegen took the writes through the variable for the binding, so it skipped them (e.g. after the loop) or panicked (in the loop). When the variable is a local, Kani panicked. - Codegen generates each target of a clause on its own. It paired the operands of the binding tuple with the fields of the generated tuple, which are in the order of its layout: with a slice first and two references, Kani panicked, and with slices of different element sizes, the target of a slice could cover the wrong number of bytes and miss a write outside of the clause. This already happened on `main`, and combining attributes makes such tuples more likely. - The targets are now evaluated right before the loop, also when the clause is written before the invariant. **Several `#[kani::loop_invariant]` attributes on one loop are now combined into their conjunction.** Each attribute added its own call to a register function, but only one of them was the loop head: on a `while` loop, the invariants of all but the last attribute were silently neither checked nor assumed, and on a `for` loop, whose attributes after the invariant are now kept, a second invariant failed to compile 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, so the first attribute now takes the others out of the loop and uses the conjunction of all invariants, for `while`, `loop`, `while let` and `for` loops. This changes the result of some programs: a `while` loop whose dropped invariant was false now fails `Check invariant before entry` or `Check invariant after step`, and a loop that needs all of its invariants now verifies. **A `loop_modifies` clause without targets is now applied.** A loop whose clause had no target got an inferred write set, so it 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 on `main` with an empty clause (`#[kani::loop_modifies()]`, whose `()` binding MIR optimizations also removed), and with a clause whose targets all have zero size, since codegen drops those targets (it did not drop a single zero-sized target, which made CBMC report pointer failures). Codegen now tracks whether a loop has a clause separately from its targets, drops a single zero-sized target as well, and when a clause has no target left (also after adding the locals above), uses an object that no code writes as its only target. For an empty clause, the macro binds a reference to a zero-sized local, which MIR optimizations keep. This can also change results: a loop with an empty or zero-sized clause that writes a variable declared before it now fails its assigns check. A `#[kani::loop_decreases]` written after the invariant on a `for` loop is now carried over as well, but its measure is not checked yet: a plain variable measure produces no decreases check because of model-checking#4942 (fix in model-checking#4946), and an arithmetic measure runs into model-checking#4585. So this PR has no verification test for `loop_decreases`. The loop contracts documentation now says which variables do not need to be listed in a `loop_modifies` clause, when its targets are evaluated, that several invariants or several `loop_modifies` attributes of a loop are combined, and that a `loop_modifies` on a loop without an invariant is ignored. Resolves model-checking#4929. Resolves model-checking#4906. Resolves model-checking#4940. ### Testing All the new tests are in `tests/expected/loop-contract`. - `for_loop_modifies.rs`: complete `loop_modifies` clauses on `for` loops, which only list variables declared before the loop. It covers both attribute orders, the patterns `x`, `(i, j)`, `&x`, `_` and `(k, x)` over `enumerate()`, a variable declared in the loop body, `prev`, nested `for` loops, and the indexed place `&out[0]` in both orders (the two cases from the review of model-checking#4930). On `main`, three harnesses fail with `Check that x is assignable`, `Check that kani_index_... is assignable` or `Check that var_25 is assignable`, and the harnesses with the clause after the invariant pass only because the clause is dropped. With the attributes carried over but without the other changes, `indexed_place_invariant_then_modifies` crashes with `not a loop head`. With this PR, all 11 harnesses verify. - `for_loop_modifies_fail.rs`, the test removed from model-checking#4930, with six harnesses that must each fail exactly their assigns check: two loops write `j`, which is not in the clause, one per attribute order; one writes `j` through a reference declared in the loop body; one writes `out[1]` with a clause for `&out[0]`; and two nested `for` loops (one per attribute order of the outer clause) whose outer loop writes `y`, which its clause does not list, while the inner loop has a clause of its own. On `main`, only `modifies_then_invariant` fails, and it also reports the generated locals; the nested ones verify because the clause of the outer loop is replaced by that of the inner loop. - `for_loop_on_entry_call.rs`: a `for` loop invariant with `on_entry(v.len())`. On `main`, Kani panics with `not a loop head`. With this PR, it verifies. - `loop_modifies_loop_locals.rs`: `while` loops with complete clauses, one with a call in the body (the example from model-checking#4906), one with `prev`, and the first one again in a generic function instantiated twice and in a closure (each loop has its own register function instance). On `main`, they fail with `Check that var_15 is assignable` (and `var_14`, `var_16`, `x`) or `Check that __kani_prev_var_... is assignable`. With this PR, all four verify. - `loop_modifies_not_added_fail.rs` (suggested in review): a variable declared before the loop that the loop writes before reading it must still fail its assigns check, and a variable declared in the loop body must still be dead after its scope. - `loop_modifies_own_loop.rs` (the two cases from the review, plus variants): nested loops whose outer clause must not go to the inner loop, which writes a variable declared in the body of the outer loop, for `for` and `while` loops and both attribute orders; and a clause (empty or not) on a `loop { break; }`, which must not go to the next loop. All six verify. On `main`, the `while` versions, the clause-before-invariant `for` version and the non-empty clause on `loop { break; }` fail. - `loop_modifies_own_loop_fail.rs`: loops that write a `bad` that their clause does not list, with a loop without a loop contract between the clause and the loop (in the iterable expression of a `for` loop or in an `on_entry` expression with the clause written first, or in a `loop_decreases` expression) or around the loop (the loop is the first statement in the body of a `loop`), and with the invariant or the clause written with another path (a re-export). Each must fail with `Check that bad is assignable`. - `loop_modifies_nested.rs` and `loop_modifies_nested_fail.rs`: nested `while` loops with complete clauses on both loops, on the outer one only and on the inner one only, an inner counter declared in the body of the outer loop, a labeled `continue 'outer`, and three levels of loops (one with a single-target innermost clause, one with an empty clause on an innermost `loop { break; }`), which verify; and loops that write a `t` that their clause does not list (outer loops with a clause on both loops, on the outer one only, and with a branch between the outer binding and the outer loop head; a `for` loop with its clause written first followed by a loop without a clause; the middle one of three loops), which must each fail with `Check that t is assignable`. On `main`, where the outer clause is attached to the inner loop, `outer_loop_with_clause` and `labeled_continue` fail, and `both_loops_with_clause` and `join_before_outer_loop` verify. - `loop_modifies_multiple.rs`: two `loop_modifies` attributes on one loop, in each order relative to the invariant and on a `for` loop, verify; with an empty clause as the second attribute, a write to `w` must fail its assigns check. On `main`, the `while` loops fail with `Check that i is assignable`. It also has clauses whose first target is a slice, which Kani used to pair with the wrong target types: one with two references verifies (Kani panicked on it), and one with a slice of `u8`, a slice of `u64` and a reference must fail its assigns check for a write outside of the `u8` slice (it verified). - `loop_modifies_no_invariant.rs`: a `loop_modifies` on a loop without an invariant, which iterates or not, is reported with a warning and is not applied to the next loop. On `main`, both harnesses fail with `Check that j is assignable`. - `loop_modifies_pointer_target.rs`: clauses whose only target is a raw pointer argument, a `&mut` argument or a raw pointer local. The loops that only write through the target verify; the loops that also write another variable, and a write through the target after the loop that the assertion relies on, must fail. On `main`, `mut_ref_argument_fail` (the case from the review) and `write_after_loop_fail` verify, and Kani panics on the others. - `loop_invariant_multiple.rs`: two invariants on `while` and `for` loops. Every false invariant fails `Check invariant before entry`, whichever its position, and loops that need both invariants (one using `prev`, one using `kani::index`) verify. On `main`, a `while` loop with a false first invariant and a `for` loop with a false second invariant verify, and the loops that need both invariants fail. - `loop_modifies_empty.rs` and `loop_modifies_empty_fail.rs`: an empty clause, one or two zero-sized targets, and an empty clause on a `for` loop. With a write to a variable declared before the loop, each must fail its assigns check (on `main`, the empty and two-target cases verify); loops that only write their own variables verify. - Unit tests in `kani_macros` check that the rewritten `for` loop keeps its label and attributes, that the other `loop_invariant` attributes and the `loop_modifies` attributes of a loop (with any path, and the `#[kanitool::loop_modifies]` that a clause written first leaves) are taken out of it, and that the binding of a single target is a tuple. - With `--keep-temps`, a `#[kani::loop_decreases]` written after the invariant on a `for` loop now produces the `kani_loop_decreases` local. - Locally, with CBMC 6.11.0: `RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib`, `cargo clippy --workspace --tests -- -D warnings`, `RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings`, `cargo test -p kani-compiler`, `cargo fmt --check` and `scripts/kani-fmt.sh --check` pass, and so do the `expected` (519 passed, 15 ignored), `ui` (153 passed), `kani` (620 passed, 23 ignored) and `script-based-pre` (91 passed) suites. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <felisous@amazon.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.
Description
A
#[kani::loop_decreases]clause whose measure is a variable produced noCheck variant decreases after stepproperty, so a wrong measure verified (#4942).CBMC reads the
#spec_decreasesannotation of a loop latch as a list of measures:dfcc_cfg_info.cpptakesget_loop_decreases(loop.latch, ..).operands(), since the C front end stores__CPROVER_decreases(e1, ..., en)as an irep whose operands are the measures. Kani attached the measure expression itself. A measure without operands (a variable, a field, a constant) therefore gave an empty list and no check, and for any other measure CBMC used its operands as the measure. For example,m as u32andhi - loare computed through MIR temporaries before the loop, so CBMC compared a temporary that the loop never changes, and the check could only fail. This has been the case since #4564 (CBMC 6.8.0 also reads the operands).This PR emits the measure as the only operand of the annotation. Once the check is generated, other problems show up, which this PR also fixes:
yindecreases_fail_stale_measure.rs, or a parameter), copy propagation merges thekani_loop_decreasesbinding into that variable, so the binding has no assignment of its own and its debug name is attached to the variable. Codegen then took the definition of the variable (y = x) for the binding: it dropped the assignment and usedxas the measure. If the measure is a constant, the binding is removed. The macro now passes a reference to the binding to a local#[inline(never)]function, which keeps MIR optimizations (also with-Zmir-opt-level=2) from removing its assignment, and codegen recognizes the binding by its exact name instead of a substring of the variable name.a[i]), and if it is the only assignment to the binding (not anifexpression or a call such asx.wrapping_sub(i)). Otherwise the measure is now the value of the binding, which does not change in the loop, so the check fails. Before, such a clause was checked on a partly stale measure or on one branch only, or (for a call) not at all.CurrentFnCtx, since codegen may generate the closure of a quantifier while it generates a function. The loop contract pass no longer copies the binding of an inner loop to the head of the outer loop, which it did for all user variables declared in a loop body.-Z loop-contracts; a loop without a loop invariant is unwound, not abstracted. The reference said that the invarianttrueis used in that case, which was not what happened, so this PR updates it, and replaces the struct-field entry of the known bugs (struct fields now work) with one for measures computed before the loop.Measures that Kani computes before the loop (arithmetic with overflow checks, casts, calls) are still evaluated only once, so a correct measure of that kind still fails the check (#4585). With this PR it fails instead of silently passing in all cases. Measures that are variables, fields or dereferences of variables are checked at each iteration.
Resolves #4942
Testing
decreases_fail_wrong_measure.rsanddecreases_fail_stale_measure.rsfailed for other reasons (an overflow and a loop invariant that does not hold), and their.expectedfiles only requiredVERIFICATION:- FAILED. They are now fixed so that the decreases check is the only failure, and their.expectedfiles require that failure.decreases_fail_wrong_measure.rsuses the reproducer from#[kani::loop_decreases]with a plain variable measure generates no decreases check #4942, plus aforloop..expectedfiles of the tests that verify with a decreases clause (simple_while_loop_decreases,decreases_expr,decreases_loop_max,decreases_with_old,decreases_with_function_contract,loop_loop_decreases) now require the decreases check with status SUCCESS. Onmain, none of them has a decreases check.tests/expected/loop-contract/:decreases_variable.rs: a variable in awhileloop, aforloop and a loop whose invariant usesprev, and a dereference.decreases_struct_field.rs: renamed fromfixme_decreases_struct_field.rs, which now verifies, plus a wrong field.decreases_fail_constant_measure.rs: a literal and aconst.decreases_fail_unsupported_measure.rs: wrongif, method call anda[i]measures.decreases_nested_loops.rs: decreases clauses on both loops, on one of them, and a wrong clause on each.decreases_nested_loops_quantifier.rs: a wrong clause on an outer loop, in a harness with a quantifier.decreases_mir_opt_level.rs: a variable, an unmodified variable and an unmodified parameter, with-Zmir-opt-level=2.decreases_no_invariant.rs: the warning for a loop without a loop invariant and for a loop whose body always exits, and that their clauses are not checked on the next loop..expectedfiles fail withmain, and pass with this PR.fixme_decreases_with_modifies.rs(5 - i) still fails the decreases check (#[kani::loop_decreases]does not support struct field projections or arithmetic expressions #4585),fixme_multi_dim_decreases.rsis still rejected, andfixme_nested_loops_decreases.rsnow checks both decreases clauses with status SUCCESS but still failsCheck assigns clause inclusion, as onmain.decreases_binary_search.rsis unchanged. Its decreases check succeeds, but only because its harness finds the target in the first iteration, so the loop latch is not reached in the step case.cargo fmt --check,scripts/kani-fmt.sh --check,cargo clippy --workspace --tests -- -D warningsandRUSTFLAGS=--cfg=kani_sysroot cargo clippy --workspace -- -D warningspass, and so do theexpected(506 passed, 14 ignored),ui(152 passed),kani(620 passed, 23 ignored) andscript-based-pre(89 passed) suites.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.