Merge pull request #228 from AeneasVerif/son/loops2

Add support for projection markers when joining environments

1 files changed, 44 insertions, 22 deletions

diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 2628b26a..0469d58e 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -255,13 +255,17 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
           (because there are no use cases requiring finer control) *)
       method! visit_aloan_content env lc =
         match lc with
-        | AMutLoan (bid, av) ->
+        | AMutLoan (pm, bid, av) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGLoanContent (Abstract lc))
-            else super#visit_AMutLoan env bid av
-        | ASharedLoan (bids, v, av) ->
+            else super#visit_AMutLoan env pm bid av
+        | ASharedLoan (pm, bids, v, av) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if BorrowId.Set.mem l bids then
               raise (FoundGLoanContent (Abstract lc))
-            else super#visit_ASharedLoan env bids v av
+            else super#visit_ASharedLoan env pm bids v av
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _)
         | AIgnoredMutLoan (_, _)
@@ -396,11 +400,15 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
 
       method! visit_aloan_content env lc =
         match lc with
-        | AMutLoan (bid, av) ->
-            if bid = l then update () else super#visit_AMutLoan env bid av
-        | ASharedLoan (bids, v, av) ->
+        | AMutLoan (pm, bid, av) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
+            if bid = l then update () else super#visit_AMutLoan env pm bid av
+        | ASharedLoan (pm, bids, v, av) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if BorrowId.Set.mem l bids then update ()
-            else super#visit_ASharedLoan env bids v av
+            else super#visit_ASharedLoan env pm bids v av
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _)
         | AIgnoredMutLoan (_, _)
@@ -422,8 +430,8 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
   ctx
 
 (** Lookup a borrow content from a borrow id. *)
-let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
-    : g_borrow_content option =
+let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind)
+    (l : BorrowId.id) (ctx : eval_ctx) : g_borrow_content option =
   let obj =
     object
       inherit [_] iter_eval_ctx as super
@@ -453,12 +461,16 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
 
       method! visit_aborrow_content env bc =
         match bc with
-        | AMutBorrow (bid, av) ->
+        | AMutBorrow (pm, bid, av) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
-            else super#visit_AMutBorrow env bid av
-        | ASharedBorrow bid ->
+            else super#visit_AMutBorrow env pm bid av
+        | ASharedBorrow (pm, bid) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then raise (FoundGBorrowContent (Abstract bc))
-            else super#visit_ASharedBorrow env bid
+            else super#visit_ASharedBorrow env pm bid
         | AIgnoredMutBorrow (_, _)
         | AEndedMutBorrow _
         | AEndedIgnoredMutBorrow
@@ -486,7 +498,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx)
 *)
 let lookup_borrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
     (ctx : eval_ctx) : g_borrow_content =
-  match lookup_borrow_opt ek l ctx with
+  match lookup_borrow_opt span ek l ctx with
   | None -> craise __FILE__ __LINE__ span "Unreachable"
   | Some lc -> lc
 
@@ -571,12 +583,16 @@ let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id)
 
       method! visit_ABorrow env bc =
         match bc with
-        | AMutBorrow (bid, av) ->
+        | AMutBorrow (pm, bid, av) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then update ()
-            else ABorrow (super#visit_AMutBorrow env bid av)
-        | ASharedBorrow bid ->
+            else ABorrow (super#visit_AMutBorrow env pm bid av)
+        | ASharedBorrow (pm, bid) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
             if bid = l then update ()
-            else ABorrow (super#visit_ASharedBorrow env bid)
+            else ABorrow (super#visit_ASharedBorrow env pm bid)
         | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow
         | AEndedIgnoredMutBorrow _ ->
             super#visit_ABorrow env bc
@@ -1182,8 +1198,14 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) :
 
       method! visit_aloan_content env lc =
         match lc with
-        | AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
-        | ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
+        | AMutLoan (pm, bid, _) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
+            raise (FoundBorrowIds (Borrow bid))
+        | ASharedLoan (pm, bids, _, _) ->
+            (* Sanity check: projection markers can only appear when we're doing a join *)
+            sanity_check __FILE__ __LINE__ (pm = PNone) span;
+            raise (FoundBorrowIds (Borrows bids))
         | AEndedMutLoan { given_back = _; child = _; given_back_span = _ }
         | AEndedSharedLoan (_, _) ->
             super#visit_aloan_content env lc
@@ -1232,7 +1254,7 @@ let lookup_shared_value_opt (span : Meta.span) (ctx : eval_ctx)
   | None -> None
   | Some (_, lc) -> (
       match lc with
-      | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) ->
+      | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, _, sv, _)) ->
           Some sv
       | _ -> None)