diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 1100 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 1115 |
2 files changed, 1116 insertions, 1099 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index afe513be..7dc37dff 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -14,6 +14,7 @@ module S = Synthesis open Utils open InterpreterUtils open InterpreterProjectors +open InterpreterBorrows (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -35,1105 +36,6 @@ type eval_error = Panic type 'a eval_result = ('a, eval_error) result -(** 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 ctx - 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 - 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 ty - 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 ty - 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) (ctx : C.eval_ctx) : - C.eval_ctx * V.typed_value = - (* Convert the type *) - let ty = Subst.erase_regions av.V.ty in - (* Generate the fresh a symbolic value *) - let ctx, sv_id = C.fresh_symbolic_value_id ctx in - let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in - let value : V.symbolic_proj_comp = - (* Note that the set of ended regions is empty: we shouldn't have to take - * into account any ended regions at this point, otherwise we would be in - * the first case where we should return ⊥ *) - { V.svalue; V.rset_ended = T.RegionId.Set.empty } - in - let value = V.Symbolic value in - (ctx, { 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 *) - let ctx = end_abstraction_regions config abs_id ctx 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 ctx, v = convert_avalue_to_value av ctx 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 - -(** Update the symbolic values in a context to register the regions in the - abstraction we are ending as already ended. - Note that this function also checks that no symbolic value in an abstraction - contains regions which we are ending. - Of course, we ignore the abstraction we are currently ending... - *) -and end_abstraction_regions (_config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Lookup the abstraction to retrieve the set of owned regions *) - let abs = C.ctx_lookup_abs ctx abs_id in - let ended_regions = abs.V.regions in - (* Update all the symbolic values in the context *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic _ sproj = - let sproj = - { - sproj with - V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions; - } - in - V.Symbolic sproj - - method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj = - (* Sanity check *) - (match aproj with - | V.AProjLoans _ -> () - | V.AProjBorrows (sv, ty) -> ( - match abs_regions with - | None -> failwith "Unexpected" - | Some abs_regions -> - assert ( - not - (projections_intersect sv.V.sv_ty ended_regions ty - abs_regions)))); - (* Return - nothing to update *) - aproj - - method! visit_abs (regions : T.RegionId.set_t option) abs = - if abs.V.abs_id = abs_id then abs - else ( - assert (Option.is_none regions); - (* Check that we don't project over already ended regions *) - assert (T.RegionId.Set.disjoint ended_regions abs.V.regions); - (* Remember the set of regions owned by the abstraction *) - let regions = Some abs.V.regions in - super#visit_abs regions abs) - (** Whenever we dive in an abstraction, we need to keep track of the - set of regions owned by the abstraction. - Also: we don't dive in the abstraction we are currently ending... *) - end - in - (* Update the context *) - obj#visit_eval_ctx None 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 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 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" - (** Paths *) (** When we fail reading from or writing to a path, it might be because we diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml new file mode 100644 index 00000000..e8503d57 --- /dev/null +++ b/src/InterpreterBorrows.ml @@ -0,0 +1,1115 @@ +module T = Types +module V = Values +open Scalars +module E = Expressions +open Errors +module C = Contexts +module Subst = Substitute +module A = CfimAst +module L = Logging +open TypesUtils +open ValuesUtils +module Inv = Invariants +module S = Synthesis +open Utils +open InterpreterUtils +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 ctx + 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 + 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 ty + 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 ty + 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) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_value = + (* Convert the type *) + let ty = Subst.erase_regions av.V.ty in + (* Generate the fresh a symbolic value *) + let ctx, sv_id = C.fresh_symbolic_value_id ctx in + let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in + let value : V.symbolic_proj_comp = + (* Note that the set of ended regions is empty: we shouldn't have to take + * into account any ended regions at this point, otherwise we would be in + * the first case where we should return ⊥ *) + { V.svalue; V.rset_ended = T.RegionId.Set.empty } + in + let value = V.Symbolic value in + (ctx, { 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 *) + let ctx = end_abstraction_regions config abs_id ctx 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 ctx, v = convert_avalue_to_value av ctx 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 + +(** Update the symbolic values in a context to register the regions in the + abstraction we are ending as already ended. + Note that this function also checks that no symbolic value in an abstraction + contains regions which we are ending. + Of course, we ignore the abstraction we are currently ending... + *) +and end_abstraction_regions (_config : C.config) (abs_id : V.AbstractionId.id) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Lookup the abstraction to retrieve the set of owned regions *) + let abs = C.ctx_lookup_abs ctx abs_id in + let ended_regions = abs.V.regions in + (* Update all the symbolic values in the context *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_Symbolic _ sproj = + let sproj = + { + sproj with + V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions; + } + in + V.Symbolic sproj + + method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj = + (* Sanity check *) + (match aproj with + | V.AProjLoans _ -> () + | V.AProjBorrows (sv, ty) -> ( + match abs_regions with + | None -> failwith "Unexpected" + | Some abs_regions -> + assert ( + not + (projections_intersect sv.V.sv_ty ended_regions ty + abs_regions)))); + (* Return - nothing to update *) + aproj + + method! visit_abs (regions : T.RegionId.set_t option) abs = + if abs.V.abs_id = abs_id then abs + else ( + assert (Option.is_none regions); + (* Check that we don't project over already ended regions *) + assert (T.RegionId.Set.disjoint ended_regions abs.V.regions); + (* Remember the set of regions owned by the abstraction *) + let regions = Some abs.V.regions in + super#visit_abs regions abs) + (** Whenever we dive in an abstraction, we need to keep track of the + set of regions owned by the abstraction. + Also: we don't dive in the abstraction we are currently ending... *) + end + in + (* Update the context *) + obj#visit_eval_ctx None 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 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 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" |