From de508db8aa554da3d26a2d6d3b07d7a2e4c6eebf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 16 Jul 2024 11:47:49 +0200 Subject: [PATCH] Lift clauses on associated types to be clauses on the whole trait --- charon-ml/src/GAst.ml | 4 +- charon-ml/src/GAstOfJson.ml | 10 +- charon-ml/src/PrintGAst.ml | 22 +-- charon-ml/src/PrintTypes.ml | 4 - charon-ml/src/Types.ml | 2 - charon/src/ast/gast.rs | 9 +- charon/src/ast/krate.rs | 11 +- charon/src/ast/types.rs | 7 +- charon/src/ast/types_utils.rs | 1 + charon/src/bin/charon-driver/driver.rs | 2 + .../bin/generate-ml/GAstOfJson.template.ml | 126 ++++++++++++++++++ charon/src/bin/generate-ml/main.rs | 2 +- charon/src/ids/vector.rs | 44 +++++- charon/src/pretty/fmt_with_ctx.rs | 18 ++- charon/src/transform/check_generics.rs | 13 +- .../transform/lift_associated_item_clauses.rs | 63 +++++++++ charon/src/transform/mod.rs | 4 + charon/tests/crate_data.rs | 33 ++--- charon/tests/ui/arrays.out | 6 +- charon/tests/ui/associated-types.out | 8 +- charon/tests/ui/external.out | 9 +- charon/tests/ui/issue-118-generic-copy.out | 5 +- .../tests/ui/issue-4-slice-try-into-array.out | 4 +- charon/tests/ui/issue-4-traits.out | 4 +- charon/tests/ui/issue-45-misc.out | 21 +-- .../ui/issue-94-recursive-trait-defns.out | 13 +- charon/tests/ui/loops.out | 25 ++-- charon/tests/ui/name-matcher-tests.out | 4 +- charon/tests/ui/no_nested_borrows.out | 2 +- charon/tests/ui/polonius_map.out | 8 +- charon/tests/ui/trait-instance-id.out | 32 ++--- charon/tests/ui/traits.out | 25 ++-- charon/tests/ui/traits_special.out | 2 +- charon/tests/ui/type_alias.out | 6 +- 34 files changed, 391 insertions(+), 158 deletions(-) create mode 100644 charon/src/transform/lift_associated_item_clauses.rs diff --git a/charon-ml/src/GAst.ml b/charon-ml/src/GAst.ml index 34a06be6d..514bd9ed1 100644 --- a/charon-ml/src/GAst.ml +++ b/charon-ml/src/GAst.ml @@ -159,7 +159,7 @@ type trait_decl = { generics : generic_params; parent_clauses : trait_clause list; consts : (trait_item_name * (ty * global_decl_id option)) list; - types : (trait_item_name * (trait_clause list * ty option)) list; + types : (trait_item_name * ty option) list; required_methods : (trait_item_name * fun_decl_id) list; provided_methods : (trait_item_name * fun_decl_id option) list; } @@ -172,7 +172,7 @@ type trait_impl = { generics : generic_params; parent_trait_refs : trait_ref list; consts : (trait_item_name * (ty * global_decl_id)) list; - types : (trait_item_name * (trait_ref list * ty)) list; + types : (trait_item_name * ty) list; required_methods : (trait_item_name * fun_decl_id) list; provided_methods : (trait_item_name * fun_decl_id) list; } diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index 9b27488f8..fd52f2ac8 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -459,12 +459,6 @@ and trait_instance_id_of_json (js : json) : (trait_instance_id, string) result = let* x1 = trait_decl_id_of_json x1 in let* x2 = trait_clause_id_of_json x2 in Ok (ParentClause (x0, x1, x2)) - | `Assoc [ ("ItemClause", `List [ x0; x1; x2; x3 ]) ] -> - let* x0 = trait_instance_id_of_json x0 in - let* x1 = trait_decl_id_of_json x1 in - let* x2 = trait_item_name_of_json x2 in - let* x3 = trait_clause_id_of_json x3 in - Ok (ItemClause (x0, x1, x2, x3)) | `String "SelfId" -> Ok Self | `Assoc [ ("BuiltinOrAuto", builtin_or_auto) ] -> let* builtin_or_auto = trait_decl_ref_of_json builtin_or_auto in @@ -1241,6 +1235,7 @@ let gglobal_decl_of_json (bodies : 'body gexpr_body option list) Ok global | _ -> Error "") +(* Defined by hand because we discard the empty list of item clauses *) and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) : (trait_decl, string) result = combine_error_msgs js __FUNCTION__ @@ -1279,6 +1274,7 @@ and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) : (option_of_json ty_of_json))) types in + let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in let* required_methods = list_of_json (pair_of_json trait_item_name_of_json fun_decl_id_of_json) @@ -1303,6 +1299,7 @@ and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) : } | _ -> Error "") +(* Defined by hand because we discard the empty list of item clauses *) and trait_impl_of_json (id_to_file : id_to_file_map) (js : json) : (trait_impl, string) result = combine_error_msgs js __FUNCTION__ @@ -1339,6 +1336,7 @@ and trait_impl_of_json (id_to_file : id_to_file_map) (js : json) : (pair_of_json (list_of_json trait_ref_of_json) ty_of_json)) types in + let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in let* required_methods = list_of_json (pair_of_json trait_item_name_of_json fun_decl_id_of_json) diff --git a/charon-ml/src/PrintGAst.ml b/charon-ml/src/PrintGAst.ml index 2a588dec6..eb271c80e 100644 --- a/charon-ml/src/PrintGAst.ml +++ b/charon-ml/src/PrintGAst.ml @@ -176,14 +176,10 @@ let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string) in let types = List.map - (fun (name, (clauses, opt_ty)) -> - let clauses = List.map (trait_clause_to_string env) clauses in - let clauses = clauses_to_string indent1 indent_incr 0 clauses in + (fun (name, opt_ty) -> match opt_ty with - | None -> indent1 ^ "type " ^ name ^ clauses ^ "\n" - | Some ty -> - indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ clauses - ^ "\n") + | None -> indent1 ^ "type " ^ name ^ "\n" + | Some ty -> indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ "\n") def.types in let required_methods = @@ -261,16 +257,8 @@ let trait_impl_to_string (env : ('a, 'b) fmt_env) (indent : string) in let types = List.map - (fun (name, (trait_refs, ty)) -> - let trait_refs = - if trait_refs <> [] then - " where [" - ^ String.concat ", " - (List.map (trait_ref_to_string env) trait_refs) - ^ "]" - else "" - in - indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ trait_refs ^ "\n") + (fun (name, ty) -> + indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ "\n") def.types in let env_method (name, f) = diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 44dd4e2ac..c1627df6b 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -230,10 +230,6 @@ and trait_instance_id_to_string (env : ('a, 'b) fmt_env) let inst_id = trait_instance_id_to_string env inst_id in let clause_id = trait_clause_id_to_string env clause_id in "parent(" ^ inst_id ^ ")::" ^ clause_id - | ItemClause (inst_id, _decl_id, item_name, clause_id) -> - let inst_id = trait_instance_id_to_string env inst_id in - let clause_id = trait_clause_id_to_string env clause_id in - "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]" | FnPointer ty -> "fn_ptr(" ^ ty_to_string env ty ^ ")" | Closure (fid, generics) -> "closure(" diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 1ff4c5bb0..925eed5fa 100644 --- a/charon-ml/src/Types.ml +++ b/charon-ml/src/Types.ml @@ -318,8 +318,6 @@ and trait_instance_id = | BuiltinOrAuto of trait_decl_ref | Clause of trait_clause_id | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id - | ItemClause of - trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id | FnPointer of ty | Closure of fun_decl_id * generic_args | Dyn of trait_decl_ref diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 0662149e9..61107ffb7 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -238,7 +238,10 @@ pub struct TraitDecl { /// /// The optional id is for the default value. pub consts: Vec<(TraitItemName, (Ty, Option))>, - /// The associated types declared in the trait. + /// The associated types declared in the trait. The `Vector` is a list of trait clauses that + /// apply to this item. This is used during translation, but the `lift_associated_item_clauses` + /// pass moves them to be parent clauses later. Hence this is empty after that pass. + /// TODO: Do this as we translate to avoid the need to store this vector. pub types: Vec<( TraitItemName, (Vector, Option), @@ -287,7 +290,9 @@ pub struct TraitImpl { pub parent_trait_refs: Vector, /// The associated constants declared in the trait. pub consts: Vec<(TraitItemName, (Ty, GlobalDeclId))>, - /// The associated types declared in the trait. + /// The associated types declared in the trait. The `Vec` corresponds to the same `Vector` in + /// `TraitDecl.types`. In the same way, this is empty after the `lift_associated_item_clauses` + /// pass. pub types: Vec<(TraitItemName, (Vec, Ty))>, /// The implemented required methods pub required_methods: Vec<(TraitItemName, FunDeclId)>, diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 5b9e796e8..ce3710f19 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -78,22 +78,29 @@ pub enum AnyTransItem<'ctx> { } /// The data of a translated crate. -#[derive(Default)] +#[derive(Default, Drive, DriveMut)] pub struct TranslatedCrate { /// The name of the crate. pub crate_name: String, /// File names to ids and vice-versa + #[drive(skip)] pub file_to_id: HashMap, + #[drive(skip)] pub id_to_file: HashMap, + #[drive(skip)] pub real_file_counter: Generator, + #[drive(skip)] pub virtual_file_counter: Generator, /// All the ids, in the order in which we encountered them + #[drive(skip)] pub all_ids: LinkedHashSet, /// The map from rustc id to translated id. + #[drive(skip)] pub id_map: HashMap, /// The reverse map of ids. + #[drive(skip)] pub reverse_id_map: HashMap, /// The translated type definitions @@ -109,6 +116,7 @@ pub struct TranslatedCrate { /// The translated trait declarations pub trait_impls: Vector, /// The re-ordered groups of declarations, initialized as empty. + #[drive(skip)] pub ordered_decls: Option, } @@ -126,7 +134,6 @@ impl TranslatedCrate { pub fn all_items(&self) -> impl Iterator> { self.all_items_with_ids().map(|(_, item)| item) } - pub fn all_items_with_ids(&self) -> impl Iterator)> { self.all_ids .iter() diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index d4bfae5c7..8deead393 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -177,8 +177,8 @@ pub enum TraitRefKind { /// ``` ParentClause(Box, TraitDeclId, TraitClauseId), - /// A clause bound in a trait item (typically a trait clause in an - /// associated type). + /// A clause defined on an associated type. This variant is only used during translation; after + /// the `lift_associated_item_clauses` pass, clauses on items become `ParentClause`s. /// /// Remark: the [TraitDeclId] gives the trait declaration which is /// implemented by the trait implementation from which we take the item @@ -202,8 +202,7 @@ pub enum TraitRefKind { /// local clause 0 implements Foo /// } /// ``` - /// - /// + #[charon::opaque] ItemClause(Box, TraitDeclId, TraitItemName, TraitClauseId), /// Self, in case of trait declarations/implementations. diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index f7bf0dfc3..fa6a637c9 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -103,6 +103,7 @@ impl GenericArgs { } /// Check whether this matches the given `GenericParams`. + /// TODO: check more things, e.g. that the trait refs use the correct trait and generics. pub fn matches(&self, params: &GenericParams) -> bool { params.regions.len() == self.regions.len() && params.types.len() == self.types.len() diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index a105966b7..d12a044df 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -251,6 +251,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa // Run the micro-passes that clean up bodies. for pass in ULLBC_PASSES.iter() { + trace!("# Starting pass {}", pass.name()); pass.transform_ctx(&mut ctx) } @@ -269,6 +270,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa // Run the micro-passes that clean up bodies. for pass in LLBC_PASSES.iter() { + trace!("# Starting pass {}", pass.name()); pass.transform_ctx(&mut ctx) } diff --git a/charon/src/bin/generate-ml/GAstOfJson.template.ml b/charon/src/bin/generate-ml/GAstOfJson.template.ml index 200b6936c..fd3076487 100644 --- a/charon/src/bin/generate-ml/GAstOfJson.template.ml +++ b/charon/src/bin/generate-ml/GAstOfJson.template.ml @@ -261,6 +261,132 @@ let gglobal_decl_of_json (bodies : 'body gexpr_body option list) Ok global | _ -> Error "") +(* Defined by hand because we discard the empty list of item clauses *) +and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) : + (trait_decl, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc + [ + ("def_id", def_id); + ("item_meta", item_meta); + ("generics", generics); + ("parent_clauses", parent_clauses); + ("consts", consts); + ("types", types); + ("required_methods", required_methods); + ("provided_methods", provided_methods); + ] -> + let* def_id = trait_decl_id_of_json def_id in + let* item_meta = item_meta_of_json id_to_file item_meta in + let* generics = generic_params_of_json id_to_file generics in + let* parent_clauses = + vector_of_json trait_clause_id_of_json + (trait_clause_of_json id_to_file) + parent_clauses + in + let* consts = + list_of_json + (pair_of_json trait_item_name_of_json + (pair_of_json ty_of_json (option_of_json global_decl_id_of_json))) + consts + in + let* types = + list_of_json + (pair_of_json trait_item_name_of_json + (pair_of_json + (vector_of_json trait_clause_id_of_json + (trait_clause_of_json id_to_file)) + (option_of_json ty_of_json))) + types + in + let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in + let* required_methods = + list_of_json + (pair_of_json trait_item_name_of_json fun_decl_id_of_json) + required_methods + in + let* provided_methods = + list_of_json + (pair_of_json trait_item_name_of_json + (option_of_json fun_decl_id_of_json)) + provided_methods + in + Ok + { + def_id; + item_meta; + generics; + parent_clauses; + consts; + types; + required_methods; + provided_methods; + } + | _ -> Error "") + +(* Defined by hand because we discard the empty list of item clauses *) +and trait_impl_of_json (id_to_file : id_to_file_map) (js : json) : + (trait_impl, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc + [ + ("def_id", def_id); + ("item_meta", item_meta); + ("impl_trait", impl_trait); + ("generics", generics); + ("parent_trait_refs", parent_trait_refs); + ("consts", consts); + ("types", types); + ("required_methods", required_methods); + ("provided_methods", provided_methods); + ] -> + let* def_id = trait_impl_id_of_json def_id in + let* item_meta = item_meta_of_json id_to_file item_meta in + let* impl_trait = trait_decl_ref_of_json impl_trait in + let* generics = generic_params_of_json id_to_file generics in + let* parent_trait_refs = + vector_of_json trait_clause_id_of_json trait_ref_of_json + parent_trait_refs + in + let* consts = + list_of_json + (pair_of_json trait_item_name_of_json + (pair_of_json ty_of_json global_decl_id_of_json)) + consts + in + let* types = + list_of_json + (pair_of_json trait_item_name_of_json + (pair_of_json (list_of_json trait_ref_of_json) ty_of_json)) + types + in + let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in + let* required_methods = + list_of_json + (pair_of_json trait_item_name_of_json fun_decl_id_of_json) + required_methods + in + let* provided_methods = + list_of_json + (pair_of_json trait_item_name_of_json fun_decl_id_of_json) + provided_methods + in + Ok + { + def_id; + item_meta; + impl_trait; + generics; + parent_trait_refs; + consts; + types; + required_methods; + provided_methods; + } + | _ -> Error "") + (* __REPLACE5__ *) let type_declaration_group_of_json (js : json) : diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 94b999e7f..1b9c5c226 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -451,7 +451,7 @@ fn main() -> Result<()> { "GExprBody", "ItemKind", ], - &["TraitDecl", "TraitImpl", "GDeclarationGroup"], + &["GDeclarationGroup"], ]; let template_path = dir.join("GAstOfJson.template.ml"); let mut template = fs::read_to_string(&template_path) diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs index 8daf4f198..2666e7d35 100644 --- a/charon/src/ids/vector.rs +++ b/charon/src/ids/vector.rs @@ -17,7 +17,7 @@ use std::{ /// Indexed vector. /// To prevent accidental id reuse, the vector supports reserving a slot to be filled later. -#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Vector where I: Idx, @@ -25,6 +25,15 @@ where vector: IndexVec>, } +impl std::fmt::Debug for Vector +where + I: Idx, +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + as std::fmt::Debug>::fmt(&self.vector, f) + } +} + pub struct ReservedSlot(I); impl Vector @@ -86,6 +95,39 @@ where id } + /// Map each entry to a new one, keeping the same ids. + pub fn map(self, mut f: impl FnMut(T) -> U) -> Vector { + Vector { + vector: self + .vector + .into_iter() + .map(|x_opt| x_opt.map(&mut f)) + .collect(), + } + } + + /// Map each entry to a new one, keeping the same ids. + pub fn map_ref<'a, U>(&'a self, mut f: impl FnMut(&'a T) -> U) -> Vector { + Vector { + vector: self + .vector + .iter() + .map(|x_opt| x_opt.as_ref().map(&mut f)) + .collect(), + } + } + + /// Map each entry to a new one, keeping the same ids. + pub fn map_ref_mut<'a, U>(&'a mut self, mut f: impl FnMut(&'a mut T) -> U) -> Vector { + Vector { + vector: self + .vector + .iter_mut() + .map(|x_opt| x_opt.as_mut().map(&mut f)) + .collect(), + } + } + /// Iter over the nonempty slots. pub fn iter(&self) -> impl Iterator + Clone { self.vector.iter().flat_map(|opt| opt.as_ref()) diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 2d3988787..984f8ecf9 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -1176,15 +1176,19 @@ impl FmtWithCtx for TraitImpl { ) })) .chain(self.types.iter().map(|(name, (trait_refs, ty))| { - let trait_refs = trait_refs - .iter() - .map(|x| x.fmt_with_ctx(ctx)) - .collect::>() - .join(", "); + let trait_refs = if trait_refs.is_empty() { + "" + } else { + let trait_refs = trait_refs + .iter() + .map(|x| x.fmt_with_ctx(ctx)) + .collect::>() + .join(", "); + &format!(" with [{trait_refs}]") + }; format!( - "{TAB_INCR}type {name} = {} with [{}]\n", + "{TAB_INCR}type {name} = {}{trait_refs}\n", ty.fmt_with_ctx(ctx), - trait_refs ) })) .chain( diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 4f4b9a45b..db6a9be85 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -43,8 +43,11 @@ impl CheckGenericsVisitor<'_, '_> { fn generics_should_match_item(&mut self, args: &GenericArgs, item_id: impl Into) { self.discharged_one_generics(); if let Some(item) = self.translated.get_item(item_id.into()) { - if !args.matches(item.generic_params()) { - self.error("Mismatched generics!") + let params = item.generic_params(); + if !args.matches(params) { + self.error(format!( + "Mismatched generics:\nexpected: {params:?}\n got: {args:?}" + )) } } } @@ -141,6 +144,12 @@ impl CheckGenericsVisitor<'_, '_> { let args_match = timpl.parent_trait_refs.len() == tdecl.parent_clauses.len() && timpl.types.len() == tdecl.types.len() && timpl.consts.len() == tdecl.consts.len(); + let args_match = args_match + && tdecl.types.iter().zip(timpl.types.iter()).all( + |((dname, (dclauses, _)), (iname, (irefs, _)))| { + dname == iname && dclauses.len() == irefs.len() + }, + ); if !args_match { self.error("The generics supplied by the trait impl don't match the trait decl.") } diff --git a/charon/src/transform/lift_associated_item_clauses.rs b/charon/src/transform/lift_associated_item_clauses.rs new file mode 100644 index 000000000..af5f1ce69 --- /dev/null +++ b/charon/src/transform/lift_associated_item_clauses.rs @@ -0,0 +1,63 @@ +//! Move clauses on associated types to be parent clauses. The distinction is not semantically +//! meaningful. We should ideally to this directly when translating but this is currently +//! difficult; instead we do this as a post-processing pass. +use std::collections::HashMap; +use std::mem; + +use derive_visitor::{visitor_enter_fn_mut, DriveMut}; + +use crate::{ast::*, ids::Vector}; + +use super::{ctx::UllbcPass, TransformCtx}; + +pub struct Transform; +impl UllbcPass for Transform { + fn transform_ctx(&self, ctx: &mut TransformCtx<'_>) { + // For each trait, we move the item-local clauses to be top-level parent clauses, and + // record the mapping from the old to the new ids. + let trait_item_clause_ids: Vector< + TraitDeclId, + HashMap>, + > = ctx.translated.trait_decls.map_ref_mut(|decl| { + decl.types + .iter_mut() + .map(|(name, (clauses, _))| { + let id_map = mem::take(clauses).map(|mut clause| { + decl.parent_clauses.push_with(|id| { + clause.clause_id = id; + clause + }) + }); + (name.clone(), id_map) + }) + .collect() + }); + + // Move the item-local trait refs to match what we did in the trait declarations. + for timpl in ctx.translated.trait_impls.iter_mut() { + for (_, (refs, _)) in timpl.types.iter_mut() { + for trait_ref in mem::take(refs) { + // Note: this assumes that we listed the types in the same order as in the trait + // decl, which we do. + timpl.parent_trait_refs.push(trait_ref); + } + } + } + + // Update trait refs. + ctx.translated + .drive_mut(&mut visitor_enter_fn_mut(|trkind: &mut TraitRefKind| { + use TraitRefKind::*; + if let ItemClause(..) = trkind { + take_mut::take(trkind, |trkind| { + let ItemClause(trait_ref, trait_decl, item_name, item_clause_id) = trkind + else { + unreachable!() + }; + let new_id = trait_item_clause_ids[trait_decl][&item_name][item_clause_id]; + ParentClause(trait_ref, trait_decl, new_id) + }) + } + })); + } +} diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 12a28f530..5e1e48367 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -11,6 +11,8 @@ pub mod inline_local_panic_functions; #[charon::opaque] pub mod insert_assign_return_unit; #[charon::opaque] +pub mod lift_associated_item_clauses; +#[charon::opaque] pub mod ops_to_function_calls; #[charon::opaque] pub mod reconstruct_asserts; @@ -37,6 +39,8 @@ pub mod update_closure_signatures; pub use ctx::TransformCtx; pub static ULLBC_PASSES: &[&dyn ctx::UllbcPass] = &[ + // Move clauses on associated types to be parent clauses + &lift_associated_item_clauses::Transform, // # Micro-pass: Remove overflow/div-by-zero/bounds checks since they are already part of the // arithmetic/array operation in the semantics of (U)LLBC. // **WARNING**: this pass uses the fact that the dynamic checks introduced by Rustc use a diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs index 1dae1df7c..30493c347 100644 --- a/charon/tests/crate_data.rs +++ b/charon/tests/crate_data.rs @@ -247,22 +247,22 @@ fn predicate_origins() -> Result<(), Box> { } ", )?; - let expected_function_clause_origins: Vec<(&str, &[_])> = vec![ + let expected_function_clause_origins: Vec<(&str, Vec<_>)> = vec![ ( "test_crate::top_level_function", - &[(WhereClauseOnFn, "Clone"), (WhereClauseOnFn, "Default")], + vec![(WhereClauseOnFn, "Clone"), (WhereClauseOnFn, "Default")], ), ( "test_crate::Struct", - &[(WhereClauseOnType, "Clone"), (WhereClauseOnType, "Default")], + vec![(WhereClauseOnType, "Clone"), (WhereClauseOnType, "Default")], ), ( "test_crate::TypeAlias", - &[(WhereClauseOnType, "Clone"), (WhereClauseOnType, "Default")], + vec![(WhereClauseOnType, "Clone"), (WhereClauseOnType, "Default")], ), ( "test_crate::::inherent_method", - &[ + vec![ (WhereClauseOnImpl, "Clone"), (WhereClauseOnImpl, "Default"), (WhereClauseOnFn, "From"), @@ -271,24 +271,25 @@ fn predicate_origins() -> Result<(), Box> { ), ( "test_crate::Trait", - &[ + vec![ (WhereClauseOnTrait, "Clone"), (WhereClauseOnTrait, "Copy"), (WhereClauseOnTrait, "Default"), + (TraitItem(TraitItemName("AssocType".to_owned())), "Default"), ], ), // Interesting note: the method definition does not mention the clauses on the trait. ( "test_crate::Trait::trait_method", - &[(WhereClauseOnFn, "From"), (WhereClauseOnFn, "From")], + vec![(WhereClauseOnFn, "From"), (WhereClauseOnFn, "From")], ), ( "test_crate::", - &[(WhereClauseOnImpl, "Copy"), (WhereClauseOnImpl, "Default")], + vec![(WhereClauseOnImpl, "Copy"), (WhereClauseOnImpl, "Default")], ), ( "test_crate::::trait_method", - &[ + vec![ (WhereClauseOnImpl, "Copy"), (WhereClauseOnImpl, "Default"), (WhereClauseOnFn, "From"), @@ -310,21 +311,11 @@ fn predicate_origins() -> Result<(), Box> { assert_eq!(origins.len(), clauses.len(), "failed for {item_name}"); for (clause, (expected_origin, expected_trait_name)) in clauses.iter().zip(origins) { let trait_name = trait_name(&crate_data, clause.trait_.trait_id); - assert_eq!(trait_name, *expected_trait_name, "failed for {item_name}"); - assert_eq!(&clause.origin, expected_origin, "failed for {item_name}"); + assert_eq!(trait_name, expected_trait_name, "failed for {item_name}"); + assert_eq!(&clause.origin, &expected_origin, "failed for {item_name}"); } } - let my_trait = items_by_name - .get("test_crate::Trait") - .unwrap() - .kind - .as_trait_decl(); - let item_clauses = &(my_trait.types[0].1).0; - assert_eq!( - item_clauses[0].origin, - TraitItem(TraitItemName("AssocType".into())) - ); Ok(()) } diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 10ab6c6f2..365af0c07 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -249,7 +249,7 @@ impl core::slice::index::{impl core::ops::index::Index for Slice}>, { - type Output = @TraitClause0::Output with [] + type Output = @TraitClause0::Output fn index = core::slice::index::{impl core::ops::index::Index for Slice}::index } @@ -270,7 +270,7 @@ fn core::slice::index::{impl core::slice::index::SliceIndex> for core:: impl core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range#4} : core::slice::index::SliceIndex, Slice> { parent_clause0 = core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for core::ops::range::Range#1} - type Output = Slice with [] + type Output = Slice fn get = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range#4}::get fn get_mut = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range#4}::get_mut fn get_unchecked = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range#4}::get_unchecked @@ -399,7 +399,7 @@ impl core::array::{impl core::ops::index::Index for Ar where [@TraitClause0]: core::ops::index::Index, I>, { - type Output = @TraitClause0::Output with [] + type Output = @TraitClause0::Output fn index = core::array::{impl core::ops::index::Index for Array#15}::index } diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out index 260c0a657..063c1e021 100644 --- a/charon/tests/ui/associated-types.out +++ b/charon/tests/ui/associated-types.out @@ -16,9 +16,8 @@ where Self::Item : 'a, { parent_clause_0 : [@TraitClause0]: core::marker::Copy + parent_clause_1 : [@TraitClause1]: core::clone::Clone type Item - where - [@TraitClause0]: core::clone::Clone, fn use_item : test_crate::Foo::use_item } @@ -60,7 +59,8 @@ where impl<'a, T> test_crate::{impl test_crate::Foo<'a> for &'a (T)}<'a, T> : test_crate::Foo<'a, &'a (T)> { parent_clause0 = core::marker::{impl core::marker::Copy for &'_0 (T)#4}<'_, T> - type Item = core::option::Option<&'a (T)> with [core::option::{impl core::clone::Clone for core::option::Option#5}<&'_ (T)>[core::clone::impls::{impl core::clone::Clone for &'_0 (T)#3}<'_, T>]] + parent_clause1 = core::option::{impl core::clone::Clone for core::option::Option#5}<&'_ (T)>[core::clone::impls::{impl core::clone::Clone for &'_0 (T)#3}<'_, T>] + type Item = core::option::Option<&'a (T)> } fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self @@ -74,7 +74,7 @@ where let @2: &'_ (@TraitClause0::Item); // anonymous local @2 := &x@1 - @0 := (@TraitClause0::Item::[@TraitClause0])::clone(move (@2)) + @0 := (parents(@TraitClause0)::[@TraitClause1])::clone(move (@2)) drop @2 drop x@1 return diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out index a23d750f9..8972334b9 100644 --- a/charon/tests/ui/external.out +++ b/charon/tests/ui/external.out @@ -36,10 +36,9 @@ trait core::num::nonzero::ZeroablePrimitive { parent_clause_0 : [@TraitClause0]: core::marker::Copy parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + parent_clause_2 : [@TraitClause2]: core::marker::Copy + parent_clause_3 : [@TraitClause3]: core::clone::Clone type NonZeroInner - where - [@TraitClause0]: core::marker::Copy, - [@TraitClause1]: core::clone::Clone, } opaque type core::num::nonzero::NonZero @@ -78,7 +77,9 @@ impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for u32#20} { parent_clause0 = core::marker::{impl core::marker::Copy for u32#41} parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for u32#19} - type NonZeroInner = core::num::nonzero::private::NonZeroU32Inner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroU32Inner#12}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner#11}] + parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroU32Inner#12} + parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner#11} + type NonZeroInner = core::num::nonzero::private::NonZeroU32Inner } enum core::option::Option = diff --git a/charon/tests/ui/issue-118-generic-copy.out b/charon/tests/ui/issue-118-generic-copy.out index e89da9195..da7911464 100644 --- a/charon/tests/ui/issue-118-generic-copy.out +++ b/charon/tests/ui/issue-118-generic-copy.out @@ -76,10 +76,9 @@ where trait test_crate::Trait { + parent_clause_0 : [@TraitClause0]: core::marker::Copy + parent_clause_1 : [@TraitClause1]: core::clone::Clone type Ty - where - [@TraitClause0]: core::marker::Copy, - [@TraitClause1]: core::clone::Clone, } fn test_crate::copy_assoc_ty(@1: @TraitClause0::Ty) diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out index 247a805d8..51fbfc024 100644 --- a/charon/tests/ui/issue-4-slice-try-into-array.out +++ b/charon/tests/ui/issue-4-slice-try-into-array.out @@ -28,7 +28,7 @@ impl core::convert::{impl core::convert::TryInto for T#6} : core: where [@TraitClause0]: core::convert::TryFrom, { - type Error = @TraitClause0::Error with [] + type Error = @TraitClause0::Error fn try_into = core::convert::{impl core::convert::TryInto for T#6}::try_into } @@ -52,7 +52,7 @@ impl<'_0, T, const N : usize> core::array::{impl core::convert::TryFrom<&'_0 (Sl where [@TraitClause0]: core::marker::Copy, { - type Error = core::array::TryFromSliceError with [] + type Error = core::array::TryFromSliceError fn try_from = core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array#7}::try_from } diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index 247a805d8..51fbfc024 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -28,7 +28,7 @@ impl core::convert::{impl core::convert::TryInto for T#6} : core: where [@TraitClause0]: core::convert::TryFrom, { - type Error = @TraitClause0::Error with [] + type Error = @TraitClause0::Error fn try_into = core::convert::{impl core::convert::TryInto for T#6}::try_into } @@ -52,7 +52,7 @@ impl<'_0, T, const N : usize> core::array::{impl core::convert::TryFrom<&'_0 (Sl where [@TraitClause0]: core::marker::Copy, { - type Error = core::array::TryFromSliceError with [] + type Error = core::array::TryFromSliceError fn try_from = core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array#7}::try_from } diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 5a11b1f09..9f040d64b 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -145,12 +145,11 @@ trait core::iter::traits::iterator::Iterator trait core::iter::traits::collect::IntoIterator where - (Self::IntoIter::[@TraitClause0])::Item = Self::Item, + (parents(Self)::[@TraitClause0])::Item = Self::Item, { + parent_clause_0 : [@TraitClause0]: core::iter::traits::iterator::Iterator type Item type IntoIter - where - [@TraitClause0]: core::iter::traits::iterator::Iterator, fn into_iter : core::iter::traits::collect::IntoIterator::into_iter } @@ -163,8 +162,9 @@ impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIter where [@TraitClause0]: core::iter::traits::iterator::Iterator, { - type Item = @TraitClause0::Item with [] - type IntoIter = I with [@TraitClause0] + parent_clause0 = @TraitClause0 + type Item = @TraitClause0::Item + type IntoIter = I fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter } @@ -285,10 +285,9 @@ trait core::num::nonzero::ZeroablePrimitive { parent_clause_0 : [@TraitClause0]: core::marker::Copy parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + parent_clause_2 : [@TraitClause2]: core::marker::Copy + parent_clause_3 : [@TraitClause3]: core::clone::Clone type NonZeroInner - where - [@TraitClause0]: core::marker::Copy, - [@TraitClause1]: core::clone::Clone, } opaque type core::num::nonzero::NonZero @@ -327,7 +326,9 @@ impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize#2 { parent_clause0 = core::marker::{impl core::marker::Copy for usize#38} parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} - type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}] + parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27} + parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} + type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner } fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero> @@ -352,7 +353,7 @@ impl core::iter::range::{impl core::iter::traits::iterator::Iterator for core where [@TraitClause0]: core::iter::range::Step, { - type Item = A with [] + type Item = A fn next = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::next fn size_hint = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::size_hint fn count = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::count diff --git a/charon/tests/ui/issue-94-recursive-trait-defns.out b/charon/tests/ui/issue-94-recursive-trait-defns.out index 21bb7bf0f..33b971617 100644 --- a/charon/tests/ui/issue-94-recursive-trait-defns.out +++ b/charon/tests/ui/issue-94-recursive-trait-defns.out @@ -2,10 +2,9 @@ trait test_crate::Trait1 { + parent_clause_0 : [@TraitClause0]: test_crate::Trait2 + parent_clause_1 : [@TraitClause1]: test_crate::Trait1 type T - where - [@TraitClause0]: test_crate::Trait2, - [@TraitClause1]: test_crate::Trait1, } trait test_crate::Trait2 @@ -25,17 +24,15 @@ trait test_crate::T2 trait test_crate::T3 { + parent_clause_0 : [@TraitClause0]: test_crate::T5 type T - where - [@TraitClause0]: test_crate::T5, } trait test_crate::T5 { + parent_clause_0 : [@TraitClause0]: test_crate::T4 + parent_clause_1 : [@TraitClause1]: test_crate::T3 type T - where - [@TraitClause0]: test_crate::T4, - [@TraitClause1]: test_crate::T3, } trait test_crate::T4 diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index 6bbf7dab6..944e024a0 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -874,12 +874,11 @@ trait core::iter::traits::iterator::Iterator trait core::iter::traits::collect::IntoIterator where - (Self::IntoIter::[@TraitClause0])::Item = Self::Item, + (parents(Self)::[@TraitClause0])::Item = Self::Item, { + parent_clause_0 : [@TraitClause0]: core::iter::traits::iterator::Iterator type Item type IntoIter - where - [@TraitClause0]: core::iter::traits::iterator::Iterator, fn into_iter : core::iter::traits::collect::IntoIterator::into_iter } @@ -892,8 +891,9 @@ impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIter where [@TraitClause0]: core::iter::traits::iterator::Iterator, { - type Item = @TraitClause0::Item with [] - type IntoIter = I with [@TraitClause0] + parent_clause0 = @TraitClause0 + type Item = @TraitClause0::Item + type IntoIter = I fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter } @@ -1014,10 +1014,9 @@ trait core::num::nonzero::ZeroablePrimitive { parent_clause_0 : [@TraitClause0]: core::marker::Copy parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + parent_clause_2 : [@TraitClause2]: core::marker::Copy + parent_clause_3 : [@TraitClause3]: core::clone::Clone type NonZeroInner - where - [@TraitClause0]: core::marker::Copy, - [@TraitClause1]: core::clone::Clone, } opaque type core::num::nonzero::NonZero @@ -1056,7 +1055,9 @@ impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize#2 { parent_clause0 = core::marker::{impl core::marker::Copy for usize#38} parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} - type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}] + parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27} + parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} + type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner } fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero> @@ -1081,7 +1082,7 @@ impl core::iter::range::{impl core::iter::traits::iterator::Iterator for core where [@TraitClause0]: core::iter::range::Step, { - type Item = A with [] + type Item = A fn next = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::next fn size_hint = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::size_hint fn count = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::count @@ -1671,7 +1672,7 @@ impl alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec>, { - type Output = @TraitClause0::Output with [] + type Output = @TraitClause0::Output fn index = alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#13}::index } @@ -1705,7 +1706,7 @@ fn core::slice::index::{impl core::slice::index::SliceIndex> for usize# impl core::slice::index::{impl core::slice::index::SliceIndex> for usize#2} : core::slice::index::SliceIndex> { parent_clause0 = core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for usize} - type Output = T with [] + type Output = T fn get = core::slice::index::{impl core::slice::index::SliceIndex> for usize#2}::get fn get_mut = core::slice::index::{impl core::slice::index::SliceIndex> for usize#2}::get_mut fn get_unchecked = core::slice::index::{impl core::slice::index::SliceIndex> for usize#2}::get_unchecked diff --git a/charon/tests/ui/name-matcher-tests.out b/charon/tests/ui/name-matcher-tests.out index a16dfefc7..303c9908c 100644 --- a/charon/tests/ui/name-matcher-tests.out +++ b/charon/tests/ui/name-matcher-tests.out @@ -89,7 +89,7 @@ impl core::slice::index::{impl core::ops::index::Index for Slice}>, { - type Output = @TraitClause0::Output with [] + type Output = @TraitClause0::Output fn index = core::slice::index::{impl core::ops::index::Index for Slice}::index } @@ -110,7 +110,7 @@ fn core::slice::index::{impl core::slice::index::SliceIndex> for core:: impl core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::RangeFrom#6} : core::slice::index::SliceIndex, Slice> { parent_clause0 = core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for core::ops::range::RangeFrom#3} - type Output = Slice with [] + type Output = Slice fn get = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::RangeFrom#6}::get fn get_mut = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::RangeFrom#6}::get_mut fn get_unchecked = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::RangeFrom#6}::get_unchecked diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out index 237fc40ea..e9611159b 100644 --- a/charon/tests/ui/no_nested_borrows.out +++ b/charon/tests/ui/no_nested_borrows.out @@ -268,7 +268,7 @@ fn alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box#38}::der impl alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box#38} : core::ops::deref::Deref> { - type Target = T with [] + type Target = T fn deref = alloc::boxed::{impl core::ops::deref::Deref for alloc::boxed::Box#38}::deref } diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index 3f53caad1..e7579bd5c 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -49,9 +49,8 @@ trait core::hash::Hash trait core::hash::BuildHasher { + parent_clause_0 : [@TraitClause0]: core::hash::Hasher type Hasher - where - [@TraitClause0]: core::hash::Hasher, fn build_hasher : core::hash::BuildHasher::build_hasher fn hash_one } @@ -125,7 +124,8 @@ fn std::hash::random::{impl core::hash::BuildHasher for std::hash::random::Rando impl std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1} : core::hash::BuildHasher { - type Hasher = std::hash::random::DefaultHasher with [std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher#4}] + parent_clause0 = std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher#4} + type Hasher = std::hash::random::DefaultHasher fn build_hasher = std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1}::build_hasher } @@ -160,7 +160,7 @@ where [@TraitClause4]: core::hash::Hash, [@TraitClause5]: core::hash::BuildHasher, { - type Output = V with [] + type Output = V fn index = std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap#9}::index } diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out index a468c58e9..158e20db0 100644 --- a/charon/tests/ui/trait-instance-id.out +++ b/charon/tests/ui/trait-instance-id.out @@ -116,12 +116,11 @@ trait core::iter::traits::iterator::Iterator trait core::iter::traits::collect::IntoIterator where - (Self::IntoIter::[@TraitClause0])::Item = Self::Item, + (parents(Self)::[@TraitClause0])::Item = Self::Item, { + parent_clause_0 : [@TraitClause0]: core::iter::traits::iterator::Iterator type Item type IntoIter - where - [@TraitClause0]: core::iter::traits::iterator::Iterator, fn into_iter : core::iter::traits::collect::IntoIterator::into_iter } @@ -172,10 +171,9 @@ trait core::num::nonzero::ZeroablePrimitive { parent_clause_0 : [@TraitClause0]: core::marker::Copy parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + parent_clause_2 : [@TraitClause2]: core::marker::Copy + parent_clause_3 : [@TraitClause3]: core::clone::Clone type NonZeroInner - where - [@TraitClause0]: core::marker::Copy, - [@TraitClause1]: core::clone::Clone, } opaque type core::num::nonzero::NonZero @@ -214,7 +212,9 @@ impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize#2 { parent_clause0 = core::marker::{impl core::marker::Copy for usize#38} parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} - type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}] + parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27} + parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} + type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner } fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::advance_by<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero> @@ -223,7 +223,7 @@ unsafe fn core::array::iter::{impl core::iter::traits::iterator::Iterator for co impl core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2} : core::iter::traits::iterator::Iterator> { - type Item = T with [] + type Item = T fn next = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::next fn size_hint = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::size_hint fn fold = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::fold @@ -237,8 +237,9 @@ fn core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array< impl core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array} : core::iter::traits::collect::IntoIterator> { - type Item = T with [] - type IntoIter = core::array::iter::IntoIter with [core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}] + parent_clause0 = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2} + type Item = T + type IntoIter = core::array::iter::IntoIter fn into_iter = core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array}::into_iter } @@ -253,8 +254,9 @@ impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIter where [@TraitClause0]: core::iter::traits::iterator::Iterator, { - type Item = @TraitClause0::Item with [] - type IntoIter = I with [@TraitClause0] + parent_clause0 = @TraitClause0 + type Item = @TraitClause0::Item + type IntoIter = I fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter } @@ -337,7 +339,7 @@ Unknown decl: 44 impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}<'a, T> : core::iter::traits::iterator::Iterator> { - type Item = &'a (T) with [] + type Item = &'a (T) fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::next fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::size_hint fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::count @@ -386,7 +388,7 @@ unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for co impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}<'a, T> : core::iter::traits::iterator::Iterator> { - type Item = &'a (Slice) with [] + type Item = &'a (Slice) fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::next fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::size_hint fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::count @@ -411,7 +413,7 @@ unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for co impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}<'a, T> : core::iter::traits::iterator::Iterator> { - type Item = &'a (Slice) with [] + type Item = &'a (Slice) fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::next fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::size_hint fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::count diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index 4d30b7b16..b5af8dbb7 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -454,12 +454,11 @@ global test_crate::WithConstTy::LEN2 { trait test_crate::WithConstTy { + parent_clause_0 : [@TraitClause0]: test_crate::ToU64 const LEN1 : usize const LEN2 : usize = test_crate::WithConstTy::LEN2 type V type W - where - [@TraitClause0]: test_crate::ToU64, fn f : test_crate::WithConstTy::f } @@ -485,10 +484,11 @@ fn test_crate::{impl test_crate::WithConstTy<32 : usize> for bool#8}::f<'_0, '_1 impl test_crate::{impl test_crate::WithConstTy<32 : usize> for bool#8} : test_crate::WithConstTy { + parent_clause0 = test_crate::{impl test_crate::ToU64 for u64#2} const LEN1 : usize = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool#8}::LEN1 const LEN2 : usize = test_crate::WithConstTy::LEN2 - type V = u8 with [] - type W = u64 with [test_crate::{impl test_crate::ToU64 for u64#2}] + type V = u8 + type W = u64 fn f = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool#8}::f } @@ -526,7 +526,7 @@ where let @2: @TraitClause0::W; // anonymous local @2 := move (x@1) - @0 := (@TraitClause0::W::[@TraitClause0])::to_u64(move (@2)) + @0 := (parents(@TraitClause0)::[@TraitClause0])::to_u64(move (@2)) drop @2 drop x@1 return @@ -644,12 +644,11 @@ trait test_crate::Iterator trait test_crate::IntoIterator where - (Self::IntoIter::[@TraitClause0])::Item = Self::Item, + (parents(Self)::[@TraitClause0])::Item = Self::Item, { + parent_clause_0 : [@TraitClause0]: test_crate::Iterator type Item type IntoIter - where - [@TraitClause0]: test_crate::Iterator, fn into_iter : test_crate::IntoIterator::into_iter } @@ -668,9 +667,8 @@ trait test_crate::WithTarget trait test_crate::ParentTrait2 { + parent_clause_0 : [@TraitClause0]: test_crate::WithTarget type U - where - [@TraitClause0]: test_crate::WithTarget, } trait test_crate::ChildTrait2 @@ -681,12 +679,13 @@ trait test_crate::ChildTrait2 impl test_crate::{impl test_crate::WithTarget for u32#11} : test_crate::WithTarget { - type Target = u32 with [] + type Target = u32 } impl test_crate::{impl test_crate::ParentTrait2 for u32#12} : test_crate::ParentTrait2 { - type U = u32 with [test_crate::{impl test_crate::WithTarget for u32#11}] + parent_clause0 = test_crate::{impl test_crate::WithTarget for u32#11} + type U = u32 } fn test_crate::{impl test_crate::ChildTrait2 for u32#13}::convert(@1: u32) -> u32 @@ -837,7 +836,7 @@ fn test_crate::WithConstTy::f<'_0, '_1, Self, const LEN : usize>(@1: &'_0 mut (S fn test_crate::IntoIterator::into_iter(@1: Self) -> Self::IntoIter -fn test_crate::ChildTrait2::convert(@1: (parents(Self)::[@TraitClause0])::U) -> ((parents(Self)::[@TraitClause0])::U::[@TraitClause0])::Target +fn test_crate::ChildTrait2::convert(@1: (parents(Self)::[@TraitClause0])::U) -> (parents((parents(Self)::[@TraitClause0]))::[@TraitClause0])::Target fn test_crate::CFnOnce::call_once(@1: Self, @2: Args) -> Self::Output diff --git a/charon/tests/ui/traits_special.out b/charon/tests/ui/traits_special.out index 0f34ed4d9..5d3ed8667 100644 --- a/charon/tests/ui/traits_special.out +++ b/charon/tests/ui/traits_special.out @@ -25,7 +25,7 @@ fn test_crate::{impl test_crate::From<&'_0 (bool)> for bool}::from<'_0, '_1>(@1: impl<'_0> test_crate::{impl test_crate::From<&'_0 (bool)> for bool}<'_0> : test_crate::From { - type Error = () with [] + type Error = () fn from = test_crate::{impl test_crate::From<&'_0 (bool)> for bool}::from } diff --git a/charon/tests/ui/type_alias.out b/charon/tests/ui/type_alias.out index e35caf4f7..61a21f7ff 100644 --- a/charon/tests/ui/type_alias.out +++ b/charon/tests/ui/type_alias.out @@ -17,9 +17,8 @@ trait core::borrow::Borrow trait alloc::borrow::ToOwned { + parent_clause_0 : [@TraitClause0]: core::borrow::Borrow type Owned - where - [@TraitClause0]: core::borrow::Borrow, fn to_owned : alloc::borrow::ToOwned::to_owned fn clone_into } @@ -59,7 +58,8 @@ impl alloc::slice::{impl alloc::borrow::ToOwned for Slice#9} : alloc::b where [@TraitClause0]: core::clone::Clone, { - type Owned = alloc::vec::Vec with [alloc::slice::{impl core::borrow::Borrow> for alloc::vec::Vec#5}] + parent_clause0 = alloc::slice::{impl core::borrow::Borrow> for alloc::vec::Vec#5} + type Owned = alloc::vec::Vec fn to_owned = alloc::slice::{impl alloc::borrow::ToOwned for Slice#9}::to_owned fn clone_into = alloc::slice::{impl alloc::borrow::ToOwned for Slice#9}::clone_into }