Detect stub_verified/Arbitrary recursion at compile time

docs/src/reference/experimental/contracts.md

@@ -62,5 +62,13 @@ fn check_foo() {
 ```
 By leveraging the stubbing feature, we can replace the (expensive) `gcd` call with a *verified abstraction* of its behavior, greatly reducing verification time for `foo`.
 
+> **Note:** A verified stub havocs its return value with `kani::any()`. If the
+> `kani::Arbitrary` implementation for that return type calls the stubbed
+> function, the stub re-enters itself and the recursion never terminates. Kani
+> reports this as a compile-time error naming the call path. To fix it, derive
+> `Arbitrary` (which generates field-by-field values without calling user
+> functions), or avoid calling the stubbed function from the `Arbitrary`
+> implementation.
+
 There is far more to learn about contracts.
 We highly recommend reading our [blog post about contracts](https://model-checking.github.io/kani-verifier-blog/2024/01/29/function-contracts.html) (from which this `gcd` example is taken). We also recommend looking at the `contracts` module in our [documentation](../../crates/index.md).

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

@@ -16,7 +16,9 @@ use rustc_public::mir::{
     Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents,
 };
 use rustc_public::rustc_internal;
-use rustc_public::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, TypeAndMut, UintTy};
+use rustc_public::ty::{
+    ClosureDef, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, TyKind, TypeAndMut, UintTy,
+};
 use rustc_span::Symbol;
 use std::collections::HashSet;
 use std::fmt::Debug;
@@ -279,6 +281,12 @@ pub struct FunctionWithContractPass {
     unused_closures: HashSet<ClosureDef>,
     /// Cache KaniRunContract function used to implement contracts.
     run_contract_fn: Option<FnDef>,
+    /// Cache `kani::any` used to detect `Arbitrary` cycles in verified stubs.
+    kani_any: Option<FnDef>,
+    /// Instances we already ran the `Arbitrary` cycle check on, so we only report
+    /// once each. Keyed by monomorphized instance so that distinct
+    /// instantiations of a generic target are each checked.
+    arbitrary_cycle_checked: HashSet<Instance>,
 }
 
 impl TransformPass for FunctionWithContractPass {
@@ -305,6 +313,15 @@ impl TransformPass for FunctionWithContractPass {
                     if mode == ContractMode::RecursiveCheck {
                         check_mutual_recursion(tcx, *def, &body);
                     }
+                    // Key the dedup on the monomorphized instance, not the
+                    // `FnDef`: a generic `stub_verified` target can be
+                    // instantiated at several types, and each instantiation has
+                    // its own return type and so its own potential cycle.
+                    if mode == ContractMode::Replace
+                        && self.arbitrary_cycle_checked.insert(instance)
+                    {
+                        self.check_arbitrary_cycle(tcx, *def, args);
+                    }
                     self.mark_unused(tcx, *def, &body, mode);
                     let new_body = self.set_mode(tcx, body, mode);
                     (true, new_body)
@@ -371,6 +388,8 @@ impl FunctionWithContractPass {
                 assert_contracts: !queries.args().no_assert_contracts,
                 unused_closures: Default::default(),
                 run_contract_fn,
+                kani_any: queries.kani_functions().get(&KaniModel::Any.into()).copied(),
+                arbitrary_cycle_checked: Default::default(),
             }
         } else {
             // If reachability mode is PubFns or Tests, we just remove any contract logic.
@@ -479,6 +498,77 @@ impl FunctionWithContractPass {
         })
     }
 
+    /// Detect the `stub_verified` / `Arbitrary` cycle described in
+    /// <https://github.com/model-checking/kani/pull/4571>.
+    ///
+    /// A contract replacement havocs its own return value with
+    /// `kani::any::<Ret>()` (see `initial_replace_stmts` in `kani_macros`, where
+    /// `any_modifies` is emitted and later rewritten to `kani::any` by
+    /// [`AnyModifiesPass`]). So if `Ret`'s `Arbitrary` implementation reaches the
+    /// stubbed function again, the replacement calls itself through
+    /// `Arbitrary::any`:
+    ///
+    /// ```text
+    /// normalize -> replace closure -> kani::any::<Wrapper> ->
+    ///     <Wrapper as Arbitrary>::any -> Wrapper::new -> normalize -> ...
+    /// ```
+    ///
+    /// This recursion is unbounded and has no fixpoint, so CBMC unwinds until it
+    /// exhausts memory. Report it at compile time instead, since the alternative
+    /// is a silent multi-minute hang followed by an out-of-memory message that
+    /// does not name the cause.
+    fn check_arbitrary_cycle(&self, tcx: TyCtxt, fn_def: FnDef, args: &GenericArgs) {
+        let Some(kani_any) = self.kani_any else { return };
+        let Ok(instance) = Instance::resolve(fn_def, args) else { return };
+        // Bail rather than ICE if the ABI is not computable; this check is
+        // diagnostic-only, so failing to run it just leaves prior behavior.
+        let Ok(fn_abi) = instance.fn_abi() else { return };
+        let ret_ty = fn_abi.ret.ty;
+
+        // Resolve `kani::any::<Ret>`. This fails when `Ret` does not implement
+        // `Arbitrary`, which `AnyModifiesPass::any_body` already diagnoses.
+        let any_args = GenericArgs(vec![GenericArgKind::Type(ret_ty)]);
+        let Ok(any_instance) = Instance::resolve(kani_any, &any_args) else { return };
+
+        let Some(path) = find_call_path(&any_instance, &instance, &mut HashSet::new()) else {
+            return;
+        };
+
+        let fn_name = tcx.def_path_str(rustc_internal::internal(tcx, fn_def.def_id()));
+        let span = rustc_internal::internal(tcx, fn_def.span());
+        // Render one uniform `-> callee` entry per line, ending at the stubbed
+        // function itself. The leading `kani::any::<Ret>` frame is dropped: the
+        // note above already names it, and starting at the `Arbitrary::any` call
+        // is where the recursion actually begins. Instance names are used
+        // throughout so the trace is consistently crate-qualified.
+        let trace = path
+            .iter()
+            .skip(1)
+            .chain(std::iter::once(&instance.name()))
+            .map(|frame| format!("    -> {frame}"))
+            .collect::<Vec<_>>()
+            .join("\n");
+        tcx.dcx()
+            .struct_span_err(
+                span,
+                format!(
+                    "`{fn_name}` is used as a verified stub, but generating an \
+                     arbitrary value of its return type `{ret_ty}` calls \
+                     `{fn_name}` again"
+                ),
+            )
+            .with_note(format!(
+                "the contract replacement havocs its return value with \
+                 `kani::any::<{ret_ty}>()`, so this forms an unbounded recursion:\n\
+                 {trace}"
+            ))
+            .with_help(format!(
+                "derive `Arbitrary` for `{ret_ty}` instead of implementing it manually, \
+                 or avoid calling `{fn_name}` from the `Arbitrary` implementation"
+            ))
+            .emit();
+    }
+
     /// Select any unused closure for body deletion.
     fn mark_unused(&mut self, tcx: TyCtxt, fn_def: FnDef, body: &Body, mode: ContractMode) {
         let contract =
@@ -556,6 +646,54 @@ fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureD
         })
 }
 
+/// Search the call graph rooted at `from` for a path reaching `target`.
+///
+/// Returns the chain of function names leading to `target` (excluding `target`
+/// itself) so the diagnostic can show the user the cycle. `visited` guards
+/// against non-terminating traversal of recursive call graphs.
+///
+/// `target` is a monomorphized instance, and callees are compared against it
+/// instance-precisely rather than by `DefId`. A generic function's `Arbitrary`
+/// implementation may call a *different* monomorphization of that same generic
+/// function; that does not re-enter the replacement instance under check, and
+/// the chain may well terminate. Comparing by `DefId` alone would reject such
+/// working proofs.
+///
+/// This is a syntactic walk over monomorphized MIR, so it only follows statically
+/// resolvable calls. Calls through function pointers or trait objects are not
+/// followed, meaning a cycle routed through them is not detected. That is
+/// acceptable here: missing a detection reproduces today's behavior (the hang),
+/// while a false positive would reject a working proof.
+fn find_call_path(
+    from: &Instance,
+    target: &Instance,
+    visited: &mut HashSet<Instance>,
+) -> Option<Vec<String>> {
+    if !visited.insert(*from) {
+        return None;
+    }
+    let body = from.body()?;
+
+    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;
+        };
+        let Ok(callee) = Instance::resolve(callee_def, &callee_args) else { continue };
+
+        if callee == *target {
+            return Some(vec![from.name()]);
+        }
+
+        if let Some(mut path) = find_call_path(&callee, target, visited) {
+            path.insert(0, from.name());
+            return Some(path);
+        }
+    }
+    None
+}
+
 /// 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

rfc/src/rfcs/0002-function-stubbing.md

@@ -367,6 +367,29 @@ One possibility would be writing proofs about stubs (possibly relating their beh
 - Our proposed approach will not work with `--concrete-playback` (for now).
 - We are only able to apply abstractions to some dependencies if the user enables the MIR linker.
 
+### `stub_verified` and `Arbitrary` interaction (known limitation)
+
+A contract replacement havocs its own return value with `kani::any::<Ret>()`.
+So if the `kani::Arbitrary` implementation for `Ret` reaches the stubbed
+function, the replacement re-enters itself through `Arbitrary::any`:
+
+```text
+normalize -> replace closure -> kani::any::<Wrapper>
+          -> <Wrapper as Arbitrary>::any -> Wrapper::new -> normalize -> ...
+```
+
+This recursion has no fixpoint, so CBMC unwinds it until it exhausts memory.
+Kani detects the cycle at compile time and reports an error naming the call
+path, rather than letting verification hang.
+
+**Workarounds:**
+- Derive `Arbitrary` instead of implementing it manually (`#[derive(kani::Arbitrary)]`
+  generates field-by-field values without calling user functions).
+- Avoid calling the stubbed function from the `Arbitrary` implementation.
+
+Note that the detection walks statically resolvable calls only, so a cycle
+routed through a function pointer or trait object is not reported.
+
 ## Future possibilities
 
 - It would increase the utility of stubbing if we supported stubs for types.

tests/expected/function-contract/stub_verified_arbitrary_cycle.expected

@@ -0,0 +1,6 @@
+error: `Wrapper::normalize` is used as a verified stub, but generating an arbitrary value of its return type `Wrapper` calls `Wrapper::normalize` again
+note: the contract replacement havocs its return value with `kani::any::<Wrapper>()`, so this forms an unbounded recursion:
+-> <stub_verified_arbitrary_cycle::Wrapper as kani::Arbitrary>::any
+-> stub_verified_arbitrary_cycle::Wrapper::new
+-> stub_verified_arbitrary_cycle::Wrapper::normalize
+help: derive `Arbitrary` for `Wrapper` instead of implementing it manually, or avoid calling `Wrapper::normalize` from the `Arbitrary` implementation

tests/expected/function-contract/stub_verified_arbitrary_cycle.rs

@@ -0,0 +1,56 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zstubbing
+
+//! Test that Kani detects the cycle between a verified stub and the `Arbitrary`
+//! implementation of its return type, and reports it at compile time.
+//!
+//! A contract replacement havocs its own return value with `kani::any::<Ret>()`.
+//! Here `<Wrapper as Arbitrary>::any` calls `Wrapper::new`, which calls the
+//! stubbed `Wrapper::normalize`, so the replacement re-enters itself through
+//! `Arbitrary::any`. Without this check, CBMC unwinds the recursion until it
+//! exhausts memory.
+//!
+//! See https://github.com/model-checking/kani/pull/4571
+
+const LIMIT: u64 = 1000;
+
+#[derive(Clone, Copy)]
+struct Wrapper {
+    value: u64,
+}
+
+impl Wrapper {
+    #[kani::ensures(|result: &Self| result.value <= LIMIT)]
+    fn normalize(self) -> Self {
+        if self.value > LIMIT { Wrapper { value: LIMIT } } else { self }
+    }
+
+    fn new(v: u64) -> Self {
+        Wrapper { value: v }.normalize()
+    }
+
+    fn process(self) -> u64 {
+        self.normalize().value * 2
+    }
+}
+
+// This `Arbitrary` implementation calls `normalize`, which closes the cycle.
+impl kani::Arbitrary for Wrapper {
+    fn any() -> Self {
+        Wrapper::new(kani::any())
+    }
+}
+
+#[kani::proof_for_contract(Wrapper::normalize)]
+fn check_normalize_contract() {
+    Wrapper { value: kani::any() }.normalize();
+}
+
+#[kani::proof]
+#[kani::stub_verified(Wrapper::normalize)]
+fn check_process_with_stub() {
+    let w: Wrapper = kani::any();
+    let result = w.process();
+    assert!(result <= LIMIT * 2);
+}

tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.expected

@@ -0,0 +1,5 @@
+error: `clamp` is used as a verified stub, but generating an arbitrary value of its return type `Cyclic` calls `clamp` again
+note: the contract replacement havocs its return value with `kani::any::<Cyclic>()`, so this forms an unbounded recursion:
+-> <stub_verified_arbitrary_cycle_generic::Cyclic as kani::Arbitrary>::any
+-> stub_verified_arbitrary_cycle_generic::clamp::<stub_verified_arbitrary_cycle_generic::Cyclic>
+help: derive `Arbitrary` for `Cyclic` instead of implementing it manually, or avoid calling `clamp` from the `Arbitrary` implementation

tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.rs

@@ -0,0 +1,74 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zstubbing
+
+//! Test that the `stub_verified` / `Arbitrary` cycle check inspects every
+//! monomorphization of a generic target, not just the first one.
+//!
+//! `clamp` is instantiated at both `Safe` and `Cyclic`. Only `Cyclic` has an
+//! `Arbitrary` implementation that calls back into `clamp`, and `clamp::<Safe>`
+//! is transformed first. Deduplicating the check per `FnDef` rather than per
+//! monomorphized instance would let the acyclic `Safe` instantiation consume the
+//! only slot, skipping `Cyclic` entirely and reintroducing the hang.
+//!
+//! See https://github.com/model-checking/kani/pull/4571
+
+trait Clampable: Copy {
+    fn val(self) -> u64;
+    fn make(v: u64) -> Self;
+}
+
+#[derive(Clone, Copy, kani::Arbitrary)]
+struct Safe {
+    v: u64,
+}
+
+impl Clampable for Safe {
+    fn val(self) -> u64 {
+        self.v
+    }
+    fn make(v: u64) -> Self {
+        Safe { v }
+    }
+}
+
+#[derive(Clone, Copy)]
+struct Cyclic {
+    v: u64,
+}
+
+impl Clampable for Cyclic {
+    fn val(self) -> u64 {
+        self.v
+    }
+    fn make(v: u64) -> Self {
+        Cyclic { v }
+    }
+}
+
+// This `Arbitrary` implementation routes back into the generic stubbed function.
+impl kani::Arbitrary for Cyclic {
+    fn any() -> Self {
+        clamp(Cyclic { v: kani::any() })
+    }
+}
+
+#[kani::ensures(|r: &T| r.val() <= 10)]
+fn clamp<T: Clampable>(x: T) -> T {
+    if x.val() > 10 { T::make(10) } else { x }
+}
+
+#[kani::proof_for_contract(clamp)]
+fn check_clamp_contract() {
+    clamp(Safe { v: kani::any() });
+}
+
+// The acyclic `Safe` instantiation is used before the cyclic `Cyclic` one.
+#[kani::proof]
+#[kani::stub_verified(clamp)]
+fn check_both_instantiations() {
+    let s: Safe = kani::any();
+    assert!(clamp(s).val() <= 10);
+    let c: Cyclic = kani::any();
+    assert!(clamp(c).val() <= 10);
+}