Introduce ended borrow/loan projectors over symbolic values

5 files changed, 57 insertions, 38 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index c471faf7..067b867e 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -976,7 +976,7 @@ and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id)
             super#visit_AEndedIgnoredMutLoan env given_back child
         | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av
 
-      method! visit_ASymbolic env sproj =
+      method! visit_ASymbolic _ sproj =
         match sproj with
         | V.AProjBorrows (_, _) -> ()
         | V.AProjLoans sv -> raise (FoundSymbolicValue sv)
@@ -1007,6 +1007,7 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
   (* Note that the abstraction mustn't contain any loans *)
   (* We end the borrows, starting with the *inner* ones. This is important
      when considering nested borrows which have the same lifetime.
+     TODO: is that really important?
 
      For instance:
      ```
@@ -1057,6 +1058,12 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
         | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
             (* Nothing to do for ignored borrows *)
             ()
+
+      method! visit_ASymbolic _ sproj =
+        match sproj with
+        | V.AProjLoans _ -> failwith "Unexpected"
+        | V.AProjBorrows (sv, proj_ty) ->
+            raise (FoundAProjBorrows (sv, proj_ty))
     end
   in
   (* Lookup the abstraction *)
@@ -1067,42 +1074,44 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
     (* No borrows: nothing to update *)
     ctx
   with
-  (* There are borrows: end them, then reexplore *)
+  (* There are concrete borrows: end them, then reexplore *)
   | FoundABorrowContent bc ->
-    (* First, replace the borrow by ⊥ *)
-    let bid =
-      match bc with
-      | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid
-      | V.AProjSharedBorrow asb -> (
-          (* There should be at least one borrow identifier in the set, which we
-           * can use to identify the whole set *)
-          match
-            List.find
-              (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
-              asb
-          with
-          | V.AsbBorrow bid -> bid
-          | _ -> failwith "Unexpected")
-      | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
-          failwith "Unexpected"
-    in
-    let ctx = update_aborrow ek_all bid V.ABottom ctx in
-    (* Then give back the value *)
-    let ctx =
-      match bc with
-      | V.AMutBorrow (bid, av) ->
-          (* First, convert the avalue to a (fresh symbolic) value *)
-          let v = convert_avalue_to_value av in
-          give_back_value config bid v ctx
-      | V.ASharedBorrow bid -> give_back_shared config bid ctx
-      | V.AProjSharedBorrow _ ->
-          (* Nothing to do *)
-          ctx
-      | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
-          failwith "Unexpected"
-    in
-    (* Reexplore *)
-    end_abstraction_borrows config abs_id ctx
+      (* First, replace the borrow by ⊥ *)
+      let bid =
+        match bc with
+        | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid
+        | V.AProjSharedBorrow asb -> (
+            (* There should be at least one borrow identifier in the set, which we
+             * can use to identify the whole set *)
+            match
+              List.find
+                (fun x -> match x with V.AsbBorrow _ -> true | _ -> false)
+                asb
+            with
+            | V.AsbBorrow bid -> bid
+            | _ -> failwith "Unexpected")
+        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+            failwith "Unexpected"
+      in
+      let ctx = update_aborrow ek_all bid V.ABottom ctx in
+      (* Then give back the value *)
+      let ctx =
+        match bc with
+        | V.AMutBorrow (bid, av) ->
+            (* First, convert the avalue to a (fresh symbolic) value *)
+            let v = convert_avalue_to_value av in
+            give_back_value config bid v ctx
+        | V.ASharedBorrow bid -> give_back_shared config bid ctx
+        | V.AProjSharedBorrow _ ->
+            (* Nothing to do *)
+            ctx
+        | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ ->
+            failwith "Unexpected"
+      in
+      (* Reexplore *)
+      end_abstraction_borrows config abs_id ctx
+  (* There are symbolic borrows: end them, then reexplore *)
+  | FoundAProjBorrows (_sv, _proj_ty) -> raise Errors.Unimplemented
 
 (** Remove an abstraction from the context, as well as all its references *)
 and end_abstraction_remove_from_context (_config : C.config)
@@ -1133,8 +1142,8 @@ and end_abstraction_remove_from_context (_config : C.config)
         intersecting proj_borrows, either in the concrete context or in an
         abstraction
 *)
-and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id)
-    (regions : T.RegionId.set_t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
+and end_proj_loans_symbolic (_config : C.config) (_abs_id : V.AbstractionId.id)
+    (_regions : T.RegionId.set_t) (_sv : V.symbolic_value) (_ctx : C.eval_ctx) :
     C.eval_ctx =
   raise Errors.Unimplemented
 
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index e19f8bb4..18ec1ecc 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -75,6 +75,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
         let proj_regions = current_abs.regions in
         let ancestors_regions = current_abs.ancestors_regions in
         match (aproj, proj_kind) with
+        | (V.AEndedProjLoans | V.AEndedProjBorrows), _ -> V.ASymbolic aproj
         | V.AProjLoans sv, LoanProj ->
             (* Check if this is the symbolic value we are looking for *)
             if same_symbolic_id sv original_sv then
@@ -311,6 +312,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
             match reborrow_ashared (Option.get proj_regions) sv proj_ty with
             | None -> super#visit_ASymbolic proj_regions aproj
             | Some asb -> V.ABorrow (V.AProjSharedBorrow asb))
+        | AEndedProjLoans | AEndedProjBorrows -> V.ASymbolic aproj
     end
   in
   (* Call the visitor *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index ce6bd0ce..9b272db8 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -133,6 +133,9 @@ exception FoundGLoanContent of g_loan_content
 exception FoundSymbolicValue of V.symbolic_value
 (** Utility exception *)
 
+exception FoundAProjBorrows of V.symbolic_value * T.rty
+(** Utility exception *)
+
 let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     bool =
   let obj =
@@ -146,6 +149,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
         match aproj with
         | AProjLoans sv | AProjBorrows (sv, _) ->
             if sv.V.sv_id = sv_id then raise Found else ()
+        | AEndedProjLoans | AEndedProjBorrows -> ()
 
       method! visit_abstract_shared_borrows _ asb =
         let visit (asb : V.abstract_shared_borrow) : unit =
diff --git a/src/Print.ml b/src/Print.ml
index bc527acc..3869012a 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -315,6 +315,8 @@ module Values = struct
         ^ ")"
     | AProjBorrows (sv, rty) ->
         "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"
+    | AEndedProjLoans -> "ended_proj_loans"
+    | AEndedProjBorrows -> "ended_proj_borrows"
 
   let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) :
       string =
diff --git a/src/Values.ml b/src/Values.ml
index e8d4560e..41d8bd85 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -186,6 +186,8 @@ type aproj =
   | AProjBorrows of symbolic_value * rty
       (** Note that an AProjBorrows only operates on a value which is not below
           a shared loan: under a shared loan, we use [abstract_shared_borrow]. *)
+  | AEndedProjLoans
+  | AEndedProjBorrows
 [@@deriving show]
 
 type region = RegionVarId.id Types.region [@@deriving show]