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

cprover_bindings/src/irep/to_irep.rs

@@ -566,7 +566,13 @@ impl ToIrep for StmtBody {
                         assigns.iter().map(|assign| assign.to_irep(mm)).collect(),
                     )])
                 });
-                let decreases = loop_decreases.clone().map(|dec| dec.to_irep(mm));
+                // CBMC takes the operands of the `#spec_decreases` irep as the components of the
+                // (lexicographic) measure, like the C front end does for `__CPROVER_decreases`.
+                // Make the measure the only operand, as otherwise a measure without operands
+                // (e.g. a variable) would be ignored, and the operands of other measures (e.g. the
+                // operand of a cast) would be used as the measure instead.
+                let decreases =
+                    loop_decreases.clone().map(|dec| Irep::just_sub(vec![dec.to_irep(mm)]));
                 code_irep(IrepId::Goto, vec![])
                     .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()))
                     .with_named_sub_option(IrepId::CSpecLoopInvariant, inv)

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

@@ -437,9 +437,10 @@ becomes negative but the loop guard is false, that is acceptable.
 ### Interaction with loop invariants
 
 Decreases clauses work in conjunction with loop invariant clauses. The invariant establishes the
-context (the inductive hypothesis) under which the decreases check is performed. If a decreases
-clause is annotated on a loop without an invariant clause, the weakest possible invariant (`true`)
-is used to model an arbitrary iteration.
+context (the inductive hypothesis) under which the decreases check is performed. A decreases
+clause on a loop without an invariant clause is ignored with a warning, since Kani does not
+abstract such a loop: it unwinds it like any other loop. To prove the termination of a loop with
+the weakest possible invariant, use `#[kani::loop_invariant(true)]`.
 
 In practice, you almost always want both: the invariant constrains the state space, and the
 decreases clause proves progress within that constrained space.
@@ -591,9 +592,8 @@ Loop contracts comes with the following limitations.
 3. We don't check if loop contracts (invariants, decreases clauses) are side-effect free. A loop contract with a side effect could lead to an unsound proof result. Make sure that the specified loop contracts are side-effect free.
 4. Decreases clauses only support integer-typed expressions. See the [decreases clause limitations](#decreases-clause-limitations-and-comparison-with-other-tools) section for a detailed comparison with other verification tools.
 5. Decreases clauses have the following known bugs (tracked in [#3168](https://github.com/model-checking/kani/issues/3168)):
-   - **Struct field projections** in decreases expressions (e.g., `#[kani::loop_decreases(s.field)]`) are not correctly processed by CBMC — the check always fails even when the measure genuinely decreases.
+   - **Measures computed before the loop.** Kani evaluates a measure at each iteration only if it reads variables of the function directly (e.g., `x`, `s.field` or `*p`). Other measures, such as arithmetic with overflow checks (e.g., `n - i`), casts, indexing, function calls, constants, or variables captured by a closure, are computed once before the loop, so the check fails even when the measure decreases, and Kani reports a warning ([#4585](https://github.com/model-checking/kani/issues/4585)).
    - **Multi-dimensional decreases** (e.g., `#[kani::loop_decreases(a, b)]`) are not correctly processed — CBMC does not perform lexicographic comparison on tuple expressions passed through Kani's irep encoding.
-   - **Combining `loop_decreases` with `loop_modifies`** causes the assigns clause check to conflict with the decreases instrumentation.
    - **Nested loops with decreases** on both inner and outer loops can cause assigns clause conflicts.
 
    These limitations are documented as `fixme` tests in `tests/expected/loop-contract/`.

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

@@ -3,7 +3,7 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use rustc_public::mir::{BasicBlock, BasicBlockIdx, Body};
-use std::collections::HashSet;
+use std::collections::{HashMap, HashSet};
 use tracing::debug;
 
 pub fn bb_label(bb: BasicBlockIdx) -> String {
@@ -19,6 +19,15 @@ impl GotocCtx<'_, '_> {
     /// `self.current_fn_mut().push_onto_block(...)`
     pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) {
         debug!(?bb, "codegen_block");
+        let clauses = self.current_fn_mut().loop_decreases_mut();
+        if clauses.loop_heads.contains(&bb)
+            && let Some(decreases) = clauses.pending.take()
+        {
+            // The binding of a decreases clause is right before its loop, and blocks are
+            // generated in reverse postorder, so the clause belongs to the first loop head that
+            // is generated after its binding. `LoopInvariantRegister` takes it from there.
+            clauses.by_head.insert(bb, decreases);
+        }
         let label = bb_label(bb);
         // the first statement should be labelled. if there is no statements, then the
         // terminator should be labelled.
@@ -56,6 +65,24 @@ pub fn reverse_postorder(body: &Body) -> impl Iterator<Item = BasicBlockIdx> {
     postorder(body, 0, &mut HashSet::with_capacity(body.blocks.len())).into_iter().rev()
 }
 
+/// The loop heads of `body`, i.e. the targets of its back edges, given its reachable basic
+/// blocks in reverse postorder.
+pub fn loop_heads(body: &Body, reverse_postorder: &[BasicBlockIdx]) -> HashSet<BasicBlockIdx> {
+    let position: HashMap<BasicBlockIdx, usize> =
+        reverse_postorder.iter().enumerate().map(|(position, bb)| (*bb, position)).collect();
+    reverse_postorder
+        .iter()
+        .flat_map(|bb| {
+            body.blocks[*bb]
+                .terminator
+                .successors()
+                .into_iter()
+                .filter(|succ| position[succ] <= position[bb])
+                .collect::<Vec<_>>()
+        })
+        .collect()
+}
+
 fn postorder(
     body: &Body,
     bb: BasicBlockIdx,

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

@@ -4,20 +4,42 @@
 //! This file contains functions related to codegenning MIR functions into gotoc
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
+use crate::codegen_cprover_gotoc::codegen::block::{loop_heads, reverse_postorder};
+use crate::kani_middle::attributes::KaniAttributes;
 use crate::kani_middle::readable_name;
 use cbmc::InternString;
 use cbmc::InternedString;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use rustc_public::CrateDef;
 use rustc_public::mir::mono::Instance;
-use rustc_public::mir::{Body, Local};
+use rustc_public::mir::{BasicBlockIdx, Body, Local, TerminatorKind};
 use rustc_public::ty::{RigidTy, TyKind};
 use std::collections::BTreeMap;
 use tracing::{debug, debug_span};
 
 /// Codegen MIR functions into gotoc
 impl GotocCtx<'_, '_> {
+    /// The heads of the loops of `body` with a loop invariant, i.e. the targets of the calls to
+    /// the functions that register loop contracts (see `LoopInvariantRegister`).
+    fn loop_contract_heads(&self, body: &Body) -> Vec<BasicBlockIdx> {
+        body.blocks
+            .iter()
+            .filter_map(|block| match &block.terminator.kind {
+                TerminatorKind::Call { func, target: Some(target), .. } => {
+                    let TyKind::RigidTy(RigidTy::FnDef(def, _)) =
+                        func.ty(body.locals()).ok()?.kind()
+                    else {
+                        return None;
+                    };
+                    (KaniAttributes::for_def_id(self.tcx, def.def_id()).fn_marker()
+                        == Some(rustc_span::Symbol::intern("kani_register_loop_contract")))
+                    .then_some(*target)
+                }
+                _ => None,
+            })
+            .collect()
+    }
+
     /// Declare variables according to their index.
     /// - Index 0 represents the return value.
     /// - Indices [1, N] represent the function parameters where N is the number of parameters.
@@ -92,7 +114,23 @@ impl GotocCtx<'_, '_> {
             self.codegen_declare_variables(&body, name.clone().into());
 
             // Get the order from internal body for now.
-            reverse_postorder(&body).for_each(|bb| self.codegen_block(bb, &body.blocks[bb]));
+            let blocks: Vec<_> = reverse_postorder(&body).collect();
+            if self.queries.args().unstable_features.contains(&"loop-contracts".to_string())
+                && body.var_debug_info.iter().any(|info| info.name == "kani_loop_decreases")
+            {
+                // Used to attach decreases clauses to their loops. The head of a loop with a loop
+                // invariant has no back edge if the body of the loop always exits.
+                let mut heads = loop_heads(&body, &blocks);
+                heads.extend(self.loop_contract_heads(&body));
+                self.current_fn_mut().loop_decreases_mut().loop_heads = heads;
+            }
+            blocks.into_iter().for_each(|bb| self.codegen_block(bb, &body.blocks[bb]));
+            // Report the decreases clauses that were not attached to a loop, e.g. the clause of a
+            // loop without a loop invariant.
+            let clauses = std::mem::take(self.current_fn_mut().loop_decreases_mut());
+            for decreases in clauses.pending.into_iter().chain(clauses.by_head.into_values()) {
+                self.report_ignored_loop_decreases(decreases.span);
+            }
 
             let loc = self.codegen_span_stable(instance.def.span());
             let stmts = self.current_fn_mut().extract_block();

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

@@ -5,6 +5,7 @@ use super::typ::FN_RETURN_VOID_VAR_NAME;
 use super::typ::TypeExt;
 use super::{PropertyClass, bb_label};
 use crate::codegen_cprover_gotoc::codegen::function::rustc_public_bridge::region_from_coverage_opaque;
+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;
@@ -17,7 +18,7 @@ use rustc_public::CrateDef;
 use rustc_public::abi::{ArgAbi, FnAbi, PassMode};
 use rustc_public::mir::mono::{Instance, InstanceKind};
 use rustc_public::mir::{
-    AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
+    AssertMessage, BasicBlockIdx, CopyNonOverlapping, Local, NonDivergingIntrinsic, Operand, Place,
     ProjectionElem, RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, Terminator,
     TerminatorKind,
 };
@@ -138,6 +139,97 @@ impl GotocCtx<'_, '_> {
         has_deref
     }
 
+    /// Whether `local` is the binding of a `#[kani::loop_decreases]` clause (see `loop_decreases`
+    /// in `kani_macros`).
+    fn is_loop_decreases_binding(&self, local: Local) -> bool {
+        self.current_fn().local_name(local).is_some_and(|name| name == "kani_loop_decreases")
+    }
+
+    /// Whether CBMC can evaluate `rvalue`, the right-hand side of the binding of a decreases
+    /// clause, before and after each iteration of the loop: it must only read user variables and
+    /// arguments, and not temporaries, whose values are computed before the loop. A constant is
+    /// not evaluated at each iteration either.
+    fn is_live_loop_decreases_measure(&self, rvalue: &Rvalue) -> bool {
+        let mut places = vec![];
+        collect_rvalue_places(rvalue, &mut places);
+        if places.is_empty() {
+            return false;
+        }
+        let arg_count = self.current_fn().arg_count();
+        places.iter().all(|place| {
+            let index_locals = place.projection.iter().filter_map(|elem| match elem {
+                ProjectionElem::Index(local) => Some(*local),
+                _ => None,
+            });
+            std::iter::once(place.local)
+                .chain(index_locals)
+                .all(|local| (1..=arg_count).contains(&local) || self.is_user_variable(&local))
+        })
+    }
+
+    /// Record `measure` as the measure of the decreases clause with binding `binding`, which is
+    /// attached to the first loop head generated after it (see `codegen_block`). If the measure
+    /// is `computed_once`, before the loop, the decreases check fails.
+    fn record_loop_decreases(
+        &mut self,
+        binding: Local,
+        measure: Expr,
+        computed_once: bool,
+        span: Span,
+    ) {
+        let decreases = LoopDecreases { binding, measure, computed_once, span };
+        let pending = self.current_fn_mut().loop_decreases_mut().pending.replace(decreases);
+        match pending {
+            Some(pending) if pending.binding == binding => {
+                // Another assignment of the same binding: report it once.
+                if computed_once && !pending.computed_once {
+                    self.report_loop_decreases_computed_once(span);
+                }
+            }
+            pending => {
+                if let Some(pending) = pending {
+                    self.report_ignored_loop_decreases(pending.span);
+                }
+                if computed_once {
+                    self.report_loop_decreases_computed_once(span);
+                }
+            }
+        }
+    }
+
+    /// Warn that the measure of the decreases clause with the binding at `span` is computed once,
+    /// before the loop, so that the decreases check fails.
+    fn report_loop_decreases_computed_once(&self, span: Span) {
+        let msg = "the measure of this `#[kani::loop_decreases]` clause is computed once, before \
+                   the loop, so the decreases check will fail even if the measure decreases";
+        self.tcx
+            .dcx()
+            .struct_span_warn(rustc_internal::internal(self.tcx, span), msg)
+            .with_note(
+                "Kani evaluates a measure at each iteration of the loop only if it reads \
+                 variables directly (e.g. `x`, `s.field` or `*p`). Other measures, such as \
+                 arithmetic with overflow checks, casts, indexing, function calls, `if` \
+                 expressions and constants, are computed before the loop.",
+            )
+            .with_note("see https://github.com/model-checking/kani/issues/4585")
+            .emit();
+    }
+
+    /// Warn that the decreases clause with the binding at `span` is ignored, since loop contracts
+    /// are not enabled.
+    fn report_loop_decreases_without_loop_contracts(&self, span: Span) {
+        let msg = "found `#[kani::loop_decreases]` without `-Z loop-contracts`. The decreases \
+                   clause will be ignored.";
+        self.tcx.dcx().span_warn(rustc_internal::internal(self.tcx, span), msg);
+    }
+
+    /// Warn that the decreases clause with the binding at `span` is not attached to a loop.
+    pub fn report_ignored_loop_decreases(&self, span: Span) {
+        let msg = "found `#[kani::loop_decreases]` that is not attached to a loop with \
+                   `#[kani::loop_invariant]`. The decreases clause will be ignored.";
+        self.tcx.dcx().span_warn(rustc_internal::internal(self.tcx, span), msg);
+    }
+
     /// 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.
@@ -165,24 +257,35 @@ impl GotocCtx<'_, '_> {
                     self.current_loop_modifies = assigns.clone();
                     return Stmt::skip(location);
                 }
-                if localname.contains("kani_loop_decreases") {
+                if self.is_loop_decreases_binding(lhs.local) {
                     if !self
                         .queries
                         .args()
                         .unstable_features
                         .contains(&"loop-contracts".to_string())
                     {
-                        let msg = "found `#[kani::loop_decreases]` without \
-                                   `-Z loop-contracts`. The decreases clause \
-                                   will be ignored.";
-                        let internal_span =
-                            rustc_internal::internal(self.tcx, stmt.source_info.span);
-                        self.tcx.dcx().span_warn(internal_span, msg);
+                        self.report_loop_decreases_without_loop_contracts(stmt.source_info.span);
                         return Stmt::skip(location);
                     }
-                    let decreases_expr = self.codegen_rvalue_stable(rhs, location);
-                    self.current_loop_decreases = Some(decreases_expr);
-                    return Stmt::skip(location);
+                    let pending_binding =
+                        self.current_fn().loop_decreases().pending.as_ref().map(|d| d.binding);
+                    if pending_binding != Some(lhs.local)
+                        && self.is_live_loop_decreases_measure(rhs)
+                    {
+                        // CBMC evaluates the right-hand side of the binding before and after each
+                        // iteration of the loop.
+                        let measure = self.codegen_rvalue_stable(rhs, location);
+                        let span = stmt.source_info.span;
+                        self.record_loop_decreases(lhs.local, measure, false, span);
+                        return Stmt::skip(location);
+                    }
+                    // The right-hand side is a constant or reads values computed before the loop
+                    // (e.g. a temporary holding the result of checked arithmetic), or the binding
+                    // is assigned more than once (e.g. the measure is an `if` expression). Use the
+                    // value of the binding as the measure instead, and assign it below. Since that
+                    // value does not change in the loop, the decreases check fails.
+                    let measure = self.codegen_local(lhs.local, location);
+                    self.record_loop_decreases(lhs.local, measure, true, stmt.source_info.span);
                 }
                 // we ignore assignment for all zero size types
                 if self.is_zst_stable(lty) {
@@ -398,6 +501,21 @@ impl GotocCtx<'_, '_> {
                 self.codegen_drop(place, target, loc)
             }
             TerminatorKind::Call { func, args, destination, target, .. } => {
+                if self.is_loop_decreases_binding(destination.local) {
+                    let span = term.source_info.span;
+                    if self.queries.args().unstable_features.contains(&"loop-contracts".to_string())
+                    {
+                        // The measure of a decreases clause is the result of a call, which is
+                        // only computed before the loop. Use the value of the binding as the
+                        // measure. Since that value does not change in the loop, the decreases
+                        // check fails.
+                        let measure =
+                            self.codegen_local(destination.local, self.codegen_span_stable(span));
+                        self.record_loop_decreases(destination.local, measure, true, span);
+                    } else {
+                        self.report_loop_decreases_without_loop_contracts(span);
+                    }
+                }
                 self.codegen_funcall(func, args, destination, target, term.source_info.span)
             }
             TerminatorKind::Assert { cond, expected, msg, target, .. } => {