diff options
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterBorrows.ml | 1057 |
1 files changed, 1057 insertions, 0 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml new file mode 100644 index 00000000..1dd4d247 --- /dev/null +++ b/src/InterpreterBorrows.ml @@ -0,0 +1,1057 @@ +module T = Types +module V = Values +module C = Contexts +module Subst = Substitute +module L = Logging +open ValuesUtils +open TypesUtils +open InterpreterUtils +open InterpreterBorrowsCore +open InterpreterProjectors + +(** Auxiliary function to end borrows: lookup a borrow in the environment, + update it (by returning an updated environment where the borrow has been + replaced by [Bottom])) if we can end the borrow (for instance, it is not + an outer borrow...) or return the reason why we couldn't update the borrow. + + [end_borrow] then simply performs a loop: as long as we need to end (outer) + borrows, we end them, before finally ending the borrow we wanted to end in the + first place. + + Note that it is possible to end a borrow in an abstraction, without ending + the whole abstraction, if the corresponding loan is inside the abstraction + as well. The [allowed_abs] parameter controls whether we allow to end borrows + in an abstraction or not, and in which abstraction. +*) +let end_borrow_get_borrow (io : inner_outer) + (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) + (ctx : C.eval_ctx) : + (C.eval_ctx * g_borrow_content option, outer_borrows_or_abs) result = + (* We use a reference to communicate the kind of borrow we found, if we + * find one *) + let replaced_bc : g_borrow_content option ref = ref None in + let set_replaced_bc (bc : g_borrow_content) = + assert (Option.is_none !replaced_bc); + replaced_bc := Some bc + in + (* Raise an exception if there are outer borrows or if we are inside an + * abstraction: this exception is caught in a wrapper function *) + let raise_if_outer (outer : V.AbstractionId.id option * borrow_ids option) = + let outer_abs, outer_borrows = outer in + match outer_abs with + | Some abs -> ( + if + (* Check if we can end borrows inside this abstraction *) + Some abs <> allowed_abs + then raise (FoundOuter (OuterAbs abs)) + else + match outer_borrows with + | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) + | None -> ()) + | None -> ( + match outer_borrows with + | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) + | None -> ()) + in + + (* The environment is used to keep track of the outer loans *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option) + lc = + match lc with + | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer bid) + | V.SharedLoan (bids, v) -> + (* Update the outer borrows before diving into the shared value *) + let outer = update_outer_borrows io outer (Borrows bids) in + V.Loan (super#visit_SharedLoan outer bids v) + (** We reimplement [visit_Loan] because we may have to update the + outer borrows *) + + method! visit_Borrow outer bc = + match bc with + | SharedBorrow l' | InactivatedMutBorrow l' -> + (* Check if this is the borrow we are looking for *) + if l = l' then ( + (* Check if there are outer borrows or if we are inside an abstraction *) + raise_if_outer outer; + (* Register the update *) + set_replaced_bc (Concrete bc); + (* Update the value *) + V.Bottom) + else super#visit_Borrow outer bc + | V.MutBorrow (l', bv) -> + (* Check if this is the borrow we are looking for *) + if l = l' then ( + (* Check if there are outer borrows or if we are inside an abstraction *) + raise_if_outer outer; + (* Register the update *) + set_replaced_bc (Concrete bc); + (* Update the value *) + V.Bottom) + else + (* Update the outer borrows before diving into the borrowed value *) + let outer = update_outer_borrows io outer (Borrow l') in + V.Borrow (super#visit_MutBorrow outer l' bv) + + method! visit_ALoan outer lc = + (* Note that the children avalues are just other, independent loans, + * so we don't need to update the outer borrows when diving in. + * We keep track of the parents/children relationship only because we + * need it to properly instantiate the backward functions when generating + * the pure translation. *) + match lc with + | V.AMutLoan (bid, av) -> + (* Nothing special to do *) + V.ALoan (super#visit_AMutLoan outer bid av) + | V.ASharedLoan (bids, v, av) -> + (* Explore the shared value - we need to update the outer borrows *) + let souter = update_outer_borrows io outer (Borrows bids) in + let v = super#visit_typed_value souter v in + (* Explore the child avalue - we keep the same outer borrows *) + let av = super#visit_typed_avalue outer av in + (* Reconstruct *) + V.ALoan (V.ASharedLoan (bids, v, av)) + | V.AEndedMutLoan { given_back; child } -> + (* The loan has ended, so no need to update the outer borrows *) + V.ALoan (super#visit_AEndedMutLoan outer given_back child) + | V.AEndedSharedLoan (v, av) -> + (* The loan has ended, so no need to update the outer borrows *) + V.ALoan (super#visit_AEndedSharedLoan outer v av) + | V.AIgnoredMutLoan (bid, av) -> + (* Nothing special to do *) + V.ALoan (super#visit_AIgnoredMutLoan outer bid av) + | V.AEndedIgnoredMutLoan { given_back; child } -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child) + | V.AIgnoredSharedLoan av -> + (* Nothing special to do *) + V.ALoan (super#visit_AIgnoredSharedLoan outer av) + (** We reimplement [visit_ALoan] because we may have to update the + outer borrows *) + + method! visit_ABorrow outer bc = + match bc with + | V.AMutBorrow (bid, av) -> + (* Check if this is the borrow we are looking for *) + if bid = l then ( + (* When ending a mut borrow, there are two cases: + * - in the general case, we have to end the whole abstraction + * (and thus raise an exception to signal that to the caller) + * - in some situations, the associated loan is inside the same + * abstraction as the borrow. In this situation, we can end + * the borrow without ending the whole abstraction, and we + * simply move the child avalue around. + *) + (* Check there are outer borrows, or if we need to end the whole + * abstraction *) + raise_if_outer outer; + (* Register the update *) + set_replaced_bc (Abstract bc); + (* Update the value - note that we are necessarily in the second + * of the two cases described above *) + V.ABottom) + else + (* Update the outer borrows before diving into the child avalue *) + let outer = update_outer_borrows io outer (Borrow bid) in + V.ABorrow (super#visit_AMutBorrow outer bid av) + | V.ASharedBorrow bid -> + (* Check if this is the borrow we are looking for *) + if bid = l then ( + (* Check there are outer borrows, or if we need to end the whole + * abstraction *) + raise_if_outer outer; + (* Register the update *) + set_replaced_bc (Abstract bc); + (* Update the value - note that we are necessarily in the second + * of the two cases described above *) + V.ABottom) + else V.ABorrow (super#visit_ASharedBorrow outer bid) + | V.AIgnoredMutBorrow av -> + (* Nothing special to do *) + V.ABorrow (super#visit_AIgnoredMutBorrow outer av) + | V.AProjSharedBorrow asb -> + (* Check if the borrow we are looking for is in the asb *) + if borrow_in_asb l asb then ( + (* Check there are outer borrows, or if we need to end the whole + * abstraction *) + raise_if_outer outer; + (* Register the update *) + set_replaced_bc (Abstract bc); + (* Update the value - note that we are necessarily in the second + * of the two cases described above *) + let asb = remove_borrow_from_asb l asb in + V.ABorrow (V.AProjSharedBorrow asb)) + else + (* Nothing special to do *) + V.ABorrow (super#visit_AProjSharedBorrow outer asb) + + method! visit_abs outer abs = + (* Update the outer abs *) + let outer_abs, outer_borrows = outer in + assert (Option.is_none outer_abs); + assert (Option.is_none outer_borrows); + let outer = (Some abs.V.abs_id, None) in + super#visit_abs outer abs + end + in + (* Catch the exceptions - raised if there are outer borrows *) + try + let ctx = obj#visit_eval_ctx (None, None) ctx in + Ok (ctx, !replaced_bc) + with FoundOuter outers -> Error outers + +(** Auxiliary function to end borrows. See [give_back]. + + When we end a mutable borrow, we need to "give back" the value it contained + to its original owner by reinserting it at the proper position. + + Note that this function checks that there is exactly one loan to which we + give the value back. + TODO: this was not the case before, so some sanity checks are not useful anymore. + *) +let give_back_value (config : C.config) (bid : V.BorrowId.id) + (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = + (* We use a reference to check that we updated exactly one loan *) + let replaced : bool ref = ref false in + let set_replaced () = + assert (not !replaced); + replaced := true + in + (* Whenever giving back symbolic values, they shouldn't contain already ended regions *) + let check_symbolic_no_ended = true in + (* We sometimes need to reborrow values while giving a value back due: prepare that *) + let allow_reborrows = true in + let fresh_reborrow, apply_registered_reborrows = + prepare_reborrows config allow_reborrows + in + (* The visitor to give back the values *) + let obj = + object (self) + inherit [_] C.map_eval_ctx as super + + method! visit_Loan opt_abs lc = + match lc with + | V.SharedLoan (bids, v) -> + (* We are giving back a value (i.e., the content of a *mutable* + * borrow): nothing special to do *) + V.Loan (super#visit_SharedLoan opt_abs bids v) + | V.MutLoan bid' -> + (* Check if this is the loan we are looking for *) + if bid' = bid then ( + set_replaced (); + nv.V.value) + else V.Loan (super#visit_MutLoan opt_abs bid') + + method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue + = + match av.V.value with + | V.ALoan lc -> + let value = self#visit_typed_ALoan opt_abs av.V.ty lc in + ({ av with V.value } : V.typed_avalue) + | _ -> super#visit_typed_avalue opt_abs av + (** This is a bit annoying, but as we need the type of the avalue we + are exploring, in order to be able to project the value we give + back, we need to reimplement [visit_typed_avalue] instead of + [visit_ALoan] *) + + method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty) + (lc : V.aloan_content) : V.avalue = + (* Preparing a bit *) + let regions = + match opt_abs with + | None -> failwith "Unreachable" + | Some abs -> abs.V.regions + in + (* Rk.: there is a small issue with the types of the aloan values *) + let borrowed_value_aty = + let _, ty, _ = ty_get_ref ty in + ty + in + match lc with + | V.AMutLoan (bid', child) -> + if bid' = bid then ( + (* This is the loan we are looking for: apply the projection to + * the value we give back and replaced this mutable loan with + * an ended loan *) + (* Register the insertion *) + set_replaced (); + (* Apply the projection *) + let given_back = + apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow + regions nv borrowed_value_aty + in + (* Return the new value *) + V.ALoan (V.AEndedMutLoan { given_back; child })) + else + (* Continue exploring *) + V.ALoan (super#visit_AMutLoan opt_abs bid' child) + | V.ASharedLoan (bids, v, av) -> + (* We are giving back a value to a *mutable* loan: nothing special to do *) + V.ALoan (super#visit_ASharedLoan opt_abs bids v av) + | V.AEndedMutLoan { given_back; child } -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child) + | V.AEndedSharedLoan (v, av) -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedSharedLoan opt_abs v av) + | V.AIgnoredMutLoan (bid', child) -> + (* This loan is ignored, but we may have to project on a subvalue + * of the value which is given back *) + if bid' = bid then + (* Note that we replace the ignored mut loan by an *ended* ignored + * mut loan. Also, this is not the loan we are looking for *per se*: + * we don't register the fact that we inserted the value somewhere + * (i.e., we don't call [set_replaced]) *) + let given_back = + apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow + regions nv borrowed_value_aty + in + V.ALoan (V.AEndedIgnoredMutLoan { given_back; child }) + else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child) + | V.AEndedIgnoredMutLoan { given_back; child } -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child) + | V.AIgnoredSharedLoan av -> + (* Nothing special to do *) + V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av) + (** We are not specializing an already existing method, but adding a + new method (for projections, we need type information) *) + + method! visit_Abs opt_abs abs = + (* We remember in which abstraction we are before diving - + * this is necessary for projecting values: we need to know + * over which regions to project *) + assert (Option.is_none opt_abs); + super#visit_Abs (Some abs) abs + end + in + + (* Explore the environment *) + let ctx = obj#visit_eval_ctx None ctx in + (* Check we gave back to exactly one loan *) + assert !replaced; + (* Apply the reborrows *) + apply_registered_reborrows ctx + +(** Auxiliary function to end borrows. See [give_back]. + + This function is similar to [give_back_value] but gives back an [avalue] + (coming from an abstraction). + + It is used when ending a borrow inside an abstraction, when the corresponding + loan is inside the same abstraction (in which case we don't need to end the whole + abstraction). + + REMARK: this function can't be used to give back the values borrowed by + end abstraction when ending this abstraction. When doing this, we need + to convert the [avalue] to a [value] by introducing the proper symbolic values. + *) +let give_back_avalue (_config : C.config) (bid : V.BorrowId.id) + (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx = + (* We use a reference to check that we updated exactly one loan *) + let replaced : bool ref = ref false in + let set_replaced () = + assert (not !replaced); + replaced := true + in + let obj = + object (self) + inherit [_] C.map_eval_ctx as super + + method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue + = + match av.V.value with + | V.ALoan lc -> + let value = self#visit_typed_ALoan opt_abs av.V.ty lc in + ({ av with V.value } : V.typed_avalue) + | _ -> super#visit_typed_avalue opt_abs av + (** This is a bit annoying, but as we need the type of the avalue we + are exploring, in order to be able to project the value we give + back, we need to reimplement [visit_typed_avalue] instead of + [visit_ALoan] *) + + method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty) + (lc : V.aloan_content) : V.avalue = + match lc with + | V.AMutLoan (bid', child) -> + if bid' = bid then ( + (* This is the loan we are looking for: apply the projection to + * the value we give back and replaced this mutable loan with + * an ended loan *) + (* Register the insertion *) + set_replaced (); + (* Sanity check *) + assert (nv.V.ty = ty); + (* Return the new value *) + V.ALoan (V.AEndedMutLoan { given_back = nv; child })) + else + (* Continue exploring *) + V.ALoan (super#visit_AMutLoan opt_abs bid' child) + | V.ASharedLoan (bids, v, av) -> + (* We are giving back a value to a *mutable* loan: nothing special to do *) + V.ALoan (super#visit_ASharedLoan opt_abs bids v av) + | V.AEndedMutLoan { given_back; child } -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child) + | V.AEndedSharedLoan (v, av) -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedSharedLoan opt_abs v av) + | V.AIgnoredMutLoan (bid', child) -> + (* This loan is ignored, but we may have to project on a subvalue + * of the value which is given back *) + if bid' = bid then ( + (* Note that we replace the ignored mut loan by an *ended* ignored + * mut loan. Also, this is not the loan we are looking for *per se*: + * we don't register the fact that we inserted the value somewhere + * (i.e., we don't call [set_replaced]) *) + (* Sanity check *) + assert (nv.V.ty = ty); + V.ALoan (V.AEndedIgnoredMutLoan { given_back = nv; child })) + else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child) + | V.AEndedIgnoredMutLoan { given_back; child } -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child) + | V.AIgnoredSharedLoan av -> + (* Nothing special to do *) + V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av) + (** We are not specializing an already existing method, but adding a + new method (for projections, we need type information) *) + end + in + + (* Explore the environment *) + let ctx = obj#visit_eval_ctx None ctx in + (* Check we gave back to exactly one loan *) + assert !replaced; + (* Return *) + ctx + +(** Auxiliary function to end borrows. See [give_back]. + + When we end a shared borrow, we need to remove the borrow id from the list + of borrows to the shared value. + + Note that this function checks that there is exactly one shared loan that + we update. + TODO: this was not the case before, so some sanity checks are not useful anymore. + *) +let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) : + C.eval_ctx = + (* We use a reference to check that we updated exactly one loan *) + let replaced : bool ref = ref false in + let set_replaced () = + assert (not !replaced); + replaced := true + in + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_Loan opt_abs lc = + match lc with + | V.SharedLoan (bids, shared_value) -> + if V.BorrowId.Set.mem bid bids then ( + (* This is the loan we are looking for *) + set_replaced (); + (* If there remains exactly one borrow identifier, we need + * to end the loan. Otherwise, we just remove the current + * loan identifier *) + if V.BorrowId.Set.cardinal bids = 1 then shared_value.V.value + else + V.Loan + (V.SharedLoan (V.BorrowId.Set.remove bid bids, shared_value))) + else + (* Not the loan we are looking for: continue exploring *) + V.Loan (super#visit_SharedLoan opt_abs bids shared_value) + | V.MutLoan bid' -> + (* We are giving back a *shared* borrow: nothing special to do *) + V.Loan (super#visit_MutLoan opt_abs bid') + + method! visit_ALoan opt_abs lc = + match lc with + | V.AMutLoan (bid, av) -> + (* Nothing special to do (we are giving back a *shared* borrow) *) + V.ALoan (super#visit_AMutLoan opt_abs bid av) + | V.ASharedLoan (bids, shared_value, child) -> + if V.BorrowId.Set.mem bid bids then ( + (* This is the loan we are looking for *) + set_replaced (); + (* If there remains exactly one borrow identifier, we need + * to end the loan. Otherwise, we just remove the current + * loan identifier *) + if V.BorrowId.Set.cardinal bids = 1 then + V.ALoan (V.AEndedSharedLoan (shared_value, child)) + else + V.ALoan + (V.ASharedLoan + (V.BorrowId.Set.remove bid bids, shared_value, child))) + else + (* Not the loan we are looking for: continue exploring *) + V.ALoan (super#visit_ASharedLoan opt_abs bids shared_value child) + | V.AEndedMutLoan { given_back; child } -> + (* Nothing special to do (the loan has ended) *) + V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child) + | V.AEndedSharedLoan (v, av) -> + (* Nothing special to do (the loan has ended) *) + V.ALoan (super#visit_AEndedSharedLoan opt_abs v av) + | V.AIgnoredMutLoan (bid, av) -> + (* Nothing special to do (we are giving back a *shared* borrow) *) + V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid av) + | V.AEndedIgnoredMutLoan { given_back; child } -> + (* Nothing special to do *) + V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child) + | V.AIgnoredSharedLoan av -> + (* Nothing special to do *) + V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av) + end + in + + (* Explore the environment *) + let ctx = obj#visit_eval_ctx None ctx in + (* Check we gave back to exactly one loan *) + assert !replaced; + (* Return *) + ctx + +(** When copying values, we duplicate the shared borrows. This is tantamount + to reborrowing the shared value. The following function applies this change + to an environment by inserting a new borrow id in the set of borrows tracked + by a shared value, referenced by the [original_bid] argument. + *) +let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Keep track of changes *) + let r = ref false in + let set_ref () = + assert (not !r); + r := true + in + + let obj = + object + inherit [_] C.map_env as super + + method! visit_SharedLoan env bids sv = + (* Shared loan: check if the borrow id we are looking for is in the + set of borrow ids. If yes, insert the new borrow id, otherwise + explore inside the shared value *) + if V.BorrowId.Set.mem original_bid bids then ( + set_ref (); + let bids' = V.BorrowId.Set.add new_bid bids in + V.SharedLoan (bids', sv)) + else super#visit_SharedLoan env bids sv + + method! visit_ASharedLoan env bids v av = + (* This case is similar to the [SharedLoan] case *) + if V.BorrowId.Set.mem original_bid bids then ( + set_ref (); + let bids' = V.BorrowId.Set.add new_bid bids in + V.ASharedLoan (bids', v, av)) + else super#visit_ASharedLoan env bids v av + end + in + + let env = obj#visit_env () ctx.env in + (* Check that we reborrowed once *) + assert !r; + { ctx with env } + +(** Auxiliary function: see [end_borrow_in_env] *) +let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) + (ctx : C.eval_ctx) : C.eval_ctx = + (* This is used for sanity checks *) + let sanity_ek = + { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } + in + match bc with + | Concrete (V.MutBorrow (l', tv)) -> + (* Sanity check *) + assert (l' = l); + (* Check that the corresponding loan is somewhere - purely a sanity check *) + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_value config l tv ctx + | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') -> + (* Sanity check *) + assert (l' = l); + (* Check that the borrow is somewhere - purely a sanity check *) + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_shared config l ctx + | Abstract (V.AMutBorrow (l', av)) -> + (* Sanity check *) + assert (l' = l); + (* Check that the corresponding loan is somewhere - purely a sanity check *) + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_avalue config l av ctx + | Abstract (V.ASharedBorrow l') -> + (* Sanity check *) + assert (l' = l); + (* Check that the borrow is somewhere - purely a sanity check *) + assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + (* Update the context *) + give_back_shared config l ctx + | Abstract (V.AProjSharedBorrow asb) -> + (* Sanity check *) + assert (borrow_in_asb l asb); + (* Update the context *) + give_back_shared config l ctx + | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable" + +(** Convert an [avalue] to a [value]. + + This function is used when ending abstractions: whenever we end a borrow + in an abstraction, we converted the borrowed [avalue] to a fresh symbolic + [value], then give back this [value] to the context. + + Note that some regions may have ended in the symbolic value we generate. + For instance, consider the following function signature: + ``` + fn f<'a>(x : &'a mut &'a mut u32); + ``` + When ending the abstraction, the value given back for the outer borrow + should be ⊥. In practice, we will give back a symbolic value which can't + be expanded (because expanding this symbolic value would require expanding + a reference whose region has already ended). + *) +let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value = + (* Convert the type *) + let ty = Subst.erase_regions av.V.ty in + (* Generate the fresh a symbolic value *) + let sv_id = C.fresh_symbolic_value_id () in + let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in + let value = V.Symbolic svalue in + { V.value; V.ty } + +(** End a borrow identified by its borrow id in a context + + First lookup the borrow in the context and replace it with [Bottom]. + Then, check that there is an associated loan in the context. When moving + values, before putting the value in its destination, we get an + intermediate state where some values are "outside" the context and thus + inaccessible. As [give_back_value] just performs a map for instance (TODO: + not the case anymore), we need to check independently that there is indeed a + loan ready to receive the value we give back (note that we also have other + invariants like: there is exacly one mutable loan associated to a mutable + borrow, etc. but they are more easily maintained). + Note that in theory, we shouldn't never reach a problematic state as the + one we describe above, because when we move a value we need to end all the + loans inside before moving it. Still, it is a very useful sanity check. + Finally, give the values back. + + Of course, we end outer borrows before updating the target borrow if it + proves necessary: this is controled by the [io] parameter. If it is [Inner], + we allow ending inner borrows (without ending the outer borrows first), + otherwise we only allow ending outer borrows. + If a borrow is inside an abstraction, we need to end the whole abstraction, + at the exception of the case where the loan corresponding to the borrow is + inside the same abstraction. We control this with the [allowed_abs] parameter: + if it is not `None`, we allow ending a borrow if it is inside the given + abstraction. In practice, if the value is `Some abs_id`, we should have + checked that the corresponding loan is inside the abstraction given by + `abs_id` before. In practice, only [end_borrow] should call itself + with `allowed_abs = Some ...`, all the other calls should use `allowed_abs = None`: + if you look ath the implementation details, `end_borrow` performs + all tne necessary checks in case a borrow is inside an abstraction. + *) +let rec end_borrow (config : C.config) (io : inner_outer) + (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + match end_borrow_get_borrow io allowed_abs l ctx with + (* Two cases: + * - error: we found outer borrows (end them first) + * - success: we didn't find outer borrows when updating (but maybe we actually + didn't find the borrow we were looking for...) + *) + | Error outer -> ( + (* End the outer borrows, abstraction, then try again to end the target + * borrow (if necessary) *) + match outer with + | OuterBorrows (Borrows bids) -> + (* Note that when ending outer borrows, we use io=Outer. However, + * we shouldn't need to end outer borrows if io=Inner, so we just + * add the following assertion *) + assert (io = Outer); + (* Note that we might get there with `allowed_abs <> None`: we might + * be trying to end a borrow inside an abstraction, but which is actually + * inside another borrow *) + let allowed_abs' = None in + let ctx = end_borrows config io allowed_abs' bids ctx in + (* Retry to end the borrow *) + end_borrow config io allowed_abs l ctx + | OuterBorrows (Borrow bid) -> + (* See the comments for the previous case *) + assert (io = Outer); + let allowed_abs' = None in + let ctx = end_borrow config io allowed_abs' bid ctx in + (* Retry to end the borrow *) + end_borrow config io allowed_abs l ctx + | OuterAbs abs_id -> ( + (* The borrow is inside an asbtraction: check if the corresponding + * loan is inside the same abstraction. If this is the case, we end + * the borrow without ending the abstraction. If not, we need to + * end the whole abstraction *) + (* Note that we can lookup the loan anywhere *) + let ek = + { + enter_shared_loans = true; + enter_mut_borrows = true; + enter_abs = true; + } + in + match lookup_loan ek l ctx with + | AbsId loan_abs_id, _ -> + if loan_abs_id = abs_id then ( + (* Same abstraction! We can end the borrow *) + let ctx = end_borrow config io (Some abs_id) l ctx in + (* Sanity check *) + assert (Option.is_none (lookup_borrow_opt ek l ctx)); + ctx) + else + (* Not the same abstraction: we need to end the whole abstraction. + * By doing that we should have ended the target borrow (see the + * below sanity check) *) + let ctx = end_abstraction config abs_id ctx in + (* Sanity check: we ended the target borrow *) + assert (Option.is_none (lookup_borrow_opt ek l ctx)); + ctx + | VarId _, _ -> + (* The loan is not inside the same abstraction (actually inside + * a non-abstraction value): we need to end the whole abstraction *) + let ctx = end_abstraction config abs_id ctx in + (* Sanity check: we ended the target borrow *) + assert (Option.is_none (lookup_borrow_opt ek l ctx)); + ctx)) + | Ok (ctx, None) -> + (* It is possible that we can't find a borrow in symbolic mode (ending + * an abstraction may end several borrows at once *) + assert (config.mode = SymbolicMode); + ctx + (* We found a borrow: give the value back (i.e., update the corresponding loan) *) + | Ok (ctx, Some bc) -> give_back config l bc ctx + +and end_borrows (config : C.config) (io : inner_outer) + (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) + (ctx : C.eval_ctx) : C.eval_ctx = + V.BorrowId.Set.fold + (fun id ctx -> end_borrow config io allowed_abs id ctx) + lset ctx + +and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Lookup the abstraction *) + let abs = C.ctx_lookup_abs ctx abs_id in + (* End the parent abstractions first *) + let ctx = end_abstractions config abs.parents ctx in + (* End the loans inside the abstraction *) + let ctx = end_abstraction_loans config abs_id ctx in + (* End the abstraction itself by redistributing the borrows it contains *) + let ctx = end_abstraction_borrows config abs_id ctx in + (* End the regions owned by the abstraction - note that we don't need to + * relookup the abstraction: the set of regions in an abstraction never + * changes... *) + let ctx = + { + ctx with + ended_regions = T.RegionId.Set.union ctx.ended_regions abs.V.regions; + } + in + (* Remove all the references to the id of the current abstraction, and remove + * the abstraction itself *) + end_abstraction_remove_from_context config abs_id ctx + +and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t) + (ctx : C.eval_ctx) : C.eval_ctx = + V.AbstractionId.Set.fold + (fun id ctx -> end_abstraction config id ctx) + abs_ids ctx + +and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Lookup the abstraction *) + let abs = C.ctx_lookup_abs ctx abs_id in + (* End the first loan we find *) + let obj = + object + inherit [_] V.iter_abs as super + + method! visit_aloan_content env lc = + match lc with + | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid)) + | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids)) + | V.AEndedMutLoan { given_back; child } -> + super#visit_AEndedMutLoan env given_back child + | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av + | V.AIgnoredMutLoan (bid, av) -> + (* Note that this loan can't come from a parent abstraction, because + * we should have ended them already) *) + super#visit_AIgnoredMutLoan env bid av + | V.AEndedIgnoredMutLoan { given_back; child } -> + super#visit_AEndedIgnoredMutLoan env given_back child + | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av + end + in + try + (* Check if there are loans *) + obj#visit_abs () abs; + (* No loans: nothing to update *) + ctx + with (* There are loans: end them, then recheck *) + | FoundBorrowIds bids -> + let ctx = + match bids with + | Borrow bid -> end_outer_borrow config bid ctx + | Borrows bids -> end_outer_borrows config bids ctx + in + (* Recheck *) + end_abstraction_loans config abs_id ctx + +and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Note that the abstraction mustn't contain any loans *) + (* We end the borrows, starting with the *inner* ones. This is important + when considering nested borrows which have the same lifetime. + + For instance: + ``` + x -> mut_loan l1 + px -> mut_loan l0 + abs0 { a_mut_borrow l0 (a_mut_borrow l1 (U32 3)) } + ``` + + becomes (`U32 3` doesn't contain ⊥, so we give back a symbolic value): + ``` + x -> @s0 + px -> mut_loan l0 + abs0 { a_mut_borrow l0 ⊥ } + ``` + + then (the borrowed value contains ⊥, we give back ⊥): + ``` + x -> @s0 + px -> ⊥ + abs0 { ⊥ } + ``` + *) + (* We explore in-depth and use exceptions. When exploring a borrow, if + * the exploration didn't trigger an exception, it means there are no + * inner borrows to end: we can thus trigger an exception for the current + * borrow. *) + let obj = + object + inherit [_] V.iter_abs as super + + method! visit_aborrow_content env bc = + (* In-depth exploration *) + super#visit_aborrow_content env bc; + (* No exception was raise: we can raise an exception for the + * current borrow *) + match bc with + | V.AMutBorrow (_, _) | V.ASharedBorrow _ -> + (* Raise an exception *) + raise (FoundABorrowContent bc) + | V.AProjSharedBorrow asb -> + (* Raise an exception only if the asb contains borrows *) + if + List.exists + (fun x -> match x with V.AsbBorrow _ -> true | _ -> false) + asb + then raise (FoundABorrowContent bc) + else () + | V.AIgnoredMutBorrow _ -> + (* Nothing to do for ignored borrows *) + () + end + in + (* Lookup the abstraction *) + let abs = C.ctx_lookup_abs ctx abs_id in + try + (* Explore the abstraction, looking for borrows *) + obj#visit_abs () abs; + (* No borrows: nothing to update *) + ctx + with + (* There are borrows: end them, then reexplore *) + | FoundABorrowContent bc -> + (* First, replace the borrow by ⊥ *) + let bid = + match bc with + | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid + | V.AProjSharedBorrow asb -> ( + (* There should be at least one borrow identifier in the set, which we + * can use to identify the whole set *) + match + List.find + (fun x -> match x with V.AsbBorrow _ -> true | _ -> false) + asb + with + | V.AsbBorrow bid -> bid + | _ -> failwith "Unexpected") + | V.AIgnoredMutBorrow _ -> failwith "Unexpected" + in + let ctx = update_aborrow ek_all bid V.ABottom ctx in + (* Then give back the value *) + let ctx = + match bc with + | V.AMutBorrow (bid, av) -> + (* First, convert the avalue to a (fresh symbolic) value *) + let v = convert_avalue_to_value av in + give_back_value config bid v ctx + | V.ASharedBorrow bid -> give_back_shared config bid ctx + | V.AProjSharedBorrow _ -> + (* Nothing to do *) + ctx + | V.AIgnoredMutBorrow _ -> failwith "Unexpected" + in + (* Reexplore *) + end_abstraction_borrows config abs_id ctx + +(** Remove an abstraction from the context, as well as all its references *) +and end_abstraction_remove_from_context (_config : C.config) + (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = + let map_env_elem (ev : C.env_elem) : C.env_elem option = + match ev with + | C.Var (_, _) | C.Frame -> Some ev + | C.Abs abs -> + if abs.abs_id = abs_id then None + else + let parents = V.AbstractionId.Set.remove abs_id abs.parents in + Some (C.Abs { abs with V.parents }) + in + let env = List.filter_map map_env_elem ctx.C.env in + { ctx with C.env } + +and end_outer_borrow config = end_borrow config Outer None + +and end_outer_borrows config = end_borrows config Outer None + +and end_inner_borrow config = end_borrow config Inner None + +and end_inner_borrows config = end_borrows config Inner None + +(** Helper function: see [activate_inactivated_mut_borrow]. + + This function updates the shared loan to a mutable loan (we then update + the borrow with another helper). Of course, the shared loan must contain + exactly one borrow id (the one we give as parameter), otherwise we can't + promote it. Also, the shared value mustn't contain any loan. + + The returned value (previously shared) is checked: + - it mustn't contain loans + - it mustn't contain [Bottom] + - it mustn't contain inactivated borrows + TODO: this kind of checks should be put in an auxiliary helper, because + they are redundant + *) +let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_value = + (* Lookup the shared loan *) + let ek = + { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } + in + match lookup_loan ek l ctx with + | _, Concrete (V.MutLoan _) -> + failwith "Expected a shared loan, found a mut loan" + | _, Concrete (V.SharedLoan (bids, sv)) -> + (* Check that there is only one borrow id (l) and update the loan *) + assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1); + (* We need to check that there aren't any loans in the value: + we should have gotten rid of those already, but it is better + to do a sanity check. *) + assert (not (loans_in_value sv)); + (* Check there isn't [Bottom] (this is actually an invariant *) + assert (not (bottom_in_value ctx.ended_regions sv)); + (* Check there aren't inactivated borrows *) + assert (not (inactivated_in_value sv)); + (* Update the loan content *) + let ctx = update_loan ek l (V.MutLoan l) ctx in + (* Return *) + (ctx, sv) + | _, Abstract _ -> + (* I don't think it is possible to have two-phase borrows involving borrows + * returned by abstractions. I'm not sure how we could handle that anyway. *) + failwith + "Can't promote a shared loan to a mutable loan if the loan is inside \ + an abstraction" + +(** Helper function: see [activate_inactivated_mut_borrow]. + + This function updates a shared borrow to a mutable borrow. + *) +let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) + (borrowed_value : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = + (* Lookup the inactivated borrow - note that we don't go inside borrows/loans: + there can't be inactivated borrows inside other borrows/loans + *) + let ek = + { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } + in + match lookup_borrow ek l ctx with + | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) -> + failwith "Expected an inactivated mutable borrow" + | Concrete (V.InactivatedMutBorrow _) -> + (* Update it *) + update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx + | Abstract _ -> + (* This can't happen for sure *) + failwith + "Can't promote a shared borrow to a mutable borrow if the borrow is \ + inside an abstraction" + +(** Promote an inactivated mut borrow to a mut borrow. + + The borrow must point to a shared value which is borrowed exactly once. + *) +let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) + (l : V.BorrowId.id) (ctx : C.eval_ctx) : C.eval_ctx = + (* Lookup the value *) + let ek = + { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } + in + match lookup_loan ek l ctx with + | _, Concrete (V.MutLoan _) -> failwith "Unreachable" + | _, Concrete (V.SharedLoan (bids, sv)) -> ( + (* If there are loans inside the value, end them. Note that there can't be + inactivated borrows inside the value. + If we perform an update, do a recursive call to lookup the updated value *) + match get_first_loan_in_value sv with + | Some lc -> + (* End the loans *) + let ctx = + match lc with + | V.SharedLoan (bids, _) -> end_outer_borrows config bids ctx + | V.MutLoan bid -> end_outer_borrow config bid ctx + in + (* Recursive call *) + activate_inactivated_mut_borrow config io l ctx + | None -> + (* No loan to end inside the value *) + (* Some sanity checks *) + L.log#ldebug + (lazy + ("activate_inactivated_mut_borrow: resulting value:\n" + ^ V.show_typed_value sv)); + assert (not (loans_in_value sv)); + assert (not (bottom_in_value ctx.ended_regions sv)); + assert (not (inactivated_in_value sv)); + (* End the borrows which borrow from the value, at the exception of + the borrow we want to promote *) + let bids = V.BorrowId.Set.remove l bids in + let allowed_abs = None in + let ctx = end_borrows config io allowed_abs bids ctx in + (* Promote the loan *) + let ctx, borrowed_value = promote_shared_loan_to_mut_loan l ctx in + (* Promote the borrow - the value should have been checked by + [promote_shared_loan_to_mut_loan] + *) + promote_inactivated_borrow_to_mut_borrow l borrowed_value ctx) + | _, Abstract _ -> + (* I don't think it is possible to have two-phase borrows involving borrows + * returned by abstractions. I'm not sure how we could handle that anyway. *) + failwith + "Can't activate an inactivated mutable borrow referencing a loan inside\n\ + \ an abstraction" |