Make good progress on end_proj_loans_symbolic

4 files changed, 175 insertions, 5 deletions

diff --git a/TODO.md b/TODO.md
index 37cfe986..808d5dec 100644
--- a/TODO.md
+++ b/TODO.md
@@ -7,6 +7,8 @@
   (but always disallow borrow overwrites on returned values)
   at the level of abstractions (not at the level of loans!)
 
+* check that no borrow_overwrites upon ending abstractions
+
 * set of types with mutable borrows (what to do when type variables appear under
   shared borrows?)
   necessary to know what to return.
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index d8c2f3a8..64e82edd 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -421,6 +421,11 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
+(** TODO: *)
+let give_back_symbolic_value (_config : C.config) (_regions : T.RegionId.set_t)
+    (_sv : V.symbolic_value) (_ctx : C.eval_ctx) : C.eval_ctx =
+  raise Errors.Unimplemented
+
 (** Auxiliary function to end borrows. See [give_back].
 
     This function is similar to [give_back_value] but gives back an [avalue]
@@ -1130,8 +1135,8 @@ and end_abstraction_remove_from_context (_config : C.config)
   let env = List.filter_map map_env_elem ctx.C.env in
   { ctx with C.env }
 
-(** End the proj_borrows which intersect a given proj_loans over a symbolic
-    value.
+(** End a proj_loan over a symbolic value by ending the proj_borrows which
+    intersect this proj_loans.
     
     Rk.:
     - if this symbolic value is primitively copiable, then:
@@ -1144,10 +1149,27 @@ 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
+  (* Find the first proj_borrows which intersects the proj_loans *)
+  let explore_shared = true in
+  match
+    lookup_first_intersecting_aproj_borrows_opt explore_shared regions sv ctx
+  with
+  | None ->
+      (* We couldn't find any in the context: it means that the symbolic value
+       * is in the concrete environment (or that we dropped it, in which case
+       * it is completely absent) *)
+      (* Update the loans depending on the current symbolic value - it is
+       * left unchanged *)
+      give_back_symbolic_value config regions sv ctx
+  | Some (abs_id', proj_ty, mutable_proj) ->
+      (* We found one in the context: if it comes from this abstraction, we can
+       * end it directly, otherwise we need to end the abstraction where it
+       * came from first *)
+      if abs_id' = abs_id then raise Errors.Unimplemented
+      else raise Errors.Unimplemented
 
 and end_outer_borrow config = end_borrow config None
 
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index e34a5383..68b24380 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -7,6 +7,7 @@ module V = Values
 module C = Contexts
 module Subst = Substitute
 module L = Logging
+open Utils
 open TypesUtils
 open InterpreterUtils
 
@@ -557,3 +558,147 @@ let get_first_outer_loan_or_borrow_in_value (with_borrows : bool)
   with
   | FoundLoanContent lc -> Some (LoanContent lc)
   | FoundBorrowContent bc -> Some (BorrowContent bc)
+
+type gproj_borrows =
+  | AProjBorrows of V.AbstractionId.id * V.symbolic_value
+  | ProjBorrows of V.symbolic_value
+
+let proj_borrows_intersects_proj_loans
+    (proj_borrows : T.RegionId.Set.t * V.symbolic_value * T.rty)
+    (proj_loans : T.RegionId.Set.t * V.symbolic_value) : bool =
+  let b_regions, b_sv, b_ty = proj_borrows in
+  let l_regions, l_sv = proj_loans in
+  if same_symbolic_id b_sv l_sv then
+    projections_intersect l_sv.V.sv_ty l_regions b_ty b_regions
+  else false
+
+(** Lookup the first aproj_borrows (including aproj_shared_borrows) over a
+    symbolic value which intersects a given set of regions.
+    
+    Note that there should be **at most one** (one reason is that we force
+    the expansion of primitively copyable values before giving them to
+    abstractions).
+    
+    Returns the id of the owning abstraction, the projection type used in
+    this abstraction and a boolean indicating whether the projector is
+    over a mutable value (`true` is "mutable", `false` is "shared").
+    
+    [explore_shared]: if `true` also explore projectors over shared values,
+    otherwise ignore.
+*)
+let lookup_first_intersecting_aproj_borrows_opt (explore_shared : bool)
+    (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
+    (V.AbstractionId.id * T.rty * bool) option =
+  let found = ref None in
+  let set r =
+    assert (Option.is_none !found);
+    found := Some r
+  in
+  let check_proj_borrows_and_raise abs sv' proj_ty =
+    if
+      proj_borrows_intersects_proj_loans
+        (abs.V.regions, sv', proj_ty)
+        (regions, sv)
+    then (
+      let is_mut = false in
+      set (abs.abs_id, proj_ty, is_mut);
+      raise Found)
+    else ()
+  in
+  let obj =
+    object
+      inherit [_] C.iter_eval_ctx as super
+
+      method! visit_abs _ abs = super#visit_abs (Some abs) abs
+
+      method! visit_abstract_shared_borrows abs asb =
+        if explore_shared then
+          let abs = Option.get abs in
+          let check asb =
+            match asb with
+            | V.AsbBorrow _ -> ()
+            | V.AsbProjReborrows (sv', proj_ty) ->
+                check_proj_borrows_and_raise abs sv' proj_ty
+          in
+          List.iter check asb
+        else ()
+
+      method! visit_ASymbolic abs sproj =
+        let abs = Option.get abs in
+        match sproj with
+        | AProjLoans _ | AEndedProjLoans | AEndedProjBorrows -> ()
+        | AProjBorrows (sv', proj_rty) ->
+            check_proj_borrows_and_raise abs sv' proj_rty
+    end
+  in
+  (* We use exceptions *)
+  try
+    obj#visit_eval_ctx None ctx;
+    None
+  with Found ->
+    (* Return - while checking that the result is indeed `Some ...` *)
+    let res = Option.get !found in
+    Some res
+
+(** Lookup the aproj_borrows (not aproj_borrows_shared!) over a symbolic
+    value which intersects a given set of regions.
+    
+    Note that there should be **at most one** (one reason is that we force
+    the expansion of primitively copyable values before giving them to
+    abstractions).
+    
+    Returns the id of the owning abstraction, and the projection type used in
+    this abstraction.
+*)
+let lookup_intersecting_aproj_borrows_not_shared_opt
+    (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
+    (V.AbstractionId.id * T.rty) option =
+  let explore_shared = false in
+  match
+    lookup_first_intersecting_aproj_borrows_opt explore_shared regions sv ctx
+  with
+  | None -> None
+  | Some (abs_id, rty, is_mut) ->
+      assert is_mut;
+      Some (abs_id, rty)
+
+(** Similar to [lookup_intersecting_aproj_borrows_not_shared_opt], but updates the
+    value.
+ *)
+let update_intersecting_aproj_borrows_not_shared (regions : T.RegionId.Set.t)
+    (sv : V.symbolic_value) (nv : V.typed_avalue) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* Small helpers to make sure we update the context exactly once *)
+  let found = ref false in
+  let set () : V.avalue =
+    assert (not !found);
+    found := true;
+    nv.V.value
+  in
+  (* The visitor *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_abs _ abs = super#visit_abs (Some abs) abs
+
+      method! visit_ASymbolic abs sproj =
+        match sproj with
+        | AProjLoans _ | AEndedProjLoans | AEndedProjBorrows ->
+            super#visit_ASymbolic abs sproj
+        | AProjBorrows (sv', proj_rty) ->
+            let abs = Option.get abs in
+            if
+              proj_borrows_intersects_proj_loans
+                (abs.regions, sv', proj_rty)
+                (regions, sv)
+            then set ()
+            else super#visit_ASymbolic (Some abs) sproj
+    end
+  in
+  (* Apply *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Check that we updated the context at least once *)
+  assert !found;
+  (* Return *)
+  ctx
diff --git a/src/Values.ml b/src/Values.ml
index 9d25025e..50bec658 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -188,6 +188,7 @@ type aproj =
           a shared loan: under a shared loan, we use [abstract_shared_borrow]. *)
   | AEndedProjLoans
   | AEndedProjBorrows
+(* TODO: remove AEndedProjBorrows? *)
 [@@deriving show]
 
 type region = RegionVarId.id Types.region [@@deriving show]