Repository navigation
Conversation
Use the same loop parser for invariants, modifies, and decreases. Consume a match-arm comma without retaining it in the generated statement, reject mixed terminators and non-loop inputs, and report malformed predicates without panic. Cover loop/while/for syntax, attribute ordering, a failing decreases check, and invalid-input diagnostics.
github-actions
Bot
added
Z-EndToEndBenchCI
v3risec
changed the title
There was a problem hiding this comment.
🟢 Approval recommended
No active review issues remain for the loop-contract parsing and diagnostic changes.
No open issues 🎉
What changed in this PR
Fixes Kani’s loop contract macros when a loop appears directly in a match arm, without changing loop transformation or modifies-clause behavior.
Changes:
- Adds a shared parser for loop expressions with an optional semicolon or trailing comma, used by all three loop contract attributes.
- Replaces parsing panics with normal compile errors.
- Adds parser, match-arm, attribute-order, diagnostic, and negative termination-check regressions.
| File | Description |
|---|---|
tests/ui/loop-contract-attributes/main.rs |
Tests invalid attribute placement and malformed invariant input. |
tests/ui/loop-contract-attributes/expected |
Records expected compile diagnostics. |
tests/expected/loop-contract/match_decreases_stale.rs |
Tests rejection of a nondecreasing termination measure. |
tests/expected/loop-contract/match_decreases_stale.expected |
Requires the termination check to fail. |
tests/expected/loop-contract/loop_match_expression.rs |
Covers match-arm loop forms and different attribute orders. |
tests/expected/loop-contract/loop_match_expression.expected |
Requires all four harnesses to verify successfully. |
library/kani_macros/src/sysroot/loop_contracts/mod.rs |
Introduces the shared parser, integrates diagnostics, and adds parser unit tests. |
Review effort: Balanced
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
Thanks, this is a clean fix: one parser for all three attributes, compile errors instead of panics, and a negative decreases test showing the check still fires inside a match arm. I added [C] Bug, [F] Crash and Z-Contracts.
| Err(error) => return error.to_compile_error().into(), | ||
| }; | ||
| // Validate that the attribute is applied to a loop statement. | ||
| match &loop_stmt { |
There was a problem hiding this comment.
Nit: LoopInput already rejects non-loops, so this check can't fire any more. Please remove it.
There was a problem hiding this comment.
Removed the redundant check. Thanks!
| // Check that the targets parse. | ||
| let _ = parse_macro_input!(attr with Punctuated::<Expr, Token![,]>::parse_terminated); | ||
| let mut loop_stmt: Stmt = syn::parse(item.clone()).unwrap(); | ||
| let LoopInput(mut loop_stmt) = match syn::parse(item.clone()) { |
There was a problem hiding this comment.
Nit: loop_invariant uses parse_macro_input!(item as LoopInput). Please use the same form here and in loop_decreases (line 1107).
There was a problem hiding this comment.
Updated both macros to use parse_macro_input! consistently.
| false => (), | ||
| } | ||
| assert_eq!(count, 3); | ||
| } |
There was a problem hiding this comment.
Nit: please add one labeled loop ('outer: loop) in a match arm, since labels go through the same parser.
There was a problem hiding this comment.
Added a match-arm regression test with 'outer: loop and break 'outer.
feliperodri
added
[C] Bug
Use parse_macro_input consistently for loop contract attributes, preserving original tokens for the loop_modifies warning path. Remove the redundant loop type check already enforced by LoopInput. Add a labeled match-arm loop with a labeled break, and update the expected harness count while retaining existing diagnostics and negative checks.
Summary
Fix loop contract attribute parsing for loop expressions used directly as match arms.
Previously, the token stream passed to
#[kani::loop_invariant],#[kani::loop_modifies], or#[kani::loop_decreases]could include the match arm's trailing comma. Parsing it as asyn::Stmtfailed, and the macro could panic instead of expanding the loop or reporting a useful diagnostic.Changes
LoopInputparser forloop,while, andforexpressions, supporting an optional statement semicolon or match-arm trailing comma.Testing
loop-contractexpected tests pass, including positive and negative decreases checks.kani_macrosunit tests pass.Related work
This fixes match-arm attribute parsing, independently of the loop transformation and modifies-clause fixes in #4930, #4947, #5068, and #5071.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.