From 7f77075fe83964261cebfb852b8fcd2a178f5133 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Mon, 28 Sep 2026 19:06:56 -0400 Subject: [PATCH 1/2] Fill omitted defaulted generic parameters during type resolution An omitted trailing type parameter with a declared default now resolves from that default, instantiated with the arguments so far (what rustc does for omitted arguments): as Trait>::m resolves as written, where the omitted allocator default previously kept the uninstantiated type. This unblocks std targets of the same shape, such as Challenge 24's as Iterator>::__iterator_get_unchecked. A parameter with no default, or a const parameter, keeps the uninstantiated type. A path with no generic arguments at all (PathArguments::None, e.g. a bare Wrapper for struct Wrapper) is now also treated as an empty argument list, so an all-defaulted type written with no argument list resolves too. Parenthesized arguments still keep the uninstantiated type, as before. --- .../kani_middle/resolve/type_resolution.rs | 70 ++++++++++--- .../generic_default_const_param.expected | 1 + .../generic_default_const_param.rs | 32 ++++++ .../generic_default_missing_bare.expected | 1 + .../generic_default_missing_bare.rs | 32 ++++++ .../generic_default_missing_required.expected | 1 + .../generic_default_missing_required.rs | 31 ++++++ .../generic_default_argument_fill.rs | 97 +++++++++++++++++++ 8 files changed, 249 insertions(+), 16 deletions(-) create mode 100644 tests/expected/function-contract/generic_default_const_param.expected create mode 100644 tests/expected/function-contract/generic_default_const_param.rs create mode 100644 tests/expected/function-contract/generic_default_missing_bare.expected create mode 100644 tests/expected/function-contract/generic_default_missing_bare.rs create mode 100644 tests/expected/function-contract/generic_default_missing_required.expected create mode 100644 tests/expected/function-contract/generic_default_missing_required.rs create mode 100644 tests/kani/FunctionContracts/generic_default_argument_fill.rs diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs index fe43d4841a5f..8b8936c961e7 100644 --- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs +++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs @@ -6,10 +6,12 @@ use crate::kani_middle::resolve::{ResolveError, resolve_path, validate_kind}; use quote::ToTokens; use rustc_hir::def::DefKind; use rustc_middle::ty::TyCtxt; +use rustc_public::CrateDef; use rustc_public::mir::Mutability; use rustc_public::rustc_internal; use rustc_public::ty::{ - FloatTy, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy, + AdtDef, FloatTy, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, + UintTy, }; use rustc_span::def_id::LocalDefId; use std::str::FromStr; @@ -102,26 +104,31 @@ 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. +/// impl. An omitted trailing parameter with a declared default is filled from the +/// default, also when the path has no generic arguments at all (`Wrapper` for +/// `struct Wrapper`). Returns `ty` unchanged when any argument cannot be +/// resolved or a parameter without a default is missing, 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; - }; + // No generic arguments (`Wrapper`) is an empty list; parenthesized args keep `ty`. + let syn_args: Vec<&syn::GenericArgument> = + match path.segments.last().map(|seg| &seg.arguments) { + Some(syn::PathArguments::AngleBracketed(args)) => args.args.iter().collect(), + Some(syn::PathArguments::None) => Vec::new(), + _ => 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 { + for arg in syn_args { match arg { syn::GenericArgument::Type(syn_ty) => match resolve_ty(tcx, current_module, syn_ty) { Ok(t) => user_tys.push(t), @@ -132,16 +139,22 @@ fn instantiate_path_args<'tcx>( } } // 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. + // parameters; fill an omitted trailing parameter that has a declared default from + // that default, instantiated with the arguments so far — what rustc does for omitted + // arguments. A missing parameter without a default keeps the uninstantiated type. let mut user_iter = user_tys.into_iter(); let mut new_args = Vec::new(); - for arg in &identity_args.0 { + for (param_index, arg) in identity_args.0.iter().enumerate() { match arg { - GenericArgKind::Type(_) => match user_iter.next() { - Some(t) => new_args.push(GenericArgKind::Type(t)), - None => return ty, - }, + GenericArgKind::Type(_) => { + let filled = user_iter + .next() + .or_else(|| default_type_arg(tcx, &adt_def, param_index, &new_args)); + match filled { + Some(t) => new_args.push(GenericArgKind::Type(t)), + None => return ty, + } + } GenericArgKind::Lifetime(_) => { new_args.push(GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased })) } @@ -154,6 +167,31 @@ fn instantiate_path_args<'tcx>( Ty::from_rigid_kind(RigidTy::Adt(adt_def, GenericArgs(new_args))) } +/// The declared default of `adt_def`'s `param_index`-th generic parameter, instantiated +/// with the arguments already substituted before it — how rustc fills an omitted trailing +/// argument (a default may only reference earlier parameters). `None` when the parameter +/// has no default or the default is not a type; the caller then keeps the uninstantiated +/// type. +fn default_type_arg<'tcx>( + tcx: TyCtxt<'tcx>, + adt_def: &AdtDef, + param_index: usize, + args_so_far: &[GenericArgKind], +) -> Option { + let def_id = rustc_internal::internal(tcx, adt_def.def_id()); + let default = tcx.generics_of(def_id).own_params.get(param_index)?.default_value(tcx)?; + let internal_args: Vec> = args_so_far + .iter() + .map(|arg| match arg { + GenericArgKind::Type(t) => Some(rustc_internal::internal(tcx, *t).into()), + GenericArgKind::Lifetime(_) => Some(tcx.lifetimes.re_erased.into()), + GenericArgKind::Const(_) => None, + }) + .collect::>()?; + let filled = default.instantiate(tcx, &internal_args[..]).skip_normalization().as_type()?; + Some(rustc_internal::stable(filled)) +} + /// 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_default_const_param.expected b/tests/expected/function-contract/generic_default_const_param.expected new file mode 100644 index 000000000000..692191ae13c9 --- /dev/null +++ b/tests/expected/function-contract/generic_default_const_param.expected @@ -0,0 +1 @@ +unable to find implementation of associated function `Probe::probe` for WithConst diff --git a/tests/expected/function-contract/generic_default_const_param.rs b/tests/expected/function-contract/generic_default_const_param.rs new file mode 100644 index 000000000000..3131e704550e --- /dev/null +++ b/tests/expected/function-contract/generic_default_const_param.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// A `proof_for_contract` path that omits a generic parameter with a declared default keeps +// the uninstantiated type when that parameter is a CONST parameter: only defaulted TYPE +// parameters are filled (see tests/kani/FunctionContracts/generic_default_argument_fill.rs). +// `WithConst` omits `N` (default 4); the const default is not filled, so the target +// keeps the uninstantiated type and fails to resolve. + +struct WithConst([T; N]); + +trait Probe { + fn probe(&self) -> u32; +} + +impl Probe for WithConst { + #[kani::ensures(|r| *r == 0)] + fn probe(&self) -> u32 { + 0 + } +} + +mod verify { + use super::*; + + #[kani::proof_for_contract( as Probe>::probe)] + fn check_const_default_not_filled() { + let w = WithConst([0u8; 4]); + let _ = w.probe(); + } +} diff --git a/tests/expected/function-contract/generic_default_missing_bare.expected b/tests/expected/function-contract/generic_default_missing_bare.expected new file mode 100644 index 000000000000..9a74957c0860 --- /dev/null +++ b/tests/expected/function-contract/generic_default_missing_bare.expected @@ -0,0 +1 @@ +unable to find implementation of associated function `Probe::probe` for NoDefaultBare diff --git a/tests/expected/function-contract/generic_default_missing_bare.rs b/tests/expected/function-contract/generic_default_missing_bare.rs new file mode 100644 index 000000000000..3067f9ea00fd --- /dev/null +++ b/tests/expected/function-contract/generic_default_missing_bare.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// A `proof_for_contract` path written with NO generic arguments (`NoDefaultBare`, not +// `NoDefaultBare<..>`) keeps the uninstantiated type when a parameter has no default. The +// no-arguments path is treated as an empty argument list, but the substitution loop still +// returns the identity type at the first parameter it cannot fill (see +// tests/kani/FunctionContracts/generic_default_argument_fill.rs). + +struct NoDefaultBare(T); + +trait Probe { + fn probe(&self) -> u32; +} + +impl Probe for NoDefaultBare { + #[kani::ensures(|r| *r == 2)] + fn probe(&self) -> u32 { + 2 + } +} + +mod verify { + use super::*; + + #[kani::proof_for_contract(::probe)] + fn check_missing_required_bare() { + let n = NoDefaultBare(1u8); + let _ = n.probe(); + } +} diff --git a/tests/expected/function-contract/generic_default_missing_required.expected b/tests/expected/function-contract/generic_default_missing_required.expected new file mode 100644 index 000000000000..b7fad8a92e08 --- /dev/null +++ b/tests/expected/function-contract/generic_default_missing_required.expected @@ -0,0 +1 @@ +unable to find implementation of associated function `Probe::probe` for NoDefault diff --git a/tests/expected/function-contract/generic_default_missing_required.rs b/tests/expected/function-contract/generic_default_missing_required.rs new file mode 100644 index 000000000000..e8dde83b8078 --- /dev/null +++ b/tests/expected/function-contract/generic_default_missing_required.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// A `proof_for_contract` path that omits a generic parameter WITHOUT a declared default +// (`NoDefault` for `NoDefault`) keeps the uninstantiated type and fails to +// resolve. Only parameters with declared defaults are filled (see +// tests/kani/FunctionContracts/generic_default_argument_fill.rs). + +struct NoDefault(T, U); + +trait Probe { + fn probe(&self) -> u32; +} + +impl Probe for NoDefault { + #[kani::ensures(|r| *r == 1)] + fn probe(&self) -> u32 { + 1 + } +} + +mod verify { + use super::*; + + #[kani::proof_for_contract( as Probe>::probe)] + fn check_missing_required_param() { + let n = NoDefault(1u8, 2u16); + let _ = n.probe(); + } +} diff --git a/tests/kani/FunctionContracts/generic_default_argument_fill.rs b/tests/kani/FunctionContracts/generic_default_argument_fill.rs new file mode 100644 index 000000000000..f1dc1826e8c8 --- /dev/null +++ b/tests/kani/FunctionContracts/generic_default_argument_fill.rs @@ -0,0 +1,97 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// `proof_for_contract` on a target that omits trailing generic parameters with declared +// defaults. An omitted trailing parameter is now filled from its declared default, +// instantiated with the arguments so far — what rustc does for omitted arguments. These +// all resolve and verify: +// * a std container default: `Vec` fills `A = Global`, +// * sibling discrimination under the fill: `Vec`'s impl has a distinct +// postcondition, so each harness only verifies if resolution picks its own impl, +// * a default referencing an earlier parameter: `Pair` fills `U = T` as `u8`, +// * the explicit spelling (`Vec`) resolves unchanged, +// * an all-defaulted type written with no argument list: `AllDefault` fills `T = u8`. +// `tests/expected/function-contract/generic_default_missing_required.rs` guards that a +// missing parameter without a default still fails to resolve. + +#![feature(allocator_api)] + +trait Sum { + fn total(&self) -> usize; +} + +impl Sum for Vec { + #[kani::requires(self.len() < 3)] + #[kani::ensures(|r| *r == self.len())] + fn total(&self) -> usize { + self.len() + } +} + +// Distinct postcondition from the `Vec` impl, so a harness only verifies if +// resolution lands on *this* impl rather than the sibling. +impl Sum for Vec { + #[kani::requires(self.len() < 3)] + #[kani::ensures(|r| *r == self.len() + 1)] + fn total(&self) -> usize { + self.len() + 1 + } +} + +// `U`'s default references the earlier parameter, so `Pair` must fill `U = u8`. +struct Pair(T, U); + +impl Sum for Pair { + #[kani::ensures(|r| *r == 2)] + fn total(&self) -> usize { + 2 + } +} + +// All parameters defaulted, written with no argument list at all (`AllDefault`, not +// `AllDefault<..>`): the omitted list must still be filled from the default `T = u8`. +struct AllDefault(T); + +impl Sum for AllDefault { + #[kani::ensures(|r| *r == 1)] + fn total(&self) -> usize { + 1 + } +} + +mod verify { + use super::*; + // Kani's path resolver does not see the prelude; name `Vec` explicitly. + use std::vec::Vec; + + #[kani::proof_for_contract( as Sum>::total)] + fn check_vec_default_filled() { + let v: Vec = vec![1, 2]; + let _ = v.total(); + } + + #[kani::proof_for_contract( as Sum>::total)] + fn check_vec_sibling_discriminated() { + let v: Vec = vec![1]; + let _ = v.total(); + } + + #[kani::proof_for_contract( as Sum>::total)] + fn check_default_from_earlier_param() { + let p = Pair(1u8, 2u8); + let _ = p.total(); + } + + #[kani::proof_for_contract( as Sum>::total)] + fn check_explicit_spelling_unchanged() { + let v: Vec = vec![1]; + let _ = v.total(); + } + + #[kani::proof_for_contract(::total)] + fn check_all_parameters_defaulted() { + let a = AllDefault(0u8); + let _ = a.total(); + } +} From 8aff4c408f2ebaec56324c721ce6f36d1a048617 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Thu, 1 Oct 2026 07:59:17 -0400 Subject: [PATCH 2/2] Format the syn_args match per rustfmt (nightly-2026-09-24) --- .../src/kani_middle/resolve/type_resolution.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs index 8b8936c961e7..6b4f221be2f5 100644 --- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs +++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs @@ -116,12 +116,12 @@ fn instantiate_path_args<'tcx>( ty: Ty, ) -> Ty { // No generic arguments (`Wrapper`) is an empty list; parenthesized args keep `ty`. - let syn_args: Vec<&syn::GenericArgument> = - match path.segments.last().map(|seg| &seg.arguments) { - Some(syn::PathArguments::AngleBracketed(args)) => args.args.iter().collect(), - Some(syn::PathArguments::None) => Vec::new(), - _ => return ty, - }; + let syn_args: Vec<&syn::GenericArgument> = match path.segments.last().map(|seg| &seg.arguments) + { + Some(syn::PathArguments::AngleBracketed(args)) => args.args.iter().collect(), + Some(syn::PathArguments::None) => Vec::new(), + _ => return ty, + }; let TyKind::RigidTy(RigidTy::Adt(adt_def, identity_args)) = ty.kind() else { return ty; };