summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-12-08 14:58:50 +0100
committerSon Ho2021-12-08 14:58:50 +0100
commit0cee9e0dbbb804350722f8fb87be5a128d1a8a54 (patch)
treeb285d609d90a519905786066e96d9d9419e9e765 /src
parent688a4e589f46892448be902b7b5467c7198627bf (diff)
Cleanup a bit
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml90
1 files changed, 0 insertions, 90 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2b6193a4..ca011bf0 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1481,96 +1481,6 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
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