[Breaking Change] Fail if stub verified doesn't have a contract harness (#4295)

Emit a compilation error if the target of a `stub_verified` attribute
does not have a contract harness. Also require `-Z stubbing` for
stub_verified. Both of these are breaking changes. The former I feel
strongly should go in, since IMO it's a soundness hole. The latter I
could be convinced to revert if we feel like it's unnecessary churn; it
just felt odd to me to have an unstable stub feature that's not behind
the unstable stub flag.

Note that this compilation error is not really sufficient to ensure that
the stub's contract holds, since a user can just pass `--harness` to
skip the contract harness. A better design would be to insert the check
automatically rather than requiring a separate harness. But this is
better than nothing and less invasive to implement, so start with this
for now.

Resolves #4294

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

Author: Carolyn Zech

kani-compiler/src/kani_middle/attributes.rs

@@ -4,6 +4,7 @@
 
 use std::collections::{BTreeMap, HashSet};
 
+use fxhash::FxHashMap;
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
 use rustc_ast::{LitKind, MetaItem, MetaItemKind};
@@ -118,6 +119,11 @@ impl KaniAttributeKind {
     pub fn demands_function_contract_use(self) -> bool {
         matches!(self, KaniAttributeKind::ProofForContract)
     }
+
+    /// Is this a stubbing attribute that requires the experimental stubbing feature?
+    pub fn demands_stubbing_use(self) -> bool {
+        matches!(self, KaniAttributeKind::Stub | KaniAttributeKind::StubVerified)
+    }
 }
 
 /// Bundles together common data used when evaluating the attributes of a given
@@ -300,11 +306,16 @@ impl<'tcx> KaniAttributes<'tcx> {
     }
 
     /// Check that all attributes assigned to an item is valid.
+    /// Returns a tuple of (stub_verified_targets_with_spans, proof_for_contract_targets).
     /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate
     /// the session and emit all errors found.
-    pub(super) fn check_attributes(&self) {
+    pub(super) fn check_attributes(&self) -> (FxHashMap<FnDefStable, Span>, HashSet<FnDefStable>) {
         // Check that all attributes are correctly used and well formed.
         let is_harness = self.is_proof_harness();
+
+        let mut contract_targets = HashSet::default();
+        let mut stub_verified_targets = FxHashMap::default();
+
         for (&kind, attrs) in self.map.iter() {
             let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span(), msg);
 
@@ -363,12 +374,19 @@ impl<'tcx> KaniAttributes<'tcx> {
                     expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| {
                         self.check_proof_attribute(kind, attr);
-                        let _ = self.parse_single_path_attr(attr);
+                        let res = self.parse_single_path_attr(attr);
+                        if let Ok(target) = res {
+                            contract_targets.insert(target.def().to_owned());
+                        }
                     })
                 }
                 KaniAttributeKind::StubVerified => {
                     attrs.iter().for_each(|attr| {
                         self.check_stub_verified(attr);
+                        let res = self.parse_single_path_attr(attr);
+                        if let Ok(target) = res {
+                            stub_verified_targets.insert(target.def().to_owned(), attr.span());
+                        }
                     });
                 }
                 KaniAttributeKind::FnMarker
@@ -393,6 +411,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 }
             }
         }
+        (stub_verified_targets, contract_targets)
     }
 
     /// Get the value of an attribute if one exists.
@@ -433,6 +452,22 @@ impl<'tcx> KaniAttributes<'tcx> {
             }
         }
 
+        // If the `stubbing` unstable feature is not enabled then no
+        // function should use any of those APIs.
+        if !enabled_features.iter().any(|feature| feature == "stubbing") {
+            for kind in self.map.keys().copied().filter(|a| a.demands_stubbing_use()) {
+                let msg = format!(
+                    "Using the {} attribute requires activating the unstable `stubbing` feature",
+                    kind.as_ref()
+                );
+                if let Some(attr) = self.map.get(&kind).unwrap().first() {
+                    self.tcx.dcx().span_err(attr.span(), msg);
+                } else {
+                    self.tcx.dcx().err(msg);
+                }
+            }
+        }
+
         if let Some(unstable_attrs) = self.map.get(&KaniAttributeKind::Unstable) {
             for attr in unstable_attrs {
                 let unstable_attr = UnstableAttribute::try_from(*attr).unwrap();

kani-compiler/src/kani_middle/mod.rs

@@ -41,9 +41,16 @@ pub mod transform;
 /// error was found.
 pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
     let krate = tcx.crate_name(LOCAL_CRATE);
+    let mut all_stub_verified_targets = FxHashMap::default();
+    let mut all_contract_targets = HashSet::new();
+
     for item in tcx.hir_free_items() {
         let def_id = item.owner_id.def_id.to_def_id();
-        KaniAttributes::for_item(tcx, def_id).check_attributes();
+        let (stub_verified_targets, contract_targets) =
+            KaniAttributes::for_item(tcx, def_id).check_attributes();
+        all_stub_verified_targets.extend(stub_verified_targets);
+        all_contract_targets.extend(contract_targets);
+
         if tcx.def_kind(def_id) == DefKind::GlobalAsm {
             if !ignore_asm {
                 let error_msg = format!(
@@ -59,6 +66,21 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
             }
         }
     }
+
+    // Validate that all stub_verified targets have corresponding proof_for_contract harnesses
+    for (stub_verified_target, span) in all_stub_verified_targets {
+        if !all_contract_targets.contains(&stub_verified_target) {
+            tcx.dcx().struct_span_err(
+                span,
+                format!(
+                    "stub verified target `{}` does not have a corresponding `#[proof_for_contract]` harness",
+                    stub_verified_target.name()
+                ),
+            ).with_help("verified stubs are meant to be sound abstractions for a function's behavior, so Kani enforces that proofs exist for the stub's contract")
+            .emit();
+        }
+    }
+
     tcx.dcx().abort_if_errors();
 }
 

kani-driver/src/harness_runner.rs

@@ -55,8 +55,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
         &self,
         harnesses: &'pr [&HarnessMetadata],
     ) -> Result<Vec<HarnessResult<'pr>>> {
-        self.check_stubbing(harnesses)?;
-
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
         let pool = {
             let mut builder = rayon::ThreadPoolBuilder::new();
@@ -114,33 +112,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
             }
         }
     }
-
-    /// Return an error if the user is trying to verify a harness with stubs without enabling the
-    /// experimental feature.
-    fn check_stubbing(&self, harnesses: &[&HarnessMetadata]) -> Result<()> {
-        if !self.sess.args.is_stubbing_enabled() {
-            let with_stubs: Vec<_> = harnesses
-                .iter()
-                .filter_map(|harness| {
-                    (!harness.attributes.stubs.is_empty()).then_some(harness.pretty_name.as_str())
-                })
-                .collect();
-            match with_stubs.as_slice() {
-                [] => { /* do nothing */ }
-                [harness] => bail!(
-                    "Use of unstable feature 'stubbing' in harness `{}`.\n\
-                    To enable stubbing, pass option `-Z stubbing`",
-                    harness
-                ),
-                harnesses => bail!(
-                    "Use of unstable feature 'stubbing' in harnesses `{}`.\n\
-                    To enable stubbing, pass option `-Z stubbing`",
-                    harnesses.join("`, `")
-                ),
-            }
-        }
-        Ok(())
-    }
 }
 
 impl KaniSession {

tests/expected/function-contract/as-assertions/precedence.expected

@@ -31,4 +31,4 @@ assertion\
 	 - Status: SUCCESS\
 	 - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr"
 
-Complete - 3 successfully verified harnesses, 0 failures, 3 total.
+Complete - 4 successfully verified harnesses, 0 failures, 4 total.

tests/expected/function-contract/as-assertions/precedence.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 // If a function is the target of a proof_for_contract or stub_verified, we should defer to the contract handling for those modes.
 
@@ -12,6 +12,7 @@ fn add_three(add_three_ptr: &mut u32) {
 }
 
 #[kani::requires(*add_two_ptr < 101)]
+#[kani::modifies(add_two_ptr)]
 #[kani::ensures(|_| old(*add_two_ptr + 2) == *add_two_ptr)]
 fn add_two(add_two_ptr: &mut u32) {
     *add_two_ptr += 1;
@@ -59,3 +60,11 @@ fn stub_verified_takes_precedence() {
     let mut i = kani::any();
     add_three(&mut i);
 }
+
+// The stub_verified contract mandates that we have a proof for the target of the verified stub
+#[kani::proof_for_contract(add_two)]
+fn check_add_two() {
+    // 3 so that when add_one's contract is generated as an assertion, its precondition holds
+    let mut x = 3;
+    add_two(&mut x);
+}

tests/expected/function-contract/gcd_rec_replacement_pass.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
@@ -47,13 +47,21 @@ impl Frac {
     }
 }
 
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(64)]
+fn gcd_harness() {
+    let x: T = kani::any();
+    let y: T = kani::any();
+    gcd(x, y);
+}
+
 #[kani::proof]
 #[kani::stub_verified(gcd)]
 fn gcd_as_replace() {
-    gcd_harness()
+    gcd_test_harness()
 }
 
-fn gcd_harness() {
+fn gcd_test_harness() {
     // Needed to avoid having `free` be removed as unused function. This is
     // because DFCC contract enforcement assumes that a definition for `free`
     // exists.

tests/expected/function-contract/gcd_replacement_fail.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
@@ -54,6 +54,14 @@ impl Frac {
     }
 }
 
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(64)]
+fn gcd_harness() {
+    let x: T = kani::any();
+    let y: T = kani::any();
+    gcd(x, y);
+}
+
 #[kani::proof]
 #[kani::stub_verified(gcd)]
 fn main() {

tests/expected/function-contract/gcd_replacement_pass.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
@@ -54,6 +54,14 @@ impl Frac {
     }
 }
 
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(64)]
+fn gcd_harness() {
+    let x: T = kani::any();
+    let y: T = kani::any();
+    gcd(x, y);
+}
+
 #[kani::proof]
 #[kani::stub_verified(gcd)]
 fn main() {

tests/expected/function-contract/history/stub.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // This test consumes > 9 GB of memory with 16 object bits. Reducing the number
 // of object bits to 8 to avoid running out of memory.
-// kani-flags: -Zfunction-contracts -Z unstable-options --cbmc-args --object-bits 8
+// kani-flags: -Zfunction-contracts -Zstubbing -Z unstable-options --cbmc-args --object-bits 8
 
 #[kani::ensures(|result| old(*ptr + *ptr) == *ptr)]
 #[kani::requires(*ptr < 100)]

tests/expected/function-contract/interior-mutability/api/cell_stub.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts --solver minisat
+// kani-flags: -Zfunction-contracts -Zstubbing --solver minisat
 
 /// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple.
 /// This shows that we can generate `kani::any()` for Cell.