summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml70
1 files changed, 55 insertions, 15 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 9f309e5e..dee5daf3 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -19,6 +19,13 @@ module L = Logging
(* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
(rather than only env) *)
+(* TODO: it would be good to find a "core", which implements the rules (like
+ "end_borrow") and on top of which we build more complex functions which
+ chose in which order to apply the rules, etc. This way we would make very
+ explicit where we need to insert sanity checks, what the preconditions are,
+ where invariants might be broken, etc.
+ *)
+
(** Some utilities *)
let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
@@ -799,14 +806,34 @@ and end_borrows_in_env (config : C.config) (io : inner_outer)
(** Same as [end_borrow_in_env], but operating on evaluation contexts *)
let end_borrow (config : C.config) (io : inner_outer) (l : V.BorrowId.id)
(ctx : C.eval_ctx) : C.eval_ctx =
+ L.log#ldebug
+ (lazy
+ ("end_borrow " ^ V.BorrowId.to_string l ^ ": context before:\n"
+ ^ eval_ctx_to_string ctx));
let env = end_borrow_in_env config io l ctx.env in
- { ctx with env }
+ let ctx = { ctx with env } in
+ L.log#ldebug
+ (lazy
+ ("end_borrow " ^ V.BorrowId.to_string l ^ ": context after:\n"
+ ^ eval_ctx_to_string ctx));
+ ctx
(** Same as [end_borrows_in_env], but operating on evaluation contexts *)
let end_borrows (config : C.config) (io : inner_outer) (lset : V.BorrowId.Set.t)
(ctx : C.eval_ctx) : C.eval_ctx =
+ L.log#ldebug
+ (lazy
+ ("end_borrows "
+ ^ V.BorrowId.set_to_string lset
+ ^ ": context before:\n" ^ eval_ctx_to_string ctx));
let env = end_borrows_in_env config io lset ctx.env in
- { ctx with env }
+ let ctx = { ctx with env } in
+ L.log#ldebug
+ (lazy
+ ("end_borrows "
+ ^ V.BorrowId.set_to_string lset
+ ^ ": context after:\n" ^ eval_ctx_to_string ctx));
+ ctx
let end_outer_borrow config = end_borrow config Outer
@@ -1447,10 +1474,23 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind)
ctx
with UpdateCtx ctx -> collect_borrows_at_place config access p ctx)
-(** Drop (end) all the borrows at a given place, which should be seen as
- an l-value (we will write to it later, but need to drop the borrows
+(** Drop (end) all the loans and borrows at a given place, which should be
+ seen as an l-value (we will write to it later, but need to drop the borrows
before writing).
+ We start by only dropping the borrows, then we end the loans. The reason
+ is that some loan we find may be borrowed by another part of the subvalue.
+ In order to correctly handle the "outer borrow" priority (we should end
+ the outer borrows first) which is not really applied here (we are preparing
+ the value for override: we can end the borrows inside, without ending the
+ borrows we traversed to actually access the value) we first end the borrows
+ we find in the place, to make sure all the "local" loans are taken care of.
+ Then, if we find a loan, it means it is "externally" borrowed (the associated
+ borrow is not in a subvalue of the place under inspection).
+ Also note that whenever we end a loan, we might propagate back a value inside
+ the place under inspection: we must re-end all the borrows we find there,
+ before reconsidering loans.
+
Repeat:
- read the value at a given place
- as long as we find a loan or a borrow, end it
@@ -1459,9 +1499,8 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind)
drop the value there to properly propagate back values which are not/can't
be borrowed anymore).
*)
-let rec drop_borrows_at_lplace (config : C.config) (p : E.place)
+let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
(ctx : C.eval_ctx) : C.eval_ctx =
- (* TODO: inner/outer + check drop_value *)
(* We do something similar to [collect_borrows_at_place].
First, retrieve the value *)
match read_place config Write p ctx with
@@ -1513,13 +1552,13 @@ let rec drop_borrows_at_lplace (config : C.config) (p : E.place)
| V.SharedBorrow bid | V.MutBorrow (bid, _) ->
L.log#ldebug
(lazy
- ("drop_borrows_at_lplace: dropping "
+ ("drop_borrows_loans_at_lplace: dropping "
^ V.BorrowId.to_string bid));
raise (UpdateCtx (end_inner_borrow config bid ctx))
| V.InactivatedMutBorrow bid ->
L.log#ldebug
(lazy
- ("drop_borrows_at_lplace: activating "
+ ("drop_borrows_loans_at_lplace: activating "
^ V.BorrowId.to_string bid));
(* We need to activate inactivated borrows - later, we will
* actually end it *)
@@ -1528,8 +1567,10 @@ let rec drop_borrows_at_lplace (config : C.config) (p : E.place)
in
raise (UpdateCtx ctx))
| V.Loan lc ->
- if (* If we can, end the loans, otherwise ignore *)
- end_loans then
+ if
+ (* If we can, end the loans, otherwise ignore: keep for later *)
+ end_loans
+ then
(* We need to end all loans. Note that as all the borrows inside
the value at place p should already have ended, the borrows
associated to the loans we find here should be borrows from
@@ -1556,7 +1597,7 @@ let rec drop_borrows_at_lplace (config : C.config) (p : E.place)
inspect_update true v;
(* No context update required: return the current context *)
ctx
- with UpdateCtx ctx -> drop_borrows_at_lplace config p ctx)
+ with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx)
(** Copy a value, and return the resulting value.
@@ -1926,10 +1967,8 @@ let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) :
(* TODO *)
let access = Write in
let ctx = update_ctx_along_write_place config access p ctx in
- (* End the loans *)
- let ctx = collect_borrows_at_place config access p ctx in
- (* End the borrows *)
- let ctx = drop_borrows_at_lplace config p ctx in
+ (* End the borrows and loans, starting with the borrows *)
+ let ctx = drop_borrows_loans_at_lplace config p ctx in
(* Read the value and check it *)
let v = read_place_unwrap config access p ctx in
(* Sanity checks *)
@@ -2003,6 +2042,7 @@ let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx =
(** Drop a value at a given place *)
let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx
=
+ L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
(* Prepare the place (by ending the loans, then the borrows) *)
let ctx, v = prepare_lplace config p ctx in
(* Replace the value with [Bottom] *)