Check #[kani::loop_decreases] clauses whose measure is a variable

[Talha-Dmr]

Description

A #[kani::loop_decreases] clause whose measure is a variable produced no Check variant decreases after step property, so a wrong measure verified (#4942).

CBMC reads the #spec_decreases annotation of a loop latch as a list of measures: dfcc_cfg_info.cpp takes get_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 u32 and hi - lo are 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:

• If the measure is a variable that is assigned only once (e.g. y in decreases_fail_stale_measure.rs, or a parameter), copy propagation merges the kani_loop_decreases binding 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 used x as 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.
• Codegen takes the measure from the right-hand side of the assignment to the binding, which CBMC evaluates before and after each iteration. That right-hand side is the measure only if it reads user variables and arguments, and not temporaries that hold values from before the loop (e.g. the copy of the index in a[i]), and if it is the only assignment to the binding (not an if expression or a call such as x.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.
• Codegen attached a clause to the next loop latch that it generated. With nested loops, the latch of the inner loop is generated first, so the clause of the outer loop went to the inner loop, and the clause of a loop without a loop invariant went to a later loop, possibly of another function. A clause is now attached to the first loop head that codegen generates after its binding (the binding is right before its loop, and blocks are generated in reverse postorder), and the loop latch takes the clause of its loop head. Loop heads are the targets of back edges and of the calls that register loop contracts (a loop whose body always exits has no back edge). This state is kept per function in 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.
• A clause that is not attached to a loop with a loop invariant is reported with a warning and ignored, as without -Z loop-contracts; a loop without a loop invariant is unwound, not abstracted. The reference said that the invariant true is 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.rs and decreases_fail_stale_measure.rs failed for other reasons (an overflow and a loop invariant that does not hold), and their .expected files only required VERIFICATION:- FAILED. They are now fixed so that the decreases check is the only failure, and their .expected files require that failure. decreases_fail_wrong_measure.rs uses the reproducer from #[kani::loop_decreases] with a plain variable measure generates no decreases check #4942, plus a for loop.
• The .expected files 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. On main, none of them has a decreases check.
• New tests in tests/expected/loop-contract/:
  • decreases_variable.rs: a variable in a while loop, a for loop and a loop whose invariant uses prev, and a dereference.
  • decreases_struct_field.rs: renamed from fixme_decreases_struct_field.rs, which now verifies, plus a wrong field.
  • decreases_fail_constant_measure.rs: a literal and a const.
  • decreases_fail_unsupported_measure.rs: wrong if, method call and a[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.
• All the new and updated .expected files fail with main, and pass with this PR.
• The other fixme tests: 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.rs is still rejected, and fixme_nested_loops_decreases.rs now checks both decreases clauses with status SUCCESS but still fails Check assigns clause inclusion, as on main.
• decreases_binary_search.rs is 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.
• Locally, with CBMC 6.11.0: cargo fmt --check, scripts/kani-fmt.sh --check, cargo clippy --workspace --tests -- -D warnings and RUSTFLAGS=--cfg=kani_sysroot cargo clippy --workspace -- -D warnings pass, and so do the expected (506 passed, 14 ignored), ui (152 passed), kani (620 passed, 23 ignored) and script-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.

[Copilot]

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]

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.