Simple Stubbing with Contracts

kani-compiler/src/kani_middle/attributes.rs

@@ -19,7 +19,7 @@ use strum_macros::{AsRefStr, EnumString};
 
 use tracing::{debug, trace};
 
-use super::resolve::{self, resolve_fn};
+use super::resolve::{self, resolve_fn, ResolveError};
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)]
 #[strum(serialize_all = "snake_case")]
@@ -31,13 +31,20 @@ enum KaniAttributeKind {
     /// Attribute used to mark unstable APIs.
     Unstable,
     Unwind,
+    /// A sound [`Self::Stub`] that replaces a function by a stub generated from
+    /// its contract.
+    StubVerified,
     /// 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.
     ProofForContract,
     /// Attribute on a function with a contract that identifies the code
     /// implementing the check for this contract.
     CheckedWith,
+    /// Internal attribute of the contracts implementation that identifies the
+    /// name of the function which was generated as the sound stub from the
+    /// contract of this function.
+    ReplacedWith,
     /// Attribute on a function that was auto-generated from expanding a
     /// function contract.
     IsContractGenerated,
@@ -52,8 +59,10 @@ impl KaniAttributeKind {
             | KaniAttributeKind::Solver
             | KaniAttributeKind::Stub
             | KaniAttributeKind::ProofForContract
+            | KaniAttributeKind::StubVerified
             | KaniAttributeKind::Unwind => true,
             KaniAttributeKind::Unstable
+            | KaniAttributeKind::ReplacedWith
             | KaniAttributeKind::CheckedWith
             | KaniAttributeKind::IsContractGenerated => false,
         }
@@ -134,6 +143,33 @@ impl<'tcx> KaniAttributes<'tcx> {
         }
     }
 
+    /// Parse, extract and resolve the target of `stub_verified(TARGET)`. The
+    /// returned `Symbol` and `DefId` are respectively the name and id of
+    /// `TARGET`. The `Span` is that of the contents of the attribute and used
+    /// for error reporting.
+    fn interpret_stub_verified_attribute(
+        &self,
+    ) -> Vec<Result<(Symbol, DefId, Span), ErrorGuaranteed>> {
+        self.map
+            .get(&KaniAttributeKind::StubVerified)
+            .map_or([].as_slice(), Vec::as_slice)
+            .iter()
+            .map(|attr| {
+                let name = expect_key_string_value(self.tcx.sess, attr)?;
+                let ok = self.resolve_sibling(name.as_str()).map_err(|e| {
+                    self.tcx.sess.span_err(
+                        attr.span,
+                        format!(
+                            "Sould not resolve replacement function {} because {e}",
+                            name.as_str()
+                        ),
+                    )
+                })?;
+                Ok((name, ok, attr.span))
+            })
+            .collect()
+    }
+
     /// Parse and extract the `proof_for_contract(TARGET)` attribute. The
     /// returned symbol and DefId are respectively the name and id of `TARGET`,
     /// the span in the span for the attribute (contents).
@@ -142,30 +178,50 @@ impl<'tcx> KaniAttributes<'tcx> {
     ) -> Option<Result<(Symbol, DefId, Span), ErrorGuaranteed>> {
         self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| {
             let name = expect_key_string_value(self.tcx.sess, target)?;
-            let resolved = resolve_fn(
-                self.tcx,
-                self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(),
-                name.as_str(),
-            );
-            resolved.map(|ok| (name, ok, target.span)).map_err(|resolve_err| {
-                self.tcx.sess.span_err(
-                    target.span,
-                    format!(
-                        "Failed to resolve replacement function {} because {resolve_err}",
-                        name.as_str()
-                    ),
-                )
-            })
+            self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err(
+                |resolve_err| {
+                    self.tcx.sess.span_err(
+                        target.span,
+                        format!(
+                            "Failed to resolve checking function {} because {resolve_err}",
+                            name.as_str()
+                        ),
+                    )
+                },
+            )
         })
     }
 
-    /// Extract the name of the sibling function this contract is checked with
-    /// (if any).
+    /// Extract the name of the sibling function this function's contract is
+    /// checked with (if any).
+    ///
+    /// `None` indicates this function does not use a contract, `Some(Err(_))`
+    /// indicates a contract does exist but an error occurred during resolution.
     pub fn checked_with(&self) -> Option<Result<Symbol, ErrorGuaranteed>> {
         self.expect_maybe_one(KaniAttributeKind::CheckedWith)
             .map(|target| expect_key_string_value(self.tcx.sess, target))
     }
 
+    /// Extract the name of the sibling function this function's contract is
+    /// stubbed as (if any).
+    ///
+    /// `None` indicates this function does not use a contract, `Some(Err(_))`
+    /// indicates a contract does exist but an error occurred during resolution.
+    pub fn replaced_with(&self) -> Option<Result<Symbol, ErrorGuaranteed>> {
+        self.expect_maybe_one(KaniAttributeKind::ReplacedWith)
+            .map(|target| expect_key_string_value(self.tcx.sess, target))
+    }
+
+    /// Resolve a function that is known to reside in the same module as the one
+    /// these attributes belong to (`self.item`).
+    fn resolve_sibling(&self, path_str: &str) -> Result<DefId, ResolveError<'tcx>> {
+        resolve_fn(
+            self.tcx,
+            self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(),
+            path_str,
+        )
+    }
+
     /// Check that all attributes assigned to an item is valid.
     /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate
     /// the session and emit all errors found.
@@ -223,7 +279,10 @@ impl<'tcx> KaniAttributes<'tcx> {
                     }
                     expect_single(self.tcx, kind, &attrs);
                 }
-                KaniAttributeKind::CheckedWith => {
+                KaniAttributeKind::StubVerified => {
+                    expect_single(self.tcx, kind, &attrs);
+                }
+                KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => {
                     self.expect_maybe_one(kind)
                         .map(|attr| expect_key_string_value(&self.tcx.sess, attr));
                 }
@@ -345,12 +404,31 @@ impl<'tcx> KaniAttributes<'tcx> {
                     };
                     harness.stubs.push(self.stub_for_relative_item(name, replacement_name));
                 }
+                KaniAttributeKind::StubVerified => {
+                    for contract in self.interpret_stub_verified_attribute() {
+                        let Ok((name, def_id, _span)) = contract else {
+                            continue;
+                        };
+                        let Some(Ok(replacement_name)) =
+                            KaniAttributes::for_item(self.tcx, def_id).replaced_with()
+                        else {
+                            self.tcx.sess.span_err(
+                                self.tcx.def_span(self.item),
+                                format!("Invalid `{}` attribute format", kind.as_ref()),
+                            );
+                            continue;
+                        };
+                        harness.stubs.push(self.stub_for_relative_item(name, replacement_name))
+                    }
+                }
                 KaniAttributeKind::Unstable => {
                     // Internal attribute which shouldn't exist here.
                     unreachable!()
                 }
-                KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => {
-                    todo!("Contract attributes are not supported on proofs")
+                KaniAttributeKind::CheckedWith
+                | KaniAttributeKind::IsContractGenerated
+                | KaniAttributeKind::ReplacedWith => {
+                    self.tcx.sess.span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
                 }
             };
             harness

library/kani_macros/src/lib.rs

@@ -162,6 +162,26 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::proof_for_contract(attr, item)
 }
 
+/// `stub_verified(TARGET)` is a harness attribute (to be used on [`proof`] or
+/// [`proof_for_contract`] function) that replaces all occurrences of `TARGET`
+/// reachable from this harness with a stub generated from the contract on
+/// `TARGET`.
+///
+/// To create a contract for `TARGET` you must decorate it with at least one
+/// [`requires`] or [`ensures`] attribute.
+///
+/// You may use multiple `stub_verified` attributes on a single harness.
+///
+/// For more information see the [function contract
+/// RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html).
+///
+/// This attribute is part of the unstable contracts API and requires
+/// `-Zfunction-contracts` flag to be used.
+#[proc_macro_attribute]
+pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream {
+    attr_impl::stub_verified(attr, item)
+}
+
 /// This module implements Kani attributes in a way that only Kani's compiler can understand.
 /// This code should only be activated when pre-building Kani's sysroot.
 #[cfg(kani_sysroot)]
@@ -170,7 +190,7 @@ mod sysroot {
 
     mod contracts;
 
-    pub use contracts::{ensures, proof_for_contract, requires};
+    pub use contracts::{ensures, proof_for_contract, requires, stub_verified};
 
     use super::*;
 
@@ -344,4 +364,5 @@ mod regular {
     no_op!(requires);
     no_op!(ensures);
     no_op!(proof_for_contract);
+    no_op!(stub_verified);
 }