diff --git a/docs/src/reference/experimental/contracts.md b/docs/src/reference/experimental/contracts.md index fd4e8169bc34..92954b680bc5 100644 --- a/docs/src/reference/experimental/contracts.md +++ b/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). diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index d555bbbaf66e..ecf1a774a3ba 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/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, /// Cache KaniRunContract function used to implement contracts. run_contract_fn: Option, + /// Cache `kani::any` used to detect `Arbitrary` cycles in verified stubs. + kani_any: Option, + /// 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, } 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 + /// . + /// + /// A contract replacement havocs its own return value with + /// `kani::any::()` (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:: -> + /// ::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::`. 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::` 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::>() + .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, +) -> Option> { + 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 diff --git a/rfc/src/rfcs/0002-function-stubbing.md b/rfc/src/rfcs/0002-function-stubbing.md index e92e3c06178b..f8590c0bdf12 100644 --- a/rfc/src/rfcs/0002-function-stubbing.md +++ b/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::()`. +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:: + -> ::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. diff --git a/tests/expected/function-contract/stub_verified_arbitrary_cycle.expected b/tests/expected/function-contract/stub_verified_arbitrary_cycle.expected new file mode 100644 index 000000000000..18f9dbece592 --- /dev/null +++ b/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::()`, so this forms an unbounded recursion: +-> ::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 diff --git a/tests/expected/function-contract/stub_verified_arbitrary_cycle.rs b/tests/expected/function-contract/stub_verified_arbitrary_cycle.rs new file mode 100644 index 000000000000..306d04cb4415 --- /dev/null +++ b/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::()`. +//! Here `::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); +} diff --git a/tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.expected b/tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.expected new file mode 100644 index 000000000000..665e4dce5082 --- /dev/null +++ b/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::()`, so this forms an unbounded recursion: +-> ::any +-> stub_verified_arbitrary_cycle_generic::clamp:: +help: derive `Arbitrary` for `Cyclic` instead of implementing it manually, or avoid calling `clamp` from the `Arbitrary` implementation diff --git a/tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.rs b/tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.rs new file mode 100644 index 000000000000..41295f9d660b --- /dev/null +++ b/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::` +//! 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(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); +} diff --git a/tests/kani/FunctionContracts/stub_verified_arbitrary_other_instantiation.rs b/tests/kani/FunctionContracts/stub_verified_arbitrary_other_instantiation.rs new file mode 100644 index 000000000000..4515d147fbf9 --- /dev/null +++ b/tests/kani/FunctionContracts/stub_verified_arbitrary_other_instantiation.rs @@ -0,0 +1,77 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z function-contracts -Z stubbing +// +//! Test that the `stub_verified` / `Arbitrary` cycle check does not fire when the +//! return type's `Arbitrary` implementation calls a *different* monomorphization +//! of the same generic stubbed function. +//! +//! `::any` calls `clamp::`, not the `clamp::` +//! instance under check. `Safe` derives `Arbitrary`, so the chain terminates and +//! there is no recursion. Comparing callees to the target by `DefId` instead of +//! by monomorphized instance would reject this working proof. +//! +//! This is the counterpart to +//! `tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.rs`, +//! where the `Arbitrary` impl does call the same instantiation and Kani errors. +//! +//! 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 } + } +} + +// Calls `clamp::`, a different instantiation than the one being stubbed. +impl kani::Arbitrary for Cyclic { + fn any() -> Self { + let s = clamp(Safe { v: kani::any() }); + Cyclic { v: s.val() } + } +} + +#[kani::ensures(|r: &T| r.val() <= 10)] +fn clamp(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() }); +} + +#[kani::proof] +#[kani::stub_verified(clamp)] +fn check_other_instantiation() { + let c: Cyclic = kani::any(); + assert!(clamp(c).val() <= 10); +} diff --git a/tests/kani/FunctionContracts/stub_verified_safe_arbitrary.rs b/tests/kani/FunctionContracts/stub_verified_safe_arbitrary.rs new file mode 100644 index 000000000000..49fde5f19bbe --- /dev/null +++ b/tests/kani/FunctionContracts/stub_verified_safe_arbitrary.rs @@ -0,0 +1,47 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z function-contracts -Z stubbing +// +//! Demonstrates that stub_verified works correctly when the Arbitrary +//! implementation does NOT call the stubbed function. +//! +//! This is the counterpart to +//! `tests/expected/function-contract/stub_verified_arbitrary_cycle.rs`, which +//! covers the case where the `Arbitrary` impl does reach the stubbed function +//! and Kani reports the resulting cycle. Here the derived `Arbitrary` builds +//! `MyType` field by field, so no cycle exists and verification succeeds. + +const LIMIT: u64 = 1000; + +#[derive(Clone, Copy, kani::Arbitrary)] +struct MyType { + value: u64, +} + +impl MyType { + #[kani::ensures(|result: &Self| result.value <= LIMIT)] + fn normalize(self) -> Self { + if self.value > LIMIT { MyType { value: LIMIT } } else { self } + } + + fn process(self) -> u64 { + self.normalize().value * 2 + } +} + +// Step 1: Verify the contract +#[kani::proof_for_contract(MyType::normalize)] +fn check_normalize_contract() { + MyType { value: kani::any() }.normalize(); +} + +// Step 2: Use stub_verified in a caller — works because +// kani::Arbitrary for MyType (derived) does NOT call normalize +#[kani::proof] +#[kani::stub_verified(MyType::normalize)] +fn check_process_with_stub() { + let t: MyType = kani::any(); + let result = t.process(); + assert!(result <= LIMIT * 2); +}