diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 870b03846f9..369a6c1c99f 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -465,6 +465,60 @@ pub enum CtorReturn { ResultOf, } +/// Build a generic-argument list for the associated item that matches its full generics +/// (impl parameters + own parameters) positionally: lifetimes (which may appear anywhere, +/// e.g. first on lifetime-parameterized impls like `impl<'h> Searcher<'h>`, or as the +/// item's own early-bound lifetime like `AtomicU8::from_ptr<'a>`) get erased regions, and +/// type/const slots are filled from `adt_args` in order. Returns None if `adt_args` does +/// not fit the non-lifetime slots -- kind mismatches must be prevented up front because +/// rustc's instantiation panics on them rather than returning an error. +fn ctor_args_with_lifetimes( + tcx: TyCtxt, + item: rustc_span::def_id::DefId, + adt_args: &GenericArgs, +) -> Option { + // Collect the full parameter list: parent (impl) generics first, then the item's own. + let mut chain = vec![tcx.generics_of(item)]; + while let Some(parent) = chain.last().unwrap().parent { + chain.push(tcx.generics_of(parent)); + } + let mut supplied = adt_args.0.iter().filter(|a| !matches!(a, GenericArgKind::Lifetime(_))); + let mut args = vec![]; + for g in chain.iter().rev() { + for p in &g.own_params { + match p.kind { + rustc_middle::ty::GenericParamDefKind::Lifetime => { + args.push(GenericArgKind::Lifetime(rustc_public::ty::Region { + kind: rustc_public::ty::RegionKind::ReErased, + })); + } + rustc_middle::ty::GenericParamDefKind::Type { .. } => match supplied.next() { + Some(a @ GenericArgKind::Type(_)) => args.push(a.clone()), + _ => return None, + }, + rustc_middle::ty::GenericParamDefKind::Const { .. } => match supplied.next() { + Some(a @ GenericArgKind::Const(_)) => args.push(a.clone()), + _ => return None, + }, + } + } + } + // All supplied non-lifetime arguments must have been consumed. + if supplied.next().is_some() { + return None; + } + Some(GenericArgs(args)) +} + +/// True if the (stable) type still carries escaping late-bound regions, e.g. an argument +/// like `BorrowedFd<'_>` read from a skipped fn-sig binder. Such types must not reach +/// trait-solver queries (rustc panics wrapping them in a dummy binder) and are not +/// generatable anyway. +fn has_escaping_bound_vars(tcx: TyCtxt, ty: Ty) -> bool { + use rustc_middle::ty::TypeVisitableExt; + rustc_internal::internal(tcx, ty).has_escaping_bound_vars() +} + /// Search `ty`'s inherent impls for an assert-guarded *representation constructor*: an /// associated function returning `Self` directly whose preconditions are stated as /// (debug_)asserts rather than validated returns — typically `unsafe`, doc-hidden or @@ -503,7 +557,10 @@ pub fn find_unchecked_constructor( // constructor with the ADT's own generic arguments: for inherent impls whose // parameters mirror the type's, this is the correct substitution; when it is // not, resolution fails and the constructor is skipped. - let Ok(instance) = Instance::resolve(ctor_def, adt_args) else { + let Some(ctor_args) = ctor_args_with_lifetimes(tcx, item, adt_args) else { + continue; + }; + let Ok(instance) = Instance::resolve(ctor_def, &ctor_args) else { continue; }; if !instance.has_body() { @@ -524,10 +581,10 @@ pub fn find_unchecked_constructor( continue; } if fn_sig.inputs().is_empty() - || !fn_sig - .inputs() - .iter() - .all(|input| implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache)) + || !fn_sig.inputs().iter().all(|input| { + !has_escaping_bound_vars(tcx, *input) + && implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache) + }) { continue; } @@ -626,14 +683,16 @@ pub fn find_arbitrary_constructor( // Every constructor argument must be plainly generatable (implements or derives // Arbitrary); constructor arguments do not get the argument-position extensions // (slices, smart pointers, nested constructors) in phase 1. - if !fn_sig - .inputs() - .iter() - .all(|input| implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache)) - { + if !fn_sig.inputs().iter().all(|input| { + !has_escaping_bound_vars(tcx, *input) + && implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache) + }) { continue; } - let Ok(instance) = Instance::resolve(ctor_def, &GenericArgs(vec![])) else { + let Some(ctor_args) = ctor_args_with_lifetimes(tcx, item, &GenericArgs(vec![])) else { + continue; + }; + let Ok(instance) = Instance::resolve(ctor_def, &ctor_args) else { continue; }; if !instance.has_body() { diff --git a/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected index 21108e3051f..8c2f9cd08f2 100644 --- a/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected @@ -5,8 +5,14 @@ | cargo_autoharness_constructor | Day::ordinal0 | #[kani::proof] | Failure | | cargo_autoharness_constructor | Even::half | #[kani::proof] | Failure | | cargo_autoharness_constructor | Even::try_new | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter2::level | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter2::zero | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter::from_ref | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter::level | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter::new | #[kani::proof] | Success | | cargo_autoharness_constructor | Ranged::new_unchecked | #[kani::proof] | Failure | | cargo_autoharness_constructor | Wrapper::from_raw_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | use_tagged | #[kani::proof] | Success | | cargo_autoharness_constructor | wrapped_ordinal0 | #[kani::proof] | Failure | === with flag === Note: harnesses marked "(ctor)" generate some values through one of a type's own constructors (--constructor-args); @@ -16,6 +22,12 @@ Note: harnesses marked "(ctor)" generate some values through one of a type's own | cargo_autoharness_constructor | Day::ordinal0 | #[kani::proof] (ctor) | Success | | cargo_autoharness_constructor | Even::half | #[kani::proof] (ctor) | Success | | cargo_autoharness_constructor | Even::try_new | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter2::level | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter2::zero | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter::from_ref | #[kani::proof] | Success | +| cargo_autoharness_constructor | Meter::level | #[kani::proof] (ctor) | Success | +| cargo_autoharness_constructor | Meter::new | #[kani::proof] | Success | | cargo_autoharness_constructor | Ranged::new_unchecked | #[kani::proof] | Failure | | cargo_autoharness_constructor | Wrapper::from_raw_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | use_tagged | #[kani::proof] | Success | | cargo_autoharness_constructor | wrapped_ordinal0 | #[kani::proof] (ctor) | Success | diff --git a/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs index b228bac1014..0a0c4e843ac 100644 --- a/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs @@ -81,3 +81,59 @@ pub fn wrapped_ordinal0(w: Wrapper) -> u16 { assert!(w.inner.value >= 1, "invariant violated"); w.inner.value - 1 } + +// REGRESSION (brotli/sharded-slab sweep ICE): a constructor with its own early-bound +// lifetime (AtomicU8::from_ptr-style) must not break discovery for the type: it gets +// erased-lifetime args (and is skipped here in favor of `new`, which scores more args). +pub struct Meter { + level: u8, +} +impl Meter { + pub fn new(level: u8, cap: u8) -> Meter { + Meter { level: level.min(cap) } + } + pub fn from_ref<'a>(r: &'a u8) -> Meter { + Meter { level: *r } + } + pub fn level(&self) -> u8 { + self.level + } +} + +// REGRESSION (regex-automata sweep ICE): impl with its own lifetime parameter FIRST and +// the ADT generic over types; argument construction must be positional against the full +// parent+own generics, not append lifetimes at the end. +pub struct Tagged { + v: T, + tag: u16, +} +impl<'h, T: Copy> Tagged { + pub fn build(v: T, tag: u16) -> Tagged { + Tagged { v, tag } + } + pub fn peek(&self, _probe: &'h u8) -> u16 { + self.tag + } +} +pub fn use_tagged(t: Tagged) -> u32 { + if t.tag > 0 { t.v } else { 0 } +} + +// REGRESSION (async-io/js-sys/quinn-udp/wasm-bindgen sweep ICE): a candidate constructor +// whose argument carries an escaping late-bound region inside an ADT (BorrowedFd-style) +// must be rejected without panicking the trait solver. +pub struct Borrowed<'a>(pub &'a u32); +pub struct Meter2 { + level: u32, +} +impl Meter2 { + pub fn from_borrowed(b: Borrowed<'_>, bump: u32) -> Meter2 { + Meter2 { level: *b.0 + bump } + } + pub fn zero() -> Meter2 { + Meter2 { level: 0 } + } + pub fn level(&self) -> u32 { + self.level + } +}