From 108b4b71be5ae67740116ef6a9371dc8b001214e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 31 Oct 2024 15:55:05 +0100 Subject: [PATCH 1/2] Rework trait impl translation --- charon/Cargo.lock | 6 +- .../translate/translate_crate_to_ullbc.rs | 26 +-- .../charon-driver/translate/translate_ctx.rs | 16 +- .../translate/translate_traits.rs | 185 +++++------------- .../translate/translate_types.rs | 10 +- charon/tests/ui/generic-associated-types.out | 16 +- charon/tests/ui/non-lifetime-gats.out | 28 +-- 7 files changed, 72 insertions(+), 215 deletions(-) diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 0700722e..9083d57e 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -786,7 +786,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#d3313f9a7f928810cf1750e3f7702fdfdb9b011c" +source = "git+https://github.com/hacspec/hax?branch=main#fdb0664bf77153977a2fa8ac4ab3d96cbced92ce" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -797,7 +797,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#d3313f9a7f928810cf1750e3f7702fdfdb9b011c" +source = "git+https://github.com/hacspec/hax?branch=main#fdb0664bf77153977a2fa8ac4ab3d96cbced92ce" dependencies = [ "extension-traits", "hax-adt-into", @@ -814,7 +814,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#d3313f9a7f928810cf1750e3f7702fdfdb9b011c" +source = "git+https://github.com/hacspec/hax?branch=main#fdb0664bf77153977a2fa8ac4ab3d96cbced92ce" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index 9d397009..5bd66fdc 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs @@ -50,25 +50,19 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { FullDefKind::Trait { .. } => { let _ = self.register_trait_decl_id(&None, def_id); } - FullDefKind::Impl { - items, - impl_subject, - .. - } => match impl_subject { - hax::ImplSubject::Trait { .. } => { - let _ = self.register_trait_impl_id(&None, def_id); - } - hax::ImplSubject::Inherent { .. } => { - if explore_inside { - for (item, _) in items { - self.register_local_item((&item.def_id).into()); - } - } - } - }, + FullDefKind::TraitImpl { .. } => { + let _ = self.register_trait_impl_id(&None, def_id); + } // TODO: trait aliases (https://github.com/AeneasVerif/charon/issues/366) FullDefKind::TraitAlias { .. } => {} + FullDefKind::InherentImpl { items, .. } => { + if explore_inside { + for (_, item_def) in items { + self.register_local_item(item_def.rust_def_id()); + } + } + } FullDefKind::Mod { items, .. } => { // Explore the module, only if it was not marked as "opaque" // TODO: we may want to accumulate the set of modules we found, to check that all diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 5d8496a8..6b01eacd 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -346,15 +346,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } DefPathData::Impl => { let def = self.hax_def(def_id)?; - let hax::FullDefKind::Impl { impl_subject, .. } = &def.kind else { - unreachable!() - }; // Two cases, depending on whether the impl block is // a "regular" impl block (`impl Foo { ... }`) or a trait // implementation (`impl Bar for Foo { ... }`). - let impl_elem = match impl_subject { + let impl_elem = match def.kind() { // Inherent impl ("regular" impl) - hax::ImplSubject::Inherent(ty) => { + hax::FullDefKind::InherentImpl { ty, .. } => { let erase_regions = false; // We need to convert the type, which may contain quantified @@ -366,10 +363,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { ImplElem::Ty(generics, ty) } // Trait implementation - hax::ImplSubject::Trait { .. } => { + hax::FullDefKind::TraitImpl { .. } => { let impl_id = self.register_trait_impl_id(&None, def_id); ImplElem::Trait(impl_id) } + _ => unreachable!(), }; Some(PathElem::Impl(impl_elem, disambiguator)) @@ -883,11 +881,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // Register the corresponding trait early so we can filter on its name. { let def = self.hax_def(id).expect("hax failed when translating item"); - let hax::FullDefKind::Impl { - impl_subject: hax::ImplSubject::Trait { trait_pred, .. }, - .. - } = def.kind() - else { + let hax::FullDefKind::TraitImpl { trait_pred, .. } = def.kind() else { unreachable!() }; let trait_rust_id = (&trait_pred.trait_ref.def_id).into(); diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index 24bf31e8..dc22a4f2 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -191,29 +191,18 @@ impl BodyTransCtx<'_, '_, '_> { let generics = self.translate_def_generics(span, def)?; - let hax::FullDefKind::Impl { - impl_subject: - hax::ImplSubject::Trait { - trait_pred, - required_impl_exprs, - .. - }, + let hax::FullDefKind::TraitImpl { + trait_pred, + required_impl_exprs, items: impl_items, .. } = &def.kind else { unreachable!() }; - let implemented_trait_id = &trait_pred.trait_ref.def_id; - let trait_def = self.t_ctx.hax_def(implemented_trait_id)?; - let hax::FullDefKind::Trait { - items: decl_items, .. - } = trait_def.kind() - else { - unreachable!() - }; // Retrieve the information about the implemented trait. + let implemented_trait_id = &trait_pred.trait_ref.def_id; let trait_id = self.register_trait_decl_id(span, implemented_trait_id); let implemented_trait = { let implemented_trait = &trait_pred.trait_ref; @@ -244,53 +233,65 @@ impl BodyTransCtx<'_, '_, '_> { } // Explore the associated items - let tcx = self.t_ctx.tcx; - let mut consts = HashMap::new(); - let mut types: HashMap = HashMap::new(); + let mut consts = Vec::new(); + let mut types: Vec<(TraitItemName, Ty)> = Vec::new(); + let mut required_methods = Vec::new(); + let mut provided_methods = Vec::new(); let mut type_clauses = Vec::new(); - let mut methods = HashMap::new(); - for (item, item_def) in impl_items { - let name = TraitItemName(item.name.clone()); - let item_span = self.def_span(&item.def_id); + for impl_item in impl_items { + use hax::ImplAssocItemValue::*; + let name = TraitItemName(impl_item.name.clone()); + let item_def = impl_item.def(); // The impl item or the corresponding trait default. + let item_span = self.def_span(item_def.rust_def_id()); + let item_def_id = item_def.rust_def_id(); match item_def.kind() { hax::FullDefKind::AssocFn { .. } => { - let fun_id = self.register_fun_decl_id(item_span, &item.def_id); - methods.insert(name, fun_id); + let fun_id = self.register_fun_decl_id(item_span, item_def_id); + match &impl_item.value { + Provided { is_override, .. } => { + if *is_override { + provided_methods.push((name, fun_id)); + } else { + required_methods.push((name, fun_id)); + } + } + DefaultedFn { .. } => { + // TODO: handle defaulted methods + } + _ => unreachable!(), + } } hax::FullDefKind::AssocConst { .. } => { + let id = self.register_global_decl_id(item_span, item_def_id); // The parameters of the constant are the same as those of the item that // declares them. - let gref = GlobalDeclRef { - id: self.register_global_decl_id(item_span, &item.def_id), - generics: generics.identity_args(), + let generics = match &impl_item.value { + Provided { .. } => generics.identity_args(), + _ => implemented_trait.generics.clone(), }; - consts.insert(name, gref); + let gref = GlobalDeclRef { id, generics }; + consts.push((name, gref)); } hax::FullDefKind::AssocTy { generics, .. } if !generics.params.is_empty() => { - error_or_panic!( - self, - item_span, - &format!("Generic associated types are not supported") - ); + // We don't support GATs; the error was already reported in the trait declaration. } - hax::FullDefKind::AssocTy { - value: Some(ty), .. - } => { + hax::FullDefKind::AssocTy { value, .. } => { + let ty = match &impl_item.value { + Provided { .. } => value.as_ref().unwrap(), + DefaultedTy { ty, .. } => ty, + _ => unreachable!(), + }; let ty = self.translate_ty(item_span, erase_regions, &ty)?; - types.insert(name.clone(), ty); + types.push((name.clone(), ty)); - // Retrieve the trait refs - let hax::AssocItemContainer::TraitImplContainer { - required_impl_exprs, - .. - } = &item.container - else { - unreachable!() - }; // TODO: use clause ids let trait_refs = self - .translate_trait_impl_exprs(span, erase_regions, &required_impl_exprs)? + .translate_trait_impl_exprs( + item_span, + erase_regions, + &impl_item.required_impl_exprs, + )? .into_iter() .collect(); type_clauses.push((name, trait_refs)); @@ -299,98 +300,6 @@ impl BodyTransCtx<'_, '_, '_> { } } - // In case of a trait implementation, some values may not have been - // provided, in case the declaration provided default values. We - // check those, and lookup the relevant values. - let partial_consts = consts; - let partial_types = types; - let mut consts = Vec::new(); - let mut types: Vec<(TraitItemName, Ty)> = Vec::new(); - let mut required_methods = Vec::new(); - let mut provided_methods = Vec::new(); - - for (decl_item, decl_item_def) in decl_items { - let item_def_id = decl_item_def.rust_def_id(); - let item_span = self.translate_span_from_hax(&decl_item_def.span); - let name = TraitItemName(decl_item.name.to_string()); - match decl_item_def.kind() { - hax::FullDefKind::AssocFn { .. } => { - if let Some(&fun_id) = methods.get(&name) { - // Check if we implement a required method or reimplement a provided - // method. - if decl_item.has_value { - provided_methods.push((name, fun_id)); - } else { - required_methods.push((name, fun_id)); - } - } - } - - hax::FullDefKind::AssocConst { .. } => { - // Does the trait impl provide an implementation for this const? - let c = match partial_consts.get(&name) { - Some(c) => c.clone(), - None => { - // The item is not defined in the trait impl: the trait decl *must* - // define a default value. - // The parameters of the constant are the same as those of the item - // that declares them. - GlobalDeclRef { - id: self.register_global_decl_id(item_span, item_def_id), - generics: implemented_trait.generics.clone(), - } - } - }; - consts.push((name, c)); - } - hax::FullDefKind::AssocTy { generics, .. } if !generics.params.is_empty() => { - // The error was already reported in the trait declaration. - } - hax::FullDefKind::AssocTy { .. } => { - // Does the trait impl provide an implementation for this type? - match partial_types.get(&name) { - Some(ty) => types.push((name.clone(), ty.clone())), - None => { - let rust_implemented_trait_ref = - tcx.impl_trait_ref(rust_id).unwrap().instantiate_identity(); - let trait_args = rust_implemented_trait_ref.args; - - // The item is not defined in the trait impl: the trait decl *must* - // define a default value. - let ty = tcx.type_of(item_def_id).instantiate(tcx, trait_args); - let ty = self.t_ctx.catch_sinto(&self.hax_state, span, &ty)?; - let ty = self.translate_ty(item_span, erase_regions, &ty)?; - types.push((name.clone(), ty)); - - // Retrieve the trait refs - let impl_exprs = { - use hax::HasOwnerIdSetter; - use rustc_middle::ty::GenericArgs; - let item_args = GenericArgs::identity_for_item(tcx, item_def_id); - // Subtlety: we have to add the GAT arguments (if any) to the trait ref arguments. - let args = item_args.rebase_onto(tcx, rust_id, trait_args); - // Note: this is wrong for GATs! We need a param_env that has the - // arguments of the impl plus those of the associated type, but - // there's no def_id with that param_env. - let state_with_id = self.hax_state.clone().with_owner_id(rust_id); - let impl_exprs = hax::solve_item_implied_traits( - &state_with_id, - item_def_id, - args, - ); - impl_exprs - }; - let trait_refs = self - .translate_trait_impl_exprs(item_span, erase_regions, &impl_exprs)? - .into_iter() - .collect(); - type_clauses.push((name.clone(), trait_refs)); - } - } - } - _ => panic!("Unexpected definition for trait item: {decl_item_def:?}"), - } - } if item_meta.opacity.is_opaque() { let ctx = self.into_fmt(); self.t_ctx.errors.dcx.span_warn( diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 379bed1e..0467dd88 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -670,12 +670,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { self.push_generic_params(generics)?; // Add the self trait clause. match &def.kind { - FullDefKind::Impl { - impl_subject: - hax::ImplSubject::Trait { - trait_pred: self_predicate, - .. - }, + FullDefKind::TraitImpl { + trait_pred: self_predicate, .. } | FullDefKind::Trait { self_predicate, .. } => { @@ -700,7 +696,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { | FullDefKind::Static { .. } => { (PredicateOrigin::WhereClauseOnFn, PredicateLocation::Base) } - FullDefKind::Impl { .. } => { + FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => { (PredicateOrigin::WhereClauseOnImpl, PredicateLocation::Base) } // TODO: distinguish trait where clauses from trait supertraits. Currently we diff --git a/charon/tests/ui/generic-associated-types.out b/charon/tests/ui/generic-associated-types.out index a0604314..03b35b24 100644 --- a/charon/tests/ui/generic-associated-types.out +++ b/charon/tests/ui/generic-associated-types.out @@ -22,18 +22,6 @@ error: Ignoring the following item due to a previous error: test_crate::lifetime 45 | trait Bar<'a> { | ^^^^^^^^^^^^^ -error: Generic associated types are not supported - --> tests/ui/generic-associated-types.rs:13:5 - | -13 | type Item<'b> = &'b T; - | ^^^^^^^^^^^^^ - -error: Ignoring the following item due to a previous error: test_crate::{impl#0} - --> tests/ui/generic-associated-types.rs:12:1 - | -12 | impl<'a, T> LendingIterator for Option<&'a T> { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - error: Found unsupported GAT `Item` when resolving trait `core::marker::Sized<@TraitClause2::Item>` --> tests/ui/generic-associated-types.rs:27:28 | @@ -78,6 +66,6 @@ error: Error during trait resolution: Found unsupported GAT `Type` when resolvin 53 | x.foo() | ^^^^^^^ -error: aborting due to 12 previous errors; 1 warning emitted +error: aborting due to 10 previous errors; 1 warning emitted -ERROR Compilation encountered 12 errors +ERROR Compilation encountered 10 errors diff --git a/charon/tests/ui/non-lifetime-gats.out b/charon/tests/ui/non-lifetime-gats.out index f4b58288..35dccc85 100644 --- a/charon/tests/ui/non-lifetime-gats.out +++ b/charon/tests/ui/non-lifetime-gats.out @@ -22,30 +22,6 @@ error: Ignoring the following item due to a previous error: test_crate::moar_var 33 | trait Trait { | ^^^^^^^^^^^^^^ -error: Generic associated types are not supported - --> tests/ui/non-lifetime-gats.rs:13:5 - | -13 | type Pointer = Box; - | ^^^^^^^^^^^^^^^ - -error: Ignoring the following item due to a previous error: test_crate::{impl#0} - --> tests/ui/non-lifetime-gats.rs:12:1 - | -12 | impl PointerFamily for BoxFamily { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -error: Generic associated types are not supported - --> tests/ui/non-lifetime-gats.rs:39:9 - | -39 | type Type = (T, U); - | ^^^^^^^^^^^^ - -error: Ignoring the following item due to a previous error: test_crate::moar_variables::{impl#1} - --> tests/ui/non-lifetime-gats.rs:38:5 - | -38 | impl Trait> for Foo { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -error: aborting due to 8 previous errors +error: aborting due to 4 previous errors -ERROR Compilation encountered 8 errors +ERROR Compilation encountered 4 errors From d39e040916cf9caba70fdbfdf43dce5ec5e02d3b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 30 Oct 2024 17:12:42 +0100 Subject: [PATCH 2/2] Use a `Vector` for `TraitImpl.type_clauses` --- charon/src/ast/gast.rs | 2 +- .../charon-driver/translate/translate_traits.rs | 14 +++++--------- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 4b51f95b..5e8fcb39 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -294,7 +294,7 @@ pub struct TraitImpl { /// The `Vec` corresponds to the same `Vector` in `TraitDecl`. In the same way, this is /// empty after the `lift_associated_item_clauses` pass. #[charon::opaque] - pub type_clauses: Vec<(TraitItemName, Vec)>, + pub type_clauses: Vec<(TraitItemName, Vector)>, /// The implemented required methods pub required_methods: Vec<(TraitItemName, FunDeclId)>, /// The re-implemented provided methods diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index dc22a4f2..1035559c 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -285,15 +285,11 @@ impl BodyTransCtx<'_, '_, '_> { let ty = self.translate_ty(item_span, erase_regions, &ty)?; types.push((name.clone(), ty)); - // TODO: use clause ids - let trait_refs = self - .translate_trait_impl_exprs( - item_span, - erase_regions, - &impl_item.required_impl_exprs, - )? - .into_iter() - .collect(); + let trait_refs = self.translate_trait_impl_exprs( + item_span, + erase_regions, + &impl_item.required_impl_exprs, + )?; type_clauses.push((name, trait_refs)); } _ => panic!("Unexpected definition for trait item: {item_def:?}"),