Fix give_back_symbolic_value

2 files changed, 86 insertions, 24 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 19e5716f..cde799d8 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -429,19 +429,18 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     Otherwise, we give back the same symbolic value, to signify the fact that
     it was left unchanged.
   *)
-let give_back_symbolic_value (_config : C.config) (sv : V.symbolic_value)
+let give_back_symbolic_value (_config : C.config)
+    (proj_regions : T.RegionId.set_t) (proj_ty : T.rty) (sv : V.symbolic_value)
     (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
-  let subst local_regions =
+  let subst local_regions local_ty =
     let child_proj =
       if sv.sv_id = nsv.sv_id then None
       else
-        Some (mk_aproj_borrows_from_symbolic_value local_regions nsv sv.V.sv_ty)
+        Some (mk_aproj_borrows_from_symbolic_value local_regions nsv local_ty)
     in
     V.AEndedProjLoans child_proj
   in
-  (* TODO: we need to use the regions!! *)
-  raise Errors.Unimplemented;
-  substitute_aproj_loans_with_id sv subst ctx
+  update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
 
 (** Auxiliary function to end borrows. See [give_back].
 
@@ -1150,7 +1149,9 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
       in
       (* Give back a fresh symbolic value *)
       let nsv = mk_fresh_symbolic_value proj_ty in
-      let ctx = give_back_symbolic_value config sv nsv ctx in
+      let ctx =
+        give_back_symbolic_value config abs.regions proj_ty sv nsv ctx
+      in
       (* Reexplore *)
       end_abstraction_borrows config chain abs_id ctx
 
@@ -1195,7 +1196,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
        * it is completely absent) *)
       (* Update the loans depending on the current symbolic value - it is
        * left unchanged *)
-      give_back_symbolic_value config sv sv ctx
+      give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx
   | Some (SharedProjs projs) ->
       (* We found projectors over shared values - split between the projectors
            * which belong to the current *)
@@ -1222,7 +1223,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
         (* All the proj_borrows are owned: simply erase them *)
         let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in
         (* Remove the proj_loans - note that the symbolic value was left unchanged *)
-        give_back_symbolic_value config sv sv ctx
+        give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx
   | Some (NonSharedProj (abs_id', _proj_ty)) ->
       (* 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
@@ -1235,7 +1236,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
         in
         (* Replace the proj_loans - note that the loaned (symbolic) value
          * was left unchanged *)
-        give_back_symbolic_value config sv sv ctx
+        give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx
       else
         (* End the abstraction.
          * Don't retry ending the current proj_loans after ending the abstraction:
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 3c39e76b..6bc31d63 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -596,14 +596,6 @@ let proj_borrows_intersects_proj_loans
     projections_intersect l_sv.V.sv_ty l_regions b_ty b_regions
   else false
 
-let proj_loans_intersect (proj_loans : T.RegionId.Set.t * V.symbolic_value)
-    (proj_loans' : T.RegionId.Set.t * V.symbolic_value) : bool =
-  let regions, sv = proj_loans in
-  let regions', sv' = proj_loans' in
-  if same_symbolic_id sv sv' then
-    projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions'
-  else false
-
 (** Result of looking up aproj_borrows which intersect a given aproj_loans in
     the context.
 
@@ -825,14 +817,33 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
   update_intersecting_aproj_borrows can_update_shared update_shared
     update_non_shared regions sv ctx
 
-(** Substitute the proj_loans based an a symbolic id *)
-let substitute_aproj_loans_with_id (sv : V.symbolic_value)
-    (subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
+(** Updates the proj_loans intersecting some projection.
+
+    Note that in practice, when we update a proj_loans, we always update exactly
+    one aproj_loans, in a specific abstraction.
+    
+    We make this function more general, by checking projection intersections
+    (rather than simply checking the abstraction and symbolic value ids)
+    for sanity checking: we check whether we need to update a loan based
+    on intersection criteria, but also check at the same time that we update
+    *exactly one* projector.
+    
+    Note that the new value [nv] with which to replace the proj_loans could
+    be untyped: we request a typed value for sanity checking.
+    
+    [subst]: takes as parameters the projection regions and the projection type
+    where we perform the substitution.
+ *)
+let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
+    (proj_ty : T.rty) (sv : V.symbolic_value)
+    (subst : T.RegionId.Set.t -> T.rty -> V.aproj) (ctx : C.eval_ctx) :
+    C.eval_ctx =
   (* Small helpers for sanity checks *)
   let updated = ref false in
-  let update regions : V.aproj =
+  let update local_regions local_proj_ty : V.aproj =
+    assert (not !updated);
     updated := true;
-    subst regions
+    subst local_regions local_proj_ty
   in
   (* The visitor *)
   let obj =
@@ -848,7 +859,13 @@ let substitute_aproj_loans_with_id (sv : V.symbolic_value)
             super#visit_aproj abs sproj
         | AProjLoans sv' ->
             let abs = Option.get abs in
-            if same_symbolic_id sv sv' then update abs.regions
+            if same_symbolic_id sv sv' then (
+              assert (sv.sv_ty = sv'.sv_ty);
+              if
+                projections_intersect proj_ty proj_regions sv'.V.sv_ty
+                  abs.regions
+              then update abs.regions sv'.V.sv_ty
+              else super#visit_aproj (Some abs) sproj)
             else super#visit_aproj (Some abs) sproj
     end
   in
@@ -858,3 +875,47 @@ let substitute_aproj_loans_with_id (sv : V.symbolic_value)
   assert !updated;
   (* Return *)
   ctx
+
+(*
+let proj_loans_intersect (proj_loans : T.RegionId.Set.t * V.symbolic_value)
+    (proj_loans' : T.RegionId.Set.t * V.symbolic_value) : bool =
+  let regions, sv = proj_loans in
+  let regions', sv' = proj_loans' in
+  if same_symbolic_id sv sv' then
+    projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions'
+  else false
+
+*)
+(*(** Substitute the proj_loans based an a symbolic id *)
+  let substitute_aproj_loans_with_id (sv : V.symbolic_value)
+      (subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
+    (* Small helpers for sanity checks *)
+    let updated = ref false in
+    let update regions : V.aproj =
+      updated := true;
+      subst regions
+    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_aproj abs sproj =
+          match sproj with
+          | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows
+          | AIgnoredProjBorrows ->
+              super#visit_aproj abs sproj
+          | AProjLoans sv' ->
+              let abs = Option.get abs in
+              if same_symbolic_id sv sv' then update abs.regions
+              else super#visit_aproj (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 !updated;
+    (* Return *)
+  ctx*)