diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 1ebe7b20..44bb89c0 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.63" +let supported_charon_version = "0.1.64" diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml index 0814facb..58f76d51 100644 --- a/charon-ml/src/generated/Generated_GAst.ml +++ b/charon-ml/src/generated/Generated_GAst.ml @@ -417,6 +417,8 @@ and cli_options = { (** Blacklist of items to keep opaque. These use the name-matcher syntax. *) exclude : string list; (** Blacklist of items to not translate at all. These use the name-matcher syntax. *) + remove_associated_types : string list; + (** List of traits for which we transform associated types to type parameters. *) hide_marker_traits : bool; (** Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show up. diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index 5b7a7ed7..ea23cc58 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -907,6 +907,13 @@ and trait_clause_id_of_json (ctx : of_json_ctx) (js : json) : | x -> TraitClauseId.id_of_json ctx x | _ -> Error "") +and trait_type_constraint_id_of_json (ctx : of_json_ctx) (js : json) : + (trait_type_constraint_id, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | x -> TraitTypeConstraintId.id_of_json ctx x + | _ -> Error "") + and type_var_of_json (ctx : of_json_ctx) (js : json) : (type_var, string) result = combine_error_msgs js __FUNCTION__ @@ -1202,7 +1209,7 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) : ctx types_outlive in let* trait_type_constraints = - list_of_json + vector_of_json trait_type_constraint_id_of_json (region_binder_of_json trait_type_constraint_of_json) ctx trait_type_constraints in @@ -1619,6 +1626,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : ("include", include_); ("opaque", opaque); ("exclude", exclude); + ("remove_associated_types", remove_associated_types); ("hide_marker_traits", hide_marker_traits); ("no_cargo", no_cargo); ("rustc_args", rustc_args); @@ -1647,6 +1655,9 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : let* included = list_of_json string_of_json ctx include_ in let* opaque = list_of_json string_of_json ctx opaque in let* exclude = list_of_json string_of_json ctx exclude in + let* remove_associated_types = + list_of_json string_of_json ctx remove_associated_types + in let* hide_marker_traits = bool_of_json ctx hide_marker_traits in let* no_cargo = bool_of_json ctx no_cargo in let* rustc_args = list_of_json string_of_json ctx rustc_args in @@ -1676,6 +1687,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) : included; opaque; exclude; + remove_associated_types; hide_marker_traits; no_cargo; rustc_args; diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index 91deed4d..a458a00f 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -20,6 +20,7 @@ module ConstGenericVarId = IdGen () module TraitDeclId = IdGen () module TraitImplId = IdGen () module TraitClauseId = IdGen () +module TraitTypeConstraintId = IdGen () module UnsolvedTraitId = IdGen () module RegionId = IdGen () module Disambiguator = IdGen () @@ -31,6 +32,11 @@ type integer_type = Values.integer_type [@@deriving show, ord] type float_type = Values.float_type [@@deriving show, ord] type literal_type = Values.literal_type [@@deriving show, ord] +(* Manually implemented because no type uses it (we use plain lists instead of + vectors in generic_params), which causes visitor inference problems if we + declare it within a visitor group. *) +type trait_type_constraint_id = TraitTypeConstraintId.id [@@deriving show, ord] + (** We define these types to control the name of the visitor functions *) type ('id, 'name) indexed_var = { index : 'id; (** Unique index identifying the variable *) @@ -256,12 +262,8 @@ and trait_instance_id = ``` *) | Self - (** Self, in case of trait declarations/implementations. - - Putting [Self] at the end on purpose, so that when ordering the clauses - we start with the other clauses (in particular, the local clauses). It - is useful to give priority to the local clauses when solving the trait - obligations which are fullfilled by the trait parameters. + (** The implicit `Self: Trait` clause. Present inside trait declarations, including trait + method declarations. Not present in trait implementations as we can use `TraitImpl` intead. *) | BuiltinOrAuto of trait_decl_ref region_binder diff --git a/charon/Cargo.lock b/charon/Cargo.lock index a6255c28..f7eada66 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -17,18 +17,6 @@ version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" -[[package]] -name = "ahash" -version = "0.8.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" -dependencies = [ - "cfg-if", - "once_cell", - "version_check", - "zerocopy", -] - [[package]] name = "aho-corasick" version = "1.1.3" @@ -213,7 +201,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.63" +version = "0.1.64" dependencies = [ "annotate-snippets", "anstream", @@ -226,10 +214,10 @@ dependencies = [ "derive_generic_visitor", "env_logger", "flate2", - "hashlink", "hax-frontend-exporter", "ignore", "index_vec", + "indexmap", "indoc", "itertools 0.13.0", "lazy_static", @@ -790,31 +778,12 @@ dependencies = [ "tracing", ] -[[package]] -name = "hashbrown" -version = "0.14.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" -dependencies = [ - "ahash", -] - [[package]] name = "hashbrown" version = "0.15.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" -[[package]] -name = "hashlink" -version = "0.9.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af" -dependencies = [ - "hashbrown 0.14.5", - "serde", -] - [[package]] name = "hax-adt-into" version = "0.1.0" @@ -1165,12 +1134,13 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62f822373a4fe84d4bb149bf54e584a7f4abec90e072ed49cda0edea5b95471f" +checksum = "8c9c992b02b5b4c94ea26e32fe5bccb7aa7d9f390ab5c1221ff895bc7ea8b652" dependencies = [ "equivalent", - "hashbrown 0.15.2", + "hashbrown", + "serde", ] [[package]] @@ -2463,12 +2433,6 @@ version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426" -[[package]] -name = "version_check" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" - [[package]] name = "wait-timeout" version = "0.2.0" @@ -2864,26 +2828,6 @@ dependencies = [ "synstructure", ] -[[package]] -name = "zerocopy" -version = "0.7.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" -dependencies = [ - "zerocopy-derive", -] - -[[package]] -name = "zerocopy-derive" -version = "0.7.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.90", -] - [[package]] name = "zerofrom" version = "0.1.5" diff --git a/charon/Cargo.toml b/charon/Cargo.toml index bf183ce1..d99c5ff1 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.63" +version = "0.1.64" authors = ["Son Ho "] edition = "2021" license = "Apache-2.0" @@ -51,7 +51,7 @@ crates_io_api = { version = "0.11.0", optional = true } derive_generic_visitor = "0.1.0" env_logger = { version = "0.11", features = ["color"] } flate2 = { version = "1.0.34", optional = true } -hashlink = { version = "0.9", features = ["serde_impl"] } +indexmap = { version = "2.7.1", features = ["serde"] } index_vec = { version = "0.1.3", features = ["serde"] } indoc = "2" itertools = "0.13" diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index 0161c64a..52f90789 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -100,16 +100,23 @@ impl ProjectionElem { if variant_id.is_some() { return Err(()); }; - let mut ty = fields.get(*field_id).ok_or(())?.ty.clone(); - ty.substitute(generics); - ty + fields + .get(*field_id) + .ok_or(())? + .ty + .clone() + .substitute(generics) } Enum(variants) => { let variant_id = variant_id.ok_or(())?; let variant = variants.get(variant_id).ok_or(())?; - let mut ty = variant.fields.get(*field_id).ok_or(())?.ty.clone(); - ty.substitute(generics); - ty + variant + .fields + .get(*field_id) + .ok_or(())? + .ty + .clone() + .substitute(generics) } Opaque | Alias(_) | Error(_) => return Err(()), } diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 5f985792..835d35fa 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -3,7 +3,7 @@ use crate::formatter::{FmtCtx, Formatter, IntoFormatter}; use crate::ids::Vector; use crate::reorder_decls::DeclarationsGroups; use derive_generic_visitor::{ControlFlow, Drive, DriveMut}; -use hashlink::LinkedHashSet; +use indexmap::IndexSet; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; use serde_map_to_array::HashMapToArray; @@ -114,7 +114,7 @@ pub struct TranslatedCrate { /// All the item ids, in the order in which we encountered them #[drive(skip)] - pub all_ids: LinkedHashSet, + pub all_ids: IndexSet, /// The names of all registered items. Available so we can know the names even of items that /// failed to translate. #[serde(with = "HashMapToArray::")] diff --git a/charon/src/ast/mod.rs b/charon/src/ast/mod.rs index 06fce9d8..e0601aff 100644 --- a/charon/src/ast/mod.rs +++ b/charon/src/ast/mod.rs @@ -28,6 +28,6 @@ pub use krate::*; pub use meta::*; pub use names::*; pub use types::*; -pub use types_utils::TyVisitable; +pub use types_utils::*; pub use values::*; pub use visitor::*; diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 07779119..cd7d02c9 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -115,12 +115,8 @@ pub enum TraitRefKind { #[charon::opaque] ItemClause(Box, TraitDeclId, TraitItemName, TraitClauseId), - /// Self, in case of trait declarations/implementations. - /// - /// Putting [Self] at the end on purpose, so that when ordering the clauses - /// we start with the other clauses (in particular, the local clauses). It - /// is useful to give priority to the local clauses when solving the trait - /// obligations which are fullfilled by the trait parameters. + /// The implicit `Self: Trait` clause. Present inside trait declarations, including trait + /// method declarations. Not present in trait implementations as we can use `TraitImpl` intead. #[charon::rename("Self")] SelfId, @@ -291,7 +287,7 @@ pub struct GenericParams { /// The type outlives the region pub types_outlive: Vec>, /// Constraints over trait associated types - pub trait_type_constraints: Vec>, + pub trait_type_constraints: Vector>, } /// A predicate of the form `exists where T: Trait`. @@ -329,7 +325,7 @@ pub enum PredicateOrigin { // trait Trait {} // ``` TraitSelf, - // Note: this also includes supertrait constraings. + // Note: this also includes supertrait constraints. // ``` // trait Trait {} // trait Trait where T: Clone {} diff --git a/charon/src/ast/types/vars.rs b/charon/src/ast/types/vars.rs index d6b69c30..bb645168 100644 --- a/charon/src/ast/types/vars.rs +++ b/charon/src/ast/types/vars.rs @@ -1,5 +1,7 @@ //! Type-level variables. There are 4 kinds of variables at the type-level: regions, types, const //! generics and trait clauses. The relevant definitions are in this module. +use std::ops::{Index, IndexMut}; + use derive_generic_visitor::{Drive, DriveMut}; use serde::{Deserialize, Serialize}; @@ -89,6 +91,7 @@ generate_index_type!(RegionId, "Region"); generate_index_type!(TypeVarId, "T"); generate_index_type!(ConstGenericVarId, "Const"); generate_index_type!(TraitClauseId, "TraitClause"); +generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint"); /// A type variable in a signature or binder. #[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] @@ -255,3 +258,98 @@ impl Default for DeBruijnId { Self::zero() } } + +/// A stack of values corresponding to nested binders. Each binder introduces an entry in this +/// stack, with the entry as index `0` being the innermost binder. This is indexed by +/// `DeBruijnId`s. +/// Most methods assume that the stack is non-empty and panic if not. +#[derive(Clone, Hash)] +pub struct BindingStack { + /// The stack, stored in reverse. We push/pop to the end of the `Vec`, and the last pushed + /// value (i.e. the end of the vec) is considered index 0. + stack: Vec, +} + +impl BindingStack { + pub fn new(x: T) -> Self { + Self { stack: vec![x] } + } + + pub fn is_empty(&self) -> bool { + self.stack.is_empty() + } + pub fn len(&self) -> usize { + self.stack.len() + } + pub fn depth(&self) -> DeBruijnId { + DeBruijnId::new(self.stack.len() - 1) + } + pub fn push(&mut self, x: T) { + self.stack.push(x); + } + pub fn pop(&mut self) -> Option { + self.stack.pop() + } + /// Helper that computes the real index into `self.stack`. + fn real_index(&self, id: DeBruijnId) -> usize { + self.stack.len() - 1 - id.index + } + pub fn get(&self, id: DeBruijnId) -> Option<&T> { + self.stack.get(self.real_index(id)) + } + pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> { + let index = self.real_index(id); + self.stack.get_mut(index) + } + /// Iterate over the binding levels, from the innermost (0) out. + pub fn iter(&self) -> impl Iterator + DoubleEndedIterator + ExactSizeIterator { + self.stack.iter().rev() + } + /// Iterate over the binding levels, from the innermost (0) out. + pub fn iter_enumerated( + &self, + ) -> impl Iterator + DoubleEndedIterator + ExactSizeIterator { + self.iter() + .enumerate() + .map(|(i, x)| (DeBruijnId::new(i), x)) + } + + pub fn innermost(&self) -> &T { + self.stack.last().unwrap() + } + pub fn innermost_mut(&mut self) -> &mut T { + self.stack.last_mut().unwrap() + } + pub fn outermost(&self) -> &T { + self.stack.first().unwrap() + } + pub fn outermost_mut(&mut self) -> &mut T { + self.stack.first_mut().unwrap() + } +} + +impl Default for BindingStack { + fn default() -> Self { + Self { + stack: Default::default(), + } + } +} + +impl std::fmt::Debug for BindingStack { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{:?}", self.stack) + } +} + +impl Index for BindingStack { + type Output = T; + fn index(&self, id: DeBruijnId) -> &Self::Output { + self.get(id).unwrap() + } +} +impl IndexMut for BindingStack { + fn index_mut(&mut self, id: DeBruijnId) -> &mut Self::Output { + self.get_mut(id).unwrap() + } +} diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 430e2b6b..778cc6ea 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -4,6 +4,7 @@ use crate::ids::Vector; use derive_generic_visitor::*; use std::collections::HashSet; use std::convert::Infallible; +use std::fmt::Debug; use std::iter::Iterator; use std::mem; use std::ops::Index; @@ -110,12 +111,10 @@ impl Binder { /// substituted inner value. pub fn apply(self, args: &GenericArgs) -> T where - T: AstVisitable, + T: TyVisitable, { - let mut val = self.skip_binder; assert!(args.matches(&self.params)); - val.drive_mut(&mut SubstVisitor::new(args)); - val + self.skip_binder.substitute(args) } } @@ -130,6 +129,27 @@ impl RegionBinder { skip_binder: x.move_under_binder(), } } + + pub fn map_ref(&self, f: impl FnOnce(&T) -> U) -> RegionBinder { + RegionBinder { + regions: self.regions.clone(), + skip_binder: f(&self.skip_binder), + } + } + + /// Substitute the bound variables with erased lifetimes. + pub fn erase(self) -> T + where + T: AstVisitable, + { + let mut val = self.skip_binder; + let args = GenericArgs { + regions: self.regions.map_ref_indexed(|_, _| Region::Erased), + ..GenericArgs::empty(GenericsSource::Builtin) + }; + val.drive_mut(&mut SubstVisitor::new(&args)); + val + } } impl GenericArgs { @@ -270,6 +290,88 @@ impl IntegerTy { } } +/// A value of type `T` bound by the generic parameters of item +/// `item`. Used when dealing with multiple items at a time, to +/// ensure we don't mix up generics. +/// +/// To get the value, use `under_binder_of` or `subst_for`. +#[derive(Debug, Clone, Copy)] +pub struct ItemBinder { + pub item_id: ItemId, + val: T, +} + +impl ItemBinder +where + ItemId: Debug + Copy + PartialEq, +{ + pub fn new(item_id: ItemId, val: T) -> Self { + Self { item_id, val } + } + + pub fn as_ref(&self) -> ItemBinder { + ItemBinder { + item_id: self.item_id, + val: &self.val, + } + } + + pub fn map_bound(self, f: impl FnOnce(T) -> U) -> ItemBinder { + ItemBinder { + item_id: self.item_id, + val: f(self.val), + } + } + + fn assert_item_id(&self, item_id: ItemId) { + assert_eq!( + self.item_id, item_id, + "Trying to use item bound for {:?} as if it belonged to {:?}", + self.item_id, item_id + ); + } + + /// Assert that the value is bound for item `item_id`, and returns it. This is used when we + /// plan to store the returned value inside that item. + pub fn under_binder_of(self, item_id: ItemId) -> T { + self.assert_item_id(item_id); + self.val + } + + /// Given generic args for `item_id`, assert that the value is bound for `item_id` and + /// substitute it with the provided generic arguments. Because the arguments are bound in the + /// context of another item, so it the resulting substituted value. + pub fn substitute( + self, + args: ItemBinder, + ) -> ItemBinder + where + ItemId: Into, + T: TyVisitable, + { + args.map_bound(|args| { + assert_eq!( + args.target, + GenericsSource::item(self.item_id), + "These `GenericArgs` are meant for {:?} but were used on {:?}", + args.target, + self.item_id + ); + self.val.substitute(args) + }) + } +} + +/// Dummy item identifier that represents the current item when not ambiguous. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct CurrentItem; + +impl ItemBinder { + pub fn under_current_binder(self) -> T { + self.val + } +} + impl Ty { /// Return true if it is actually unit (i.e.: 0-tuple) pub fn is_unit(&self) -> bool { @@ -567,8 +669,9 @@ impl VisitAstMut for SubstVisitor<'_> { /// Types that are involved at the type-level and may be substituted around. pub trait TyVisitable: Sized + AstVisitable { - fn substitute(&mut self, generics: &GenericArgs) { + fn substitute(mut self, generics: &GenericArgs) -> Self { self.drive_mut(&mut SubstVisitor::new(generics)); + self } /// Move under one binder. diff --git a/charon/src/ast/visitor.rs b/charon/src/ast/visitor.rs index 7930530e..b59f1c2c 100644 --- a/charon/src/ast/visitor.rs +++ b/charon/src/ast/visitor.rs @@ -46,8 +46,8 @@ use index_vec::Idx; FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy, llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch, Locals, Name, NullOp, Opaque, Operand, PathElem, Place, PlaceKind, ProjectionElem, RawConstantExpr, - RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClause, TraitClauseId, TraitItemName, - TraitRefKind, TraitTypeConstraint, TranslatedCrate, TyKind, TypeDeclKind, TypeId, TypeVar, TypeVarId, + RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClauseId, TraitItemName, + TranslatedCrate, TypeDeclKind, TypeId, TypeVar, TypeVarId, ullbc_ast::BlockData, ullbc_ast::BlockId, ullbc_ast::ExprBody, ullbc_ast::RawStatement, ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets, ullbc_ast::Terminator, UnOp, Var, Variant, VariantId, VarId, @@ -62,9 +62,9 @@ use index_vec::Idx; // Types for which we call the corresponding `visit_$ty` method, which by default explores the // type but can be overridden. override( - DeBruijnId, Ty, Region, ConstGeneric, TraitRef, + DeBruijnId, Ty, TyKind, Region, ConstGeneric, TraitRef, TraitRefKind, FunDeclRef, GlobalDeclRef, TraitDeclRef, TraitImplRef, - GenericArgs, GenericParams, + GenericArgs, GenericParams, TraitClause, TraitTypeConstraint, for DeBruijnVar, for RegionBinder, for Binder, diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index 63bd69f3..d2b85768 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -252,7 +252,10 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa // run several passes that simplify the items and cleanup the bodies. for pass in transformation_passes(options) { trace!("# Starting pass {}", pass.name()); - pass.run(&mut transform_ctx) + pass.run(&mut transform_ctx); + if transform_ctx.errors.borrow().has_errors() { + break; + } } // Update the error count 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 301e14ae..5703be98 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 @@ -1,7 +1,6 @@ use super::translate_ctx::*; use charon_lib::ast::*; use charon_lib::options::CliOpts; -use charon_lib::transform::ctx::TransformOptions; use charon_lib::transform::TransformCtx; use hax_frontend_exporter as hax; use rustc_hir::def_id::DefId; @@ -297,13 +296,9 @@ pub fn translate<'tcx, 'ctx>( } // Return the context, dropping the hax state and rustc `tcx`. - let transform_options = TransformOptions { - no_code_duplication: options.no_code_duplication, - hide_marker_traits: options.hide_marker_traits, - no_merge_goto_chains: options.no_merge_goto_chains, - print_built_llbc: options.print_built_llbc, - item_opacities: ctx.options.item_opacities, - }; + let transform_options = ctx + .options + .into_transform_options(&mut *ctx.errors.borrow_mut(), options); TransformCtx { options: transform_options, diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index e5e79a6e..b88207aa 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -6,6 +6,7 @@ use charon_lib::formatter::{FmtCtx, IntoFormatter}; use charon_lib::ids::{MapGenerator, Vector}; use charon_lib::name_matcher::NamePattern; use charon_lib::options::CliOpts; +use charon_lib::transform::ctx::TransformOptions; use charon_lib::ullbc_ast as ast; use hax_frontend_exporter::SInto; use hax_frontend_exporter::{self as hax, DefPathItem}; @@ -49,6 +50,8 @@ pub struct TranslateOptions { /// matches determines the opacity of the item. When no options are provided this is initialized /// to treat items in the crate as transparent and items in other crates as foreign. pub item_opacities: Vec<(NamePattern, ItemOpacity)>, + /// List of traits for which we transform associated types to type parameters. + pub remove_associated_types: Vec, } impl TranslateOptions { @@ -110,9 +113,31 @@ impl TranslateOptions { .collect() }; + let remove_associated_types = options + .remove_associated_types + .iter() + .filter_map(|s| parse_pattern(&s).ok()) + .collect(); + TranslateOptions { mir_level, item_opacities, + remove_associated_types, + } + } + + pub(crate) fn into_transform_options( + self, + _error_ctx: &mut ErrorCtx, + options: &CliOpts, + ) -> TransformOptions { + TransformOptions { + no_code_duplication: options.no_code_duplication, + hide_marker_traits: options.hide_marker_traits, + no_merge_goto_chains: options.no_merge_goto_chains, + print_built_llbc: options.print_built_llbc, + item_opacities: self.item_opacities, + remove_associated_types: self.remove_associated_types, } } } @@ -333,7 +358,7 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx> { /// The stack of generic parameter binders for the current context. Each binder introduces an /// entry in this stack, with the entry as index `0` being the innermost binder. These /// parameters are referenced using [`DeBruijnVar`]; see there for details. - pub binding_levels: VecDeque, + pub binding_levels: BindingStack, /// (For traits only) accumulated implied trait clauses. pub parent_trait_clauses: Vector, /// (For traits only) accumulated trait clauses on associated types. @@ -1074,39 +1099,34 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { } pub(crate) fn outermost_binder(&self) -> &BindingLevel { - self.binding_levels.back().unwrap() + self.binding_levels.outermost() } pub(crate) fn innermost_binder(&self) -> &BindingLevel { - self.binding_levels.front().unwrap() + self.binding_levels.innermost() } pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel { - self.binding_levels.front_mut().unwrap() + self.binding_levels.innermost_mut() } pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams { &mut self.innermost_binder_mut().params } - /// Make a `DeBruijnVar`, where we use `Free` for the outermost binder and `Bound` for the - /// others. - fn bind_var(&self, dbid: usize, varid: Id) -> DeBruijnVar { - DeBruijnVar::bound(DeBruijnId::new(dbid), varid) - } - pub(crate) fn lookup_bound_region( &mut self, span: Span, dbid: hax::DebruijnIndex, var: hax::BoundVar, ) -> Result { + let dbid = DeBruijnId::new(dbid); if let Some(rid) = self .binding_levels .get(dbid) .and_then(|bl| bl.bound_region_vars.get(var)) { - Ok(self.bind_var(dbid, *rid)) + Ok(DeBruijnVar::bound(dbid, *rid)) } else { raise_error!( self, @@ -1122,9 +1142,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { f: impl for<'a> Fn(&'a BindingLevel) -> Option, mk_err: impl FnOnce() -> String, ) -> Result, Error> { - for (dbid, bl) in self.binding_levels.iter().enumerate() { + for (dbid, bl) in self.binding_levels.iter_enumerated() { if let Some(id) = f(bl) { - return Ok(self.bind_var(dbid, id)); + return Ok(DeBruijnVar::bound(dbid, id)); } } let err = mk_err(); @@ -1178,17 +1198,16 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // ignore the clause count. let innermost_item_binder_id = self .binding_levels - .iter() - .enumerate() + .iter_enumerated() .find(|(_, bl)| bl.is_item_binder) .unwrap() .0; // Iterate over the binders, starting from the outermost. - for (dbid, bl) in self.binding_levels.iter().enumerate().rev() { + for (dbid, bl) in self.binding_levels.iter_enumerated().rev() { let num_clauses_bound_at_this_level = bl.params.trait_clauses.len(); if id < num_clauses_bound_at_this_level || dbid == innermost_item_binder_id { let id = TraitClauseId::from_usize(id); - return Ok(self.bind_var(dbid, id)); + return Ok(DeBruijnVar::bound(dbid, id)); } else { id -= num_clauses_bound_at_this_level } @@ -1231,13 +1250,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // Register the variables let mut binding_level = BindingLevel::new(false); binding_level.push_params_from_binder(binder.rebind(()))?; - self.binding_levels.push_front(binding_level); + self.binding_levels.push(binding_level); // Call the continuation. Important: do not short-circuit on error here. let res = f(self, binder.hax_skip_binder_ref()); // Reset - let regions = self.binding_levels.pop_front().unwrap().params.regions; + let regions = self.binding_levels.pop().unwrap().params.regions; // Return res.map(|skip_binder| RegionBinder { @@ -1267,7 +1286,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { let res = f(self); // Reset - let params = self.binding_levels.pop_front().unwrap().params; + let params = self.binding_levels.pop().unwrap().params; // Return res.map(|skip_binder| Binder { diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index f52d0d99..781353d4 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -548,7 +548,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { def: &hax::FullDef, ) -> Result<(), Error> { assert!(self.binding_levels.len() == 0); - self.binding_levels.push_front(BindingLevel::new(true)); + self.binding_levels.push(BindingLevel::new(true)); self.push_generics_for_def(span, def, false)?; self.innermost_binder_mut().params.check_consistency(); Ok(()) @@ -560,7 +560,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { span: Span, def: &hax::FullDef, ) -> Result<(), Error> { - self.binding_levels.push_front(BindingLevel::new(true)); + self.binding_levels.push(BindingLevel::new(true)); self.push_generics_for_def_without_parents(span, def, true, true)?; self.innermost_binder().params.check_consistency(); Ok(()) @@ -568,7 +568,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { pub(crate) fn into_generics(mut self) -> GenericParams { assert!(self.binding_levels.len() == 1); - self.binding_levels.pop_back().unwrap().params + self.binding_levels.pop().unwrap().params } /// Add the generics and predicates of this item and its parents to the current context. diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index a6a121a4..1beb2a3c 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -1078,7 +1078,13 @@ fn generate_ml( ), ]; // Types for which we don't want to generate a type at all. - let dont_generate_ty = &["ItemOpacity", "PredicateOrigin", "Ty", "Vector"]; + let dont_generate_ty = &[ + "ItemOpacity", + "PredicateOrigin", + "TraitTypeConstraintId", + "Ty", + "Vector", + ]; // Types that we don't want visitors to go into. let opaque_for_visitor = &["Name"]; let ctx = GenerateCtx::new( diff --git a/charon/src/bin/generate-ml/templates/Types.ml b/charon/src/bin/generate-ml/templates/Types.ml index 91aa64c2..f6a3dd9b 100644 --- a/charon/src/bin/generate-ml/templates/Types.ml +++ b/charon/src/bin/generate-ml/templates/Types.ml @@ -22,6 +22,7 @@ module ConstGenericVarId = IdGen () module TraitDeclId = IdGen () module TraitImplId = IdGen () module TraitClauseId = IdGen () +module TraitTypeConstraintId = IdGen () module UnsolvedTraitId = IdGen () module RegionId = IdGen () module Disambiguator = IdGen () @@ -34,6 +35,11 @@ type integer_type = Values.integer_type [@@deriving show, ord] type float_type = Values.float_type [@@deriving show, ord] type literal_type = Values.literal_type [@@deriving show, ord] +(* Manually implemented because no type uses it (we use plain lists instead of + vectors in generic_params), which causes visitor inference problems if we + declare it within a visitor group. *) +type trait_type_constraint_id = TraitTypeConstraintId.id [@@deriving show, ord] + (** We define these types to control the name of the visitor functions *) type ('id, 'name) indexed_var = { index : 'id; (** Unique index identifying the variable *) diff --git a/charon/src/errors.rs b/charon/src/errors.rs index 26f33b6a..7be947c5 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -210,7 +210,7 @@ impl ErrorCtx { pub fn continue_on_failure(&self) -> bool { self.continue_on_failure } - pub(crate) fn has_errors(&self) -> bool { + pub fn has_errors(&self) -> bool { self.error_count > 0 } diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs index 59f7eaab..141cabe3 100644 --- a/charon/src/ids/vector.rs +++ b/charon/src/ids/vector.rs @@ -126,6 +126,16 @@ where self.real_len += other.real_len; } + /// Get a mutable reference into the ith element. If the vector is too short, extend it until + /// it has enough elements. If the element doesn't exist, use the provided function to + /// initialize it. + pub fn get_or_extend_and_insert(&mut self, id: I, f: impl FnOnce() -> T) -> &mut T { + if id.index() >= self.vector.len() { + self.vector.resize_with(id.index() + 1, || None); + } + self.vector[id].get_or_insert_with(f) + } + /// Map each entry to a new one, keeping the same ids. pub fn map(self, mut f: impl FnMut(T) -> U) -> Vector { Vector { @@ -174,6 +184,27 @@ where } } + /// Map each entry to a new one, keeping the same ids. Includes empty slots. + pub fn map_opt(self, f: impl FnMut(Option) -> Option) -> Vector { + Vector { + vector: self.vector.into_iter().map(f).collect(), + real_len: self.real_len, + } + } + + /// Map each entry to a new one, keeping the same ids. Includes empty slots. + pub fn map_ref_opt<'a, U>( + &'a self, + mut f: impl FnMut(Option<&'a T>) -> Option, + ) -> Vector { + let mut ret = Vector { + vector: self.vector.iter().map(|x_opt| f(x_opt.as_ref())).collect(), + real_len: self.real_len, + }; + ret.real_len = ret.iter().count(); + ret + } + /// Iter over the nonempty slots. pub fn iter(&self) -> impl Iterator + DoubleEndedIterator + Clone { self.vector.iter().filter_map(|opt| opt.as_ref()) @@ -189,6 +220,12 @@ where .flat_map(|(i, opt)| Some((i, opt.as_ref()?))) } + pub fn iter_mut_indexed(&mut self) -> impl Iterator { + self.vector + .iter_mut_enumerated() + .flat_map(|(i, opt)| Some((i, opt.as_mut()?))) + } + pub fn into_iter_indexed(self) -> impl Iterator { self.vector .into_iter_enumerated() diff --git a/charon/src/options.rs b/charon/src/options.rs index 0c86db18..d13b023d 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -156,6 +156,14 @@ pub struct CliOpts { )] #[serde(default)] pub exclude: Vec, + /// List of traits for which we transform associated types to type parameters. + #[clap( + long = "remove-associated-types", + help = "List of traits for which we transform associated types to type parameters. \ + The syntax is like `--include`, see the doc there." + )] + #[serde(default)] + pub remove_associated_types: Vec, /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show /// up. #[clap(long = "hide-marker-traits")] diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index 8b4724eb..2360ed52 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -24,6 +24,8 @@ pub struct TransformOptions { /// List of patterns to assign a given opacity to. Same as the corresponding `TranslateOptions` /// field. pub item_opacities: Vec<(NamePattern, ItemOpacity)>, + /// List of traits for which we transform associated types to type parameters. + pub remove_associated_types: Vec, } /// Simpler context used for rustc-independent code transformation. This only depends on rustc for @@ -222,6 +224,29 @@ impl<'ctx> TransformCtx { } } } + + /// Iterate mutably over all items, keeping access to `self`. To make this work, we move out + /// each item before iterating over it. + pub fn for_each_item_mut( + &mut self, + mut f: impl for<'a> FnMut(&'a mut Self, AnyTransItemMut<'a>), + ) { + macro_rules! for_each { + ($vector:ident, $kind:ident) => { + for id in self.translated.$vector.all_indices() { + if let Some(mut decl) = self.translated.$vector.remove(id) { + f(self, AnyTransItemMut::$kind(&mut decl)); + self.translated.$vector.set_slot(id, decl); + } + } + }; + } + for_each!(type_decls, Type); + for_each!(fun_decls, Fun); + for_each!(global_decls, Global); + for_each!(trait_decls, TraitDecl); + for_each!(trait_impls, TraitImpl); + } } impl<'a> IntoFormatter for &'a TransformCtx { diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs new file mode 100644 index 00000000..19978d56 --- /dev/null +++ b/charon/src/transform/expand_associated_types.rs @@ -0,0 +1,1295 @@ +//! Change trait associated types to be type parameters instead. E.g. +//! ```rust,ignore +//! trait Iterator { +//! type Item; +//! } +//! fn merge(...) -> ... +//! where +//! I: Iterator, +//! J: Iterator, +//! {} +//! // becomes +//! trait Iterator { +//! } +//! fn merge(...) -> ... +//! where +//! I: Iterator, +//! J: Iterator, +//! {} +//! ``` +//! +//! This pass only transforms traits that are selected with the `--remove-associated-types` option. +//! The pass also normalizes associated types everywhere. +//! +//! The pass works as follows: +//! 1. We compute for each item the list of associated types that need to be provided a value, +//! represented with `AssocTypePath`. E.g. the above example gives us one extra param for +//! `Iterator`, corresponding to `Self::Item`. +//! If the associated type was constrained by a `Trait::Type = T` clause, we remember that. +//! 2. For each item, for each such associated type for which we don't have a value, we add a type +//! parameter to the item. We then update each `GenericArgs`,`TraitRef` and `TyKind::TraitType` +//! pointing to a modified item. This includes going into function and type bodies to replace +//! all trait type references with our new parameters. +//! +//! Note that the first step is recursive: if a trait has parent clauses, types needed by these +//! parent clauses will be needed by the trait itself too. +//! ```rust,ignore +//! trait Foo { +//! type Item: Bar; +//! } +//! trait Bar { +//! type Output; +//! } +//! // becomes: +//! trait Foo +//! where Item: Bar {} +//! trait Bar {} +//! ``` +//! +//! In this process we detect recursive cases that we can't handle and skip them. For example: +//! ```rust,ignore +//! trait Bar { +//! type BarTy; +//! } +//! trait Foo { +//! type FooTy: Foo + Bar; +//! } +//! // becomes: +//! trait Bar {} +//! trait Foo { +//! type FooTy: Foo + Bar; +//! // We need to supply an argument to `Bar` but we can't add a type parameter, so we add a +//! // new associated type. +//! type FooTy_BarTy; +//! } +//! ``` +//! +//! Limitations: +//! - we're missing assoc type info in `dyn Trait`, so we can't fixup the generics there. +//! - we don't track bound lifetimes in quantified clauses properly (https://github.com/AeneasVerif/charon/issues/534). +//! - type aliases don't have the correct clauses in scope (https://github.com/AeneasVerif/charon/issues/531). +//! - we don't take into account unicity of trait implementations. This means we won't detect type +//! equalities due to the same trait predicate appearing twice, or a trait predicate coinciding +//! with an existing trait impl. See the `dictionary_passing_style_woes.rs` test file. +use derive_generic_visitor::*; +use itertools::Itertools; +use std::{ + collections::{HashMap, HashSet}, + mem, +}; + +use macros::EnumAsGetters; + +use crate::{ast::*, formatter::FmtCtx, ids::Vector, pretty::FmtWithCtx, register_error}; + +use super::{ctx::TransformPass, TransformCtx}; + +/// Represent some `TraitRef`s as paths for easier manipulation. +use trait_ref_path::*; +mod trait_ref_path { + use macros::{EnumIsA, EnumToGetters}; + + use crate::ast::*; + + /// A base clause: the special `Self: Trait` clause present in trait declarations, or a local + /// clause. + #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, EnumIsA, EnumToGetters)] + pub enum BaseClause { + SelfClause, + Local(DeBruijnVar), + } + + /// A `TraitRef` represented as a path. + #[derive(Debug, Clone, PartialEq, Eq)] + pub struct TraitRefPath { + /// The base clause we start from. + pub base: BaseClause, + /// Starting from `base`, recursively take the ith parent clause of the current clause. Each id + /// corresponds to a parent of the previous one, e.g. + /// ```rust,ignore + /// trait Foo { + /// type FooTy; + /// } + /// trait Bar: Foo {} // `Self: Foo` is parent clause 0 + /// trait Baz: Copy // `Self: Copy` is parent clause 0 + /// { + /// // `Self::BazTy: Bar` is parent clause 1 + /// // `::FooTy = bool` is type constraint 0 + /// // The `TraitRefPath` for `` has base `Self` and `parent_path == [1, 0]`. + /// type BazTy: Bar; + /// } + /// ``` + pub parent_path: Vec, + } + + impl TraitRefPath { + /// Make a trait ref that refers to the special `Self` clause. + pub fn self_ref() -> Self { + Self { + base: BaseClause::SelfClause, + parent_path: vec![], + } + } + /// Make a trait ref that refers to the given clause at depth 0. + pub fn local_clause(clause_id: TraitClauseId) -> Self { + Self { + base: BaseClause::Local(DeBruijnVar::new_at_zero(clause_id)), + parent_path: vec![], + } + } + /// Make a trait ref that refers to the given parent clause on `Self`. + /// Given a ref on a local clause, move it to refer to `Self`. This is used when we generate + /// paths for the `GenericParams` of a trait: within the `GenericParams` we don't know whether + /// we're talking about local clauses of trait implied clauses; we fix this here. + pub fn parent_clause(id: TraitClauseId) -> Self { + Self { + base: BaseClause::SelfClause, + parent_path: vec![id], + } + } + + pub fn with_assoc_type(self, type_name: TraitItemName) -> AssocTypePath { + AssocTypePath { + tref: self, + type_name, + } + } + + /// Given a ref on `Self`, make it into a ref on the given clause. + pub fn on_local_clause(&self, id: TraitClauseId) -> Self { + assert!(matches!(self.base, BaseClause::SelfClause)); + let mut new_ref = self.clone(); + new_ref.base = BaseClause::Local(DeBruijnVar::new_at_zero(id)); + new_ref + } + + /// Given a ref on `Self`, apply it on top of given ref. + pub fn on_tref(&self, tref: &TraitRefPath) -> TraitRefPath { + assert!(matches!(self.base, BaseClause::SelfClause)); + let mut new_ref = tref.clone(); + new_ref.parent_path.extend(self.parent_path.iter().copied()); + new_ref + } + + /// References the same clause one level up. + pub fn pop_base(&self) -> Self { + let mut new_ref = self.clone(); + match self.base { + BaseClause::Local(_) => { + new_ref.base = BaseClause::SelfClause; + } + BaseClause::SelfClause => panic!(), + } + new_ref + } + + /// For a ref based on `Self` parent clauses, this returns the first parent id and the rest of + /// the ref (that applies to the parent trait). + pub fn pop_first_parent(&self) -> Option<(TraitClauseId, Self)> { + assert!(self.base.is_self_clause()); + if self.parent_path.is_empty() { + None + } else { + let mut this = self.clone(); + let clause_id = this.parent_path.remove(0); + Some((clause_id, this)) + } + } + + fn move_from_under_binders(mut self, depth: DeBruijnId) -> Option { + match &mut self.base { + BaseClause::SelfClause => {} + BaseClause::Local(var) => *var = var.move_from_under_binders(depth)?, + } + Some(self) + } + } + + impl TraitRefKind { + pub fn to_path(&self) -> Option { + match self { + TraitRefKind::SelfId => Some(TraitRefPath { + base: BaseClause::SelfClause, + parent_path: vec![], + }), + TraitRefKind::Clause(id) => Some(TraitRefPath { + base: BaseClause::Local(*id), + parent_path: vec![], + }), + TraitRefKind::ParentClause(tref, _, id) => { + let mut path = tref.to_path()?; + path.parent_path.push(*id); + Some(path) + } + TraitRefKind::ItemClause(_, _, _, _) => unreachable!(), + TraitRefKind::TraitImpl(_, _) + | TraitRefKind::BuiltinOrAuto { .. } + | TraitRefKind::Dyn(_) + | TraitRefKind::Unknown(_) => None, + } + } + } + + impl TraitRef { + pub fn to_path(&self) -> Option { + self.kind.to_path() + } + } + + /// The path to an associated type that depends on a local clause. + #[derive(Debug, Clone)] + pub struct AssocTypePath { + /// The trait clause that has the associated type. + pub tref: TraitRefPath, + /// The name of the associated type. + pub type_name: TraitItemName, + } + + impl AssocTypePath { + /// See [`TraitRefPath::on_local_clause`]. + pub fn on_local_clause(&self, id: TraitClauseId) -> AssocTypePath { + Self { + tref: self.tref.on_local_clause(id), + type_name: self.type_name.clone(), + } + } + + /// See [`TraitRefPath::on_local_tref`]. + pub fn on_tref(&self, tref: &TraitRefPath) -> AssocTypePath { + Self { + tref: self.tref.on_tref(&tref), + type_name: self.type_name.clone(), + } + } + + /// See [`TraitRefPath::pop_base`]. + pub fn pop_base(&self) -> Self { + Self { + tref: self.tref.pop_base(), + type_name: self.type_name.clone(), + } + } + + /// For a ref based on `Self` parent clauses, this returns the first parent id and the rest of + /// the ref (that applies to the parent trait). + pub fn pop_first_parent(&self) -> Option<(TraitClauseId, Self)> { + let (clause_id, sub_tref) = self.tref.pop_first_parent()?; + let sub_path = Self { + tref: sub_tref, + type_name: self.type_name.clone(), + }; + Some((clause_id, sub_path)) + } + + /// Transform a trait type constraint into a (path, ty) pair. If the constraint does not refer + /// to a local clause, we return it unchanged. + pub fn from_constraint(cstr: &RegionBinder) -> Option { + // `unwrap()` is ok because a path only contains clause variables, which can't be bound + // in a predicate binder. + let tref = cstr + .skip_binder + .trait_ref + .to_path()? + .move_from_under_binders(DeBruijnId::one()) + .unwrap(); + Some(AssocTypePath { + tref, + type_name: cstr.skip_binder.type_name.clone(), + }) + } + + /// Construct a name that can be used to name a new type parameter/associated type + /// corresponding to this path. + pub fn to_name(&self) -> String { + use std::fmt::Write; + let mut buf = match &self.tref.base { + BaseClause::SelfClause => "Self".to_string(), + BaseClause::Local(var) => { + format!("Clause{}", var.bound_at_depth(DeBruijnId::zero()).unwrap()) + } + }; + for id in &self.tref.parent_path { + let _ = write!(&mut buf, "_Clause{id}"); + } + let _ = write!(&mut buf, "_{}", self.type_name); + buf + } + } + + impl std::fmt::Display for AssocTypePath { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match &self.tref.base { + BaseClause::SelfClause => write!(f, "Self")?, + BaseClause::Local(var) => write!(f, "Clause{var}")?, + }; + for id in &self.tref.parent_path { + write!(f, "::Clause{id}")?; + } + write!(f, "::{}", self.type_name)?; + Ok(()) + } + } +} + +/// Efficient representation of a set of `::Type = T` constraints. +use type_constraint_set::*; +mod type_constraint_set { + use std::collections::HashMap; + + use super::trait_ref_path::*; + use crate::ast::*; + + /// A set of local `TraitTypeConstraint`s, represented as a trie. + #[derive(Default, Clone)] + pub struct TypeConstraintSet { + /// For each base clause, a sub-trie of type constraints. + clauses: HashMap, + } + + /// A set of `TraitTypeConstraint`s that apply to a trait. + #[derive(Debug, Default, Clone)] + struct TypeConstraintSetInner { + /// The types that correspond to `Self::` for each `Name`. We also remember the id of the + /// original constraint if applicable. + assoc_tys: HashMap, Ty)>, + /// The types constraints that depend on the ith parent clause. + parent_clauses: Vector, + } + + impl TypeConstraintSet { + pub fn from_constraints( + constraints: &Vector>, + ) -> Self { + let mut this = TypeConstraintSet::default(); + for (i, c) in constraints.iter_indexed() { + this.insert_type_constraint(i, c); + } + this + } + + /// Add a type constraint to the set. + fn insert_inner( + &mut self, + path: &AssocTypePath, + cid: Option, + ty: Ty, + ) { + let mut trie = self.clauses.entry(path.tref.base).or_default(); + for id in &path.tref.parent_path { + trie = trie + .parent_clauses + .get_or_extend_and_insert(*id, Default::default); + } + trie.assoc_tys.insert(path.type_name.clone(), (cid, ty)); + } + + /// Add a type constraint to the set that doesn't come from a `TraitTypeConstraint`. + pub fn insert_path(&mut self, path: &AssocTypePath, ty: Ty) { + self.insert_inner(path, None, ty); + } + + /// Add a type constraint to the set. + fn insert_type_constraint( + &mut self, + cid: TraitTypeConstraintId, + cstr: &RegionBinder, + ) { + let Some(path) = AssocTypePath::from_constraint(cstr) else { + // We ignore non-local constraints. + return; + }; + // Erase bound lifetimes; handling them correctly would require tracking a lot more + // info. + let ty = cstr.map_ref(|cstr| cstr.ty.clone()).erase(); + self.insert_inner(&path, Some(cid), ty); + } + + /// Find the entry at that path from the trie, if it exists. + pub fn find(&self, path: &AssocTypePath) -> Option<(Option, &Ty)> { + if let BaseClause::Local(var) = path.tref.base { + // Only lookup at level zero because replacements are always at level zero relative to + // the item. + assert!(var.bound_at_depth(DeBruijnId::zero()).is_some()); + } + let mut trie = self.clauses.get(&path.tref.base)?; + for id in &path.tref.parent_path { + trie = trie.parent_clauses.get(*id)?; + } + trie.assoc_tys + .get(&path.type_name) + .map(|(id, ty)| (*id, ty)) + } + + pub fn iter(&self) -> impl Iterator { + let mut vec = vec![]; + for (base, inner) in &self.clauses { + inner.to_vec_inner( + &mut vec, + &TraitRefPath { + base: *base, + parent_path: vec![], + }, + ) + } + vec.into_iter() + } + } + + impl TypeConstraintSetInner { + fn debug_fmt( + &self, + f: &mut std::fmt::Formatter<'_>, + base: BaseClause, + parents: &[TraitClauseId], + ) -> std::fmt::Result { + for (name, (_, ty)) in &self.assoc_tys { + match base { + BaseClause::SelfClause => write!(f, "Self")?, + BaseClause::Local(id) => write!(f, "Clause{id}")?, + } + for id in parents { + write!(f, "::Clause{id}")?; + } + write!(f, "::{name} = {ty:?}, ")?; + } + for (parent_id, parent_trie) in self.parent_clauses.iter_indexed() { + let mut new_parents = parents.to_vec(); + new_parents.push(parent_id); + parent_trie.debug_fmt(f, base, &new_parents)?; + } + Ok(()) + } + + fn to_vec_inner(&self, vec: &mut Vec<(AssocTypePath, Ty)>, base_path: &TraitRefPath) { + for (name, (_, ty)) in &self.assoc_tys { + vec.push((base_path.clone().with_assoc_type(name.clone()), ty.clone())); + } + for (clause_id, inner) in self.parent_clauses.iter_indexed() { + let mut base_path = base_path.clone(); + base_path.parent_path.push(clause_id); + inner.to_vec_inner(vec, &base_path); + } + } + } + + impl std::fmt::Debug for TypeConstraintSet { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.write_str("{ ")?; + for (base, inner) in self.clauses.iter() { + inner.debug_fmt(f, *base, &[])?; + } + f.write_str("}")?; + Ok(()) + } + } +} + +/// Records the modifications we are operating on the given item. +#[derive(Debug, Clone)] +struct ItemModifications { + /// The constraints on associated types for this item. + type_constraints: TypeConstraintSet, + /// Associated item paths for which we don't know a type they correspond to, so we will have to + /// add a new type parameter to the signature of the item. + required_extra_paths: Vec, + /// These constraints refer to now-removed associated types. We have taken them into account, + /// they should be removed. + remove_constraints: HashSet, + /// For trait declarations only: if `true`, we turn its associated types into parameters and + /// turn any extra required params into new params. If `false`, we keep its associated types + /// and turn extra require params into new associated types. + /// For non-traits, this is always `true`. + add_type_params: bool, +} + +impl ItemModifications { + fn new( + type_constraints: &Vector>, + add_type_params: bool, + ) -> Self { + Self::from_constraint_set( + TypeConstraintSet::from_constraints(type_constraints), + add_type_params, + ) + } + + fn from_constraint_set(type_constraints: TypeConstraintSet, add_type_params: bool) -> Self { + Self { + type_constraints, + required_extra_paths: Default::default(), + remove_constraints: Default::default(), + add_type_params, + } + } + + /// Record that we must replace this path. If there is a relevant type constraint we can use + /// it, otherwise we will need to add a new type parameter to supply a value for this path. + fn replace_path(&mut self, path: AssocTypePath) { + if let Some((cstr_id, _)) = self.type_constraints.find(&path) { + // The local constraints already give us a value for this associated type; we + // use that. + if let Some(cstr_id) = cstr_id { + self.remove_constraints.insert(cstr_id); + } + // The path is already in the set, no need to replace it. + } else { + // We don't have a value for this associated type; we add a new type parameter + // to supply it. + self.required_extra_paths.push(path); + } + } + + /// Iterate over the paths that need to be filled. + fn required_extra_paths(&self) -> impl Iterator { + self.required_extra_paths.iter() + } + + /// Iterate over the paths that require adding new type parameters. + fn required_extra_params(&self) -> impl Iterator { + if self.add_type_params { + Some(self.required_extra_paths()) + } else { + None + } + .into_iter() + .flatten() + } + + /// Iterate over the paths that require adding new associated types. + fn required_extra_assoc_types(&self) -> impl Iterator { + if self.add_type_params { + None + } else { + Some(self.required_extra_paths()) + } + .into_iter() + .flatten() + } + + /// Compute the type replacements needed to update the body of this item. We use the provided + /// function to make new types for each missing type. That function will typically add new type + /// parameters to the item signature. + fn compute_replacements(&self, mut f: impl FnMut(&AssocTypePath) -> Ty) -> TypeConstraintSet { + let mut set = self.type_constraints.clone(); + for path in &self.required_extra_paths { + let ty = f(path); + set.insert_path(path, ty); + } + set + } +} + +/// An enum to manage potentially-cyclic computations. +#[derive(Debug, EnumAsGetters)] +enum Processing { + /// We haven't analyzed this yet. + Unprocessed, + /// Sentinel value that we set when starting the computation on an item. If we ever encounter + /// this, we know we encountered a loop that we can't handle. + Processing, + /// Sentinel value we put when encountering a cycle, so we can know that happened. + Cyclic, + /// The final result of the computation. + Processed(T), +} + +struct ComputeItemModifications<'a> { + ctx: &'a TransformCtx, + /// Records the modifications for each trait. + trait_modifications: Vector>, + /// Records the set of known associated types for this trait impl, including parent impls and + /// associated type constraints. + impl_assoc_tys: Vector>, +} + +impl<'a> ComputeItemModifications<'a> { + fn new(ctx: &'a TransformCtx) -> Self { + ComputeItemModifications { + ctx, + trait_modifications: ctx + .translated + .trait_decls + .map_ref_opt(|_| Some(Processing::Unprocessed)), + impl_assoc_tys: ctx + .translated + .trait_impls + .map_ref_opt(|_| Some(Processing::Unprocessed)), + } + } + + fn compute_item_modifications(&mut self, item: AnyTransItem<'_>) -> ItemModifications { + if let AnyTransItem::TraitDecl(tdecl) = item { + // The complex case is traits: we call `compute_extra_params_for_trait` to + // compute the right thing. + let id = tdecl.def_id; + let _ = self.compute_extra_params_for_trait(id); + self.trait_modifications[id].as_processed().unwrap().clone() + } else if let AnyTransItem::TraitImpl(timpl) = item { + let _ = self.compute_assoc_tys_for_impl(timpl.def_id); + let type_constraints = self.impl_assoc_tys[timpl.def_id] + .as_processed() + .unwrap() + .clone(); + let mut modifications = ItemModifications::from_constraint_set(type_constraints, true); + for clause in &timpl.generics.trait_clauses { + for path in self.compute_extra_params_for_clause(clause, TraitRefPath::local_clause) + { + modifications.replace_path(path); + } + } + modifications + } else { + let mut modifications = self.compute_non_trait_modifications(item.generic_params()); + // Trait method declarations have an implicit `Self` clause. We process it like a real + // clause. + if let AnyTransItem::Fun(FunDecl { + kind: ItemKind::TraitDecl { trait_ref, .. }, + .. + }) + | AnyTransItem::Global(GlobalDecl { + kind: ItemKind::TraitDecl { trait_ref, .. }, + .. + }) = item + { + let trait_id = trait_ref.trait_id; + if self.ctx.translated.trait_decls.get(trait_id).is_some() { + for path in self.compute_extra_params_for_trait(trait_id) { + modifications.replace_path(path.clone()); + } + } + } + modifications + } + } + + fn compute_non_trait_modifications(&mut self, params: &GenericParams) -> ItemModifications { + // For non-traits, we simply iterate through the clauses of the item and + // collect new paths to replace. + let mut modifications = ItemModifications::new(¶ms.trait_type_constraints, true); + // For each clause, we need to supply types for the new parameters. `replace_path` either + // finds the right type in the type constraints, or records that we need to add new + // parameters to this trait's signature. + for clause in ¶ms.trait_clauses { + for path in self.compute_extra_params_for_clause(clause, TraitRefPath::local_clause) { + modifications.replace_path(path); + } + } + modifications + } + + /// Returns the extra parameters that we add to the given trait. If we hadn't processed this + /// trait before, we modify it to add the parameters in question and remove its associated + /// types. + fn compute_extra_params_for_trait( + &mut self, + id: TraitDeclId, + ) -> impl Iterator { + if let Processing::Unprocessed = self.trait_modifications[id] { + if let Some(tr) = self.ctx.translated.trait_decls.get(id) { + // Put the sentinel value to detect loops. + self.trait_modifications[id] = Processing::Processing; + + // The heart of the recursion: we process the trait clauses, which recursively computes + // the extra parameters needed for each corresponding trait. Each of the referenced + // traits may need to be supplied extra type parameters. `replace_path` either finds + // the right type in the type constraints, or records that we need to add new + // parameters to this trait's signature. + let mut replace = vec![]; + for clause in &tr.generics.trait_clauses { + for path in + self.compute_extra_params_for_clause(clause, TraitRefPath::local_clause) + { + replace.push(path); + } + } + for clause in &tr.parent_clauses { + for path in + self.compute_extra_params_for_clause(clause, TraitRefPath::parent_clause) + { + replace.push(path); + } + } + + let is_self_referential = match &self.trait_modifications[id] { + Processing::Unprocessed | Processing::Processed(_) => unreachable!(), + Processing::Processing => false, + Processing::Cyclic => true, + }; + let remove_assoc_type = self + .ctx + .options + .remove_associated_types + .iter() + .any(|pat| pat.matches(&self.ctx.translated, &tr.item_meta.name)); + let remove_assoc_types = !is_self_referential && remove_assoc_type; + let mut modifications = + ItemModifications::new(&tr.generics.trait_type_constraints, remove_assoc_types); + if modifications.add_type_params { + // Remove all associated types and turn them into new parameters. We add these + // before the paths in `replace` because it's more logical to do the local + // types first. + for type_name in &tr.types { + let path = TraitRefPath::self_ref().with_assoc_type(type_name.clone()); + modifications.replace_path(path); + } + } + for path in replace { + modifications.replace_path(path); + } + + self.trait_modifications[id] = Processing::Processed(modifications); + } + } else if let Processing::Processing = self.trait_modifications[id] { + // This is already being processed: we encountered a cycle. + self.trait_modifications[id] = Processing::Cyclic; + } + + match &self.trait_modifications[id] { + Processing::Unprocessed => None, + Processing::Processing | Processing::Cyclic => { + // We're recursively processing ourselves. We already know we won't add new type + // parameters, so we correctly return an empty iterator. + None + } + Processing::Processed(modifs) => Some(modifs.required_extra_params()), + } + .into_iter() + .flatten() + } + + fn compute_extra_params_for_clause<'b, F>( + &'b mut self, + clause: &TraitClause, + clause_to_path: F, + ) -> impl Iterator + use<'b, F> + where + F: Fn(TraitClauseId) -> TraitRefPath, + { + let trait_id = clause.trait_.skip_binder.trait_id; + let clause_path = clause_to_path(clause.clause_id); + self.compute_extra_params_for_trait(trait_id) + .map(move |path| path.on_tref(&clause_path)) + } + + /// Returns the associated types values known for the given impl. If the impl is cyclic, the + /// set will not be exhaustive. + fn compute_assoc_tys_for_impl(&mut self, id: TraitImplId) -> Option<&TypeConstraintSet> { + if let Processing::Unprocessed = self.impl_assoc_tys[id] { + if let Some(timpl) = self.ctx.translated.trait_impls.get(id) { + // Put the sentinel value to detect loops. + self.impl_assoc_tys[id] = Processing::Processing; + + let mut set = + TypeConstraintSet::from_constraints(&timpl.generics.trait_type_constraints); + for (name, ty) in &timpl.types { + let path = TraitRefPath::self_ref().with_assoc_type(name.clone()); + set.insert_path(&path, ty.clone()); + } + for (clause_id, tref) in timpl.parent_trait_refs.iter_indexed() { + let clause_path = TraitRefPath::parent_clause(clause_id); + for (path, ty) in + self.compute_assoc_tys_for_tref(timpl.item_meta.span, &tref.kind) + { + let path = path.on_tref(&clause_path); + set.insert_path(&path, ty); + } + } + + self.impl_assoc_tys[id] = Processing::Processed(set); + } + } + self.impl_assoc_tys[id].as_processed() + } + + /// Returns the associated types values known for the given trait ref. + // TODO: also extract refs from `dyn Trait` refs. + fn compute_assoc_tys_for_tref( + &mut self, + span: Span, + tref: &TraitRefKind, + ) -> Vec<(AssocTypePath, Ty)> { + let mut out = vec![]; + match tref { + TraitRefKind::Clause(..) + | TraitRefKind::ParentClause(..) + | TraitRefKind::ItemClause(..) + | TraitRefKind::SelfId + | TraitRefKind::Unknown(_) => {} + TraitRefKind::TraitImpl(clause_impl_id, generics) => { + let generics = ItemBinder::new(CurrentItem, generics); + if let Some(set_for_clause) = self.compute_assoc_tys_for_impl(*clause_impl_id) { + for (path, ty) in set_for_clause.iter() { + let ty = ItemBinder::new(*clause_impl_id, ty) + .substitute(generics) + .under_current_binder(); + out.push((path, ty)); + } + } + } + TraitRefKind::BuiltinOrAuto { + parent_trait_refs, + types, + .. + } => { + for (name, ty) in types.iter().cloned() { + let path = TraitRefPath::self_ref().with_assoc_type(name); + out.push((path, ty)); + } + for (parent_clause_id, parent_ref) in parent_trait_refs.iter_indexed() { + let clause_path = TraitRefPath::parent_clause(parent_clause_id); + out.extend( + self.compute_assoc_tys_for_tref(span, &parent_ref.kind) + .into_iter() + .map(|(path, ty)| { + let path = path.on_tref(&clause_path); + (path, ty) + }), + ) + } + } + TraitRefKind::Dyn(..) => { + register_error!( + self.ctx, + span, + "Can't process associated types for `dyn Trait`" + ); + } + } + out + } +} + +/// Visitor that will traverse item bodies and update `GenericArgs` to match the new item +/// signatures. This also replaces `TyKind::TraitType`s for which we have a replacement. +/// +/// The tricky part is that to update `GenericArgs` that apply to traits, we need to know the +/// `TraitRef` they apply to in order to get the values of the appropriate types. To do this, +/// `visit_generic_args` will skip `GenericArgs` meant for traits, and we must manually catch +#[derive(Visitor)] +struct UpdateItemBody<'a> { + ctx: &'a TransformCtx, + span: Span, + item_modifications: &'a HashMap, + // It's a reversed stack, for when we go under binders. + type_replacements: BindingStack, +} + +impl UpdateItemBody<'_> { + fn under_binder(&mut self, repls: TypeConstraintSet, f: impl FnOnce(&mut Self) -> R) -> R { + self.type_replacements.push(repls); + let ret = f(self); + self.type_replacements.pop(); + ret + } + + fn lookup_type_replacement(&self, path: &AssocTypePath) -> Option { + let mut path = path.clone(); + let dbid = match &mut path.tref.base { + BaseClause::Local(DeBruijnVar::Bound(dbid, _)) => { + // Make the variable relative to the target item. Where clauses are always at + // binder level zero. + mem::replace(dbid, DeBruijnId::zero()) + } + _ => self.type_replacements.depth(), + }; + let ty = self.type_replacements[dbid].find(&path)?.1; + Some(ty.clone().move_under_binders(dbid)) + } + + fn lookup_path_on_trait_ref(&self, path: &AssocTypePath, tref: &TraitRefKind) -> Option { + assert!(path.tref.base.is_self_clause()); + match tref { + TraitRefKind::TraitImpl(impl_id, generics) => { + // The type constraints of trait impls already contain all relevant type + // equalities. + let (_, ty) = self + .item_modifications + .get(&GenericsSource::item(*impl_id))? + .type_constraints + .find(path)?; + Some( + ItemBinder::new(*impl_id, ty.clone()) + .substitute(ItemBinder::new(CurrentItem, generics)) + .under_current_binder(), + ) + } + TraitRefKind::Clause(..) + | TraitRefKind::ParentClause(..) + | TraitRefKind::ItemClause(..) + | TraitRefKind::SelfId => { + let path = path.on_tref(&tref.to_path().unwrap()); + self.lookup_type_replacement(&path) + } + TraitRefKind::BuiltinOrAuto { + parent_trait_refs, + types, + .. + } => match path.pop_first_parent() { + None => types + .iter() + .find(|(name, _)| name == &path.type_name) + .map(|(_, ty)| ty.clone()), + Some((parent_clause_id, sub_path)) => { + let parent_ref = &parent_trait_refs[parent_clause_id]; + self.lookup_path_on_trait_ref(&sub_path, &parent_ref.kind) + } + }, + // TODO: add enough info to recover assoc types. + TraitRefKind::Dyn(..) => None, + TraitRefKind::Unknown(..) => None, + } + } + + fn update_generics(&mut self, args: &mut GenericArgs, self_path: Option) { + let Some(modifications) = self.item_modifications.get(&args.target) else { + return; + }; + for path in modifications.required_extra_params() { + let mut path = path.clone(); + let base_tref = match path.tref.base { + BaseClause::SelfClause => { + match &self_path { + Some(self_path) => self_path, + None => { + // For traits we provide a `self_path`. The only other items that can + // have `Self` modifications are method/assoc global declarations. + // These are only referred to from a `TraitDecl`, so we know that their + // `Self` actually refers to the current `Self`. + match &args.target { + GenericsSource::Item(AnyTransId::Fun(_)) + | GenericsSource::Item(AnyTransId::Global(_)) => { + &TraitRefKind::SelfId + } + target => unreachable!( + "Found unexpected target with a `Self` \ + clause modification: {target:?}" + ), + } + } + } + } + BaseClause::Local(var) => { + let clause_id = var + .bound_at_depth(DeBruijnId::zero()) + .expect("found replacement not at binder level 0?"); + path = path.pop_base(); + &args.trait_refs[clause_id].kind + } + }; + if let Some(ty) = self.lookup_path_on_trait_ref(&path, &base_tref) { + args.types.push(ty.clone()); + } else { + let mut path = path; + if let Some(tref) = base_tref.to_path() { + path = path.on_tref(&tref); + } + register_error!( + self.ctx, + self.span, + "Could not compute the value of {path} needed to update \ + generics {args:?} for item {:?}.\ + \nConstraints in scope:\n{}", + args.target, + self.type_replacements + .iter() + .flat_map(|x| x.iter()) + .map(|(path, ty)| format!( + " - {path} = {}", + ty.fmt_with_ctx(&FmtCtx::new()) + )) + .join("\n"), + ); + } + } + } + + /// A `TraitDeclRef` must always be paired with a path in order to get access to the + /// appropriate associated types. We therefore ignore the trait args in `enter_generic_args`, + /// and must carefully call `process_trait_decl_ref` on all the right places of the AST to + /// catch the `GenericArgs` we skipped. + /// `TraitDeclRef`s exist in three places: in `TraitClause`, `TraitRef`, and directly in + /// `TraitImpl`. + fn process_trait_decl_ref(&mut self, tref: &mut TraitDeclRef, self_path: TraitRefKind) { + trace!("{tref:?}"); + self.update_generics(&mut tref.generics, Some(self_path)); + } + + /// See `process_trait_decl_ref`. + fn process_poly_trait_decl_ref( + &mut self, + tref: &mut PolyTraitDeclRef, + self_path: TraitRefKind, + ) { + trace!("{tref:?}"); + self.under_binder(Default::default(), |this| { + let self_path = self_path.move_under_binder(); + this.process_trait_decl_ref(&mut tref.skip_binder, self_path) + }); + } +} + +impl VisitAstMut for UpdateItemBody<'_> { + fn visit_binder( + &mut self, + binder: &mut Binder, + ) -> ControlFlow { + let generics = &mut binder.params; + let mut modifications; + let modifications = match &binder.kind { + BinderKind::TraitMethod(trait_id, method_name) => self + .item_modifications + .get(&GenericsSource::Method(*trait_id, method_name.clone())), + BinderKind::InherentImplBlock => { + // An inner binder. Because it's not a globally-addressable item, we haven't computed + // appropriate modifications yet, so we compute them. + modifications = ItemModifications::new(&generics.trait_type_constraints, true); + for clause in &generics.trait_clauses { + let trait_id = clause.trait_.skip_binder.trait_id; + if let Some(tmods) = + self.item_modifications.get(&GenericsSource::item(trait_id)) + { + for path in tmods.required_extra_params() { + let path = path.on_local_clause(clause.clause_id); + modifications.replace_path(path); + } + } + } + Some(&modifications) + } + BinderKind::Other => unreachable!("no `BinderKind::Other` in the AST"), + }; + let replacements = modifications + .map(|mods| { + mods.compute_replacements(|path| { + let var_id = generics + .types + .push_with(|id| TypeVar::new(id, path.to_name())); + TyKind::TypeVar(DeBruijnVar::new_at_zero(var_id)).into_ty() + }) + }) + .unwrap_or_default(); + self.under_binder(replacements, |this| { + this.visit_inner(binder); + }); + Continue(()) + } + + fn visit_region_binder( + &mut self, + binder: &mut RegionBinder, + ) -> ControlFlow { + self.under_binder(Default::default(), |this| { + this.visit_inner(binder); + }); + Continue(()) + } + + fn enter_trait_impl(&mut self, timpl: &mut TraitImpl) { + self.process_trait_decl_ref(&mut timpl.impl_trait, TraitRefKind::SelfId); + } + + fn enter_trait_decl(&mut self, tdecl: &mut TraitDecl) { + for (clause_id, clause) in tdecl.parent_clauses.iter_mut_indexed() { + let self_path = + TraitRefKind::ParentClause(Box::new(TraitRefKind::SelfId), tdecl.def_id, clause_id); + self.process_poly_trait_decl_ref(&mut clause.trait_, self_path); + } + } + + fn enter_generic_params(&mut self, params: &mut GenericParams) { + for (clause_id, clause) in params.trait_clauses.iter_mut_indexed() { + let self_path = TraitRefKind::Clause(DeBruijnVar::new_at_zero(clause_id)); + self.process_poly_trait_decl_ref(&mut clause.trait_, self_path); + } + } + + fn enter_generic_args(&mut self, args: &mut GenericArgs) { + if !matches!(args.target, GenericsSource::Item(AnyTransId::TraitDecl(..))) { + // To update `GenericArgs` that apply to traits we need to know the `TraitRef` they + // apply to. Hence we skip them here and we have to manually catch all these cases with + // `process_trait_decl_ref`. + self.update_generics(args, None); + } + } + + fn enter_trait_ref(&mut self, tref: &mut TraitRef) { + self.process_poly_trait_decl_ref(&mut tref.trait_decl_ref, tref.kind.clone()); + } + + fn enter_trait_ref_kind(&mut self, kind: &mut TraitRefKind) { + // There are some stray `TraitDeclRef`s that we have to update. + // TODO: we should make `TraitRefKind` recursively contain full `TraitRef`s so we have the + // implemented trait info at each level. This would require hax to give us more info. + let kind_clone = kind.clone(); + match kind { + TraitRefKind::BuiltinOrAuto { + trait_decl_ref: tref, + .. + } + | TraitRefKind::Dyn(tref) => { + self.process_poly_trait_decl_ref(tref, kind_clone); + } + _ => {} + } + } + + fn enter_item_kind(&mut self, kind: &mut ItemKind) { + match kind { + ItemKind::Regular => {} + // Inside method declarations, we have access to the implicit `Self` clause. + ItemKind::TraitDecl { trait_ref, .. } => { + self.process_trait_decl_ref(trait_ref, TraitRefKind::SelfId) + } + ItemKind::TraitImpl { + impl_ref, + trait_ref, + .. + } => self.process_trait_decl_ref( + trait_ref, + TraitRefKind::TraitImpl(impl_ref.impl_id, impl_ref.generics.clone()), + ), + } + } + + fn enter_ty_kind(&mut self, kind: &mut TyKind) { + if let TyKind::TraitType(tref, name) = kind { + let path = TraitRefPath::self_ref().with_assoc_type(name.clone()); + if let Some(new_ty) = self.lookup_path_on_trait_ref(&path, &tref.kind) { + *kind = new_ty.kind().clone(); + // Fix the newly-substituted type. + self.visit(kind); + } + } + } + + fn visit_ullbc_statement(&mut self, st: &mut ullbc_ast::Statement) -> ControlFlow { + // Track span for more precise error messages. + let old_span = self.span; + self.span = st.span; + self.visit_inner(st)?; + self.span = old_span; + Continue(()) + } + + fn visit_llbc_statement(&mut self, st: &mut llbc_ast::Statement) -> ControlFlow { + // Track span for more precise error messages. + let old_span = self.span; + self.span = st.span; + self.visit_inner(st)?; + self.span = old_span; + Continue(()) + } +} + +pub struct Transform; +impl TransformPass for Transform { + fn transform_ctx(&self, ctx: &mut TransformCtx) { + // Compute all the necessary type info to be able to replace and normalize associated + // types. + let item_modifications: HashMap = { + let mut computer = ComputeItemModifications::new(ctx); + let mut item_modifications = HashMap::new(); + for (id, item) in ctx.translated.all_items_with_ids() { + let modifications = computer.compute_item_modifications(item); + item_modifications.insert(GenericsSource::Item(id), modifications); + if let AnyTransItem::TraitDecl(tdecl) = item { + for (name, bound_fn) in + tdecl.required_methods.iter().chain(&tdecl.provided_methods) + { + let modifications = + computer.compute_non_trait_modifications(&bound_fn.params); + item_modifications.insert( + GenericsSource::Method(tdecl.def_id, name.clone()), + modifications, + ); + } + } + } + item_modifications + }; + + // Apply the computed modifications to each item. + ctx.for_each_item_mut(|ctx, mut item| { + let id = item.as_ref().id(); + let span = item.as_ref().item_meta().span; + let modifications = item_modifications.get(&GenericsSource::Item(id)).unwrap(); + + // Add new parameters or associated types in order to have types to fill in all the + // replaced paths. We then collect the replaced paths and their associated value. + let type_replacements: TypeConstraintSet = if let AnyTransItemMut::TraitDecl(tr) = + &mut item + && !modifications.add_type_params + { + // If we're self-referential, instead of adding new type parameters to pass to our + // parent clauses, we add new associated types. That way the parameter list of the + // trait stays unchanged. + let self_tref = TraitRef { + kind: TraitRefKind::SelfId, + trait_decl_ref: RegionBinder::empty(TraitDeclRef { + trait_id: tr.def_id, + generics: tr.generics.identity_args(GenericsSource::item(tr.def_id)), + }), + }; + modifications.compute_replacements(|path| { + let new_type_name = TraitItemName(path.to_name()); + tr.types.push(new_type_name.clone()); + TyKind::TraitType(self_tref.clone(), new_type_name).into_ty() + }) + } else { + modifications.compute_replacements(|path| { + let var_id = item + .generic_params() + .types + .push_with(|id| TypeVar::new(id, path.to_name())); + TyKind::TypeVar(DeBruijnVar::new_at_zero(var_id)).into_ty() + }) + }; + + // Remove used constraints. + for cid in &modifications.remove_constraints { + item.generic_params().trait_type_constraints.remove(*cid); + } + + // Remove trait associated types. + if let AnyTransItemMut::TraitDecl(tr) = &mut item + && modifications.add_type_params + { + tr.types.clear(); + } + + // Adjust impl associated types. + if let AnyTransItemMut::TraitImpl(timpl) = &mut item { + let trait_id = timpl.impl_trait.trait_id; + if let Some(decl_modifs) = item_modifications.get(&GenericsSource::item(trait_id)) { + if decl_modifs.add_type_params { + timpl.types.clear(); + } + for path in decl_modifs.required_extra_assoc_types() { + let new_type_name = TraitItemName(path.to_name()); + if let Some((_, ty)) = type_replacements.find(&path) { + trace!("Adding associated type {new_type_name} = {ty:?}"); + timpl.types.push((new_type_name, ty.clone())); + } else { + register_error!( + ctx, + span, + "Could not figure out type for new associated type {new_type_name}.\ + \nAvailable: {:?}", + type_replacements + ); + } + } + } + } + + // Update the rest of the items: all the `GenericArgs` and the non-top-level binders + // (trait methods and inherent impls in `Name`s). + item.drive_mut(&mut UpdateItemBody { + ctx, + span, + item_modifications: &item_modifications, + type_replacements: BindingStack::new(type_replacements), + }); + }); + } +} diff --git a/charon/src/transform/graphs.rs b/charon/src/transform/graphs.rs index 04a1ff13..9e9c717e 100644 --- a/charon/src/transform/graphs.rs +++ b/charon/src/transform/graphs.rs @@ -1,4 +1,4 @@ -use hashlink::LinkedHashSet; +use indexmap::IndexSet; use std::collections::BTreeSet as OrdSet; use std::collections::HashMap; use std::iter::FromIterator; @@ -23,7 +23,7 @@ pub struct SCCs { /// We also compute the SCC dependencies while performing this exploration. fn insert_scc_with_deps( get_id_dependencies: &dyn Fn(Id) -> Vec, - reordered_sccs: &mut LinkedHashSet, + reordered_sccs: &mut IndexSet, scc_deps: &mut Vec>, sccs: &Vec>, id_to_scc: &HashMap, @@ -131,7 +131,7 @@ pub fn reorder_sccs( // Reorder the SCCs themselves - just do a depth first search. Iterate over // the def ids, and add the corresponding SCCs (with their dependencies). - let mut reordered_sccs_ids = LinkedHashSet::::new(); + let mut reordered_sccs_ids = IndexSet::::new(); let mut scc_deps: Vec> = reordered_sccs.iter().map(|_| OrdSet::new()).collect(); for id in ids { let scc_id = id_to_scc.get(id).unwrap(); diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index f4fa13ce..b919f011 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -1,6 +1,7 @@ pub mod check_generics; pub mod ctx; pub mod duplicate_return; +pub mod expand_associated_types; pub mod filter_invisible_trait_impls; pub mod filter_unreachable_blocks; pub mod graphs; @@ -39,6 +40,7 @@ pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[ // Move clauses on associated types to be parent clauses NonBody(&lift_associated_item_clauses::Transform), // Check that all supplied generic types match the corresponding generic parameters. + // Needs `lift_associated_item_clauses`. NonBody(&check_generics::Check("after translation")), // # Micro-pass: hide some overly-common traits we don't need: Sized, Sync, Allocator, etc.. NonBody(&hide_marker_traits::Transform), @@ -49,6 +51,8 @@ pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[ // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove // some sources of mutual recursion. UnstructuredBody(&skip_trait_refs_when_known::Transform), + // Change trait associated types to be type parameters instead. See the module for details. + NonBody(&expand_associated_types::Transform), ]; /// Body cleanup passes on the ullbc. diff --git a/charon/src/transform/reorder_decls.rs b/charon/src/transform/reorder_decls.rs index 0807eaa2..966eca6a 100644 --- a/charon/src/transform/reorder_decls.rs +++ b/charon/src/transform/reorder_decls.rs @@ -4,7 +4,7 @@ use crate::graphs::*; use crate::transform::TransformCtx; use crate::ullbc_ast::*; use derive_generic_visitor::*; -use hashlink::{LinkedHashMap, LinkedHashSet}; +use indexmap::{IndexMap, IndexSet}; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use petgraph::algo::tarjan_scc; use petgraph::graphmap::DiGraphMap; @@ -153,7 +153,7 @@ impl Display for DeclarationGroup { pub struct Deps { dgraph: DiGraphMap, // Want to make sure we remember the order of insertion - graph: LinkedHashMap>, + graph: IndexMap>, // We use this when computing the graph current_id: Option, // We use this to track the trait impl block the current item belongs to @@ -205,7 +205,7 @@ impl Deps { fn new() -> Self { Deps { dgraph: DiGraphMap::new(), - graph: LinkedHashMap::new(), + graph: IndexMap::new(), current_id: None, parent_trait_impl: None, parent_trait_decl: None, @@ -253,7 +253,7 @@ impl Deps { if !self.dgraph.contains_node(id) { self.dgraph.add_node(id); assert!(!self.graph.contains_key(&id)); - self.graph.insert(id, LinkedHashSet::new()); + self.graph.insert(id, IndexSet::new()); } } diff --git a/charon/src/transform/ullbc_to_llbc.rs b/charon/src/transform/ullbc_to_llbc.rs index e28b6df5..818cbb0e 100644 --- a/charon/src/transform/ullbc_to_llbc.rs +++ b/charon/src/transform/ullbc_to_llbc.rs @@ -28,7 +28,7 @@ use crate::llbc_ast as tgt; use crate::meta::{combine_span, Span}; use crate::transform::TransformCtx; use crate::ullbc_ast::{self as src}; -use hashlink::linked_hash_map::LinkedHashMap; +use indexmap::IndexMap; use itertools::Itertools; use num_bigint::BigInt; use num_rational::BigRational; @@ -365,7 +365,7 @@ fn list_reachable(cfg: &Cfg, start: src::BlockId) -> HashMap>, + loop_exits: &mut HashMap>, removed_parent_loops: &Vec<(src::BlockId, usize)>, block_id: src::BlockId, ) { @@ -412,7 +412,7 @@ fn compute_loop_exit_candidates( cfg: &CfgInfo, explored: &mut HashSet, ordered_loops: &mut Vec, - loop_exits: &mut HashMap>, + loop_exits: &mut HashMap>, // List of parent loops, with the distance to the entry of the loop (the distance // is the distance between the current node and the loop entry for the last parent, // and the distance between the parents for the others). @@ -638,7 +638,7 @@ fn compute_loop_exits( // Initialize the loop exits candidates for loop_id in &cfg.loop_entries { - loop_exits.insert(*loop_id, LinkedHashMap::new()); + loop_exits.insert(*loop_id, IndexMap::new()); } // Compute the candidates @@ -1543,8 +1543,8 @@ fn translate_terminator( // We link block ids to: // - vector of matched integer values // - translated blocks - let mut branches: LinkedHashMap, tgt::Block)> = - LinkedHashMap::new(); + let mut branches: IndexMap, tgt::Block)> = + IndexMap::new(); // Translate the children expressions for (v, bid) in targets.iter() { diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 8fc2d33c..0c543a3d 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -250,62 +250,60 @@ enum core::option::Option | Some(T) -trait core::slice::index::SliceIndex +trait core::slice::index::SliceIndex { parent_clause0 : [@TraitClause0]: core::slice::index::private_slice_index::Sealed - type Output - fn get<'_0> = core::slice::index::SliceIndex::get<'_0_0, Self, T> - fn get_mut<'_0> = core::slice::index::SliceIndex::get_mut<'_0_0, Self, T> - fn get_unchecked = core::slice::index::SliceIndex::get_unchecked - fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut - fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T> - fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T> + fn get<'_0> = core::slice::index::SliceIndex::get<'_0_0, Self, T, Self_Output> + fn get_mut<'_0> = core::slice::index::SliceIndex::get_mut<'_0_0, Self, T, Self_Output> + fn get_unchecked = core::slice::index::SliceIndex::get_unchecked + fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut + fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T, Self_Output> + fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T, Self_Output> } -fn core::slice::index::{impl core::ops::index::Index for Slice}::index<'_0, T, I>(@1: &'_0 (Slice), @2: I) -> &'_0 (@TraitClause2::Output) +fn core::slice::index::{impl core::ops::index::Index for Slice}::index<'_0, T, I, Clause2_Output>(@1: &'_0 (Slice), @2: I) -> &'_0 (Clause2_Output) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::slice::index::SliceIndex>, + [@TraitClause2]: core::slice::index::SliceIndex, Clause2_Output>, impl core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for core::ops::range::Range[core::marker::Sized]}#1 : core::slice::index::private_slice_index::Sealed[core::marker::Sized]> -fn core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 (Slice)) -> core::option::Option<&'_0 (Slice)>[core::marker::Sized<&'_0 (Slice)>] +fn core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 (Slice)) -> core::option::Option<&'_0 (Slice)>[core::marker::Sized<&'_0 (Slice)>] where [@TraitClause0]: core::marker::Sized, -fn core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get_mut<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 mut (Slice)) -> core::option::Option<&'_0 mut (Slice)>[core::marker::Sized<&'_0 mut (Slice)>] +fn core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get_mut<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 mut (Slice)) -> core::option::Option<&'_0 mut (Slice)>[core::marker::Sized<&'_0 mut (Slice)>] where [@TraitClause0]: core::marker::Sized, -unsafe fn core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked(@1: core::ops::range::Range[core::marker::Sized], @2: *const Slice) -> *const Slice +unsafe fn core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked(@1: core::ops::range::Range[core::marker::Sized], @2: *const Slice) -> *const Slice where [@TraitClause0]: core::marker::Sized, -unsafe fn core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked_mut(@1: core::ops::range::Range[core::marker::Sized], @2: *mut Slice) -> *mut Slice +unsafe fn core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked_mut(@1: core::ops::range::Range[core::marker::Sized], @2: *mut Slice) -> *mut Slice where [@TraitClause0]: core::marker::Sized, -fn core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::index<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 (Slice)) -> &'_0 (Slice) +fn core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::index<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 (Slice)) -> &'_0 (Slice) where [@TraitClause0]: core::marker::Sized, -fn core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::index_mut<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 mut (Slice)) -> &'_0 mut (Slice) +fn core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::index_mut<'_0, T>(@1: core::ops::range::Range[core::marker::Sized], @2: &'_0 mut (Slice)) -> &'_0 mut (Slice) where [@TraitClause0]: core::marker::Sized, -impl core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4 : core::slice::index::SliceIndex[core::marker::Sized], Slice> +impl core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4 : core::slice::index::SliceIndex[core::marker::Sized], Slice, Slice> where [@TraitClause0]: core::marker::Sized, { parent_clause0 = core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for core::ops::range::Range[core::marker::Sized]}#1 - type Output = Slice - fn get<'_0> = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get<'_0_0, T>[@TraitClause0] - fn get_mut<'_0> = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get_mut<'_0_0, T>[@TraitClause0] - fn get_unchecked = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked[@TraitClause0] - fn get_unchecked_mut = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked_mut[@TraitClause0] - fn index<'_0> = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::index<'_0_0, T>[@TraitClause0] - fn index_mut<'_0> = core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4::index_mut<'_0_0, T>[@TraitClause0] + fn get<'_0> = core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get<'_0_0, T>[@TraitClause0] + fn get_mut<'_0> = core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get_mut<'_0_0, T>[@TraitClause0] + fn get_unchecked = core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked[@TraitClause0] + fn get_unchecked_mut = core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::get_unchecked_mut[@TraitClause0] + fn index<'_0> = core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::index<'_0_0, T>[@TraitClause0] + fn index_mut<'_0> = core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4::index_mut<'_0_0, T>[@TraitClause0] } fn test_crate::slice_subslice_shared_<'_0>(@1: &'_0 (Slice), @2: usize, @3: usize) -> &'_0 (Slice) @@ -327,7 +325,7 @@ fn test_crate::slice_subslice_shared_<'_0>(@1: &'_0 (Slice), @2: usize, @3: @7 := core::ops::range::Range { start: move (@8), end: move (@9) } drop @9 drop @8 - @5 := core::slice::index::{impl core::ops::index::Index for Slice}::index<'_, u32, core::ops::range::Range[core::marker::Sized]>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]](move (@6), move (@7)) + @5 := core::slice::index::{impl core::ops::index::Index for Slice}::index<'_, u32, core::ops::range::Range[core::marker::Sized], Slice>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]](move (@6), move (@7)) drop @7 drop @6 @4 := &*(@5) @@ -337,11 +335,11 @@ fn test_crate::slice_subslice_shared_<'_0>(@1: &'_0 (Slice), @2: usize, @3: return } -fn core::slice::index::{impl core::ops::index::IndexMut for Slice}#1::index_mut<'_0, T, I>(@1: &'_0 mut (Slice), @2: I) -> &'_0 mut (@TraitClause2::Output) +fn core::slice::index::{impl core::ops::index::IndexMut for Slice}#1::index_mut<'_0, T, I, Clause2_Output>(@1: &'_0 mut (Slice), @2: I) -> &'_0 mut (Clause2_Output) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::slice::index::SliceIndex>, + [@TraitClause2]: core::slice::index::SliceIndex, Clause2_Output>, fn test_crate::slice_subslice_mut_<'_0>(@1: &'_0 mut (Slice), @2: usize, @3: usize) -> &'_0 mut (Slice) { @@ -363,7 +361,7 @@ fn test_crate::slice_subslice_mut_<'_0>(@1: &'_0 mut (Slice), @2: usize, @3 @8 := core::ops::range::Range { start: move (@9), end: move (@10) } drop @10 drop @9 - @6 := core::slice::index::{impl core::ops::index::IndexMut for Slice}#1::index_mut<'_, u32, core::ops::range::Range[core::marker::Sized]>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]](move (@7), move (@8)) + @6 := core::slice::index::{impl core::ops::index::IndexMut for Slice}#1::index_mut<'_, u32, core::ops::range::Range[core::marker::Sized], Slice>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]](move (@7), move (@8)) drop @8 drop @7 @5 := &mut *(@6) @@ -402,26 +400,24 @@ fn test_crate::array_to_slice_mut_<'_0>(@1: &'_0 mut (Array)) - return } -trait core::ops::index::Index +trait core::ops::index::Index { - type Output - fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx> + fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx, Self_Output> } -fn core::array::{impl core::ops::index::Index for Array}#15::index<'_0, T, I, const N : usize>(@1: &'_0 (Array), @2: I) -> &'_0 (core::array::{impl core::ops::index::Index for Array}#15[@TraitClause0, @TraitClause1, @TraitClause2]::Output) +fn core::array::{impl core::ops::index::Index for Array}#15::index<'_0, T, I, Clause2_Output, const N : usize>(@1: &'_0 (Array), @2: I) -> &'_0 (Clause2_Output) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::ops::index::Index, I>, + [@TraitClause2]: core::ops::index::Index, I, Clause2_Output>, -impl core::slice::index::{impl core::ops::index::Index for Slice} : core::ops::index::Index, I> +impl core::slice::index::{impl core::ops::index::Index for Slice} : core::ops::index::Index, I, Clause2_Output> where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::slice::index::SliceIndex>, + [@TraitClause2]: core::slice::index::SliceIndex, Clause2_Output>, { - type Output = @TraitClause2::Output - fn index<'_0> = core::slice::index::{impl core::ops::index::Index for Slice}::index<'_0_0, T, I>[@TraitClause0, @TraitClause1, @TraitClause2] + fn index<'_0> = core::slice::index::{impl core::ops::index::Index for Slice}::index<'_0_0, T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2] } fn test_crate::array_subslice_shared_<'_0>(@1: &'_0 (Array), @2: usize, @3: usize) -> &'_0 (Slice) @@ -443,7 +439,7 @@ fn test_crate::array_subslice_shared_<'_0>(@1: &'_0 (Array), @2 @7 := core::ops::range::Range { start: move (@8), end: move (@9) } drop @9 drop @8 - @5 := core::array::{impl core::ops::index::Index for Array}#15::index<'_, u32, core::ops::range::Range[core::marker::Sized], 32 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::Index for Slice}[core::marker::Sized]>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@6), move (@7)) + @5 := core::array::{impl core::ops::index::Index for Array}#15::index<'_, u32, core::ops::range::Range[core::marker::Sized], Slice, 32 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::Index for Slice}[core::marker::Sized], Slice>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@6), move (@7)) drop @7 drop @6 @4 := &*(@5) @@ -453,36 +449,26 @@ fn test_crate::array_subslice_shared_<'_0>(@1: &'_0 (Array), @2 return } -trait core::ops::index::IndexMut +trait core::ops::index::IndexMut { - parent_clause0 : [@TraitClause0]: core::ops::index::Index - fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx> + parent_clause0 : [@TraitClause0]: core::ops::index::Index + fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx, Self_Clause0_Output> } -impl core::array::{impl core::ops::index::Index for Array}#15 : core::ops::index::Index, I> +fn core::array::{impl core::ops::index::IndexMut for Array}#16::index_mut<'_0, T, I, Clause2_Clause0_Output, const N : usize>(@1: &'_0 mut (Array), @2: I) -> &'_0 mut (Clause2_Clause0_Output) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::ops::index::Index, I>, -{ - type Output = @TraitClause2::Output - fn index<'_0> = core::array::{impl core::ops::index::Index for Array}#15::index<'_0_0, T, I, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] -} - -fn core::array::{impl core::ops::index::IndexMut for Array}#16::index_mut<'_0, T, I, const N : usize>(@1: &'_0 mut (Array), @2: I) -> &'_0 mut (core::array::{impl core::ops::index::Index for Array}#15[@TraitClause0, @TraitClause1, @TraitClause2::parent_clause0]::Output) -where - [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::ops::index::IndexMut, I>, + [@TraitClause2]: core::ops::index::IndexMut, I, Clause2_Clause0_Output>, -impl core::slice::index::{impl core::ops::index::IndexMut for Slice}#1 : core::ops::index::IndexMut, I> +impl core::slice::index::{impl core::ops::index::IndexMut for Slice}#1 : core::ops::index::IndexMut, I, Clause2_Output> where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::slice::index::SliceIndex>, + [@TraitClause2]: core::slice::index::SliceIndex, Clause2_Output>, { - parent_clause0 = core::slice::index::{impl core::ops::index::Index for Slice}[@TraitClause0, @TraitClause1, @TraitClause2] - fn index_mut<'_0> = core::slice::index::{impl core::ops::index::IndexMut for Slice}#1::index_mut<'_0_0, T, I>[@TraitClause0, @TraitClause1, @TraitClause2] + parent_clause0 = core::slice::index::{impl core::ops::index::Index for Slice}[@TraitClause0, @TraitClause1, @TraitClause2] + fn index_mut<'_0> = core::slice::index::{impl core::ops::index::IndexMut for Slice}#1::index_mut<'_0_0, T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2] } fn test_crate::array_subslice_mut_<'_0>(@1: &'_0 mut (Array), @2: usize, @3: usize) -> &'_0 mut (Slice) @@ -505,7 +491,7 @@ fn test_crate::array_subslice_mut_<'_0>(@1: &'_0 mut (Array), @ @8 := core::ops::range::Range { start: move (@9), end: move (@10) } drop @10 drop @9 - @6 := core::array::{impl core::ops::index::IndexMut for Array}#16::index_mut<'_, u32, core::ops::range::Range[core::marker::Sized], 32 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::IndexMut for Slice}#1[core::marker::Sized]>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@7), move (@8)) + @6 := core::array::{impl core::ops::index::IndexMut for Array}#16::index_mut<'_, u32, core::ops::range::Range[core::marker::Sized], Slice, 32 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::IndexMut for Slice}#1[core::marker::Sized], Slice>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@7), move (@8)) drop @8 drop @7 @5 := &mut *(@6) @@ -1104,7 +1090,7 @@ fn test_crate::range_all() // CONFIRM: there is no way to shrink [T;N] into [T;M] with M for Array}#16::index_mut<'_, u32, core::ops::range::Range[core::marker::Sized], 4 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::IndexMut for Slice}#1[core::marker::Sized]>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@6), move (@7)) + @5 := core::array::{impl core::ops::index::IndexMut for Array}#16::index_mut<'_, u32, core::ops::range::Range[core::marker::Sized], Slice, 4 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::IndexMut for Slice}#1[core::marker::Sized], Slice>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@6), move (@7)) drop @7 drop @6 @4 := &mut *(@5) @@ -1457,7 +1443,7 @@ fn test_crate::f4<'_0>(@1: &'_0 (Array), @2: usize, @3: usize) @7 := core::ops::range::Range { start: move (@8), end: move (@9) } drop @9 drop @8 - @5 := core::array::{impl core::ops::index::Index for Array}#15::index<'_, u32, core::ops::range::Range[core::marker::Sized], 32 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::Index for Slice}[core::marker::Sized]>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@6), move (@7)) + @5 := core::array::{impl core::ops::index::Index for Array}#15::index<'_, u32, core::ops::range::Range[core::marker::Sized], Slice, 32 : usize>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::ops::index::Index for Slice}[core::marker::Sized], Slice>[core::marker::Sized, core::marker::Sized[core::marker::Sized]>, core::slice::index::{impl core::slice::index::SliceIndex, Slice> for core::ops::range::Range[core::marker::Sized]}#4[core::marker::Sized]]](move (@6), move (@7)) drop @7 drop @6 @4 := &*(@5) @@ -1874,31 +1860,40 @@ fn test_crate::slice_pattern_4<'_0>(@1: &'_0 (Slice<()>)) return } -fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output) +fn core::ops::index::Index::index<'_0, Self, Idx, Self_Output>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self_Output) -fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (Self::parent_clause0::Output) +fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx, Self_Clause0_Output>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (Self_Clause0_Output) + +impl core::array::{impl core::ops::index::Index for Array}#15 : core::ops::index::Index, I, Clause2_Output> +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: core::ops::index::Index, I, Clause2_Output>, +{ + fn index<'_0> = core::array::{impl core::ops::index::Index for Array}#15::index<'_0_0, T, I, Clause2_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] +} -impl core::array::{impl core::ops::index::IndexMut for Array}#16 : core::ops::index::IndexMut, I> +impl core::array::{impl core::ops::index::IndexMut for Array}#16 : core::ops::index::IndexMut, I, Clause2_Clause0_Output> where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::ops::index::IndexMut, I>, + [@TraitClause2]: core::ops::index::IndexMut, I, Clause2_Clause0_Output>, { - parent_clause0 = core::array::{impl core::ops::index::Index for Array}#15[@TraitClause0, @TraitClause1, @TraitClause2::parent_clause0] - fn index_mut<'_0> = core::array::{impl core::ops::index::IndexMut for Array}#16::index_mut<'_0_0, T, I, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] + parent_clause0 = core::array::{impl core::ops::index::Index for Array}#15[@TraitClause0, @TraitClause1, @TraitClause2::parent_clause0] + fn index_mut<'_0> = core::array::{impl core::ops::index::IndexMut for Array}#16::index_mut<'_0_0, T, I, Clause2_Clause0_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2] } -fn core::slice::index::SliceIndex::get<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> core::option::Option<&'_0 (Self::Output)>[core::marker::Sized<&'_0 (Self::Output)>] +fn core::slice::index::SliceIndex::get<'_0, Self, T, Self_Output>(@1: Self, @2: &'_0 (T)) -> core::option::Option<&'_0 (Self_Output)>[core::marker::Sized<&'_0 (Self_Output)>] -fn core::slice::index::SliceIndex::get_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> core::option::Option<&'_0 mut (Self::Output)>[core::marker::Sized<&'_0 mut (Self::Output)>] +fn core::slice::index::SliceIndex::get_mut<'_0, Self, T, Self_Output>(@1: Self, @2: &'_0 mut (T)) -> core::option::Option<&'_0 mut (Self_Output)>[core::marker::Sized<&'_0 mut (Self_Output)>] -unsafe fn core::slice::index::SliceIndex::get_unchecked(@1: Self, @2: *const T) -> *const Self::Output +unsafe fn core::slice::index::SliceIndex::get_unchecked(@1: Self, @2: *const T) -> *const Self_Output -unsafe fn core::slice::index::SliceIndex::get_unchecked_mut(@1: Self, @2: *mut T) -> *mut Self::Output +unsafe fn core::slice::index::SliceIndex::get_unchecked_mut(@1: Self, @2: *mut T) -> *mut Self_Output -fn core::slice::index::SliceIndex::index<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> &'_0 (Self::Output) +fn core::slice::index::SliceIndex::index<'_0, Self, T, Self_Output>(@1: Self, @2: &'_0 (T)) -> &'_0 (Self_Output) -fn core::slice::index::SliceIndex::index_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> &'_0 mut (Self::Output) +fn core::slice::index::SliceIndex::index_mut<'_0, Self, T, Self_Output>(@1: Self, @2: &'_0 mut (T)) -> &'_0 mut (Self_Output) diff --git a/charon/tests/ui/arrays.rs b/charon/tests/ui/arrays.rs index eed5f333..b5d11413 100644 --- a/charon/tests/ui/arrays.rs +++ b/charon/tests/ui/arrays.rs @@ -1,3 +1,4 @@ +//@ charon-args=--remove-associated-types=* //! Exercise the translation of arrays, with features supported by Eurydice pub enum AB { diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out index 754aa9e3..f867e596 100644 --- a/charon/tests/ui/associated-types.out +++ b/charon/tests/ui/associated-types.out @@ -14,17 +14,25 @@ trait core::marker::Copy parent_clause0 : [@TraitClause0]: core::clone::Clone } -trait test_crate::Foo<'a, Self> +trait test_crate::Foo<'a, Self, Self_Item> where - Self::Item : 'a, + Self_Item : 'a, { parent_clause0 : [@TraitClause0]: core::marker::Copy - parent_clause1 : [@TraitClause1]: core::marker::Sized - parent_clause2 : [@TraitClause2]: core::clone::Clone - type Item - fn use_item<'_0> = test_crate::Foo::use_item<'a, '_0_0, Self> + parent_clause1 : [@TraitClause1]: core::marker::Sized + parent_clause2 : [@TraitClause2]: core::clone::Clone + fn use_item_required = test_crate::Foo::use_item_required<'a, Self, Self_Item> + fn use_item_provided> = test_crate::Foo::use_item_provided<'a, Self, Clause0_Item, Self_Item>[@TraitClause0_0] } +enum core::option::Option + where + [@TraitClause0]: core::marker::Sized, + = +| None() +| Some(T) + + fn core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3::clone<'_0, '_1, T>(@1: &'_1 (&'_0 (T))) -> &'_0 (T) impl<'_0, T> core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_0, T> : core::clone::Clone<&'_0 (T)> @@ -38,14 +46,6 @@ impl<'_0, T> core::marker::{impl core::marker::Copy for &'_0 (T)}#4<'_0, T> : co parent_clause0 = core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, T> } -enum core::option::Option - where - [@TraitClause0]: core::marker::Sized, - = -| None() -| Some(T) - - fn core::option::{impl core::clone::Clone for core::option::Option[@TraitClause0]}#5::clone<'_0, T>(@1: &'_0 (core::option::Option[@TraitClause0])) -> core::option::Option[@TraitClause0] where [@TraitClause0]: core::marker::Sized, @@ -66,31 +66,90 @@ where fn clone_from<'_0, '_1> = core::option::{impl core::clone::Clone for core::option::Option[@TraitClause0]}#5::clone_from<'_0_0, '_0_1, T>[@TraitClause0, @TraitClause1] } -impl<'a, T> test_crate::{impl test_crate::Foo<'a> for &'a (T)}<'a, T> : test_crate::Foo<'a, &'a (T)> +fn test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_required<'a, T>(@1: core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]) -> core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>] +where + [@TraitClause0]: core::marker::Sized, +{ + let @0: core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]; // return + let x@1: core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]; // arg #1 + + @0 := copy (x@1) + return +} + +impl<'a, T> test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}<'a, T> : test_crate::Foo<'a, &'a (T), core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> where [@TraitClause0]: core::marker::Sized, { parent_clause0 = core::marker::{impl core::marker::Copy for &'_0 (T)}#4<'_, T> parent_clause1 = core::marker::Sized[core::marker::Sized<&'_ (T)>]> parent_clause2 = core::option::{impl core::clone::Clone for core::option::Option[@TraitClause0]}#5<&'_ (T)>[core::marker::Sized<&'_ (T)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, T>] - type Item = core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>] + fn use_item_required = test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_required<'a, T>[@TraitClause0] } -fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self +impl core::option::{impl core::marker::Copy for core::option::Option[@TraitClause0]}#44 : core::marker::Copy[@TraitClause0]> +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Copy, +{ + parent_clause0 = core::option::{impl core::clone::Clone for core::option::Option[@TraitClause0]}#5[@TraitClause0, @TraitClause1::parent_clause0] +} -fn test_crate::external_use_item<'a, T>(@1: @TraitClause1::Item) -> @TraitClause1::Item +fn test_crate::{impl test_crate::Foo<'a, T> for core::option::Option[@TraitClause0]}#1::use_item_required<'a, T>(@1: T) -> T where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::Foo<'_, T>, + [@TraitClause1]: core::marker::Copy, { - let @0: @TraitClause1::Item; // return - let x@1: @TraitClause1::Item; // arg #1 - let @2: &'_ (@TraitClause1::Item); // anonymous local + let @0: T; // return + let x@1: T; // arg #1 - @2 := &x@1 - @0 := @TraitClause1::parent_clause2::clone<'_>(move (@2)) + @0 := copy (x@1) + return +} + +impl<'a, T> test_crate::{impl test_crate::Foo<'a, T> for core::option::Option[@TraitClause0]}#1<'a, T> : test_crate::Foo<'a, core::option::Option[@TraitClause0], T> +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Copy, +{ + parent_clause0 = core::option::{impl core::marker::Copy for core::option::Option[@TraitClause0]}#44[@TraitClause0, @TraitClause1] + parent_clause1 = @TraitClause0 + parent_clause2 = @TraitClause1::parent_clause0 + fn use_item_required = test_crate::{impl test_crate::Foo<'a, T> for core::option::Option[@TraitClause0]}#1::use_item_required<'a, T>[@TraitClause0, @TraitClause1] +} + +fn test_crate::Foo::use_item_provided<'a, Self, Clause0_Item, Self_Item>(@1: Self_Item) -> Self_Item +where + [@TraitClause0]: test_crate::Foo<'_, Self_Item, Clause0_Item>, +{ + let @0: Self_Item; // return + let x@1: Self_Item; // arg #1 + + @0 := copy (x@1) + return +} + +fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self + +fn test_crate::external_use_item<'a, T, Clause1_Item, Clause2_Item>(@1: Clause1_Item) -> Clause1_Item +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: test_crate::Foo<'_, T, Clause1_Item>, + [@TraitClause2]: test_crate::Foo<'_, Clause1_Item, Clause2_Item>, +{ + let @0: Clause1_Item; // return + let x@1: Clause1_Item; // arg #1 + let @2: &'_ (Clause1_Item); // anonymous local + let @3: Clause1_Item; // anonymous local + let @4: Clause1_Item; // anonymous local + + @4 := copy (x@1) + @3 := @TraitClause1::use_item_provided[@TraitClause2](move (@4)) + @2 := &@3 + drop @4 + @0 := @TraitClause2::parent_clause0::parent_clause0::clone<'_>(move (@2)) drop @2 - drop x@1 + drop @3 return } @@ -102,7 +161,7 @@ fn test_crate::call_fn() let @3: (); // anonymous local @2 := core::option::Option::None { } - @1 := test_crate::external_use_item<'_, &'_ (bool)>[core::marker::Sized<&'_ (bool)>, test_crate::{impl test_crate::Foo<'a> for &'a (T)}<'_, bool>[core::marker::Sized]](move (@2)) + @1 := test_crate::external_use_item<'_, &'_ (bool), core::option::Option<&'_ (bool)>[core::marker::Sized<&'_ (bool)>], &'_ (bool)>[core::marker::Sized<&'_ (bool)>, test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}<'_, bool>[core::marker::Sized], test_crate::{impl test_crate::Foo<'a, T> for core::option::Option[@TraitClause0]}#1<'_, &'_ (bool)>[core::marker::Sized<&'_ (bool)>, core::marker::{impl core::marker::Copy for &'_0 (T)}#4<'_, bool>]](move (@2)) drop @2 @fake_read(@1) drop @1 @@ -112,84 +171,83 @@ fn test_crate::call_fn() return } -fn test_crate::type_equality<'a, I, J>(@1: @TraitClause2::Item) -> @TraitClause3::Item +fn test_crate::type_equality<'a, I, J, Clause2_Item>(@1: Clause2_Item) -> Clause2_Item where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: test_crate::Foo<'_, I>, - [@TraitClause3]: test_crate::Foo<'_, J>, - @TraitClause3::Item = @TraitClause2::Item, + [@TraitClause2]: test_crate::Foo<'_, I, Clause2_Item>, + [@TraitClause3]: test_crate::Foo<'_, J, Clause2_Item>, { - let @0: @TraitClause2::Item; // return - let x@1: @TraitClause2::Item; // arg #1 + let @0: Clause2_Item; // return + let x@1: Clause2_Item; // arg #1 @0 := move (x@1) drop x@1 return } -trait test_crate::loopy::Bar +trait test_crate::loopy::Bar { - parent_clause0 : [@TraitClause0]: core::marker::Sized - type BarTy + parent_clause0 : [@TraitClause0]: core::marker::Sized } -impl test_crate::loopy::{impl test_crate::loopy::Bar for ()} : test_crate::loopy::Bar<()> +impl test_crate::loopy::{impl test_crate::loopy::Bar for ()} : test_crate::loopy::Bar<(), bool> { parent_clause0 = core::marker::Sized - type BarTy = bool } trait test_crate::loopy::Foo { parent_clause0 : [@TraitClause0]: core::marker::Sized parent_clause1 : [@TraitClause1]: test_crate::loopy::Foo - parent_clause2 : [@TraitClause2]: test_crate::loopy::Bar + parent_clause2 : [@TraitClause2]: test_crate::loopy::Bar type FooTy + type Self_Clause2_BarTy } impl test_crate::loopy::{impl test_crate::loopy::Foo for ()}#1 : test_crate::loopy::Foo<()> { parent_clause0 = core::marker::Sized<()> parent_clause1 = test_crate::loopy::{impl test_crate::loopy::Foo for ()}#1 - parent_clause2 = test_crate::loopy::{impl test_crate::loopy::Bar for ()} + parent_clause2 = test_crate::loopy::{impl test_crate::loopy::Bar for ()} type FooTy = () + type Self_Clause2_BarTy = bool } trait test_crate::loopy::Baz { parent_clause0 : [@TraitClause0]: core::marker::Sized parent_clause1 : [@TraitClause1]: test_crate::loopy::Baz - parent_clause2 : [@TraitClause2]: test_crate::loopy::Bar + parent_clause2 : [@TraitClause2]: test_crate::loopy::Bar parent_clause3 : [@TraitClause3]: core::marker::Sized type BazTy + type Self_Clause2_BarTy } impl test_crate::loopy::{impl test_crate::loopy::Baz<()> for ()}#2 : test_crate::loopy::Baz<(), ()> { parent_clause0 = core::marker::Sized<()> parent_clause1 = test_crate::loopy::{impl test_crate::loopy::Baz<()> for ()}#2 - parent_clause2 = test_crate::loopy::{impl test_crate::loopy::Bar for ()} + parent_clause2 = test_crate::loopy::{impl test_crate::loopy::Bar for ()} parent_clause3 = core::marker::Sized type BazTy = usize + type Self_Clause2_BarTy = bool } -trait test_crate::loopy_with_generics::Bar<'a, Self, T, U> +trait test_crate::loopy_with_generics::Bar<'a, Self, T, U, Self_BarTy> { parent_clause0 : [@TraitClause0]: core::marker::Sized parent_clause1 : [@TraitClause1]: core::marker::Sized - parent_clause2 : [@TraitClause2]: core::marker::Sized - type BarTy + parent_clause2 : [@TraitClause2]: core::marker::Sized } -impl<'a, T> test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Bar<'a, u8, T> for ()}<'a, T> : test_crate::loopy_with_generics::Bar<'a, (), u8, T> +impl<'a, T> test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Bar<'a, u8, T, &'a (T)> for ()}<'a, T> : test_crate::loopy_with_generics::Bar<'a, (), u8, T, &'a (T)> where [@TraitClause0]: core::marker::Sized, { parent_clause0 = core::marker::Sized parent_clause1 = @TraitClause0 parent_clause2 = core::marker::Sized<&'_ (T)> - type BarTy = &'a (T) } trait test_crate::loopy_with_generics::Foo<'b, Self, T> @@ -197,8 +255,9 @@ trait test_crate::loopy_with_generics::Foo<'b, Self, T> parent_clause0 : [@TraitClause0]: core::marker::Sized parent_clause1 : [@TraitClause1]: core::marker::Sized parent_clause2 : [@TraitClause2]: test_crate::loopy_with_generics::Foo<'_, Self::FooTy, T> - parent_clause3 : [@TraitClause3]: test_crate::loopy_with_generics::Bar<'_, Self::FooTy, u8, core::option::Option[Self::parent_clause0]> + parent_clause3 : [@TraitClause3]: test_crate::loopy_with_generics::Bar<'_, Self::FooTy, u8, core::option::Option[Self::parent_clause0], Self::Self_Clause3_BarTy> type FooTy + type Self_Clause3_BarTy } impl test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Foo<'static, u16> for ()}#1 : test_crate::loopy_with_generics::Foo<'static, (), u16> @@ -206,8 +265,9 @@ impl test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Foo parent_clause0 = core::marker::Sized parent_clause1 = core::marker::Sized<()> parent_clause2 = test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Foo<'static, u16> for ()}#1 - parent_clause3 = test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Bar<'a, u8, T> for ()}<'_, core::option::Option[core::marker::Sized]>[core::marker::Sized[core::marker::Sized]>] + parent_clause3 = test_crate::loopy_with_generics::{impl test_crate::loopy_with_generics::Bar<'a, u8, T, &'a (T)> for ()}<'_, core::option::Option[core::marker::Sized]>[core::marker::Sized[core::marker::Sized]>] type FooTy = () + type Self_Clause3_BarTy = &'_ (core::option::Option[core::marker::Sized]) } trait core::borrow::Borrow @@ -215,59 +275,47 @@ trait core::borrow::Borrow fn borrow<'_0> = core::borrow::Borrow::borrow<'_0_0, Self, Borrowed> } -trait alloc::borrow::ToOwned +trait alloc::borrow::ToOwned { - parent_clause0 : [@TraitClause0]: core::marker::Sized - parent_clause1 : [@TraitClause1]: core::borrow::Borrow - type Owned - fn to_owned<'_0> = alloc::borrow::ToOwned::to_owned<'_0_0, Self> - fn clone_into<'_0, '_1> = alloc::borrow::ToOwned::clone_into<'_0_0, '_0_1, Self> + parent_clause0 : [@TraitClause0]: core::marker::Sized + parent_clause1 : [@TraitClause1]: core::borrow::Borrow + fn to_owned<'_0> = alloc::borrow::ToOwned::to_owned<'_0_0, Self, Self_Owned> + fn clone_into<'_0, '_1> = alloc::borrow::ToOwned::clone_into<'_0_0, '_0_1, Self, Self_Owned> } -enum test_crate::cow::Cow<'a, B> +enum test_crate::cow::Cow<'a, B, Clause0_Owned> where - [@TraitClause0]: alloc::borrow::ToOwned, + [@TraitClause0]: alloc::borrow::ToOwned, B : 'a, B : 'a, = | Borrowed(&'a (B)) -| Owned(@TraitClause0::Owned) +| Owned(Clause0_Owned) -trait test_crate::params::Foo<'a, Self, T> +trait test_crate::params::Foo<'a, Self, T, Self_X, Self_Item> { parent_clause0 : [@TraitClause0]: core::marker::Sized - parent_clause1 : [@TraitClause1]: core::marker::Sized - parent_clause2 : [@TraitClause2]: core::marker::Sized - type X - type Item + parent_clause1 : [@TraitClause1]: core::marker::Sized + parent_clause2 : [@TraitClause2]: core::marker::Sized } -impl<'a, T> test_crate::params::{impl test_crate::params::Foo<'a, core::option::Option[@TraitClause0]> for ()}<'a, T> : test_crate::params::Foo<'a, (), core::option::Option[@TraitClause0]> +impl<'a, T> test_crate::params::{impl test_crate::params::Foo<'a, core::option::Option[@TraitClause0], &'a (()), &'a ((core::option::Option[@TraitClause0], &'_ (())))> for ()}<'a, T> : test_crate::params::Foo<'a, (), core::option::Option[@TraitClause0], &'a (()), &'a ((core::option::Option[@TraitClause0], &'_ (())))> where [@TraitClause0]: core::marker::Sized, { parent_clause0 = core::marker::Sized[@TraitClause0]> parent_clause1 = core::marker::Sized<&'_ (())> parent_clause2 = core::marker::Sized<&'_ ((core::option::Option[@TraitClause0], &'_ (())))> - type X = &'a (()) - type Item = &'a ((core::option::Option[@TraitClause0], test_crate::params::{impl test_crate::params::Foo<'a, core::option::Option[@TraitClause0]> for ()}<'_, T>[@TraitClause0]::X)) } -fn test_crate::Foo::use_item<'a, '_1, Self>(@1: &'_1 (Self::Item)) -> &'_1 (Self::Item) -{ - let @0: &'_ (Self::Item); // return - let x@1: &'_ (Self::Item); // arg #1 - - @0 := copy (x@1) - return -} +fn test_crate::Foo::use_item_required<'a, Self, Self_Item>(@1: Self_Item) -> Self_Item fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self)) -fn alloc::borrow::ToOwned::to_owned<'_0, Self>(@1: &'_0 (Self)) -> Self::Owned +fn alloc::borrow::ToOwned::to_owned<'_0, Self, Self_Owned>(@1: &'_0 (Self)) -> Self_Owned -fn alloc::borrow::ToOwned::clone_into<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 mut (Self::Owned)) +fn alloc::borrow::ToOwned::clone_into<'_0, '_1, Self, Self_Owned>(@1: &'_0 (Self), @2: &'_1 mut (Self_Owned)) fn core::borrow::Borrow::borrow<'_0, Self, Borrowed>(@1: &'_0 (Self)) -> &'_0 (Borrowed) diff --git a/charon/tests/ui/associated-types.rs b/charon/tests/ui/associated-types.rs index 3d65c16c..f43b2bad 100644 --- a/charon/tests/ui/associated-types.rs +++ b/charon/tests/ui/associated-types.rs @@ -1,19 +1,37 @@ +//@ charon-args=--remove-associated-types=* #![feature(associated_type_defaults)] trait Foo<'a>: Copy { - // FIXME: the `+ 'a` appears to be completely ignored. type Item: Clone + 'a; - fn use_item(x: &Self::Item) -> &Self::Item { + fn use_item_required(x: Self::Item) -> Self::Item; + fn use_item_provided(x: Self::Item) -> Self::Item + where + Self::Item: Foo<'a>, + { x } } impl<'a, T> Foo<'a> for &'a T { type Item = Option<&'a T>; + + fn use_item_required(x: Self::Item) -> Self::Item { + x + } } -fn external_use_item<'a, T: Foo<'a>>(x: T::Item) -> T::Item { - x.clone() +impl<'a, T: Copy> Foo<'a> for Option { + type Item = T; + fn use_item_required(x: Self::Item) -> Self::Item { + x + } +} + +fn external_use_item<'a, T: Foo<'a>>(x: T::Item) -> T::Item +where + T::Item: Foo<'a>, +{ + T::use_item_provided(x).clone() } fn call_fn() { diff --git a/charon/tests/ui/call-to-known-trait-method.out b/charon/tests/ui/call-to-known-trait-method.out index b7d25321..54e61487 100644 --- a/charon/tests/ui/call-to-known-trait-method.out +++ b/charon/tests/ui/call-to-known-trait-method.out @@ -42,12 +42,11 @@ where fn default = test_crate::{impl core::default::Default for test_crate::Struct[@TraitClause0]}#1::default[@TraitClause0, @TraitClause1] } -trait test_crate::Trait +trait test_crate::Trait { parent_clause0 : [@TraitClause0]: core::marker::Sized - parent_clause1 : [@TraitClause1]: core::marker::Sized - type Item - fn method> = test_crate::Trait::method[@TraitClause0_0] + parent_clause1 : [@TraitClause1]: core::marker::Sized + fn method> = test_crate::Trait::method[@TraitClause0_0] } trait core::clone::Clone @@ -63,7 +62,7 @@ trait core::cmp::PartialEq fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs> } -fn test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]}::method() +fn test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]}::method() where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, @@ -80,7 +79,7 @@ where return } -impl test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]} : test_crate::Trait[@TraitClause0], B> +impl test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]} : test_crate::Trait[@TraitClause0], B, (A, B)> where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, @@ -89,8 +88,7 @@ where { parent_clause0 = @TraitClause1 parent_clause1 = core::marker::Sized<(A, B)> - type Item = (A, B) - fn method> = test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]}::method[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3, @TraitClause0_0] + fn method> = test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]}::method[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3, @TraitClause0_0] } fn core::default::{impl core::default::Default for bool}#1::default() -> bool @@ -133,7 +131,7 @@ fn test_crate::main() @fake_read(_x@1) _y@2 := test_crate::{impl core::default::Default for test_crate::Struct[@TraitClause0]}#1::default[core::marker::Sized, core::default::{impl core::default::Default for bool}#1]() @fake_read(_y@2) - @3 := test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]}::method[core::marker::Sized, core::marker::Sized, core::clone::impls::{impl core::clone::Clone for u8}#6, core::cmp::impls::{impl core::cmp::PartialEq for bool}#19, core::marker::Sized]() + @3 := test_crate::{impl test_crate::Trait for test_crate::Struct[@TraitClause0]}::method[core::marker::Sized, core::marker::Sized, core::clone::impls::{impl core::clone::Clone for u8}#6, core::cmp::impls::{impl core::cmp::PartialEq for bool}#19, core::marker::Sized]() drop @3 @4 := () @0 := move (@4) @@ -143,7 +141,7 @@ fn test_crate::main() return } -fn test_crate::Trait::method() +fn test_crate::Trait::method() where [@TraitClause0]: core::marker::Sized, diff --git a/charon/tests/ui/call-to-known-trait-method.rs b/charon/tests/ui/call-to-known-trait-method.rs index 849c0eaa..673791f4 100644 --- a/charon/tests/ui/call-to-known-trait-method.rs +++ b/charon/tests/ui/call-to-known-trait-method.rs @@ -1,3 +1,4 @@ +//@ charon-args=--remove-associated-types=* //! Test that we pass generics correctly in the `skip_trait_refs_when_known` pass. #[derive(Default)] struct Struct(A); diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index e5580948..9ac80315 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -16,29 +16,28 @@ trait core::marker::Sized trait core::marker::Tuple -trait core::ops::function::FnOnce +trait core::ops::function::FnOnce { parent_clause0 : [@TraitClause0]: core::marker::Sized parent_clause1 : [@TraitClause1]: core::marker::Tuple - parent_clause2 : [@TraitClause2]: core::marker::Sized - type Output - fn call_once = core::ops::function::FnOnce::call_once + parent_clause2 : [@TraitClause2]: core::marker::Sized + fn call_once = core::ops::function::FnOnce::call_once } -trait core::ops::function::FnMut +trait core::ops::function::FnMut { - parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce + parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce parent_clause1 : [@TraitClause1]: core::marker::Sized parent_clause2 : [@TraitClause2]: core::marker::Tuple - fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args> + fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args, Self_Clause0_Output> } -trait core::ops::function::Fn +trait core::ops::function::Fn { - parent_clause0 : [@TraitClause0]: core::ops::function::FnMut + parent_clause0 : [@TraitClause0]: core::ops::function::FnMut parent_clause1 : [@TraitClause1]: core::marker::Sized parent_clause2 : [@TraitClause2]: core::marker::Tuple - fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args> + fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args, Self_Clause0_Clause0_Output> } enum core::option::Option @@ -49,14 +48,13 @@ enum core::option::Option | Some(T) -fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> Self::parent_clause0::parent_clause0::Output +fn core::ops::function::Fn::call<'_0, Self, Args, Self_Clause0_Clause0_Output>(@1: &'_0 (Self), @2: Args) -> Self_Clause0_Clause0_Output fn test_crate::map_option(@1: core::option::Option[@TraitClause0], @2: F) -> core::option::Option[@TraitClause0] where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::ops::function::Fn, - @TraitClause2::parent_clause0::parent_clause0::Output = T, + [@TraitClause2]: core::ops::function::Fn, { let @0: core::option::Option[@TraitClause0]; // return let x@1: core::option::Option[@TraitClause0]; // arg #1 @@ -136,7 +134,7 @@ fn test_crate::test_map_option1(@1: core::option::Option[core::marker::Size let @2: core::option::Option[core::marker::Sized]; // anonymous local @2 := copy (x@1) - @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32)>](move (@2), const (test_crate::incr_u32)) + @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32), u32>](move (@2), const (test_crate::incr_u32)) drop @2 return } @@ -360,7 +358,7 @@ fn test_crate::test_map_option2(@1: core::option::Option[core::marker::Size @fake_read(f@2) @4 := copy (x@1) @5 := copy (f@2) - @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32)>](move (@4), move (@5)) + @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32), u32>](move (@4), move (@5)) drop @5 drop @4 drop f@2 @@ -386,7 +384,7 @@ fn test_crate::test_map_option_id1(@1: core::option::Option[core::marker::S let @2: core::option::Option[core::marker::Sized]; // anonymous local @2 := copy (x@1) - @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32)>](move (@2), const (test_crate::id[core::marker::Sized])) + @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32), u32>](move (@2), const (test_crate::id[core::marker::Sized])) drop @2 return } @@ -403,7 +401,7 @@ fn test_crate::test_map_option_id2(@1: core::option::Option[core::marker::S @fake_read(f@2) @3 := copy (x@1) @4 := copy (f@2) - @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32)>](move (@3), move (@4)) + @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32), u32>](move (@3), move (@4)) drop @4 drop @3 drop f@2 @@ -492,7 +490,7 @@ fn test_crate::test_map_option_id_clone(@1: core::option::Option[core::mark let @2: core::option::Option[core::marker::Sized]; // anonymous local @2 := copy (x@1) - @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32)>](move (@2), const (test_crate::id_clone[core::marker::Sized, core::clone::impls::{impl core::clone::Clone for u32}#8])) + @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32), u32>](move (@2), const (test_crate::id_clone[core::marker::Sized, core::clone::impls::{impl core::clone::Clone for u32}#8])) drop @2 return } @@ -519,7 +517,7 @@ fn test_crate::test_map_option3(@1: core::option::Option[core::marker::Size @2 := copy (x@1) @3 := {test_crate::test_map_option3::closure} {} - @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32)>](move (@2), move (@3)) + @0 := test_crate::map_option u32>[core::marker::Sized, core::marker::Sized u32>, core::ops::function::Fn u32, (u32), u32>](move (@2), move (@3)) drop @3 drop @2 return @@ -603,7 +601,7 @@ fn test_crate::test_closure_capture(@1: u32, @2: u32) -> u32 @fake_read(f@3) @7 := &*(f@3) @8 := (const (0 : u32)) - @0 := core::ops::function::Fn u32, (u32)>::call<'_>(move (@7), move (@8)) + @0 := core::ops::function::Fn u32, (u32), u32>::call<'_>(move (@7), move (@8)) drop @8 drop @7 drop @4 @@ -647,7 +645,7 @@ where @4 := &*(f@2) @6 := move (x@1) @5 := (move (@6)) - @0 := core::ops::function::Fn T, (T)>::call<'_>(move (@4), move (@5)) + @0 := core::ops::function::Fn T, (T), T>::call<'_>(move (@4), move (@5)) drop @6 drop @6 drop @5 @@ -673,8 +671,7 @@ where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, [@TraitClause2]: core::marker::Sized, - [@TraitClause3]: core::ops::function::FnMut, - @TraitClause3::parent_clause0::Output = U, + [@TraitClause3]: core::ops::function::FnMut, fn test_crate::test_array_map(@1: Array) -> Array { @@ -685,7 +682,7 @@ fn test_crate::test_array_map(@1: Array) -> Array}#23::map i32, i32, 256 : usize>[core::marker::Sized, core::marker::Sized i32>, core::marker::Sized, core::ops::function::FnMut i32, (i32)>](move (@2), move (@3)) + @0 := core::array::{Array}#23::map i32, i32, 256 : usize>[core::marker::Sized, core::marker::Sized i32>, core::marker::Sized, core::ops::function::FnMut i32, (i32), i32>](move (@2), move (@3)) drop @3 drop @2 return @@ -769,17 +766,17 @@ where @fake_read(clo@2) @8 := &clo@2 @9 := () - @7 := core::ops::function::Fn fn() -> fn() -> T, ()>::call<'_>(move (@8), move (@9)) + @7 := core::ops::function::Fn fn() -> fn() -> T, (), fn() -> fn() -> T>::call<'_>(move (@8), move (@9)) @6 := &@7 drop @9 drop @8 @10 := () - @5 := core::ops::function::Fn fn() -> T, ()>::call<'_>(move (@6), move (@10)) + @5 := core::ops::function::Fn fn() -> T, (), fn() -> T>::call<'_>(move (@6), move (@10)) @4 := &@5 drop @10 drop @6 @11 := () - @0 := core::ops::function::Fn T, ()>::call<'_>(move (@4), move (@11)) + @0 := core::ops::function::Fn T, (), T>::call<'_>(move (@4), move (@11)) drop @11 drop @4 drop clo@2 @@ -808,7 +805,7 @@ fn test_crate::BLAH() -> u32 @fake_read(clo@1) @2 := &clo@1 @3 := () - @0 := core::ops::function::Fn u32, ()>::call<'_>(move (@2), move (@3)) + @0 := core::ops::function::Fn u32, (), u32>::call<'_>(move (@2), move (@3)) drop @3 drop @2 drop clo@1 @@ -819,9 +816,9 @@ global test_crate::BLAH: u32 = test_crate::BLAH() fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self)) -fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> Self::parent_clause0::Output +fn core::ops::function::FnMut::call_mut<'_0, Self, Args, Self_Clause0_Output>(@1: &'_0 mut (Self), @2: Args) -> Self_Clause0_Output -fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> Self::Output +fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> Self_Output diff --git a/charon/tests/ui/closures.rs b/charon/tests/ui/closures.rs index 6e81f751..0f2ec751 100644 --- a/charon/tests/ui/closures.rs +++ b/charon/tests/ui/closures.rs @@ -1,3 +1,4 @@ +//@ charon-args=--remove-associated-types=* //@ output=pretty-llbc pub fn incr_u32(x: u32) -> u32 { x + 1 diff --git a/charon/tests/ui/dictionary_passing_style_woes.out b/charon/tests/ui/dictionary_passing_style_woes.out index 4c5408bd..f3c6f4c7 100644 --- a/charon/tests/ui/dictionary_passing_style_woes.out +++ b/charon/tests/ui/dictionary_passing_style_woes.out @@ -2,90 +2,82 @@ trait core::marker::Sized -trait test_crate::Iterator +trait test_crate::Iterator { - parent_clause0 : [@TraitClause0]: core::marker::Sized - type Item + parent_clause0 : [@TraitClause0]: core::marker::Sized } -trait test_crate::IntoIterator -where - Self::parent_clause2::Item = Self::Item, +trait test_crate::IntoIterator { - parent_clause0 : [@TraitClause0]: core::marker::Sized - parent_clause1 : [@TraitClause1]: core::marker::Sized - parent_clause2 : [@TraitClause2]: test_crate::Iterator - type Item - type IntoIter + parent_clause0 : [@TraitClause0]: core::marker::Sized + parent_clause1 : [@TraitClause1]: core::marker::Sized + parent_clause2 : [@TraitClause2]: test_crate::Iterator } -impl test_crate::{impl test_crate::IntoIterator for I} : test_crate::IntoIterator +impl test_crate::{impl test_crate::IntoIterator for I} : test_crate::IntoIterator where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::Iterator, + [@TraitClause1]: test_crate::Iterator, { parent_clause0 = @TraitClause1::parent_clause0 parent_clause1 = @TraitClause0 parent_clause2 = @TraitClause1 - type Item = @TraitClause1::Item - type IntoIter = I } -fn test_crate::callee(@1: @TraitClause1::Item) -> test_crate::{impl test_crate::IntoIterator for I}[@TraitClause0, @TraitClause1]::Item +fn test_crate::callee(@1: Clause1_Item) -> Clause1_Item where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::Iterator, + [@TraitClause1]: test_crate::Iterator, { - let @0: @TraitClause1::Item; // return - let t@1: @TraitClause1::Item; // arg #1 + let @0: Clause1_Item; // return + let t@1: Clause1_Item; // arg #1 @0 := move (t@1) drop t@1 return } -fn test_crate::caller(@1: @TraitClause1::Item) -> @TraitClause2::Item +fn test_crate::caller(@1: Clause1_Item) -> Clause2_Item where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::Iterator, - [@TraitClause2]: test_crate::IntoIterator, + [@TraitClause1]: test_crate::Iterator, + [@TraitClause2]: test_crate::IntoIterator, { - let @0: @TraitClause2::Item; // return - let t@1: @TraitClause1::Item; // arg #1 - let @2: @TraitClause1::Item; // anonymous local + let @0: Clause2_Item; // return + let t@1: Clause1_Item; // arg #1 + let @2: Clause1_Item; // anonymous local @2 := move (t@1) - @0 := test_crate::callee[@TraitClause0, @TraitClause1](move (@2)) + @0 := test_crate::callee[@TraitClause0, @TraitClause1](move (@2)) drop @2 drop t@1 return } -trait test_crate::X +trait test_crate::X { - parent_clause0 : [@TraitClause0]: core::marker::Sized - type Assoc - fn method<'_0> = test_crate::X::method<'_0_0, Self> + parent_clause0 : [@TraitClause0]: core::marker::Sized + fn method<'_0> = test_crate::X::method<'_0_0, Self, Self_Assoc> } -trait test_crate::A +trait test_crate::A { - parent_clause0 : [@TraitClause0]: test_crate::X + parent_clause0 : [@TraitClause0]: test_crate::X } -trait test_crate::B +trait test_crate::B { - parent_clause0 : [@TraitClause0]: test_crate::X + parent_clause0 : [@TraitClause0]: test_crate::X } -fn test_crate::X::method<'_0, Self>(@1: &'_0 (Self)) -> Self::Assoc +fn test_crate::X::method<'_0, Self, Self_Assoc>(@1: &'_0 (Self)) -> Self_Assoc -fn test_crate::a(@1: T) -> @TraitClause1::parent_clause0::Assoc +fn test_crate::a(@1: T) -> Clause1_Clause0_Assoc where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::A, + [@TraitClause1]: test_crate::A, { - let @0: @TraitClause1::parent_clause0::Assoc; // return + let @0: Clause1_Clause0_Assoc; // return let x@1: T; // arg #1 let @2: &'_ (T); // anonymous local @@ -96,12 +88,12 @@ where return } -fn test_crate::b(@1: T) -> @TraitClause1::parent_clause0::Assoc +fn test_crate::b(@1: T) -> Clause1_Clause0_Assoc where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::B, + [@TraitClause1]: test_crate::B, { - let @0: @TraitClause1::parent_clause0::Assoc; // return + let @0: Clause1_Clause0_Assoc; // return let x@1: T; // arg #1 let @2: &'_ (T); // anonymous local @@ -112,24 +104,24 @@ where return } -fn test_crate::x(@1: T) -> (@TraitClause1::parent_clause0::Assoc, @TraitClause1::parent_clause0::Assoc) +fn test_crate::x(@1: T) -> (Clause1_Clause0_Assoc, Clause1_Clause0_Assoc) where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: test_crate::A, - [@TraitClause2]: test_crate::B, + [@TraitClause1]: test_crate::A, + [@TraitClause2]: test_crate::B, { - let @0: (@TraitClause1::parent_clause0::Assoc, @TraitClause1::parent_clause0::Assoc); // return + let @0: (Clause1_Clause0_Assoc, Clause1_Clause0_Assoc); // return let x@1: T; // arg #1 - let @2: @TraitClause1::parent_clause0::Assoc; // anonymous local + let @2: Clause1_Clause0_Assoc; // anonymous local let @3: T; // anonymous local - let @4: @TraitClause1::parent_clause0::Assoc; // anonymous local + let @4: Clause1_Clause0_Assoc; // anonymous local let @5: T; // anonymous local @3 := move (x@1) - @2 := test_crate::a[@TraitClause0, @TraitClause1](move (@3)) + @2 := test_crate::a[@TraitClause0, @TraitClause1](move (@3)) drop @3 @5 := move (x@1) - @4 := test_crate::b[@TraitClause0, @TraitClause2](move (@5)) + @4 := test_crate::b[@TraitClause0, @TraitClause2](move (@5)) drop @5 @0 := (move (@2), move (@4)) drop @4 diff --git a/charon/tests/ui/dictionary_passing_style_woes.rs b/charon/tests/ui/dictionary_passing_style_woes.rs index 93bbfe3d..a048ed10 100644 --- a/charon/tests/ui/dictionary_passing_style_woes.rs +++ b/charon/tests/ui/dictionary_passing_style_woes.rs @@ -1,3 +1,4 @@ +//@ charon-args=--remove-associated-types=* trait Iterator { type Item; } diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out index 8966b19b..b0f7cf84 100644 --- a/charon/tests/ui/impl-trait.out +++ b/charon/tests/ui/impl-trait.out @@ -61,9 +61,9 @@ fn test_crate::use_foo() { let @0: (); // return let foo@1: (); // local - let @2: test_crate::{impl test_crate::Foo for ()}::Type; // anonymous local - let @3: &'_ (test_crate::{impl test_crate::Foo for ()}::Type); // anonymous local - let @4: &'_ (test_crate::{impl test_crate::Foo for ()}::Type); // anonymous local + let @2: u32; // anonymous local + let @3: &'_ (u32); // anonymous local + let @4: &'_ (u32); // anonymous local let @5: &'_ (()); // anonymous local let @6: (); // anonymous local diff --git a/charon/tests/ui/issue-297-cfg.out b/charon/tests/ui/issue-297-cfg.out index 67bb6646..4da53611 100644 --- a/charon/tests/ui/issue-297-cfg.out +++ b/charon/tests/ui/issue-297-cfg.out @@ -570,15 +570,15 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli where [@TraitClause0]: core::marker::Sized, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> core::option::Option[@TraitClause0]}#71<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (Slice)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> core::option::Option<&'_ (Slice)>[core::marker::Sized<&'_ (Slice)>] where [@TraitClause0]: core::marker::Sized, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option[@TraitClause0]}#71<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (Slice)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'_ (Slice)>[core::marker::Sized<&'_ (Slice)>] where [@TraitClause0]: core::marker::Sized, -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71<'_, T>[@TraitClause0]::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice) where [@TraitClause0]: core::marker::Sized, diff --git a/charon/tests/ui/issue-369-mismatched-genericparams.out b/charon/tests/ui/issue-369-mismatched-genericparams.out index 3508a207..38a3328f 100644 --- a/charon/tests/ui/issue-369-mismatched-genericparams.out +++ b/charon/tests/ui/issue-369-mismatched-genericparams.out @@ -22,20 +22,20 @@ enum core::option::Option | Some(T) -impl test_crate::{impl test_crate::Try for core::option::Option[@TraitClause0]} : test_crate::Try[@TraitClause0]> +impl test_crate::{impl test_crate::FromResidual<()> for core::option::Option[@TraitClause0]}#1 : test_crate::FromResidual[@TraitClause0], ()> where [@TraitClause0]: core::marker::Sized, { - parent_clause0 = test_crate::{impl test_crate::FromResidual[@TraitClause0]}[@TraitClause0]::Residual> for core::option::Option[@TraitClause0]}#1[@TraitClause0] - parent_clause1 = core::marker::Sized<()> - type Residual = () + parent_clause0 = core::marker::Sized<()> } -impl test_crate::{impl test_crate::FromResidual[@TraitClause0]}[@TraitClause0]::Residual> for core::option::Option[@TraitClause0]}#1 : test_crate::FromResidual[@TraitClause0], test_crate::{impl test_crate::Try for core::option::Option[@TraitClause0]}[@TraitClause0]::Residual> +impl test_crate::{impl test_crate::Try for core::option::Option[@TraitClause0]} : test_crate::Try[@TraitClause0]> where [@TraitClause0]: core::marker::Sized, { - parent_clause0 = core::marker::Sized<()> + parent_clause0 = test_crate::{impl test_crate::FromResidual<()> for core::option::Option[@TraitClause0]}#1[@TraitClause0] + parent_clause1 = core::marker::Sized<()> + type Residual = () } 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 4465c483..019aa9c0 100644 --- a/charon/tests/ui/issue-4-slice-try-into-array.out +++ b/charon/tests/ui/issue-4-slice-try-into-array.out @@ -40,7 +40,7 @@ trait core::marker::Copy parent_clause0 : [@TraitClause0]: core::clone::Clone } -fn core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7::try_from<'_0, T, const N : usize>(@1: &'_0 (Slice)) -> core::result::Result, core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7<'_, T, const N : usize>[@TraitClause0, @TraitClause1]::Error>[core::marker::Sized>, core::marker::Sized] +fn core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7::try_from<'_0, T, const N : usize>(@1: &'_0 (Slice)) -> core::result::Result, core::array::TryFromSliceError>[core::marker::Sized>, core::marker::Sized] where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Copy, diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index 4465c483..019aa9c0 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -40,7 +40,7 @@ trait core::marker::Copy parent_clause0 : [@TraitClause0]: core::clone::Clone } -fn core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7::try_from<'_0, T, const N : usize>(@1: &'_0 (Slice)) -> core::result::Result, core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7<'_, T, const N : usize>[@TraitClause0, @TraitClause1]::Error>[core::marker::Sized>, core::marker::Sized] +fn core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7::try_from<'_0, T, const N : usize>(@1: &'_0 (Slice)) -> core::result::Result, core::array::TryFromSliceError>[core::marker::Sized>, core::marker::Sized] where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Copy, diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 68927cae..35d568ee 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -586,7 +586,7 @@ where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::iter::range::Step, -unsafe fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range[@TraitClause0]}#6::__iterator_get_unchecked<'_0, A>(@1: &'_0 mut (core::ops::range::Range[@TraitClause0]), @2: usize) -> core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range[@TraitClause0]}#6[@TraitClause0, @TraitClause1]::Item +unsafe fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range[@TraitClause0]}#6::__iterator_get_unchecked<'_0, A>(@1: &'_0 mut (core::ops::range::Range[@TraitClause0]), @2: usize) -> A where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::iter::range::Step, diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index d088e24e..28ae448c 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -1313,7 +1313,7 @@ where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::iter::range::Step, -unsafe fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range[@TraitClause0]}#6::__iterator_get_unchecked<'_0, A>(@1: &'_0 mut (core::ops::range::Range[@TraitClause0]), @2: usize) -> core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range[@TraitClause0]}#6[@TraitClause0, @TraitClause1]::Item +unsafe fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range[@TraitClause0]}#6::__iterator_get_unchecked<'_0, A>(@1: &'_0 mut (core::ops::range::Range[@TraitClause0]), @2: usize) -> A where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::iter::range::Step, @@ -1899,31 +1899,7 @@ trait core::slice::index::SliceIndex fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T> } -trait core::ops::index::Index -{ - type Output - fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx> -} - -fn alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13::index<'_0, T, I, A>(@1: &'_0 (alloc::vec::Vec[@TraitClause0, @TraitClause2]), @2: I) -> &'_0 (alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3]::Output) -where - [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::marker::Sized, - [@TraitClause3]: core::slice::index::SliceIndex>, - -impl alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13 : core::ops::index::Index[@TraitClause0, @TraitClause2], I> -where - [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: core::marker::Sized, - [@TraitClause3]: core::slice::index::SliceIndex>, -{ - type Output = @TraitClause3::Output - fn index<'_0> = alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13::index<'_0_0, T, I, A>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] -} - -fn alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#14::index_mut<'_0, T, I, A>(@1: &'_0 mut (alloc::vec::Vec[@TraitClause0, @TraitClause2]), @2: I) -> &'_0 mut (alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3]::Output) +fn alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#14::index_mut<'_0, T, I, A>(@1: &'_0 mut (alloc::vec::Vec[@TraitClause0, @TraitClause2]), @2: I) -> &'_0 mut (@TraitClause3::Output) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, @@ -2164,6 +2140,12 @@ where fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option[Self::parent_clause0] +trait core::ops::index::Index +{ + type Output + fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx> +} + fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (Self::parent_clause0::Output) trait core::ops::index::IndexMut @@ -2172,6 +2154,24 @@ trait core::ops::index::IndexMut fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx> } +fn alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13::index<'_0, T, I, A>(@1: &'_0 (alloc::vec::Vec[@TraitClause0, @TraitClause2]), @2: I) -> &'_0 (@TraitClause3::Output) +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: core::marker::Sized, + [@TraitClause3]: core::slice::index::SliceIndex>, + +impl alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13 : core::ops::index::Index[@TraitClause0, @TraitClause2], I> +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: core::marker::Sized, + [@TraitClause3]: core::slice::index::SliceIndex>, +{ + type Output = @TraitClause3::Output + fn index<'_0> = alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#13::index<'_0_0, T, I, A>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3] +} + impl alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec[@TraitClause0, @TraitClause2]}#14 : core::ops::index::IndexMut[@TraitClause0, @TraitClause2], I> where [@TraitClause0]: core::marker::Sized, diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index 6a3d448d..d60b0856 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -154,13 +154,7 @@ where [@TraitClause4]: core::hash::Hash, [@TraitClause5]: core::hash::BuildHasher, -trait core::ops::index::Index -{ - type Output - fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx> -} - -fn std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]}#9::index<'_0, '_1, K, Q, V, S>(@1: &'_1 (std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]), @2: &'_0 (Q)) -> &'_1 (std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]}#9<'_, K, Q, V, S>[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3, @TraitClause4, @TraitClause5, @TraitClause6, @TraitClause7, @TraitClause8]::Output) +fn std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]}#9::index<'_0, '_1, K, Q, V, S>(@1: &'_1 (std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]), @2: &'_0 (Q)) -> &'_1 (V) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, @@ -233,6 +227,12 @@ fn test_crate::get_or_insert<'_0>(@1: &'_0 mut (std::collections::hash::map::Has fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output) +trait core::ops::index::Index +{ + type Output + fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx> +} + impl<'_0, K, Q, V, S> std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]}#9<'_0, K, Q, V, S> : core::ops::index::Index[@TraitClause0, @TraitClause1, @TraitClause2], &'_0 (Q)> where [@TraitClause0]: core::marker::Sized, diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out index 8ee6fef5..963ab264 100644 --- a/charon/tests/ui/predicates-on-late-bound-vars.out +++ b/charon/tests/ui/predicates-on-late-bound-vars.out @@ -96,7 +96,7 @@ trait test_crate::Foo type S } -fn test_crate::f() -> core::option::Option<@TraitClause2::S>[@TraitClause3::parent_clause0] +fn test_crate::f() -> core::option::Option<@TraitClause3::S>[@TraitClause3::parent_clause0] where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, diff --git a/charon/tests/ui/region-inference-vars.out b/charon/tests/ui/region-inference-vars.out index e356ad3d..1fbd493a 100644 --- a/charon/tests/ui/region-inference-vars.out +++ b/charon/tests/ui/region-inference-vars.out @@ -19,7 +19,7 @@ trait test_crate::MyTryFrom fn from<[@TraitClause0]: core::marker::Sized> = test_crate::MyTryFrom::from[@TraitClause0_0] } -fn test_crate::{impl test_crate::MyTryFrom<&'_0 (bool)> for bool}::from<'_0>(@1: &'_0 (bool)) -> core::result::Result for bool}<'_>::Error>[core::marker::Sized, core::marker::Sized<()>] +fn test_crate::{impl test_crate::MyTryFrom<&'_0 (bool)> for bool}::from<'_0>(@1: &'_0 (bool)) -> core::result::Result[core::marker::Sized, core::marker::Sized<()>] { let @0: core::result::Result[core::marker::Sized, core::marker::Sized<()>]; // return let v@1: &'_ (bool); // arg #1 diff --git a/charon/tests/ui/simple/assoc-type-with-fn-bound.out b/charon/tests/ui/simple/assoc-type-with-fn-bound.out new file mode 100644 index 00000000..8a385edc --- /dev/null +++ b/charon/tests/ui/simple/assoc-type-with-fn-bound.out @@ -0,0 +1,10 @@ +error: Could not compute the value of Self::Clause1::Clause0::Clause0::Output needed to update generics for item Item(TraitDecl(3)). + Constraints in scope: + - Self::Foo = @Type0_1 + --> tests/ui/simple/assoc-type-with-fn-bound.rs:9:5 + | +9 | fn call(&self) -> >::Output; + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + +ERROR The extraction generated 1 errors diff --git a/charon/tests/ui/simple/assoc-type-with-fn-bound.rs b/charon/tests/ui/simple/assoc-type-with-fn-bound.rs new file mode 100644 index 00000000..25f411dc --- /dev/null +++ b/charon/tests/ui/simple/assoc-type-with-fn-bound.rs @@ -0,0 +1,19 @@ +//@ known-failure +//@ charon-args=--remove-associated-types=* +// Fails because of bad handling of `Self` clauses. Should be fixed by +// https://github.com/AeneasVerif/charon/pull/514. +#![feature(unboxed_closures)] + +trait Trait { + type Foo: Fn(); + fn call(&self) -> >::Output; +} + +impl Trait for F { + type Foo = F; + fn call(&self) -> >::Output { + self() + } +} + +fn use_foo() -> <::Foo as FnOnce<()>>::Output {} diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out index 21e85f48..d3d0ef0d 100644 --- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out @@ -2,16 +2,14 @@ trait core::marker::Sized -trait test_crate::Trait +trait test_crate::Trait { - parent_clause0 : [@TraitClause0]: core::marker::Sized - type Type + parent_clause0 : [@TraitClause0]: core::marker::Sized } -impl test_crate::{impl test_crate::Trait for ()} : test_crate::Trait<()> +impl test_crate::{impl test_crate::Trait<()> for ()} : test_crate::Trait<(), ()> { parent_clause0 = core::marker::Sized<()> - type Type = () } struct test_crate::HashMap @@ -22,11 +20,11 @@ struct test_crate::HashMap S, } -fn test_crate::{test_crate::HashMap[@TraitClause0]}#1::get(@1: test_crate::HashMap[@TraitClause0], @2: Q) +fn test_crate::{test_crate::HashMap[@TraitClause0]}#1::get(@1: test_crate::HashMap[@TraitClause0], @2: Q) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: test_crate::Trait, + [@TraitClause2]: test_crate::Trait, { let @0: (); // return let _x@1: test_crate::HashMap[@TraitClause0]; // arg #1 @@ -41,11 +39,11 @@ where return } -fn test_crate::top_level_get(@1: test_crate::HashMap[@TraitClause0], @2: Q) +fn test_crate::top_level_get(@1: test_crate::HashMap[@TraitClause0], @2: Q) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized, - [@TraitClause2]: test_crate::Trait, + [@TraitClause2]: test_crate::Trait, { let @0: (); // return let _x@1: test_crate::HashMap[@TraitClause0]; // arg #1 @@ -74,13 +72,13 @@ fn test_crate::test(@1: test_crate::HashMap<()>[core::marker::Sized<()>]) @3 := move (map@1) @4 := () - @2 := test_crate::top_level_get<(), ()>[core::marker::Sized<()>, core::marker::Sized<()>, test_crate::{impl test_crate::Trait for ()}](move (@3), move (@4)) + @2 := test_crate::top_level_get<(), (), ()>[core::marker::Sized<()>, core::marker::Sized<()>, test_crate::{impl test_crate::Trait<()> for ()}](move (@3), move (@4)) drop @4 drop @3 drop @2 @6 := move (map@1) @7 := () - @5 := test_crate::{test_crate::HashMap[@TraitClause0]}#1::get<(), ()>[core::marker::Sized<()>, core::marker::Sized<()>, test_crate::{impl test_crate::Trait for ()}](move (@6), move (@7)) + @5 := test_crate::{test_crate::HashMap[@TraitClause0]}#1::get<(), (), ()>[core::marker::Sized<()>, core::marker::Sized<()>, test_crate::{impl test_crate::Trait<()> for ()}](move (@6), move (@7)) drop @7 drop @6 drop @5 diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs index 03dfe12d..c6a3fbbc 100644 --- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs @@ -1,3 +1,4 @@ +//@ charon-args=--remove-associated-types=* pub trait Trait { type Type; } diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.2.out b/charon/tests/ui/simple/fewer-clauses-in-method-impl.2.out new file mode 100644 index 00000000..6fa7c46a --- /dev/null +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.2.out @@ -0,0 +1,13 @@ +error: Mismatched method generics: + params: + supplied: [@TraitDecl1<()>] + --> tests/ui/simple/fewer-clauses-in-method-impl.2.rs:14:5 + | +14 | <() as Trait>::method() + | ^^^^^^^^^^^^^^^^^^^^^^^ + | + +thread 'rustc' panicked at src/ast/types_utils.rs:116:9: +assertion failed: args.matches(&self.params) +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace +ERROR Compilation encountered 0 errors diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.2.rs b/charon/tests/ui/simple/fewer-clauses-in-method-impl.2.rs new file mode 100644 index 00000000..a2d5e9c8 --- /dev/null +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.2.rs @@ -0,0 +1,15 @@ +//@ known-failure +//@ charon-args=--remove-associated-types=* +trait Trait { + fn method() + where + Self: Sized; +} + +impl Trait for () { + fn method() {} +} + +fn main() { + <() as Trait>::method() +} diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out new file mode 100644 index 00000000..1b6a6679 --- /dev/null +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out @@ -0,0 +1,24 @@ +error: Found inconsistent generics after transformations: + Mismatched trait clause: + expected: [@TraitClause1]: core::clone::Clone + got: core::marker::Copy<()>: core::marker::Copy<()> + Visitor stack: + charon_lib::ast::types::GenericArgs + charon_lib::ast::expressions::FnPtr + charon_lib::ast::gast::FnOperand + charon_lib::ast::gast::Call + charon_lib::ast::llbc_ast::RawStatement + charon_lib::ast::llbc_ast::Statement + alloc::vec::Vec + charon_lib::ast::llbc_ast::Block + charon_lib::ast::gast::GExprBody + charon_lib::ast::gast::Body + core::result::Result + charon_lib::ast::gast::FunDecl + --> tests/ui/simple/fewer-clauses-in-method-impl.rs:12:5 + | +12 | <() as Trait>::method::<()>() + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + +ERROR The extraction generated 1 errors diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs b/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs new file mode 100644 index 00000000..b35a5e92 --- /dev/null +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs @@ -0,0 +1,13 @@ +//@ known-failure +//@ charon-args=--remove-associated-types=* +trait Trait { + fn method(); +} + +impl Trait for () { + fn method() {} +} + +fn main() { + <() as Trait>::method::<()>() +} diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out index e1dd7e77..e27e4149 100644 --- a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out +++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out @@ -13,36 +13,34 @@ trait core::marker::Sized trait core::marker::Tuple -trait core::ops::function::FnOnce +trait core::ops::function::FnOnce { parent_clause0 : [@TraitClause0]: core::marker::Sized parent_clause1 : [@TraitClause1]: core::marker::Tuple - parent_clause2 : [@TraitClause2]: core::marker::Sized - type Output - fn call_once = core::ops::function::FnOnce::call_once + parent_clause2 : [@TraitClause2]: core::marker::Sized + fn call_once = core::ops::function::FnOnce::call_once } -trait core::ops::function::FnMut +trait core::ops::function::FnMut { - parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce + parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce parent_clause1 : [@TraitClause1]: core::marker::Sized parent_clause2 : [@TraitClause2]: core::marker::Tuple - fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args> + fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args, Self_Clause0_Output> } -trait core::ops::function::Fn +trait core::ops::function::Fn { - parent_clause0 : [@TraitClause0]: core::ops::function::FnMut + parent_clause0 : [@TraitClause0]: core::ops::function::FnMut parent_clause1 : [@TraitClause1]: core::marker::Sized parent_clause2 : [@TraitClause2]: core::marker::Tuple - fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args> + fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args, Self_Clause0_Clause0_Output> } fn test_crate::call<'b, F>(@1: F) where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: core::ops::function::Fn, - @TraitClause1::parent_clause0::parent_clause0::Output = &'b (()), + [@TraitClause1]: core::ops::function::Fn, { let @0: (); // return let @1: F; // arg #1 @@ -61,7 +59,7 @@ fn test_crate::flibidi() let @1: (); // anonymous local let @2: (); // anonymous local - @1 := test_crate::call<'_, fn<'a>(&'a (())) -> &'a (())>[core::marker::Sized(&'a (())) -> &'a (())>, core::ops::function::Fn(&'a (())) -> &'a (()), (&'_ (()))>](const (test_crate::flabada<'_>)) + @1 := test_crate::call<'_, fn<'a>(&'a (())) -> &'a (())>[core::marker::Sized(&'a (())) -> &'a (())>, core::ops::function::Fn(&'a (())) -> &'a (()), (&'_ (())), &'_ (())>](const (test_crate::flabada<'_>)) drop @1 @2 := () @0 := move (@2) @@ -69,11 +67,11 @@ fn test_crate::flibidi() return } -fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> Self::parent_clause0::parent_clause0::Output +fn core::ops::function::Fn::call<'_0, Self, Args, Self_Clause0_Clause0_Output>(@1: &'_0 (Self), @2: Args) -> Self_Clause0_Clause0_Output -fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> Self::parent_clause0::Output +fn core::ops::function::FnMut::call_mut<'_0, Self, Args, Self_Clause0_Output>(@1: &'_0 mut (Self), @2: Args) -> Self_Clause0_Output -fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> Self::Output +fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> Self_Output diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs index a91f9716..54eb4e41 100644 --- a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs +++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs @@ -1,3 +1,4 @@ +//@ charon-args=--remove-associated-types=* pub fn flabada<'a>(x: &'a ()) -> &'a () { x } diff --git a/charon/tests/ui/simple/quantified-trait-type-constraint.out b/charon/tests/ui/simple/quantified-trait-type-constraint.out new file mode 100644 index 00000000..ef41c507 --- /dev/null +++ b/charon/tests/ui/simple/quantified-trait-type-constraint.out @@ -0,0 +1,25 @@ +# Final LLBC before serialization: + +trait core::marker::Sized + +trait test_crate::Trait<'a, Self, Self_Type> +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized +} + +fn test_crate::foo() +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: for<'_0> test_crate::Trait<'_0_0, T, &'_ (())>, +{ + let @0: (); // return + let @1: (); // anonymous local + + @1 := () + @0 := move (@1) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/quantified-trait-type-constraint.rs b/charon/tests/ui/simple/quantified-trait-type-constraint.rs new file mode 100644 index 00000000..586f09a2 --- /dev/null +++ b/charon/tests/ui/simple/quantified-trait-type-constraint.rs @@ -0,0 +1,11 @@ +//@ charon-args=--remove-associated-types=* +trait Trait<'a> { + type Type; +} + +// This is incorrectly translated (https://github.com/AeneasVerif/charon/issues/534). +fn foo() +where + T: for<'a> Trait<'a, Type = &'a ()>, +{ +} diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out index d5f02099..7329ae45 100644 --- a/charon/tests/ui/trait-instance-id.out +++ b/charon/tests/ui/trait-instance-id.out @@ -42,6 +42,10 @@ opaque type core::fmt::Arguments<'a> where 'a : 'a, +fn core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array}::into_iter(@1: Array) -> core::array::iter::IntoIter[@TraitClause0] +where + [@TraitClause0]: core::marker::Sized, + enum core::result::Result where [@TraitClause0]: core::marker::Sized, @@ -498,16 +502,12 @@ trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce fn size<'_0, [@TraitClause0]: core::iter::traits::iterator::Iterator> = core::iter::adapters::zip::TrustedRandomAccessNoCoerce::size<'_0_0, Self>[@TraitClause0_0] } -fn core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array}::into_iter(@1: Array) -> core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array}[@TraitClause0]::IntoIter -where - [@TraitClause0]: core::marker::Sized, - fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter(@1: I) -> I where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::iter::traits::iterator::Iterator, -fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter[@TraitClause0]}#2::next<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter[@TraitClause0])) -> core::option::Option[@TraitClause0]}#2[@TraitClause0]::Item>[@TraitClause0] +fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter[@TraitClause0]}#2::next<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter[@TraitClause0])) -> core::option::Option[@TraitClause0] where [@TraitClause0]: core::marker::Sized, @@ -519,7 +519,7 @@ fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::arr where [@TraitClause0]: core::marker::Sized, -fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter[@TraitClause0]}#2::last(@1: core::array::iter::IntoIter[@TraitClause0]) -> core::option::Option[@TraitClause0]}#2[@TraitClause0]::Item>[@TraitClause0] +fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter[@TraitClause0]}#2::last(@1: core::array::iter::IntoIter[@TraitClause0]) -> core::option::Option[@TraitClause0] where [@TraitClause0]: core::marker::Sized, @@ -535,7 +535,7 @@ where [@TraitClause3]: core::ops::function::FnMut, @TraitClause3::parent_clause0::Output = Acc, -unsafe fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter[@TraitClause0]}#2::__iterator_get_unchecked<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter[@TraitClause0]), @2: usize) -> core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter[@TraitClause0]}#2[@TraitClause0]::Item +unsafe fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter[@TraitClause0]}#2::__iterator_get_unchecked<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter[@TraitClause0]), @2: usize) -> T where [@TraitClause0]: core::marker::Sized, @@ -614,7 +614,7 @@ where [@TraitClause3]: core::ops::function::FnMut, @TraitClause3::parent_clause0::Output = bool, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option[@TraitClause0]}#182<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (T)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>] where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized

, @@ -657,7 +657,7 @@ where [@TraitClause3]: for<'_0, '_1> core::ops::function::FnMut, for<'_0, '_1> @TraitClause3::parent_clause0::Output = bool, -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182<'_, T>[@TraitClause0]::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> &'_ (T) where [@TraitClause0]: core::marker::Sized, @@ -703,15 +703,15 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli where [@TraitClause0]: core::marker::Sized, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> core::option::Option[@TraitClause0]}#71<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (Slice)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> core::option::Option<&'_ (Slice)>[core::marker::Sized<&'_ (Slice)>] where [@TraitClause0]: core::marker::Sized, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option[@TraitClause0]}#71<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (Slice)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'_ (Slice)>[core::marker::Sized<&'_ (Slice)>] where [@TraitClause0]: core::marker::Sized, -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71<'_, T>[@TraitClause0]::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice) where [@TraitClause0]: core::marker::Sized, @@ -745,15 +745,15 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli where [@TraitClause0]: core::marker::Sized, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::last<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>[@TraitClause0]) -> core::option::Option[@TraitClause0]}#90<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (Slice)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::last<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>[@TraitClause0]) -> core::option::Option<&'_ (Slice)>[core::marker::Sized<&'_ (Slice)>] where [@TraitClause0]: core::marker::Sized, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option[@TraitClause0]}#90<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (Slice)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'_ (Slice)>[core::marker::Sized<&'_ (Slice)>] where [@TraitClause0]: core::marker::Sized, -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90<'_, T>[@TraitClause0]::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice) where [@TraitClause0]: core::marker::Sized, diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index b1c91c2d..6411cb2b 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -509,7 +509,7 @@ fn test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1() -> global test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1: usize = test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::LEN1() -fn test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0, '_1>(@1: &'_0 mut (test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::W), @2: &'_1 (Array)) +fn test_crate::{impl test_crate::WithConstTy<32 : usize> for bool}#8::f<'_0, '_1>(@1: &'_0 mut (u64), @2: &'_1 (Array)) { let @0: (); // return let @1: &'_ mut (u64); // arg #1 @@ -592,7 +592,7 @@ where return } -fn test_crate::test_where2(@1: @TraitClause1::V) +fn test_crate::test_where2(@1: u32) where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: test_crate::WithConstTy, diff --git a/charon/tests/ui/traits_special.out b/charon/tests/ui/traits_special.out index 2aa0f9a0..3a19ab0e 100644 --- a/charon/tests/ui/traits_special.out +++ b/charon/tests/ui/traits_special.out @@ -19,7 +19,7 @@ trait test_crate::From fn from<[@TraitClause0]: core::marker::Sized> = test_crate::From::from[@TraitClause0_0] } -fn test_crate::{impl test_crate::From<&'_0 (bool)> for bool}::from<'_0>(@1: &'_0 (bool)) -> core::result::Result for bool}<'_>::Error>[core::marker::Sized, core::marker::Sized<()>] +fn test_crate::{impl test_crate::From<&'_0 (bool)> for bool}::from<'_0>(@1: &'_0 (bool)) -> core::result::Result[core::marker::Sized, core::marker::Sized<()>] { let @0: core::result::Result[core::marker::Sized, core::marker::Sized<()>]; // return let v@1: &'_ (bool); // arg #1 diff --git a/charon/tests/ui/type_alias.out b/charon/tests/ui/type_alias.out index 00f9636d..2f551847 100644 --- a/charon/tests/ui/type_alias.out +++ b/charon/tests/ui/type_alias.out @@ -1,13 +1,7 @@ # Final LLBC before serialization: -type test_crate::Foo = usize - trait core::marker::Sized -type test_crate::Generic<'a, T> - where - [@TraitClause0]: core::marker::Sized, = &'a (T) - trait core::clone::Clone { parent_clause0 : [@TraitClause0]: core::marker::Sized @@ -81,14 +75,15 @@ where fn clone_into<'_0, '_1> = alloc::slice::{impl alloc::borrow::ToOwned for Slice}#9::clone_into<'_0_0, '_0_1, T>[@TraitClause0, @TraitClause1] } -type test_crate::Generic2<'a, T> +struct test_crate::Generic2<'a, T> where [@TraitClause0]: core::marker::Sized, - [@TraitClause1]: core::clone::Clone, = alloc::borrow::Cow<'a, Slice>[alloc::slice::{impl alloc::borrow::ToOwned for Slice}#9[@TraitClause0, @TraitClause1]] - -type test_crate::GenericWithoutBound<'a, T> - where - [@TraitClause0]: core::marker::Sized, = alloc::borrow::Cow<'a, Slice>[UNKNOWN(Could not find a clause for `Binder { value: <[T] as std::borrow::ToOwned>, bound_vars: [] }` in the current context: `Unimplemented`)] + [@TraitClause1]: core::clone::Clone, + T : 'a, + = +{ + alloc::borrow::Cow<'a, Slice>[alloc::slice::{impl alloc::borrow::ToOwned for Slice}#9[@TraitClause0, @TraitClause1]], +} fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self diff --git a/charon/tests/ui/type_alias.rs b/charon/tests/ui/type_alias.rs index e08f21d8..d978808c 100644 --- a/charon/tests/ui/type_alias.rs +++ b/charon/tests/ui/type_alias.rs @@ -1,5 +1,6 @@ use std::borrow::Cow; -type Foo = usize; -type Generic<'a, T> = &'a T; -type Generic2<'a, T: Clone> = Cow<'a, [T]>; -type GenericWithoutBound<'a, T> = Cow<'a, [T]>; +// type Foo = usize; +// type Generic<'a, T> = &'a T; +// type Generic2<'a, T: Clone> = Cow<'a, [T]>; +// type GenericWithoutBound<'a, T> = Cow<'a, [T]>; +struct Generic2<'a, T: Clone>(Cow<'a, [T]>); diff --git a/charon/tests/ui/unsupported/issue-79-bound-regions.out b/charon/tests/ui/unsupported/issue-79-bound-regions.out index c214e0ae..54474bd6 100644 --- a/charon/tests/ui/unsupported/issue-79-bound-regions.out +++ b/charon/tests/ui/unsupported/issue-79-bound-regions.out @@ -575,7 +575,7 @@ where [@TraitClause3]: core::ops::function::FnMut, @TraitClause3::parent_clause0::Output = bool, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option[@TraitClause0]}#182<'_, T>[@TraitClause0]::Item>[core::marker::Sized<&'_ (T)>] +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>] where [@TraitClause0]: core::marker::Sized, [@TraitClause1]: core::marker::Sized

, @@ -618,7 +618,7 @@ where [@TraitClause3]: for<'_0, '_1> core::ops::function::FnMut, for<'_0, '_1> @TraitClause3::parent_clause0::Output = bool, -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182<'_, T>[@TraitClause0]::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> &'_ (T) where [@TraitClause0]: core::marker::Sized,