From 9619d9c9ace40bafc4b806172b4615a7559ddfaf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 7 Jan 2025 17:36:15 +0100 Subject: [PATCH 1/6] Reorganize the main `translate` function --- charon/src/bin/charon-driver/driver.rs | 122 +++++++++++-------------- charon/src/transform/mod.rs | 24 +++++ 2 files changed, 75 insertions(+), 71 deletions(-) diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index a8822d9e..08886865 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -1,8 +1,9 @@ use crate::translate::translate_crate_to_ullbc; use charon_lib::export; use charon_lib::options; +use charon_lib::options::CliOpts; use charon_lib::transform::{ - FINAL_CLEANUP_PASSES, INITIAL_CLEANUP_PASSES, LLBC_PASSES, ULLBC_PASSES, + Pass, PrintCtxPass, FINAL_CLEANUP_PASSES, INITIAL_CLEANUP_PASSES, LLBC_PASSES, ULLBC_PASSES, }; use rustc_driver::{Callbacks, Compilation}; use rustc_interface::{interface::Compiler, Queries}; @@ -197,86 +198,65 @@ pub fn get_args_crate_index>(args: &[T]) -> Option }) } -/// Translate a crate to LLBC (Low-Level Borrow Calculus). -/// -/// This function is a callback function for the Rust compiler. -pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateData { - trace!(); - let options = &internal.options; - - // Some important notes about crates and how to interact with rustc: - // - when calling rustc, we should give it the root of the crate, for - // instance the "main.rs" file. From there, rustc will load all the - // *modules* (i.e., files) in the crate - // - whenever there is a `mod MODULE` in a file (for instance, in the - // "main.rs" file), it becomes a Module HIR item - - // # Translate the declarations in the crate. - // We translate the declarations in an ad-hoc order, and do not group - // the mutually recursive groups - we do this in the next step. - let mut ctx = translate_crate_to_ullbc::translate(options, tcx, internal.sysroot.clone()); - - if options.print_original_ullbc { - println!("# ULLBC after translation from MIR:\n\n{ctx}\n"); - } else { - trace!("# ULLBC after translation from MIR:\n\n{ctx}\n"); - } - - // - // ================= - // **Micro-passes**: - // ================= - // At this point, the bulk of the translation is done. From now onwards, - // we simply apply some micro-passes to make the code cleaner, before - // serializing the result. +/// Calculate the list of passes we will run on the crate before outputting it. +pub fn transformation_passes(options: &CliOpts) -> Vec { + let print_original_ullbc = PrintCtxPass::new( + options.print_original_ullbc, + format!("# ULLBC after translation from MIR"), + ); + let print_ullbc = PrintCtxPass::new(options.print_ullbc, { + let next_phase = if options.ullbc { + "serialization" + } else { + "control-flow reconstruction" + }; + format!("# Final ULLBC before {next_phase}") + }); + let print_llbc = PrintCtxPass::new( + options.print_llbc, + format!("# Final LLBC before serialization"), + ); - // Run the micro-passes that clean up bodies. - for pass in INITIAL_CLEANUP_PASSES.iter() { - trace!("# Starting pass {}", pass.name()); - pass.run(&mut ctx) - } - for pass in ULLBC_PASSES.iter() { - trace!("# Starting pass {}", pass.name()); - pass.run(&mut ctx) - } - - let next_phase = if options.ullbc { - "serialization" - } else { - "control-flow reconstruction" - }; - if options.print_ullbc { - println!("# Final ULLBC before {next_phase}:\n\n{ctx}\n"); - } else { - trace!("# Final ULLBC before {next_phase}:\n\n{ctx}\n"); - } + let mut passes: Vec = vec![]; + passes.push(Pass::NonBody(print_original_ullbc)); + passes.extend(INITIAL_CLEANUP_PASSES); + passes.extend(ULLBC_PASSES); + passes.push(Pass::NonBody(print_ullbc)); // # There are two options: // - either the user wants the unstructured LLBC, in which case we stop there - // - or they want the structured LLBC, in which case we reconstruct the - // control-flow and apply micro-passes + // - or they want the structured LLBC, in which case we reconstruct the control-flow and apply + // more micro-passes if !options.ullbc { - // Run the micro-passes that clean up bodies. - for pass in LLBC_PASSES.iter() { - trace!("# Starting pass {}", pass.name()); - pass.run(&mut ctx) - } - - if options.print_llbc { - println!("# Final LLBC before serialization:\n\n{ctx}\n"); - } else { - trace!("# Final LLBC before serialization:\n\n{ctx}\n"); - } + passes.extend(LLBC_PASSES); + passes.push(Pass::NonBody(print_llbc)); } - // Final passes before serialization. - for pass in FINAL_CLEANUP_PASSES.iter() { + passes.extend(FINAL_CLEANUP_PASSES); + passes +} + +/// Translate a crate to LLBC (Low-Level Borrow Calculus). +/// +/// This function is a callback function for the Rust compiler. The `tcx` parameter allows us to +/// interact with compiler internals to explore the crates and translate relevant items. +pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateData { + trace!(); + let options = &internal.options; + + // Translate the contents of the crate. + let mut transform_ctx = + translate_crate_to_ullbc::translate(options, tcx, internal.sysroot.clone()); + + // The bulk of the translation is done, we no longer need to interact with rustc internals. We + // 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 ctx) + pass.run(&mut transform_ctx) } // Update the error count - internal.error_count = ctx.errors.error_count; + internal.error_count = transform_ctx.errors.error_count; - export::CrateData::new(&ctx) + export::CrateData::new(&transform_ctx) } diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 3eb339d9..f4fa13ce 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -173,3 +173,27 @@ impl Pass { } } } + +pub struct PrintCtxPass { + pub message: String, + /// Whether we're printing to stdout or only logging. + pub to_stdout: bool, +} + +impl PrintCtxPass { + pub fn new(to_stdout: bool, message: String) -> &'static Self { + let ret = Self { message, to_stdout }; + Box::leak(Box::new(ret)) + } +} + +impl TransformPass for PrintCtxPass { + fn transform_ctx(&self, ctx: &mut TransformCtx) { + let message = &self.message; + if self.to_stdout { + println!("{message}:\n\n{ctx}\n"); + } else { + trace!("{message}:\n\n{ctx}\n"); + } + } +} From 6b2712f14d55db82a58aa9b9bd93b98900058626 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 8 Jan 2025 15:03:55 +0100 Subject: [PATCH 2/6] Let ml visitors substitute arbitrary items --- charon-ml/src/Substitute.ml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index a47b8264..555598e8 100644 --- a/charon-ml/src/Substitute.ml +++ b/charon-ml/src/Substitute.ml @@ -158,14 +158,20 @@ let st_substitute_visitor = (* Note that we don't visit the bound variables. *) let { binder_params; binder_value } = x in (* Crucial: we shift the substitution to be valid under this binder. *) - let binder_value = visit_value (shift_subst subst) binder_value in + let subst = shift_subst subst in + let binder_params = self#visit_generic_params subst binder_params in + let binder_value = visit_value subst binder_value in { binder_params; binder_value } method! visit_region_binder visit_value (subst : subst) x = (* Note that we don't visit the bound variables. *) let { binder_regions; binder_value } = x in (* Crucial: we shift the substitution to be valid under this binder. *) - let binder_value = visit_value (shift_subst subst) binder_value in + let subst = shift_subst subst in + let binder_regions = + self#visit_list self#visit_region_var subst binder_regions + in + let binder_value = visit_value subst binder_value in { binder_regions; binder_value } method! visit_RVar (subst : subst) var = subst.r_subst var @@ -173,14 +179,6 @@ let st_substitute_visitor = method! visit_CgVar (subst : subst) var = subst.cg_subst var method! visit_Clause (subst : subst) var = subst.tr_subst var method! visit_Self (subst : subst) = subst.tr_self - - method! visit_type_var_id _ _ = - (* We should never get here because we reimplemented [visit_TypeVar] *) - raise (Failure "Unexpected") - - method! visit_const_generic_var_id _ _ = - (* We should never get here because we reimplemented [visit_Var] *) - raise (Failure "Unexpected") end (** Substitute types variables and regions in a type. From 46085469d0adb12c0a95a00cecaac2250c4e7a12 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 8 Jan 2025 15:09:16 +0100 Subject: [PATCH 3/6] Use upstream hax again --- charon/Cargo.lock | 6 +++--- charon/Cargo.toml | 3 +-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/charon/Cargo.lock b/charon/Cargo.lock index c7fb22fc..52dc1fb5 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -816,7 +816,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-rc.1" -source = "git+https://github.com/Nadrieril/hax?branch=fix-call-generics#79e2da0452a0b94056becba46b98304ca230a502" +source = "git+https://github.com/hacspec/hax?branch=main#98ded931baf06ffb5802d1b55cd42ef39177beb6" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -827,7 +827,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-rc.1" -source = "git+https://github.com/Nadrieril/hax?branch=fix-call-generics#79e2da0452a0b94056becba46b98304ca230a502" +source = "git+https://github.com/hacspec/hax?branch=main#98ded931baf06ffb5802d1b55cd42ef39177beb6" dependencies = [ "extension-traits", "hax-adt-into", @@ -844,7 +844,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-rc.1" -source = "git+https://github.com/Nadrieril/hax?branch=fix-call-generics#79e2da0452a0b94056becba46b98304ca230a502" +source = "git+https://github.com/hacspec/hax?branch=main#98ded931baf06ffb5802d1b55cd42ef39177beb6" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 5d060a00..7abc7a88 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -76,8 +76,7 @@ tracing = { version = "0.1", features = [ "max_level_trace" ] } wait-timeout = { version = "0.2.0", optional = true } which = "7.0" -# hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true } -hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "fix-call-generics", optional = true } +hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true } # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true } macros = { path = "./macros" } From 23a268cdc2df018edaec529fd060d2b67d799792 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Jan 2025 01:26:25 +0100 Subject: [PATCH 4/6] Add a helper --- charon/src/ast/types_utils.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index e6e16bee..fe85bfe7 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -118,6 +118,19 @@ impl Binder { } } +impl RegionBinder { + /// Wrap the value in an empty region binder, shifting variables appropriately. + pub fn empty(x: T) -> Self + where + T: TyVisitable, + { + RegionBinder { + regions: Default::default(), + skip_binder: x.move_under_binder(), + } + } +} + impl GenericArgs { pub fn len(&self) -> usize { let GenericArgs { @@ -557,6 +570,11 @@ pub trait TyVisitable: Sized + AstVisitable { self.drive_mut(&mut SubstVisitor::new(generics)); } + /// Move under one binder. + fn move_under_binder(self) -> Self { + self.move_under_binders(DeBruijnId::one()) + } + /// Move under `depth` binders. fn move_under_binders(mut self, depth: DeBruijnId) -> Self { let Continue(()) = self.visit_db_id::(|id| { From 860aa476f3270598508e5d322ab7e17b9c85da98 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Jan 2025 01:24:13 +0100 Subject: [PATCH 5/6] Track the origin of each binder --- charon-ml/src/CharonVersion.ml | 2 +- .../src/generated/Generated_GAstOfJson.ml | 21 +++++-- charon-ml/src/generated/Generated_Types.ml | 19 ++++-- charon/Cargo.lock | 2 +- charon/Cargo.toml | 2 +- charon/src/ast/types.rs | 21 ++++++- charon/src/ast/types_utils.rs | 3 +- .../charon-driver/translate/translate_ctx.rs | 3 + .../translate/translate_traits.rs | 60 ++++++++++++------- .../transform/skip_trait_refs_when_known.rs | 7 ++- 10 files changed, 100 insertions(+), 40 deletions(-) diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index e312aef4..1ec2b06e 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.61" +let supported_charon_version = "0.1.62" diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index 6222a456..9d2a6036 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -1063,12 +1063,12 @@ and generics_source_of_json (ctx : of_json_ctx) (js : json) : (match js with | `Assoc [ ("Item", item) ] -> let* item = any_decl_id_of_json ctx item in - Ok (Item item) + Ok (GSItem item) | `Assoc [ ("Method", `List [ x_0; x_1 ]) ] -> let* x_0 = trait_decl_id_of_json ctx x_0 in let* x_1 = trait_item_name_of_json ctx x_1 in - Ok (Method (x_0, x_1)) - | `String "Builtin" -> Ok Builtin + Ok (GSMethod (x_0, x_1)) + | `String "Builtin" -> Ok GSBuiltin | _ -> Error "") and generic_args_of_json (ctx : of_json_ctx) (js : json) : @@ -1115,6 +1115,18 @@ and region_binder_of_json : Ok ({ binder_regions; binder_value } : _ region_binder) | _ -> Error "") +and binder_kind_of_json (ctx : of_json_ctx) (js : json) : + (binder_kind, string) result = + combine_error_msgs js __FUNCTION__ + (match js with + | `Assoc [ ("TraitMethod", `List [ x_0; x_1 ]) ] -> + let* x_0 = trait_decl_id_of_json ctx x_0 in + let* x_1 = trait_item_name_of_json ctx x_1 in + Ok (BKTraitMethod (x_0, x_1)) + | `String "InherentImplBlock" -> Ok BKInherentImplBlock + | `String "Other" -> Ok BKOther + | _ -> Error "") + and binder_of_json : 'a0. (of_json_ctx -> json -> ('a0, string) result) -> @@ -1124,7 +1136,8 @@ and binder_of_json : fun arg0_of_json ctx js -> combine_error_msgs js __FUNCTION__ (match js with - | `Assoc [ ("params", params); ("skip_binder", skip_binder) ] -> + | `Assoc [ ("params", params); ("skip_binder", skip_binder); ("kind", _) ] + -> let* binder_params = generic_params_of_json ctx params in let* binder_value = arg0_of_json ctx skip_binder in Ok ({ binder_params; binder_value } : _ binder) diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index c4ba1651..fea1661e 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -300,9 +300,9 @@ and trait_impl_ref = { (** Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one. *) and generics_source = - | Item of any_decl_id (** A top-level item. *) - | Method of trait_decl_id * trait_item_name (** A trait method. *) - | Builtin (** A builtin item like `Box`. *) + | GSItem of any_decl_id (** A top-level item. *) + | GSMethod of trait_decl_id * trait_item_name (** A trait method. *) + | GSBuiltin (** A builtin item like `Box`. *) (** A set of generic arguments. *) and generic_args = { @@ -578,9 +578,18 @@ and trait_type_constraint = { ty : ty; } +and binder_kind = + | BKTraitMethod of trait_decl_id * trait_item_name + (** The parameters of a trait method. Used in the `methods` lists in trait decls and trait + impls. + *) + | BKInherentImplBlock + (** The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods. *) + | BKOther (** Some other use of a binder outside the main Charon ast. *) + (** A value of type `T` bound by generic parameters. Used in any context where we're adding generic - parameters that aren't on the top-level item, e.g. `for<'a>` clauses, trait methods (TODO), - GATs (TODO). + parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for + now), trait methods, GATs (TODO). *) and 'a0 binder = { binder_params : generic_params; diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 52dc1fb5..a1923657 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -213,7 +213,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.61" +version = "0.1.62" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 7abc7a88..20f8a9df 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.61" +version = "0.1.62" authors = ["Son Ho "] edition = "2021" license = "Apache-2.0" diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index e6b4b67d..62877e6d 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -197,6 +197,7 @@ pub struct TraitTypeConstraint { /// Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one. #[derive(Debug, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)] +#[charon::variants_prefix("GS")] pub enum GenericsSource { /// A top-level item. Item(AnyTransId), @@ -238,9 +239,21 @@ pub type BoundTypeOutlives = RegionBinder; pub type BoundRegionOutlives = RegionBinder; pub type BoundTraitTypeConstraint = RegionBinder; +#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] +#[charon::variants_prefix("BK")] +pub enum BinderKind { + /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait + /// impls. + TraitMethod(TraitDeclId, TraitItemName), + /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods. + InherentImplBlock, + /// Some other use of a binder outside the main Charon ast. + Other, +} + /// A value of type `T` bound by generic parameters. Used in any context where we're adding generic -/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses, trait methods (TODO), -/// GATs (TODO). +/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for +/// now), trait methods, GATs (TODO). #[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] pub struct Binder { #[charon::rename("binder_params")] @@ -249,6 +262,10 @@ pub struct Binder { /// incorrectly. Prefer using helper methods. #[charon::rename("binder_value")] pub skip_binder: T, + /// The kind of binder this is. + #[charon::opaque] + #[drive(skip)] + pub kind: BinderKind, } /// Generic parameters for a declaration. diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index fe85bfe7..430e2b6b 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -98,10 +98,11 @@ impl GenericParams { } impl Binder { - pub fn new(params: GenericParams, skip_binder: T) -> Self { + pub fn new(kind: BinderKind, params: GenericParams, skip_binder: T) -> Self { Self { params, skip_binder, + kind, } } diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 22cdbd43..49c9ac6d 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -441,6 +441,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { bt_ctx.translate_def_generics(span, &full_def)?; let ty = bt_ctx.translate_ty(span, &ty)?; ImplElem::Ty(Binder { + kind: BinderKind::InherentImplBlock, params: bt_ctx.into_generics(), skip_binder: ty, }) @@ -1247,6 +1248,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { pub(crate) fn translate_binder_for_def( &mut self, span: Span, + kind: BinderKind, def: &hax::FullDef, f: F, ) -> Result, Error> @@ -1266,6 +1268,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // Return res.map(|skip_binder| Binder { + kind, params, skip_binder, }) diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index e919ff32..520c5c99 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -88,26 +88,35 @@ impl BodyTransCtx<'_, '_> { match &hax_def.kind { hax::FullDefKind::AssocFn { .. } => { let fun_def = self.t_ctx.hax_def(item_def_id)?; - let fn_ref = self.translate_binder_for_def(item_span, &fun_def, |bt_ctx| { - let fun_id = bt_ctx.register_fun_decl_id(item_span, item_def_id); - // TODO: there's probably a cleaner way to write this - assert_eq!(bt_ctx.binding_levels.len(), 2); - let fun_generics = bt_ctx - .outermost_binder() - .params - .identity_args_at_depth(GenericsSource::item(def_id), DeBruijnId::one()) - .concat( - GenericsSource::item(fun_id), - &bt_ctx.innermost_binder().params.identity_args_at_depth( - GenericsSource::Method(def_id.into(), item_name.clone()), - DeBruijnId::zero(), - ), - ); - Ok(FunDeclRef { - id: fun_id, - generics: fun_generics, - }) - })?; + let binder_kind = BinderKind::TraitMethod(def_id, item_name.clone()); + let fn_ref = self.translate_binder_for_def( + item_span, + binder_kind, + &fun_def, + |bt_ctx| { + let fun_id = bt_ctx.register_fun_decl_id(item_span, item_def_id); + // TODO: there's probably a cleaner way to write this + assert_eq!(bt_ctx.binding_levels.len(), 2); + let fun_generics = bt_ctx + .outermost_binder() + .params + .identity_args_at_depth( + GenericsSource::item(def_id), + DeBruijnId::one(), + ) + .concat( + GenericsSource::item(fun_id), + &bt_ctx.innermost_binder().params.identity_args_at_depth( + GenericsSource::Method(def_id.into(), item_name.clone()), + DeBruijnId::zero(), + ), + ); + Ok(FunDeclRef { + id: fun_id, + generics: fun_generics, + }) + }, + )?; if hax_item.has_value { // This is a provided method, provided_methods.push((item_name.clone(), fn_ref)); @@ -257,8 +266,12 @@ impl BodyTransCtx<'_, '_> { match &impl_item.value { Provided { is_override, .. } => { let fun_def = self.t_ctx.hax_def(item_def_id)?; - let fn_ref = - self.translate_binder_for_def(item_span, &fun_def, |bt_ctx| { + let binder_kind = BinderKind::TraitMethod(trait_id, name.clone()); + let fn_ref = self.translate_binder_for_def( + item_span, + binder_kind, + &fun_def, + |bt_ctx| { // TODO: there's probably a cleaner way to write this assert_eq!(bt_ctx.binding_levels.len(), 2); let fun_generics = bt_ctx @@ -285,7 +298,8 @@ impl BodyTransCtx<'_, '_> { id: fun_id, generics: fun_generics, }) - })?; + }, + )?; if *is_override { provided_methods.push((name, fn_ref)); } else { diff --git a/charon/src/transform/skip_trait_refs_when_known.rs b/charon/src/transform/skip_trait_refs_when_known.rs index a25a8c16..ba70091b 100644 --- a/charon/src/transform/skip_trait_refs_when_known.rs +++ b/charon/src/transform/skip_trait_refs_when_known.rs @@ -37,8 +37,11 @@ fn transform_call(ctx: &mut TransformCtx, span: Span, call: &mut Call) { // Make the two levels of binding explicit: outer binder for the impl block, inner binder for // the method. - let fn_ref: Binder> = - Binder::new(trait_impl.generics.clone(), bound_fn.clone()); + let fn_ref: Binder> = Binder::new( + BinderKind::Other, + trait_impl.generics.clone(), + bound_fn.clone(), + ); // Substitute the appropriate generics into the function call. let fn_ref = fn_ref.apply(impl_generics).apply(method_generics); fn_ptr.generics = fn_ref.generics; From fec3e8f9209e41e74ff34a25639c55f4816baa12 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 5 Jan 2025 01:31:05 +0100 Subject: [PATCH 6/6] No longer need the `Bound*` type aliases --- charon/src/ast/names.rs | 5 +---- charon/src/ast/types.rs | 15 ++++----------- 2 files changed, 5 insertions(+), 15 deletions(-) diff --git a/charon/src/ast/names.rs b/charon/src/ast/names.rs index 8ce3c0b2..73f0f944 100644 --- a/charon/src/ast/names.rs +++ b/charon/src/ast/names.rs @@ -29,13 +29,10 @@ pub enum PathElem { #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)] #[charon::variants_prefix("ImplElem")] pub enum ImplElem { - Ty(BoundTy), + Ty(Binder), Trait(TraitImplId), } -/// Alias used for visitors. -pub type BoundTy = Binder; - /// An item name/path /// /// A name really is a list of strings. However, we sometimes need to diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs index 62877e6d..666521c0 100644 --- a/charon/src/ast/types.rs +++ b/charon/src/ast/types.rs @@ -234,11 +234,6 @@ pub struct RegionBinder { pub skip_binder: T, } -// Renames useful for visitor derives -pub type BoundTypeOutlives = RegionBinder; -pub type BoundRegionOutlives = RegionBinder; -pub type BoundTraitTypeConstraint = RegionBinder; - #[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)] #[charon::variants_prefix("BK")] pub enum BinderKind { @@ -283,11 +278,11 @@ pub struct GenericParams { // TODO: rename to match [GenericArgs]? pub trait_clauses: Vector, /// The first region in the pair outlives the second region - pub regions_outlive: Vec, + pub regions_outlive: Vec>, /// The type outlives the region - pub types_outlive: Vec, + pub types_outlive: Vec>, /// Constraints over trait associated types - pub trait_type_constraints: Vec, + pub trait_type_constraints: Vec>, } /// A predicate of the form `exists where T: Trait`. @@ -694,11 +689,9 @@ pub enum TyKind { /// This is essentially a "constrained" function signature: /// arrow types can only contain generic lifetime parameters /// (no generic types), no predicates, etc. - Arrow(BoundArrowSig), + Arrow(RegionBinder<(Vec, Ty)>), } -pub type BoundArrowSig = RegionBinder<(Vec, Ty)>; - /// Builtin types identifiers. /// /// WARNING: for now, all the built-in types are covariant in the generic