Implement the avalue cases of give_back_value

4 files changed, 95 insertions, 14 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index cf8817f7..0dc18952 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -191,7 +191,6 @@ class ['self] iter_frame =
   object (self : 'self)
     inherit [_] V.iter_abs
 
-    (* TODO: remove "env_elem" from the name *)
     method visit_Var : 'acc -> binder -> typed_value -> unit =
       fun acc vid v -> self#visit_typed_value acc v
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 929f2df5..2282c724 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -577,6 +577,10 @@ type outer_borrows_or_abs =
 exception FoundOuter of outer_borrows_or_abs
 (** Utility exception *)
 
+let apply_proj_borrows (regions : V.RegionId.set_t) (v : V.typed_value)
+    (ty : T.rty) : V.typed_avalue =
+  raise Unimplemented
+
 (** Auxiliary function to end borrows: lookup a borrow in the environment,
     update it (by returning an updated environment where the borrow has been
     replaced by [Bottom])) if we can end the borrow (for instance, it is not
@@ -822,28 +826,97 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     replaced := true
   in
   let obj =
-    object
+    object (self)
       inherit [_] C.map_env as super
 
-      method! visit_Loan elem lc =
+      method! visit_Loan opt_abs lc =
         match lc with
         | V.SharedLoan (bids, v) ->
             (* We are giving back a value (i.e., the content of a *mutable*
              * borrow): nothing special to do *)
-            V.Loan (super#visit_SharedLoan elem bids v)
+            V.Loan (super#visit_SharedLoan opt_abs bids v)
         | V.MutLoan bid' ->
             (* Check if this is the loan we are looking for *)
             if bid' = bid then (
               set_replaced ();
               nv.V.value)
-            else V.Loan (super#visit_MutLoan elem bid')
-
-      method! visit_ALoan elem lc = raise Unimplemented
-
-      method! visit_env_elem elem em =
-        assert (Option.is_none elem);
-        let elem = Some em in
-        super#visit_env_elem elem em
+            else V.Loan (super#visit_MutLoan opt_abs bid')
+
+      method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
+          =
+        match av.V.value with
+        | V.ALoan lc ->
+            let value = self#visit_typed_ALoan opt_abs av.V.ty lc in
+            ({ av with V.value } : V.typed_avalue)
+        | _ -> super#visit_typed_avalue opt_abs av
+      (** This is a bit annoying, but as we need the type of the avalue we
+          are exploring, in order to be able to project the value we give
+          back, we need to reimplement [visit_typed_avalue] instead of
+          [visit_ALoan] *)
+
+      method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
+          (lc : V.aloan_content) : V.avalue =
+        (* Preparing a bit *)
+        let regions =
+          match opt_abs with
+          | None -> failwith "Unreachable"
+          | Some abs -> abs.V.regions
+        in
+        match lc with
+        | V.AMutLoan (bid', child) ->
+            if bid' = bid then (
+              (* This is the loan we are looking for: apply the projection to
+               * the value we give back and replaced this mutable loan with
+               * an ended loan *)
+              (* Register the insertion *)
+              set_replaced ();
+              (* Apply the projection *)
+              let given_back = apply_proj_borrows regions nv ty in
+              (* Explore the child - not necessary, but consistent to do (allows
+               * to check the invariants at the same time) *)
+              let child = self#visit_typed_avalue opt_abs child in
+              (* Return the new value *)
+              V.ALoan (V.AEndedMutLoan { given_back; child }))
+            else
+              (* Continue exploring *)
+              V.ALoan (super#visit_AMutLoan opt_abs bid' child)
+        | V.ASharedLoan (bids, v, av) ->
+            (* We are giving back a value to a *mutable* loan: nothing special to do *)
+            V.ALoan (super#visit_ASharedLoan opt_abs bids v av)
+        | V.AEndedMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child)
+        | V.AEndedSharedLoan (v, av) ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedSharedLoan opt_abs v av)
+        | V.AIgnoredMutLoan (bid', child) ->
+            (* This loan is ignored, but we may have to project on a subvalue
+             * of the value which is given back *)
+            if bid' = bid then
+              (* Note that we replace the ignored mut loan by an *ended* ignored
+               * mut loan. Also, this is not the loan we are looking for *per se*:
+               * we don't register the fact that we inserted the value somewhere
+               * (i.e., we don't call [set_replaced]) *)
+              let given_back = apply_proj_borrows regions nv ty in
+              (* We explore the child - not necessary, but consistent *)
+              let child = self#visit_typed_avalue opt_abs child in
+              V.ALoan (V.AEndedIgnoredMutLoan { given_back; child })
+            else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child)
+        | V.AEndedIgnoredMutLoan { given_back; child } ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child)
+        | V.AIgnoredSharedLoan asb ->
+            (* Nothing special to do *)
+            V.ALoan (super#visit_AIgnoredSharedLoan opt_abs asb)
+      (** We are not specializing an already existing method, but adding a
+          new method (for projections, we need type information) *)
+
+      method! visit_Abs opt_abs abs =
+        (* We remember in which abstraction we are before diving -
+         * this is necessary for projecting values: we need to know
+         * over which regions to project *)
+        assert (Option.is_none opt_abs);
+        super#visit_Abs (Some abs) abs
     end
   in
 
diff --git a/src/Print.ml b/src/Print.ml
index e8471704..e9ba4730 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -361,7 +361,7 @@ module Values = struct
         ^ ")"
     | AEndedMutLoan ml ->
         "@ended_mut_loan{ given_back="
-        ^ typed_value_to_string fmt ml.given_back
+        ^ typed_avalue_to_string fmt ml.given_back
         ^ "; child="
         ^ typed_avalue_to_string fmt ml.child
         ^ " }"
diff --git a/src/Values.ml b/src/Values.ml
index e0b0b59d..09cf8aa6 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -227,7 +227,16 @@ and adt_avalue = {
 and aloan_content =
   | AMutLoan of (BorrowId.id[@opaque]) * typed_avalue
   | ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue
-  | AEndedMutLoan of { given_back : typed_value; child : typed_avalue }
+  | AEndedMutLoan of { given_back : typed_avalue; child : typed_avalue }
+      (** TODO: in the formalization, given_back was initially a typed value
+       (not an avalue). It seems more consistent to use a value, especially
+       because then the invariants about the borrows are simpler (otherwise,
+       there may be borrow ids duplicated in the context, which is very
+       annoying).
+       I think the original idea was that using values would make it
+       simple to instantiate the backward function (because projecting
+       deconstructs a bit the values with which we feed the function).
+    *)
   | AEndedSharedLoan of typed_value * typed_avalue
   | AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue
   | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }