From 506e9dc3f8f2759769c3293e9cbeba5d6fe79a31 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 27 May 2024 16:03:36 +0200 Subject: Add markers everywhere, do not use them yet --- compiler/InterpreterLoopsJoinCtxs.ml | 33 ++++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 11 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index c67869ac..7ea442db 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -39,13 +39,13 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) *) let get_borrow_id (av : typed_avalue) : BorrowId.id = match av.value with - | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid + | ABorrow (AMutBorrow (_, bid, _) | ASharedBorrow (_, bid)) -> bid | _ -> craise __FILE__ __LINE__ span "Unexpected" in let get_loan_id (av : typed_avalue) : BorrowId.id = match av.value with - | ALoan (AMutLoan (lid, _)) -> lid - | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids + | ALoan (AMutLoan (_, lid, _)) -> lid + | ALoan (ASharedLoan (_, lids, _, _)) -> BorrowId.Set.min_elt lids | _ -> craise __FILE__ __LINE__ span "Unexpected" in (* We use ordered maps to reorder the borrows and loans *) @@ -314,11 +314,14 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) Note that the join matcher doesn't implement match functions for avalues (see the comments in {!MakeJoinMatcher}. *) - let merge_amut_borrows id ty0 child0 _ty1 child1 = + let merge_amut_borrows id ty0 pm0 child0 _ty1 pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + (* We need to pick a type for the avalue. The types on the left and on the right may use different regions: it doesn't really matter (here, we pick the one from the left), because we will merge those regions together @@ -326,11 +329,11 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) *) let ty = ty0 in let child = child0 in - let value = ABorrow (AMutBorrow (id, child)) in + let value = ABorrow (AMutBorrow (PNone, id, child)) in { value; ty } in - let merge_ashared_borrows id ty0 ty1 = + let merge_ashared_borrows id ty0 pm0 ty1 pm1 = (* Sanity checks *) let _ = let _, ty0, _ = ty_as_ref ty0 in @@ -343,23 +346,28 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) span in + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + (* Same remarks as for [merge_amut_borrows] *) let ty = ty0 in - let value = ABorrow (ASharedBorrow id) in + let value = ABorrow (ASharedBorrow (PNone, id)) in { value; ty } in - let merge_amut_loans id ty0 child0 _ty1 child1 = + let merge_amut_loans id ty0 pm0 child0 _ty1 pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; (* Same remarks as for [merge_amut_borrows] *) let ty = ty0 in let child = child0 in - let value = ALoan (AMutLoan (id, child)) in + let value = ALoan (AMutLoan (PNone, id, child)) in { value; ty } in - let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1 + let merge_ashared_loans ids ty0 pm0 (sv0 : typed_value) child0 _ty1 pm1 (sv1 : typed_value) child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; @@ -375,10 +383,13 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv1.value)) span; + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + let ty = ty0 in let child = child0 in let sv = M.match_typed_values ctx ctx sv0 sv1 in - let value = ALoan (ASharedLoan (ids, sv, child)) in + let value = ALoan (ASharedLoan (PNone, ids, sv, child)) in { value; ty } in { -- cgit v1.2.3 From c236ccfb22e64f56f4398d067582ebd570bf1a0b Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 27 May 2024 16:44:28 +0200 Subject: Add projection markers when joining environments --- compiler/InterpreterLoopsJoinCtxs.ml | 59 ++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 7ea442db..0f61f619 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -467,6 +467,65 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) (* This should have been eliminated *) craise __FILE__ __LINE__ span "Unreachable" in + + (* Add a projection marker to a typed avalue *) + let add_marker_avalue (pm : proj_marker) (av : typed_avalue) : typed_avalue + = + let obj = + object + inherit [_] map_typed_avalue as super + + method! visit_borrow_content _ _ = + craise __FILE__ __LINE__ span "Unexpected borrow" + + method! visit_loan_content _ _ = + craise __FILE__ __LINE__ span "Unexpected loan" + + method! visit_symbolic_value _ sv = + (* While ctx0 and ctx1 are different, we assume that the type info context is + the same in both. Hence, we can use ctx0's types wlog *) + sanity_check __FILE__ __LINE__ + (not (symbolic_value_has_borrows ctx0 sv)) + span; + sv + + method! visit_aloan_content env lc = + match lc with + | AMutLoan (pm0, bid, av) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aloan_content env (AMutLoan (pm, bid, av)) + | ASharedLoan (pm0, bids, av, child) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aloan_content env + (ASharedLoan (pm, bids, av, child)) + | _ -> craise __FILE__ __LINE__ span "Unsupported yet" + + method! visit_aborrow_content env bc = + match bc with + | AMutBorrow (pm0, bid, av) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aborrow_content env (AMutBorrow (pm, bid, av)) + | ASharedBorrow (pm0, bid) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aborrow_content env (ASharedBorrow (pm, bid)) + | _ -> craise __FILE__ __LINE__ span "Unsupported yet" + end + in + obj#visit_typed_avalue () av + in + + (* Add projection marker to all abstractions in the left and right environments *) + let add_marker (pm : proj_marker) (ee : env_elem) : env_elem = + match ee with + | EAbs abs -> + EAbs + { abs with avalues = List.map (add_marker_avalue pm) abs.avalues } + | x -> x + in + + let env0 = List.map (add_marker PLeft) env0 in + let env1 = List.map (add_marker PRight) env1 in + List.iter check_valid env0; List.iter check_valid env1; (* Concatenate the suffixes and append the abstractions introduced while -- cgit v1.2.3 From 309435d24edb689736da83025eb08a6761b28b8b Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 27 May 2024 17:51:50 +0200 Subject: Split collapse into collapse and reduce, rename accordingly --- compiler/InterpreterLoopsJoinCtxs.ml | 193 +++++++++++++++++++++++++++++++++-- 1 file changed, 182 insertions(+), 11 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 0f61f619..960edb99 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -17,7 +17,7 @@ let log = Logging.loops_join_ctxs_log We do this in order to enforce some structure in the environments: this allows us to find fixed-points. Note that this function needs to be called typically after we merge abstractions together (see {!collapse_ctx} - for instance). + and {!reduce_ctx} for instance). *) let reorder_loans_borrows_in_fresh_abs (span : Meta.span) (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = @@ -70,7 +70,7 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) { ctx with env } -(** Collapse an environment. +(** Reduce an environment. We do this to simplify an environment, for the purpose of finding a loop fixed point. @@ -129,6 +129,171 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) This can happen when merging environments (note that such environments are not well-formed - they become well formed again after collapsing). *) +let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) + (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) + (ctx0 : eval_ctx) : eval_ctx = + (* Debug *) + log#ldebug + (lazy + ("reduce_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids ^ "\n\n- ctx0:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx0 + ^ "\n\n")); + + let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in + let can_end = true in + let destructure_shared_values = true in + let is_fresh_abs_id (id : AbstractionId.id) : bool = + not (AbstractionId.Set.mem id old_ids.aids) + in + let is_fresh_did (id : DummyVarId.id) : bool = + not (DummyVarId.Set.mem id old_ids.dids) + in + (* Convert the dummy values to abstractions (note that when we convert + values to abstractions, the resulting abstraction should be destructured) *) + (* Note that we preserve the order of the dummy values: we replace them with + abstractions in place - this makes matching easier *) + let env = + List.concat + (List.map + (fun ee -> + match ee with + | EAbs _ | EFrame | EBinding (BVar _, _) -> [ ee ] + | EBinding (BDummy id, v) -> + if is_fresh_did id then + let absl = + convert_value_to_abstractions span abs_kind can_end + destructure_shared_values ctx0 v + in + List.map (fun abs -> EAbs abs) absl + else [ ee ]) + ctx0.env) + in + let ctx = { ctx0 with env } in + log#ldebug + (lazy + ("reduce_ctx: after converting values to abstractions:\n" + ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n")); + + log#ldebug + (lazy + ("reduce_ctx: after decomposing the shared values in the abstractions:\n" + ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n")); + + (* Explore all the *new* abstractions, and compute various maps *) + let explore (abs : abs) = is_fresh_abs_id abs.abs_id in + let ids_maps = + compute_abs_borrows_loans_maps span (merge_funs = None) explore env + in + let { + abs_ids; + abs_to_borrows; + abs_to_loans = _; + abs_to_borrows_loans; + borrow_to_abs = _; + loan_to_abs; + borrow_loan_to_abs; + } = + ids_maps + in + + (* Change the merging behaviour depending on the input parameters *) + let abs_to_borrows, loan_to_abs = + if merge_funs <> None then (abs_to_borrows_loans, borrow_loan_to_abs) + else (abs_to_borrows, loan_to_abs) + in + + (* Merge the abstractions together *) + let merged_abs : AbstractionId.id UnionFind.elem AbstractionId.Map.t = + AbstractionId.Map.of_list + (List.map (fun id -> (id, UnionFind.make id)) abs_ids) + in + + let ctx = ref ctx in + + (* Merge all the mergeable abs. + + We iterate over the abstractions, then over the borrows in the abstractions. + We do this because we want to control the order in which abstractions + are merged (the ids are iterated in increasing order). Otherwise, we + could simply iterate over all the borrows in [borrow_to_abs]... + *) + List.iter + (fun abs_id0 -> + let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in + let bids = BorrowId.Set.elements bids in + List.iter + (fun bid -> + match BorrowId.Map.find_opt bid loan_to_abs with + | None -> (* Nothing to do *) () + | Some abs_ids1 -> + AbstractionId.Set.iter + (fun abs_id1 -> + (* We need to merge - unless we have already merged *) + (* First, find the representatives for the two abstractions (the + representative is the abstraction into which we merged) *) + let abs_ref0 = + UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) + in + let abs_id0 = UnionFind.get abs_ref0 in + let abs_ref1 = + UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) + in + let abs_id1 = UnionFind.get abs_ref1 in + (* If the two ids are the same, it means the abstractions were already merged *) + if abs_id0 = abs_id1 then () + else ( + (* We actually need to merge the abstractions *) + + (* Debug *) + log#ldebug + (lazy + ("reduce_ctx: merging abstraction " + ^ AbstractionId.to_string abs_id1 + ^ " into " + ^ AbstractionId.to_string abs_id0 + ^ ":\n\n" + ^ eval_ctx_to_string ~span:(Some span) !ctx)); + + (* Update the environment - pay attention to the order: we + we merge [abs_id1] *into* [abs_id0] *) + let nctx, abs_id = + merge_into_abstraction span abs_kind can_end merge_funs + !ctx abs_id1 abs_id0 + in + ctx := nctx; + + (* Update the union find *) + let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in + UnionFind.set abs_ref_merged abs_id)) + abs_ids1) + bids) + abs_ids; + + log#ldebug + (lazy + ("reduce_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- after reduce:\n" + ^ eval_ctx_to_string ~span:(Some span) !ctx + ^ "\n\n")); + + (* Reorder the loans and borrows in the fresh abstractions *) + let ctx = reorder_loans_borrows_in_fresh_abs span old_ids.aids !ctx in + + log#ldebug + (lazy + ("reduce_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- after reduce and reorder borrows/loans:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n")); + + (* Return the new context *) + ctx + +(* TODO Adapt and comment *) let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = @@ -523,9 +688,10 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) | x -> x in - let env0 = List.map (add_marker PLeft) env0 in - let env1 = List.map (add_marker PRight) env1 in - + (* TODO: Readd this + let env0 = List.map (add_marker PLeft) env0 in + let env1 = List.map (add_marker PRight) env1 in + *) List.iter check_valid env0; List.iter check_valid env1; (* Concatenate the suffixes and append the abstractions introduced while @@ -776,11 +942,11 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span) ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); - (* Collapse the context we want to add to the join *) - let ctx = collapse_ctx span loop_id None fixed_ids ctx in + (* Reduce the context we want to add to the join *) + let ctx = reduce_ctx span loop_id None fixed_ids ctx in log#ldebug (lazy - ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n" + ("loop_join_origin_with_continue_ctxs:join_one: after reduce:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Refresh the fresh abstractions *) @@ -793,15 +959,20 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span) ("loop_join_origin_with_continue_ctxs:join_one: after join:\n" ^ eval_ctx_to_string ~span:(Some span) ctx1)); - (* Collapse again - the join might have introduce abstractions we want - to merge with the others (note that those abstractions may actually - lead to borrows/loans duplications) *) + (* Collapse to eliminate the markers *) joined_ctx := collapse_ctx_with_merge span loop_id fixed_ids !joined_ctx; log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n" ^ eval_ctx_to_string ~span:(Some span) !joined_ctx)); + (* Reduce again to reach fixed point *) + joined_ctx := reduce_ctx span loop_id None fixed_ids !joined_ctx; + log#ldebug + (lazy + ("loop_join_origin_with_continue_ctxs:join_one: after last reduce:\n" + ^ eval_ctx_to_string ~span:(Some span) !joined_ctx)); + (* Sanity check *) if !Config.sanity_checks then Invariants.check_invariants span !joined_ctx; (* Return *) -- cgit v1.2.3 From 3c1e6d37a2b40b880b04b2d2aac95d6f06822327 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 27 May 2024 17:56:10 +0200 Subject: Simplify reduce_ctx --- compiler/InterpreterLoopsJoinCtxs.ml | 27 ++++++--------------------- 1 file changed, 6 insertions(+), 21 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 960edb99..5b9022b2 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -122,15 +122,8 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) i -> s@7 : u32 abs@4 { MB l0, ML l4 } ]} - - [merge_funs]: those are used to merge loans or borrows which appear in both - abstractions (rem.: here we mean that, for instance, both abstractions - contain a shared loan with id l0). - This can happen when merging environments (note that such environments are not well-formed - - they become well formed again after collapsing). *) -let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) - (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) +let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = (* Debug *) log#ldebug @@ -185,9 +178,7 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (* Explore all the *new* abstractions, and compute various maps *) let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = - compute_abs_borrows_loans_maps span (merge_funs = None) explore env - in + let ids_maps = compute_abs_borrows_loans_maps span true explore env in let { abs_ids; abs_to_borrows; @@ -200,12 +191,6 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) ids_maps in - (* Change the merging behaviour depending on the input parameters *) - let abs_to_borrows, loan_to_abs = - if merge_funs <> None then (abs_to_borrows_loans, borrow_loan_to_abs) - else (abs_to_borrows, loan_to_abs) - in - (* Merge the abstractions together *) let merged_abs : AbstractionId.id UnionFind.elem AbstractionId.Map.t = AbstractionId.Map.of_list @@ -261,8 +246,8 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (* Update the environment - pay attention to the order: we we merge [abs_id1] *into* [abs_id0] *) let nctx, abs_id = - merge_into_abstraction span abs_kind can_end merge_funs - !ctx abs_id1 abs_id0 + merge_into_abstraction span abs_kind can_end None !ctx + abs_id1 abs_id0 in ctx := nctx; @@ -943,7 +928,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span) ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Reduce the context we want to add to the join *) - let ctx = reduce_ctx span loop_id None fixed_ids ctx in + let ctx = reduce_ctx span loop_id fixed_ids ctx in log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after reduce:\n" @@ -967,7 +952,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span) ^ eval_ctx_to_string ~span:(Some span) !joined_ctx)); (* Reduce again to reach fixed point *) - joined_ctx := reduce_ctx span loop_id None fixed_ids !joined_ctx; + joined_ctx := reduce_ctx span loop_id fixed_ids !joined_ctx; log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after last reduce:\n" -- cgit v1.2.3 From 4b14d42b2c2eff3104f0bc342f0bc5ff7cecd5e9 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 27 May 2024 17:57:50 +0200 Subject: Simplify collapse_ctx --- compiler/InterpreterLoopsJoinCtxs.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 5b9022b2..81e5004f 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -280,7 +280,7 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (* TODO Adapt and comment *) let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) - (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) + (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = (* Debug *) log#ldebug @@ -337,7 +337,7 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Explore all the *new* abstractions, and compute various maps *) let explore (abs : abs) = is_fresh_abs_id abs.abs_id in let ids_maps = - compute_abs_borrows_loans_maps span (merge_funs = None) explore env + compute_abs_borrows_loans_maps span false explore env in let { abs_ids; @@ -353,8 +353,7 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Change the merging behaviour depending on the input parameters *) let abs_to_borrows, loan_to_abs = - if merge_funs <> None then (abs_to_borrows_loans, borrow_loan_to_abs) - else (abs_to_borrows, loan_to_abs) + (abs_to_borrows_loans, borrow_loan_to_abs) in (* Merge the abstractions together *) @@ -412,7 +411,7 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Update the environment - pay attention to the order: we we merge [abs_id1] *into* [abs_id0] *) let nctx, abs_id = - merge_into_abstraction span abs_kind can_end merge_funs + merge_into_abstraction span abs_kind can_end (Some merge_funs) !ctx abs_id1 abs_id0 in ctx := nctx; @@ -566,7 +565,7 @@ let merge_into_abstraction (span : Meta.span) (loop_id : LoopId.id) let collapse_ctx_with_merge (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = let merge_funs = mk_collapse_ctx_merge_duplicate_funs span loop_id ctx in - try collapse_ctx span loop_id (Some merge_funs) old_ids ctx + try collapse_ctx span loop_id merge_funs old_ids ctx with ValueMatchFailure _ -> craise __FILE__ __LINE__ span "Unexpected" let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) -- cgit v1.2.3 From 445c566f11dcc9ba8c69a154902a12a18ba3a2aa Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 28 May 2024 14:28:40 +0200 Subject: Add type and set/map for marker and borrow id --- compiler/InterpreterLoopsJoinCtxs.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 81e5004f..5c3ce66d 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -280,8 +280,8 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (* TODO Adapt and comment *) let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) - (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) - (ctx0 : eval_ctx) : eval_ctx = + (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) + : eval_ctx = (* Debug *) log#ldebug (lazy @@ -336,9 +336,7 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Explore all the *new* abstractions, and compute various maps *) let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = - compute_abs_borrows_loans_maps span false explore env - in + let ids_maps = compute_abs_borrows_loans_maps span false explore env in let { abs_ids; abs_to_borrows; @@ -353,7 +351,7 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Change the merging behaviour depending on the input parameters *) let abs_to_borrows, loan_to_abs = - (abs_to_borrows_loans, borrow_loan_to_abs) + (abs_to_borrows_loans, borrow_loan_to_abs) in (* Merge the abstractions together *) @@ -411,8 +409,8 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Update the environment - pay attention to the order: we we merge [abs_id1] *into* [abs_id0] *) let nctx, abs_id = - merge_into_abstraction span abs_kind can_end (Some merge_funs) - !ctx abs_id1 abs_id0 + merge_into_abstraction span abs_kind can_end + (Some merge_funs) !ctx abs_id1 abs_id0 in ctx := nctx; -- cgit v1.2.3 From 96d803a7aefe27d4401a336c426161d387987b63 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 28 May 2024 14:51:25 +0200 Subject: Compute marker information for borrow/loan maps --- compiler/InterpreterLoopsJoinCtxs.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 5c3ce66d..7f80e496 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -209,10 +209,10 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) List.iter (fun abs_id0 -> let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in - let bids = BorrowId.Set.elements bids in + let bids = MarkerBorrowId.Set.elements bids in List.iter (fun bid -> - match BorrowId.Map.find_opt bid loan_to_abs with + match MarkerBorrowId.Map.find_opt bid loan_to_abs with | None -> (* Nothing to do *) () | Some abs_ids1 -> AbstractionId.Set.iter @@ -372,10 +372,10 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) List.iter (fun abs_id0 -> let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in - let bids = BorrowId.Set.elements bids in + let bids = MarkerBorrowId.Set.elements bids in List.iter (fun bid -> - match BorrowId.Map.find_opt bid loan_to_abs with + match MarkerBorrowId.Map.find_opt bid loan_to_abs with | None -> (* Nothing to do *) () | Some abs_ids1 -> AbstractionId.Set.iter -- cgit v1.2.3 From ce8614be6bd96c51756bf5922b5dfd4c59650dd4 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 30 May 2024 12:33:05 +0200 Subject: Implement two phases of loops join + collapse --- compiler/InterpreterLoopsJoinCtxs.ml | 346 ++++++++++++++++++++--------------- 1 file changed, 197 insertions(+), 149 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 7f80e496..1e099d96 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -122,8 +122,13 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) i -> s@7 : u32 abs@4 { MB l0, ML l4 } ]} + + If [merge_funs] is None, we ensure that there are no markers in the environments. + If [merge_funs] is Some _, we merge environments that contain borrow/loan pairs with the same markers, omitting + pairs with the PNone marker (i.e., no marker) *) -let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) +let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) + (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = (* Debug *) log#ldebug @@ -132,6 +137,8 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) ^ eval_ctx_to_string ~span:(Some span) ctx0 ^ "\n\n")); + let allow_markers = merge_funs <> None in + let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in let destructure_shared_values = true in @@ -212,49 +219,53 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) let bids = MarkerBorrowId.Set.elements bids in List.iter (fun bid -> + if not allow_markers then + sanity_check __FILE__ __LINE__ (fst bid = PNone) span; match MarkerBorrowId.Map.find_opt bid loan_to_abs with | None -> (* Nothing to do *) () | Some abs_ids1 -> - AbstractionId.Set.iter - (fun abs_id1 -> - (* We need to merge - unless we have already merged *) - (* First, find the representatives for the two abstractions (the - representative is the abstraction into which we merged) *) - let abs_ref0 = - UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) - in - let abs_id0 = UnionFind.get abs_ref0 in - let abs_ref1 = - UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) - in - let abs_id1 = UnionFind.get abs_ref1 in - (* If the two ids are the same, it means the abstractions were already merged *) - if abs_id0 = abs_id1 then () - else ( - (* We actually need to merge the abstractions *) - - (* Debug *) - log#ldebug - (lazy - ("reduce_ctx: merging abstraction " - ^ AbstractionId.to_string abs_id1 - ^ " into " - ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx)); - - (* Update the environment - pay attention to the order: we - we merge [abs_id1] *into* [abs_id0] *) - let nctx, abs_id = - merge_into_abstraction span abs_kind can_end None !ctx - abs_id1 abs_id0 + if allow_markers && fst bid = PNone then () + else + AbstractionId.Set.iter + (fun abs_id1 -> + (* We need to merge - unless we have already merged *) + (* First, find the representatives for the two abstractions (the + representative is the abstraction into which we merged) *) + let abs_ref0 = + UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) in - ctx := nctx; - - (* Update the union find *) - let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in - UnionFind.set abs_ref_merged abs_id)) - abs_ids1) + let abs_id0 = UnionFind.get abs_ref0 in + let abs_ref1 = + UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) + in + let abs_id1 = UnionFind.get abs_ref1 in + (* If the two ids are the same, it means the abstractions were already merged *) + if abs_id0 = abs_id1 then () + else ( + (* We actually need to merge the abstractions *) + + (* Debug *) + log#ldebug + (lazy + ("reduce_ctx: merging abstraction " + ^ AbstractionId.to_string abs_id1 + ^ " into " + ^ AbstractionId.to_string abs_id0 + ^ ":\n\n" + ^ eval_ctx_to_string ~span:(Some span) !ctx)); + + (* Update the environment - pay attention to the order: we + we merge [abs_id1] *into* [abs_id0] *) + let nctx, abs_id = + merge_into_abstraction span abs_kind can_end merge_funs + !ctx abs_id1 abs_id0 + in + ctx := nctx; + + (* Update the union find *) + let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in + UnionFind.set abs_ref_merged abs_id)) + abs_ids1) bids) abs_ids; @@ -278,8 +289,11 @@ let reduce_ctx (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (* Return the new context *) ctx +(* Reduce_ctx can only be called in a context with no markers *) +let reduce_ctx = reduce_ctx_with_markers None + (* TODO Adapt and comment *) -let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) +let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = (* Debug *) @@ -296,128 +310,153 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) let is_fresh_abs_id (id : AbstractionId.id) : bool = not (AbstractionId.Set.mem id old_ids.aids) in - let is_fresh_did (id : DummyVarId.id) : bool = - not (DummyVarId.Set.mem id old_ids.dids) - in - (* Convert the dummy values to abstractions (note that when we convert - values to abstractions, the resulting abstraction should be destructured) *) - (* Note that we preserve the order of the dummy values: we replace them with - abstractions in place - this makes matching easier *) - let env = - List.concat - (List.map - (fun ee -> - match ee with - | EAbs _ | EFrame | EBinding (BVar _, _) -> [ ee ] - | EBinding (BDummy id, v) -> - if is_fresh_did id then - let absl = - convert_value_to_abstractions span abs_kind can_end - destructure_shared_values ctx0 v - in - List.map (fun abs -> EAbs abs) absl - else [ ee ]) - ctx0.env) - in - let ctx = { ctx0 with env } in - log#ldebug - (lazy - ("collapse_ctx: after converting values to abstractions:\n" - ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" - ^ eval_ctx_to_string ~span:(Some span) ctx - ^ "\n\n")); - - log#ldebug - (lazy - ("collapse_ctx: after decomposing the shared values in the abstractions:\n" - ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" - ^ eval_ctx_to_string ~span:(Some span) ctx - ^ "\n\n")); (* Explore all the *new* abstractions, and compute various maps *) let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = compute_abs_borrows_loans_maps span false explore env in + let ids_maps = compute_abs_borrows_loans_maps span false explore ctx0.env in let { abs_ids; abs_to_borrows; - abs_to_loans = _; + abs_to_loans; abs_to_borrows_loans; - borrow_to_abs = _; + borrow_to_abs; loan_to_abs; borrow_loan_to_abs; } = ids_maps in - (* Change the merging behaviour depending on the input parameters *) - let abs_to_borrows, loan_to_abs = - (abs_to_borrows_loans, borrow_loan_to_abs) - in - (* Merge the abstractions together *) let merged_abs : AbstractionId.id UnionFind.elem AbstractionId.Map.t = AbstractionId.Map.of_list (List.map (fun id -> (id, UnionFind.make id)) abs_ids) in - let ctx = ref ctx in + let ctx = ref ctx0 in - (* Merge all the mergeable abs. + let invert_proj_marker = function + | PNone -> craise __FILE__ __LINE__ span "Unreachable" + | PLeft -> PRight + | PRight -> PLeft + in - We iterate over the abstractions, then over the borrows in the abstractions. - We do this because we want to control the order in which abstractions - are merged (the ids are iterated in increasing order). Otherwise, we - could simply iterate over all the borrows in [borrow_to_abs]... + (* Merge all the mergeable abs where the same element in present in both abs, + but with left and right markers respectively. + + We first check all borrows, then all loans *) List.iter (fun abs_id0 -> let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in let bids = MarkerBorrowId.Set.elements bids in List.iter - (fun bid -> - match MarkerBorrowId.Map.find_opt bid loan_to_abs with - | None -> (* Nothing to do *) () - | Some abs_ids1 -> - AbstractionId.Set.iter - (fun abs_id1 -> - (* We need to merge - unless we have already merged *) - (* First, find the representatives for the two abstractions (the - representative is the abstraction into which we merged) *) - let abs_ref0 = - UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) - in - let abs_id0 = UnionFind.get abs_ref0 in - let abs_ref1 = - UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) - in - let abs_id1 = UnionFind.get abs_ref1 in - (* If the two ids are the same, it means the abstractions were already merged *) - if abs_id0 = abs_id1 then () - else ( - (* We actually need to merge the abstractions *) - - (* Debug *) - log#ldebug - (lazy - ("collapse_ctx: merging abstraction " - ^ AbstractionId.to_string abs_id1 - ^ " into " - ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx)); - - (* Update the environment - pay attention to the order: we - we merge [abs_id1] *into* [abs_id0] *) - let nctx, abs_id = - merge_into_abstraction span abs_kind can_end - (Some merge_funs) !ctx abs_id1 abs_id0 + (fun (pm, bid) -> + if pm = PNone then () + else + (* We are looking for an element with the same borrow_id, but with the dual marker *) + match + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + borrow_to_abs + with + | None -> (* Nothing to do *) () + | Some abs_ids1 -> + AbstractionId.Set.iter + (fun abs_id1 -> + (* We need to merge - unless we have already merged *) + (* First, find the representatives for the two abstractions (the + representative is the abstraction into which we merged) *) + let abs_ref0 = + UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) in - ctx := nctx; - - (* Update the union find *) - let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in - UnionFind.set abs_ref_merged abs_id)) - abs_ids1) + let abs_id0 = UnionFind.get abs_ref0 in + let abs_ref1 = + UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) + in + let abs_id1 = UnionFind.get abs_ref1 in + (* If the two ids are the same, it means the abstractions were already merged *) + if abs_id0 = abs_id1 then () + else ( + (* We actually need to merge the abstractions *) + + (* Debug *) + log#ldebug + (lazy + ("collapse_ctx: merging abstraction " + ^ AbstractionId.to_string abs_id1 + ^ " into " + ^ AbstractionId.to_string abs_id0 + ^ ":\n\n" + ^ eval_ctx_to_string ~span:(Some span) !ctx)); + + (* Update the environment - pay attention to the order: we + we merge [abs_id1] *into* [abs_id0] *) + let nctx, abs_id = + merge_into_abstraction span abs_kind can_end + (Some merge_funs) !ctx abs_id1 abs_id0 + in + ctx := nctx; + + (* Update the union find *) + let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in + UnionFind.set abs_ref_merged abs_id)) + abs_ids1) + bids; + (* We now traverse the loans *) + let bids = AbstractionId.Map.find abs_id0 abs_to_loans in + let bids = MarkerBorrowId.Set.elements bids in + List.iter + (fun (pm, bid) -> + if pm = PNone then () + else + (* We are looking for an element with the same borrow_id, but with the dual marker *) + match + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + loan_to_abs + with + | None -> (* Nothing to do *) () + | Some abs_ids1 -> + AbstractionId.Set.iter + (fun abs_id1 -> + (* We need to merge - unless we have already merged *) + (* First, find the representatives for the two abstractions (the + representative is the abstraction into which we merged) *) + let abs_ref0 = + UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) + in + let abs_id0 = UnionFind.get abs_ref0 in + let abs_ref1 = + UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) + in + let abs_id1 = UnionFind.get abs_ref1 in + (* If the two ids are the same, it means the abstractions were already merged *) + if abs_id0 = abs_id1 then () + else ( + (* We actually need to merge the abstractions *) + + (* Debug *) + log#ldebug + (lazy + ("collapse_ctx: merging abstraction " + ^ AbstractionId.to_string abs_id1 + ^ " into " + ^ AbstractionId.to_string abs_id0 + ^ ":\n\n" + ^ eval_ctx_to_string ~span:(Some span) !ctx)); + + (* Update the environment - pay attention to the order: we + we merge [abs_id1] *into* [abs_id0] *) + let nctx, abs_id = + merge_into_abstraction span abs_kind can_end + (Some merge_funs) !ctx abs_id1 abs_id0 + in + ctx := nctx; + + (* Update the union find *) + let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in + UnionFind.set abs_ref_merged abs_id)) + abs_ids1) bids) abs_ids; @@ -441,6 +480,25 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Return the new context *) ctx +(* Collapse two environments containing projection markers; this function is called after + joining environments. + + The collapse is done in two steps. + First, we reduce the environment, merging for instance abstractions containing MB l0 _ and ML l0, + when both elements have the same marker, e.g., PNone, PLeft, or PRight. + + Second, we merge abstractions containing the same element with left and right markers respectively. + + At the end of the second step, all markers should have been removed from the resulting environment. +*) +let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) + (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) + : eval_ctx = + let ctx = + reduce_ctx_with_markers (Some merge_funs) span loop_id old_ids ctx0 + in + collapse_ctx_markers span loop_id merge_funs old_ids ctx + let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) (loop_id : LoopId.id) (ctx : eval_ctx) : merge_duplicates_funcs = (* Rem.: the merge functions raise exceptions (that we catch). *) @@ -466,9 +524,6 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; - (* TODO: Handle markers *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; - (* We need to pick a type for the avalue. The types on the left and on the right may use different regions: it doesn't really matter (here, we pick the one from the left), because we will merge those regions together @@ -493,9 +548,6 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) span in - (* TODO: Handle markers *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; - (* Same remarks as for [merge_amut_borrows] *) let ty = ty0 in let value = ABorrow (ASharedBorrow (PNone, id)) in @@ -506,8 +558,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; - (* TODO: Handle markers *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + (* Same remarks as for [merge_amut_borrows] *) let ty = ty0 in let child = child0 in @@ -530,8 +581,6 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv1.value)) span; - (* TODO: Handle markers *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; let ty = ty0 in let child = child0 in @@ -670,10 +719,9 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) | x -> x in - (* TODO: Readd this - let env0 = List.map (add_marker PLeft) env0 in - let env1 = List.map (add_marker PRight) env1 in - *) + let env0 = List.map (add_marker PLeft) env0 in + let env1 = List.map (add_marker PRight) env1 in + List.iter check_valid env0; List.iter check_valid env1; (* Concatenate the suffixes and append the abstractions introduced while -- cgit v1.2.3 From 52bcaf0cdd1c08ece0f9f09bdc0d32b753a2a00f Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 31 May 2024 11:55:51 +0200 Subject: Add markers when creating new abstractions because of a join with bottom --- compiler/InterpreterLoopsJoinCtxs.ml | 51 +++--------------------------------- 1 file changed, 4 insertions(+), 47 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 1e099d96..2f2dba41 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -664,58 +664,15 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) craise __FILE__ __LINE__ span "Unreachable" in - (* Add a projection marker to a typed avalue *) - let add_marker_avalue (pm : proj_marker) (av : typed_avalue) : typed_avalue - = - let obj = - object - inherit [_] map_typed_avalue as super - - method! visit_borrow_content _ _ = - craise __FILE__ __LINE__ span "Unexpected borrow" - - method! visit_loan_content _ _ = - craise __FILE__ __LINE__ span "Unexpected loan" - - method! visit_symbolic_value _ sv = - (* While ctx0 and ctx1 are different, we assume that the type info context is - the same in both. Hence, we can use ctx0's types wlog *) - sanity_check __FILE__ __LINE__ - (not (symbolic_value_has_borrows ctx0 sv)) - span; - sv - - method! visit_aloan_content env lc = - match lc with - | AMutLoan (pm0, bid, av) -> - sanity_check __FILE__ __LINE__ (pm0 = PNone) span; - super#visit_aloan_content env (AMutLoan (pm, bid, av)) - | ASharedLoan (pm0, bids, av, child) -> - sanity_check __FILE__ __LINE__ (pm0 = PNone) span; - super#visit_aloan_content env - (ASharedLoan (pm, bids, av, child)) - | _ -> craise __FILE__ __LINE__ span "Unsupported yet" - - method! visit_aborrow_content env bc = - match bc with - | AMutBorrow (pm0, bid, av) -> - sanity_check __FILE__ __LINE__ (pm0 = PNone) span; - super#visit_aborrow_content env (AMutBorrow (pm, bid, av)) - | ASharedBorrow (pm0, bid) -> - sanity_check __FILE__ __LINE__ (pm0 = PNone) span; - super#visit_aborrow_content env (ASharedBorrow (pm, bid)) - | _ -> craise __FILE__ __LINE__ span "Unsupported yet" - end - in - obj#visit_typed_avalue () av - in - (* Add projection marker to all abstractions in the left and right environments *) let add_marker (pm : proj_marker) (ee : env_elem) : env_elem = match ee with | EAbs abs -> EAbs - { abs with avalues = List.map (add_marker_avalue pm) abs.avalues } + { + abs with + avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues; + } | x -> x in -- cgit v1.2.3 From e2afa2a24b290a55451431373152bf5a26c78d24 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 31 May 2024 13:48:44 +0200 Subject: Fix unused variables warnings --- compiler/InterpreterLoopsJoinCtxs.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 2f2dba41..4b5cfb82 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -190,10 +190,10 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) abs_ids; abs_to_borrows; abs_to_loans = _; - abs_to_borrows_loans; + abs_to_borrows_loans = _; borrow_to_abs = _; loan_to_abs; - borrow_loan_to_abs; + borrow_loan_to_abs = _; } = ids_maps in @@ -306,7 +306,6 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in - let destructure_shared_values = true in let is_fresh_abs_id (id : AbstractionId.id) : bool = not (AbstractionId.Set.mem id old_ids.aids) in @@ -318,10 +317,10 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) abs_ids; abs_to_borrows; abs_to_loans; - abs_to_borrows_loans; + abs_to_borrows_loans = _; borrow_to_abs; loan_to_abs; - borrow_loan_to_abs; + borrow_loan_to_abs = _; } = ids_maps in @@ -519,7 +518,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) Note that the join matcher doesn't implement match functions for avalues (see the comments in {!MakeJoinMatcher}. *) - let merge_amut_borrows id ty0 pm0 child0 _ty1 pm1 child1 = + let merge_amut_borrows id ty0 _pm0 child0 _ty1 _pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; @@ -535,7 +534,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) { value; ty } in - let merge_ashared_borrows id ty0 pm0 ty1 pm1 = + let merge_ashared_borrows id ty0 _pm0 ty1 _pm1 = (* Sanity checks *) let _ = let _, ty0, _ = ty_as_ref ty0 in @@ -554,7 +553,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) { value; ty } in - let merge_amut_loans id ty0 pm0 child0 _ty1 pm1 child1 = + let merge_amut_loans id ty0 _pm0 child0 _ty1 _pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; @@ -565,7 +564,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) let value = ALoan (AMutLoan (PNone, id, child)) in { value; ty } in - let merge_ashared_loans ids ty0 pm0 (sv0 : typed_value) child0 _ty1 pm1 + let merge_ashared_loans ids ty0 _pm0 (sv0 : typed_value) child0 _ty1 _pm1 (sv1 : typed_value) child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; -- cgit v1.2.3 From 3598da14b7de6452b03e98e701996a8b6d4d5d38 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 31 May 2024 14:46:12 +0200 Subject: Add documentation to collapse --- compiler/InterpreterLoopsJoinCtxs.ml | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 4b5cfb82..930bffac 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -292,7 +292,33 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) (* Reduce_ctx can only be called in a context with no markers *) let reduce_ctx = reduce_ctx_with_markers None -(* TODO Adapt and comment *) +(* Collapse an environment + + This is the second part of a join, where we attempt to simplify and remove all projection markers. + This function is called after reducing the environments, and attempting to simplify all the pairs + of borrows and loans. + + We traverse all abstractions, and merge abstractions when they contain the same element, + but with dual markers (i.e., PLeft and PRight). + + For instance, if we have the abstractions + + abs@0 { | MB l0 _ |, ML l1 } + abs@1 { ︙MB l0 _ ︙, ML l2 } + + we will merge abs@0 and abs@1 into a new abstraction abs@2, removing the marker for duplicated elements, + and taking the join of the remaining elements + + abs@2 { MB l0 _, ML l1, ML l2 } + + Rem.: Doing this might introduce new pairs of borrow/loans to be merged in different abstractions: in the example above, + this could occur if there was another abstraction in the context containing ML l0, which would need to be simplified through + a further reduce. + It is unclear whether this can happen in practice. If so, a solution would be to preprocess the environments when doing + a join: while not in the current formalism, it is sound to split an element with no markers into a duplicated pair of the + same element with left and right markers. Doing this before reduce would allow to reduce all possible pairs of borrow/loans, + before finally collapsing and removing all markers. +*) let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = -- cgit v1.2.3 From f5a7a0ceccfeec0dd8801d5a874cb66c1a356f8f Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 31 May 2024 15:00:23 +0200 Subject: format --- compiler/InterpreterLoopsJoinCtxs.ml | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 930bffac..b58d1b3e 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -294,30 +294,30 @@ let reduce_ctx = reduce_ctx_with_markers None (* Collapse an environment - This is the second part of a join, where we attempt to simplify and remove all projection markers. - This function is called after reducing the environments, and attempting to simplify all the pairs - of borrows and loans. + This is the second part of a join, where we attempt to simplify and remove all projection markers. + This function is called after reducing the environments, and attempting to simplify all the pairs + of borrows and loans. - We traverse all abstractions, and merge abstractions when they contain the same element, - but with dual markers (i.e., PLeft and PRight). + We traverse all abstractions, and merge abstractions when they contain the same element, + but with dual markers (i.e., PLeft and PRight). - For instance, if we have the abstractions + For instance, if we have the abstractions - abs@0 { | MB l0 _ |, ML l1 } - abs@1 { ︙MB l0 _ ︙, ML l2 } + abs@0 { | MB l0 _ |, ML l1 } + abs@1 { ︙MB l0 _ ︙, ML l2 } - we will merge abs@0 and abs@1 into a new abstraction abs@2, removing the marker for duplicated elements, - and taking the join of the remaining elements + we will merge abs@0 and abs@1 into a new abstraction abs@2, removing the marker for duplicated elements, + and taking the join of the remaining elements - abs@2 { MB l0 _, ML l1, ML l2 } + abs@2 { MB l0 _, ML l1, ML l2 } - Rem.: Doing this might introduce new pairs of borrow/loans to be merged in different abstractions: in the example above, - this could occur if there was another abstraction in the context containing ML l0, which would need to be simplified through - a further reduce. - It is unclear whether this can happen in practice. If so, a solution would be to preprocess the environments when doing - a join: while not in the current formalism, it is sound to split an element with no markers into a duplicated pair of the - same element with left and right markers. Doing this before reduce would allow to reduce all possible pairs of borrow/loans, - before finally collapsing and removing all markers. + Rem.: Doing this might introduce new pairs of borrow/loans to be merged in different abstractions: in the example above, + this could occur if there was another abstraction in the context containing ML l0, which would need to be simplified through + a further reduce. + It is unclear whether this can happen in practice. If so, a solution would be to preprocess the environments when doing + a join: while not in the current formalism, it is sound to split an element with no markers into a duplicated pair of the + same element with left and right markers. Doing this before reduce would allow to reduce all possible pairs of borrow/loans, + before finally collapsing and removing all markers. *) let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) -- cgit v1.2.3 From 9aa328a70011d2784a943830bffabc600caba4ab Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 12:52:04 +0200 Subject: Cleanup a bit --- compiler/InterpreterLoopsJoinCtxs.ml | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index b58d1b3e..ce874992 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -185,15 +185,13 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) (* Explore all the *new* abstractions, and compute various maps *) let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = compute_abs_borrows_loans_maps span true explore env in + let ids_maps = compute_abs_borrows_loans_maps span explore env in let { abs_ids; abs_to_borrows; abs_to_loans = _; - abs_to_borrows_loans = _; borrow_to_abs = _; loan_to_abs; - borrow_loan_to_abs = _; } = ids_maps in @@ -338,16 +336,8 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) (* Explore all the *new* abstractions, and compute various maps *) let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = compute_abs_borrows_loans_maps span false explore ctx0.env in - let { - abs_ids; - abs_to_borrows; - abs_to_loans; - abs_to_borrows_loans = _; - borrow_to_abs; - loan_to_abs; - borrow_loan_to_abs = _; - } = + let ids_maps = compute_abs_borrows_loans_maps span explore ctx0.env in + let { abs_ids; abs_to_borrows; abs_to_loans; borrow_to_abs; loan_to_abs } = ids_maps in -- cgit v1.2.3 From ec1e958fd7bd82a4e931e1dc7acb79eeccef92ac Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 14:30:31 +0200 Subject: Factor out some code and update some comments --- compiler/InterpreterLoopsJoinCtxs.ml | 186 +++++++++++++++++------------------ 1 file changed, 88 insertions(+), 98 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index ce874992..d2f52781 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -1,6 +1,7 @@ open Types open Values open Contexts +open Utils open TypesUtils open ValuesUtils open InterpreterUtils @@ -12,64 +13,6 @@ open Errors (** The local logger *) let log = Logging.loops_join_ctxs_log -(** Reorder the loans and borrows in the fresh abstractions. - - We do this in order to enforce some structure in the environments: this - allows us to find fixed-points. Note that this function needs to be - called typically after we merge abstractions together (see {!collapse_ctx} - and {!reduce_ctx} for instance). - *) -let reorder_loans_borrows_in_fresh_abs (span : Meta.span) - (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = - let reorder_in_fresh_abs (abs : abs) : abs = - (* Split between the loans and borrows *) - let is_borrow (av : typed_avalue) : bool = - match av.value with - | ABorrow _ -> true - | ALoan _ -> false - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - let aborrows, aloans = List.partition is_borrow abs.avalues in - - (* Reoder the borrows, and the loans. - - After experimenting, it seems that a good way of reordering the loans - and the borrows to find fixed points is simply to sort them by increasing - order of id (taking the smallest id of a set of ids, in case of sets). - *) - let get_borrow_id (av : typed_avalue) : BorrowId.id = - match av.value with - | ABorrow (AMutBorrow (_, bid, _) | ASharedBorrow (_, bid)) -> bid - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - let get_loan_id (av : typed_avalue) : BorrowId.id = - match av.value with - | ALoan (AMutLoan (_, lid, _)) -> lid - | ALoan (ASharedLoan (_, lids, _, _)) -> BorrowId.Set.min_elt lids - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - (* We use ordered maps to reorder the borrows and loans *) - let reorder (get_bid : typed_avalue -> BorrowId.id) - (values : typed_avalue list) : typed_avalue list = - List.map snd - (BorrowId.Map.bindings - (BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values))) - in - let aborrows = reorder get_borrow_id aborrows in - let aloans = reorder get_loan_id aloans in - let avalues = List.append aborrows aloans in - { abs with avalues } - in - - let reorder_in_abs (abs : abs) = - if AbstractionId.Set.mem abs.abs_id old_abs_ids then abs - else reorder_in_fresh_abs abs - in - - let env = env_map_abs reorder_in_abs ctx.env in - - { ctx with env } - (** Reduce an environment. We do this to simplify an environment, for the purpose of finding a loop @@ -84,8 +27,8 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) In effect, this allows us to merge newly introduced abstractions/borrows with their parent abstractions. - For instance, when evaluating the first loop iteration, we start in the - following environment: + For instance, looking at the [list_nth_mut] example, when evaluating the + first loop iteration, we start in the following environment: {[ abs@0 { ML l0 } ls -> MB l0 (s2 : loops::List) @@ -115,7 +58,8 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) abs@3 { MB l1 } ]} - We finally merge the new abstractions together. It gives: + We finally merge the new abstractions together (abs@1 and abs@2 because + of l2, and abs@1 and abs@3 because of l1). It gives: {[ abs@0 { ML l0 } ls -> MB l4 (s@6 : loops::List) @@ -123,9 +67,20 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) abs@4 { MB l0, ML l4 } ]} - If [merge_funs] is None, we ensure that there are no markers in the environments. - If [merge_funs] is Some _, we merge environments that contain borrow/loan pairs with the same markers, omitting - pairs with the PNone marker (i.e., no marker) + If [merge_funs] is [None], we check that there are no markers in the environments. + This is the "reduce" operation. + If [merge_funs] is [Some _], when merging abstractions together, we merge the pairs + of borrows and the pairs of loans with complementary markers. This is useful to + reuse the reduce operation to implement the collapse. + For instance, when merging: + {[ + abs@0 { ML l0, |MB l1| } + abs@1 { MB l0, ︙MB l1︙ } + ]} + We get: + {[ + abs@2 { MB l1 } + ]} *) let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) @@ -274,8 +229,9 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) ^ eval_ctx_to_string ~span:(Some span) !ctx ^ "\n\n")); - (* Reorder the loans and borrows in the fresh abstractions *) - let ctx = reorder_loans_borrows_in_fresh_abs span old_ids.aids !ctx in + (* Reorder the loans and borrows in the fresh abstractions - note that we may + not have eliminated all the markers at this point. *) + let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids !ctx in log#ldebug (lazy @@ -287,37 +243,28 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) (* Return the new context *) ctx -(* Reduce_ctx can only be called in a context with no markers *) +(** Reduce_ctx can only be called in a context with no markers *) let reduce_ctx = reduce_ctx_with_markers None -(* Collapse an environment - - This is the second part of a join, where we attempt to simplify and remove all projection markers. - This function is called after reducing the environments, and attempting to simplify all the pairs - of borrows and loans. +(** Auxiliary function for collapse (see below). We traverse all abstractions, and merge abstractions when they contain the same element, - but with dual markers (i.e., PLeft and PRight). + but with dual markers (i.e., [PLeft] and [PRight]). For instance, if we have the abstractions - abs@0 { | MB l0 _ |, ML l1 } - abs@1 { ︙MB l0 _ ︙, ML l2 } - - we will merge abs@0 and abs@1 into a new abstraction abs@2, removing the marker for duplicated elements, - and taking the join of the remaining elements + {[ + abs@0 { | MB l0 _ |, ML l1 } + abs@1 { ︙MB l0 _ ︙, ML l2 } + ]} - abs@2 { MB l0 _, ML l1, ML l2 } - - Rem.: Doing this might introduce new pairs of borrow/loans to be merged in different abstractions: in the example above, - this could occur if there was another abstraction in the context containing ML l0, which would need to be simplified through - a further reduce. - It is unclear whether this can happen in practice. If so, a solution would be to preprocess the environments when doing - a join: while not in the current formalism, it is sound to split an element with no markers into a duplicated pair of the - same element with left and right markers. Doing this before reduce would allow to reduce all possible pairs of borrow/loans, - before finally collapsing and removing all markers. + We merge abs@0 and abs@1 into a new abstraction abs@2. This allows us to + eliminate the markers used for [MB l0]: + {[ + abs@2 { MB l0 _, ML l1, ML l2 } + ]} *) -let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) +let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = (* Debug *) @@ -482,8 +429,9 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) ^ eval_ctx_to_string ~span:(Some span) !ctx ^ "\n\n")); - (* Reorder the loans and borrows in the fresh abstractions *) - let ctx = reorder_loans_borrows_in_fresh_abs span old_ids.aids !ctx in + (* Reorder the loans and borrows in the fresh abstractions - note that we may + not have eliminated all the markers yet *) + let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids !ctx in log#ldebug (lazy @@ -495,16 +443,55 @@ let collapse_ctx_markers (span : Meta.span) (loop_id : LoopId.id) (* Return the new context *) ctx -(* Collapse two environments containing projection markers; this function is called after - joining environments. +(** Small utility: check whether an environment contains markers *) +let eval_ctx_has_markers (ctx : eval_ctx) : bool = + let visitor = + object + inherit [_] iter_eval_ctx + + method! visit_proj_marker _ pm = + match pm with PNone -> () | PLeft | PRight -> raise Found + end + in + try + visitor#visit_eval_ctx () ctx; + false + with Found -> true + +(** Collapse two environments containing projection markers; this function is called after + joining environments. - The collapse is done in two steps. - First, we reduce the environment, merging for instance abstractions containing MB l0 _ and ML l0, - when both elements have the same marker, e.g., PNone, PLeft, or PRight. + The collapse is done in two steps. - Second, we merge abstractions containing the same element with left and right markers respectively. + First, we reduce the environment, merging any two pair of fresh abstractions + which contain a loan (in one) and its corresponding borrow (in the other). + For instance, we merge abs@0 and abs@1 below: + {[ + abs@0 { |ML l0|, ML l1 } + abs@1 { |MB l0 _|, ML l2 } + ~~> + abs@2 { ML l1, ML l2 } + ]} + Note that we also merge abstractions when the loan/borrow don't have the same + markers. For instance, below: + {[ + abs@0 { ML l0, ML l1 } // ML l0 doesn't have markers + abs@1 { |MB l0 _|, ML l2 } + ~~> + abs@2 { ︙ML l0︙, ML l1, ML l2 } + ]} - At the end of the second step, all markers should have been removed from the resulting environment. + Second, we merge abstractions containing the same element with left and right markers + respectively. For instance: + {[ + abs@0 { | MB l0 _ |, ML l1 } + abs@1 { ︙MB l0 _ ︙, ML l2 } + ~~> + abs@2 { MB l0 _, ML l1, ML l2 } + ]} + + At the end of the second step, all markers should have been removed from the resulting + environment. *) let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) @@ -512,7 +499,10 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) let ctx = reduce_ctx_with_markers (Some merge_funs) span loop_id old_ids ctx0 in - collapse_ctx_markers span loop_id merge_funs old_ids ctx + let ctx = collapse_ctx_collapse span loop_id merge_funs old_ids ctx in + (* Sanity check: there are no markers remaining *) + sanity_check __FILE__ __LINE__ (not (eval_ctx_has_markers ctx)) span; + ctx let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) (loop_id : LoopId.id) (ctx : eval_ctx) : merge_duplicates_funcs = -- cgit v1.2.3 From 67ef9b5316b6550c3386ae095197ea513ed7dfbb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 14:56:42 +0200 Subject: Cleanup a bit --- compiler/InterpreterLoopsJoinCtxs.ml | 67 ++++++++++++++++++++---------------- 1 file changed, 37 insertions(+), 30 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index d2f52781..b25ea0fc 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -67,20 +67,23 @@ let log = Logging.loops_join_ctxs_log abs@4 { MB l0, ML l4 } ]} - If [merge_funs] is [None], we check that there are no markers in the environments. - This is the "reduce" operation. - If [merge_funs] is [Some _], when merging abstractions together, we merge the pairs - of borrows and the pairs of loans with complementary markers. This is useful to - reuse the reduce operation to implement the collapse. - For instance, when merging: - {[ - abs@0 { ML l0, |MB l1| } - abs@1 { MB l0, ︙MB l1︙ } - ]} - We get: - {[ - abs@2 { MB l1 } - ]} + - If [merge_funs] is [None], we check that there are no markers in the environments. + This is the "reduce" operation. + - If [merge_funs] is [Some _], when merging abstractions together, we merge the pairs + of borrows and the pairs of loans with the same markers **if this marker is not** + [PNone]. This is useful to reuse the reduce operation to implement the collapse. + Note that we ignore borrows/loans with the [PNone] marker: the goal of the collapse + operation is to *eliminate* markers, not to simplify the environment. + + For instance, when merging: + {[ + abs@0 { ML l0, |MB l1| } + abs@1 { MB l0, ︙MB l1︙ } + ]} + We get: + {[ + abs@2 { MB l1 } + ]} *) let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) @@ -92,7 +95,7 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) ^ eval_ctx_to_string ~span:(Some span) ctx0 ^ "\n\n")); - let allow_markers = merge_funs <> None in + let with_markers = merge_funs <> None in let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in @@ -172,18 +175,27 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) let bids = MarkerBorrowId.Set.elements bids in List.iter (fun bid -> - if not allow_markers then + if not with_markers then sanity_check __FILE__ __LINE__ (fst bid = PNone) span; - match MarkerBorrowId.Map.find_opt bid loan_to_abs with - | None -> (* Nothing to do *) () - | Some abs_ids1 -> - if allow_markers && fst bid = PNone then () - else + (* If we use markers: we are doing a collapse, which means we attempt + to eliminate markers (and this is the only goal of the operation). + We thus ignore the non-marked values (we merge non-marked values + when doing a "real" reduce, to simplify the environment in order + to converge to a fixed-point, for instance). *) + if with_markers && fst bid = PNone then () + else + match MarkerBorrowId.Map.find_opt bid loan_to_abs with + | None -> (* Nothing to do *) () + | Some abs_ids1 -> AbstractionId.Set.iter (fun abs_id1 -> (* We need to merge - unless we have already merged *) - (* First, find the representatives for the two abstractions (the - representative is the abstraction into which we merged) *) + (* First, find the representatives for the two abstractions. + + We may have merged some abstractions already, so maybe abs_id0 + and abs_id1 don't exist anymore, because they may have been + merged into other abstractions: we look for the abstractions + resulting from such merged. *) let abs_ref0 = UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) in @@ -207,7 +219,7 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) ^ ":\n\n" ^ eval_ctx_to_string ~span:(Some span) !ctx)); - (* Update the environment - pay attention to the order: we + (* Update the environment - pay attention to the order: we merge [abs_id1] *into* [abs_id0] *) let nctx, abs_id = merge_into_abstraction span abs_kind can_end merge_funs @@ -672,12 +684,7 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) (* Add projection marker to all abstractions in the left and right environments *) let add_marker (pm : proj_marker) (ee : env_elem) : env_elem = match ee with - | EAbs abs -> - EAbs - { - abs with - avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues; - } + | EAbs abs -> EAbs (abs_add_marker span ctx0 pm abs) | x -> x in -- cgit v1.2.3 From 311a162dcc65233d628303a1114b529b8eff29a0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 16:11:24 +0200 Subject: Change the order in which we merge abstractions --- compiler/InterpreterLoopsJoinCtxs.ml | 52 +++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 24 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index b25ea0fc..8ad5272a 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -146,10 +146,10 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) let ids_maps = compute_abs_borrows_loans_maps span explore env in let { abs_ids; - abs_to_borrows; - abs_to_loans = _; - borrow_to_abs = _; - loan_to_abs; + abs_to_borrows = _; + abs_to_loans; + borrow_to_abs; + loan_to_abs = _; } = ids_maps in @@ -164,27 +164,28 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) (* Merge all the mergeable abs. - We iterate over the abstractions, then over the borrows in the abstractions. + We iterate over the abstractions, then over the loans in the abstractions. We do this because we want to control the order in which abstractions are merged (the ids are iterated in increasing order). Otherwise, we - could simply iterate over all the borrows in [borrow_to_abs]... + could simply iterate over all the borrows in [loan_to_abs]... *) List.iter (fun abs_id0 -> - let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in - let bids = MarkerBorrowId.Set.elements bids in + let lids = AbstractionId.Map.find abs_id0 abs_to_loans in + let lids = MarkerBorrowId.Set.elements lids in List.iter - (fun bid -> + (fun lid -> if not with_markers then - sanity_check __FILE__ __LINE__ (fst bid = PNone) span; + sanity_check __FILE__ __LINE__ (fst lid = PNone) span; (* If we use markers: we are doing a collapse, which means we attempt to eliminate markers (and this is the only goal of the operation). We thus ignore the non-marked values (we merge non-marked values when doing a "real" reduce, to simplify the environment in order to converge to a fixed-point, for instance). *) - if with_markers && fst bid = PNone then () + if with_markers && fst lid = PNone then () else - match MarkerBorrowId.Map.find_opt bid loan_to_abs with + (* Find the borrow corresponding to the loan we want to eliminate *) + match MarkerBorrowId.Map.find_opt lid borrow_to_abs with | None -> (* Nothing to do *) () | Some abs_ids1 -> AbstractionId.Set.iter @@ -220,10 +221,12 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) ^ eval_ctx_to_string ~span:(Some span) !ctx)); (* Update the environment - pay attention to the order: - we merge [abs_id1] *into* [abs_id0] *) + we merge [abs_id1] *into* [abs_id0]. + In particular, as [abs_id0] contains the loan, it has + to be on the left. *) let nctx, abs_id = - merge_into_abstraction span abs_kind can_end merge_funs - !ctx abs_id1 abs_id0 + merge_into_first_abstraction span abs_kind can_end + merge_funs !ctx abs_id0 abs_id1 in ctx := nctx; @@ -231,7 +234,7 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in UnionFind.set abs_ref_merged abs_id)) abs_ids1) - bids) + lids) abs_ids; log#ldebug @@ -366,8 +369,8 @@ let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) (* Update the environment - pay attention to the order: we we merge [abs_id1] *into* [abs_id0] *) let nctx, abs_id = - merge_into_abstraction span abs_kind can_end - (Some merge_funs) !ctx abs_id1 abs_id0 + merge_into_first_abstraction span abs_kind can_end + (Some merge_funs) !ctx abs_id0 abs_id1 in ctx := nctx; @@ -422,8 +425,8 @@ let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) (* Update the environment - pay attention to the order: we we merge [abs_id1] *into* [abs_id0] *) let nctx, abs_id = - merge_into_abstraction span abs_kind can_end - (Some merge_funs) !ctx abs_id1 abs_id0 + merge_into_first_abstraction span abs_kind can_end + (Some merge_funs) !ctx abs_id0 abs_id1 in ctx := nctx; @@ -544,7 +547,7 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) (* We need to pick a type for the avalue. The types on the left and on the right may use different regions: it doesn't really matter (here, we pick the one from the left), because we will merge those regions together - anyway (see the comments for {!merge_into_abstraction}). + anyway (see the comments for {!merge_into_first_abstraction}). *) let ty = ty0 in let child = child0 in @@ -612,12 +615,13 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) merge_ashared_loans; } -let merge_into_abstraction (span : Meta.span) (loop_id : LoopId.id) +let merge_into_first_abstraction (span : Meta.span) (loop_id : LoopId.id) (abs_kind : abs_kind) (can_end : bool) (ctx : eval_ctx) (aid0 : AbstractionId.id) (aid1 : AbstractionId.id) : eval_ctx * AbstractionId.id = let merge_funs = mk_collapse_ctx_merge_duplicate_funs span loop_id ctx in - merge_into_abstraction span abs_kind can_end (Some merge_funs) ctx aid0 aid1 + merge_into_first_abstraction span abs_kind can_end (Some merge_funs) ctx aid0 + aid1 (** Collapse an environment, merging the duplicated borrows/loans. @@ -965,7 +969,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span) ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n" ^ eval_ctx_to_string ~span:(Some span) !joined_ctx)); - (* Reduce again to reach fixed point *) + (* Reduce again to reach a fixed point *) joined_ctx := reduce_ctx span loop_id fixed_ids !joined_ctx; log#ldebug (lazy -- cgit v1.2.3 From 3cb17966aa0c5d0e84b734c2afb4dce0f4bf22d2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jun 2024 10:52:00 +0200 Subject: Start factoring out the code of reduce_ctx and collapse_ctx --- compiler/InterpreterLoopsJoinCtxs.ml | 253 ++++++++++++++++++++++------------- 1 file changed, 162 insertions(+), 91 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 8ad5272a..e1a91707 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -13,6 +13,128 @@ open Errors (** The local logger *) let log = Logging.loops_join_ctxs_log +(** Utility. + + An environment augmented with information about its borrows/loans/abstractions + for the purpose of merging abstractions together. + We provide functions to update this information when merging two abstractions + together. We use it in {!reduce_ctx} and {!collapse_ctx}. +*) +type ctx_with_info = { ctx : eval_ctx; info : abs_borrows_loans_maps } + +let ctx_with_info_merge_into_first_abs (span : Meta.span) (abs_kind : abs_kind) + (can_end : bool) (merge_funs : merge_duplicates_funcs option) + (ctx : ctx_with_info) (abs_id0 : AbstractionId.id) + (abs_id1 : AbstractionId.id) : ctx_with_info = + (* Compute the new context and the new abstraction id *) + let nctx, nabs_id = + merge_into_first_abstraction span abs_kind can_end merge_funs ctx.ctx + abs_id0 abs_id1 + in + let nabs = ctx_lookup_abs nctx nabs_id in + (* Update the information *) + let { + abs_to_borrows = nabs_to_borrows; + abs_to_loans = nabs_to_loans; + borrow_to_abs = borrow_to_nabs; + loan_to_abs = loan_to_nabs; + _; + } = + compute_abs_borrows_loans_maps span (fun _ -> true) [ EAbs nabs ] + in + let { abs_ids; abs_to_borrows; abs_to_loans; borrow_to_abs; loan_to_abs } = + ctx.info + in + let abs_ids = + List.filter_map + (fun id -> + if id = abs_id0 then Some nabs_id + else if id = abs_id1 then None + else Some id) + abs_ids + in + (* Update the maps from makred borrows/loans to abstractions *) + let update_to_abs abs_to to_nabs to_abs = + (* Remove the old bindings *) + let abs0_elems = AbstractionId.Map.find abs_id0 abs_to in + let abs1_elems = AbstractionId.Map.find abs_id1 abs_to in + let abs01_elems = MarkerBorrowId.Set.union abs0_elems abs1_elems in + let to_abs = + MarkerBorrowId.Map.filter + (fun id _ -> not (MarkerBorrowId.Set.mem id abs01_elems)) + to_abs + in + (* Add the new ones *) + let merge _ _ _ = + (* We shouldn't have twice the same key *) + craise __FILE__ __LINE__ span "Unreachable" + in + MarkerBorrowId.Map.union merge to_nabs to_abs + in + let borrow_to_abs = + update_to_abs abs_to_borrows borrow_to_nabs borrow_to_abs + in + let loan_to_abs = update_to_abs abs_to_loans loan_to_nabs loan_to_abs in + + (* Update the maps from abstractions to marked borrows/loans *) + let update_abs_to nabs_to abs_to = + AbstractionId.Map.add_strict nabs_id + (AbstractionId.Map.find nabs_id nabs_to) + (AbstractionId.Map.remove abs_id0 + (AbstractionId.Map.remove abs_id1 abs_to)) + in + let abs_to_borrows = update_abs_to nabs_to_borrows abs_to_borrows in + let abs_to_loans = update_abs_to nabs_to_loans abs_to_loans in + let info = + { abs_ids; abs_to_borrows; abs_to_loans; borrow_to_abs; loan_to_abs } + in + { ctx = nctx; info } + +exception AbsToMerge of abstraction_id * abstraction_id + +(** Repeatedly iterate through the borrows/loans in an environment and merge the + abstractions that have to be merged according to a user-provided policy. *) +let repeat_iter_borrows_merge (span : Meta.span) (old_ids : ids_sets) + (abs_kind : abs_kind) (can_end : bool) + (merge_funs : merge_duplicates_funcs option) + (iter : + ctx_with_info -> (abstraction_id -> marker_borrow_id -> unit) -> unit) + (policy : + ctx_with_info -> + abstraction_id -> + marker_borrow_id -> + (abstraction_id * abstraction_id) option) (ctx : eval_ctx) : eval_ctx = + (* Compute the information *) + let ctx = + let is_fresh_abs_id (id : AbstractionId.id) : bool = + not (AbstractionId.Set.mem id old_ids.aids) + in + let explore (abs : abs) = is_fresh_abs_id abs.abs_id in + let info = compute_abs_borrows_loans_maps span explore ctx.env in + { ctx; info } + in + (* Explore and merge *) + let rec explore_merge (ctx : ctx_with_info) : eval_ctx = + try + iter ctx (fun aid mbid -> + (* Check if we need to merge some abstractions *) + match policy ctx aid mbid with + | None -> (* No *) () + | Some (abs_id0, abs_id1) -> + (* Yes: raise an exception *) + raise (AbsToMerge (abs_id0, abs_id1))); + (* No exception raise: return the current context *) + ctx.ctx + with AbsToMerge (abs_id0, abs_id1) -> + (* Merge and recurse *) + let ctx = + ctx_with_info_merge_into_first_abs span abs_kind can_end merge_funs ctx + abs_id0 abs_id1 + in + explore_merge ctx + in + explore_merge ctx + (** Reduce an environment. We do this to simplify an environment, for the purpose of finding a loop @@ -141,112 +263,61 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); - (* Explore all the *new* abstractions, and compute various maps *) - let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = compute_abs_borrows_loans_maps span explore env in - let { - abs_ids; - abs_to_borrows = _; - abs_to_loans; - borrow_to_abs; - loan_to_abs = _; - } = - ids_maps - in - - (* Merge the abstractions together *) - let merged_abs : AbstractionId.id UnionFind.elem AbstractionId.Map.t = - AbstractionId.Map.of_list - (List.map (fun id -> (id, UnionFind.make id)) abs_ids) - in - - let ctx = ref ctx in - (* Merge all the mergeable abs. - We iterate over the abstractions, then over the loans in the abstractions. + We iterate over the *new* abstractions, then over the loans in the abstractions. We do this because we want to control the order in which abstractions are merged (the ids are iterated in increasing order). Otherwise, we could simply iterate over all the borrows in [loan_to_abs]... *) - List.iter - (fun abs_id0 -> - let lids = AbstractionId.Map.find abs_id0 abs_to_loans in - let lids = MarkerBorrowId.Set.elements lids in - List.iter - (fun lid -> - if not with_markers then - sanity_check __FILE__ __LINE__ (fst lid = PNone) span; - (* If we use markers: we are doing a collapse, which means we attempt - to eliminate markers (and this is the only goal of the operation). - We thus ignore the non-marked values (we merge non-marked values - when doing a "real" reduce, to simplify the environment in order - to converge to a fixed-point, for instance). *) - if with_markers && fst lid = PNone then () - else - (* Find the borrow corresponding to the loan we want to eliminate *) - match MarkerBorrowId.Map.find_opt lid borrow_to_abs with - | None -> (* Nothing to do *) () - | Some abs_ids1 -> - AbstractionId.Set.iter - (fun abs_id1 -> - (* We need to merge - unless we have already merged *) - (* First, find the representatives for the two abstractions. - - We may have merged some abstractions already, so maybe abs_id0 - and abs_id1 don't exist anymore, because they may have been - merged into other abstractions: we look for the abstractions - resulting from such merged. *) - let abs_ref0 = - UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) - in - let abs_id0 = UnionFind.get abs_ref0 in - let abs_ref1 = - UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) - in - let abs_id1 = UnionFind.get abs_ref1 in - (* If the two ids are the same, it means the abstractions were already merged *) - if abs_id0 = abs_id1 then () - else ( - (* We actually need to merge the abstractions *) - - (* Debug *) - log#ldebug - (lazy - ("reduce_ctx: merging abstraction " - ^ AbstractionId.to_string abs_id1 - ^ " into " - ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx)); - - (* Update the environment - pay attention to the order: - we merge [abs_id1] *into* [abs_id0]. - In particular, as [abs_id0] contains the loan, it has - to be on the left. *) - let nctx, abs_id = - merge_into_first_abstraction span abs_kind can_end - merge_funs !ctx abs_id0 abs_id1 - in - ctx := nctx; - - (* Update the union find *) - let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in - UnionFind.set abs_ref_merged abs_id)) - abs_ids1) - lids) - abs_ids; + let ctx = + repeat_iter_borrows_merge span old_ids abs_kind can_end merge_funs + (fun ctx f -> + List.iter + (fun abs_id0 -> + let lids = AbstractionId.Map.find abs_id0 ctx.info.abs_to_loans in + MarkerBorrowId.Set.iter (f abs_id0) lids) + ctx.info.abs_ids) + (fun ctx abs_id0 lid -> + if not with_markers then + sanity_check __FILE__ __LINE__ (fst lid = PNone) span; + (* If we use markers: we are doing a collapse, which means we attempt + to eliminate markers (and this is the only goal of the operation). + We thus ignore the non-marked values (we merge non-marked values + when doing a "real" reduce, to simplify the environment in order + to converge to a fixed-point, for instance). *) + if with_markers && fst lid = PNone then None + else + (* Find the borrow corresponding to the loan we want to eliminate *) + match MarkerBorrowId.Map.find_opt lid ctx.info.borrow_to_abs with + | None -> (* Nothing to to *) None + | Some abs_ids1 -> ( + (* We need to merge *) + match AbstractionId.Set.elements abs_ids1 with + | [] -> None + | abs_id1 :: _ -> + log#ldebug + (lazy + ("reduce_ctx: merging abstraction " + ^ AbstractionId.to_string abs_id1 + ^ " into " + ^ AbstractionId.to_string abs_id0 + ^ ":\n\n" + ^ eval_ctx_to_string ~span:(Some span) ctx.ctx)); + Some (abs_id0, abs_id1))) + ctx + in log#ldebug (lazy ("reduce_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids ^ "\n\n- after reduce:\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); (* Reorder the loans and borrows in the fresh abstractions - note that we may not have eliminated all the markers at this point. *) - let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids !ctx in + let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids ctx in log#ldebug (lazy -- cgit v1.2.3 From 90a1c44c1be56e81c17373723d5098e2cfa48a37 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jun 2024 13:14:39 +0200 Subject: Factor out the code in collapse_ctx --- compiler/InterpreterLoopsJoinCtxs.ml | 207 +++++++++-------------------------- 1 file changed, 54 insertions(+), 153 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index e1a91707..7405f651 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -97,13 +97,9 @@ exception AbsToMerge of abstraction_id * abstraction_id let repeat_iter_borrows_merge (span : Meta.span) (old_ids : ids_sets) (abs_kind : abs_kind) (can_end : bool) (merge_funs : merge_duplicates_funcs option) - (iter : - ctx_with_info -> (abstraction_id -> marker_borrow_id -> unit) -> unit) - (policy : - ctx_with_info -> - abstraction_id -> - marker_borrow_id -> - (abstraction_id * abstraction_id) option) (ctx : eval_ctx) : eval_ctx = + (iter : ctx_with_info -> ('a -> unit) -> unit) + (policy : ctx_with_info -> 'a -> (abstraction_id * abstraction_id) option) + (ctx : eval_ctx) : eval_ctx = (* Compute the information *) let ctx = let is_fresh_abs_id (id : AbstractionId.id) : bool = @@ -116,9 +112,9 @@ let repeat_iter_borrows_merge (span : Meta.span) (old_ids : ids_sets) (* Explore and merge *) let rec explore_merge (ctx : ctx_with_info) : eval_ctx = try - iter ctx (fun aid mbid -> + iter ctx (fun x -> (* Check if we need to merge some abstractions *) - match policy ctx aid mbid with + match policy ctx x with | None -> (* No *) () | Some (abs_id0, abs_id1) -> (* Yes: raise an exception *) @@ -222,9 +218,6 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in let destructure_shared_values = true in - let is_fresh_abs_id (id : AbstractionId.id) : bool = - not (AbstractionId.Set.mem id old_ids.aids) - in let is_fresh_did (id : DummyVarId.id) : bool = not (DummyVarId.Set.mem id old_ids.dids) in @@ -276,9 +269,9 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) List.iter (fun abs_id0 -> let lids = AbstractionId.Map.find abs_id0 ctx.info.abs_to_loans in - MarkerBorrowId.Set.iter (f abs_id0) lids) + MarkerBorrowId.Set.iter (fun lid -> f (abs_id0, lid)) lids) ctx.info.abs_ids) - (fun ctx abs_id0 lid -> + (fun ctx (abs_id0, lid) -> if not with_markers then sanity_check __FILE__ __LINE__ (fst lid = PNone) span; (* If we use markers: we are doing a collapse, which means we attempt @@ -351,36 +344,18 @@ let reduce_ctx = reduce_ctx_with_markers None ]} *) let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) - (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) + (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = (* Debug *) log#ldebug (lazy ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids - ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string ~span:(Some span) ctx0 + ^ "\n\n- initial ctx:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in - let is_fresh_abs_id (id : AbstractionId.id) : bool = - not (AbstractionId.Set.mem id old_ids.aids) - in - - (* Explore all the *new* abstractions, and compute various maps *) - let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = compute_abs_borrows_loans_maps span explore ctx0.env in - let { abs_ids; abs_to_borrows; abs_to_loans; borrow_to_abs; loan_to_abs } = - ids_maps - in - - (* Merge the abstractions together *) - let merged_abs : AbstractionId.id UnionFind.elem AbstractionId.Map.t = - AbstractionId.Map.of_list - (List.map (fun id -> (id, UnionFind.make id)) abs_ids) - in - - let ctx = ref ctx0 in let invert_proj_marker = function | PNone -> craise __FILE__ __LINE__ span "Unreachable" @@ -390,134 +365,60 @@ let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) (* Merge all the mergeable abs where the same element in present in both abs, but with left and right markers respectively. - - We first check all borrows, then all loans *) - List.iter - (fun abs_id0 -> - let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in - let bids = MarkerBorrowId.Set.elements bids in - List.iter - (fun (pm, bid) -> - if pm = PNone then () - else - (* We are looking for an element with the same borrow_id, but with the dual marker *) - match - MarkerBorrowId.Map.find_opt - (invert_proj_marker pm, bid) - borrow_to_abs - with - | None -> (* Nothing to do *) () - | Some abs_ids1 -> - AbstractionId.Set.iter - (fun abs_id1 -> - (* We need to merge - unless we have already merged *) - (* First, find the representatives for the two abstractions (the - representative is the abstraction into which we merged) *) - let abs_ref0 = - UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) - in - let abs_id0 = UnionFind.get abs_ref0 in - let abs_ref1 = - UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) - in - let abs_id1 = UnionFind.get abs_ref1 in - (* If the two ids are the same, it means the abstractions were already merged *) - if abs_id0 = abs_id1 then () - else ( - (* We actually need to merge the abstractions *) - - (* Debug *) - log#ldebug - (lazy - ("collapse_ctx: merging abstraction " - ^ AbstractionId.to_string abs_id1 - ^ " into " - ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx)); - - (* Update the environment - pay attention to the order: we - we merge [abs_id1] *into* [abs_id0] *) - let nctx, abs_id = - merge_into_first_abstraction span abs_kind can_end - (Some merge_funs) !ctx abs_id0 abs_id1 - in - ctx := nctx; - - (* Update the union find *) - let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in - UnionFind.set abs_ref_merged abs_id)) - abs_ids1) - bids; - (* We now traverse the loans *) - let bids = AbstractionId.Map.find abs_id0 abs_to_loans in - let bids = MarkerBorrowId.Set.elements bids in - List.iter - (fun (pm, bid) -> - if pm = PNone then () - else - (* We are looking for an element with the same borrow_id, but with the dual marker *) - match - MarkerBorrowId.Map.find_opt - (invert_proj_marker pm, bid) - loan_to_abs - with - | None -> (* Nothing to do *) () - | Some abs_ids1 -> - AbstractionId.Set.iter - (fun abs_id1 -> - (* We need to merge - unless we have already merged *) - (* First, find the representatives for the two abstractions (the - representative is the abstraction into which we merged) *) - let abs_ref0 = - UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) - in - let abs_id0 = UnionFind.get abs_ref0 in - let abs_ref1 = - UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) - in - let abs_id1 = UnionFind.get abs_ref1 in - (* If the two ids are the same, it means the abstractions were already merged *) - if abs_id0 = abs_id1 then () - else ( - (* We actually need to merge the abstractions *) - - (* Debug *) - log#ldebug - (lazy - ("collapse_ctx: merging abstraction " - ^ AbstractionId.to_string abs_id1 - ^ " into " - ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx)); - - (* Update the environment - pay attention to the order: we - we merge [abs_id1] *into* [abs_id0] *) - let nctx, abs_id = - merge_into_first_abstraction span abs_kind can_end - (Some merge_funs) !ctx abs_id0 abs_id1 - in - ctx := nctx; - - (* Update the union find *) - let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in - UnionFind.set abs_ref_merged abs_id)) - abs_ids1) - bids) - abs_ids; + (* The iter function: iterate over the abstractions, and inside an abstraction + over the borrows then the loans *) + let iter ctx f = + List.iter + (fun abs_id0 -> + (* Small helper *) + let iterate is_borrow = + let m = + if is_borrow then ctx.info.abs_to_borrows else ctx.info.abs_to_loans + in + let ids = AbstractionId.Map.find abs_id0 m in + MarkerBorrowId.Set.iter (fun id -> f (abs_id0, is_borrow, id)) ids + in + (* Iterate over the borrows *) + iterate true; + (* Iterate over the loans *) + iterate false) + ctx.info.abs_ids + in + (* Check if there is an abstraction with the same borrow/loan id and the dual + marker, and merge them if it is the case. *) + let merge_policy ctx (abs_id0, is_borrow, (pm, bid)) = + if pm = PNone then None + else + (* Look for an element with the dual marker *) + match + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + (if is_borrow then ctx.info.borrow_to_abs else ctx.info.loan_to_abs) + with + | None -> (* Nothing to do *) None + | Some abs_ids1 -> ( + (* We need to merge *) + match AbstractionId.Set.elements abs_ids1 with + | [] -> None + | abs_id1 :: _ -> Some (abs_id0, abs_id1)) + in + (* Iterate and merge *) + let ctx = + repeat_iter_borrows_merge span old_ids abs_kind can_end (Some merge_funs) + iter merge_policy ctx + in log#ldebug (lazy ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids ^ "\n\n- after collapse:\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); (* Reorder the loans and borrows in the fresh abstractions - note that we may not have eliminated all the markers yet *) - let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids !ctx in + let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids ctx in log#ldebug (lazy -- cgit v1.2.3 From aa847c5ea1cfc1695b95d91cd10e3dc5bace4c33 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jun 2024 13:17:26 +0200 Subject: Do more cleanup --- compiler/InterpreterLoopsJoinCtxs.ml | 84 +++++++++++++++++++----------------- 1 file changed, 44 insertions(+), 40 deletions(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 7405f651..20271f9c 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -256,49 +256,53 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); - (* Merge all the mergeable abs. - - We iterate over the *new* abstractions, then over the loans in the abstractions. + (* + * Merge all the mergeable abs. + *) + (* We iterate over the *new* abstractions, then over the loans in the abstractions. We do this because we want to control the order in which abstractions are merged (the ids are iterated in increasing order). Otherwise, we - could simply iterate over all the borrows in [loan_to_abs]... - *) + could simply iterate over all the borrows in [loan_to_abs]... *) + let iterate ctx f = + List.iter + (fun abs_id0 -> + let lids = AbstractionId.Map.find abs_id0 ctx.info.abs_to_loans in + MarkerBorrowId.Set.iter (fun lid -> f (abs_id0, lid)) lids) + ctx.info.abs_ids + in + (* Given a loan, check if there is a fresh abstraction with the corresponding borrow *) + let merge_policy ctx (abs_id0, lid) = + if not with_markers then + sanity_check __FILE__ __LINE__ (fst lid = PNone) span; + (* If we use markers: we are doing a collapse, which means we attempt + to eliminate markers (and this is the only goal of the operation). + We thus ignore the non-marked values (we merge non-marked values + when doing a "real" reduce, to simplify the environment in order + to converge to a fixed-point, for instance). *) + if with_markers && fst lid = PNone then None + else + (* Find the borrow corresponding to the loan we want to eliminate *) + match MarkerBorrowId.Map.find_opt lid ctx.info.borrow_to_abs with + | None -> (* Nothing to to *) None + | Some abs_ids1 -> ( + (* We need to merge *) + match AbstractionId.Set.elements abs_ids1 with + | [] -> None + | abs_id1 :: _ -> + log#ldebug + (lazy + ("reduce_ctx: merging abstraction " + ^ AbstractionId.to_string abs_id1 + ^ " into " + ^ AbstractionId.to_string abs_id0 + ^ ":\n\n" + ^ eval_ctx_to_string ~span:(Some span) ctx.ctx)); + Some (abs_id0, abs_id1)) + in + (* Iterate and merge *) let ctx = - repeat_iter_borrows_merge span old_ids abs_kind can_end merge_funs - (fun ctx f -> - List.iter - (fun abs_id0 -> - let lids = AbstractionId.Map.find abs_id0 ctx.info.abs_to_loans in - MarkerBorrowId.Set.iter (fun lid -> f (abs_id0, lid)) lids) - ctx.info.abs_ids) - (fun ctx (abs_id0, lid) -> - if not with_markers then - sanity_check __FILE__ __LINE__ (fst lid = PNone) span; - (* If we use markers: we are doing a collapse, which means we attempt - to eliminate markers (and this is the only goal of the operation). - We thus ignore the non-marked values (we merge non-marked values - when doing a "real" reduce, to simplify the environment in order - to converge to a fixed-point, for instance). *) - if with_markers && fst lid = PNone then None - else - (* Find the borrow corresponding to the loan we want to eliminate *) - match MarkerBorrowId.Map.find_opt lid ctx.info.borrow_to_abs with - | None -> (* Nothing to to *) None - | Some abs_ids1 -> ( - (* We need to merge *) - match AbstractionId.Set.elements abs_ids1 with - | [] -> None - | abs_id1 :: _ -> - log#ldebug - (lazy - ("reduce_ctx: merging abstraction " - ^ AbstractionId.to_string abs_id1 - ^ " into " - ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" - ^ eval_ctx_to_string ~span:(Some span) ctx.ctx)); - Some (abs_id0, abs_id1))) - ctx + repeat_iter_borrows_merge span old_ids abs_kind can_end merge_funs iterate + merge_policy ctx in log#ldebug -- cgit v1.2.3 From 2a7a18d6a07ea4967ba9ec0763e6b7d04849dc7e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jun 2024 13:33:32 +0200 Subject: Improve collapse_ctx --- compiler/InterpreterLoopsJoinCtxs.ml | 43 +++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) (limited to 'compiler/InterpreterLoopsJoinCtxs.ml') diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 20271f9c..dbb4e5e9 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -389,6 +389,43 @@ let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) iterate false) ctx.info.abs_ids in + (* Small utility: check if we need to swap two region abstractions before + merging them. + + We might have to swap the order to make sure that if there + are loans in one abstraction and the corresponding borrows + in the other they get properly merged (if we merge them in the wrong + order, we might introduce borrowing cycles). + + Example: + If we are merging abs0 and abs1 because of the marked value + [MB l0]: + {[ + abs0 { |MB l0|, MB l1 } + abs1 { ︙MB l0︙, ML l1 } + ]} + we want to make sure that we swap them (abs1 goes to the + left) to make sure [MB l1] and [ML l1] get properly eliminated. + + Remark: in case there is a borrowing cycle between the two abstractions + (which shouldn't happen) then there isn't much we can do, and whatever + the order in which we merge, we will preserve the cycle. + *) + let swap_abs info abs_id0 abs_id1 = + let abs0_borrows = + BorrowId.Set.of_list + (List.map snd + (MarkerBorrowId.Set.elements + (AbstractionId.Map.find abs_id0 info.abs_to_borrows))) + in + let abs1_loans = + BorrowId.Set.of_list + (List.map snd + (MarkerBorrowId.Set.elements + (AbstractionId.Map.find abs_id1 info.abs_to_loans))) + in + not (BorrowId.Set.disjoint abs0_borrows abs1_loans) + in (* Check if there is an abstraction with the same borrow/loan id and the dual marker, and merge them if it is the case. *) let merge_policy ctx (abs_id0, is_borrow, (pm, bid)) = @@ -405,7 +442,11 @@ let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) (* We need to merge *) match AbstractionId.Set.elements abs_ids1 with | [] -> None - | abs_id1 :: _ -> Some (abs_id0, abs_id1)) + | abs_id1 :: _ -> + (* Check if we need to swap *) + Some + (if swap_abs ctx.info abs_id0 abs_id1 then (abs_id1, abs_id0) + else (abs_id0, abs_id1))) in (* Iterate and merge *) let ctx = -- cgit v1.2.3