diff options
author | Son HO | 2023-12-05 16:47:51 +0100 |
---|---|---|
committer | GitHub | 2023-12-05 16:47:51 +0100 |
commit | 4795e5f823bc89504855d8eb946b111d9314f4d5 (patch) | |
tree | 4c35c707e74c14ad7a554147cff20b2e17c28659 /compiler/RegionsHierarchy.ml | |
parent | 789ba1473acd287814a0d659b5f5a0e480e4e9d7 (diff) | |
parent | a212ab42927e0f9ffa3ed0dfa0140b231e725008 (diff) |
Merge pull request #48 from AeneasVerif/son_closures
Prepare support for function pointers and closures
Diffstat (limited to 'compiler/RegionsHierarchy.ml')
-rw-r--r-- | compiler/RegionsHierarchy.ml | 66 |
1 files changed, 52 insertions, 14 deletions
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index e101ba49..80b67a54 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -23,6 +23,8 @@ have to compute the SCCs of the lifetimes (two lifetimes 'a and 'b may satisfy 'a : 'b and 'b : 'a, meaning they are actually equal and should be grouped together). + + TODO: we don't handle locally bound regions yet. *) open Types @@ -42,7 +44,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) (trait_impls : trait_impl TraitImplId.Map.t) (fun_name : string) - (sg : fun_sig) : region_groups = + (sg : fun_sig) : region_var_groups = log#ldebug (lazy (__FUNCTION__ ^ ": " ^ fun_name)); (* Initialize a normalization context (we may need to normalize some associated types) *) @@ -74,12 +76,27 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) - the region variables - 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 + level of the signature (this excludes the regions locally bound inside + the types, for instance at the level of an arrow type). *) + let bound_regions, bound_regions_id_subst, bound_regions_subst = + Subst.fresh_regions_with_substs_from_vars ~fail_if_not_found:true + sg.generics.regions + in + let region_id_to_var_map : RegionVarId.id RegionId.Map.t = + RegionId.Map.of_list + (List.combine bound_regions + (List.map (fun (r : region_var) -> r.index) sg.generics.regions)) + 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 r.index, s_set)) + (fun (r : region_var) -> + (RFVar (Option.get (bound_regions_id_subst r.index)), s_set)) sg.generics.regions in let s = (RStatic, RegionSet.empty) in @@ -87,10 +104,17 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) in let add_edge ~(short : region) ~(long : region) = - let m = !g in - let s = RegionMap.find short !g in - let s = RegionSet.add long s in - g := RegionMap.add short s m + (* Sanity checks *) + assert (short <> RErased); + assert (long <> RErased); + (* Ignore the locally bound regions (at the level of arrow types for instance *) + match (short, long) with + | RBVar _, _ | _, RBVar _ -> () + | _, _ -> + let m = !g in + let s = RegionMap.find short !g in + let s = RegionSet.add long s in + g := RegionMap.add short s m in let add_edge_from_region_constraint ((long, short) : region_outlives) = @@ -152,22 +176,30 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); (* We have nothing to do *) () - | TArrow (inputs, output) -> - (* TODO: this may be too constraining *) - List.iter (explore_ty outer) (output :: inputs) + | TArrow (regions, inputs, output) -> + (* TODO: *) + assert (regions = []); + (* We can ignore the outer regions *) + List.iter (explore_ty []) (output :: inputs) and explore_generics (outer : region list) (generics : generic_args) = let { regions; types; const_generics = _; trait_refs = _ } = generics in List.iter (fun long -> add_edges ~long ~shorts:outer) regions; List.iter (explore_ty outer) types 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 + (* Normalize the types then explore *) let tys = List.map (AssociatedTypes.norm_ctx_normalize_ty norm_ctx) (sg.output :: sg.inputs) in - List.iter (explore_ty []) tys; + List.iter explore_ty_subst tys; (* Compute the ordered SCCs *) let module Scc = SCC.Make (RegionOrderedType) in @@ -240,10 +272,12 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) let id = RegionGroupId.of_int i in (* Retrieve the set of regions in the group *) - let regions = + let regions : RegionVarId.id list = List.map (fun r -> - match r with RVar r -> r | _ -> raise (Failure "Unreachable")) + match r with + | RFVar rid -> RegionId.Map.find rid region_id_to_var_map + | _ -> raise (Failure "Unreachable")) scc in @@ -262,7 +296,8 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) (fun_decls : fun_decl FunDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) - (trait_impls : trait_impl TraitImplId.Map.t) : region_groups FunIdMap.t = + (trait_impls : trait_impl TraitImplId.Map.t) : region_var_groups FunIdMap.t + = let open Print in let env : fmt_env = { @@ -271,7 +306,10 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) global_decls; trait_decls; trait_impls; - generics = empty_generic_params; + regions = []; + types = []; + const_generics = []; + trait_clauses = []; preds = empty_predicates; locals = []; } |