summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-12-17 13:28:51 +0100
committerSon Ho2021-12-17 13:28:51 +0100
commit2e1903b951b496dd3f0bde08d9b5d524659a3bac (patch)
tree1e9933c5b979b021d6bb41dc0b9a5b4e31c9f555
parent4c498a62391624425b05b99197b40fd992626ed5 (diff)
Implement the avalue cases of give_back_value
Diffstat (limited to '')
-rw-r--r--src/Contexts.ml1
-rw-r--r--src/Interpreter.ml95
-rw-r--r--src/Print.ml2
-rw-r--r--src/Values.ml11
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 }