[Breaking Change] Fail if stub verified doesn't have a contract harness

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.

tests/expected/function-contract/missing_contract_for_replace.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
 
 fn no_contract() {}
 

tests/expected/function-contract/modifies/check_invalid_modifies.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
 
 //! Check that Kani reports the correct error message when modifies clause
 //! includes objects of types that do not implement `kani::Arbitrary`.
@@ -25,3 +25,9 @@ fn harness() {
     let mut i = kani::any_where(|x| *x < 100);
     use_modify(&mut i);
 }
+
+#[kani::proof_for_contract(modify)]
+fn check_modify() {
+    let mut x: u32 = kani::any();
+    modify(&mut x);
+}

tests/expected/function-contract/modifies/check_only_verification.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
 
 //! Check that Kani does not report any error when unused modifies clauses
 //! includes objects of types that do not implement `kani::Arbitrary`.
@@ -26,6 +26,12 @@ fn use_modify(ptr: &mut u32) {
     assert!(modify(ptr) == 100);
 }
 
+#[kani::proof_for_contract(modify)]
+fn modify_harness() {
+    let ptr = &mut kani::any();
+    modify(ptr);
+}
+
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn harness() {

tests/expected/function-contract/modifies/expr_replace_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
 
 // Tests that providing the "modifies" clause havocks the pointer such
 // that the increment can no longer be observed (in the absence of an
@@ -20,3 +20,10 @@ fn main() {
     modify(&mut i);
     assert!(*i == val + 1, "Increment");
 }
+
+#[kani::proof_for_contract(modify)]
+fn check_modify() {
+    let val = kani::any();
+    let mut ptr = Box::new(val);
+    modify(&mut ptr);
+}

tests/expected/function-contract/modifies/expr_replace_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
 
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
@@ -9,6 +9,13 @@ fn modify(ptr: &mut Box<u32>, prior: u32) {
     *ptr.as_mut() += 1;
 }
 
+#[kani::proof_for_contract(modify)]
+fn modify_harness() {
+    let ptr = &mut Box::new(kani::any());
+    let prior = kani::any();
+    modify(ptr, prior);
+}
+
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn main() {