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,30 @@ 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!("Could not resolve replacement function {}: {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 +175,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 +276,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));
                 }
@@ -325,38 +381,87 @@ impl<'tcx> KaniAttributes<'tcx> {
                     harness.unwind_value = parse_unwind(self.tcx, attributes[0])
                 }
                 KaniAttributeKind::Proof => harness.proof = true,
-                KaniAttributeKind::ProofForContract => {
-                    harness.proof = true;
-                    let Some(Ok((name, id, span))) = self.interpret_the_for_contract_attribute()
-                    else {
-                        self.tcx.sess.span_err(
-                            self.tcx.def_span(self.item),
-                            format!("Invalid `{}` attribute format", kind.as_ref()),
-                        );
-                        return harness;
-                    };
-                    let Some(Ok(replacement_name)) =
-                        KaniAttributes::for_item(self.tcx, id).checked_with()
-                    else {
-                        self.tcx
-                            .sess
-                            .span_err(span, "Target function for this check has no contract");
-                        return harness;
-                    };
-                    harness.stubs.push(self.stub_for_relative_item(name, replacement_name));
-                }
+                KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness),
+                KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness),
                 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
         })
     }
 
+    fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) {
+        let sess = self.tcx.sess;
+        let (name, id, span) = match self.interpret_the_for_contract_attribute() {
+            None => unreachable!(
+                "impossible, was asked to handle `proof_for_contract` but didn't find such an attribute."
+            ),
+            Some(Err(_)) => return, // This error was already emitted
+            Some(Ok(values)) => values,
+        };
+        let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with()
+        else {
+            sess.struct_span_err(
+                span,
+                format!(
+                    "Failed to check contract: Function `{}` has no contract.",
+                    self.item_name(),
+                ),
+            )
+            .span_note(self.tcx.def_span(id), "Try adding a contract to this function.")
+            .emit();
+            return;
+        };
+        harness.stubs.push(self.stub_for_relative_item(name, replacement_name));
+    }
+
+    fn handle_stub_verified(&self, harness: &mut HarnessAttributes) {
+        let sess = self.tcx.sess;
+        for contract in self.interpret_stub_verified_attribute() {
+            let Ok((name, def_id, span)) = contract else {
+                // This error has already been emitted so we can ignore it now.
+                // Later the session will fail anyway so we can just
+                // optimistically forge on and try to find more errors.
+                continue;
+            };
+            let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with()
+            {
+                None => {
+                    sess.struct_span_err(
+                        span,
+                        format!(
+                            "Failed to generate verified stub: Function `{}` has no contract.",
+                            self.item_name(),
+                        ),
+                    )
+                    .span_note(
+                        self.tcx.def_span(def_id),
+                        format!(
+                            "Try adding a contract to this function or use the unsound `{}` attribute instead.", 
+                            KaniAttributeKind::Stub.as_ref(),
+                        )
+                    )
+                    .emit();
+                    continue;
+                }
+                Some(Ok(replacement_name)) => replacement_name,
+                Some(Err(_)) => continue,
+            };
+            harness.stubs.push(self.stub_for_relative_item(name, replacement_name))
+        }
+    }
+
+    fn item_name(&self) -> Symbol {
+        self.tcx.item_name(self.item)
+    }
+
     /// Check that if this item is tagged with a proof_attribute, it is a valid harness.
     fn check_proof_attribute(&self, proof_attribute: &Attribute) {
         let span = proof_attribute.span;