diff --git a/docs/src/reference/experimental/stubbing.md b/docs/src/reference/experimental/stubbing.md index 487a1f479de9..d4d0eb53bde4 100644 --- a/docs/src/reference/experimental/stubbing.md +++ b/docs/src/reference/experimental/stubbing.md @@ -106,6 +106,18 @@ VERIFICATION:- SUCCESSFUL Kani shows that the assertion is successful, avoiding any issues that appear if we attempt to verify the code without stubbing. +## Stub visibility in verification output + +When stubs are applied to a harness, Kani prints them before verification begins: + +``` +Checking harness encrypt_then_decrypt_is_identity... + - Stub: rand::random -> mock_random +``` + +This helps you confirm which stubs are active and makes the assumptions introduced by +stubbing visible in the verification output. + ## Stubbing foreign functions Kani supports stubbing foreign functions declared in `extern` blocks. This is useful for @@ -142,15 +154,35 @@ stubs, check whether the lifetime annotations match. ## Limitations -In the following, we describe all the limitations of the stubbing feature. +In the following, we describe the known limitations of the stubbing feature. + +### Feature interactions + +- **Function contracts:** Stubbing works with function contracts. Use `#[kani::stub_verified(fn)]` + to replace a function with its verified contract abstraction. This requires a + `#[kani::proof_for_contract(fn)]` harness to exist. Regular `#[kani::stub]` can also be + combined with `-Z function-contracts` in the same harness. +- **Loop contracts:** Stubbing and loop contracts (`-Z loop-contracts`) can be used together + in the same harness without issues. +- **Concrete playback:** Stubbing is compatible with `--concrete-playback`. When a stubbed + harness fails, Kani can generate a concrete test case that reproduces the failure using + the stub's behavior. + +### Trait method stubbing + +Stubbing trait method implementations (e.g., `::method`) is **not supported**. +Only free functions and inherent methods can be stubbed. Rust's attribute path syntax does not +support the fully-qualified `::method` form, and the resolution algorithm does not +search through trait implementations. + +If you need to stub a trait method, consider stubbing the calling function instead, or using +conditional compilation (`#[cfg(kani)]`) to provide an alternative implementation. ### Usage restrictions The usage of stubbing is limited to the verification of a single harness. Therefore, users are **required to pass the `--harness` option** when using the stubbing feature. -In addition, this feature **isn't compatible with [concrete playback](./concrete-playback.md)**. - ### Support Support for stubbing is currently **limited to functions and methods**. All other items aren't supported. diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 4d57e90ba052..f9e4932b1c35 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -799,7 +799,8 @@ impl<'tcx> KaniAttributes<'tcx> { if o_bad || r_bad { let mut err = self.tcx.dcx().struct_span_err( attr.span(), - "invalid stub: function does not have a body, but is not an extern function", + "invalid stub: function does not have a body. \ + This typically means a trait method without a default implementation was specified.", ); if o_bad { err = err.with_span_note( diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index fa7b6cdb4fb4..391848395d00 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -97,13 +97,21 @@ impl TransformPass for ExternFnStubPass { /// Search for calls to extern functions that should be stubbed. /// /// We need to find function calls and function pointers. - /// We should replace this with a visitor once rustc_public includes a mutable one. + /// Only allocate a mutable copy of the body if stubs actually apply (#2664). fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "transform"); + // Scan the body for any reference to a stubbed function before allocating + // a mutable copy (COW pattern). This uses the read-only MirVisitor to + // check all operands (calls, function pointers, constants) without + // heap-allocating a MutableBody. + let mut scanner = StubScanner { stubs: &self.stubs, found: false }; + scanner.visit_body(&body); + if !scanner.found { + return (false, body); + } let mut new_body = MutableBody::from(body); - let changed = false; let locals = new_body.locals().to_vec(); - let mut visitor = ExternFnStubVisitor { changed, locals, stubs: &self.stubs }; + let mut visitor = ExternFnStubVisitor { changed: false, locals, stubs: &self.stubs }; visitor.visit_body(&mut new_body); (visitor.changed, new_body.into()) } @@ -162,15 +170,11 @@ impl MirVisitor for FnStubValidator<'_, '_> { self.tcx.dcx().span_err( rustc_internal::internal(self.tcx, loc.span()), format!( - "`{}` doesn't implement \ - `{}`. The function `{}` \ - cannot be stubbed by `{}` due to \ - generic bounds not being met. Callee: {}", - receiver_ty, - trait_, + "type `{receiver_ty}` doesn't implement trait `{trait_}`, \ + so `{}` cannot be stubbed by `{}`. \ + All trait bounds of the stub must be satisfied by the original's call sites.", self.stub.0.name(), self.stub.1.name(), - callee, ), ); } @@ -217,3 +221,23 @@ impl MutMirVisitor for ExternFnStubVisitor<'_> { } } } + +/// Read-only visitor that checks if a body contains any reference to a stubbed +/// function. Used as a fast pre-scan to avoid allocating a MutableBody when no +/// stubs apply (COW pattern for #2664). +struct StubScanner<'a> { + stubs: &'a Stubs, + found: bool, +} + +impl MirVisitor for StubScanner<'_> { + fn visit_operand(&mut self, op: &Operand, _loc: Location) { + if !self.found + && let Operand::Constant(c) = op + && let TyKind::RigidTy(RigidTy::FnDef(def, _)) = c.const_.ty().kind() + && self.stubs.contains_key(&def) + { + self.found = true; + } + } +} diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 708a4064cd72..1823bd6b19b2 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -202,6 +202,26 @@ impl KaniSession { } println!("{msg}"); + + // Print stubs applied to this harness so users know which + // assumptions are in effect (#2119). + let multi = rayon::current_num_threads() > 1; + for stub in &harness.attributes.stubs { + let line = format!(" - Stub: {} -> {}", stub.original, stub.replacement); + if multi { + println!("Thread {thread_index}: {line}"); + } else { + println!("{line}"); + } + } + for verified in &harness.attributes.verified_stubs { + let line = format!(" - Verified stub: {verified}"); + if multi { + println!("Thread {thread_index}: {line}"); + } else { + println!("{line}"); + } + } } let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; diff --git a/tests/cargo-kani/stubbing-foreign-method/main.expected b/tests/cargo-kani/stubbing-foreign-method/expected similarity index 100% rename from tests/cargo-kani/stubbing-foreign-method/main.expected rename to tests/cargo-kani/stubbing-foreign-method/expected diff --git a/tests/cargo-kani/stubbing-foreign-method/src/main.rs b/tests/cargo-kani/stubbing-foreign-method/src/main.rs index ee3b8163dd4c..2a601a1ad124 100644 --- a/tests/cargo-kani/stubbing-foreign-method/src/main.rs +++ b/tests/cargo-kani/stubbing-foreign-method/src/main.rs @@ -5,14 +5,22 @@ use other_crate; -// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that. -// #[kani::proof] #[kani::stub(other_crate::PubType::pub_fn, other_crate::PubType::the_answer)] -#[kani::stub(other_crate::PubType::priv_fn, other_crate::PubType::the_answer)] -#[kani::stub(other_crate::PrivType::priv_fn, other_crate::PrivType::the_answer)] -fn main() { +fn check_pub_method_stub() { assert_eq!(other_crate::PubType::new().pub_fn(), 42); +} + +#[kani::proof] +#[kani::stub(other_crate::PubType::priv_fn, other_crate::PubType::the_answer)] +fn check_priv_method_stub() { assert_eq!(other_crate::PubType::new().fn_delegating_to_priv_fn(), 42); +} + +#[kani::proof] +#[kani::stub(other_crate::PrivType::priv_fn, other_crate::PrivType::the_answer)] +fn check_priv_type_method_stub() { assert_eq!(other_crate::PubType::new().fn_delegating_to_priv_type(), 42); } + +fn main() {} diff --git a/tests/cargo-kani/stubbing-private-foreign-function/main.expected b/tests/cargo-kani/stubbing-private-foreign-function/expected similarity index 100% rename from tests/cargo-kani/stubbing-private-foreign-function/main.expected rename to tests/cargo-kani/stubbing-private-foreign-function/expected diff --git a/tests/cargo-kani/stubbing-private-foreign-function/src/main.rs b/tests/cargo-kani/stubbing-private-foreign-function/src/main.rs index 0df0066fd755..92aa5b1233b2 100644 --- a/tests/cargo-kani/stubbing-private-foreign-function/src/main.rs +++ b/tests/cargo-kani/stubbing-private-foreign-function/src/main.rs @@ -5,12 +5,16 @@ use other_crate; -// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that. -// #[kani::proof] #[kani::stub(other_crate::priv_fn, other_crate::the_answer)] -#[kani::stub(other_crate::pub_mod::priv_mod::pub_fn, other_crate::pub_mod::priv_mod::the_answer)] -fn main() { +fn check_priv_fn_stub() { assert_eq!(other_crate::fn_delegating_to_priv_fn(), 42); +} + +#[kani::proof] +#[kani::stub(other_crate::pub_mod::priv_mod::pub_fn, other_crate::pub_mod::priv_mod::the_answer)] +fn check_priv_mod_fn_stub() { assert_eq!(other_crate::pub_mod::fn_delegating_to_priv_fn(), 42); } + +fn main() {} diff --git a/tests/cargo-kani/stubbing-public-foreign-function/main.expected b/tests/cargo-kani/stubbing-public-foreign-function/expected similarity index 100% rename from tests/cargo-kani/stubbing-public-foreign-function/main.expected rename to tests/cargo-kani/stubbing-public-foreign-function/expected diff --git a/tests/cargo-kani/stubbing-public-foreign-function/src/main.rs b/tests/cargo-kani/stubbing-public-foreign-function/src/main.rs index 1630a63da0b6..64f5ea7b4ca9 100644 --- a/tests/cargo-kani/stubbing-public-foreign-function/src/main.rs +++ b/tests/cargo-kani/stubbing-public-foreign-function/src/main.rs @@ -9,12 +9,16 @@ fn the_answer() -> u32 { 42 } -// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that. -// #[kani::proof] #[kani::stub(other_crate::pub_fn, the_answer)] -#[kani::stub(other_crate::pub_mod::pub_fn, the_answer)] -fn main() { +fn check_pub_fn_stub() { assert_eq!(other_crate::pub_fn(), 42); +} + +#[kani::proof] +#[kani::stub(other_crate::pub_mod::pub_fn, the_answer)] +fn check_pub_mod_fn_stub() { assert_eq!(other_crate::pub_mod::pub_fn(), 42); } + +fn main() {} diff --git a/tests/cargo-ui/function-stubbing-trait-mismatch/main.expected b/tests/cargo-ui/function-stubbing-trait-mismatch/main.expected index 8093e4a76a10..d144ed2a51a9 100644 --- a/tests/cargo-ui/function-stubbing-trait-mismatch/main.expected +++ b/tests/cargo-ui/function-stubbing-trait-mismatch/main.expected @@ -1,2 +1,2 @@ -error: `&str` doesn't implement `DoIt`. The function `foo` cannot be stubbed by `bar` due to generic bounds not being met. -error: `&str` doesn't implement `std::cmp::PartialEq`. The function `foo` cannot be stubbed by `bar` due to generic bounds not being met. +type `&str` doesn't implement trait `DoIt`, so `foo` cannot be stubbed by `bar`. All trait bounds of the stub must be satisfied by the original's call sites. +type `&str` doesn't implement trait `std::cmp::PartialEq`, so `foo` cannot be stubbed by `bar`. All trait bounds of the stub must be satisfied by the original's call sites. diff --git a/tests/kani/Stubbing/enum_method.rs b/tests/kani/Stubbing/enum_method.rs index ac1c5351b976..e943aa9d3eb4 100644 --- a/tests/kani/Stubbing/enum_method.rs +++ b/tests/kani/Stubbing/enum_method.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main -Z stubbing +// kani-flags: -Z stubbing // //! This tests stubbing for methods in local enums. @@ -31,12 +31,14 @@ impl LocalType { } } -// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that. -// #[kani::proof] #[kani::stub(LocalType::pub_fn, LocalType::the_answer)] -#[kani::stub(LocalType::priv_fn, LocalType::the_answer)] -fn main() { +fn check_enum_pub_method_stub() { assert_eq!(LocalType::new().pub_fn(), 42); +} + +#[kani::proof] +#[kani::stub(LocalType::priv_fn, LocalType::the_answer)] +fn check_enum_priv_method_via_delegation() { assert_eq!(LocalType::new().fn_delegating_to_priv_fn(), 42); } diff --git a/tests/kani/Stubbing/method_generic_type.rs b/tests/kani/Stubbing/method_generic_type.rs index 804c2c5c7f5e..fdca689145a2 100644 --- a/tests/kani/Stubbing/method_generic_type.rs +++ b/tests/kani/Stubbing/method_generic_type.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main -Z stubbing +// kani-flags: -Z stubbing // //! This tests stubbing for methods of a local type that has generic parameters. @@ -31,12 +31,14 @@ impl LocalType { } } -// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that. -// #[kani::proof] #[kani::stub(LocalType::pub_fn, LocalType::the_answer)] -#[kani::stub(LocalType::priv_fn, LocalType::the_answer)] -fn main() { +fn check_generic_type_pub_method_stub() { assert_eq!(LocalType::::new().pub_fn(), 42); +} + +#[kani::proof] +#[kani::stub(LocalType::priv_fn, LocalType::the_answer)] +fn check_generic_type_priv_method_via_delegation() { assert_eq!(LocalType::::new().fn_delegating_to_priv_fn(), 42); } diff --git a/tests/kani/Stubbing/public_function.rs b/tests/kani/Stubbing/public_function.rs index 8257081241b5..8ac00c165014 100644 --- a/tests/kani/Stubbing/public_function.rs +++ b/tests/kani/Stubbing/public_function.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main -Z stubbing +// kani-flags: -Z stubbing // //! This tests stubbing for public local functions. @@ -23,12 +23,14 @@ mod local_mod { } } -// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that. -// #[kani::proof] #[kani::stub(local_fn, the_answer)] -#[kani::stub(local_mod::pub_fn, the_answer)] -fn main() { +fn check_local_fn_stub() { assert_eq!(local_fn(), 42); +} + +#[kani::proof] +#[kani::stub(local_mod::pub_fn, the_answer)] +fn check_pub_fn_in_module_stub() { assert_eq!(local_mod::pub_fn(), 42); } diff --git a/tests/kani/Stubbing/struct_method.rs b/tests/kani/Stubbing/struct_method.rs index 0270941ef705..d8ed93c6e2e4 100644 --- a/tests/kani/Stubbing/struct_method.rs +++ b/tests/kani/Stubbing/struct_method.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main -Z stubbing +// kani-flags: -Z stubbing // //! This tests stubbing for methods in local structs. @@ -29,12 +29,14 @@ impl LocalType { } } -// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that. -// #[kani::proof] #[kani::stub(LocalType::pub_fn, LocalType::the_answer)] -#[kani::stub(LocalType::priv_fn, LocalType::the_answer)] -fn main() { +fn check_pub_method_stub() { assert_eq!(LocalType::new().pub_fn(), 42); +} + +#[kani::proof] +#[kani::stub(LocalType::priv_fn, LocalType::the_answer)] +fn check_priv_method_via_delegation() { assert_eq!(LocalType::new().fn_delegating_to_priv_fn(), 42); } diff --git a/tests/ui/function-stubbing-error/resolution_errors.expected b/tests/ui/function-stubbing-error/resolution_errors.expected index 3d317e44c3e1..aa313a74d445 100644 --- a/tests/ui/function-stubbing-error/resolution_errors.expected +++ b/tests/ui/function-stubbing-error/resolution_errors.expected @@ -34,7 +34,7 @@ resolution_errors.rs | #[kani::stub(::bar, stub_foo)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -error: invalid stub: function does not have a body, but is not an extern function\ +error: invalid stub: function does not have a body. This typically means a trait method without a default implementation was specified.\ resolution_errors.rs\ |\ | #[kani::stub(::bar, B::bar)]\ diff --git a/tests/ui/stubbing/stubbing-trait-validation/expected b/tests/ui/stubbing/stubbing-trait-validation/expected index 9b0bbd8464a0..68df05ba43b7 100644 --- a/tests/ui/stubbing/stubbing-trait-validation/expected +++ b/tests/ui/stubbing/stubbing-trait-validation/expected @@ -1,3 +1,3 @@ -error: `&str` doesn't implement `DoIt`. The function `foo` cannot be stubbed by `bar` due to generic bounds not being met. -error: `&str` doesn't implement `std::cmp::PartialEq`. The function `foo` cannot be stubbed by `bar` due to generic bounds not being met. -error: aborting due to 2 previous errors \ No newline at end of file +error: type `&str` doesn't implement trait `DoIt`, so `foo` cannot be stubbed by `bar`. All trait bounds of the stub must be satisfied by the original's call sites. +error: type `&str` doesn't implement trait `std::cmp::PartialEq`, so `foo` cannot be stubbed by `bar`. All trait bounds of the stub must be satisfied by the original's call sites. +error: aborting due to 2 previous errors