From 39d9fe494d2ceb62d9d43631ea5456766b7f5fbf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 09:21:49 +0200 Subject: [PATCH 1/6] Avoid a panic when retrieving attributes --- frontend/exporter/src/types/new/full_def.rs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index a24e9b357..b060de84a 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -53,7 +53,7 @@ impl<'tcx, S: BaseState<'tcx>> SInto> for RDefId { span: tcx.def_span(def_id).sinto(s), source_span: source_span.sinto(s), source_text, - attributes: tcx.get_attrs_unchecked(def_id).sinto(s), + attributes: get_def_attrs(tcx, def_id).sinto(s), visibility: get_def_visibility(tcx, def_id), lang_item: s .base() @@ -424,6 +424,17 @@ fn get_def_visibility<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> Option(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> &'tcx [rustc_ast::ast::Attribute] { + use rustc_hir::def::DefKind::*; + match tcx.def_kind(def_id) { + // These kinds cause `get_attrs_unchecked` to panic. + ConstParam | LifetimeParam | TyParam => &[], + _ => tcx.get_attrs_unchecked(def_id), + } +} + /// This normalizes trait clauses before calling `sinto` on them. This is a bit of a hack required /// by charon for now. We can't normalize all clauses as this would lose region information in /// outlives clauses. From f7e01ae58a62cf9d2aaa0244cac219d33f40f6f0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 14:29:24 +0200 Subject: [PATCH 2/6] Ignore nested obligations when resolving local clauses --- frontend/exporter/src/traits/resolution.rs | 31 +++++++++++----------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 342025f6f..4a50a002e 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -338,27 +338,28 @@ impl<'tcx> PredicateSearcher<'tcx> { let nested = match &impl_source { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { nested, .. })) => { - nested.as_slice() + // The nested obligations of depth 1 correspond (we hope) to the predicates on the + // relevant impl that need to be satisfied. + nested + .iter() + .filter(|obligation| obligation.recursion_depth == 1) + .filter_map(|obligation| { + obligation.predicate.as_trait_clause().map(|trait_ref| { + self.resolve(&trait_ref.map_bound(|p| p.trait_ref), warn) + }) + }) + .collect::>()? } - Ok(ImplSource::Param(nested)) => nested.as_slice(), + // Nested obligations can happen e.g. for GATs. We ignore these as we resolve local + // clauses ourselves. + Ok(ImplSource::Param(_)) => vec![], // We ignore the contained obligations here. For example for `(): Send`, the // obligations contained would be `[(): Send]`, which leads to an infinite loop. There // might be important obligations here in other cases; we'll have to see if that comes // up. - Ok(ImplSource::Builtin(_, _ignored)) => &[], - Err(_) => &[], + Ok(ImplSource::Builtin(..)) => vec![], + Err(_) => vec![], }; - let nested = nested - .iter() - // Only keep depth-1 obligations to avoid duplicate impl exprs. - .filter(|obligation| obligation.recursion_depth == 1) - .filter_map(|obligation| { - obligation - .predicate - .as_trait_clause() - .map(|trait_ref| self.resolve(&trait_ref.map_bound(|p| p.trait_ref), warn)) - }) - .collect::>()?; Ok(ImplExpr { r#impl: atom, From 114519c0574a131df6042fb40919849eef93df87 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 15:29:03 +0200 Subject: [PATCH 3/6] Track GAT information in trait resolution --- frontend/exporter/src/traits.rs | 16 ++++- frontend/exporter/src/traits/resolution.rs | 68 +++++++++++++++++----- 2 files changed, 68 insertions(+), 16 deletions(-) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 80ceb27fb..0799cad29 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -17,17 +17,29 @@ pub use resolution::PredicateSearcher; pub enum ImplExprPathChunk { AssocItem { item: AssocItem, + /// The arguments provided to the item (for GATs). + generic_args: Vec, + /// The impl exprs that must be satisfied to apply the given arguments to the item. E.g. + /// `T: Clone` in the following example: + /// ```ignore + /// trait Foo { + /// type Type: Debug; + /// } + /// ``` + impl_exprs: Vec, + /// The implemented predicate. predicate: Binder, #[value(<_ as SInto<_, Clause>>::sinto(predicate, s).id)] predicate_id: PredicateId, - /// The nth predicate returned by `tcx.item_bounds`. + /// The index of this predicate in the list returned by `tcx.item_bounds`. index: usize, }, Parent { + /// The implemented predicate. predicate: Binder, #[value(<_ as SInto<_, Clause>>::sinto(predicate, s).id)] predicate_id: PredicateId, - /// The nth predicate returned by `tcx.predicates_of`. + /// The index of this predicate in the list returned by `tcx.predicates_of`. index: usize, }, } diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 4a50a002e..725044b64 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -14,13 +14,25 @@ use crate::traits::utils::erase_and_norm; pub enum PathChunk<'tcx> { AssocItem { item: AssocItem, + /// The arguments provided to the item (for GATs). + generic_args: &'tcx [GenericArg<'tcx>], + /// The impl exprs that must be satisfied to apply the given arguments to the item. E.g. + /// `T: Clone` in the following example: + /// ```ignore + /// trait Foo { + /// type Type: Debug; + /// } + /// ``` + impl_exprs: Vec>, + /// The implemented predicate. predicate: PolyTraitPredicate<'tcx>, - /// The nth predicate returned by `tcx.item_bounds`. + /// The index of this predicate in the list returned by `tcx.item_bounds`. index: usize, }, Parent { + /// The implemented predicate. predicate: PolyTraitPredicate<'tcx>, - /// The nth predicate returned by `tcx.predicates_of`. + /// The index of this predicate in the list returned by `tcx.predicates_of`. index: usize, }, } @@ -213,20 +225,27 @@ impl<'tcx> PredicateSearcher<'tcx> { } /// If the type is a trait associated type, we add any relevant bounds to our context. - fn add_associated_type_refs(&mut self, ty: Binder<'tcx, Ty<'tcx>>) { + fn add_associated_type_refs( + &mut self, + ty: Binder<'tcx, Ty<'tcx>>, + // Call back into hax-related code to display a nice warning. + warn: &impl Fn(&str), + ) -> Result<(), String> { let tcx = self.tcx; // Note: We skip a binder but rebind it just after. let TyKind::Alias(AliasTyKind::Projection, alias_ty) = ty.skip_binder().kind() else { - return; + return Ok(()); }; - let trait_ref = ty.rebind(alias_ty.trait_ref(tcx)).upcast(tcx); + let (trait_ref, item_args) = alias_ty.trait_ref_and_own_args(tcx); + let trait_ref = ty.rebind(trait_ref).upcast(tcx); // The predicate we're looking for is is `::Type: OtherTrait`. We look up `T as // Trait` in the current context and add all the bounds on `Trait::Type` to our context. - let Some(trait_candidate) = self.lookup(trait_ref) else { - return; + let Some(trait_candidate) = self.resolve_local(trait_ref, warn)? else { + return Ok(()); }; + // The bounds that the associated type must validate. let item_bounds = tcx // TODO: `item_bounds` can contain parent traits, we don't want them .item_bounds(alias_ty.def_id) @@ -235,6 +254,16 @@ impl<'tcx> PredicateSearcher<'tcx> { .filter_map(|pred| pred.as_trait_clause()) .enumerate(); + // Resolve predicates required to mention the item. + let nested_impl_exprs: Vec<_> = tcx + .predicates_defined_on(alias_ty.def_id) + .predicates + .iter() + .filter_map(|(clause, _span)| clause.as_trait_clause()) + .map(|trait_pred| trait_pred.map_bound(|p| p.trait_ref)) + .map(|trait_ref| self.resolve(&trait_ref, warn)) + .collect::>()?; + // Add all the bounds on the corresponding associated item. self.extend(item_bounds.map(|(index, pred)| { let mut candidate = Candidate { @@ -244,26 +273,35 @@ impl<'tcx> PredicateSearcher<'tcx> { }; candidate.path.push(PathChunk::AssocItem { item: tcx.associated_item(alias_ty.def_id), + generic_args: item_args, + impl_exprs: nested_impl_exprs.clone(), predicate: pred, index, }); candidate })); + + Ok(()) } - /// Lookup a predicate in this set. If the predicate applies to an associated type, we - /// add the relevant implied associated type bounds to the set as well. - fn lookup(&mut self, target: PolyTraitPredicate<'tcx>) -> Option> { + /// Resolve a local clause by looking it up in this set. If the predicate applies to an + /// associated type, we add the relevant implied associated type bounds to the set as well. + fn resolve_local( + &mut self, + target: PolyTraitPredicate<'tcx>, + // Call back into hax-related code to display a nice warning. + warn: &impl Fn(&str), + ) -> Result>, String> { tracing::trace!("Looking for {target:?}"); // Look up the predicate let ret = self.candidates.get(&target).cloned(); if ret.is_some() { - return ret; + return Ok(ret); } // Add clauses related to associated type in the `Self` type of the predicate. - self.add_associated_type_refs(target.self_ty()); + self.add_associated_type_refs(target.self_ty(), warn)?; let ret = self.candidates.get(&target).cloned(); if ret.is_none() { @@ -275,7 +313,7 @@ impl<'tcx> PredicateSearcher<'tcx> { .join("") ); } - ret + Ok(ret) } /// Resolve the given trait reference in the local context. @@ -304,7 +342,9 @@ impl<'tcx> PredicateSearcher<'tcx> { def_id: impl_def_id, generics, }, - Ok(ImplSource::Param(_)) => match self.lookup(erased_tref.upcast(self.tcx)) { + Ok(ImplSource::Param(_)) => match self + .resolve_local(erased_tref.upcast(self.tcx), warn)? + { Some(candidate) => { let path = candidate.path; let r#trait = candidate.origin.clause.to_poly_trait_ref(); From 1c87998b12027f5018ea4f8205556f432ea43f71 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 17:24:33 +0200 Subject: [PATCH 4/6] Support non-tuple constant references --- frontend/exporter/src/constant_utils.rs | 46 +++++++++++++++++-------- 1 file changed, 31 insertions(+), 15 deletions(-) diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index 7005b7eb8..99cc977a3 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -581,27 +581,43 @@ mod rustc { .s_unwrap(s); // Iterate over the fields, which should be values - assert!(dc.variant.is_none()); - - // The type should be tuple - let hax_ty: Ty = ty.sinto(s); - match hax_ty.kind() { - TyKind::Tuple(_) => (), - _ => { - fatal!(s[span], "Expected the type to be tuple: {:?}", val) - } - }; - // Below: we are mutually recursive with [const_value_to_constant_expr], // which takes a [Const] as input, but it should be // ok because we call it on a strictly smaller value. - let fields: Vec = dc + let fields = dc .fields .iter() .copied() - .map(|(val, ty)| const_value_to_constant_expr(s, ty, val, span)) - .collect(); - (ConstantExprKind::Tuple { fields }).decorate(hax_ty, span.sinto(s)) + .map(|(val, ty)| const_value_to_constant_expr(s, ty, val, span)); + + // The type should be tuple + let hax_ty: Ty = ty.sinto(s); + match ty.kind() { + ty::TyKind::Tuple(_) => { + assert!(dc.variant.is_none()); + let fields = fields.collect(); + ConstantExprKind::Tuple { fields } + } + ty::TyKind::Adt(adt_def, ..) => { + let variant = dc.variant.unwrap_or(rustc_target::abi::FIRST_VARIANT); + let variants_info = get_variant_information(adt_def, variant, s); + let fields = fields + .zip(&adt_def.variant(variant).fields) + .map(|(value, field)| ConstantFieldExpr { + field: field.did.sinto(s), + value, + }) + .collect(); + ConstantExprKind::Adt { + info: variants_info, + fields, + } + } + _ => { + fatal!(s[span], "Expected the type to be tuple or adt: {:?}", val) + } + } + .decorate(hax_ty, span.sinto(s)) } pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( From 4d5abb0d234b8022f5faea176365958424ffe05f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 17:25:12 +0200 Subject: [PATCH 5/6] Support non-tuple ZSTs --- frontend/exporter/src/constant_utils.rs | 36 ++++++++++++++----------- 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index 99cc977a3..bb1a81463 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -649,26 +649,30 @@ mod rustc { ConstValue::ZeroSized { .. } => { // Should be unit let hty: Ty = ty.sinto(s); - let cv = match hty.kind() { - TyKind::Tuple(tys) if tys.is_empty() => { + let cv = match ty.kind() { + ty::TyKind::Tuple(tys) if tys.is_empty() => { ConstantExprKind::Tuple { fields: Vec::new() } } - TyKind::Arrow(_) => match ty.kind() { - rustc_middle::ty::TyKind::FnDef(def_id, args) => { - let (def_id, generics, generics_impls, method_impl) = - get_function_from_def_id_and_generics(s, *def_id, args); - - ConstantExprKind::FnPtr { - def_id, - generics, - generics_impls, - method_impl, - } + ty::TyKind::FnDef(def_id, args) => { + let (def_id, generics, generics_impls, method_impl) = + get_function_from_def_id_and_generics(s, *def_id, args); + + ConstantExprKind::FnPtr { + def_id, + generics, + generics_impls, + method_impl, } - kind => { - fatal!(s[span], "Unexpected:"; {kind}) + } + ty::TyKind::Adt(adt_def, ..) => { + assert_eq!(adt_def.variants().len(), 1); + let variant = rustc_target::abi::FIRST_VARIANT; + let variants_info = get_variant_information(adt_def, variant, s); + ConstantExprKind::Adt { + info: variants_info, + fields: vec![], } - }, + } _ => { fatal!( s[span], From c134d50283bd040a03fd076221a40c5211c1717e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 17:48:53 +0200 Subject: [PATCH 6/6] Reveal the underlying types of `impl Trait` opaque types --- engine/lib/import_thir.ml | 2 +- frontend/exporter/src/types/copied.rs | 23 ++++++++++++++++------- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index eb44d8c51..27870ae89 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1019,7 +1019,7 @@ end) : EXPR = struct let impl = c_impl_expr span impl_expr in let item = Concrete_ident.of_def_id (AssociatedItem Type) def_id in TAssociatedType { impl; item } - | Alias { kind = Opaque; def_id; _ } -> + | Alias { kind = Opaque _; def_id; _ } -> TOpaque (Concrete_ident.of_def_id Type def_id) | Alias { kind = Inherent; _ } -> assertion_failure [ span ] "Ty::Alias with AliasTyKind::Inherent" diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 8054f6fe9..0344024d1 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1766,7 +1766,10 @@ pub enum AliasKind { /// An associated type in an inherent impl. Inherent, /// An `impl Trait` opaque type. - Opaque, + Opaque { + /// The real type hidden inside this opaque type. + hidden_ty: Ty, + }, /// A type alias that references opaque types. Likely to always be normalized away. Weak, } @@ -1778,11 +1781,11 @@ impl Alias { s: &S, alias_kind: &rustc_type_ir::AliasTyKind, alias_ty: &rustc_middle::ty::AliasTy<'tcx>, - ) -> Self { + ) -> TyKind { + let tcx = s.base().tcx; use rustc_type_ir::AliasTyKind as RustAliasKind; let kind = match alias_kind { RustAliasKind::Projection => { - let tcx = s.base().tcx; let trait_ref = alias_ty.trait_ref(tcx); // In a case like: // ``` @@ -1803,14 +1806,20 @@ impl Alias { } } RustAliasKind::Inherent => AliasKind::Inherent, - RustAliasKind::Opaque => AliasKind::Opaque, + RustAliasKind::Opaque => { + // Reveal the underlying `impl Trait` type. + let ty = tcx.type_of(alias_ty.def_id).instantiate(tcx, alias_ty.args); + AliasKind::Opaque { + hidden_ty: ty.sinto(s), + } + } RustAliasKind::Weak => AliasKind::Weak, }; - Alias { + TyKind::Alias(Alias { kind, args: alias_ty.args.sinto(s), def_id: alias_ty.def_id.sinto(s), - } + }) } } @@ -1903,7 +1912,7 @@ pub enum TyKind { Tuple(Vec), #[custom_arm( rustc_middle::ty::TyKind::Alias(alias_kind, alias_ty) => { - TyKind::Alias(Alias::from(state, alias_kind, alias_ty)) + Alias::from(state, alias_kind, alias_ty) }, )] Alias(Alias),