Add a loop's dead temporaries and loop-body variables to an explicit loop_modifies

docs/src/reference/experimental/loop-contracts.md

@@ -5,6 +5,7 @@
 Loop contracts are used to specify invariants for loops for the sake of extending Kani's *bounded proofs* to *unbounded proofs*.
 A [loop invariant](https://en.wikipedia.org/wiki/Loop_invariant) is an expression that holds upon entering a loop and after every execution of the loop body.
 Loop contracts are composed of one or more loop invariants as well as optional `loop_modifies` attributes.
+A loop with several `#[kani::loop_invariant]` attributes has the conjunction (`&&`) of their invariants as its invariant.
 It captures something that does not change about every step of the loop.
 
 It is worth revisiting the discussion about [bounded proof](../../tutorial-loop-unwinding.md#bounded-proof) and
@@ -299,6 +300,31 @@ fn main() {
 }
 ```
 
+The targets are evaluated right before the loop, after the code that `#[kani::loop_invariant]` adds before it
+(e.g., the `on_entry` values and, for a `for` loop, the iterator).
+A loop with several `loop_modifies` attributes may modify the targets of all of them.
+A `loop_modifies` attribute on a loop without a `#[kani::loop_invariant]` is ignored with a warning,
+since Kani does not abstract such a loop: it unwinds it like any other loop.
+
+The `loop_modifies` clause only needs to list memory that exists outside of the loop.
+Kani adds the variables that it generates for the loop to the clause
+(the variables for `prev` and, for `for` loops, the pattern bindings and the loop index `kani::index`),
+as well as the variables declared in the loop body that it initializes before the loop.
+For example, the following loop verifies with a clause that only lists `sum`:
+```Rust
+#[kani::proof]
+fn main() {
+    let a: [u8; 10] = kani::any();
+    let mut sum: u32 = 0;
+    #[kani::loop_invariant(sum <= kani::index as u32 * 255)]
+    #[kani::loop_modifies(&sum)]
+    for (_i, x) in a.iter().enumerate() {
+        let y = *x as u32;
+        sum = sum + y;
+    }
+}
+```
+
 ## Decreases clauses (Termination proofs)
 
 ### Why termination matters

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -8,7 +8,6 @@ use crate::codegen_cprover_gotoc::codegen::function::rustc_public_bridge::region
 use crate::codegen_cprover_gotoc::context::LoopDecreases;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
-use cbmc::goto_program::ExprValue;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use rustc_abi::Size;
 use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
@@ -71,20 +70,18 @@ impl GotocCtx<'_, '_> {
         .call(vec![effective_ptr, size])
     }
 
+    /// The assigns targets of a loop modifies clause, given the right-hand side of its binding:
+    /// a tuple of pointers to the targets (see `loop_modifies_binding` in `kani_macros`), or a
+    /// reference to a local of zero size for an empty clause.
     pub fn rvalue_to_assign_targets(&mut self, rvalue: &Rvalue, location: Location) -> Vec<Expr> {
-        let assigns = self.codegen_rvalue_stable(rvalue, location);
-        let assigns_value = assigns.value().clone();
-        let assign_exprs = if let ExprValue::Struct { values } = assigns_value {
-            values.clone()
-        } else {
-            vec![assigns.clone()]
-        };
         match rvalue {
-            Rvalue::Aggregate(_agg_kind, operands) => {
-                let mut ptr_exprs = Vec::new();
-                for (operand, expr) in operands.iter().zip(assign_exprs.iter()) {
+            // Generate each operand on its own, rather than the tuple: the fields of the
+            // generated tuple are in the order of its layout, which can differ from the order of
+            // the operands.
+            Rvalue::Aggregate(_agg_kind, operands) => operands
+                .iter()
+                .filter_map(|operand| {
                     let operand_ty = self.operand_ty_stable(operand);
-                    debug!("Ty {:?}", operand_ty);
                     // Do not emit an assigns target for a pointer to a ZST. Havocking a
                     // zero-sized location is a no-op (a ZST has a single inhabitant and
                     // occupies zero bytes), so dropping it preserves soundness, while
@@ -93,14 +90,25 @@ impl GotocCtx<'_, '_> {
                     // capture-free closure). This mirrors the function-contract handling
                     // in `codegen_modifies_target`.
                     if pointee_type_stable(operand_ty).is_some_and(|ty| self.is_zst_stable(ty)) {
-                        continue;
+                        return None;
                     }
-                    let ptr_expr = self.ty_to_assign_target(operand_ty, expr);
-                    ptr_exprs.push(ptr_expr)
+                    let expr = self.codegen_operand_stable(operand);
+                    Some(self.ty_to_assign_target(operand_ty, &expr))
+                })
+                .collect(),
+            // A single target. Like above, a pointer to a ZST is not a target, and neither is
+            // the reference to a local of zero size of an empty clause.
+            _ => {
+                let rvalue_ty = self.rvalue_ty_stable(rvalue);
+                if self.is_zst_stable(rvalue_ty)
+                    || pointee_type_stable(rvalue_ty).is_some_and(|ty| self.is_zst_stable(ty))
+                {
+                    vec![]
+                } else {
+                    let assigns = self.codegen_rvalue_stable(rvalue, location);
+                    vec![self.ty_to_assign_target(rvalue_ty, &assigns)]
                 }
-                ptr_exprs
             }
-            _ => vec![assigns.dereference()],
         }
     }
 
@@ -230,6 +238,27 @@ impl GotocCtx<'_, '_> {
         self.tcx.dcx().span_warn(rustc_internal::internal(self.tcx, span), msg);
     }
 
+    /// `StorageLive(var_id)`: see the `StorageLive` and `StorageDead` case of
+    /// [GotocCtx::codegen_statement].
+    pub fn codegen_storage_live(&mut self, var_id: Local, location: Location) -> Stmt {
+        if !self.current_fn().is_address_taken_local(var_id) {
+            Stmt::skip(location)
+        } else {
+            let global_dead_object = cbmc::global_dead_object(&self.symbol_table);
+            Stmt::assign(
+                global_dead_object.clone(),
+                global_dead_object
+                    .clone()
+                    .eq(self
+                        .codegen_local(var_id, location)
+                        .address_of()
+                        .cast_to(global_dead_object.typ().clone()))
+                    .ternary(global_dead_object.typ().null(), global_dead_object),
+                location,
+            )
+        }
+    }
+
     /// Generate Goto-C for MIR [Statement]s.
     /// This does not cover all possible "statements" because MIR distinguishes between ordinary
     /// statements and [Terminator]s, which can exclusively appear at the end of a basic block.
@@ -251,10 +280,17 @@ impl GotocCtx<'_, '_> {
             StatementKind::Assign(lhs, rhs) => {
                 let lty = self.place_ty_stable(lhs);
                 let rty = self.rvalue_ty_stable(rhs);
-                let localname = self.codegen_var_name(&lhs.local);
-                if localname.contains("kani_loop_modifies") {
+                let instance = self.current_fn().instance_stable();
+                if lhs.projection.is_empty()
+                    && let Some(register_fn) =
+                        self.transformer.loop_of_modifies_binding(instance, lhs.local)
+                {
+                    // The binding of the loop modifies clause of the loop that the loop contract
+                    // pass determined (see `LoopContractPass::find_loop_modifies_bindings`).
+                    // Record the clause for that loop, even if no target is left (e.g. an empty
+                    // clause, or only targets of zero size).
                     let assigns = self.rvalue_to_assign_targets(rhs, location);
-                    self.current_loop_modifies = assigns.clone();
+                    self.loop_modifies.insert((instance, register_fn), assigns);
                     return Stmt::skip(location);
                 }
                 if self.is_loop_decreases_binding(lhs.local) {
@@ -357,24 +393,7 @@ impl GotocCtx<'_, '_> {
             // This approach will also work when there are multiple occurrences of StorageLive (or
             // StorageDead) on a path, or across control-flow branches, and even when StorageDead
             // occurs without a preceding StorageLive.
-            StatementKind::StorageLive(var_id) => {
-                if !self.current_fn().is_address_taken_local(*var_id) {
-                    Stmt::skip(location)
-                } else {
-                    let global_dead_object = cbmc::global_dead_object(&self.symbol_table);
-                    Stmt::assign(
-                        global_dead_object.clone(),
-                        global_dead_object
-                            .clone()
-                            .eq(self
-                                .codegen_local(*var_id, location)
-                                .address_of()
-                                .cast_to(global_dead_object.typ().clone()))
-                            .ternary(global_dead_object.typ().null(), global_dead_object),
-                        location,
-                    )
-                }
-            }
+            StatementKind::StorageLive(var_id) => self.codegen_storage_live(*var_id, location),
             StatementKind::StorageDead(var_id) => {
                 if !self.current_fn().is_address_taken_local(*var_id) {
                     Stmt::skip(location)

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -94,8 +94,11 @@ pub struct GotocCtx<'tcx, 'r> {
     pub transformer: &'r mut BodyTransformation,
     /// If there exist some usage of loop contracts int context.
     pub has_loop_contracts: bool,
-    /// Track loop assign clause
-    pub current_loop_modifies: Vec<Expr>,
+    /// The targets of the loop modifies clause of each loop whose clause binding has been
+    /// generated but whose loop latch has not, by the instance of the function that contains the
+    /// loop and the instance of the register function of the loop. A loop without an entry has no
+    /// clause, which is not the same as a clause without targets.
+    pub loop_modifies: HashMap<(Instance, Instance), Vec<Expr>>,
 }
 
 /// Constructor
@@ -126,7 +129,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
             concurrent_constructs: FxHashMap::default(),
             transformer,
             has_loop_contracts: false,
-            current_loop_modifies: Vec::new(),
+            loop_modifies: HashMap::new(),
         }
     }
 

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -880,10 +880,35 @@ impl GotocHook for LoopInvariantRegister {
 
             let mut stmt = Stmt::goto(bb_label(target.unwrap()), loc)
                 .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)));
-            let assigns = gcx.current_loop_modifies.clone();
-            if !assigns.is_empty() {
-                stmt = stmt.with_loop_modifies(assigns.clone());
-                gcx.current_loop_modifies.clear();
+            let current_fn = gcx.current_fn().instance_stable();
+            let mut storage_live = Vec::new();
+            if let Some(mut assigns) = gcx.loop_modifies.remove(&(current_fn, instance)) {
+                // The user wrote a loop modifies clause, possibly without any target. Add the
+                // locals that the loop contract transformation makes live across iterations of
+                // this loop, which the user cannot name (without a user clause, CBMC infers the
+                // clause instead).
+                let generated =
+                    gcx.transformer.generated_loop_modifies(current_fn, instance).to_vec();
+                // The storage of such a local can end in the loop body, which can make it the
+                // dead object (see `codegen_storage_live`) when the latch jumps back to the
+                // loop head, where the loop havocs it. It is dead there: mark its storage live,
+                // as its `StorageLive` in the body would.
+                storage_live =
+                    generated.iter().map(|local| gcx.codegen_storage_live(*local, loc)).collect();
+                assigns.extend(generated.into_iter().map(|local| gcx.codegen_local(local, loc)));
+                if assigns.is_empty() {
+                    // The clause has no target (e.g. `#[kani::loop_modifies()]`, or only targets
+                    // of zero size). CBMC infers the write set of a loop whose assigns clause has
+                    // no target, so use an object that no code writes as the only target instead.
+                    let nothing = gcx.ensure_global_var(
+                        "__kani_loop_assigns_nothing",
+                        false,
+                        Type::unsigned_int(8),
+                        loc,
+                    );
+                    assigns.push(nothing.to_expr());
+                }
+                stmt = stmt.with_loop_modifies(assigns);
             }
             // The decreases clause of this loop, if any, was attached to the head of the loop,
             // which is the target of this latch (see `codegen_block`).
@@ -895,15 +920,14 @@ impl GotocHook for LoopInvariantRegister {
 
             // Add `free(0)` to make sure the body of `free` won't be dropped to
             // satisfy the requirement of DFCC.
-            Stmt::block(
-                vec![
-                    BuiltinFn::Free
-                        .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
-                        .as_stmt(loc),
-                    stmt,
-                ],
-                loc,
-            )
+            let mut stmts = vec![
+                BuiltinFn::Free
+                    .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
+                    .as_stmt(loc),
+            ];
+            stmts.extend(storage_live);
+            stmts.push(stmt);
+            Stmt::block(stmts, loc)
         } else {
             // When loop-contracts is not enabled, codegen
             // assign_to = true