diff options
| -rw-r--r-- | src/Interpreter.ml | 70 |
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] *) |