Towards stubbing stabilization

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., `<MyType as MyTrait>::method`) is **not supported**.
+Only free functions and inherent methods can be stubbed. Rust's attribute path syntax does not
+support the fully-qualified `<Type as Trait>::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.

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(

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;
+        }
+    }
+}

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")?;

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.
-// <https://github.com/model-checking/kani/issues/1861>
 #[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() {}

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.
-// <https://github.com/model-checking/kani/issues/1861>
 #[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() {}

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.
-// <https://github.com/model-checking/kani/issues/1861>
 #[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() {}

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.

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.
-// <https://github.com/model-checking/kani/issues/1861>
 #[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);
 }

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<T> LocalType<T> {
     }
 }
 
-// TODO: Split up these assertions into separate harnesses, once stubbing is able to support that.
-// <https://github.com/model-checking/kani/issues/1861>
 #[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::<i32>::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::<String>::new().fn_delegating_to_priv_fn(), 42);
 }

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.
-// <https://github.com/model-checking/kani/issues/1861>
 #[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);
 }

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.
-// <https://github.com/model-checking/kani/issues/1861>
 #[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);
 }

tests/ui/function-stubbing-error/resolution_errors.expected

@@ -34,7 +34,7 @@ resolution_errors.rs
 | #[kani::stub(<Bar as Foo>::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(<X as A>::bar, B::bar)]\

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
+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