feat(contracts): Detect and warn about mutual recursion with #[kani::recursion]

The per-function REENTRY mechanism used by #[kani::recursion] only handles
direct recursion (f calls f) soundly. For mutual recursion (f calls g,
g calls f), the REENTRY flag for g is never set, so g's body executes
fully instead of being replaced by its contract. This is a silent
soundness gap — no error or warning was emitted.

This change adds check_mutual_recursion() in the contract transform pass.
When a function with #[kani::recursion] is being processed in
RecursiveCheck mode, we scan its MIR body for calls to other functions
that also have contracts AND #[kani::recursion]. For each such callee,
we check if the callee's body calls back to the original function. If
so, we emit a span_warn pointing at the call site.

We require both has_contract() and has_recursion() on the callee because
if the callee has a contract but no #[kani::recursion], Kani replaces
the call with the contract abstraction — no mutual recursion occurs.

Limitations:
- Only detects one level of indirection (f->g->f), not deeper chains.
- Reports only the first mutual-recursive callee per function.

Includes a test case (mutual_recursion_unsound.rs) with two mutually
recursive functions that triggers the warning.

Author: feliperodri

kani-compiler/src/kani_middle/transform/contracts.rs

@@ -302,6 +302,9 @@ impl TransformPass for FunctionWithContractPass {
         match instance.ty().kind().rigid().unwrap() {
             RigidTy::FnDef(def, args) => {
                 if let Some(mode) = self.contract_mode(tcx, *def) {
+                    if mode == ContractMode::RecursiveCheck {
+                        check_mutual_recursion(tcx, *def, &body);
+                    }
                     self.mark_unused(tcx, *def, &body, mode);
                     let new_body = self.set_mode(tcx, body, mode);
                     (true, new_body)
@@ -552,3 +555,74 @@ fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureD
             unreachable!()
         })
 }
+
+/// Check if a function with `#[kani::recursion]` is involved in mutual recursion.
+///
+/// Scans the function's MIR body for calls to other functions that also have
+/// `#[kani::recursion]`. For each such callee, checks if the callee's body calls
+/// back to the original function (one level of indirection). If so, emits a
+/// warning because the per-function REENTRY mechanism only handles direct
+/// recursion soundly.
+///
+/// We require both `has_contract()` and `has_recursion()` on the callee because
+/// if the callee has a contract but no `#[kani::recursion]`, Kani replaces the
+/// callee with its contract abstraction — no mutual recursion occurs.
+///
+/// Limitations:
+/// - Only detects one level of indirection (f→g→f), not deeper chains (f→g→h→f).
+///   TODO(#3316): Extend to detect deeper mutual recursion chains.
+fn check_mutual_recursion(tcx: TyCtxt, fn_def: FnDef, body: &Body) {
+    let fn_name = tcx.def_path_str(rustc_internal::internal(tcx, fn_def.def_id()));
+
+    for bb in body.blocks.iter() {
+        let TerminatorKind::Call { func, .. } = &bb.terminator.kind else { continue };
+        let Ok(func_ty) = func.ty(body.locals()) else { continue };
+        let TyKind::RigidTy(RigidTy::FnDef(callee_def, callee_args)) = func_ty.kind() else {
+            continue;
+        };
+
+        // Skip direct recursion (that's handled correctly by REENTRY).
+        if callee_def.def_id() == fn_def.def_id() {
+            continue;
+        }
+
+        // Only error when the callee also uses #[kani::recursion] with a contract.
+        // If the callee has a contract but no #[kani::recursion], Kani replaces
+        // the call with the contract abstraction, so no mutual recursion occurs.
+        let callee_attrs = KaniAttributes::for_def_id(tcx, callee_def.def_id());
+        if !callee_attrs.has_contract() || !callee_attrs.has_recursion() {
+            continue;
+        }
+
+        // Check if the callee calls back to us (one level deep).
+        let Ok(callee_instance) = Instance::resolve(callee_def, &callee_args) else { continue };
+        let Some(callee_body) = callee_instance.body() else { continue };
+
+        for callee_bb in callee_body.blocks.iter() {
+            let TerminatorKind::Call { func: callee_func, .. } = &callee_bb.terminator.kind else {
+                continue;
+            };
+            let Ok(callee_func_ty) = callee_func.ty(callee_body.locals()) else { continue };
+            let TyKind::RigidTy(RigidTy::FnDef(transitive_def, _)) = callee_func_ty.kind() else {
+                continue;
+            };
+
+            if transitive_def.def_id() == fn_def.def_id() {
+                let callee_name =
+                    tcx.def_path_str(rustc_internal::internal(tcx, callee_def.def_id()));
+                let span = rustc_internal::internal(tcx, bb.terminator.span);
+                tcx.dcx().span_err(
+                    span,
+                    format!(
+                        "`#[kani::recursion]` is used on `{fn_name}`, which calls \
+                         `{callee_name}` that calls back to `{fn_name}`. \
+                         Mutual recursion is not supported by contract verification \
+                         and produces unsound results. Only direct recursion \
+                         (a function calling itself) is handled correctly."
+                    ),
+                );
+                break; // One error per callee is enough; continue checking other callees.
+            }
+        }
+    }
+}

tests/expected/function-contract/mutual_recursion_unsound.expected

@@ -0,0 +1,2 @@
+error: `#[kani::recursion]` is used on `mutual_a`, which calls `mutual_b` that calls back to `mutual_a`. Mutual recursion is not supported by contract verification and produces unsound results.
+error: `#[kani::recursion]` is used on `mutual_b`, which calls `mutual_a` that calls back to `mutual_b`. Mutual recursion is not supported by contract verification and produces unsound results.

tests/expected/function-contract/mutual_recursion_unsound.rs

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Test that Kani detects mutual recursion in functions with contracts and
+//! emits an error about unsoundness.
+
+#[kani::requires(x < 100)]
+#[kani::ensures(|&result| result <= x)]
+#[kani::recursion]
+fn mutual_a(x: u32) -> u32 {
+    if x == 0 { 0 } else { mutual_b(x - 1) }
+}
+
+#[kani::requires(x < 100)]
+#[kani::ensures(|&result| result <= x)]
+#[kani::recursion]
+fn mutual_b(x: u32) -> u32 {
+    if x == 0 { 0 } else { mutual_a(x - 1) }
+}
+
+#[kani::proof_for_contract(mutual_a)]
+fn check_mutual_a() {
+    let x: u32 = kani::any();
+    mutual_a(x);
+}
+
+#[kani::proof_for_contract(mutual_b)]
+fn check_mutual_b() {
+    let x: u32 = kani::any();
+    mutual_b(x);
+}