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/InterpreterBorrows.ml | 531 +++++++++++++++++++++-------------- compiler/InterpreterLoopsCore.ml | 27 -- compiler/InterpreterLoopsJoinCtxs.ml | 346 +++++++++++++---------- compiler/Values.ml | 31 ++ 4 files changed, 552 insertions(+), 383 deletions(-) (limited to 'compiler') diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 94f32b73..e9be07aa 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1993,7 +1993,9 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) (* Return *) List.rev !absl -type borrow_or_loan_id = BorrowId of borrow_id | LoanId of loan_id +type marker_borrow_or_loan_id = + | BorrowId of proj_marker * borrow_id + | LoanId of proj_marker * loan_id type g_loan_content_with_ty = (ety * loan_content, rty * aloan_content) concrete_or_abs @@ -2002,12 +2004,12 @@ type g_borrow_content_with_ty = (ety * borrow_content, rty * aborrow_content) concrete_or_abs type merge_abstraction_info = { - loans : loan_id_set; - borrows : borrow_id_set; - borrows_loans : borrow_or_loan_id list; + loans : MarkerBorrowId.Set.t; + borrows : MarkerBorrowId.Set.t; + borrows_loans : marker_borrow_or_loan_id list; (** We use a list to preserve the order in which the borrows were found *) - loan_to_content : g_loan_content_with_ty BorrowId.Map.t; - borrow_to_content : g_borrow_content_with_ty BorrowId.Map.t; + loan_to_content : g_loan_content_with_ty MarkerBorrowId.Map.t; + borrow_to_content : g_borrow_content_with_ty MarkerBorrowId.Map.t; } (** Small utility to help merging abstractions. @@ -2023,46 +2025,57 @@ type merge_abstraction_info = { contain shared loans). *) let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) - (abs : abs) : merge_abstraction_info = - let loans : loan_id_set ref = ref BorrowId.Set.empty in - let borrows : borrow_id_set ref = ref BorrowId.Set.empty in - let borrows_loans : borrow_or_loan_id list ref = ref [] in - let loan_to_content : g_loan_content_with_ty BorrowId.Map.t ref = - ref BorrowId.Map.empty + (avalues : typed_avalue list) : merge_abstraction_info = + let loans : MarkerBorrowId.Set.t ref = ref MarkerBorrowId.Set.empty in + let borrows : MarkerBorrowId.Set.t ref = ref MarkerBorrowId.Set.empty in + let borrows_loans : marker_borrow_or_loan_id list ref = ref [] in + let loan_to_content : g_loan_content_with_ty MarkerBorrowId.Map.t ref = + ref MarkerBorrowId.Map.empty in - let borrow_to_content : g_borrow_content_with_ty BorrowId.Map.t ref = - ref BorrowId.Map.empty + let borrow_to_content : g_borrow_content_with_ty MarkerBorrowId.Map.t ref = + ref MarkerBorrowId.Map.empty in - let push_loans ids (lc : g_loan_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) span; - loans := BorrowId.Set.union !loans ids; - BorrowId.Set.iter - (fun id -> + let push_loans pm ids (lc : g_loan_content_with_ty) : unit = + let pm_ids = + BorrowId.Set.to_seq ids + |> Seq.map (fun x -> (pm, x)) + |> MarkerBorrowId.Set.of_seq + in + sanity_check __FILE__ __LINE__ + (MarkerBorrowId.Set.disjoint !loans pm_ids) + span; + loans := MarkerBorrowId.Set.union !loans pm_ids; + MarkerBorrowId.Set.iter + (fun (pm, id) -> sanity_check __FILE__ __LINE__ - (not (BorrowId.Map.mem id !loan_to_content)) + (not (MarkerBorrowId.Map.mem (pm, id) !loan_to_content)) span; - loan_to_content := BorrowId.Map.add id lc !loan_to_content; - borrows_loans := LoanId id :: !borrows_loans) - ids + loan_to_content := MarkerBorrowId.Map.add (pm, id) lc !loan_to_content; + borrows_loans := LoanId (pm, id) :: !borrows_loans) + pm_ids in - let push_loan id (lc : g_loan_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) span; - loans := BorrowId.Set.add id !loans; + let push_loan pm id (lc : g_loan_content_with_ty) : unit = + sanity_check __FILE__ __LINE__ + (not (MarkerBorrowId.Set.mem (pm, id) !loans)) + span; + loans := MarkerBorrowId.Set.add (pm, id) !loans; sanity_check __FILE__ __LINE__ - (not (BorrowId.Map.mem id !loan_to_content)) + (not (MarkerBorrowId.Map.mem (pm, id) !loan_to_content)) span; - loan_to_content := BorrowId.Map.add id lc !loan_to_content; - borrows_loans := LoanId id :: !borrows_loans + loan_to_content := MarkerBorrowId.Map.add (pm, id) lc !loan_to_content; + borrows_loans := LoanId (pm, id) :: !borrows_loans in - let push_borrow id (bc : g_borrow_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) span; - borrows := BorrowId.Set.add id !borrows; + let push_borrow pm id (bc : g_borrow_content_with_ty) : unit = + sanity_check __FILE__ __LINE__ + (not (MarkerBorrowId.Set.mem (pm, id) !borrows)) + span; + borrows := MarkerBorrowId.Set.add (pm, id) !borrows; sanity_check __FILE__ __LINE__ - (not (BorrowId.Map.mem id !borrow_to_content)) + (not (MarkerBorrowId.Map.mem (pm, id) !borrow_to_content)) span; - borrow_to_content := BorrowId.Map.add id bc !borrow_to_content; - borrows_loans := BorrowId id :: !borrows_loans + borrow_to_content := MarkerBorrowId.Map.add (pm, id) bc !borrow_to_content; + borrows_loans := BorrowId (pm, id) :: !borrows_loans in let iter_avalues = @@ -2086,7 +2099,7 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) | Abstract _ -> craise __FILE__ __LINE__ span "Unreachable" in (match lc with - | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc)) + | VSharedLoan (bids, _) -> push_loans PNone bids (Concrete (ty, lc)) | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable"); (* Continue *) super#visit_loan_content env lc @@ -2104,14 +2117,8 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) in (* Register the loans *) (match lc with - | ASharedLoan (pm, bids, _, _) -> - (* TODO: We should keep track of the marker here *) - sanity_check __FILE__ __LINE__ (pm = PNone) span; - push_loans bids (Abstract (ty, lc)) - | AMutLoan (pm, bid, _) -> - (* TODO: We should keep track of the marker here *) - sanity_check __FILE__ __LINE__ (pm = PNone) span; - push_loan bid (Abstract (ty, lc)) + | ASharedLoan (pm, bids, _, _) -> push_loans pm bids (Abstract (ty, lc)) + | AMutLoan (pm, bid, _) -> push_loan pm bid (Abstract (ty, lc)) | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) @@ -2127,18 +2134,12 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) in (* Explore the borrow content *) (match bc with - | AMutBorrow (pm, bid, _) -> - (* TODO: We should keep track of the marker here *) - sanity_check __FILE__ __LINE__ (pm = PNone) span; - push_borrow bid (Abstract (ty, bc)) - | ASharedBorrow (pm, bid) -> - (* TODO: We should keep track of the marker here *) - sanity_check __FILE__ __LINE__ (pm = PNone) span; - push_borrow bid (Abstract (ty, bc)) + | AMutBorrow (pm, bid, _) | ASharedBorrow (pm, bid) -> + push_borrow pm bid (Abstract (ty, bc)) | AProjSharedBorrow asb -> let register asb = match asb with - | AsbBorrow bid -> push_borrow bid (Abstract (ty, bc)) + | AsbBorrow bid -> push_borrow PNone bid (Abstract (ty, bc)) | AsbProjReborrows _ -> (* Can only happen if the symbolic value (potentially) contains borrows - i.e., we have nested borrows *) @@ -2159,7 +2160,7 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) end in - List.iter (iter_avalues#visit_typed_avalue None) abs.avalues; + List.iter (iter_avalues#visit_typed_avalue None) avalues; { loans = !loans; @@ -2275,7 +2276,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) loan_to_content = loan_to_content0; borrow_to_content = borrow_to_content0; } = - compute_merge_abstraction_info span ctx abs0 + compute_merge_abstraction_info span ctx abs0.avalues in let { @@ -2285,17 +2286,28 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) loan_to_content = loan_to_content1; borrow_to_content = borrow_to_content1; } = - compute_merge_abstraction_info span ctx abs1 + compute_merge_abstraction_info span ctx abs1.avalues in (* Sanity check: there is no loan/borrows which appears in both abstractions, unless we allow to merge duplicates *) if merge_funs = None then ( - (* TODO: In this case, there should be no proj markers *) sanity_check __FILE__ __LINE__ - (BorrowId.Set.disjoint borrows0 borrows1) + (List.for_all + (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) + borrows_loans0) + span; + sanity_check __FILE__ __LINE__ + (List.for_all + (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) + borrows_loans1) span; - sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) span); + sanity_check __FILE__ __LINE__ + (MarkerBorrowId.Set.disjoint borrows0 borrows1) + span; + sanity_check __FILE__ __LINE__ + (MarkerBorrowId.Set.disjoint loans0 loans1) + span); (* Merge. There are several cases: @@ -2315,8 +2327,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) We ignore this case for now: we check that whenever we merge two shared loans, then their sets of ids are equal. *) - let merged_borrows = ref BorrowId.Set.empty in - let merged_loans = ref BorrowId.Set.empty in + let merged_borrows = ref MarkerBorrowId.Set.empty in + let merged_loans = ref MarkerBorrowId.Set.empty in let avalues = ref [] in let push_avalue av = log#ldebug @@ -2329,142 +2341,43 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) match av with None -> () | Some av -> push_avalue av in - let intersect = - BorrowId.Set.union - (BorrowId.Set.inter loans0 borrows1) - (BorrowId.Set.inter loans1 borrows0) - in - let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t = - let bids = BorrowId.Set.diff bids intersect in - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span; - bids + (* Phase 1 of the merge: We want to simplify all loan/borrow pairs. *) + + (* There is an asymetry in the merge: We only simplify a loan/borrow pair if the loan is in + the abstraction on the left *) + let intersect = MarkerBorrowId.Set.inter loans0 borrows1 in + + (* This function is called when handling shared loans, where the projection marker is global to a set of borrow ids. + Tracking this requires some set transformations *) + let filter_bids (pm : proj_marker) (bids : BorrowId.Set.t) : BorrowId.Set.t = + let bids = + BorrowId.Set.to_seq bids + |> Seq.map (fun x -> (pm, x)) + |> MarkerBorrowId.Set.of_seq + in + let bids = MarkerBorrowId.Set.diff bids intersect in + sanity_check __FILE__ __LINE__ (not (MarkerBorrowId.Set.is_empty bids)) span; + MarkerBorrowId.Set.to_seq bids |> Seq.map snd |> BorrowId.Set.of_seq in - let filter_bid (bid : BorrowId.id) : BorrowId.id option = - if BorrowId.Set.mem bid intersect then None else Some bid + let filter_bid (bid : marker_borrow_id) : marker_borrow_id option = + if MarkerBorrowId.Set.mem bid intersect then None else Some bid in - let borrow_is_merged id = BorrowId.Set.mem id !merged_borrows in + let borrow_is_merged id = MarkerBorrowId.Set.mem id !merged_borrows in let set_borrow_as_merged id = - merged_borrows := BorrowId.Set.add id !merged_borrows + merged_borrows := MarkerBorrowId.Set.add id !merged_borrows in - let loan_is_merged id = BorrowId.Set.mem id !merged_loans in + let loan_is_merged id = MarkerBorrowId.Set.mem id !merged_loans in let set_loan_as_merged id = - merged_loans := BorrowId.Set.add id !merged_loans + merged_loans := MarkerBorrowId.Set.add id !merged_loans in - let set_loans_as_merged ids = BorrowId.Set.iter set_loan_as_merged ids in - - (* Some utility functions *) - (* Merge two aborrow contents - note that those contents must have the same id *) - let merge_aborrow_contents (ty0 : rty) (bc0 : aborrow_content) (ty1 : rty) - (bc1 : aborrow_content) : typed_avalue = - match (bc0, bc1) with - | AMutBorrow (pm0, id0, child0), AMutBorrow (pm1, id1, child1) -> - (* Sanity-check of the precondition *) - sanity_check __FILE__ __LINE__ (id0 = id1) span; - (* TODO: We should handle the markers here *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; - (Option.get merge_funs).merge_amut_borrows id0 ty0 pm0 child0 ty1 pm1 - child1 - | ASharedBorrow (pm0, id0), ASharedBorrow (pm1, id1) -> - (* Sanity-check of the precondition *) - sanity_check __FILE__ __LINE__ (id0 = id1) span; - (* TODO: We should handle the markers here *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; - (Option.get merge_funs).merge_ashared_borrows id0 ty0 pm0 ty1 pm1 - | AProjSharedBorrow _, AProjSharedBorrow _ -> - (* Unreachable because requires nested borrows *) - craise __FILE__ __LINE__ span "Unreachable" - | _ -> - (* Unreachable because those cases are ignored (ended/ignored borrows) - or inconsistent *) - craise __FILE__ __LINE__ span "Unreachable" - in - - let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) - (bc1 : g_borrow_content_with_ty) : typed_avalue = - match (bc0, bc1) with - | Concrete _, Concrete _ -> - (* This can happen only in case of nested borrows *) - craise __FILE__ __LINE__ span "Unreachable" - | Abstract (ty0, bc0), Abstract (ty1, bc1) -> - merge_aborrow_contents ty0 bc0 ty1 bc1 - | Concrete _, Abstract _ | Abstract _, Concrete _ -> - (* TODO: is it really unreachable? *) - craise __FILE__ __LINE__ span "Unreachable" - in - - let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty) - (lc1 : aloan_content) : typed_avalue option = - match (lc0, lc1) with - | AMutLoan (pm0, id0, child0), AMutLoan (pm1, id1, child1) -> - (* Sanity-check of the precondition *) - sanity_check __FILE__ __LINE__ (id0 = id1) span; - (* TODO: We should handle the markers here *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; - (* Register the loan id *) - set_loan_as_merged id0; - (* Merge *) - Some - ((Option.get merge_funs).merge_amut_loans id0 ty0 pm0 child0 ty1 pm1 - child1) - | ASharedLoan (pm0, ids0, sv0, child0), ASharedLoan (pm1, ids1, sv1, child1) - -> - (* TODO: We should handle the markers here *) - sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; - (* Filter the ids *) - let ids0 = filter_bids ids0 in - let ids1 = filter_bids ids1 in - (* Check that the sets of ids are the same - if it is not the case, it - means we actually need to merge more than 2 avalues: we ignore this - case for now *) - sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span; - let ids = ids0 in - if BorrowId.Set.is_empty ids then ( - (* If the set of ids is empty, we can eliminate this shared loan. - For now, we check that we can eliminate the whole shared value - altogether. - A more complete approach would be to explore the value and introduce - as many shared loans/borrows/etc. as necessary for the sub-values. - For now, we check that there are no such values that we would need - to preserve (in practice it works because we destructure the - shared values in the abstractions, and forbid nested borrows). - *) - sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv0.value)) - span; - sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv0.value)) - span; - sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; - sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; - None) - else ( - (* Register the loan ids *) - set_loans_as_merged ids; - (* Merge *) - Some - ((Option.get merge_funs).merge_ashared_loans ids ty0 pm0 sv0 child0 - ty1 pm1 sv1 child1)) - | _ -> - (* Unreachable because those cases are ignored (ended/ignored borrows) - or inconsistent *) - craise __FILE__ __LINE__ span "Unreachable" - in - - (* Note that because we may filter ids from a set of id, this function has - to register the merged loan ids: the caller doesn't do it (contrary to - the borrow case) *) - let merge_g_loan_contents (lc0 : g_loan_content_with_ty) - (lc1 : g_loan_content_with_ty) : typed_avalue option = - match (lc0, lc1) with - | Concrete _, Concrete _ -> - (* This can not happen: the values should have been destructured *) - craise __FILE__ __LINE__ span "Unreachable" - | Abstract (ty0, lc0), Abstract (ty1, lc1) -> - merge_aloan_contents ty0 lc0 ty1 lc1 - | Concrete _, Abstract _ | Abstract _, Concrete _ -> - (* TODO: is it really unreachable? *) - craise __FILE__ __LINE__ span "Unreachable" + let set_loans_as_merged pm ids = + let ids = + BorrowId.Set.to_seq ids + |> Seq.map (fun x -> (pm, x)) + |> MarkerBorrowId.Set.of_seq + in + MarkerBorrowId.Set.iter set_loan_as_merged ids in (* Note that we first explore the borrows/loans of [abs1], because we @@ -2475,11 +2388,12 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) List.iter (fun bl -> match bl with - | BorrowId bid -> + | BorrowId (pm, bid) -> + let bid = (pm, bid) in log#ldebug (lazy ("merge_into_abstraction_aux: merging borrow " - ^ BorrowId.to_string bid)); + ^ MarkerBorrowId.to_string bid)); (* Check if the borrow has already been merged - this can happen because we go through all the borrows/loans in [abs0] *then* @@ -2493,8 +2407,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) | None -> () | Some bid -> (* Lookup the contents *) - let bc0 = BorrowId.Map.find_opt bid borrow_to_content0 in - let bc1 = BorrowId.Map.find_opt bid borrow_to_content1 in + let bc0 = MarkerBorrowId.Map.find_opt bid borrow_to_content0 in + let bc1 = MarkerBorrowId.Map.find_opt bid borrow_to_content1 in (* Merge *) let av : typed_avalue = match (bc0, bc1) with @@ -2508,12 +2422,15 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty, bc) -> { value = ABorrow bc; ty }) | Some bc0, Some bc1 -> - sanity_check __FILE__ __LINE__ (merge_funs <> None) span; - merge_g_borrow_contents bc0 bc1 + (* With markers, the case where the same borrow is duplicated should now be unreachable. + Note, this is due to all shared borrows currently taking different ids, this will + not be the case anymore when shared loans will take a unique id instead of a set *) + craise __FILE__ __LINE__ span "Unreachable" | None, None -> craise __FILE__ __LINE__ span "Unreachable" in push_avalue av) - | LoanId bid -> + | LoanId (pm, bid) -> + let bid = (pm, bid) in if (* Check if the loan has already been treated - it can happen for the same reason as for borrows, and also because shared @@ -2526,15 +2443,15 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) log#ldebug (lazy ("merge_into_abstraction_aux: merging loan " - ^ BorrowId.to_string bid)); + ^ MarkerBorrowId.to_string bid)); (* Check if we need to filter it *) match filter_bid bid with | None -> () | Some bid -> (* Lookup the contents *) - let lc0 = BorrowId.Map.find_opt bid loan_to_content0 in - let lc1 = BorrowId.Map.find_opt bid loan_to_content1 in + let lc0 = MarkerBorrowId.Map.find_opt bid loan_to_content0 in + let lc1 = MarkerBorrowId.Map.find_opt bid loan_to_content1 in (* Merge *) let av : typed_avalue option = match (lc0, lc1) with @@ -2547,9 +2464,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) | Abstract (ty, lc) -> ( match lc with | ASharedLoan (pm, bids, sv, child) -> - (* TODO: We should handle the markers here *) - sanity_check __FILE__ __LINE__ (pm = PNone) span; - let bids = filter_bids bids in + let bids = filter_bids pm bids in sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span; @@ -2559,7 +2474,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) (not (value_has_loans_or_borrows ctx sv.value)) span; let lc = ASharedLoan (pm, bids, sv, child) in - set_loans_as_merged bids; + set_loans_as_merged pm bids; Some { value = ALoan lc; ty } | AMutLoan _ -> set_loan_as_merged bid; @@ -2570,8 +2485,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) (* The abstraction has been destructured, so those shouldn't appear *) craise __FILE__ __LINE__ span "Unreachable")) | Some lc0, Some lc1 -> - sanity_check __FILE__ __LINE__ (merge_funs <> None) span; - merge_g_loan_contents lc0 lc1 + (* With projection markers, shared loans should not be duplicated *) + craise __FILE__ __LINE__ span "Unreachable" | None, None -> craise __FILE__ __LINE__ span "Unreachable" in push_opt_avalue av)) @@ -2579,7 +2494,209 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) (* Reverse the avalues (we visited the loans/borrows in order, but pushed new values at the beggining of the stack of avalues) *) - let avalues = List.rev !avalues in + let abs_values = List.rev !avalues in + + (* Phase 2: We now remove markers, by replacing pairs of the same element with left/right markers into one element + with only one marker. To do so, we linearly traverse the abstraction created through the first phase *) + + (* We first reset the list of avalues, and will construct avalues similarly to the previous phase *) + avalues := []; + + (* We recompute the relevant information on the abstraction after phase 1 *) + let { loans; borrows; borrows_loans; loan_to_content; borrow_to_content } = + compute_merge_abstraction_info span ctx abs_values + in + + (* We will merge elements with the same borrow/loan id, but with different markers. + Hence, we only keep track of the id here: if Borrow PLeft bid has been merged + and we see Borrow PRight bid, we should ignore Borrow PRight bid *) + let merged_borrows = ref BorrowId.Set.empty in + let merged_loans = ref BorrowId.Set.empty in + + let borrow_is_merged id = BorrowId.Set.mem id !merged_borrows in + let set_borrow_as_merged id = + merged_borrows := BorrowId.Set.add id !merged_borrows + in + + let loan_is_merged id = BorrowId.Set.mem id !merged_loans in + let set_loan_as_merged id = + merged_loans := BorrowId.Set.add id !merged_loans + in + let set_loans_as_merged ids = BorrowId.Set.iter set_loan_as_merged ids in + + (* Recreates an avalue from a borrow_content. *) + let avalue_from_bc = function + | Concrete (_, _) -> + (* This can happen only in case of nested borrows, and should have been filtered during phase 1 *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty, bc) -> { value = ABorrow bc; ty } + in + + (* Recreates an avalue from a loan_content *) + let avalue_from_lc = function + | Concrete (_, _) -> + (* This can happen only in case of nested borrows, and should have been filtered during phase 1 *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty, bc) -> { value = ALoan bc; ty } + in + + (* Some utility functions *) + (* Merge two aborrow contents - note that those contents must have the same id *) + let merge_aborrow_contents (ty0 : rty) (bc0 : aborrow_content) (ty1 : rty) + (bc1 : aborrow_content) : typed_avalue = + match (bc0, bc1) with + | AMutBorrow (pm0, id0, child0), AMutBorrow (pm1, id1, child1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + sanity_check __FILE__ __LINE__ + ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft)) + span; + (Option.get merge_funs).merge_amut_borrows id0 ty0 pm0 child0 ty1 pm1 + child1 + | ASharedBorrow (pm0, id0), ASharedBorrow (pm1, id1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + sanity_check __FILE__ __LINE__ + ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft)) + span; + (Option.get merge_funs).merge_ashared_borrows id0 ty0 pm0 ty1 pm1 + | AProjSharedBorrow _, AProjSharedBorrow _ -> + (* Unreachable because requires nested borrows *) + craise __FILE__ __LINE__ span "Unreachable" + | _ -> + (* Unreachable because those cases are ignored (ended/ignored borrows) + or inconsistent *) + craise __FILE__ __LINE__ span "Unreachable" + in + + let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) + (bc1 : g_borrow_content_with_ty) : typed_avalue = + match (bc0, bc1) with + | Concrete _, Concrete _ -> + (* This can happen only in case of nested borrows *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty0, bc0), Abstract (ty1, bc1) -> + merge_aborrow_contents ty0 bc0 ty1 bc1 + | Concrete _, Abstract _ | Abstract _, Concrete _ -> + (* TODO: is it really unreachable? *) + craise __FILE__ __LINE__ span "Unreachable" + in + + let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty) + (lc1 : aloan_content) : typed_avalue = + match (lc0, lc1) with + | AMutLoan (pm0, id0, child0), AMutLoan (pm1, id1, child1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + sanity_check __FILE__ __LINE__ + ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft)) + span; + (* Register the loan id *) + set_loan_as_merged id0; + (* Merge *) + (Option.get merge_funs).merge_amut_loans id0 ty0 pm0 child0 ty1 pm1 + child1 + | ASharedLoan (pm0, ids0, sv0, child0), ASharedLoan (pm1, ids1, sv1, child1) + -> + sanity_check __FILE__ __LINE__ + ((pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft)) + span; + (* Check that the sets of ids are the same - if it is not the case, it + means we actually need to merge more than 2 avalues: we ignore this + case for now *) + sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span; + let ids = ids0 in + (* Register the loan ids *) + set_loans_as_merged ids; + (* Merge *) + (Option.get merge_funs).merge_ashared_loans ids ty0 pm0 sv0 child0 ty1 + pm1 sv1 child1 + | _ -> + (* Unreachable because those cases are ignored (ended/ignored borrows) + or inconsistent *) + craise __FILE__ __LINE__ span "Unreachable" + in + + (* Note that because we may filter ids from a set of id, this function has + to register the merged loan ids: the caller doesn't do it (contrary to + the borrow case) *) + let merge_g_loan_contents (lc0 : g_loan_content_with_ty) + (lc1 : g_loan_content_with_ty) : typed_avalue = + match (lc0, lc1) with + | Concrete _, Concrete _ -> + (* This can not happen: the values should have been destructured *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty0, lc0), Abstract (ty1, lc1) -> + merge_aloan_contents ty0 lc0 ty1 lc1 + | Concrete _, Abstract _ | Abstract _, Concrete _ -> + (* TODO: is it really unreachable? *) + craise __FILE__ __LINE__ span "Unreachable" + in + + let invert_proj_marker = function + | PNone -> craise __FILE__ __LINE__ span "Unreachable" + | PLeft -> PRight + | PRight -> PLeft + in + + (* We now iter over all elements in the current abstraction. For each element with a marker + (i.e., not PNone), we attempt to find the dual element in the rest of the list. If so, + we remove both elements, and insert the same element but with no marker. + + Importantly, attempting the merge when first seeing a marked element allows us to preserve + the structure of the abstraction we are merging into (abs1). During phase1, we traversed + the borrow_loans of the abs1 first, and hence these elements are at the top of the list *) + List.iter + (function + | BorrowId (PNone, bid) -> + (* This element has no marker. We do not filter it, hence we retrieve the contents and inject it into + the avalues list *) + let bc = MarkerBorrowId.Map.find (PNone, bid) borrow_to_content in + push_avalue (avalue_from_bc bc) + | BorrowId (pm, bid) -> + (* Check if the borrow has already been merged. If so, it was already added to the avalues list, we skip it *) + if borrow_is_merged bid then () + else ( + set_borrow_as_merged bid; + let bc0 = MarkerBorrowId.Map.find (pm, bid) borrow_to_content in + let obc1 = + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + borrow_to_content + in + match obc1 with + | None -> + (* No dual element found, we keep the current one in the list of avalues, with the same marker *) + push_avalue (avalue_from_bc bc0) + | Some bc1 -> + (* We have borrows with left and right markers in the environment. + We merge their values, and push the result to the list of avalues. The merge will also remove the projection marker *) + push_avalue (merge_g_borrow_contents bc0 bc1)) + | LoanId (PNone, bid) -> + (* Same as BorrowId PNone above. We do not filter this element *) + let lc = MarkerBorrowId.Map.find (PNone, bid) loan_to_content in + push_avalue (avalue_from_lc lc) + | LoanId (pm, bid) -> ( + if + (* Check if the loan has already been merged. If so, we skip it *) + loan_is_merged bid + then () + else + let lc0 = MarkerBorrowId.Map.find (pm, bid) loan_to_content in + let olc1 = + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + loan_to_content + in + match olc1 with + | None -> + (* No dual element found, we keep the current one with the same marker *) + push_avalue (avalue_from_lc lc0) + | Some lc1 -> push_avalue (merge_g_loan_contents lc0 lc1))) + borrows_loans; + + (* We traversed and pushed elements in the same order as the traversal, so we do not need to reverse the list *) + let avalues = !avalues in (* Reorder the avalues. We want the avalues to have the borrows first, then the loans (this structure is more stable when we merge abstractions together, diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 23e05e06..cd609ab0 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -26,33 +26,6 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result (** Union Find *) module UF = UnionFind.Make (UnionFind.StoreMap) -type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord] - -module MarkerBorrowIdOrd = struct - type t = marker_borrow_id - - let compare = compare_marker_borrow_id - let to_string = show_marker_borrow_id - let pp_t = pp_marker_borrow_id - let show_t = show_marker_borrow_id -end - -module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd) -module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd) - -module MarkerBorrowId : sig - type t - - module Set : Collections.Set with type elt = t - module Map : Collections.Map with type key = t -end -with type t = marker_borrow_id = struct - type t = marker_borrow_id - - module Set = MarkerBorrowIdSet - module Map = MarkerBorrowIdMap -end - (** A small utility - Rem.: some environments may be ill-formed (they may contain several times 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 diff --git a/compiler/Values.ml b/compiler/Values.ml index ca33604d..c32cbc6e 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -180,6 +180,37 @@ type abstraction_id_set = AbstractionId.Set.t [@@deriving show, ord] For additional explanations see: https://arxiv.org/pdf/2404.02680#section.5 *) type proj_marker = PNone | PLeft | PRight [@@deriving show, ord] +type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord] + +module MarkerBorrowIdOrd = struct + type t = marker_borrow_id + + let compare = compare_marker_borrow_id + let to_string = show_marker_borrow_id + let pp_t = pp_marker_borrow_id + let show_t = show_marker_borrow_id +end + +module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd) +module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd) + +module MarkerBorrowId : sig + type t + + val to_string : t -> string + + module Set : Collections.Set with type elt = t + module Map : Collections.Map with type key = t +end +with type t = marker_borrow_id = struct + type t = marker_borrow_id + + let to_string = show_marker_borrow_id + + module Set = MarkerBorrowIdSet + module Map = MarkerBorrowIdMap +end + (** Ancestor for {!typed_avalue} iter visitor *) class ['self] iter_typed_avalue_base = object (self : 'self) -- cgit v1.2.3