Loop contracts: #[kani::loop_modifies] written after #[kani::loop_invariant] is silently dropped on while let and for loops #4929

I tried this code:

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]

// Both loops write `j`, which is not in the modifies clause.

#[kani::proof]
fn invariant_then_modifies() {
    let mut k: u8 = kani::any();
    let mut i: u8 = 0;
    let mut j: u8 = 0;
    #[kani::loop_invariant(i == j)]
    #[kani::loop_modifies(&k, &i)]
    while let Some(n) = k.checked_sub(1) {
        k = n;
        i = i.wrapping_add(1);
        j = j.wrapping_add(1);
    }
}

#[kani::proof]
fn modifies_then_invariant() {
    let mut k: u8 = kani::any();
    let mut i: u8 = 0;
    let mut j: u8 = 0;
    #[kani::loop_modifies(&k, &i)]
    #[kani::loop_invariant(i == j)]
    while let Some(n) = k.checked_sub(1) {
        k = n;
        i = i.wrapping_add(1);
        j = j.wrapping_add(1);
    }
}

using the following command line invocation:

kani while_let_modifies.rs -Z loop-contracts

with Kani version: 0.68.0, built from source at 7207ac1 (current main); CBMC 6.11.0; Arch Linux x86_64. I first saw it at 152c6a8.

I expected to see this happen: both harnesses fail with Check that j is assignable. The order of the loop contract attributes should not matter, and the existing loop_assigns_* tests write loop_modifies after loop_invariant.

Instead, this happened: only modifies_then_invariant fails. invariant_then_modifies verifies successfully, because its loop_modifies clause is ignored and CBMC infers the assigns clause instead:

Checking harness modifies_then_invariant...
Failed Checks: Check that j is assignable
VERIFICATION:- FAILED
Checking harness invariant_then_modifies...
VERIFICATION:- SUCCESSFUL

Same experiment for the other loop forms (the loop writes a variable that is not in loop_modifies):

Cause: #[kani::loop_invariant] rewrites a while let loop into loop { match .. } (while_let_rewrite in library/kani_macros/src/sysroot/loop_contracts/mod.rs) and a for loop into a while loop (transform_for_to_loop). The attributes written after #[kani::loop_invariant] are part of the loop expression that the macro receives, but both rewrites rebuild the loop from its condition (or pattern and iterator) and body only, so those attributes are lost and the let kani_loop_modifies = .. binding is never generated. Plain while and loop loops are modified in place and keep their attributes.

#[kani::loop_decreases] written after #[kani::loop_invariant] is dropped in the same way on while let and for loops (with --keep-temps, the kani_loop_decreases local is missing from the symbol table). The two rewrites also drop the loop label, so a labeled while let or for loop with a loop invariant whose body uses break 'outer fails to compile with E0426 (use of undeclared label 'outer).

Workaround: write #[kani::loop_modifies] and #[kani::loop_decreases] before #[kani::loop_invariant].