From aa8c7758ed8f5981839178ada0669c42048f5b4b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 10 Dec 2024 17:14:36 +0100 Subject: [PATCH 1/6] Remove `visit_region_id` --- src/interp/InterpreterLoopsMatchCtxs.ml | 9 ++++++++- src/interp/InterpreterUtils.ml | 9 ++++++++- src/llbc/Substitute.ml | 10 +++++++++- src/llbc/Values.ml | 16 ++-------------- 4 files changed, 27 insertions(+), 17 deletions(-) diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml index 57621a86..01fe7355 100644 --- a/src/interp/InterpreterLoopsMatchCtxs.ml +++ b/src/interp/InterpreterLoopsMatchCtxs.ml @@ -1992,7 +1992,14 @@ let match_ctx_with_target (config : config) (span : Meta.span) method! visit_symbolic_value_id _ _ = fresh_symbolic_value_id () method! visit_abstraction_id _ id = get_abs_id id - method! visit_region_id _ id = get_region_id id + + method! visit_RVar _ var = + match var with + | Free id -> RVar (Free (get_region_id id)) + | Bound _ -> RVar var + + method! visit_region_id_set _ (ids : region_id_set) : region_id_set = + RegionId.Set.map get_region_id ids (** We also need to change the abstraction kind *) method! visit_abs env abs = diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index ee845eb3..336fe61d 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -388,7 +388,14 @@ let compute_ids () = loan_ids := BorrowId.Set.add id !loan_ids method! visit_abstraction_id _ id = aids := AbstractionId.Set.add id !aids - method! visit_region_id _ id = rids := RegionId.Set.add id !rids + + method! visit_RVar _ var = + match var with + | Free id -> rids := RegionId.Set.add id !rids + | Bound _ -> () + + method! visit_region_id_set _ (ids : region_id_set) : unit = + rids := RegionId.Set.union ids !rids method! visit_symbolic_value env sv = sids := SymbolicValueId.Set.add sv.sv_id !sids; diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml index f49e1b41..2e8aea85 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -118,7 +118,15 @@ let subst_ids_visitor (subst : id_subst) = inherit [_] map_env method! visit_type_var_id _ id = subst.ty_subst id method! visit_const_generic_var_id _ id = subst.cg_subst id - method! visit_region_id _ rid = subst.r_subst rid + + method! visit_region_id_set _ (ids : region_id_set) : region_id_set = + RegionId.Set.map subst.r_subst ids + + method! visit_RVar _ var = + match var with + | Free rid -> RVar (Free (subst.r_subst rid)) + | Bound _ -> RVar var + method! visit_borrow_id _ bid = subst.bsubst bid method! visit_loan_id _ bid = subst.bsubst bid method! visit_symbolic_value_id _ id = subst.ssubst id diff --git a/src/llbc/Values.ml b/src/llbc/Values.ml index da6119b5..0fc6e50b 100644 --- a/src/llbc/Values.ml +++ b/src/llbc/Values.ml @@ -25,11 +25,6 @@ class ['self] iter_typed_value_base = object (self : 'self) inherit [_] iter_ty - (** Rename the charon name for consistency *) - method! visit_free_region_id env id = self#visit_region_id env id - - method visit_region_id _ _ = () - method visit_symbolic_value_id : 'env -> symbolic_value_id -> unit = fun _ _ -> () @@ -49,11 +44,6 @@ class ['self] map_typed_value_base = object (self : 'self) inherit [_] map_ty - (** Rename the charon name for consistency *) - method! visit_free_region_id env id = self#visit_region_id env id - - method visit_region_id _ id = id - method visit_symbolic_value_id : 'env -> symbolic_value_id -> symbolic_value_id = fun _ x -> x @@ -228,9 +218,7 @@ class ['self] iter_typed_avalue_base = method visit_msymbolic_value : 'env -> msymbolic_value -> unit = fun _ _ -> () - method visit_region_id_set : 'env -> region_id_set -> unit = - fun env ids -> RegionId.Set.iter (self#visit_region_id env) ids - + method visit_region_id_set : 'env -> region_id_set -> unit = fun _ _ -> () method visit_abstraction_id : 'env -> abstraction_id -> unit = fun _ _ -> () method visit_abstraction_id_set : 'env -> abstraction_id_set -> unit = @@ -249,7 +237,7 @@ class ['self] map_typed_avalue_base = fun _ m -> m method visit_region_id_set : 'env -> region_id_set -> region_id_set = - fun env ids -> RegionId.Set.map (self#visit_region_id env) ids + fun _ s -> s method visit_abstraction_id : 'env -> abstraction_id -> abstraction_id = fun _ x -> x From fb88ad4a099bedde58255db01a7378d66e39a124 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 10 Dec 2024 17:25:58 +0100 Subject: [PATCH 2/6] Use a single type for region ids --- src/interp/InterpreterLoopsMatchCtxs.ml | 5 +++++ src/interp/InterpreterUtils.ml | 5 +++++ src/llbc/AssociatedTypes.ml | 2 +- src/llbc/Builtin.ml | 2 +- src/llbc/RegionsHierarchy.ml | 6 +++--- src/llbc/Substitute.ml | 25 +++++++++++++++---------- src/llbc/Types.ml | 3 --- src/llbc/TypesAnalysis.ml | 14 +++++++------- src/llbc/TypesUtils.ml | 6 +++--- src/symbolic/SymbolicToPure.ml | 2 +- 10 files changed, 41 insertions(+), 29 deletions(-) diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml index 01fe7355..1da1dc6e 100644 --- a/src/interp/InterpreterLoopsMatchCtxs.ml +++ b/src/interp/InterpreterLoopsMatchCtxs.ml @@ -1993,6 +1993,11 @@ let match_ctx_with_target (config : config) (span : Meta.span) method! visit_symbolic_value_id _ _ = fresh_symbolic_value_id () method! visit_abstraction_id _ id = get_abs_id id + method! visit_region_id _ _ = + craise_opt_span __FILE__ __LINE__ None + "Region ids should not be visited directly; the visitor should catch \ + cases that contain region ids earlier." + method! visit_RVar _ var = match var with | Free id -> RVar (Free (get_region_id id)) diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index 336fe61d..31dabae4 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -389,6 +389,11 @@ let compute_ids () = method! visit_abstraction_id _ id = aids := AbstractionId.Set.add id !aids + method! visit_region_id _ _ = + craise_opt_span __FILE__ __LINE__ None + "Region ids should not be visited directly; the visitor should catch \ + cases that contain region ids earlier." + method! visit_RVar _ var = match var with | Free id -> rids := RegionId.Set.add id !rids diff --git a/src/llbc/AssociatedTypes.ml b/src/llbc/AssociatedTypes.ml index 34d8754b..e18bafa0 100644 --- a/src/llbc/AssociatedTypes.ml +++ b/src/llbc/AssociatedTypes.ml @@ -499,7 +499,7 @@ let ctx_adt_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx) (** Same as [substitute_signature] but normalizes the types *) let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx) (asubst : RegionGroupId.id -> AbstractionId.id) - (r_subst : BoundRegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) + (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) (cg_subst : ConstGenericVarId.id -> const_generic) (tr_subst : TraitClauseId.id -> trait_instance_id) (tr_self : trait_instance_id) (sg : fun_sig) diff --git a/src/llbc/Builtin.ml b/src/llbc/Builtin.ml index d25bc9bd..0ed44e92 100644 --- a/src/llbc/Builtin.ml +++ b/src/llbc/Builtin.ml @@ -36,7 +36,7 @@ open LlbcAst module Sig = struct (** A few utilities *) - let rvar_id_0 = BoundRegionId.of_int 0 + let rvar_id_0 = RegionId.of_int 0 let rvar_0 : region = RVar (zero_db_var rvar_id_0) let rg_id_0 = RegionGroupId.of_int 0 let tvar_id_0 = TypeVarId.of_int 0 diff --git a/src/llbc/RegionsHierarchy.ml b/src/llbc/RegionsHierarchy.ml index 120c882a..a52ef6b9 100644 --- a/src/llbc/RegionsHierarchy.ml +++ b/src/llbc/RegionsHierarchy.ml @@ -88,11 +88,11 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) Subst.fresh_regions_with_substs_from_vars sg.generics.regions (snd (RegionId.fresh_stateful_generator ())) in - let region_id_to_var_map : BoundRegionId.id RegionId.Map.t = + let region_id_to_var_map : RegionId.id RegionId.Map.t = RegionId.Map.of_list (List.map (fun (var_id, id) -> (id, var_id)) - (BoundRegionId.Map.bindings region_var_to_id_map)) + (RegionId.Map.bindings region_var_to_id_map)) in let subst = { Subst.empty_subst with r_subst = bound_regions_subst } in let g : RegionSet.t RegionMap.t ref = @@ -298,7 +298,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) let id = RegionGroupId.of_int i in (* Retrieve the set of regions in the group *) - let regions : BoundRegionId.id list = + let regions : RegionId.id list = List.map (fun r -> match r with diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml index 2e8aea85..b291d0e8 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -17,7 +17,7 @@ let expect_free_var span (var : ('b, 'f) de_bruijn_var) : 'f = | Free id -> id (** Substitute regions at the binding level where we start to substitute *) -let make_region_subst_from_fn (subst : BoundRegionId.id -> region) : +let make_region_subst_from_fn (subst : RegionId.id -> region) : region_db_var -> region = function (* The DeBruijn index is kept correct wrt the start of the substituttion *) | Bound (bdid, rid) when bdid = 0 -> subst rid @@ -28,20 +28,20 @@ let make_region_subst_from_fn (subst : BoundRegionId.id -> region) : Return the list of new regions and appropriate substitutions from the original region variables to the fresh regions. - TODO: simplify? we only need the subst [BoundRegionId.id -> RegionId.id] + TODO: simplify? we only need the subst [RegionId.id -> RegionId.id] *) -let fresh_regions_with_substs (region_vars : BoundRegionId.id list) +let fresh_regions_with_substs (region_vars : RegionId.id list) (fresh_region_id : unit -> region_id) : - RegionId.id BoundRegionId.Map.t - * (BoundRegionId.id -> RegionId.id) + RegionId.id RegionId.Map.t + * (RegionId.id -> RegionId.id) * (region_db_var -> region) = (* Map each region var id to a fresh region *) let rid_map = - BoundRegionId.Map.of_list + RegionId.Map.of_list (List.map (fun var -> (var, fresh_region_id ())) region_vars) in (* Generate the substitution from region var id to region *) - let rid_subst id = BoundRegionId.Map.find id rid_map in + let rid_subst id = RegionId.Map.find id rid_map in (* Generate the substitution from region to region *) let r_subst = make_region_subst_from_fn (fun id -> RVar (Free (rid_subst id))) @@ -51,8 +51,8 @@ let fresh_regions_with_substs (region_vars : BoundRegionId.id list) let fresh_regions_with_substs_from_vars (region_vars : region_var list) (fresh_region_id : unit -> region_id) : - RegionId.id BoundRegionId.Map.t - * (BoundRegionId.id -> RegionId.id) + RegionId.id RegionId.Map.t + * (RegionId.id -> RegionId.id) * (region_db_var -> region) = fresh_regions_with_substs (List.map (fun (r : region_var) -> r.index) region_vars) @@ -64,7 +64,7 @@ let fresh_regions_with_substs_from_vars (region_vars : region_var list) **IMPORTANT:** this function doesn't normalize the types. *) let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id) - (r_subst : BoundRegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) + (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) (cg_subst : ConstGenericVarId.id -> const_generic) (tr_subst : TraitClauseId.id -> trait_instance_id) (tr_self : trait_instance_id) (sg : fun_sig) @@ -119,6 +119,11 @@ let subst_ids_visitor (subst : id_subst) = method! visit_type_var_id _ id = subst.ty_subst id method! visit_const_generic_var_id _ id = subst.cg_subst id + method! visit_region_id _ _ = + craise_opt_span __FILE__ __LINE__ None + "Region ids should not be visited directly; the visitor should catch \ + cases that contain region ids earlier." + method! visit_region_id_set _ (ids : region_id_set) : region_id_set = RegionId.Set.map subst.r_subst ids diff --git a/src/llbc/Types.ml b/src/llbc/Types.ml index 551c5536..1a8edb0e 100644 --- a/src/llbc/Types.ml +++ b/src/llbc/Types.ml @@ -1,6 +1,3 @@ include Charon.Types -module RegionId = FreeRegionId -type bound_region_id = BoundRegionId.id [@@deriving show, ord] -type region_id = RegionId.id [@@deriving show, ord] type region_id_set = RegionId.Set.t [@@deriving show, ord] diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml index d2c68d91..ca8b44e2 100644 --- a/src/llbc/TypesAnalysis.ml +++ b/src/llbc/TypesAnalysis.ml @@ -35,7 +35,7 @@ type 'p g_type_info = { (** If true, it means the type is a record that we should extract as a tuple. This field is only valid for type declarations. *) - mut_regions : BoundRegionId.Set.t; + mut_regions : RegionId.Set.t; (** The set of regions used in mutable borrows *) } [@@deriving show] @@ -83,7 +83,7 @@ let initialize_g_type_info (is_tuple_struct : bool) (param_infos : 'p) : borrows_info = type_borrows_info_init; is_tuple_struct; param_infos; - mut_regions = BoundRegionId.Set.empty; + mut_regions = RegionId.Set.empty; } let initialize_type_decl_info (is_rec : bool) (def : type_decl) : type_decl_info @@ -137,11 +137,11 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref) in let r_is_static (r : region) : bool = r = RStatic in let update_mut_regions_with_rid mut_regions rid = - let rid = BoundRegionId.of_int (RegionId.to_int rid) in - if BoundRegionId.Set.mem rid mut_regions then ty_info.mut_regions + let rid = RegionId.of_int (RegionId.to_int rid) in + if RegionId.Set.mem rid mut_regions then ty_info.mut_regions else ( updated := true; - BoundRegionId.Set.add rid mut_regions) + RegionId.Set.add rid mut_regions) in let update_mut_regions mut_regions mut_region = match mut_region with @@ -343,11 +343,11 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref) (* We can have bound vars because of arrows, and erased regions when analyzing types appearing in function bodies *) | RVar (Free rid) -> - if BoundRegionId.Set.mem adt_rid adt_info.mut_regions then + if RegionId.Set.mem adt_rid adt_info.mut_regions then update_mut_regions_with_rid mut_regions rid else mut_regions) ty_info.mut_regions - (BoundRegionId.mapi + (RegionId.mapi (fun adt_rid r -> (adt_rid, r)) generics.regions) in diff --git a/src/llbc/TypesUtils.ml b/src/llbc/TypesUtils.ml index 21fc7048..0dfe226d 100644 --- a/src/llbc/TypesUtils.ml +++ b/src/llbc/TypesUtils.ml @@ -92,10 +92,10 @@ let ty_has_mut_borrow_for_region_in_pred (infos : TypesAnalysis.type_infos) | TTuple | TBuiltin (TBox | TArray | TSlice | TStr) -> () | TAdtId adt_id -> let info = TypeDeclId.Map.find adt_id infos in - BoundRegionId.iteri + RegionId.iteri (fun adt_rid r -> - if BoundRegionId.Set.mem adt_rid info.mut_regions && pred r - then raise Found + if RegionId.Set.mem adt_rid info.mut_regions && pred r then + raise Found else ()) generics.regions end; diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index 9a3f1a65..3602e4c6 100644 --- a/src/symbolic/SymbolicToPure.ml +++ b/src/symbolic/SymbolicToPure.ml @@ -1620,7 +1620,7 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx) let rg = RegionGroupId.nth regions_hierarchy gid in let region_names = List.map - (fun rid -> (T.BoundRegionId.nth sg.generics.regions rid).name) + (fun rid -> (T.RegionId.nth sg.generics.regions rid).name) rg.regions in let name = From 7b7413dec81a9576bb2b2b40025873e5b7024dc7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 11 Dec 2024 10:07:52 +0100 Subject: [PATCH 3/6] `DeBruijnVar` takes a single type parameter --- src/llbc/Substitute.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml index b291d0e8..77988231 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -10,7 +10,7 @@ open ContextsBase open Errors (* Fails if the variable is bound *) -let expect_free_var span (var : ('b, 'f) de_bruijn_var) : 'f = +let expect_free_var span (var : 'id de_bruijn_var) : 'id = match var with | Bound _ -> craise_opt_span __FILE__ __LINE__ span "Found unexpected bound variable" From c776917df111384fb9f0031c6277af72bea1a403 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 11 Dec 2024 11:28:24 +0100 Subject: [PATCH 4/6] Signature-bound region vars are now `Free` --- src/interp/InterpreterUtils.ml | 4 ++-- src/llbc/Builtin.ml | 2 +- src/llbc/RegionsHierarchy.ml | 23 ++++---------------- src/llbc/Substitute.ml | 39 ++++++---------------------------- src/llbc/TypesAnalysis.ml | 11 +--------- src/symbolic/SymbolicToPure.ml | 18 ++++++---------- 6 files changed, 22 insertions(+), 75 deletions(-) diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index 31dabae4..9b45a44a 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -514,8 +514,8 @@ let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx) let asubst (rg_id : RegionGroupId.id) : AbstractionId.id = RegionGroupId.Map.find rg_id asubst_map in - (* Generate fresh regions and their substitutions *) - let _, rsubst, _ = + (* Refresh the region ids so that we can subsequently generate more fresh regions without clash *) + let rsubst = Substitute.fresh_regions_with_substs_from_vars sg.generics.regions fresh_region_id in diff --git a/src/llbc/Builtin.ml b/src/llbc/Builtin.ml index 0ed44e92..91b5c901 100644 --- a/src/llbc/Builtin.ml +++ b/src/llbc/Builtin.ml @@ -37,7 +37,7 @@ module Sig = struct (** A few utilities *) let rvar_id_0 = RegionId.of_int 0 - let rvar_0 : region = RVar (zero_db_var rvar_id_0) + let rvar_0 : region = RVar (Free rvar_id_0) let rg_id_0 = RegionGroupId.of_int 0 let tvar_id_0 = TypeVarId.of_int 0 let tvar_0 : ty = TVar (Free tvar_id_0) diff --git a/src/llbc/RegionsHierarchy.ml b/src/llbc/RegionsHierarchy.ml index a52ef6b9..c021b5d6 100644 --- a/src/llbc/RegionsHierarchy.ml +++ b/src/llbc/RegionsHierarchy.ml @@ -80,27 +80,15 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) - the static region - edges from the region variables to the static region - Note that we introduce free variables for all the regions bound at the + Note that we only consider the regions bound at the level of the signature (this excludes the regions locally bound inside the types, for instance at the level of an arrow type). *) - let region_var_to_id_map, bound_regions_id_subst, bound_regions_subst = - Subst.fresh_regions_with_substs_from_vars sg.generics.regions - (snd (RegionId.fresh_stateful_generator ())) - in - let region_id_to_var_map : RegionId.id RegionId.Map.t = - RegionId.Map.of_list - (List.map - (fun (var_id, id) -> (id, var_id)) - (RegionId.Map.bindings region_var_to_id_map)) - in - let subst = { Subst.empty_subst with r_subst = bound_regions_subst } in let g : RegionSet.t RegionMap.t ref = let s_set = RegionSet.singleton RStatic in let m = List.map - (fun (r : region_var) -> - (RVar (Free (bound_regions_id_subst r.index)), s_set)) + (fun (r : region_var) -> (RVar (Free r.index), s_set)) sg.generics.regions in let s = (RStatic, RegionSet.empty) in @@ -214,10 +202,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) in (* Substitute the regions in a type, then explore *) - let explore_ty_subst ty = - let ty = Subst.ty_substitute subst ty in - explore_ty [] ty - in + let explore_ty_subst ty = explore_ty [] ty in (* Normalize the types then explore *) let tys = @@ -302,7 +287,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) List.map (fun r -> match r with - | RVar (Free rid) -> RegionId.Map.find rid region_id_to_var_map + | RVar (Free rid) -> rid | _ -> craise __FILE__ __LINE__ (Option.get span) "Unreachable") scc in diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml index 77988231..18b6a352 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -16,44 +16,18 @@ let expect_free_var span (var : 'id de_bruijn_var) : 'id = craise_opt_span __FILE__ __LINE__ span "Found unexpected bound variable" | Free id -> id -(** Substitute regions at the binding level where we start to substitute *) -let make_region_subst_from_fn (subst : RegionId.id -> region) : - region_db_var -> region = function - (* The DeBruijn index is kept correct wrt the start of the substituttion *) - | Bound (bdid, rid) when bdid = 0 -> subst rid - | r -> RVar r - -(** Generate fresh regions for region variables. - - Return the list of new regions and appropriate substitutions from the - original region variables to the fresh regions. - - TODO: simplify? we only need the subst [RegionId.id -> RegionId.id] - *) +(** Generate fresh regions for region variables. *) let fresh_regions_with_substs (region_vars : RegionId.id list) - (fresh_region_id : unit -> region_id) : - RegionId.id RegionId.Map.t - * (RegionId.id -> RegionId.id) - * (region_db_var -> region) = + (fresh_region_id : unit -> region_id) : RegionId.id -> RegionId.id = (* Map each region var id to a fresh region *) let rid_map = RegionId.Map.of_list (List.map (fun var -> (var, fresh_region_id ())) region_vars) in - (* Generate the substitution from region var id to region *) - let rid_subst id = RegionId.Map.find id rid_map in - (* Generate the substitution from region to region *) - let r_subst = - make_region_subst_from_fn (fun id -> RVar (Free (rid_subst id))) - in - (* Return *) - (rid_map, rid_subst, r_subst) + fun id -> RegionId.Map.find id rid_map let fresh_regions_with_substs_from_vars (region_vars : region_var list) - (fresh_region_id : unit -> region_id) : - RegionId.id RegionId.Map.t - * (RegionId.id -> RegionId.id) - * (region_db_var -> region) = + (fresh_region_id : unit -> region_id) : RegionId.id -> RegionId.id = fresh_regions_with_substs (List.map (fun (r : region_var) -> r.index) region_vars) fresh_region_id @@ -69,8 +43,9 @@ let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id) (tr_subst : TraitClauseId.id -> trait_instance_id) (tr_self : trait_instance_id) (sg : fun_sig) (regions_hierarchy : region_var_groups) : inst_fun_sig = - let r_subst' = - make_region_subst_from_fn (fun id -> RVar (Free (r_subst id))) + let r_subst' = function + | Bound _ as var -> RVar var + | Free id -> RVar (Free (r_subst id)) in let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in let inputs = List.map (ty_substitute subst) sg.inputs in diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml index ca8b44e2..b395f531 100644 --- a/src/llbc/TypesAnalysis.ml +++ b/src/llbc/TypesAnalysis.ml @@ -347,9 +347,7 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref) update_mut_regions_with_rid mut_regions rid else mut_regions) ty_info.mut_regions - (RegionId.mapi - (fun adt_rid r -> (adt_rid, r)) - generics.regions) + (RegionId.mapi (fun adt_rid r -> (adt_rid, r)) generics.regions) in (* Return *) { ty_info with mut_regions } @@ -394,13 +392,6 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos) | Opaque | TError _ -> craise __FILE__ __LINE__ def.item_meta.span "unreachable" in - (* Substitute the regions in the fields *) - let _, _, r_subst = - Substitute.fresh_regions_with_substs_from_vars def.generics.regions - (snd (RegionId.fresh_stateful_generator ())) - in - let subst = { Substitute.empty_subst with r_subst } in - let fields_tys = List.map (Substitute.ty_substitute subst) fields_tys in (* Explore the types and accumulate information *) let type_decl_info = TypeDeclId.Map.find def.def_id infos in let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index 3602e4c6..3c3fd616 100644 --- a/src/symbolic/SymbolicToPure.ml +++ b/src/symbolic/SymbolicToPure.ml @@ -1152,22 +1152,18 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed let translate_back_ty_for_gid (gid : T.RegionGroupId.id) (ty : T.ty) : ty option = let rg = T.RegionGroupId.nth regions_hierarchy gid in - (* Turn *all* the outer bound regions into free regions *) - let _, rid_subst, r_subst = - Substitute.fresh_regions_with_substs_from_vars sg.generics.regions - (snd (T.RegionId.fresh_stateful_generator ())) - in - let subst = { Substitute.empty_subst with r_subst } in - let ty = Substitute.ty_substitute subst ty in (* Compute the set of regions belonging to this group *) - let gr_regions = T.RegionId.Set.of_list (List.map rid_subst rg.regions) in + let gr_regions = T.RegionId.Set.of_list rg.regions in let keep_region r = match r with - | T.RStatic -> craise_opt_span __FILE__ __LINE__ span "Unimplemented" + | T.RStatic -> + craise_opt_span __FILE__ __LINE__ span "Unimplemented: static region" | RErased -> craise_opt_span __FILE__ __LINE__ span "Unexpected erased region" - | RVar (Bound _) -> - craise_opt_span __FILE__ __LINE__ span "Unexpected bound region" + | RVar (Bound _ as var) -> + craise_opt_span __FILE__ __LINE__ span + ("Unexpected bound region: " + ^ Charon.PrintTypes.region_db_var_to_pretty_string var) | RVar (Free rid) -> T.RegionId.Set.mem rid gr_regions in let inside_mut = false in From ee3ac39268366aca00e3d08146c1717be4ae53bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 11 Dec 2024 14:55:06 +0100 Subject: [PATCH 5/6] Update to new substitution API --- src/interp/InterpreterStatements.ml | 18 ++++-------------- src/llbc/Substitute.ml | 18 +++++++++--------- 2 files changed, 13 insertions(+), 23 deletions(-) diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml index e78d1402..c78a3097 100644 --- a/src/interp/InterpreterStatements.ml +++ b/src/interp/InterpreterStatements.ml @@ -287,13 +287,8 @@ let get_builtin_function_return_type (span : Meta.span) (ctx : eval_ctx) (* There shouldn't be any reference to Self *) let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in let generics = Subst.generic_args_erase_regions generics in - let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = - Subst.make_subst_from_generics sg.generics generics tr_self - in - let ty = - Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self - sg.output - in + let subst = Subst.make_subst_from_generics sg.generics generics tr_self in + let ty = Subst.erase_regions_substitute_types subst sg.output in AssociatedTypes.ctx_normalize_erase_ty span ctx ty let move_return_value (config : config) (span : Meta.span) @@ -845,13 +840,8 @@ let eval_global_as_fresh_symbolic_value (span : Meta.span) (* There shouldn't be any reference to Self *) let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in let generics = Subst.generic_args_erase_regions generics in - let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } = - Subst.make_subst_from_generics global.generics generics tr_self - in - let ty = - Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self - global.ty - in + let subst = Subst.make_subst_from_generics global.generics generics tr_self in + let ty = Subst.erase_regions_substitute_types subst global.ty in mk_fresh_symbolic_value span ty (** Evaluate a statement *) diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml index 18b6a352..80b54055 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -38,21 +38,21 @@ let fresh_regions_with_substs_from_vars (region_vars : region_var list) **IMPORTANT:** this function doesn't normalize the types. *) let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id) - (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) - (cg_subst : ConstGenericVarId.id -> const_generic) - (tr_subst : TraitClauseId.id -> trait_instance_id) - (tr_self : trait_instance_id) (sg : fun_sig) + (r_id_subst : RegionId.id -> RegionId.id) (ty_sb_subst : TypeVarId.id -> ty) + (cg_sb_subst : ConstGenericVarId.id -> const_generic) + (tr_sb_subst : TraitClauseId.id -> trait_instance_id) + (tr_sb_self : trait_instance_id) (sg : fun_sig) (regions_hierarchy : region_var_groups) : inst_fun_sig = - let r_subst' = function - | Bound _ as var -> RVar var - | Free id -> RVar (Free (r_subst id)) + let r_sb_subst id = RVar (Free (r_id_subst id)) in + let subst = + subst_free_vars + { r_sb_subst; ty_sb_subst; cg_sb_subst; tr_sb_subst; tr_sb_self } in - let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in let inputs = List.map (ty_substitute subst) sg.inputs in let output = ty_substitute subst sg.output in let subst_region_group (rg : region_var_group) : abs_region_group = let id = asubst rg.id in - let regions = List.map r_subst rg.regions in + let regions = List.map r_id_subst rg.regions in let parents = List.map asubst rg.parents in ({ id; regions; parents } : abs_region_group) in From 06b0c9c6ad087b8634ea8ae5f9f1d374e4ce3165 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 11 Dec 2024 15:04:22 +0100 Subject: [PATCH 6/6] Update charon pin --- charon-pin | 2 +- flake.lock | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/charon-pin b/charon-pin index 0f87c3e8..29ec2632 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -b487babe3ae3021b484373ce59196896e3b43448 +c114a3aabc989b5ea3d72c3eccbde9869834460e diff --git a/flake.lock b/flake.lock index 38796eff..30627d90 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1733735940, - "narHash": "sha256-4eZTI72w5iTqV31z99ErYi2/q1cEfc/ZZCuI5ZoEIaI=", + "lastModified": 1733929967, + "narHash": "sha256-RaCG23BtUsa6iCoFBgS5Uv7FdLzKQX8zPFHBDvl/v58=", "owner": "aeneasverif", "repo": "charon", - "rev": "b487babe3ae3021b484373ce59196896e3b43448", + "rev": "c114a3aabc989b5ea3d72c3eccbde9869834460e", "type": "github" }, "original": {