Support contracts & stubs in trait implementations (partial fix)

Cargo.lock

@@ -1187,6 +1187,8 @@ dependencies = [
  "proc-macro-error2",
  "proc-macro2",
  "quote",
+ "strum",
+ "strum_macros",
  "syn",
 ]
 

kani-compiler/src/kani_middle/attributes.rs

@@ -679,11 +679,27 @@ impl<'tcx> KaniAttributes<'tcx> {
                 span,
                 format!("failed to resolve `{}`: {resolve_err}", pretty_type_path(path)),
             );
-            if let ResolveError::AmbiguousPartialPath { .. } = resolve_err {
-                err = err.with_help(format!(
-                    "replace `{}` with a specific implementation.",
-                    pretty_type_path(path)
-                ));
+            match resolve_err {
+                ResolveError::AmbiguousPartialPath { .. } => {
+                    err = err.with_help(format!(
+                        "replace `{}` with a specific implementation.",
+                        pretty_type_path(path)
+                    ));
+                }
+                ResolveError::MissingTraitImpl { tcx: _, trait_fn_id, ty: _ } => {
+                    let generics = self.tcx.generics_of(trait_fn_id);
+                    let parent_generics =
+                        generics.parent.map(|parent| self.tcx.generics_of(parent));
+                    if !generics.own_params.is_empty()
+                        || parent_generics.is_some_and(|generics| !generics.own_params.is_empty())
+                    {
+                        err = err.with_note(
+                            "Kani does not currently support stubs or function contracts on generic functions in traits.\n \
+                            See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.",
+                        );
+                    }
+                }
+                _ => {}
             }
             err.emit();
         }
@@ -732,8 +748,43 @@ impl<'tcx> KaniAttributes<'tcx> {
             });
             match paths.as_slice() {
                 [orig, replace] => {
-                    let _ = self.resolve_path(current_module, orig, attr.span());
-                    let _ = self.resolve_path(current_module, replace, attr.span());
+                    let original_res = self.resolve_path(current_module, orig, attr.span()).map(|res| res.def());
+                    let replace_res = self.resolve_path(current_module, replace, attr.span()).map(|res| res.def());
+
+                    if let Ok(original_res) = original_res && let Ok(replace_res) = replace_res {
+                        // Emit an error if either function is local, yet doesn't have a body.
+                        // This can happen if a user specifies a trait fn without a default body, e.g. B::bar, where B is a trait.
+                        let o_bad = original_res.krate().is_local && !original_res.has_body();
+                        let r_bad = replace_res.krate().is_local && !replace_res.has_body();
+
+                        if o_bad || r_bad {
+                            let mut err = self.tcx.dcx().struct_span_err(
+                                attr.span(),
+                                "invalid stub: function does not have a body, but is not an extern function",
+                            );
+                            if o_bad {
+                                err = err.with_span_note(
+                                    rustc_internal::internal(self.tcx, original_res.span()),
+                                    format!(
+                                    "`{}` does not have a body",
+                                    original_res.name()
+                                ));
+                            }
+                            if r_bad {
+                                err = err.with_span_note(
+                                    rustc_internal::internal(self.tcx, replace_res.span()),
+                                    format!(
+                                    "`{}` does not have a body",
+                                    replace_res.name()
+                                ));
+                            }
+                            err = err.with_help(
+                                "if this stub refers to associated functions, try using fully-qualified syntax instead"
+                            );
+                            err.emit();
+                        }
+                    }
+
                     Some(Stub {
                         original: orig.to_token_stream().to_string(),
                         replacement: replace.to_token_stream().to_string(),

kani-compiler/src/kani_middle/resolve.rs

@@ -5,9 +5,6 @@
 //! `DefId`s for functions and methods. For the definition of a path, see
 //! <https://doc.rust-lang.org/reference/paths.html>.
 //!
-//! TODO: Change `resolve_fn` in order to return information about trait implementations.
-//! <https://github.com/model-checking/kani/issues/1997>
-//!
 //! Note that glob use statements can form loops. The paths can also walk through the loop.
 
 use crate::kani_middle::stable_fn_def;
@@ -17,9 +14,12 @@ use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalMo
 use rustc_hir::{ItemKind, UseKind};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::ty::fast_reject::{self, TreatParams};
-use rustc_public::CrateDef;
+use rustc_public::mir::mono::Instance;
 use rustc_public::rustc_internal;
-use rustc_public::ty::{FnDef, RigidTy, Ty, TyKind};
+use rustc_public::ty::{
+    AssocItem, FnDef, GenericArgKind, GenericArgs, RigidTy, TraitDef, Ty, TyKind,
+};
+use rustc_public::{CrateDef, CrateDefItems};
 use std::collections::HashSet;
 use std::fmt;
 use std::iter::Peekable;
@@ -67,10 +67,13 @@ pub fn resolve_fn_path<'tcx>(
     match &path.qself {
         // Qualified path for a trait method implementation, like `<Foo as Bar>::bar`.
         Some(QSelf { ty: syn_ty, position, .. }) if *position > 0 => {
+            // Resolve the self type and DefId of the trait definition method.
+            // E.g., in path <usize as SliceIndex<[i32]>>::get_unchecked, ty = `usize` and `trait_fn_id` is the ID of `get_unchecked`
+            // in the definition of the `SliceIndex`` trait.
             let ty = type_resolution::resolve_ty(tcx, current_module, syn_ty)?;
-            let def_id = resolve_path(tcx, current_module, &path.path)?;
-            validate_kind!(tcx, def_id, "function / method", DefKind::Fn | DefKind::AssocFn)?;
-            Ok(FnResolution::FnImpl { def: stable_fn_def(tcx, def_id).unwrap(), ty })
+            let trait_fn_id = resolve_path(tcx, current_module, &path.path)?;
+            validate_kind!(tcx, trait_fn_id, "function / method", DefKind::Fn | DefKind::AssocFn)?;
+            resolve_in_trait_impl(tcx, ty, trait_fn_id)
         }
         // Qualified path for a primitive type, such as `<[u8]::sort>`.
         Some(QSelf { ty: syn_ty, .. }) if type_resolution::is_type_primitive(syn_ty) => {
@@ -98,9 +101,7 @@ pub fn resolve_fn_path<'tcx>(
     }
 }
 
-/// Attempts to resolve a *simple path* (in the form of a string) to a function / method `DefId`.
-///
-/// Use `[resolve_fn_path]` if you want to handle qualified paths and simple paths.
+/// Attempts to resolve a path (in the form of a string) to a function / method `DefId`.
 pub fn resolve_fn<'tcx>(
     tcx: TyCtxt<'tcx>,
     current_module: LocalDefId,
@@ -111,11 +112,7 @@ pub fn resolve_fn<'tcx>(
         msg: format!("Expected a path, but found `{path_str}`. {err}"),
     })?;
     let result = resolve_fn_path(tcx, current_module, &path)?;
-    if let FnResolution::Fn(def) = result {
-        Ok(rustc_internal::internal(tcx, def.def_id()))
-    } else {
-        Err(ResolveError::UnsupportedPath { kind: "qualified paths" })
-    }
+    Ok(rustc_internal::internal(tcx, result.def().def_id()))
 }
 
 /// Attempts to resolve a simple path (in the form of a string) to a `DefId`.
@@ -136,7 +133,7 @@ fn resolve_path<'tcx>(
             DefKind::Struct | DefKind::Enum | DefKind::Union => {
                 resolve_in_type_def(tcx, base, &path.base_path_args, &name)
             }
-            DefKind::Trait => resolve_in_trait(tcx, base, &name),
+            DefKind::Trait => resolve_in_trait_def(tcx, base, &name),
             kind => {
                 debug!(?base, ?kind, "resolve_path: unexpected item");
                 Err(ResolveError::UnexpectedType { tcx, item: base, expected: "module" })
@@ -158,6 +155,8 @@ pub enum ResolveError<'tcx> {
     InvalidPath { msg: String },
     /// Unable to find an item.
     MissingItem { tcx: TyCtxt<'tcx>, base: DefId, unresolved: String },
+    /// Unable to find the specified implementation of a trait.
+    MissingTraitImpl { tcx: TyCtxt<'tcx>, trait_fn_id: DefId, ty: Ty },
     /// Unable to find an item in a primitive type.
     MissingPrimitiveItem { base: Ty, unresolved: String },
     /// Error triggered when the identifier points to an item with unexpected type.
@@ -213,6 +212,10 @@ impl fmt::Display for ResolveError<'_> {
                 let def_desc = description(*tcx, *base);
                 write!(f, "unable to find `{unresolved}` inside {def_desc}")
             }
+            ResolveError::MissingTraitImpl { tcx, trait_fn_id, ty } => {
+                let def_desc = description(*tcx, *trait_fn_id);
+                write!(f, "unable to find implementation of {def_desc} for {ty}")
+            }
             ResolveError::MissingPrimitiveItem { base, unresolved } => {
                 write!(f, "unable to find `{unresolved}` inside `{base}`")
             }
@@ -385,6 +388,43 @@ fn resolve_in_foreign_module(tcx: TyCtxt, foreign_mod: DefId, name: &str) -> Opt
         .find_map(|item| if item.ident.as_str() == name { item.res.opt_def_id() } else { None })
 }
 
+/// Scan all traits in the local crate to check if any of their associated items match `name`.
+/// If so, check if `ty` implements the trait, and return a match if so.
+fn resolve_in_any_trait<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty, name: &str) -> Option<FnResolution> {
+    let matches: Vec<FnResolution> = rustc_public::all_trait_decls()
+        .into_iter()
+        .filter_map(|trait_def| {
+            resolve_in_trait_def_stable(tcx, trait_def, name).ok().and_then(|item| {
+                resolve_in_trait_impl(tcx, ty, rustc_internal::internal(tcx, item.def_id.def_id()))
+                    .ok()
+            })
+        })
+        .collect();
+    debug!(?name, ?ty, ?matches, "resolve_in_any_trait");
+    if matches.len() == 1 { Some(matches[0]) } else { None }
+}
+
+/// Resolves a trait method implementation by checking if there exists an Instance of the trait method for `ty`.
+/// This is distinct from `resolve_in_trait_def`: that function checks if the associated function is defined for the trait,
+/// while this function checks if it's implemented for `ty`.
+fn resolve_in_trait_impl(
+    tcx: TyCtxt<'_>,
+    ty: Ty,
+    trait_fn_id: DefId,
+) -> Result<FnResolution, ResolveError<'_>> {
+    debug!(?ty, "resolve_in_trait_impl");
+    // Given the `FnDef` of the *definition* of the trait method, see if there exists an Instance
+    // that implements that method for `ty`.
+    let trait_fn_fn_def = stable_fn_def(tcx, trait_fn_id).unwrap();
+    let desired_generic_args = GenericArgs(vec![GenericArgKind::Type(ty)]);
+    let exists = Instance::resolve(trait_fn_fn_def, &desired_generic_args);
+
+    // If such an Instance exists, return *its* FnDef (i.e., the FnDef inside the impl block for this `ty`)
+    exists.map_or(Err(ResolveError::MissingTraitImpl { tcx, trait_fn_id, ty }), |inst| {
+        Ok(FnResolution::FnImpl { def: inst.ty().kind().fn_def().unwrap().0, ty })
+    })
+}
+
 /// Generates a more friendly string representation of a def_id including kind and name.
 /// (the default representation for the crate root is the empty string).
 fn description(tcx: TyCtxt, def_id: DefId) -> String {
@@ -557,7 +597,7 @@ fn resolve_in_type_def<'tcx>(
     base_path_args: &PathArguments,
     name: &str,
 ) -> Result<DefId, ResolveError<'tcx>> {
-    debug!(?name, ?type_id, "resolve_in_type");
+    debug!(?name, ?type_id, "resolve_in_type_def");
     // Try the inherent `impl` blocks (i.e., non-trait `impl`s).
     let candidates: Vec<DefId> = tcx
         .inherent_impls(type_id)
@@ -568,7 +608,17 @@ fn resolve_in_type_def<'tcx>(
         .collect();
 
     match candidates.len() {
-        0 => Err(ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() }),
+        0 => {
+            // Try to find the method in any trait implementation
+            let ty = rustc_internal::stable(tcx.type_of(type_id)).value;
+            resolve_in_any_trait(tcx, ty, name)
+                .map(|res| rustc_internal::internal(tcx, res.def().def_id()))
+                .ok_or_else(|| ResolveError::MissingItem {
+                    tcx,
+                    base: type_id,
+                    unresolved: name.to_string(),
+                })
+        }
         1 => Ok(candidates[0]),
         _ => {
             let invalid_path_err = |generic_args, candidates: Vec<DefId>| -> ResolveError {
@@ -624,13 +674,35 @@ fn resolve_in_type_def<'tcx>(
     }
 }
 
-/// Resolves a function in a trait.
-fn resolve_in_trait<'tcx>(
+/// Resolves a function in a trait definition.
+fn resolve_in_trait_def_stable<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    trait_def: TraitDef,
+    name: &str,
+) -> Result<AssocItem, ResolveError<'tcx>> {
+    debug!(?name, ?trait_def, "resolve_in_trait_def_stable");
+    let trait_def_def_id = rustc_internal::internal(tcx, trait_def.def_id());
+    let missing_item_err =
+        || ResolveError::MissingItem { tcx, base: trait_def_def_id, unresolved: name.to_string() };
+    // Look for the given name in the list of associated items for the trait definition.
+    trait_def
+        .associated_items()
+        .into_iter()
+        .find(|item| {
+            let item_def_id = rustc_internal::internal(tcx, item.def_id.def_id());
+            is_item_name(tcx, item_def_id, name)
+        })
+        .ok_or_else(missing_item_err)
+}
+
+/// Resolves a function in a trait definition.
+/// TODO: remove this function in favor of `resolve_in_trait_def_stable`, c.f. https://github.com/model-checking/kani/issues/4252
+fn resolve_in_trait_def<'tcx>(
     tcx: TyCtxt<'tcx>,
     trait_id: DefId,
     name: &str,
 ) -> Result<DefId, ResolveError<'tcx>> {
-    debug!(?name, ?trait_id, "resolve_in_trait");
+    debug!(?name, ?trait_id, "resolve_in_trait_def");
     let missing_item_err =
         || ResolveError::MissingItem { tcx, base: trait_id, unresolved: name.to_string() };
     let trait_def = tcx.trait_def(trait_id);
@@ -670,6 +742,10 @@ where
                     .copied()
                     .find(|item| is_item_name(tcx, *item, &name))
             })
+            .or_else(|| {
+                resolve_in_any_trait(tcx, ty, &name)
+                    .map(|res| rustc_internal::internal(tcx, res.def().def_id()))
+            })
             .ok_or_else(|| ResolveError::MissingPrimitiveItem {
                 base: ty,
                 unresolved: name.to_string(),

kani-compiler/src/kani_middle/resolve/type_resolution.rs

@@ -32,7 +32,9 @@ pub fn resolve_ty<'tcx>(
     #[warn(non_exhaustive_omitted_patterns)]
     match typ {
         Type::Path(TypePath { qself, path }) => {
-            assert_eq!(*qself, None, "Unexpected qualified path");
+            if (*qself).is_some() {
+                return unsupported("nested qualified paths");
+            }
             if let Some(primitive) =
                 path.get_ident().and_then(|ident| PrimitiveIdent::from_str(&ident.to_string()).ok())
             {

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -17,7 +17,7 @@ use rustc_public::mir::ConstOperand;
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::visit::{Location, MirVisitor};
 use rustc_public::rustc_internal;
-use rustc_public::ty::{FnDef, RigidTy, TyKind};
+use rustc_public::ty::{FnDef, GenericArgs, RigidTy, TyKind};
 use rustc_public::{CrateDef, CrateItem};
 
 use self::annotations::update_stub_mapping;
@@ -37,6 +37,37 @@ pub fn harness_stub_map(
     stub_pairs
 }
 
+/// For the purpose of checking generic argument length, don't consider the `Self` generic argument.
+/// The purpose is to allow stubbing out:
+/// ```rust
+/// pub trait Foo {
+///    fn foo(&self) -> bool {
+///        false
+///    }
+/// }
+/// ```
+/// with:
+/// ```rust
+/// pub fn stub_foo() -> bool {
+///    true
+/// }
+/// ```
+/// Since `rustc_public` APIs introduce a `Self` generic argument for trait functions
+fn generic_args_len_without_self(args: &GenericArgs) -> usize {
+    let len = args.0.len();
+    if len == 0 {
+        return len;
+    }
+    let has_self = args.0.iter().any(|arg| {
+        if let TyKind::Param(param_ty) = arg.expect_ty().kind() {
+            param_ty.name == "Self"
+        } else {
+            false
+        }
+    });
+    if has_self { len - 1 } else { len }
+}
+
 /// Checks whether the stub is compatible with the original function/method: do
 /// the arities and types (of the parameters and return values) match up? This
 /// does **NOT** check whether the type variables are constrained to implement
@@ -70,14 +101,17 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul
         unreachable!("Expected function, but found {new_ty}")
     };
 
+    let old_args_len = generic_args_len_without_self(&old_args);
+    let new_args_len = generic_args_len_without_self(&new_args);
+
     // TODO: We should check for the parameter type too or replacement will fail.
-    if old_args.0.len() != new_args.0.len() {
+    if old_args_len != new_args_len {
         let msg = format!(
             "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}",
             old_def.name(),
-            old_args.0.len(),
+            old_args_len,
             new_def.name(),
-            new_args.0.len(),
+            new_args_len,
         );
         return Err(msg);
     }

library/kani_macros/Cargo.toml

@@ -16,6 +16,8 @@ proc-macro2 = "1.0"
 proc-macro-error2 = { version = "2.0.0", features = ["nightly"] }
 quote = "1.0.20"
 syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-traits"] }
+strum = "0.27.1"
+strum_macros = "0.27.1"
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.