Instantiate path generic arguments during type resolution

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

@@ -8,7 +8,9 @@ use rustc_hir::def::DefKind;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::Mutability;
 use rustc_public::rustc_internal;
-use rustc_public::ty::{FloatTy, IntTy, Region, RegionKind, RigidTy, Ty, UintTy};
+use rustc_public::ty::{
+    FloatTy, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy,
+};
 use rustc_span::def_id::LocalDefId;
 use std::str::FromStr;
 use strum_macros::{EnumString, IntoStaticStr};
@@ -47,7 +49,8 @@ pub fn resolve_ty<'tcx>(
                     "type",
                     DefKind::Struct | DefKind::Union | DefKind::Enum
                 )?;
-                Ok(rustc_internal::stable(tcx.type_of(def_id)).value)
+                let ty = rustc_internal::stable(tcx.type_of(def_id)).value;
+                Ok(instantiate_path_args(tcx, current_module, path, ty))
             }
         }
         Type::Array(array) => {
@@ -96,6 +99,61 @@ pub fn resolve_ty<'tcx>(
     }
 }
 
+/// If `path`'s final segment carries angle-bracketed generic arguments, instantiate `ty`
+/// (the definition's identity type, e.g. `Wrap<T>`) with those arguments resolved to
+/// concrete types (e.g. `Wrap<u8>`), so trait-implementation lookups can match a concrete
+/// impl. Returns `ty` unchanged when there are no arguments or when any argument cannot
+/// be resolved — preserving the previous behavior for everything that resolved before.
+fn instantiate_path_args<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    current_module: LocalDefId,
+    path: &syn::Path,
+    ty: Ty,
+) -> Ty {
+    let Some(syn::PathArguments::AngleBracketed(syn_args)) =
+        path.segments.last().map(|seg| &seg.arguments)
+    else {
+        return ty;
+    };
+    let TyKind::RigidTy(RigidTy::Adt(adt_def, identity_args)) = ty.kind() else {
+        return ty;
+    };
+    // Resolve the user-written type arguments; lifetimes are erased below, and anything
+    // else (const arguments, associated-type bindings) keeps the uninstantiated type.
+    let mut user_tys = Vec::new();
+    for arg in &syn_args.args {
+        match arg {
+            syn::GenericArgument::Type(syn_ty) => match resolve_ty(tcx, current_module, syn_ty) {
+                Ok(t) => user_tys.push(t),
+                Err(_) => return ty,
+            },
+            syn::GenericArgument::Lifetime(_) => {}
+            _ => return ty,
+        }
+    }
+    // Substitute the definition's type parameters in declaration order; erase lifetime
+    // parameters. A count mismatch (e.g. defaulted parameters the user omitted) keeps
+    // the uninstantiated type.
+    let mut user_iter = user_tys.into_iter();
+    let mut new_args = Vec::new();
+    for arg in &identity_args.0 {
+        match arg {
+            GenericArgKind::Type(_) => match user_iter.next() {
+                Some(t) => new_args.push(GenericArgKind::Type(t)),
+                None => return ty,
+            },
+            GenericArgKind::Lifetime(_) => {
+                new_args.push(GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased }))
+            }
+            GenericArgKind::Const(_) => return ty,
+        }
+    }
+    if user_iter.next().is_some() {
+        return ty;
+    }
+    Ty::from_rigid_kind(RigidTy::Adt(adt_def, GenericArgs(new_args)))
+}
+
 /// Enumeration of existing primitive types that are not parametric.
 #[derive(Copy, Clone, Debug, Eq, PartialEq, IntoStaticStr, EnumString)]
 #[strum(serialize_all = "lowercase")]

tests/expected/function-contract/generic_arg_unimplemented.expected

@@ -0,0 +1 @@
+unable to find implementation of associated function `Generic::generic` for S

tests/expected/function-contract/generic_arg_unimplemented.rs

@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// A proof_for_contract on an instantiation that is NOT implemented (`Generic<Wrap<u16>>`,
+// where only `Generic<Wrap<u8>>` exists) must fail to resolve. Guards that instantiating
+// the path's generic arguments (kani#1997) does not over-resolve to the wrong impl.
+
+struct S(u32);
+struct Wrap<T>(T);
+
+trait Generic<T> {
+    fn generic(&self) -> u32;
+}
+
+impl Generic<Wrap<u8>> for S {
+    #[kani::requires(self.0 < 100)]
+    #[kani::ensures(|r| *r == self.0)]
+    fn generic(&self) -> u32 {
+        self.0
+    }
+}
+
+#[cfg(kani)]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(<S as Generic<Wrap<u16>>>::generic)]
+    fn check_unimplemented() {
+        let s = S(kani::any());
+        let _ = Generic::<Wrap<u8>>::generic(&s);
+    }
+}

tests/expected/function-contract/generic_method_unimplemented.expected

@@ -0,0 +1 @@
+unable to find implementation of associated function `Compute::compute` for S

tests/expected/function-contract/generic_method_unimplemented.rs

@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// A `proof_for_contract` on a trait method that carries its OWN generic parameter
+// (`fn compute<T>`) is the case kani#1997 still does not support. Instantiating the
+// path's generic arguments (this change) binds the self type and the trait's arguments,
+// not a method-level type parameter, so this must still fail to resolve.
+
+struct S(u32);
+
+trait Compute {
+    fn compute<T>(&self, x: T) -> u32;
+}
+
+impl Compute for S {
+    #[kani::requires(self.0 < 100)]
+    #[kani::ensures(|r| *r == self.0)]
+    fn compute<T>(&self, _x: T) -> u32 {
+        self.0
+    }
+}
+
+#[cfg(kani)]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(<S as Compute>::compute)]
+    fn check_generic_method() {
+        let s = S(kani::any());
+        let _ = s.compute(0u8);
+    }
+}

tests/kani/FunctionContracts/generic_argument_instantiation.rs

@@ -0,0 +1,156 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// `proof_for_contract` on a target whose type carries generic arguments — the remaining
+// generic-parameter case from https://github.com/model-checking/kani/issues/1997.
+// `resolve_ty` now instantiates a path type's generic arguments before resolution, so
+// these all resolve and verify:
+//   * a generic *argument* that is itself generic (`Generic<Wrap<u8>>`),
+//   * a generic *self* type with an associated-type return and a `where`-bounded method,
+//   * a concrete DST self type with a generic argument (the `<CStr as Index<RangeFrom>>` shape),
+//   * a generic *impl* (`impl<T> Get for W<T>`) queried at a concrete instantiation,
+//   * a type with a lifetime parameter beside a type parameter (`Borrowed<'a, T>`) — lifetime erased.
+// `check_primitive_arg` guards that the already-working concrete-argument case is unchanged.
+
+struct S(u32);
+struct Wrap<T>(T);
+
+trait Generic<T> {
+    fn generic(&self) -> u32;
+}
+
+impl Generic<u8> for S {
+    #[kani::requires(self.0 < 100)]
+    #[kani::ensures(|r| *r == self.0)]
+    fn generic(&self) -> u32 {
+        self.0
+    }
+}
+
+// Distinct body from the `Generic<u8>` impl above, so the harness only verifies
+// if resolution lands on *this* impl rather than the sibling.
+impl Generic<Wrap<u8>> for S {
+    #[kani::requires(self.0 < 100)]
+    #[kani::ensures(|r| *r == self.0 + 1)]
+    fn generic(&self) -> u32 {
+        self.0 + 1
+    }
+}
+
+trait Access {}
+
+struct W<T>(T);
+
+impl Access for W<u8> {}
+
+trait Indexed {
+    type Item;
+    unsafe fn get_unchecked(&self, i: usize) -> Self::Item
+    where
+        Self: Access;
+}
+
+impl Indexed for W<u8> {
+    type Item = u8;
+    #[kani::requires(i < 1)]
+    #[kani::ensures(|r| *r == 0)]
+    unsafe fn get_unchecked(&self, i: usize) -> u8
+    where
+        Self: Access,
+    {
+        let _ = i;
+        0
+    }
+}
+
+trait Get {
+    fn get(&self) -> u32;
+}
+
+// A generic impl: the query `<W<u8> as Get>::get` supplies the concrete instantiation.
+impl<T> Get for W<T> {
+    #[kani::requires(true)]
+    #[kani::ensures(|r| *r == 7)]
+    fn get(&self) -> u32 {
+        7
+    }
+}
+
+#[repr(transparent)]
+struct Dst([u8]);
+
+trait Peek<T> {
+    fn peek(&self) -> u32;
+}
+
+impl Peek<Wrap<u8>> for Dst {
+    #[kani::requires(true)]
+    #[kani::ensures(|r| *r as usize == self.0.len())]
+    fn peek(&self) -> u32 {
+        self.0.len() as u32
+    }
+}
+
+struct Borrowed<'a, T>(&'a T);
+
+trait Held {
+    fn held(&self) -> u32;
+}
+
+impl<'a, T> Held for Borrowed<'a, T> {
+    #[kani::requires(true)]
+    #[kani::ensures(|r| *r == 0)]
+    fn held(&self) -> u32 {
+        0
+    }
+}
+
+#[cfg(kani)]
+mod verify {
+    use super::*;
+
+    // Concrete (primitive) argument — resolved before this change; must still resolve.
+    #[kani::proof_for_contract(<S as Generic<u8>>::generic)]
+    fn check_primitive_arg() {
+        let s = S(kani::any());
+        let _ = Generic::<u8>::generic(&s);
+    }
+
+    // Generic argument that is itself generic — now resolves.
+    #[kani::proof_for_contract(<S as Generic<Wrap<u8>>>::generic)]
+    fn check_generic_arg() {
+        let s = S(kani::any());
+        let _ = Generic::<Wrap<u8>>::generic(&s);
+    }
+
+    // Generic self type + associated-type return + `where`-bounded method — now resolves.
+    #[kani::proof_for_contract(<W<u8> as Indexed>::get_unchecked)]
+    fn check_generic_self() {
+        let w = W(0u8);
+        let _ = unsafe { <W<u8> as Indexed>::get_unchecked(&w, kani::any()) };
+    }
+
+    // Concrete DST self with a generic argument — now resolves.
+    #[kani::proof_for_contract(<Dst as Peek<Wrap<u8>>>::peek)]
+    fn check_dst_self() {
+        let bytes = [1u8, 2, 3];
+        let dst: &Dst = unsafe { &*(&bytes[..] as *const [u8] as *const Dst) };
+        let _ = dst.peek();
+    }
+
+    // Generic impl queried at a concrete instantiation — now resolves.
+    #[kani::proof_for_contract(<W<u8> as Get>::get)]
+    fn check_generic_impl() {
+        let w = W(0u8);
+        let _ = w.get();
+    }
+
+    // Lifetime parameter beside a type parameter — lifetime erased, type substituted.
+    #[kani::proof_for_contract(<Borrowed<'static, u8> as Held>::held)]
+    fn check_lifetime_param() {
+        let x = 0u8;
+        let b = Borrowed(&x);
+        let _ = b.held();
+    }
+}