Emit an error when proof_for_contract function is not found

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

@@ -7,6 +7,7 @@ use cbmc::goto_program::{Expr, Lambda, Location, Type};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
+use rustc_span::Span;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::mir::{Local, VarDebugInfoContents};
@@ -18,7 +19,8 @@ impl GotocCtx<'_> {
     /// for which it needs to be enforced.
     ///
     /// 1. Gets the `#[kanitool::modifies_wrapper = "..."]` target, then resolves exactly one
-    ///    instance of it. Panics if there are more or less than one instance.
+    ///    instance of it. Returns `None` if the target was not found. Panics if there are more
+    ///    than one instance.
     /// 2. The additional arguments for the inner checks are locations that may be modified.
     ///    Add them to the list of CBMC's assigns.
     /// 3. Returns the mangled name of the symbol it attached the contract to.
@@ -29,24 +31,35 @@ impl GotocCtx<'_> {
     pub fn handle_check_contract(
         &mut self,
         function_under_contract: InternalDefId,
+        span: Span,
         items: &[MonoItem],
-    ) -> AssignsContract {
+    ) -> Option<AssignsContract> {
         let tcx = self.tcx;
-        let modify = items
-            .iter()
-            .find_map(|item| {
-                // Find the instance under contract
-                let MonoItem::Fn(instance) = *item else { return None };
-                if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract {
-                    self.find_modifies(instance)
-                } else {
-                    None
-                }
+        let modify = items.iter().find_map(|item| {
+            // Find the instance under contract
+            let MonoItem::Fn(instance) = *item else { return None };
+            if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract {
+                self.find_modifies(instance)
+            } else {
+                None
+            }
+        });
+        if let Some(modify) = modify {
+            self.attach_modifies_contract(modify);
+            let recursion_tracker = self.find_recursion_tracker(items);
+            Some(AssignsContract {
+                recursion_tracker,
+                contracted_function_name: modify.mangled_name(),
             })
-            .unwrap();
-        self.attach_modifies_contract(modify);
-        let recursion_tracker = self.find_recursion_tracker(items);
-        AssignsContract { recursion_tracker, contracted_function_name: modify.mangled_name() }
+        } else {
+            let name = tcx.def_path_str(function_under_contract);
+            let err_msg = format!(
+                "The function specified in the `proof_for_contract` attribute, `{name}`, was not found.\
+                \nMake sure the function is reachable from the harness."
+            );
+            tcx.dcx().span_err(span, err_msg);
+            None
+        }
     }
 
     /// The name and location for the recursion tracker should match the exact information added

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -40,6 +40,7 @@ use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 use rustc_smir::rustc_internal;
+use rustc_span::Span;
 use rustc_target::abi::Endian;
 use rustc_target::spec::PanicStrategy;
 use stable_mir::mir::mono::{Instance, MonoItem};
@@ -81,7 +82,7 @@ impl GotocCodegenBackend {
         starting_items: &[MonoItem],
         symtab_goto: &Path,
         machine_model: &MachineModel,
-        check_contract: Option<InternalDefId>,
+        check_contract: Option<(InternalDefId, Span)>,
         mut transformer: BodyTransformation,
     ) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
         // This runs reachability analysis before global passes are applied.
@@ -180,7 +181,8 @@ impl GotocCodegenBackend {
                     }
                 }
 
-                check_contract.map(|check_id| gcx.handle_check_contract(check_id, &items))
+                check_contract
+                    .and_then(|(check_id, span)| gcx.handle_check_contract(check_id, span, &items))
             },
             "codegen",
         );
@@ -452,9 +454,9 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
     }
 }
 
-fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<InternalDefId> {
+fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<(InternalDefId, Span)> {
     let attrs = KaniAttributes::for_def_id(tcx, def_id);
-    attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)
+    attrs.interpret_for_contract_attribute().map(|(_, id, span)| (id, span))
 }
 
 fn check_target(session: &Session) {

tests/ui/unknown-contract-harness/expected

@@ -0,0 +1,6 @@
+error: The function specified in the `proof_for_contract` attribute, `foo`, was not found.\
+Make sure the function is reachable from the harness.
+test.rs:\
+|\
+| #[kani::proof_for_contract(foo)]\
+| ^^^^^^^^^^^^^^

tests/ui/unknown-contract-harness/test.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// This test checks Kani's error when function specified in `proof_for_contract`
+// harness is not found (e.g. because it's not reachable from the harness)
+
+#[kani::requires(true)]
+fn foo() {}
+
+#[kani::proof_for_contract(foo)]
+fn check_foo() {
+    assert!(true);
+}