diff --git a/docs/src/reference/experimental/contracts.md b/docs/src/reference/experimental/contracts.md index fd4e8169bc34..d3f51f7c754a 100644 --- a/docs/src/reference/experimental/contracts.md +++ b/docs/src/reference/experimental/contracts.md @@ -62,5 +62,15 @@ 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:** `stub_verified` replaces calls globally, including inside +> `kani::Arbitrary` implementations. Kani automatically detects when a call +> originates from `kani::any()` (input generation) and uses the original +> function body instead of the contract replacement. This means +> `stub_verified` works correctly even when the type's `Arbitrary` impl calls +> the stubbed function. If you encounter issues, you can work around them by +> deriving `Arbitrary` (which generates field-by-field values without calling +> user functions) or by using standalone proof harnesses instead of +> `stub_verified`. + 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/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 87e01b7971fc..1aa0058583af 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -275,6 +275,7 @@ macro_rules! kani_intrinsics { #[kanitool::fn_marker = "AnyModel"] #[inline(always)] pub fn any() -> T { + let _guard = internal::ArbitraryContextGuard::enter(); T::any() } @@ -284,6 +285,7 @@ macro_rules! kani_intrinsics { /// *Note*: Any proof using a bounded symbolic value is only valid up to that bound. #[inline(always)] pub fn bounded_any() -> T { + let _guard = internal::ArbitraryContextGuard::enter(); T::bounded_any::() } @@ -325,7 +327,7 @@ macro_rules! kani_intrinsics { /// valid values for type `T`. #[inline(always)] pub fn any_where bool>(f: F) -> T { - let result = T::any(); + let result = any(); assume(f(&result)); result } @@ -535,7 +537,7 @@ macro_rules! kani_intrinsics { #[kanitool::fn_marker = "WriteAnySliceModel"] #[inline(always)] pub unsafe fn write_any_slice(slice: *mut [T]) { - (*slice).fill_with(T::any) + (*slice).fill_with(|| super::any::()) } /// Fill in a pointer with kani::any. @@ -543,7 +545,7 @@ macro_rules! kani_intrinsics { #[kanitool::fn_marker = "WriteAnySlimModel"] #[inline(always)] pub unsafe fn write_any_slim(pointer: *mut T) { - ptr::write(pointer, T::any()) + ptr::write(pointer, super::any::()) } /// Fill in a str with kani::any. @@ -601,6 +603,71 @@ macro_rules! kani_intrinsics { /// Insert the contract into the body of the function as assertion(s). pub const ASSERT: Mode = 4; + /// Nesting depth counter for `Arbitrary::any()` calls — see + /// `docs/dev/stub-verified-arbitrary.md` for design rationale. + /// Not public — only accessible via `in_arbitrary_context()` and + /// `ArbitraryContextGuard`. + /// + /// This static is guaranteed to be a single instance per compilation + /// unit: both `kani_lib!(kani)` and `kani_lib!(core)` expand + /// `kani_intrinsics!()` exactly once, producing one `kani::internal` + /// module with one copy of this static. + static mut ARBITRARY_NESTING_DEPTH: u32 = 0; + + /// Increment the arbitrary nesting depth counter. + /// Note: `debug_assert!` guards are active in concrete playback + /// but compiled away during symbolic execution (release-like MIR). + #[inline(always)] + fn enter_arbitrary_context() { + unsafe { + debug_assert!( + ARBITRARY_NESTING_DEPTH < u32::MAX, + "ArbitraryContextGuard: nesting depth overflow" + ); + ARBITRARY_NESTING_DEPTH = ARBITRARY_NESTING_DEPTH.wrapping_add(1); + } + } + + /// Decrement the arbitrary nesting depth counter. + #[inline(always)] + fn exit_arbitrary_context() { + unsafe { + debug_assert!( + ARBITRARY_NESTING_DEPTH > 0, + "ArbitraryContextGuard: mismatched exit (underflow)" + ); + ARBITRARY_NESTING_DEPTH = ARBITRARY_NESTING_DEPTH.wrapping_sub(1); + } + } + + /// Returns true if we are inside a `kani::any()` call (i.e., during + /// `Arbitrary` input generation). Used by the contract `REPLACE` arm + /// to fall back to the original function body. + #[inline(always)] + pub fn in_arbitrary_context() -> bool { + unsafe { ARBITRARY_NESTING_DEPTH > 0 } + } + + /// RAII guard that increments the arbitrary nesting depth on creation + /// and decrements it on drop. Ensures the counter is correctly + /// maintained even if `T::any()` panics (concrete playback mode). + pub struct ArbitraryContextGuard; + + impl ArbitraryContextGuard { + #[inline(always)] + pub fn enter() -> Self { + enter_arbitrary_context(); + ArbitraryContextGuard + } + } + + impl Drop for ArbitraryContextGuard { + #[inline(always)] + fn drop(&mut self) { + exit_arbitrary_context(); + } + } + /// Creates a non-fatal property with the specified condition and message. /// /// This check will not impact the program control flow even when it fails. diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index ed8bde7f8974..43b644ea1655 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -83,6 +83,17 @@ impl<'a> ContractConditionsHandler<'a> { kani_register_contract(#recursion_ident) } kani::internal::REPLACE => { + // When called from within kani::any() (Arbitrary input + // generation), use the original body to avoid infinite + // recursion from stub_verified replacing calls inside + // Arbitrary impls. This early return avoids the replace + // closure capturing function parameters by move. + if kani::internal::in_arbitrary_context() { + return #block + } + // The replace closure must remain at the top level of this + // arm so that subsequent contract attributes can find it via + // expect_closure_in_match. #replace_closure; kani_register_contract(#replace_ident) } diff --git a/rfc/src/rfcs/0002-function-stubbing.md b/rfc/src/rfcs/0002-function-stubbing.md index e92e3c06178b..40922fc6d339 100644 --- a/rfc/src/rfcs/0002-function-stubbing.md +++ b/rfc/src/rfcs/0002-function-stubbing.md @@ -367,6 +367,28 @@ 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 + +When a type's `kani::Arbitrary` implementation calls a function targeted by +`#[kani::stub_verified]`, the global contract replacement would normally apply +inside `Arbitrary::any()` too, causing infinite recursion during test input +generation. + +To prevent this, `kani::any()` tracks nesting depth via an internal counter +(`ARBITRARY_NESTING_DEPTH`) managed by an RAII guard. The contract `REPLACE` +match arm checks this counter — when inside an Arbitrary context (depth > 0), +it executes the original function body instead of the contract replacement. + +This is sound because the real function produces a subset of valid outputs +compared to the contract abstraction (which havocs all outputs). Using the real +function during Arbitrary input generation gives tighter (more precise) inputs, +not less sound verification. + +The counter (not a boolean) correctly handles nested `kani::any()` calls, e.g., +when `Arbitrary` for a struct calls `kani::any()` for each field. All entry +points (`any()`, `bounded_any()`, `any_where()`, `write_any_slim()`, +`write_any_slice()`) route through the guard. + ## Future possibilities - It would increase the utility of stubbing if we supported stubs for types. diff --git a/tests/kani/FunctionContracts/stub_verified_arbitrary_fix.rs b/tests/kani/FunctionContracts/stub_verified_arbitrary_fix.rs new file mode 100644 index 000000000000..1dc4140be31e --- /dev/null +++ b/tests/kani/FunctionContracts/stub_verified_arbitrary_fix.rs @@ -0,0 +1,49 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z function-contracts -Z stubbing +// +//! Regression test: stub_verified no longer causes infinite recursion when +//! the type's Arbitrary implementation calls the stubbed function. +//! See: docs/dev/stub-verified-arbitrary.md + +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() + } +} + +// Arbitrary calls new() which calls normalize() — the stubbed function +impl kani::Arbitrary for Wrapper { + fn any() -> Self { + Wrapper::new(kani::any()) + } +} + +#[kani::proof_for_contract(Wrapper::normalize)] +fn check_contract() { + Wrapper { value: kani::any() }.normalize(); +} + +// This previously caused infinite recursion because stub_verified replaced +// normalize globally, including inside Arbitrary::any(). +// The fix: kani::any() sets ARBITRARY_NESTING_DEPTH, and the contract +// REPLACE arm falls back to the original body when the depth is > 0. +#[kani::proof] +#[kani::stub_verified(Wrapper::normalize)] +fn check_caller_with_stub() { + let w: Wrapper = kani::any(); + assert!(w.normalize().value <= LIMIT); +} diff --git a/tests/kani/FunctionContracts/stub_verified_arbitrary_workaround.rs b/tests/kani/FunctionContracts/stub_verified_arbitrary_workaround.rs new file mode 100644 index 000000000000..4287975f681c --- /dev/null +++ b/tests/kani/FunctionContracts/stub_verified_arbitrary_workaround.rs @@ -0,0 +1,61 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z function-contracts -Z stubbing +// +//! Demonstrates that stub_verified works correctly even when the Arbitrary +//! implementation calls the stubbed function, using the standalone proof +//! pattern as an alternative approach. + +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 + } +} + +// Arbitrary calls new() which calls normalize() +impl kani::Arbitrary for Wrapper { + fn any() -> Self { + Wrapper::new(kani::any()) + } +} + +// Step 1: Verify the contract +#[kani::proof_for_contract(Wrapper::normalize)] +fn check_normalize_contract() { + Wrapper { value: kani::any() }.normalize(); +} + +// Step 2: Use stub_verified — works even though Arbitrary calls normalize, +// thanks to the ARBITRARY_NESTING_DEPTH mechanism. +#[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); +} + +// Alternative: standalone proof without stub_verified +#[kani::proof] +fn check_process_standalone() { + let w: Wrapper = kani::any(); + let result = w.process(); + assert!(result <= LIMIT * 2); +} 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..26d24d6b7386 --- /dev/null +++ b/tests/kani/FunctionContracts/stub_verified_safe_arbitrary.rs @@ -0,0 +1,41 @@ +// 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. + +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); +}