Add kani::stub attribute (rust-lang#1814)

Author: aaronbembenek-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -375,6 +375,10 @@ impl<'tcx> GotocCtx<'tcx> {
         let mut harness = self.default_kanitool_proof();
         for attr in other_attributes.iter() {
             match attr.0.as_str() {
+                "stub" => self
+                    .tcx
+                    .sess
+                    .span_warn(attr.1.span, "Attribute `kani::stub` is currently ignored by Kani"),
                 "unwind" => self.handle_kanitool_unwind(attr.1, &mut harness),
                 _ => {
                     self.tcx.sess.span_err(

library/kani_macros/src/lib.rs

@@ -118,3 +118,30 @@ pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
     result.extend(item);
     result
 }
+
+#[cfg(not(kani))]
+#[proc_macro_attribute]
+pub fn stub(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    // When the config is not kani, we should leave the function alone
+    item
+}
+
+/// Specify a function/method stub pair to use for proof harness
+///
+/// The attribute `#[kani::stub(original, replacement)]` can only be used alongside `#[kani::proof]`.
+///
+/// # Arguments
+/// * `original` - The function or method to replace, specified as a path.
+/// * `replacement` - The function or method to use as a replacement, specified as a path.
+#[cfg(kani)]
+#[proc_macro_attribute]
+pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let mut result = TokenStream::new();
+
+    // Translate #[kani::stub(original, replacement)] to #[kanitool::stub(original, replacement)]
+    let insert_string = "#[kanitool::stub(".to_owned() + &attr.to_string() + ")]";
+    result.extend(insert_string.parse::<TokenStream>().unwrap());
+
+    result.extend(item);
+    result
+}

tests/ui/stub-attribute/attribute.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Checks that the `kani::stub` attribute is accepted
+
+fn foo() {}
+
+fn bar() {}
+
+#[kani::proof]
+#[kani::stub(foo, bar)]
+fn main() {}

tests/ui/stub-attribute/expected

@@ -0,0 +1 @@
+warning: Attribute `kani::stub` is currently ignored by Kani