Change the order in which we merge abstractions

5 files changed, 99 insertions, 105 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 48292181..b46a5da8 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -566,7 +566,9 @@ let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span)
         | AEndedSharedLoan (_, _) ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
-        | ASharedLoan (_, _, _, _) -> internal_error __FILE__ __LINE__ span
+        | ASharedLoan (_, _, _, _) ->
+            (* We get there if the projection marker is not [PNone] *)
+            internal_error __FILE__ __LINE__ span
         | AIgnoredMutLoan (bid_opt, child) ->
             (* This loan is ignored, but we may have to project on a subvalue
              * of the value which is given back *)
@@ -2013,7 +2015,7 @@ type merge_abstraction_info = {
     We compute the list of loan/borrow contents, maps from borrow/loan ids
     to borrow/loan contents, etc.
 
-    Note that this function is very specific to [merge_into_abstraction]: we
+    Note that this function is very specific to [merge_into_first_abstraction]: we
     have strong assumptions about the shape of the abstraction, and in
     particular that:
     - its values don't contain nested borrows
@@ -2032,25 +2034,6 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
     ref MarkerBorrowId.Map.empty
   in
 
-  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 (MarkerBorrowId.Map.mem (pm, id) !loan_to_content))
-          span;
-        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 pm id (lc : g_loan_content_with_ty) : unit =
     sanity_check __FILE__ __LINE__
       (not (MarkerBorrowId.Set.mem (pm, id) !loans))
@@ -2062,6 +2045,9 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
     loan_to_content := MarkerBorrowId.Map.add (pm, id) lc !loan_to_content;
     borrows_loans := LoanId (pm, id) :: !borrows_loans
   in
+  let push_loans pm ids lc : unit =
+    BorrowId.Set.iter (fun id -> push_loan pm id lc) ids
+  in
   let push_borrow pm id (bc : g_borrow_content_with_ty) : unit =
     sanity_check __FILE__ __LINE__
       (not (MarkerBorrowId.Set.mem (pm, id) !borrows))
@@ -2086,19 +2072,11 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx)
       method! visit_typed_value _ (v : typed_value) =
         super#visit_typed_value (Some (Concrete v.ty)) v
 
-      method! visit_loan_content env lc =
-        (* Can happen if we explore shared values whose sub-values are
-           reborrowed *)
-        let ty =
-          match Option.get env with
-          | Concrete ty -> ty
-          | Abstract _ -> craise __FILE__ __LINE__ span "Unreachable"
-        in
-        (match lc with
-        | VSharedLoan (bids, _) -> push_loans PNone bids (Concrete (ty, lc))
-        | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable");
-        (* Continue *)
-        super#visit_loan_content env lc
+      method! visit_loan_content _ _ =
+        (* Could happen if we explore shared values whose sub-values are
+           reborrowed. We use the fact that we destructure the nested shared
+           loans before reducing a context or computing a join. *)
+        craise __FILE__ __LINE__ span "Unreachable"
 
       method! visit_borrow_content _ _ =
         (* Can happen if we explore shared values which contain borrows -
@@ -2244,12 +2222,12 @@ type merge_duplicates_funcs = {
 
     Merge two abstractions into one, without updating the context.
  *)
-let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
+let merge_into_first_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
     (can_end : bool) (merge_funs : merge_duplicates_funcs option)
     (ctx : eval_ctx) (abs0 : abs) (abs1 : abs) : abs =
   log#ldebug
     (lazy
-      ("merge_into_abstraction_aux:\n- abs0:\n"
+      ("merge_into_first_abstraction_aux:\n- abs0:\n"
       ^ abs_to_string span ctx abs0
       ^ "\n\n- abs1:\n"
       ^ abs_to_string span ctx abs1));
@@ -2285,8 +2263,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
     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 *)
+  (* Sanity check: no markers appear unless we allow merging duplicates *)
   if merge_funs = None then (
     sanity_check __FILE__ __LINE__
       (List.for_all
@@ -2313,7 +2290,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
      - if a borrow/loan is present in both abstractions, we need to merge its
        content.
 
-     Note that it is possible that we may need to merge strictly more than 2 avalues,
+     Note that it is possible that we may need to merge strictly more than two avalues,
      because of shared loans. For instance, if we have:
      {[
        abs'0 { shared_loan { l0, l1 } ... }
@@ -2329,7 +2306,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
   let push_avalue av =
     log#ldebug
       (lazy
-        ("merge_into_abstraction_aux: push_avalue: "
+        ("merge_into_first_abstraction_aux: push_avalue: "
         ^ typed_avalue_to_string ~span:(Some span) ctx av));
     avalues := av :: !avalues
   in
@@ -2337,14 +2314,14 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
     match av with None -> () | Some av -> push_avalue av
   in
 
-  (* Phase 1 of the merge: We want to simplify all loan/borrow pairs. *)
+  (* Phase 1 of the merge: we 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 *)
+  (* 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 *)
+  (* This function is called when handling shared loans: we have to apply a projection
+     marker to a set of borrow ids. *)
   let filter_bids (pm : proj_marker) (bids : BorrowId.Set.t) : BorrowId.Set.t =
     let bids =
       BorrowId.Set.to_seq bids
@@ -2388,7 +2365,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
           let bid = (pm, bid) in
           log#ldebug
             (lazy
-              ("merge_into_abstraction_aux: merging borrow "
+              ("merge_into_first_abstraction_aux: merging borrow "
               ^ MarkerBorrowId.to_string bid));
 
           (* Check if the borrow has already been merged - this can happen
@@ -2438,7 +2415,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
           else (
             log#ldebug
               (lazy
-                ("merge_into_abstraction_aux: merging loan "
+                ("merge_into_first_abstraction_aux: merging loan "
                 ^ MarkerBorrowId.to_string bid));
 
             (* Check if we need to filter it *)
@@ -2496,7 +2473,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind)
      with only one marker. To do so, we linearly traverse the abstraction created through the first phase *)
   log#ldebug
     (lazy
-      ("merge_into_abstraction_aux: starting phase 2\n- abs:\n"
+      ("merge_into_first_abstraction_aux: starting phase 2\n- abs:\n"
       ^ abs_to_string span ctx { abs0 with avalues = abs_values }));
 
   (* We first reset the list of avalues, and will construct avalues similarly to the previous phase *)
@@ -2777,7 +2754,7 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id)
   let env = Substitute.env_subst_rids rsubst ctx.env in
   { ctx with env }
 
-let merge_into_abstraction (span : Meta.span) (abs_kind : abs_kind)
+let merge_into_first_abstraction (span : Meta.span) (abs_kind : abs_kind)
     (can_end : bool) (merge_funs : merge_duplicates_funcs option)
     (ctx : eval_ctx) (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) :
     eval_ctx * AbstractionId.id =
@@ -2787,13 +2764,14 @@ let merge_into_abstraction (span : Meta.span) (abs_kind : abs_kind)
 
   (* Merge them *)
   let nabs =
-    merge_into_abstraction_aux span abs_kind can_end merge_funs ctx abs0 abs1
+    merge_into_first_abstraction_aux span abs_kind can_end merge_funs ctx abs0
+      abs1
   in
 
-  (* Update the environment: replace the abstraction 1 with the result of the merge,
-     remove the abstraction 0 *)
-  let ctx = fst (ctx_subst_abs span ctx abs_id1 nabs) in
-  let ctx = fst (ctx_remove_abs span ctx abs_id0) in
+  (* Update the environment: replace the abstraction 0 with the result of the merge,
+     remove the abstraction 1 *)
+  let ctx = fst (ctx_subst_abs span ctx abs_id0 nabs) in
+  let ctx = fst (ctx_remove_abs span ctx abs_id1) in
 
   (* Merge all the regions from the abstraction into one (the first - i.e., the
      one with the smallest id). Note that we need to do this in the whole
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 0bc2bfab..cf14e94b 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -212,24 +212,36 @@ type merge_duplicates_funcs = {
 
 (** Merge an abstraction into another abstraction.
 
-    We insert the result of the merge in place of the second abstraction (and in
+    We insert the result of the merge in place of the first abstraction (and in
     particular, we don't simply push the merged abstraction at the end of the
     environment: this helps preserving the structure of the environment, when
     computing loop fixed points for instance).
 
-    When we merge two abstractions together, we remove the loans/borrows
-    which appear in one and whose associated loans/borrows appear in the
-    other. For instance:
+    When we merge two abstractions together, we remove the loans which appear
+    in the *left* abstraction and whose corresponding borrows appear in the
+    **right** abstraction.
+    For instance:
     {[
       abs'0 { mut_borrow l0, mut_loan l1 }   // Rem.: mut_loan l1
       abs'1 { mut_borrow l1, mut_borrow l2 } // Rem.: mut_borrow l1
 
           ~~>
 
-      abs'01 { mut_borrow l0, mut_borrow l2 }
+      abs'2 { mut_borrow l0, mut_borrow l2 }
+    ]}
+
+    We also simplify the markers, when the same value appears in both abstractions
+    but with different markers. For instance:
+    {[
+      abs'0 { |mut_borrow l0|, mut_loan l1 }
+      abs'1 { ︙mut_borrow l0︙, mut_borrow l1 }
+
+          ~~>
+
+      abs'2 { mut_borrow l0 }
     ]}
 
-    Also, we merge all their regions together. For instance, if [abs'0] projects
+    Finally, we merge all their regions together. For instance, if [abs'0] projects
     region [r0] and [abs'1] projects region [r1], we pick one of the two, say [r0]
     (the one with the smallest index in practice) and substitute [r1] with [r0]
     in the whole context.
@@ -237,22 +249,10 @@ type merge_duplicates_funcs = {
     Parameters:
     - [kind]
     - [can_end]
-    - [merge_funs]: Those functions are used to merge borrows/loans with the
-      *same ids*. For instance, when performing environment joins we may introduce
-      abstractions which both contain loans/borrows with the same ids. When we
-      later merge those abstractions together, we need to call a merge function
-      to reconcile the borrows/loans. For instance, if both abstractions contain
-      the same shared loan [l0], we will call {!merge_ashared_borrows} to derive
-      a shared value for the merged shared loans.
-
-      For instance, this happens for the following abstractions:
-      {[
-        abs'0 { mut_borrow l0, mut_loan l1 } // mut_borrow l0 !
-        abs'1 { mut_borrow l0, mut_loan l2 } // mut_borrow l0 !
-      ]}
-      If you want to forbid this, provide [None]. In that case, [merge_into_abstraction]
-      actually simply performs some sort of a union.
-
+    - [merge_funs]: those functions are used to merge borrows/loans with the
+      *same ids* but different markers. This is necessary when doing a collapse
+      (see the computation of joins).
+      If [merge_funs] are not provided, we check that there are no markers.
     - [ctx]
     - [abs_id0]
     - [abs_id1]
@@ -260,7 +260,7 @@ type merge_duplicates_funcs = {
     We return the updated context as well as the id of the new abstraction which
     results from the merge.
  *)
-val merge_into_abstraction :
+val merge_into_first_abstraction :
   Meta.span ->
   abs_kind ->
   bool ->
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';
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
diff --git a/compiler/InterpreterLoopsJoinCtxs.mli b/compiler/InterpreterLoopsJoinCtxs.mli
index f4b5194a..a194e25b 100644
--- a/compiler/InterpreterLoopsJoinCtxs.mli
+++ b/compiler/InterpreterLoopsJoinCtxs.mli
@@ -15,7 +15,7 @@ open InterpreterLoopsCore
     - [aid0]
     - [aid1]
  *)
-val merge_into_abstraction :
+val merge_into_first_abstraction :
   Meta.span ->
   loop_id ->
   abs_kind ->