Make more fixes

2 files changed, 222 insertions, 86 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index bb843714..eb3b9898 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1748,9 +1748,8 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
   let push_abs (r_id : T.RegionId.id) (avalues : V.typed_avalue list) : unit =
     if avalues = [] then ()
     else
-      (* Reverse the list of avalues *)
-      let avalues = List.rev avalues in
-      (* Create the abs *)
+      (* Create the abs - note that we keep the order of the avalues as it is
+         (unlike the environments) *)
       let abs =
         {
           V.abs_id = C.fresh_abstraction_id ();
@@ -2121,6 +2120,11 @@ type merge_duplicates_funcs = {
 let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
     (merge_funs : merge_duplicates_funcs option) (ctx : C.eval_ctx)
     (abs0 : V.abs) (abs1 : V.abs) : V.abs =
+  log#ldebug
+    (lazy
+      ("merge_abstractions_aux:\n- abs0:\n" ^ abs_to_string ctx abs0
+     ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1));
+
   (* Check that the abstractions are destructured *)
   if !Config.check_invariants then (
     let destructure_shared_values = true in
@@ -2277,48 +2281,67 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
         raise (Failure "Unreachable")
   in
 
-  let borrows_loans = List.append borrows_loans0 borrows_loans1 in
-  (* Iterate over all the borrows/loans ids found in teh abstractions *)
+  (* Note that we first explore the borrows/loans of [abs1], because we
+     want to merge *into* this abstraction, and as a consequence we want to
+     preserve its structure as much as we can *)
+  let borrows_loans = List.append borrows_loans1 borrows_loans0 in
+  (* Iterate over all the borrows/loans ids found in the abstractions *)
   List.iter
     (fun bl ->
       match bl with
-      | BorrowId bid -> (
-          (* Check if the borrow has already been merged *)
-          assert (not (borrow_is_merged bid));
-          set_borrow_as_merged bid;
-          (* Check if we need to filter it *)
-          match filter_bid bid with
-          | None -> ()
-          | Some bid ->
-              (* Lookup the contents *)
-              let bc0 = V.BorrowId.Map.find_opt bid borrow_to_content0 in
-              let bc1 = V.BorrowId.Map.find_opt bid borrow_to_content1 in
-              (* Merge *)
-              let av : V.typed_avalue =
-                match (bc0, bc1) with
-                | None, Some bc | Some bc, None -> (
-                    match bc with
-                    | Concrete (_, _) ->
-                        (* This can happen only in case of nested borrows -
-                           a concrete borrow can only happen inside a shared
-                           loan
-                        *)
-                        raise (Failure "Unreachable")
-                    | Abstract (ty, bc) -> { V.value = V.ABorrow bc; ty })
-                | Some bc0, Some bc1 ->
-                    assert (merge_funs <> None);
-                    merge_g_borrow_contents bc0 bc1
-                | None, None -> raise (Failure "Unreachable")
-              in
-              push_avalue av)
-      | LoanId bid -> (
+      | BorrowId bid ->
+          log#ldebug
+            (lazy
+              ("merge_abstractions_aux: merging borrow "
+             ^ V.BorrowId.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*
+             all the borrows/loans in [abs1], and there may be duplicates
+             between the two *)
+          if borrow_is_merged bid then ()
+          else (
+            set_borrow_as_merged bid;
+            (* Check if we need to filter it *)
+            match filter_bid bid with
+            | None -> ()
+            | Some bid ->
+                (* Lookup the contents *)
+                let bc0 = V.BorrowId.Map.find_opt bid borrow_to_content0 in
+                let bc1 = V.BorrowId.Map.find_opt bid borrow_to_content1 in
+                (* Merge *)
+                let av : V.typed_avalue =
+                  match (bc0, bc1) with
+                  | None, Some bc | Some bc, None -> (
+                      match bc with
+                      | Concrete (_, _) ->
+                          (* This can happen only in case of nested borrows -
+                             a concrete borrow can only happen inside a shared
+                             loan
+                          *)
+                          raise (Failure "Unreachable")
+                      | Abstract (ty, bc) -> { V.value = V.ABorrow bc; ty })
+                  | Some bc0, Some bc1 ->
+                      assert (merge_funs <> None);
+                      merge_g_borrow_contents bc0 bc1
+                  | None, None -> raise (Failure "Unreachable")
+                in
+                push_avalue av)
+      | LoanId bid ->
           if
             (* Check if the loan has already been treated - it can happen
-               because shared loans contain sets of borrows.
+               for the same reason as for borrows, and also because shared
+               loans contain sets of borrows (meaning that when taking care
+               of one loan, we can merge several other loans at once).
             *)
             loan_is_merged bid
           then ()
-          else
+          else (
+            log#ldebug
+              (lazy
+                ("merge_abstractions_aux: merging loan "
+               ^ V.BorrowId.to_string bid));
+
             (* Check if we need to filter it *)
             match filter_bid bid with
             | None -> ()
@@ -2359,8 +2382,9 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool)
                 push_avalue av))
     borrows_loans;
 
-  (* Note that we *don't* reverse the avalues *)
-  let avalues = !avalues in
+  (* 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
 
   (* Filter the regions *)
 
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 2fc474fc..70a5f1bf 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -237,9 +237,7 @@ let collapse_ctx (loop_id : V.LoopId.id)
   log#ldebug
     (lazy
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
-     ^ "\n\n- ctx0:\n"
-      ^ eval_ctx_to_string_no_filter ctx0
-      ^ "\n\n"));
+     ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n"));
 
   let abs_kind = V.Loop loop_id in
   let can_end = false in
@@ -250,9 +248,8 @@ let collapse_ctx (loop_id : V.LoopId.id)
   let is_fresh_did (id : C.DummyVarId.id) : bool =
     not (C.DummyVarId.Set.mem id old_ids.dids)
   in
-  (* Convert the dummy values to abstractions, and destructure all the new
-     abstractions at the same time (note that when we convert values to
-     abstractions, the resulting abstraction should be destructured) *)
+  (* 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 =
@@ -271,6 +268,12 @@ let collapse_ctx (loop_id : V.LoopId.id)
                else [ ee ])
          ctx0.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 { ctx0 with env }
+      ^ "\n\n"));
 
   (* Explore all the *new* abstractions, and compute various maps *)
   let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in
@@ -591,17 +594,20 @@ module Match (M : Matcher) = struct
         let bc =
           match (bc0, bc1) with
           | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
-              (* Not completely sure what to do with the meta-value. If a shared
-                 symbolic value gets expanded in a branch, it may be simplified
-                 (by being folded back to a symbolic value) upon doing the join,
-                 which as a result would lead to code where it is considered as
-                 mutable (which is sound). On the other hand, if we access a
-                 symbolic value in a loop, the translated loop should take it as
-                 input anyway, so maybe this actually leads to equivalent
-                 code.
+              (* Not completely sure what to do with the meta-value, as we use
+                 it for the translation. TODO: remove meta-values from shared borrows?
+
+                 If a shared symbolic value gets expanded in a branch, it may be
+                 simplified (by being folded back to a symbolic value) upon
+                 doing the join, which as a result would lead to code where it
+                 is considered as mutable (which is sound). On the other hand,
+                 if we access a symbolic value in a loop, the translated loop
+                 should take it as input anyway, so maybe this actually leads to
+                 equivalent code.
               *)
+              assert (not (value_has_borrows ctx mv0.V.value));
+              assert (not (value_has_borrows ctx mv1.V.value));
               let mv = match_rec mv0 mv1 in
-              assert (not (value_has_borrows ctx mv.V.value));
               let mv, bid = M.match_shared_borrows ty mv bid0 bid1 in
               V.SharedBorrow (mv, bid)
           | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
@@ -672,6 +678,13 @@ module Match (M : Matcher) = struct
    *)
   and match_typed_avalues (ctx : C.eval_ctx) (v0 : V.typed_avalue)
       (v1 : V.typed_avalue) : V.typed_avalue =
+    log#ldebug
+      (lazy
+        ("match_typed_avalues:\n- value0: "
+        ^ typed_avalue_to_string ctx v0
+        ^ "\n- value1: "
+        ^ typed_avalue_to_string ctx v1));
+
     let match_rec = match_typed_values ctx in
     let match_arec = match_typed_avalues ctx in
     let ty = M.match_rtys v0.V.ty v1.V.ty in
@@ -691,14 +704,19 @@ module Match (M : Matcher) = struct
           { V.value; ty }
         else (* Merge *)
           M.match_distinct_aadts v0.V.ty av0 v1.V.ty av1 ty
-    | ABottom, ABottom -> v0
+    | ABottom, ABottom -> mk_abottom ty
+    | AIgnored, AIgnored -> mk_aignored ty
     | ABorrow bc0, ABorrow bc1 -> (
         match (bc0, bc1) with
         | ASharedBorrow bid0, ASharedBorrow bid1 ->
             M.match_ashared_borrows v0.V.ty bid0 v1.V.ty bid1 ty
         | AMutBorrow (mv0, bid0, av0), AMutBorrow (mv1, bid1, av1) ->
-            (* Not sure what to do with the meta-value *)
-            let mv = match_rec mv0 mv1 in
+            (* The meta-value should be the value consumed by the abstracion.
+               This only makes sense if the abstraction was introduced because
+               of a function call (we use it for the translation).
+               TODO: make it optional?
+            *)
+            let mv = mk_bottom mv0.V.ty in
             let av = match_arec av0 av1 in
             M.match_amut_borrows v0.V.ty mv0 bid0 av0 v1.V.ty mv1 bid1 av1 ty mv
               av
@@ -1051,8 +1069,34 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
   end in
   let module JM = MakeJoinMatcher (S) in
   let module M = Match (JM) in
-  let merge_amut_borrows _ _ _ _ _ _ _ = raise (Failure "Unexpected") in
-  let merge_ashared_borrows _ _ _ = raise (Failure "Unexpected") in
+  (* TODO: why not simply call: M.match_type_avalues? (or move this code to
+     MakeJoinMatcher?) *)
+  let merge_amut_borrows id ty0 (mv0 : V.typed_value) child0 _ty1
+      (mv1 : V.typed_value) child1 =
+    (* Sanity checks *)
+    assert (is_aignored child0.V.value);
+    assert (is_aignored child1.V.value);
+    assert (mv0.V.ty = mv1.V.ty);
+
+    (* Same remarks as for [merge_amut_loans] *)
+    let ty = ty0 in
+    let child = child0 in
+    let mv = mk_bottom mv0.ty in
+    let value = V.ABorrow (V.AMutBorrow (mv, id, child)) in
+    { V.value; ty }
+  in
+
+  let merge_ashared_borrows id ty0 ty1 =
+    (* Sanity checks *)
+    assert (not (ty_has_borrows ctx.type_context.type_infos ty0));
+    assert (not (ty_has_borrows ctx.type_context.type_infos ty1));
+
+    (* Same remarks as for [merge_amut_loans] *)
+    let ty = ty0 in
+    let value = V.ABorrow (V.ASharedBorrow id) in
+    { V.value; ty }
+  in
+
   let merge_amut_loans id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
     assert (is_aignored child0.V.value);
@@ -1327,6 +1371,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
 
 (* Very annoying: functors only take modules as inputs... *)
 module type MatchCheckEquivState = sig
+  val ctx : C.eval_ctx
   val rid_map : T.RegionId.InjSubst.t ref
   val bid_map : V.BorrowId.InjSubst.t ref
   val sid_map : V.SymbolicValueId.InjSubst.t ref
@@ -1474,7 +1519,14 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
     let value = V.ALoan (V.AMutLoan (id, av)) in
     { V.value; ty }
 
-  let match_avalues _ _ = raise Distinct
+  let match_avalues v0 v1 =
+    log#ldebug
+      (lazy
+        ("avalues don't match:\n- v0: "
+        ^ typed_avalue_to_string S.ctx v0
+        ^ "\n- v1: "
+        ^ typed_avalue_to_string S.ctx v1));
+    raise Distinct
 end
 
 (** Compute whether two contexts are equivalent modulo an identifier substitution.
@@ -1524,6 +1576,7 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
   in
 
   let module S : MatchCheckEquivState = struct
+    let ctx = ctx0
     let rid_map = rid_map
     let bid_map = bid_map
     let sid_map = sid_map
@@ -1585,6 +1638,8 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
     let _ = CEM.match_aidl original_parents0 original_parents1 in
     let _ = CEM.match_rids regions0 regions1 in
     let _ = CEM.match_rids ancestors_regions0 ancestors_regions1 in
+
+    log#ldebug (lazy "match_abstractions: matching values");
     let _ =
       List.map
         (fun (v0, v1) -> M.match_typed_avalues ctx v0 v1)
@@ -1598,7 +1653,15 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
     log#ldebug
       (lazy
         ("ctxs_are_equivalent: match_envs:\n\n- fixed_ids:\n"
-       ^ show_ids_sets fixed_ids ^ "\n\n- ctx0:\n"
+       ^ show_ids_sets fixed_ids ^ "\n\n- rid_map: "
+        ^ T.RegionId.InjSubst.show_t !rid_map
+        ^ "\n- bid_map: "
+        ^ V.BorrowId.InjSubst.show_t !bid_map
+        ^ "\n- sid_map: "
+        ^ V.SymbolicValueId.InjSubst.show_t !sid_map
+        ^ "\n- aid_map: "
+        ^ V.AbstractionId.InjSubst.show_t !aid_map
+        ^ "\n\n- ctx0:\n"
         ^ eval_ctx_to_string_no_filter { ctx0 with env = List.rev env0 }
         ^ "\n\n- ctx1:\n"
         ^ eval_ctx_to_string_no_filter { ctx1 with env = List.rev env1 }
@@ -1608,8 +1671,8 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
     | ( C.Var (C.DummyBinder b0, v0) :: env0',
         C.Var (C.DummyBinder b1, v1) :: env1' ) ->
         (* Two cases: the dummy value is an old value, in which case the bindings
-           must be the same and we must join their values. Otherwise, it means we
-           are not in the prefix *)
+           must be the same and their values equal (and the borrows/loans/symbolic
+           values they reference must be fixed) *)
         if C.DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Fixed values: the values must be equal *)
           assert (b0 = b1);
@@ -1648,7 +1711,7 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
         (* Done *)
         ()
     | _ ->
-        (* The elements don't match: we are not in the prefix anymore *)
+        (* The elements don't match *)
         raise Distinct
   in
 
@@ -1677,21 +1740,8 @@ let ctxs_are_equivalent (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
     we return those updated environments, and the joined environment.
  *)
 let loop_join_origin_with_continue_ctxs (config : C.config)
-    (loop_id : V.LoopId.id) (old_ctx : C.eval_ctx) (ctxl : C.eval_ctx list) :
-    (C.eval_ctx * C.eval_ctx list) * C.eval_ctx =
-  (* # Look for borrows and abstractions that exist in [old_ctx] and not in [ctxl]:
-   * we need to end those *)
-  (* Compute the sets of borrows and abstractions *)
-  let old_ids = compute_context_ids old_ctx in
-  let new_ids = compute_contexts_ids ctxl in
-  let bids = V.BorrowId.Set.diff old_ids.bids new_ids.bids in
-  let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in
-  (* End those borrows and abstractions *)
-  let old_ctx = InterpreterBorrows.end_borrows_no_synth config bids old_ctx in
-  let old_ctx =
-    InterpreterBorrows.end_abstractions_no_synth config aids old_ctx
-  in
-
+    (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (old_ctx : C.eval_ctx)
+    (ctxl : C.eval_ctx list) : (C.eval_ctx * C.eval_ctx list) * C.eval_ctx =
   (* # Join with the new contexts, one by one
 
      For every context, we repeteadly attempt to join it with the current
@@ -1702,7 +1752,7 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
   *)
   let joined_ctx = ref old_ctx in
   let rec join_one_aux (ctx : C.eval_ctx) : C.eval_ctx =
-    match join_ctxs loop_id old_ids !joined_ctx ctx with
+    match join_ctxs loop_id fixed_ids !joined_ctx ctx with
     | Ok nctx ->
         joined_ctx := nctx;
         ctx
@@ -1719,16 +1769,41 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
         join_one_aux ctx
   in
   let join_one (ctx : C.eval_ctx) : C.eval_ctx =
+    log#ldebug
+      (lazy
+        ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
+       ^ eval_ctx_to_string ctx));
+
     (* Destructure the abstractions introduced in the new context *)
-    let ctx = destructure_new_abs loop_id old_ids.aids ctx in
+    let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in
+    log#ldebug
+      (lazy
+        ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n"
+       ^ eval_ctx_to_string ctx));
+
     (* Collapse the context we want to add to the join *)
-    let ctx = collapse_ctx loop_id None old_ids ctx in
+    let ctx = collapse_ctx loop_id None fixed_ids ctx in
+    log#ldebug
+      (lazy
+        ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
+       ^ eval_ctx_to_string ctx));
+
     (* Join the two contexts  *)
     let ctx1 = join_one_aux ctx in
+    log#ldebug
+      (lazy
+        ("loop_join_origin_with_continue_ctxs:join_one: after join:\n"
+       ^ eval_ctx_to_string ctx1));
+
     (* Collapse again - the join might have introduce abstractions we want
        to merge with the others (note that those abstractions may actually
        lead to borrows/loans duplications) *)
-    joined_ctx := collapse_ctx_with_merge loop_id old_ids !joined_ctx;
+    joined_ctx := collapse_ctx_with_merge loop_id fixed_ids !joined_ctx;
+    log#ldebug
+      (lazy
+        ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n"
+        ^ eval_ctx_to_string !joined_ctx));
+
     (* Sanity check *)
     if !Config.check_invariants then Invariants.check_invariants !joined_ctx;
     (* Return *)
@@ -1765,10 +1840,39 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
         (* We don't support nested loops for now *)
         raise (Failure "Nested loops are not supported for now")
   in
+
+  (* The fixed ids. They are the ids of the original ctx, after we ended
+     the borrows/loans which end during the first loop iteration (we do
+     one loop iteration, then set it to [Some].
+  *)
+  let fixed_ids = ref None in
+
   (* Join the contexts at the loop entry *)
   let join_ctxs (ctx0 : C.eval_ctx) : C.eval_ctx =
+    (* If this is the first iteration, end the borrows/loans/abs which
+       appear in ctx0 and not in the other contexts, then compute the
+       set of fixed ids. This means those borrows/loans have to end
+       in the loop, and we rather end them *before* the loop. *)
+    let ctx0 =
+      match !fixed_ids with
+      | Some _ -> ctx0
+      | None ->
+          let old_ids = compute_context_ids ctx0 in
+          let new_ids = compute_contexts_ids !ctxs in
+          let bids = V.BorrowId.Set.diff old_ids.bids new_ids.bids in
+          let aids = V.AbstractionId.Set.diff old_ids.aids new_ids.aids in
+          (* End those borrows and abstractions *)
+          let ctx0 = InterpreterBorrows.end_borrows_no_synth config bids ctx0 in
+          let ctx0 =
+            InterpreterBorrows.end_abstractions_no_synth config aids ctx0
+          in
+          fixed_ids := Some (compute_context_ids ctx0);
+          ctx0
+    in
+
+    let fixed_ids = Option.get !fixed_ids in
     let (ctx0', _), ctx1 =
-      loop_join_origin_with_continue_ctxs config loop_id ctx0 !ctxs
+      loop_join_origin_with_continue_ctxs config loop_id fixed_ids ctx0 !ctxs
     in
     ctxs := [];
     if !ctx_upon_entry = None then ctx_upon_entry := Some ctx0';
@@ -1777,9 +1881,17 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
   (* Check if two contexts are equivalent - modulo alpha conversion on the
      existentially quantified borrows/abstractions/symbolic values *)
   let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool =
+    (* Compute the set of fixed ids - for the symbolic ids, we compute the
+       intersection of ids between the original environment and [ctx1]
+       and [ctx2] *)
     let fixed_ids = compute_context_ids (Option.get !ctx_upon_entry) in
-    let { aids; bids; dids; rids; sids = _ } = fixed_ids in
-    let sids = V.SymbolicValueId.Set.empty in
+    let { aids; bids; dids; rids; sids } = fixed_ids in
+    let fixed_ids1 = compute_context_ids ctx1 in
+    let fixed_ids2 = compute_context_ids ctx2 in
+    let sids =
+      V.SymbolicValueId.Set.inter sids
+        (V.SymbolicValueId.Set.inter fixed_ids1.sids fixed_ids2.sids)
+    in
     let fixed_ids = { aids; bids; dids; rids; sids } in
     ctxs_are_equivalent fixed_ids ctx1 ctx2
   in