Factorize some code in InterpreterBorrows*

2 files changed, 77 insertions, 49 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 1905cf79..f5f3a8fa 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1058,54 +1058,17 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
  fun cf ctx ->
   (* Lookup the abstraction *)
   let abs = C.ctx_lookup_abs ctx abs_id in
-  (* End the first loan we find *)
-  let obj =
-    object
-      inherit [_] V.iter_abs as super
-
-      method! visit_aloan_content env lc =
-        match lc with
-        | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
-        | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
-        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
-        | V.AEndedSharedLoan (_, _) ->
-            super#visit_aloan_content env lc
-        | V.AIgnoredMutLoan (_, _) ->
-            (* Note that this loan can't come from a parent abstraction, because
-             * we should have ended them already) *)
-            super#visit_aloan_content env lc
-        | V.AEndedIgnoredMutLoan
-            { given_back = _; child = _; given_back_meta = _ }
-        | V.AIgnoredSharedLoan _ ->
-            super#visit_aloan_content env lc
-
-      method! visit_loan_content _ lc =
-        match lc with
-        | V.MutLoan _ ->
-            (* The mut loan linked to the mutable borrow present in a shared
-             * value in an abstraction should be in an AProjBorrows *)
-            failwith "Unreachable"
-        | V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
-      (** We may need to visit loan contents because of shared values *)
-
-      method! visit_aproj env sproj =
-        (match sproj with
-        | V.AProjBorrows (_, _)
-        | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
-            ()
-        | V.AProjLoans (sv, _) -> raise (FoundSymbolicValue sv));
-        super#visit_aproj env sproj
-    end
-  in
-  try
-    (* Check if there are loans *)
-    obj#visit_abs () abs;
-    (* No loans: nothing to update *)
-    cf ctx
-  with
-  (* There are loans: end them, then recheck *)
-  | FoundBorrowIds bids ->
-      (* End the corresponding borrows *)
+  (* End the first loan we find.
+   *
+   * We ignore the "ignored mut/shared loans": as we should have already ended
+   * the parent abstractions, they necessarily come from children. *)
+  let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in
+  match opt_loan with
+  | None ->
+      (* No loans: nothing to update *)
+      cf ctx
+  | Some (BorrowIds bids) ->
+      (* There are loans: end the corresponding borrows, then recheck *)
       let cc : cm_fun =
         match bids with
         | Borrow bid -> end_borrow config chain None bid
@@ -1115,7 +1078,7 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
       let cc = comp cc (end_abstraction_loans config chain abs_id) in
       (* Continue *)
       cc cf ctx
-  | FoundSymbolicValue sv ->
+  | Some (SymbolicValue sv) ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
        * which intersect this proj_loans, then end the proj_loans itself *)
       let cc = end_proj_loans_symbolic config chain abs_id abs.regions sv in
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index d1c60941..d47989c3 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -43,6 +43,11 @@ type priority_borrows_or_abs =
   | InnerLoans of borrow_ids
 [@@deriving show]
 
+type borrow_ids_or_symbolic_value =
+  | BorrowIds of borrow_ids
+  | SymbolicValue of V.symbolic_value
+[@@deriving show]
+
 let update_if_none opt x = match opt with None -> Some x | _ -> opt
 
 exception FoundPriority of priority_borrows_or_abs
@@ -1119,3 +1124,63 @@ let no_aproj_over_symbolic_in_context (sv : V.symbolic_value) (ctx : C.eval_ctx)
   (* Apply *)
   try obj#visit_eval_ctx () ctx
   with Found -> failwith "update_aproj_loans_to_ended: failed"
+
+(** Helper function
+
+    Return the loan (aloan, loan, proj_loans over a symbolic value) we find
+    in an abstraction, if there is.
+    
+    **Remark:** we don't take the *ignored* mut/shared loans into account.
+ *)
+let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) :
+    borrow_ids_or_symbolic_value option =
+  (* Explore to find a loan *)
+  let obj =
+    object
+      inherit [_] V.iter_abs as super
+
+      method! visit_aloan_content env lc =
+        match lc with
+        | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid))
+        | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids))
+        | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedLoan (_, _) ->
+            super#visit_aloan_content env lc
+        | V.AIgnoredMutLoan (_, _) ->
+            (* Ignore *)
+            super#visit_aloan_content env lc
+        | V.AEndedIgnoredMutLoan
+            { given_back = _; child = _; given_back_meta = _ }
+        | V.AIgnoredSharedLoan _ ->
+            (* Ignore *)
+            super#visit_aloan_content env lc
+
+      method! visit_loan_content _ lc =
+        match lc with
+        | V.MutLoan _ ->
+            (* The mut loan linked to the mutable borrow present in a shared
+             * value in an abstraction should be in an AProjBorrows *)
+            failwith "Unreachable"
+        | V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
+      (** We may need to visit loan contents because of shared values *)
+
+      method! visit_aproj env sproj =
+        (match sproj with
+        | V.AProjBorrows (_, _)
+        | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
+            ()
+        | V.AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv));
+        super#visit_aproj env sproj
+    end
+  in
+  try
+    (* Check if there are loans *)
+    obj#visit_abs () abs;
+    (* No loans *)
+    None
+  with
+  (* There are loans *)
+  | FoundBorrowIds bids -> Some (BorrowIds bids)
+  | ValuesUtils.FoundSymbolicValue sv ->
+      (* There are loan projections over symbolic values *)
+      Some (SymbolicValue sv)