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": { diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml index 57621a86..1da1dc6e 100644 --- a/src/interp/InterpreterLoopsMatchCtxs.ml +++ b/src/interp/InterpreterLoopsMatchCtxs.ml @@ -1992,7 +1992,19 @@ 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_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)) + | 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/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/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index ee845eb3..9b45a44a 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -388,7 +388,19 @@ 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_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 + | 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; @@ -502,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/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..91b5c901 100644 --- a/src/llbc/Builtin.ml +++ b/src/llbc/Builtin.ml @@ -36,8 +36,8 @@ open LlbcAst module Sig = struct (** A few utilities *) - let rvar_id_0 = BoundRegionId.of_int 0 - let rvar_0 : region = RVar (zero_db_var rvar_id_0) + let rvar_id_0 = RegionId.of_int 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 120c882a..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 : BoundRegionId.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)) - 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 = @@ -298,11 +283,11 @@ 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 - | 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 f49e1b41..80b54055 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -10,50 +10,24 @@ 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" | Free id -> id -(** Substitute regions at the binding level where we start to substitute *) -let make_region_subst_from_fn (subst : BoundRegionId.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 [BoundRegionId.id -> RegionId.id] - *) -let fresh_regions_with_substs (region_vars : BoundRegionId.id list) - (fresh_region_id : unit -> region_id) : - RegionId.id BoundRegionId.Map.t - * (BoundRegionId.id -> RegionId.id) - * (region_db_var -> region) = +(** 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.id = (* 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 - (* 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 BoundRegionId.Map.t - * (BoundRegionId.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 @@ -64,20 +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 : BoundRegionId.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' = - make_region_subst_from_fn (fun 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 @@ -118,7 +93,20 @@ 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 _ _ = + 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 + + 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/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..b395f531 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,13 +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 - (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/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/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 diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index 9a3f1a65..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 @@ -1620,7 +1616,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 =