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