summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-08 14:58:15 +0100
committerSon Ho2021-12-08 14:58:15 +0100
commit688a4e589f46892448be902b7b5467c7198627bf (patch)
tree6e3764c98de42a73ce23f526ac49faa3e4c7dd6f /src
parente70af1f2f080ceb7a79d64ee14176f5dc334b4d2 (diff)
Reimplement drop_borrows_loans_at_place
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml232
1 files changed, 155 insertions, 77 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 7a193c0d..2b6193a4 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1398,86 +1398,74 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
*)
let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
(ctx : C.eval_ctx) : C.eval_ctx =
+ (* Iterator to explore a value and update the context whenever we find
+ borrows/loans.
+ We use exceptions to make it handy: whenever we update the
+ context, we raise an exception wrapping the updated context.
+
+ Note that we can end the borrows which are inside the value (while the
+ value itself might be inside a borrow/loan: we are thus ending inner
+ borrows). Because a loan inside the value may be linked to a borrow
+ somewhere else *also inside* the value (it's possible with adts),
+ we first end all the borrows we find - by using [Inner] to allow
+ ending inner borrows - then end all the loans we find. It is really
+ important to do this in two steps: the borrow linked to a loan may
+ be inside the value at place p, in which case this borrow may be
+ an inner borrow that we *can* end, but it may also be outside this
+ value, in which case we need to end all the outer borrows first...
+ Also, whenever the context is updated, we need to re-inspect
+ the value at place p *in two steps* again (end borrows, then end
+ loans).
+ *)
+ let obj =
+ object
+ inherit [_] V.iter_typed_value as super
+
+ method! visit_borrow_content end_loans bc =
+ (* Sanity check: we should have ended all the borrows before starting
+ to end loans *)
+ assert (not end_loans);
+
+ (* We need to end all borrows. Note that we ignore the outer borrows
+ when ending the borrows we find here (we call [end_inner_borrow(s)]:
+ the value at place p might be below a borrow/loan). Note however
+ that if we restrain ourselves at the value at place p, the borrow we
+ found here can be considered as an outer borrow.
+ *)
+ match bc with
+ | V.SharedBorrow bid | V.MutBorrow (bid, _) ->
+ raise (UpdateCtx (end_inner_borrow config bid ctx))
+ | V.InactivatedMutBorrow bid ->
+ (* We need to activate ithe nactivated borrow - later, we will
+ * actually end it - Rk.: we could actually end it straight away
+ * (this is not really important) *)
+ let ctx = activate_inactivated_mut_borrow config Inner bid ctx in
+ raise (UpdateCtx ctx)
+
+ method! visit_loan_content end_loans lc =
+ 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
+ outside this value: we need to call [end_outer_borrow(s)]
+ (we can't ignore outer borrows this time).
+ *)
+ match lc with
+ | V.SharedLoan (bids, _) ->
+ raise (UpdateCtx (end_outer_borrows config bids ctx))
+ | V.MutLoan bid -> raise (UpdateCtx (end_outer_borrow config bid ctx))
+ else super#visit_loan_content end_loans lc
+ end
+ in
+
(* We do something similar to [end_loans_at_place].
First, retrieve the value *)
match read_place config Write p ctx with
| Error _ -> failwith "Unreachable"
| Ok v -> (
- (* Explore the value to check if we need to update the environment.
-
- Note that we can end the borrows which are inside the value (while the
- value itself might be inside a borrow/loan: we are thus ending inner
- borrows). Because a loan inside the value may be linked to a borrow
- somewhere else *also inside* the value (it's possible with adts),
- we first end all the borrows we find - by using [Inner] to allow
- ending inner borrows - then end all the loans we find. It is really
- important to do this in two steps: the borrow linked to a loan may
- be inside the value at place p, in which case this borrow may be
- an inner borrow that we *can* end, but it may also be outside this
- value, in which case we need to end all the outer borrows first...
- Also, whenever the environment is updated, we need to re-inspect
- the value at place p *in two steps* again (end borrows, then end loans).
-
- We use exceptions to make it handy.
- *)
- let rec inspect_update (end_loans : bool) (v : V.typed_value) : unit =
- match v.V.value with
- | V.Concrete _ -> ()
- | V.Bottom ->
- (* Note that we are going to *write* to the value: it is ok if this
- value contains [Bottom] - and actually we introduce some
- occurrences of [Bottom] by ending borrows *)
- ()
- | V.Symbolic _ ->
- (* Nothing to do for symbolic values - TODO: not sure *)
- raise Unimplemented
- | V.Adt adt -> List.iter (inspect_update end_loans) adt.field_values
- | V.Borrow bc -> (
- assert (not end_loans);
-
- (* Sanity check *)
- (* We need to end all borrows. Note that we ignore the outer borrows
- when ending the borrows we find here (we call [end_inner_borrow(s)]:
- the value at place p might be below a borrow/loan. Note however
- that the borrow we found here is an outer borrow, if we restrain
- ourselves at the value at place p.
- *)
- match bc with
- | V.SharedBorrow bid | V.MutBorrow (bid, _) ->
- L.log#ldebug
- (lazy
- ("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_loans_at_lplace: activating "
- ^ V.BorrowId.to_string bid));
- (* We need to activate inactivated borrows - later, we will
- * actually end it *)
- let ctx =
- activate_inactivated_mut_borrow config Inner bid ctx
- in
- raise (UpdateCtx ctx))
- | V.Loan lc ->
- 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
- outside this value: we need to call [end_outer_borrow(s)]
- (we can't ignore outer borrows this time).
- *)
- match lc with
- | V.SharedLoan (bids, _) ->
- raise (UpdateCtx (end_outer_borrows config bids ctx))
- | V.MutLoan bid ->
- raise (UpdateCtx (end_outer_borrow config bid ctx))
- else ()
- in
(* Inspect the value and update the context while doing so.
If the context gets updated: perform a recursive call (many things
may have been updated in the context: first we need to retrieve the
@@ -1486,13 +1474,103 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
*)
try
(* Inspect the value: end the borrows only *)
- inspect_update false v;
+ obj#visit_typed_value false v;
(* Inspect the value: end the loans *)
- inspect_update true v;
+ obj#visit_typed_value true v;
(* No context update required: return the current context *)
ctx
with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx)
+(* (* Explore the value to check if we need to update the environment.
+
+ Note that we can end the borrows which are inside the value (while the
+ value itself might be inside a borrow/loan: we are thus ending inner
+ borrows). Because a loan inside the value may be linked to a borrow
+ somewhere else *also inside* the value (it's possible with adts),
+ we first end all the borrows we find - by using [Inner] to allow
+ ending inner borrows - then end all the loans we find. It is really
+ important to do this in two steps: the borrow linked to a loan may
+ be inside the value at place p, in which case this borrow may be
+ an inner borrow that we *can* end, but it may also be outside this
+ value, in which case we need to end all the outer borrows first...
+ Also, whenever the environment is updated, we need to re-inspect
+ the value at place p *in two steps* again (end borrows, then end loans).
+
+ We use exceptions to make it handy.
+ *)
+ let rec inspect_update (end_loans : bool) (v : V.typed_value) : unit =
+ match v.V.value with
+ | V.Concrete _ -> ()
+ | V.Bottom ->
+ (* Note that we are going to *write* to the value: it is ok if this
+ value contains [Bottom] - and actually we introduce some
+ occurrences of [Bottom] by ending borrows *)
+ ()
+ | V.Symbolic _ ->
+ (* Nothing to do for symbolic values - TODO: not sure *)
+ raise Unimplemented
+ | V.Adt adt -> List.iter (inspect_update end_loans) adt.field_values
+ | V.Borrow bc -> (
+ assert (not end_loans);
+
+ (* Sanity check *)
+ (* We need to end all borrows. Note that we ignore the outer borrows
+ when ending the borrows we find here (we call [end_inner_borrow(s)]:
+ the value at place p might be below a borrow/loan. Note however
+ that the borrow we found here is an outer borrow, if we restrain
+ ourselves at the value at place p.
+ *)
+ match bc with
+ | V.SharedBorrow bid | V.MutBorrow (bid, _) ->
+ L.log#ldebug
+ (lazy
+ ("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_loans_at_lplace: activating "
+ ^ V.BorrowId.to_string bid));
+ (* We need to activate ithe nactivated borrow - later, we will
+ * actually end it *)
+ let ctx =
+ activate_inactivated_mut_borrow config Inner bid ctx
+ in
+ raise (UpdateCtx ctx))
+ | V.Loan lc ->
+ 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
+ outside this value: we need to call [end_outer_borrow(s)]
+ (we can't ignore outer borrows this time).
+ *)
+ match lc with
+ | V.SharedLoan (bids, _) ->
+ raise (UpdateCtx (end_outer_borrows config bids ctx))
+ | V.MutLoan bid ->
+ raise (UpdateCtx (end_outer_borrow config bid ctx))
+ else ()
+ in
+ (* Inspect the value and update the context while doing so.
+ If the context gets updated: perform a recursive call (many things
+ may have been updated in the context: first we need to retrieve the
+ proper updated value - and this value may actually not be accessible
+ anymore
+ *)
+ try
+ (* Inspect the value: end the borrows only *)
+ inspect_update false v;
+ (* Inspect the value: end the loans *)
+ inspect_update true v;
+ (* No context update required: return the current context *)
+ ctx
+ with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx)*)
+
(** Copy a value, and return the resulting value.
Note that copying values might update the context. For instance, when