From 25090ddd535774dc590fef5aa356cdee228c3d84 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Wed, 23 Sep 2026 15:02:08 -0400 Subject: [PATCH] Instantiate path generic arguments during type resolution resolve_ty returned tcx.type_of(def_id) uninstantiated for path types, dropping the path's own generic arguments (RangeFrom became RangeFrom), so Instance::resolve could not match a concrete trait implementation. Resolve the angle-bracketed arguments and substitute them into the definition's identity args; any argument shape that cannot be resolved keeps the previous uninstantiated behavior. --- .../kani_middle/resolve/type_resolution.rs | 62 ++++++- .../generic_arg_unimplemented.expected | 1 + .../generic_arg_unimplemented.rs | 33 ++++ .../generic_method_unimplemented.expected | 1 + .../generic_method_unimplemented.rs | 33 ++++ .../generic_argument_instantiation.rs | 156 ++++++++++++++++++ 6 files changed, 284 insertions(+), 2 deletions(-) create mode 100644 tests/expected/function-contract/generic_arg_unimplemented.expected create mode 100644 tests/expected/function-contract/generic_arg_unimplemented.rs create mode 100644 tests/expected/function-contract/generic_method_unimplemented.expected create mode 100644 tests/expected/function-contract/generic_method_unimplemented.rs create mode 100644 tests/kani/FunctionContracts/generic_argument_instantiation.rs diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs index 7e136a47f6de..fe43d4841a5f 100644 --- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs +++ b/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`) with those arguments resolved to +/// concrete types (e.g. `Wrap`), 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")] diff --git a/tests/expected/function-contract/generic_arg_unimplemented.expected b/tests/expected/function-contract/generic_arg_unimplemented.expected new file mode 100644 index 000000000000..e79e83302f6d --- /dev/null +++ b/tests/expected/function-contract/generic_arg_unimplemented.expected @@ -0,0 +1 @@ +unable to find implementation of associated function `Generic::generic` for S diff --git a/tests/expected/function-contract/generic_arg_unimplemented.rs b/tests/expected/function-contract/generic_arg_unimplemented.rs new file mode 100644 index 000000000000..402b1f1d1333 --- /dev/null +++ b/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>`, +// where only `Generic>` 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); + +trait Generic { + fn generic(&self) -> u32; +} + +impl Generic> 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(>>::generic)] + fn check_unimplemented() { + let s = S(kani::any()); + let _ = Generic::>::generic(&s); + } +} diff --git a/tests/expected/function-contract/generic_method_unimplemented.expected b/tests/expected/function-contract/generic_method_unimplemented.expected new file mode 100644 index 000000000000..a38913e94d86 --- /dev/null +++ b/tests/expected/function-contract/generic_method_unimplemented.expected @@ -0,0 +1 @@ +unable to find implementation of associated function `Compute::compute` for S diff --git a/tests/expected/function-contract/generic_method_unimplemented.rs b/tests/expected/function-contract/generic_method_unimplemented.rs new file mode 100644 index 000000000000..9f692e3c3c56 --- /dev/null +++ b/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`) 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(&self, x: T) -> u32; +} + +impl Compute for S { + #[kani::requires(self.0 < 100)] + #[kani::ensures(|r| *r == self.0)] + fn compute(&self, _x: T) -> u32 { + self.0 + } +} + +#[cfg(kani)] +mod verify { + use super::*; + + #[kani::proof_for_contract(::compute)] + fn check_generic_method() { + let s = S(kani::any()); + let _ = s.compute(0u8); + } +} diff --git a/tests/kani/FunctionContracts/generic_argument_instantiation.rs b/tests/kani/FunctionContracts/generic_argument_instantiation.rs new file mode 100644 index 000000000000..3ce4ee34597c --- /dev/null +++ b/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>`), +// * a generic *self* type with an associated-type return and a `where`-bounded method, +// * a concrete DST self type with a generic argument (the `>` shape), +// * a generic *impl* (`impl Get for W`) 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); + +trait Generic { + fn generic(&self) -> u32; +} + +impl Generic for S { + #[kani::requires(self.0 < 100)] + #[kani::ensures(|r| *r == self.0)] + fn generic(&self) -> u32 { + self.0 + } +} + +// Distinct body from the `Generic` impl above, so the harness only verifies +// if resolution lands on *this* impl rather than the sibling. +impl Generic> 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); + +impl Access for W {} + +trait Indexed { + type Item; + unsafe fn get_unchecked(&self, i: usize) -> Self::Item + where + Self: Access; +} + +impl Indexed for W { + 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 ` as Get>::get` supplies the concrete instantiation. +impl Get for W { + #[kani::requires(true)] + #[kani::ensures(|r| *r == 7)] + fn get(&self) -> u32 { + 7 + } +} + +#[repr(transparent)] +struct Dst([u8]); + +trait Peek { + fn peek(&self) -> u32; +} + +impl Peek> 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(>::generic)] + fn check_primitive_arg() { + let s = S(kani::any()); + let _ = Generic::::generic(&s); + } + + // Generic argument that is itself generic — now resolves. + #[kani::proof_for_contract(>>::generic)] + fn check_generic_arg() { + let s = S(kani::any()); + let _ = Generic::>::generic(&s); + } + + // Generic self type + associated-type return + `where`-bounded method — now resolves. + #[kani::proof_for_contract( as Indexed>::get_unchecked)] + fn check_generic_self() { + let w = W(0u8); + let _ = unsafe { as Indexed>::get_unchecked(&w, kani::any()) }; + } + + // Concrete DST self with a generic argument — now resolves. + #[kani::proof_for_contract(>>::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( 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( as Held>::held)] + fn check_lifetime_param() { + let x = 0u8; + let b = Borrowed(&x); + let _ = b.held(); + } +}