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/InterpreterLoopsFixedPoint.ml | 33 ++++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 11 deletions(-) (limited to 'compiler/InterpreterLoopsFixedPoint.ml') diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 1a0bb090..599fabfd 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -153,13 +153,19 @@ 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 (pm, bid, _) | ASharedBorrow (pm, bid)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + 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 (pm, lid, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + lid + | ALoan (ASharedLoan (pm, lids, _, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + BorrowId.Set.min_elt lids | _ -> craise __FILE__ __LINE__ span "Unexpected" in (* We use ordered maps to reorder the borrows and loans *) @@ -245,7 +251,8 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : SL {l0, l1} s0 ]} - and introduce the corresponding abstraction: + and introduce the corresponding abstraction for the borrow l0 + (and we do something similar for l1): {[ abs'2 { SB l0, SL {l2} s2 } ]} @@ -283,13 +290,13 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : (* Create the shared loan *) let loan_rty = TRef (RFVar nrid, rty, RShared) in let loan_value = - ALoan (ASharedLoan (BorrowId.Set.singleton nlid, nsv, child_av)) + ALoan (ASharedLoan (PNone, BorrowId.Set.singleton nlid, nsv, child_av)) in let loan_value = mk_typed_avalue span loan_rty loan_value in (* Create the shared borrow *) let borrow_rty = loan_rty in - let borrow_value = ABorrow (ASharedBorrow lid) in + let borrow_value = ABorrow (ASharedBorrow (PNone, lid)) in let borrow_value = mk_typed_avalue span borrow_rty borrow_value in (* Create the abstraction *) @@ -344,11 +351,11 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : (* Continue the exploration *) super#visit_VSharedLoan env lids sv - method! visit_ASharedLoan env lids sv av = + method! visit_ASharedLoan env pm lids sv av = collect_shared_value lids sv; (* Continue the exploration *) - super#visit_ASharedLoan env lids sv av + super#visit_ASharedLoan env pm lids sv av (** Check that there are no symbolic values with *borrows* inside the abstraction - shouldn't happen if the symbolic values are greedily @@ -905,7 +912,9 @@ let compute_fixed_point_id_correspondance (span : Meta.span) let lookup_shared_loan lid ctx : typed_value = match snd (lookup_loan span ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v - | Abstract (ASharedLoan (_, v, _)) -> v + | Abstract (ASharedLoan (pm, _, v, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + v | _ -> craise __FILE__ __LINE__ span "Unreachable" in let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in @@ -1044,7 +1053,7 @@ let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx) object (self) inherit [_] iter_env - method! visit_ASharedLoan inside_shared _ sv child_av = + method! visit_ASharedLoan inside_shared _ _ sv child_av = self#visit_typed_value true sv; self#visit_typed_avalue inside_shared child_av @@ -1094,7 +1103,9 @@ let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx) let v = match snd (lookup_loan span ek_all bid fp_ctx) with | Concrete (VSharedLoan (_, v)) -> v - | Abstract (ASharedLoan (_, v, _)) -> v + | Abstract (ASharedLoan (pm, _, v, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + v | _ -> craise __FILE__ __LINE__ span "Unreachable" in self#visit_typed_value env v -- 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/InterpreterLoopsFixedPoint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/InterpreterLoopsFixedPoint.ml') diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 599fabfd..26505902 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -131,7 +131,7 @@ let cleanup_fresh_values_and_abs (config : config) (span : Meta.span) 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 = -- 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/InterpreterLoopsFixedPoint.ml | 76 ++++------------------------------ 1 file changed, 8 insertions(+), 68 deletions(-) (limited to 'compiler/InterpreterLoopsFixedPoint.ml') diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 26505902..033deebb 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -126,70 +126,6 @@ let cleanup_fresh_values_and_abs (config : config) (span : Meta.span) let ctx = cleanup_fresh_values fixed_ids ctx in (ctx, cc) -(** 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 (pm, bid, _) | ASharedBorrow (pm, bid)) -> - sanity_check __FILE__ __LINE__ (pm = PNone) span; - bid - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - let get_loan_id (av : typed_avalue) : BorrowId.id = - match av.value with - | ALoan (AMutLoan (pm, lid, _)) -> - sanity_check __FILE__ __LINE__ (pm = PNone) span; - lid - | ALoan (ASharedLoan (pm, lids, _, _)) -> - sanity_check __FILE__ __LINE__ (pm = PNone) span; - 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 } - let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : cm_fun = fun ctx0 -> @@ -251,11 +187,14 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : SL {l0, l1} s0 ]} - and introduce the corresponding abstraction for the borrow l0 - (and we do something similar for l1): + and introduce the corresponding abstractions for the borrows l0 and l1: {[ - abs'2 { SB l0, SL {l2} s2 } + abs'2 { SB l0, SL {l0'} s1 } // Reborrow for l0 + abs'3 { SB l1, SL {l1'} s2 } // Reborrow for l1 ]} + + Remark: of course we also need to replace the [SB l0] and the [SB l1] + values we find in the environments with [SB l0'] and [SB l1']. *) let push_abs_for_shared_value (abs : abs) (sv : typed_value) (lid : BorrowId.id) : unit = @@ -821,7 +760,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *) let fp = - reorder_loans_borrows_in_fresh_abs span (Option.get !fixed_ids).aids !fp + reorder_loans_borrows_in_fresh_abs span false (Option.get !fixed_ids).aids + !fp in (* Update the abstraction's [can_end] field and their kinds. -- 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/InterpreterLoopsFixedPoint.ml | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'compiler/InterpreterLoopsFixedPoint.ml') diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 033deebb..79beb761 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -696,10 +696,22 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) region id to abstraction id *) let fp = ref fp in let rg_to_abs = ref RegionGroupId.Map.empty in + (* List the ids of all the abstractions in the context, in the order in + which they appear (this is important to preserve some structure: + we will explore them in this order) *) + let all_abs_ids = + List.filter_map + (function EAbs abs -> Some abs.abs_id | _ -> None) + !fp.env + in let _ = RegionGroupId.Map.iter (fun rg_id ids -> - let ids = AbstractionId.Set.elements ids in + (* Make sure we explore the ids in the order in which they appear + in the context *) + let ids = + List.filter (fun id -> AbstractionId.Set.mem id ids) all_abs_ids + in (* Retrieve the first id of the group *) match ids with | [] -> @@ -742,8 +754,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) ^ AbstractionId.to_string !id0)); (* Note that we merge *into* [id0] *) let fp', id0' = - merge_into_abstraction span loop_id abs_kind false !fp id - !id0 + merge_into_first_abstraction span loop_id abs_kind false + !fp !id0 id in fp := fp'; id0 := id0'; -- cgit v1.2.3 From 5a3b8b399c182f38586b44abcf53041845d0f672 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 20:50:56 +0200 Subject: Fix an issue with the type of the values given back by loops --- compiler/InterpreterLoopsFixedPoint.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterLoopsFixedPoint.ml') diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 79beb761..b68f2a4d 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -393,7 +393,7 @@ let prepare_ashared_loans_no_synth (span : Meta.span) (loop_id : LoopId.id) let compute_loop_entry_fixed_point (config : config) (span : Meta.span) (loop_id : LoopId.id) (eval_loop_body : stl_cm_fun) (ctx0 : eval_ctx) : - eval_ctx * ids_sets * abs RegionGroupId.Map.t = + eval_ctx * ids_sets * AbstractionId.id RegionGroupId.Map.t = (* Introduce "reborrows" for the shared values in the abstractions, so that the shared values in the fixed abstractions never get modified (technically, they are immutable, but in practice we can introduce more shared loans, or @@ -702,7 +702,9 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) let all_abs_ids = List.filter_map (function EAbs abs -> Some abs.abs_id | _ -> None) - !fp.env + (* TODO: we may want to use a different order, for instance the order + in which the regions were ended. *) + (List.rev !fp.env) in let _ = RegionGroupId.Map.iter @@ -764,8 +766,7 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) craise __FILE__ __LINE__ span "Unexpected") ids; (* Register the mapping *) - let abs = ctx_lookup_abs !fp !id0 in - rg_to_abs := RegionGroupId.Map.add_strict rg_id abs !rg_to_abs) + rg_to_abs := RegionGroupId.Map.add_strict rg_id !id0 !rg_to_abs) !fp_ended_aids in let rg_to_abs = !rg_to_abs in -- cgit v1.2.3