Cleanup a bit

4 files changed, 87 insertions, 91 deletions

diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 8d6caac4..4149b19e 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -26,21 +26,21 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result
 (** Union Find *)
 module UF = UnionFind.Make (UnionFind.StoreMap)
 
-(** A small utility -
-
-    Rem.: some environments may be ill-formed (they may contain several times
-    the same loan or borrow - this happens for instance when merging
-    environments). This is the reason why we use sets in some places (for
-    instance, [borrow_to_abs] maps to a *set* of ids).
+(** A small utility.
+
+    Remark: we use projection markers, meaning we compute maps from/to
+    pairs of (projection marker, borrow/loan id). This allows us to use
+    this utility during a reduce phase (when we simplify the environment
+    and all markers should be [PNone]) as well as during a collapse (where
+    we actually have markers because we performed a join and are progressively
+    transforming the environment to get rid of those markers).
 *)
 type abs_borrows_loans_maps = {
   abs_ids : AbstractionId.id list;
   abs_to_borrows : MarkerBorrowId.Set.t AbstractionId.Map.t;
   abs_to_loans : MarkerBorrowId.Set.t AbstractionId.Map.t;
-  abs_to_borrows_loans : MarkerBorrowId.Set.t AbstractionId.Map.t;
   borrow_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t;
   loan_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t;
-  borrow_loan_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t;
 }
 
 (** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher].
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
 
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 713f462b..bc39d5ec 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -20,32 +20,28 @@ module S = SynthesizeSymbolic
 (** The local logger *)
 let log = Logging.loops_match_ctxs_log
 
-let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
-    (explore : abs -> bool) (env : env) : abs_borrows_loans_maps =
+let compute_abs_borrows_loans_maps (span : Meta.span) (explore : abs -> bool)
+    (env : env) : abs_borrows_loans_maps =
   let abs_ids = ref [] in
   let abs_to_borrows = ref AbstractionId.Map.empty in
   let abs_to_loans = ref AbstractionId.Map.empty in
-  let abs_to_borrows_loans = ref AbstractionId.Map.empty in
   let borrow_to_abs = ref MarkerBorrowId.Map.empty in
   let loan_to_abs = ref MarkerBorrowId.Map.empty in
-  let borrow_loan_to_abs = ref MarkerBorrowId.Map.empty in
 
   let module R (M : Collections.Map) (S : Collections.Set) = struct
     (*
        [check_singleton_sets]: check that the mapping maps to a singleton.
-       [check_not_already_registered]: check if the mapping was not already registered.
+       We need this because to tweak the behavior of the sanity checks because
+       of the following cases:
+       - when computing the map from borrow ids (with marker) to the region
+         abstractions they belong to, the marked borrow ids can map to a single
+         region abstraction, i.e., to a singleton set of region abstraction ids
+       - however, when computing the mapping from region abstractions to
+         the borrow ids they contain, this time we do map abstraction ids
+         to sets which can compute strictly more than one value
     *)
-    let register_mapping (check_singleton_sets : bool)
-        (check_not_already_registered : bool) (map : S.t M.t ref) (id0 : M.key)
-        (id1 : S.elt) : unit =
-      (* Sanity check *)
-      (if check_singleton_sets || check_not_already_registered then
-         match M.find_opt id0 !map with
-         | None -> ()
-         | Some set ->
-             sanity_check __FILE__ __LINE__
-               ((not check_not_already_registered) || not (S.mem id1 set))
-               span);
+    let register_mapping (check_singleton_sets : bool) (map : S.t M.t ref)
+        (id0 : M.key) (id1 : S.elt) : unit =
       (* Update the mapping *)
       map :=
         M.update id0
@@ -53,11 +49,11 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
             match ids with
             | None -> Some (S.singleton id1)
             | Some ids ->
-                (* Sanity check *)
+                (* Check that we are allowed to map id0 to a set which is not
+                   a singleton *)
                 sanity_check __FILE__ __LINE__ (not check_singleton_sets) span;
-                sanity_check __FILE__ __LINE__
-                  ((not check_not_already_registered) || not (S.mem id1 ids))
-                  span;
+                (* Check that the mapping was not already registered *)
+                sanity_check __FILE__ __LINE__ (not (S.mem id1 ids)) span;
                 (* Update *)
                 Some (S.add id1 ids))
           !map
@@ -65,20 +61,13 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
   let module RAbsBorrow = R (AbstractionId.Map) (MarkerBorrowId.Set) in
   let module RBorrowAbs = R (MarkerBorrowId.Map) (AbstractionId.Set) in
   let register_borrow_id abs_id pm bid =
-    RAbsBorrow.register_mapping false no_duplicates abs_to_borrows abs_id
-      (pm, bid);
-    RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id (pm, bid);
-    RBorrowAbs.register_mapping no_duplicates no_duplicates borrow_to_abs
-      (pm, bid) abs_id;
-    RBorrowAbs.register_mapping false false borrow_loan_to_abs (pm, bid) abs_id
+    RAbsBorrow.register_mapping false abs_to_borrows abs_id (pm, bid);
+    RBorrowAbs.register_mapping true borrow_to_abs (pm, bid) abs_id
   in
 
   let register_loan_id abs_id pm bid =
-    RAbsBorrow.register_mapping false no_duplicates abs_to_loans abs_id (pm, bid);
-    RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id (pm, bid);
-    RBorrowAbs.register_mapping no_duplicates no_duplicates loan_to_abs
-      (pm, bid) abs_id;
-    RBorrowAbs.register_mapping false false borrow_loan_to_abs (pm, bid) abs_id
+    RAbsBorrow.register_mapping false abs_to_loans abs_id (pm, bid);
+    RBorrowAbs.register_mapping true loan_to_abs (pm, bid) abs_id
   in
 
   let explore_abs =
@@ -87,10 +76,19 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
 
       (** Make sure we don't register the ignored ids *)
       method! visit_aloan_content (abs_id, pm) lc =
+        sanity_check __FILE__ __LINE__ (pm = PNone) span;
         match lc with
-        | AMutLoan (pm, _, _) | ASharedLoan (pm, _, _, _) ->
-            (* Process those normally *)
-            super#visit_aloan_content (abs_id, pm) lc
+        | AMutLoan (npm, lid, child) ->
+            (* Add the current marker when visiting the loan id *)
+            self#visit_loan_id (abs_id, npm) lid;
+            (* Recurse with the old marker *)
+            super#visit_typed_avalue (abs_id, pm) child
+        | ASharedLoan (npm, lids, sv, child) ->
+            (* Add the current marker when visiting the loan ids and the shared value *)
+            self#visit_loan_id_set (abs_id, npm) lids;
+            self#visit_typed_value (abs_id, npm) sv;
+            (* Recurse with the old marker *)
+            self#visit_typed_avalue (abs_id, pm) child
         | AIgnoredMutLoan (_, child)
         | AEndedIgnoredMutLoan { child; given_back = _; given_back_span = _ }
         | AIgnoredSharedLoan child ->
@@ -102,10 +100,16 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
 
       (** Make sure we don't register the ignored ids *)
       method! visit_aborrow_content (abs_id, pm) bc =
+        sanity_check __FILE__ __LINE__ (pm = PNone) span;
         match bc with
-        | AMutBorrow (pm, _, _) | ASharedBorrow (pm, _) ->
-            (* Add the current marker, and process them recursively *)
-            super#visit_aborrow_content (abs_id, pm) bc
+        | AMutBorrow (npm, bid, child) ->
+            (* Add the current marker when visiting the borrow id *)
+            self#visit_borrow_id (abs_id, npm) bid;
+            (* Recurse with the old marker *)
+            self#visit_typed_avalue (abs_id, pm) child
+        | ASharedBorrow (npm, bid) ->
+            (* Add the current marker when visiting the borrow id *)
+            self#visit_borrow_id (abs_id, npm) bid
         | AProjSharedBorrow _ ->
             sanity_check __FILE__ __LINE__ (pm = PNone) span;
             (* Process those normally *)
@@ -147,10 +151,8 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool)
     abs_ids = !abs_ids;
     abs_to_borrows = !abs_to_borrows;
     abs_to_loans = !abs_to_loans;
-    abs_to_borrows_loans = !abs_to_borrows_loans;
     borrow_to_abs = !borrow_to_abs;
     loan_to_abs = !loan_to_abs;
-    borrow_loan_to_abs = !borrow_loan_to_abs;
   }
 
 (** Match two types during a join.
@@ -557,7 +559,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
          an abstraction:
 
          {[
-           { MB bid0, ML nbid }  // where nbid fresh
+           { MB bid0, ML bid' }  // where bid' fresh
          ]}
 
          and we use bid' for the borrow id that we return.
@@ -565,7 +567,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
          We do this because we want to make sure that, whenever a mutably
          borrowed value is modified in a loop iteration, then there is
          a fresh abstraction between this borrowed value and the fixed
-         abstractions.
+         abstractions (this is tantamount to introducing a reborrow).
 
          Example:
          ========
@@ -596,6 +598,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
          to say [unit]) while the backward loop function gives back a new value
          for [v] (i.e., a new symbolic value which will replace [s0]).
 
+         By introducing the fresh region abstraction wet get:
+         {[
+           abs'0 { ML l0 } // input abstraction
+           abs'1 { MB l0, ML l1 } // fresh abstraction
+           v -> MB l1 s1
+           i -> 0
+         ]}
+
+
          In the future, we will also compute joins at the *loop exits*: when we
          do so, we won't introduce reborrows like above: the forward loop function
          will update [v], while the backward loop function will return nothing.
@@ -613,7 +624,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
         let kind = RMut in
         let bv_ty = bv.ty in
-        sanity_check __FILE__ __LINE__ (ty_no_regions bv_ty) span;
+        cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span
+          "Nested borrows are not supported yet";
         let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
         let borrow_av =
@@ -651,9 +663,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
         (nbid, bv))
     else
       (* We replace bid0 and bid1 with a fresh borrow id, and introduce
-         an abstraction which links all of them:
+         an abstraction which links all of them. This time we have to introduce
+         markers:
          {[
-           { MB bid0, MB bid1, ML bid2 }
+           { |MB bid0|, ︙MB bid1︙, ML bid2 }
          ]}
       *)
       let rid = fresh_region_id () in
@@ -761,24 +774,16 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     (* Check that:
        - there are no borrows in the symbolic value
        - there are no borrows in the "regular" value
-       If there are loans in the regular value, raise an exception.
     *)
     let type_infos = ctx0.type_ctx.type_infos in
-    cassert __FILE__ __LINE__
+    sanity_check __FILE__ __LINE__
       (not (ty_has_borrows type_infos sv.sv_ty))
-      span
-      "Check that:\n\
-      \    - there are no borrows in the symbolic value\n\
-      \    - there are no borrows in the \"regular\" value\n\
-      \    If there are loans in the regular value, raise an exception.";
-    cassert __FILE__ __LINE__
+      span;
+    sanity_check __FILE__ __LINE__
       (not (ValuesUtils.value_has_borrows type_infos v.value))
-      span
-      "Check that:\n\
-      \    - there are no borrows in the symbolic value\n\
-      \    - there are no borrows in the \"regular\" value\n\
-      \    If there are loans in the regular value, raise an exception.";
+      span;
     let value_is_left = not left in
+    (* If there are loans in the regular value, raise an exception. *)
     (match InterpreterBorrowsCore.get_first_loan_in_value v with
     | None -> ()
     | Some (VSharedLoan (ids, _)) ->
@@ -798,13 +803,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     then mk_bottom span sv.sv_ty
     else mk_fresh_symbolic_typed_value span sv.sv_ty
 
-  let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
-      (v : typed_value) : typed_value =
+  let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+      (bottom_is_left : bool) (v : typed_value) : typed_value =
+    let value_is_left = not bottom_is_left in
     (* If there are outer loans in the non-bottom value, raise an exception.
        Otherwise, convert it to an abstraction and return [Bottom].
     *)
     let with_borrows = false in
-    let value_is_left = not left in
     match
       InterpreterBorrowsCore.get_first_outer_loan_or_borrow_in_value
         with_borrows v
@@ -821,8 +826,6 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
             if value_is_left then raise (ValueMatchFailure (LoanInLeft id))
             else raise (ValueMatchFailure (LoanInRight id)))
     | None ->
-        (*   *)
-
         (* Convert the value to an abstraction *)
         let abs_kind : abs_kind = Loop (S.loop_id, None, LoopSynthInput) in
         let can_end = true in
@@ -833,16 +836,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
             destructure_shared_values ctx v
         in
         (* Add a marker to the abstraction indicating the provenance of the value *)
+        let pm = if value_is_left then PLeft else PRight in
         let absl =
           List.map
             (fun abs ->
               {
                 abs with
-                avalues =
-                  List.map
-                    (add_marker_avalue span ctx0
-                       (if value_is_left then PLeft else PRight))
-                    abs.avalues;
+                avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues;
               })
             absl
         in
@@ -1246,6 +1246,8 @@ struct
 
   let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _ty1 pm1
       bid1 ty =
+    (* We are checking whether that two environments are equivalent:
+       there shouldn't be any projection markers *)
     sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     let bid = match_borrow_id bid0 bid1 in
     let value = ABorrow (ASharedBorrow (PNone, bid)) in
@@ -1253,6 +1255,8 @@ struct
 
   let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _av0 _ty1
       pm1 bid1 _av1 ty av =
+    (* We are checking whether that two environments are equivalent:
+       there shouldn't be any projection markers *)
     sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     let bid = match_borrow_id bid0 bid1 in
     let value = ABorrow (AMutBorrow (PNone, bid, av)) in
@@ -1260,6 +1264,8 @@ struct
 
   let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 ids0 _v0 _av0
       _ty1 pm1 ids1 _v1 _av1 ty v av =
+    (* We are checking whether that two environments are equivalent:
+       there shouldn't be any projection markers *)
     sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     let bids = match_loan_ids ids0 ids1 in
     let value = ALoan (ASharedLoan (PNone, bids, v, av)) in
@@ -1267,6 +1273,8 @@ struct
 
   let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0 id0 _av0
       _ty1 pm1 id1 _av1 ty av =
+    (* We are checking whether that two environments are equivalent:
+       there shouldn't be any projection markers *)
     sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span;
     log#ldebug
       (lazy
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 7d214cb6..cd807358 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -13,13 +13,11 @@ open InterpreterLoopsCore
 (** Compute various maps linking the abstractions and the borrows/loans they contain.
 
     Parameters:
-    - [no_duplicates]: checks that borrows/loans are not referenced more than once
-      (see the documentation for {!type:InterpreterLoopsCore.abs_borrows_loans_maps}).
     - [explore]: this function is used to filter abstractions.
     - [env]
  *)
 val compute_abs_borrows_loans_maps :
-  Meta.span -> bool -> (abs -> bool) -> env -> abs_borrows_loans_maps
+  Meta.span -> (abs -> bool) -> env -> abs_borrows_loans_maps
 
 (** Generic functor to implement matching functions between values, environments,
     etc.