Update end_abstraction_regions

1 files changed, 54 insertions, 1 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 71475ee5..17dd14a4 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2000,9 +2000,62 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
     (* Reexplore *)
     end_abstraction_borrows config abs_id ctx
 
+(** Update the symbolic values in a context to register the regions in the
+    abstraction we are ending as already ended.
+    Note that this function also checks that no symbolic value in an abstraction
+    contains regions which we are ending.
+    Of course, we ignore the abstraction we are currently ending...
+ *)
 and end_abstraction_regions (config : C.config) (abs_id : V.AbstractionId.id)
     (ctx : C.eval_ctx) : C.eval_ctx =
-  raise Unimplemented
+  (* Lookup the abstraction to retrieve the set of owned regions *)
+  let abs = C.ctx_lookup_abs ctx abs_id in
+  let ended_regions = abs.V.regions in
+  (* Update all the symbolic values in the context *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Symbolic _ sproj =
+        let sproj =
+          {
+            sproj with
+            V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions;
+          }
+        in
+        V.Symbolic sproj
+
+      method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj =
+        (* Sanity check *)
+        (match aproj with
+        | V.AProjLoans _ -> ()
+        | V.AProjBorrows (sv, ty) -> (
+            match abs_regions with
+            | None -> failwith "Unexpected"
+            | Some abs_regions ->
+                assert (
+                  not
+                    (projections_intersect sv.V.sv_ty ended_regions ty
+                       abs_regions))));
+        (* Return - nothing to update *)
+        aproj
+
+      method! visit_abs (regions : T.RegionId.set_t option) abs =
+        if abs.V.abs_id = abs_id then abs
+        else (
+          assert (Option.is_none regions);
+          (* Check that we don't project over already ended regions *)
+          assert (T.RegionId.Set.disjoint ended_regions abs.V.regions);
+          (* Remember the set of regions owned by the abstraction *)
+          let regions = Some abs.V.regions in
+          super#visit_abs regions abs)
+      (** Whenever we dive in an abstraction, we need to keep track of the
+          set of regions owned by the abstraction.
+          Also: we don't dive in the abstraction we are currently ending... *)
+    end
+  in
+  (* Update the context *)
+  obj#visit_eval_ctx None ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
 and end_abstraction_remove_from_context (_config : C.config)