Add markers when creating new abstractions because of a join with bottom

3 files changed, 63 insertions, 48 deletions

diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index cd609ab0..8d6caac4 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -429,3 +429,47 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets =
     }
   in
   ids
+
+(* Small utility: Add a projection marker to a typed avalue.
+   This can be used in combination with List.map to add markers to an entire abstraction
+*)
+let add_marker_avalue (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker)
+    (av : typed_avalue) : typed_avalue =
+  let obj =
+    object
+      inherit [_] map_typed_avalue as super
+
+      method! visit_borrow_content _ _ =
+        craise __FILE__ __LINE__ span "Unexpected borrow"
+
+      method! visit_loan_content _ _ =
+        craise __FILE__ __LINE__ span "Unexpected loan"
+
+      method! visit_symbolic_value _ sv =
+        sanity_check __FILE__ __LINE__
+          (not (symbolic_value_has_borrows ctx sv))
+          span;
+        sv
+
+      method! visit_aloan_content env lc =
+        match lc with
+        | AMutLoan (pm0, bid, av) ->
+            sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+            super#visit_aloan_content env (AMutLoan (pm, bid, av))
+        | ASharedLoan (pm0, bids, av, child) ->
+            sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+            super#visit_aloan_content env (ASharedLoan (pm, bids, av, child))
+        | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
+
+      method! visit_aborrow_content env bc =
+        match bc with
+        | AMutBorrow (pm0, bid, av) ->
+            sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+            super#visit_aborrow_content env (AMutBorrow (pm, bid, av))
+        | ASharedBorrow (pm0, bid) ->
+            sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
+            super#visit_aborrow_content env (ASharedBorrow (pm, bid))
+        | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
+    end
+  in
+  obj#visit_typed_avalue () av
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 1e099d96..2f2dba41 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -664,58 +664,15 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
           craise __FILE__ __LINE__ span "Unreachable"
     in
 
-    (* Add a projection marker to a typed avalue *)
-    let add_marker_avalue (pm : proj_marker) (av : typed_avalue) : typed_avalue
-        =
-      let obj =
-        object
-          inherit [_] map_typed_avalue as super
-
-          method! visit_borrow_content _ _ =
-            craise __FILE__ __LINE__ span "Unexpected borrow"
-
-          method! visit_loan_content _ _ =
-            craise __FILE__ __LINE__ span "Unexpected loan"
-
-          method! visit_symbolic_value _ sv =
-            (* While ctx0 and ctx1 are different, we assume that the type info context is
-               the same in both. Hence, we can use ctx0's types wlog *)
-            sanity_check __FILE__ __LINE__
-              (not (symbolic_value_has_borrows ctx0 sv))
-              span;
-            sv
-
-          method! visit_aloan_content env lc =
-            match lc with
-            | AMutLoan (pm0, bid, av) ->
-                sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
-                super#visit_aloan_content env (AMutLoan (pm, bid, av))
-            | ASharedLoan (pm0, bids, av, child) ->
-                sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
-                super#visit_aloan_content env
-                  (ASharedLoan (pm, bids, av, child))
-            | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
-
-          method! visit_aborrow_content env bc =
-            match bc with
-            | AMutBorrow (pm0, bid, av) ->
-                sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
-                super#visit_aborrow_content env (AMutBorrow (pm, bid, av))
-            | ASharedBorrow (pm0, bid) ->
-                sanity_check __FILE__ __LINE__ (pm0 = PNone) span;
-                super#visit_aborrow_content env (ASharedBorrow (pm, bid))
-            | _ -> craise __FILE__ __LINE__ span "Unsupported yet"
-        end
-      in
-      obj#visit_typed_avalue () av
-    in
-
     (* Add projection marker to all abstractions in the left and right environments *)
     let add_marker (pm : proj_marker) (ee : env_elem) : env_elem =
       match ee with
       | EAbs abs ->
           EAbs
-            { abs with avalues = List.map (add_marker_avalue pm) abs.avalues }
+            {
+              abs with
+              avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues;
+            }
       | x -> x
     in
 
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 9b1d3dd0..713f462b 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -516,7 +516,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
-      let mk_aborrow (pm: proj_marker) (bid : borrow_id) : typed_avalue =
+      let mk_aborrow (pm : proj_marker) (bid : borrow_id) : typed_avalue =
         let value = ABorrow (ASharedBorrow (pm, bid)) in
         { value; ty = borrow_ty }
       in
@@ -832,6 +832,20 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
           convert_value_to_abstractions span abs_kind can_end
             destructure_shared_values ctx v
         in
+        (* Add a marker to the abstraction indicating the provenance of the value *)
+        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;
+              })
+            absl
+        in
         push_absl absl;
         (* Return [Bottom] *)
         mk_bottom span v.ty