From 0e84aeeedfa9060228c4b3bfc44ce35805ec4464 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 12 Dec 2024 11:49:57 +0000 Subject: [PATCH 1/2] Make minor modifications --- src/interp/InterpreterLoopsMatchCtxs.ml | 10 +++++++--- src/interp/InterpreterUtils.ml | 5 ++++- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml index 1da1dc6e..789303ac 100644 --- a/src/interp/InterpreterLoopsMatchCtxs.ml +++ b/src/interp/InterpreterLoopsMatchCtxs.ml @@ -1995,12 +1995,16 @@ let match_ctx_with_target (config : config) (span : Meta.span) 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." + "Internal error: 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)) + | Free id -> + (* If the bound region is free, then it is a region owned + by an abstraction, so we do the same as for the case + [abs_region_id]. *) + RVar (Free (get_region_id id)) | Bound _ -> RVar var method! visit_region_id_set _ (ids : region_id_set) : region_id_set = diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index 9b45a44a..8e00866a 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -342,6 +342,9 @@ type ids_sets = { loan_ids : BorrowId.Set.t; (** Only the loan ids *) dids : DummyVarId.Set.t; rids : RegionId.Set.t; + (** This should only contain **free** region ids (note that we have to be + careful because we use the same index type for bound regions and free + regions - see the implementation of [compute_ids] below) *) sids : SymbolicValueId.Set.t; } [@@deriving show] @@ -514,7 +517,7 @@ 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 - (* Refresh the region ids so that we can subsequently generate more fresh regions without clash *) + (* Generate fresh regions *) let rsubst = Substitute.fresh_regions_with_substs_from_vars sg.generics.regions fresh_region_id From e5e240aba5c4dd51e4e4b934421df0bbcce1b776 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 12 Dec 2024 13:55:25 +0000 Subject: [PATCH 2/2] Introduce the abs_regions helper type --- src/interp/Interpreter.ml | 8 +++-- src/interp/InterpreterBorrows.ml | 38 ++++++++++++++++-------- src/interp/InterpreterBorrowsCore.ml | 6 ++-- src/interp/InterpreterExpansion.ml | 6 ++-- src/interp/InterpreterLoopsFixedPoint.ml | 12 +++++--- src/interp/InterpreterLoopsMatchCtxs.ml | 34 +++++++++++++-------- src/interp/InterpreterStatements.ml | 28 ++++++++--------- src/interp/InterpreterUtils.ml | 5 ++-- src/interp/Invariants.ml | 10 +++---- src/llbc/Print.ml | 2 +- src/llbc/Substitute.ml | 7 +++-- src/llbc/Values.ml | 12 +++++--- 12 files changed, 101 insertions(+), 67 deletions(-) diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml index ed7ce976..589cf976 100644 --- a/src/interp/Interpreter.ml +++ b/src/interp/Interpreter.ml @@ -209,7 +209,9 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : eval_ctx * typed_avalue list = (* Project over the values - we use *loan* projectors, as explained above *) let avalues = - List.map (mk_aproj_loans_value_from_symbolic_value abs.regions) input_svs + List.map + (mk_aproj_loans_value_from_symbolic_value abs.regions.owned) + input_svs in (ctx, avalues) in @@ -308,8 +310,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : eval_ctx * typed_avalue list = let ctx, avalue = - apply_proj_borrows_on_input_value config span ctx abs.regions - abs.ancestors_regions ret_value ret_rty + apply_proj_borrows_on_input_value config span ctx abs.regions.owned + abs.regions.ancestors ret_value ret_rty in (ctx, [ avalue ]) in diff --git a/src/interp/InterpreterBorrows.ml b/src/interp/InterpreterBorrows.ml index bcffdb03..c366c64d 100644 --- a/src/interp/InterpreterBorrows.ml +++ b/src/interp/InterpreterBorrows.ml @@ -348,7 +348,8 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) let given_back_meta = as_symbolic span nv.value in (* The loan projector *) let given_back = - mk_aproj_loans_value_from_symbolic_value abs.regions sv + mk_aproj_loans_value_from_symbolic_value abs.regions.owned + sv in (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in @@ -372,7 +373,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) let regions, ancestors_regions = match opt_abs with | None -> craise __FILE__ __LINE__ span "Unreachable" - | Some abs -> (abs.regions, abs.ancestors_regions) + | Some abs -> (abs.regions.owned, abs.regions.ancestors) in (* Rk.: there is a small issue with the types of the aloan values. * See the comment at the level of definition of {!typed_avalue} *) @@ -1069,7 +1070,9 @@ and end_abstraction_aux (config : config) (span : Meta.span) relookup the abstraction: the set of regions in an abstraction never changes... *) let ctx = - let ended_regions = RegionId.Set.union ctx.ended_regions abs.regions in + let ended_regions = + RegionId.Set.union ctx.ended_regions abs.regions.owned + in { ctx with ended_regions } in @@ -1137,7 +1140,8 @@ and end_abstraction_loans (config : config) (span : Meta.span) (* There is a proj_loans over a symbolic value: end the proj_borrows which intersect this proj_loans, then end the proj_loans itself *) let ctx, cc = - end_proj_loans_symbolic config span chain abs_id abs.regions sv ctx + end_proj_loans_symbolic config span chain abs_id abs.regions.owned sv + ctx in (* Reexplore, looking for loans *) comp cc (end_abstraction_loans config span chain abs_id ctx) @@ -1287,7 +1291,8 @@ and end_abstraction_borrows (config : config) (span : Meta.span) let ctx = update_aproj_borrows span abs.abs_id sv ended_borrow ctx in (* Give back the symbolic value *) let ctx = - give_back_symbolic_value config span abs.regions proj_ty sv nsv ctx + give_back_symbolic_value config span abs.regions.owned proj_ty sv nsv + ctx in (* Reexplore *) end_abstraction_borrows config span chain abs_id ctx @@ -1812,7 +1817,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) have the type `& ...` - TODO: this is annoying and not very clean... *) let ty = (* Take the first region of the abstraction - this doesn't really matter *) - let r = RegionId.Set.min_elt abs0.regions in + let r = RegionId.Set.min_elt abs0.regions.owned in TRef (RVar (Free r), ty, RShared) in { value; ty } @@ -1860,8 +1865,11 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) can_end; parents = AbstractionId.Set.empty; original_parents = []; - regions = RegionId.Set.singleton r_id; - ancestors_regions = RegionId.Set.empty; + regions = + { + owned = RegionId.Set.singleton r_id; + ancestors = RegionId.Set.empty; + }; avalues; } in @@ -2924,9 +2932,14 @@ let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (AbstractionId.Set.of_list [ abs0.abs_id; abs1.abs_id ]) in let original_parents = AbstractionId.Set.elements parents in - let regions = RegionId.Set.union abs0.regions abs1.regions in - let ancestors_regions = - RegionId.Set.diff (RegionId.Set.union abs0.regions abs1.regions) regions + let regions = + let owned = RegionId.Set.union abs0.regions.owned abs1.regions.owned in + let ancestors = + RegionId.Set.diff + (RegionId.Set.union abs0.regions.ancestors abs1.regions.ancestors) + owned + in + { owned; ancestors } in let abs = { @@ -2936,7 +2949,6 @@ let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) parents; original_parents; regions; - ancestors_regions; avalues; } in @@ -2978,7 +2990,7 @@ let merge_into_first_abstraction (span : Meta.span) (abs_kind : abs_kind) is not the case if there are no nested borrows, but we anticipate). *) let ctx = - let regions = nabs.regions in + let regions = nabs.regions.owned in (* Pick the first region id (this is the smallest) *) let rid = RegionId.Set.min_elt regions in (* If there is only one region, do nothing *) diff --git a/src/interp/InterpreterBorrowsCore.ml b/src/interp/InterpreterBorrowsCore.ml index 4ffa40bf..2b71f013 100644 --- a/src/interp/InterpreterBorrowsCore.ml +++ b/src/interp/InterpreterBorrowsCore.ml @@ -738,7 +738,7 @@ let lookup_intersecting_aproj_borrows_opt (span : Meta.span) let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty = if proj_borrows_intersects_proj_loans span - (abs.regions, sv', proj_ty) + (abs.regions.owned, sv', proj_ty) (regions, sv) then let x = (abs.abs_id, proj_ty) in @@ -832,7 +832,7 @@ let update_intersecting_aproj_borrows (span : Meta.span) let check_proj_borrows is_shared abs sv' proj_ty = if proj_borrows_intersects_proj_loans span - (abs.regions, sv', proj_ty) + (abs.regions.owned, sv', proj_ty) (regions, sv) then ( if is_shared then add_shared () else set_non_shared (); @@ -994,7 +994,7 @@ let update_intersecting_aproj_loans (span : Meta.span) sanity_check __FILE__ __LINE__ (sv.sv_ty = sv'.sv_ty) span; if projections_intersect span proj_ty proj_regions sv'.sv_ty - abs.regions + abs.regions.owned then update abs given_back else super#visit_aproj (Some abs) sproj) else super#visit_aproj (Some abs) sproj diff --git a/src/interp/InterpreterExpansion.ml b/src/interp/InterpreterExpansion.ml index 9c6355ef..e3ada531 100644 --- a/src/interp/InterpreterExpansion.ml +++ b/src/interp/InterpreterExpansion.ml @@ -86,8 +86,8 @@ let apply_symbolic_expansion_to_target_avalues (config : config) method! visit_ASymbolic current_abs aproj = let current_abs = Option.get current_abs in - let proj_regions = current_abs.regions in - let ancestors_regions = current_abs.ancestors_regions in + let proj_regions = current_abs.regions.owned in + let ancestors_regions = current_abs.regions.ancestors in (* Explore in depth first - we won't update anything: we simply * want to check we don't have to expand inner symbolic value *) match (aproj, proj_kind) with @@ -336,7 +336,7 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span) method! visit_EAbs proj_regions abs = sanity_check __FILE__ __LINE__ (Option.is_none proj_regions) span; - let proj_regions = Some abs.regions in + let proj_regions = Some abs.regions.owned in super#visit_EAbs proj_regions abs method! visit_AProjSharedBorrow proj_regions asb = diff --git a/src/interp/InterpreterLoopsFixedPoint.ml b/src/interp/InterpreterLoopsFixedPoint.ml index ab6f4760..10a9141d 100644 --- a/src/interp/InterpreterLoopsFixedPoint.ml +++ b/src/interp/InterpreterLoopsFixedPoint.ml @@ -209,7 +209,9 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : let nrid = fresh_region_id () in (* Prepare the shared value *) - let nsv = mk_value_with_fresh_sids_no_shared_loans abs.regions nrid sv in + let nsv = + mk_value_with_fresh_sids_no_shared_loans abs.regions.owned nrid sv + in (* Save the borrow substitution, to apply it to the context later *) borrow_substs := (lid, nlid) :: !borrow_substs; @@ -218,7 +220,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) span; sanity_check __FILE__ __LINE__ (abs.original_parents = []) span; sanity_check __FILE__ __LINE__ - (RegionId.Set.is_empty abs.ancestors_regions) + (RegionId.Set.is_empty abs.regions.ancestors) span; (* Introduce the new abstraction for the shared values *) @@ -250,6 +252,9 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : | None -> Identity in let can_end = true in + let regions : abs_regions = + { owned = RegionId.Set.singleton nrid; ancestors = RegionId.Set.empty } + in let fresh_abs = { abs_id = fresh_abstraction_id (); @@ -257,8 +262,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : can_end; parents = AbstractionId.Set.empty; original_parents = []; - regions = RegionId.Set.singleton nrid; - ancestors_regions = RegionId.Set.empty; + regions; avalues; } in diff --git a/src/interp/InterpreterLoopsMatchCtxs.ml b/src/interp/InterpreterLoopsMatchCtxs.ml index 789303ac..cf651285 100644 --- a/src/interp/InterpreterLoopsMatchCtxs.ml +++ b/src/interp/InterpreterLoopsMatchCtxs.ml @@ -546,8 +546,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct can_end = true; parents = AbstractionId.Set.empty; original_parents = []; - regions = RegionId.Set.singleton rid; - ancestors_regions = RegionId.Set.empty; + regions = + { + owned = RegionId.Set.singleton rid; + ancestors = RegionId.Set.empty; + }; avalues; } in @@ -661,8 +664,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct can_end = true; parents = AbstractionId.Set.empty; original_parents = []; - regions = RegionId.Set.singleton rid; - ancestors_regions = RegionId.Set.empty; + regions = + { + owned = RegionId.Set.singleton rid; + ancestors = RegionId.Set.empty; + }; avalues; } in @@ -714,8 +720,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct can_end = true; parents = AbstractionId.Set.empty; original_parents = []; - regions = RegionId.Set.singleton rid; - ancestors_regions = RegionId.Set.empty; + regions = + { + owned = RegionId.Set.singleton rid; + ancestors = RegionId.Set.empty; + }; avalues; } in @@ -1388,8 +1397,7 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets) can_end = can_end0; parents = parents0; original_parents = original_parents0; - regions = regions0; - ancestors_regions = ancestors_regions0; + regions = { owned = regions0; ancestors = ancestors_regions0 }; avalues = avalues0; } = abs0 @@ -1401,8 +1409,7 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets) can_end = can_end1; parents = parents1; original_parents = original_parents1; - regions = regions1; - ancestors_regions = ancestors_regions1; + regions = { owned = regions1; ancestors = ancestors_regions1 }; avalues = avalues1; } = abs1 @@ -2007,8 +2014,11 @@ let match_ctx_with_target (config : config) (span : Meta.span) 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 + method! visit_abs_regions _ regions = + let { owned; ancestors } = regions in + let owned = RegionId.Set.map get_region_id owned in + let ancestors = RegionId.Set.map get_region_id ancestors in + { owned; ancestors } (** 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 c78a3097..73748081 100644 --- a/src/interp/InterpreterStatements.ml +++ b/src/interp/InterpreterStatements.ml @@ -514,19 +514,18 @@ let create_empty_abstractions_from_abs_region_groups AbstractionId.Set.empty rg.parents in let regions = - List.fold_left - (fun s rid -> RegionId.Set.add rid s) - RegionId.Set.empty rg.regions - in - let ancestors_regions = - List.fold_left - (fun acc parent_id -> - RegionId.Set.union acc - (AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) - RegionId.Set.empty rg.parents + let owned = RegionId.Set.of_list rg.regions in + let ancestors = + List.fold_left + (fun acc parent_id -> + RegionId.Set.union acc + (AbstractionId.Map.find parent_id !abs_to_ancestors_regions)) + RegionId.Set.empty rg.parents + in + { owned; ancestors } in let ancestors_regions_union_current_regions = - RegionId.Set.union ancestors_regions regions + RegionId.Set.union regions.owned regions.owned in let can_end = region_can_end rg_id in abs_to_ancestors_regions := @@ -540,7 +539,6 @@ let create_empty_abstractions_from_abs_region_groups parents; original_parents; regions; - ancestors_regions; avalues = []; } in @@ -1443,12 +1441,12 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let ctx, args_projs = List.fold_left_map (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config span ctx abs.regions - abs.ancestors_regions arg arg_rty) + apply_proj_borrows_on_input_value config span ctx abs.regions.owned + abs.regions.ancestors arg arg_rty) ctx args_with_rtypes in (* Group the input and output values *) - (ctx, List.append args_projs [ ret_av abs.regions ]) + (ctx, List.append args_projs [ ret_av abs.regions.owned ]) in (* Actually initialize and insert the abstractions *) let call_id = fresh_fun_call_id () in diff --git a/src/interp/InterpreterUtils.ml b/src/interp/InterpreterUtils.ml index 8e00866a..d2b5ac30 100644 --- a/src/interp/InterpreterUtils.ml +++ b/src/interp/InterpreterUtils.ml @@ -402,8 +402,9 @@ let compute_ids () = | 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_abs_regions _ (regions : abs_regions) : unit = + let { owned; ancestors } = regions in + rids := RegionId.Set.union (RegionId.Set.union owned ancestors) !rids method! visit_symbolic_value env sv = sids := SymbolicValueId.Set.add sv.sv_id !sids; diff --git a/src/interp/Invariants.ml b/src/interp/Invariants.ml index e9e20460..3f5c2f9f 100644 --- a/src/interp/Invariants.ml +++ b/src/interp/Invariants.ml @@ -695,7 +695,7 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = * otherwise they should have been reduced to [_] *) let abs = Option.get info in sanity_check __FILE__ __LINE__ - (ty_has_regions_in_set abs.regions sv.sv_ty) + (ty_has_regions_in_set abs.regions.owned sv.sv_ty) span | AProjBorrows (sv, proj_ty) -> let ty2 = Substitute.erase_regions sv.sv_ty in @@ -704,7 +704,7 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = * otherwise they should have been reduced to [_] *) let abs = Option.get info in sanity_check __FILE__ __LINE__ - (ty_has_regions_in_set abs.regions proj_ty) + (ty_has_regions_in_set abs.regions.owned proj_ty) span | AEndedProjLoans (_msv, given_back_ls) -> List.iter @@ -806,14 +806,14 @@ let check_symbolic_values (span : Meta.span) (ctx : eval_ctx) : unit = match asb with | AsbBorrow _ -> () | AsbProjReborrows (sv, proj_ty) -> - add_aproj_borrows sv abs.abs_id abs.regions proj_ty true + add_aproj_borrows sv abs.abs_id abs.regions.owned proj_ty true method! visit_aproj abs aproj = (let abs = Option.get abs in match aproj with - | AProjLoans (sv, _) -> add_aproj_loans sv abs.abs_id abs.regions + | AProjLoans (sv, _) -> add_aproj_loans sv abs.abs_id abs.regions.owned | AProjBorrows (sv, proj_ty) -> - add_aproj_borrows sv abs.abs_id abs.regions proj_ty false + add_aproj_borrows sv abs.abs_id abs.regions.owned proj_ty false | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj abs aproj end diff --git a/src/llbc/Print.ml b/src/llbc/Print.ml index 2a60b193..657b4d2f 100644 --- a/src/llbc/Print.ml +++ b/src/llbc/Print.ml @@ -314,7 +314,7 @@ module Values = struct ^ kind ^ "{parents=" ^ AbstractionId.Set.to_string None abs.parents ^ "}" ^ "{regions=" - ^ RegionId.Set.to_string None abs.regions + ^ RegionId.Set.to_string None abs.regions.owned ^ "}" ^ can_end ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" let inst_fun_sig_to_string (env : fmt_env) (sg : LlbcAst.inst_fun_sig) : diff --git a/src/llbc/Substitute.ml b/src/llbc/Substitute.ml index 80b54055..96bb79d8 100644 --- a/src/llbc/Substitute.ml +++ b/src/llbc/Substitute.ml @@ -99,8 +99,11 @@ let subst_ids_visitor (subst : id_subst) = "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_abs_regions _ regions = + let { owned; ancestors } = regions in + let owned = RegionId.Set.map subst.r_subst owned in + let ancestors = RegionId.Set.map subst.r_subst ancestors in + { owned; ancestors } method! visit_RVar _ var = match var with diff --git a/src/llbc/Values.ml b/src/llbc/Values.ml index 0fc6e50b..e94545d7 100644 --- a/src/llbc/Values.ml +++ b/src/llbc/Values.ml @@ -831,15 +831,19 @@ type abs = { when generating the backward function for 'a, we have to make sure we don't need to end the return region for 'b (if it is the case, it means the function doesn't borrow check). - *) + *) parents : abstraction_id_set; (** The parent abstractions *) original_parents : abstraction_id list; (** The original list of parents, ordered. This is used for synthesis. TODO: remove? *) - regions : region_id_set; (** Regions owned by this abstraction *) - ancestors_regions : region_id_set; + regions : abs_regions; + avalues : typed_avalue list; (** The values in this abstraction *) +} + +and abs_regions = { + owned : region_id_set; (** Regions owned by the abstraction *) + ancestors : region_id_set; (** Union of the regions owned by this abstraction's ancestors (not including the regions of this abstraction itself) *) - avalues : typed_avalue list; (** The values in this abstraction *) } [@@deriving show,