Repository navigation
Conversation
At -Zmir-opt-level=2 and above, MIR optimizations removed the kani_loop_modifies binding because nothing read it, so codegen found no modifies clause and CBMC inferred the write set from the loop body, admitting writes the clause omitted. Pass a reference to the binding to an #[inline(never)] function, as model-checking#4946 did for loop_decreases, so the assignment survives optimization and the declared clause is enforced. The keep-alive adds two MIR locals before the loop, shifting the CBMC temporary indices in the existing loop_modifies assigns checks; the six loop_assigns_for_* expected files are updated to match (behavior unchanged, only the var_N index in the descriptions). Resolves model-checking#5053
github-actions
Bot
added
Z-EndToEndBenchCI
Member
|
@kasimte could you resolve the branch conflicts? |
Contributor
There was a problem hiding this comment.
Warning
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Copilot review overview
2 open issues
What changed in this PR
This PR fixes an enforcement gap where #[kani::loop_modifies] stops being honored under higher MIR optimization levels by ensuring the internal kani_loop_modifies binding remains visible through optimization.
Changes:
- Add a regression test that runs with
-Zmir-opt-level=2and checks both incomplete and complete modifies clauses. - Update multiple loop-contract golden outputs due to shifted CBMC temporary indices.
- Update the loop-contract macro expansion to keep the modifies binding alive via an
#[inline(never)]keep-alive call.
| File | Description |
|---|---|
| tests/expected/loop-contract/modifies_mir_opt_level.rs | New regression test for loop modifies enforcement under MIR opt level 2. |
| tests/expected/loop-contract/modifies_mir_opt_level.expected | New expected output validating the regression failure mode. |
| tests/expected/loop-contract/loop_assigns_for_ref.expected | Update golden to match new CBMC temp indices. |
| tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected | Update golden to match new CBMC temp indices. |
| tests/expected/loop-contract/loop_assigns_for_ptr.expected | Update golden to match new CBMC temp indices. |
| tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.expected | Update golden to match new CBMC temp indices. |
| tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected | Update golden to match new CBMC temp indices. |
| tests/expected/loop-contract/loop_assigns_for_empty_slice_fail.expected | Update golden to match new CBMC temp indices. |
| library/kani_macros/src/sysroot/loop_contracts/mod.rs | Macro change to try to prevent the modifies binding from being optimized out. |
Review effort: Lite
| let loop_assign_keep_stmts: Vec<Stmt> = parse_quote! { | ||
| #[inline(never)] | ||
| #[kanitool::fn_marker = "kani_keep_loop_modifies_binding"] | ||
| const fn kani_keep_loop_modifies_binding<T>(_binding: &T) {} |
Comment on lines
+921
to
+926
| let loop_assign_keep_stmts: Vec<Stmt> = parse_quote! { | ||
| #[inline(never)] | ||
| #[kanitool::fn_marker = "kani_keep_loop_modifies_binding"] | ||
| const fn kani_keep_loop_modifies_binding<T>(_binding: &T) {} | ||
| kani_keep_loop_modifies_binding(&#loop_assign_ident); | ||
| }; |
Copilot stopped reviewing on behalf of
feliperodri due to an error
November 6, 2026 19:48
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.
Fixes #5053.
#[kani::loop_modifies]is not enforced at-Zmir-opt-level=2and above. Thekani_loop_modifiesbinding is optimized out before codegen reads it. As suggested in the issue, the fix passes a reference to the binding to an#[inline(never)]function. The binding then survives optimization.Testing
modifies_mir_opt_level.rs(-Zmir-opt-level=2): an undeclared write failsCheck that hidden is assignable. A complete clause verifies.loop_assigns_for_*.expectedgoldens are updated to match (same statuses,var_Nonly).By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.