Implement stub sets for reusable stub groups (#4594)

Add `kani::stub_set!` macro and `#[kani::use_stub_set]` attribute for
defining reusable groups of stubs that can be applied to multiple proof
harnesses without repeating individual `#[kani::stub]` annotations.

Resolves #2096.

## Problem

When multiple proof harnesses need the same set of stubs (e.g., mocking
I/O, randomness, or network calls), users must duplicate
`#[kani::stub(orig, repl)]` annotations on every harness. This is
verbose, error-prone, and makes it hard to maintain consistent stub
configurations across a test suite.

## Solution

### `kani::stub_set!` macro

Defines a named, reusable group of stub pairs:

```rust
kani::stub_set! {
    pub my_io_stubs {
        stub(std::fs::read, mock_read)
        stub(std::fs::write, mock_write)
        use_stub_set(other_stubs)  // compose with other sets
    }
}
```

### `#[kani::use_stub_set]` attribute

Applies a stub set to a harness:

```rust
#[kani::proof]
#[kani::use_stub_set(my_io_stubs)]
fn check_with_mocked_io() { ... }
```

### Features

- **Composition**: Stub sets can include `use_stub_set(other_set)`
entries to compose sets
- **Visibility**: `pub` modifier for cross-module access
- **Combining**: `#[kani::use_stub_set]` works alongside individual
`#[kani::stub]` attributes
- **Per-harness**: Different harnesses can use different stub sets
- **Circular reference detection**: Errors on circular `use_stub_set`
references

### Implementation

- `stub_set!` generates a `const` with a `#[kanitool::stub_set(...)]`
attribute encoding the stub pairs
- `use_stub_set` resolution in `attributes.rs` reads the attribute,
resolves paths relative to the harness module, and expands the pairs
into the harness's stub list
- Path resolution in `resolve.rs` extended to look up `stub_set` consts

## Testing

5 tests covering:
- `stub_set_basic.rs` — basic stub set definition and usage
- `stub_set_composed.rs` — composing stub sets via `use_stub_set`
entries
- `stub_set_module.rs` — cross-module access with `pub` visibility
- `stub_set_per_harness.rs` — different stub sets per harness
- `stub_set_with_individual.rs` — combining stub sets with individual
`#[kani::stub]`

---

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: feliperodri

docs/src/reference/experimental/stubbing.md

@@ -212,6 +212,57 @@ The following trait patterns are supported:
 
 **Known limitation:** Traits with const generic parameters (e.g., `<Type as Buf<16>>::write`) or associated type constraints (e.g., `<Type as Iterator<Item = u32>>::next`) are not currently supported and will produce a resolution error.
 
+### Stub sets
+
+When multiple harnesses share the same set of stubs, you can define a reusable stub set
+with the `kani::stub_set!` macro and apply it with `#[kani::use_stub_set(...)]`:
+
+```rust
+fn mock_read(_path: std::path::PathBuf) -> std::io::Result<Vec<u8>> {
+    Ok(vec![0; 10])
+}
+
+fn mock_write(_path: std::path::PathBuf, _contents: &[u8]) -> std::io::Result<()> {
+    Ok(())
+}
+
+kani::stub_set!(io_stubs,
+    stub(std::fs::read, mock_read),
+    stub(std::fs::write, mock_write),
+);
+
+#[kani::proof]
+#[kani::use_stub_set(io_stubs)]
+fn check_with_io_stubs() {
+    // Both stubs are applied
+}
+```
+
+Stub sets can compose other stub sets using `use_stub_set(...)`:
+
+```rust
+kani::stub_set!(all_stubs,
+    use_stub_set(io_stubs),
+    stub(other::func, my_func),
+);
+```
+
+You can also combine `#[kani::use_stub_set(...)]` with individual `#[kani::stub(...)]`
+attributes on the same harness. Different harnesses can use different stub sets.
+
+To make a stub set accessible from other modules, add a visibility modifier:
+
+```rust
+mod stubs {
+    kani::stub_set!(pub my_set,
+        stub(real_fn, stub_fn),
+    );
+}
+```
+
+**Note:** Paths inside a stub set are resolved relative to the harness that uses it,
+not relative to the module where the stub set is defined.
+
 ### Usage restrictions
 
 Stub annotations (`#[kani::stub]`) are specified per-harness. When a crate contains multiple

kani-compiler/src/kani_middle/attributes.rs

@@ -28,7 +28,7 @@ use syn::parse::Parser;
 use syn::punctuated::Punctuated;
 use syn::{Expr, ExprLit, Lit, PathSegment, TypePath};
 
-use super::resolve::{FnResolution, ResolveError, resolve_fn_path};
+use super::resolve::{FnResolution, ResolveError, resolve_fn_path, resolve_item};
 use tracing::{debug, trace};
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)]
@@ -44,6 +44,10 @@ enum KaniAttributeKind {
     /// A sound [`Self::Stub`] that replaces a function by a stub generated from
     /// its contract.
     StubVerified,
+    /// Apply a named stub set defined with `kani::stub_set!`.
+    UseStubSet,
+    /// Marks a const as a stub set definition (generated by `kani::stub_set!`).
+    StubSet,
     /// A harness, similar to [`Self::Proof`], but for checking a function
     /// contract, e.g. the contract check is substituted for the target function
     /// before the the verification runs.
@@ -94,8 +98,10 @@ impl KaniAttributeKind {
             | KaniAttributeKind::Stub
             | KaniAttributeKind::ProofForContract
             | KaniAttributeKind::StubVerified
+            | KaniAttributeKind::UseStubSet
             | KaniAttributeKind::Unwind => true,
             KaniAttributeKind::Unstable
+            | KaniAttributeKind::StubSet
             | KaniAttributeKind::FnMarker
             | KaniAttributeKind::Recursion
             | KaniAttributeKind::RecursionTracker
@@ -122,7 +128,12 @@ impl KaniAttributeKind {
 
     /// Is this a stubbing attribute that requires the experimental stubbing feature?
     pub fn demands_stubbing_use(self) -> bool {
-        matches!(self, KaniAttributeKind::Stub | KaniAttributeKind::StubVerified)
+        matches!(
+            self,
+            KaniAttributeKind::Stub
+                | KaniAttributeKind::StubVerified
+                | KaniAttributeKind::UseStubSet
+        )
     }
 }
 
@@ -409,6 +420,13 @@ impl<'tcx> KaniAttributes<'tcx> {
                     // Ignored here, because it should be an internal attribute. Actual validation
                     // happens when pragmas are generated.
                 }
+                KaniAttributeKind::UseStubSet => {
+                    // Validated when harness attributes are extracted.
+                }
+                KaniAttributeKind::StubSet => {
+                    // Marker attribute on const items generated by kani::stub_set!.
+                    // No validation needed here.
+                }
             }
         }
         (stub_verified_targets, contract_targets)
@@ -584,6 +602,14 @@ impl<'tcx> KaniAttributes<'tcx> {
                 KaniAttributeKind::FnMarker => {
                     /* no-op */
                 }
+                KaniAttributeKind::UseStubSet => {
+                    harness
+                        .stubs
+                        .extend_from_slice(&self.parse_use_stub_sets(attributes));
+                }
+                KaniAttributeKind::StubSet => {
+                    unreachable!("`StubSet` attribute should only appear on const items generated by `kani::stub_set!`, not on harnesses")
+                }
             };
             harness
         })
@@ -848,6 +874,182 @@ impl<'tcx> KaniAttributes<'tcx> {
         })
         .collect()
     }
+
+    /// Parse `#[kani::use_stub_set(name)]` attributes and resolve the stub sets
+    /// to their constituent stub pairs.
+    fn parse_use_stub_sets(&self, attributes: &[&'tcx Attribute]) -> Vec<Stub> {
+        let current_module =
+            self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id();
+        let mut stubs = Vec::new();
+        for attr in attributes {
+            let paths = match parse_paths(self.tcx, attr) {
+                Ok(p) => p,
+                Err(_) => {
+                    self.tcx.dcx().span_err(
+                        attr.span(),
+                        "attribute `kani::use_stub_set` takes a single path argument",
+                    );
+                    continue;
+                }
+            };
+            if paths.len() != 1 {
+                self.tcx.dcx().span_err(
+                    attr.span(),
+                    format!(
+                        "attribute `kani::use_stub_set` takes exactly one argument; found {}",
+                        paths.len()
+                    ),
+                );
+                continue;
+            }
+            let name_str = paths[0].to_token_stream().to_string();
+            match resolve_item(self.tcx, current_module, &name_str) {
+                Ok(def_id) => {
+                    self.collect_stubs_from_set(
+                        def_id,
+                        attr.span(),
+                        &mut stubs,
+                        &mut HashSet::from([def_id]),
+                        &mut vec![def_id],
+                    );
+                }
+                Err(err) => {
+                    self.tcx.dcx().span_err(
+                        attr.span(),
+                        format!("failed to resolve stub set `{name_str}`: {err}"),
+                    );
+                }
+            }
+        }
+        stubs
+    }
+
+    /// Recursively collect stubs from a stub set definition, following
+    /// `use_stub_set(...)` entries. Uses `visited` for deduplication (diamond
+    /// composition) and `path` for cycle detection.
+    fn collect_stubs_from_set(
+        &self,
+        def_id: DefId,
+        span: Span,
+        stubs: &mut Vec<Stub>,
+        visited: &mut HashSet<DefId>,
+        stack: &mut Vec<DefId>,
+    ) {
+        let current_module =
+            self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id();
+
+        // Find the kanitool::stub_set attribute on this item.
+        let attrs = self.tcx.get_all_attrs(def_id);
+        let stub_set_attr = attrs.iter().find(|a| {
+            if let Attribute::Unparsed(normal) = a {
+                let segments = &normal.path.segments;
+                segments.len() == 2
+                    && segments[0].as_str() == "kanitool"
+                    && segments[1].as_str() == "stub_set"
+            } else {
+                false
+            }
+        });
+
+        let Some(attr) = stub_set_attr else {
+            self.tcx.dcx().span_err(
+                span,
+                format!(
+                    "`{}` is not a stub set (missing `kani::stub_set!` definition)",
+                    self.tcx.def_path_str(def_id)
+                ),
+            );
+            return;
+        };
+
+        // Parse the attribute arguments: stub(a, b), use_stub_set(c), ...
+        let syn_attribute = syn_attr(self.tcx, attr);
+        let parser = Punctuated::<syn::Expr, syn::Token![,]>::parse_terminated;
+        let entries = match syn_attribute.parse_args_with(parser) {
+            Ok(entries) => entries,
+            Err(err) => {
+                self.tcx.dcx().span_err(span, format!("failed to parse stub set: {err}"));
+                return;
+            }
+        };
+
+        for entry in entries {
+            // Each entry is a function call expression: stub(a, b) or use_stub_set(c)
+            if let Expr::Call(call) = &entry {
+                if let Expr::Path(path) = call.func.as_ref() {
+                    let func_name = path.path.segments.last().map(|s| s.ident.to_string());
+                    match func_name.as_deref() {
+                        Some("stub") if call.args.len() == 2 => {
+                            let orig = call.args[0].to_token_stream().to_string();
+                            let repl = call.args[1].to_token_stream().to_string();
+                            stubs.push(Stub { original: orig, replacement: repl });
+                        }
+                        Some("use_stub_set") if call.args.len() == 1 => {
+                            let set_path = call.args[0].to_token_stream().to_string();
+                            match resolve_item(self.tcx, current_module, &set_path) {
+                                Ok(nested_def_id) => {
+                                    if stack.contains(&nested_def_id) {
+                                        // True cycle detected (A→B→A).
+                                        self.tcx.dcx().span_err(
+                                            span,
+                                            format!("circular stub set reference: `{set_path}`"),
+                                        );
+                                    } else if visited.insert(nested_def_id) {
+                                        // Not yet processed — recurse.
+                                        stack.push(nested_def_id);
+                                        self.collect_stubs_from_set(
+                                            nested_def_id,
+                                            span,
+                                            stubs,
+                                            visited,
+                                            stack,
+                                        );
+                                        stack.pop();
+                                    }
+                                    // else: already processed via another path (diamond) — skip.
+                                }
+                                Err(err) => {
+                                    self.tcx.dcx().span_err(
+                                        span,
+                                        format!("failed to resolve stub set `{set_path}`: {err}"),
+                                    );
+                                }
+                            }
+                        }
+                        Some("stub") => {
+                            self.tcx.dcx().span_err(
+                                span,
+                                "stub() in stub set takes exactly 2 arguments: stub(original, replacement)",
+                            );
+                        }
+                        Some("use_stub_set") => {
+                            self.tcx.dcx().span_err(
+                                span,
+                                "use_stub_set() in stub set takes exactly 1 argument",
+                            );
+                        }
+                        _ => {
+                            self.tcx.dcx().span_err(
+                                span,
+                                format!(
+                                    "unknown entry in stub set: `{}`. Expected `stub(...)` or `use_stub_set(...)`",
+                                    entry.to_token_stream()
+                                ),
+                            );
+                        }
+                    }
+                }
+            } else {
+                self.tcx.dcx().span_err(
+                    span,
+                    format!(
+                        "invalid stub set entry: `{}`. Expected `stub(...)` or `use_stub_set(...)`",
+                        entry.to_token_stream()
+                    ),
+                );
+            }
+        }
+    }
 }
 
 /// An efficient check for the existence for a particular [`KaniAttributeKind`].

kani-compiler/src/kani_middle/resolve.rs

@@ -132,6 +132,19 @@ pub fn resolve_fn<'tcx>(
     Ok(rustc_internal::internal(tcx, result.def().def_id()))
 }
 
+/// Resolve a path string to a `DefId` for any item (not just functions).
+pub fn resolve_item<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    current_module: LocalDefId,
+    path_str: &str,
+) -> Result<DefId, ResolveError<'tcx>> {
+    let _span = debug_span!("resolve_item", ?path_str, ?current_module).entered();
+    let path: syn::Path = syn::parse_str(path_str).map_err(|err| ResolveError::InvalidPath {
+        msg: format!("Expected a path, but found `{path_str}`. {err}"),
+    })?;
+    resolve_path(tcx, current_module, &path)
+}
+
 /// Attempts to resolve a simple path (in the form of a string) to a `DefId`.
 /// The current module is provided as an argument in order to resolve relative
 /// paths.

library/kani/src/lib.rs

@@ -88,6 +88,45 @@ macro_rules! implies {
     };
 }
 
+/// Define a reusable set of function stubs that can be applied to multiple proof harnesses.
+///
+/// # Example
+///
+/// ```ignore
+/// kani::stub_set!(my_stubs,
+///     stub(std::fs::read, my_read),
+///     stub(std::fs::write, my_write),
+/// );
+///
+/// #[kani::proof]
+/// #[kani::use_stub_set(my_stubs)]
+/// fn my_harness() { /* ... */ }
+/// ```
+///
+/// Stub sets can also include other stub sets:
+///
+/// ```ignore
+/// kani::stub_set!(all_stubs,
+///     use_stub_set(my_stubs),
+///     stub(other::func, my_func),
+/// );
+/// ```
+#[macro_export]
+macro_rules! stub_set {
+    (pub $name:ident, $($entry:tt)*) => {
+        /// A Kani stub set definition.
+        #[allow(non_upper_case_globals)]
+        #[kanitool::stub_set($($entry)*)]
+        pub const $name: () = ();
+    };
+    ($vis:vis $name:ident, $($entry:tt)*) => {
+        #[doc(hidden)]
+        #[allow(non_upper_case_globals)]
+        #[kanitool::stub_set($($entry)*)]
+        $vis const $name: () = ();
+    };
+}
+
 pub(crate) use kani_macros::unstable_feature as unstable;
 
 pub mod contracts;