From dcde15cec7ae6df3e8e9d8db1b1f3d5fd69c1049 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 7 Jan 2025 15:47:33 +0100 Subject: [PATCH] Make `Self` clause explicit in trait global declarations too Both for consistency fir the corresponding method generics and in case the default const uses values from `Self`. --- .../translate/translate_traits.rs | 30 ++++++++++++++----- .../translate/translate_types.rs | 5 ++-- charon/tests/crate_data.rs | 8 ++--- charon/tests/ui/assoc-const-with-generics.out | 9 ++++-- charon/tests/ui/traits.out | 9 ++++-- 5 files changed, 40 insertions(+), 21 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index a169d78a4..5da7620a9 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -138,10 +138,10 @@ impl BodyTransCtx<'_, '_> { // declares them. let id = self.register_global_decl_id(item_span, item_def_id); let generics_target = GenericsSource::item(id); - let gref = GlobalDeclRef { - id, - generics: self.the_only_binder().params.identity_args(generics_target), - }; + let mut generics = + self.the_only_binder().params.identity_args(generics_target); + generics.trait_refs.push(self_trait_ref.clone()); + let gref = GlobalDeclRef { id, generics }; const_defaults.insert(item_name.clone(), gref); }; let ty = self.translate_ty(item_span, ty)?; @@ -238,6 +238,16 @@ impl BodyTransCtx<'_, '_> { )?; TraitDeclRef { trait_id, generics } }; + // A `TraitRef` that points to this impl with the correct generics. + let self_predicate = TraitRef { + kind: TraitRefKind::TraitImpl( + def_id, + self.the_only_binder() + .params + .identity_args(GenericsSource::item(def_id)), + ), + trait_decl_ref: RegionBinder::empty(implemented_trait.clone()), + }; // The trait refs which implement the parent clauses of the implemented trait decl. let parent_trait_refs = self.translate_trait_impl_exprs(span, &required_impl_exprs)?; @@ -322,10 +332,14 @@ impl BodyTransCtx<'_, '_> { Provided { .. } => { self.the_only_binder().params.identity_args(generics_target) } - _ => implemented_trait - .generics - .clone() - .with_target(generics_target), + _ => { + let mut generics = implemented_trait + .generics + .clone() + .with_target(generics_target); + generics.trait_refs.push(self_predicate.clone()); + generics + } }; let gref = GlobalDeclRef { id, generics }; consts.push((name, gref)); diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 57e2d0ca1..e923eb946 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -593,9 +593,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { | Variant { .. } => { let parent_def_id = def.parent.as_ref().unwrap(); let parent_def = self.t_ctx.hax_def(parent_def_id)?; - let explicit_self_clause = matches!(def.kind(), AssocFn { .. }) - && matches!(parent_def.kind(), Trait { .. }); - // Add an explicit `Self` clause to trait method declarations. + // Add an explicit `Self` clause to trait item declarations. + let explicit_self_clause = matches!(parent_def.kind(), Trait { .. }); self.push_generics_for_def(span, &parent_def, true, explicit_self_clause)?; } _ => {} diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs index cbc7f7061..9a07fb900 100644 --- a/charon/tests/crate_data.rs +++ b/charon/tests/crate_data.rs @@ -612,14 +612,10 @@ fn declaration_groups() -> anyhow::Result<()> { "#, )?; - // There are two function ids registered, but only one is nonempty. `functions.len() == 2` as - // `len()` counts the empty slots too. - let decl_groups = crate_data.ordered_decls.unwrap(); + // There are two function items: one for `foo`, one for the initializer of `Trait::FOO`. assert_eq!(crate_data.fun_decls.iter().count(), 2); + let decl_groups = crate_data.ordered_decls.unwrap(); assert_eq!(decl_groups.len(), 5); - assert!(decl_groups - .iter() - .all(|group| group.to_mixed_group().is_non_rec())); Ok(()) } diff --git a/charon/tests/ui/assoc-const-with-generics.out b/charon/tests/ui/assoc-const-with-generics.out index 2ac607db1..8c11ebf4b 100644 --- a/charon/tests/ui/assoc-const-with-generics.out +++ b/charon/tests/ui/assoc-const-with-generics.out @@ -61,6 +61,8 @@ impl test_crate::{impl test_crate::HasLen for Array() -> usize +where + [@TraitClause0]: test_crate::HasDefaultLen, { let @0: usize; // return @@ -68,7 +70,10 @@ fn test_crate::HasDefaultLen::LEN() -> usize return } -global test_crate::HasDefaultLen::LEN: usize = test_crate::HasDefaultLen::LEN() +global test_crate::HasDefaultLen::LEN: usize + where + [@TraitClause0]: test_crate::HasDefaultLen, + = test_crate::HasDefaultLen::LEN() trait test_crate::HasDefaultLen { @@ -77,7 +82,7 @@ trait test_crate::HasDefaultLen impl test_crate::{impl test_crate::HasDefaultLen for Array<(), const N : usize>}#3 : test_crate::HasDefaultLen, const N : usize> { - const LEN = test_crate::HasDefaultLen::LEN, const N : usize> + const LEN = test_crate::HasDefaultLen::LEN, const N : usize>[test_crate::{impl test_crate::HasDefaultLen for Array<(), const N : usize>}#3] } fn test_crate::{impl test_crate::HasDefaultLen for Array}#4::LEN() -> usize diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index 91cd09ca1..06a1fdadd 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -488,6 +488,8 @@ where } fn test_crate::WithConstTy::LEN2() -> usize +where + [@TraitClause0]: test_crate::WithConstTy, { let @0: usize; // return @@ -495,7 +497,10 @@ fn test_crate::WithConstTy::LEN2() -> usize return } -global test_crate::WithConstTy::LEN2: usize = test_crate::WithConstTy::LEN2() +global test_crate::WithConstTy::LEN2: usize + where + [@TraitClause0]: test_crate::WithConstTy, + = test_crate::WithConstTy::LEN2() trait test_crate::WithConstTy { @@ -538,7 +543,7 @@ impl test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8 : test_cr parent_clause1 = test_crate::{impl test_crate::ToU64 for u64}#2 parent_clause2 = core::marker::Sized const LEN1 = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1 - const LEN2 = test_crate::WithConstTy::LEN2 + const LEN2 = test_crate::WithConstTy::LEN2[test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8] type V = u8 type W = u64 fn f<'_0, '_1> = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0_0, '_0_1>