diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 90 |
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 |