KaniAttributes Path Resolution Refactor (#4249)

Standardize our resolution handling for contracts and stubs:

- Make sure that the function paths for stubs and contract proofs
resolve ASAP (during `check_attributes`, pre-codegen), rather than
waiting until we're trying to actually do the stubbing or contract
instrumentation logic. The current implementation only does this for
stubs. Users get errors faster this way.
- Use the updated path resolution logic (c.f.
#4057) for both contracts
and stubs.
- Deduplicate a lot of the logic and make error messages/spans more
precise

This is useful to ensure that our error messages are consistent across
stubs and contracts for the same kinds of problems.

I opened #4251 with some
thoughts about further improvements.

Resolves #4057

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/codegen_aeneas_llbc/compiler_interface.rs

@@ -35,6 +35,7 @@ use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
 use rustc_public::mir::mono::{Instance, MonoItem};
 use rustc_public::rustc_internal;
+use rustc_public::ty::FnDef;
 use rustc_public::{CrateDef, DefId};
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
@@ -233,7 +234,8 @@ impl CodegenBackend for LlbcCodegenBackend {
                                 tcx,
                                 &[MonoItem::Fn(*harness)],
                                 model_path,
-                                contract_metadata,
+                                contract_metadata
+                                    .map(|def| rustc_internal::internal(tcx, def.def_id())),
                                 transformer,
                             );
                             transformer = BodyTransformation::new(&queries, tcx, &unit);
@@ -351,9 +353,9 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
 fn contract_metadata_for_harness(
     tcx: TyCtxt,
     def_id: DefId,
-) -> Result<Option<InternalDefId>, ErrorGuaranteed> {
+) -> Result<Option<FnDef>, ErrorGuaranteed> {
     let attrs = KaniAttributes::for_def_id(tcx, def_id);
-    Ok(attrs.interpret_for_contract_attribute().map(|(_, id, _)| id))
+    Ok(attrs.interpret_for_contract_attribute())
 }
 
 /// Return a struct that contains information about the codegen results as expected by `rustc`.

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -37,6 +37,7 @@ use rustc_middle::util::Providers;
 use rustc_public::CrateDef;
 use rustc_public::mir::mono::{Instance, MonoItem};
 use rustc_public::rustc_internal;
+use rustc_public::ty::FnDef;
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
@@ -215,24 +216,23 @@ impl GotocCodegenBackend {
         (gcx, items, contract_info)
     }
 
-    /// Given a contract harness, get the DefId of its target.
+    /// Given a harness, return the DefId of its target if it's a contract harness.
     /// For manual harnesses, extract it from the #[proof_for_contract] attribute.
     /// For automatic harnesses, extract the target from the harness's GenericArgs.
-    fn target_def_id_for_harness(
+    fn target_if_contract_harness(
         &self,
         tcx: TyCtxt,
         harness: &Instance,
         is_automatic_harness: bool,
-    ) -> Option<InternalDefId> {
+    ) -> Option<FnDef> {
         if is_automatic_harness {
             let kind = harness.args().0[0].expect_ty().kind();
             let (fn_to_verify_def, _) = kind.fn_def().unwrap();
-            let def_id = fn_to_verify_def.def_id();
-            let attrs = KaniAttributes::for_def_id(tcx, def_id);
-            if attrs.has_contract() { Some(rustc_internal::internal(tcx, def_id)) } else { None }
+            let attrs = KaniAttributes::for_def_id(tcx, fn_to_verify_def.def_id());
+            if attrs.has_contract() { Some(fn_to_verify_def) } else { None }
         } else {
             let harness_attrs = KaniAttributes::for_def_id(tcx, harness.def.def_id());
-            harness_attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)
+            harness_attrs.interpret_for_contract_attribute()
         }
     }
 }
@@ -343,13 +343,14 @@ impl CodegenBackend for GotocCodegenBackend {
                             let model_path = units.harness_model_path(*harness).unwrap();
                             let is_automatic_harness = units.is_automatic_harness(harness);
                             let contract_metadata =
-                                self.target_def_id_for_harness(tcx, harness, is_automatic_harness);
+                                self.target_if_contract_harness(tcx, harness, is_automatic_harness);
                             let (gcx, items, contract_info) = self.codegen_items(
                                 tcx,
                                 &[MonoItem::Fn(*harness)],
                                 model_path,
                                 &results.machine_model,
-                                contract_metadata,
+                                contract_metadata
+                                    .map(|def| rustc_internal::internal(tcx, def.def_id())),
                                 transformer,
                             );
                             if gcx.has_loop_contracts {