diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Cps.ml | 61 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 297 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 10 |
3 files changed, 253 insertions, 115 deletions
diff --git a/src/Cps.ml b/src/Cps.ml new file mode 100644 index 00000000..adb42831 --- /dev/null +++ b/src/Cps.ml @@ -0,0 +1,61 @@ +(** This module defines various utilities to write the interpretation functions + in continuation passing style. *) + +module T = Types +module V = Values +module C = Contexts + +(** Result of evaluating a statement *) +type statement_eval_res = Unit | Break of int | Continue of int | Return + +(** Synthesized expresssion - dummy for now *) +type sexpr = SExpr + +(** TODO: change the name *) +type eval_error = Panic + +type eval_result = (sexpr option, eval_error) Result.result + +type m_fun = C.eval_ctx -> eval_result +(** Monadic function *) + +type cm_fun = m_fun -> m_fun +(** Monadic function with continuation *) + +type typed_value_cm_fun = V.typed_value -> cm_fun +(** Monadic function with continuation and receiving a typed value *) + +(** Convert a unit function to a cm function *) +let unit_to_cm_fun (f : C.eval_ctx -> unit) : cm_fun = + fun cf ctx -> + f ctx; + cf ctx + +(** *) +let update_to_cm_fun (f : C.eval_ctx -> C.eval_ctx) : cm_fun = + fun cf ctx -> + let ctx = f ctx in + cf ctx + +(** Composition of functions taking continuations as paramters. + We tried to make this as general as possible. *) +let comp (f : 'c -> 'd -> 'e) (g : ('a -> 'b) -> 'c) : ('a -> 'b) -> 'd -> 'e = + fun cf ctx -> f (g cf) ctx + +let comp_unit (f : cm_fun) (g : C.eval_ctx -> unit) : cm_fun = + comp f (unit_to_cm_fun g) + +let comp_update (f : cm_fun) (g : C.eval_ctx -> C.eval_ctx) : cm_fun = + comp f (update_to_cm_fun g) + +(** This is just a test, to check that [comp] is general enough to handle a case + where a function must compute a value and give it to the continuation. + It happens for functions like [eval_operand]. + *) +let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun) + (g : m_fun -> V.typed_value -> m_fun) : cm_fun = + comp f g + +let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx + +let id_cm_fun : cm_fun = fun cf ctx -> cf ctx diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index e64dbe77..9333d389 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -3,6 +3,7 @@ module V = Values module C = Contexts module Subst = Substitute module L = Logging +open Cps open ValuesUtils open TypesUtils open InterpreterUtils @@ -777,7 +778,11 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) let convert_avalue_to_given_back_value (av : V.typed_avalue) : V.typed_value = mk_fresh_symbolic_typed_value V.FunCallGivenBack av.V.ty -(** End a borrow identified by its borrow id in a context +(** End a borrow identified by its borrow id in a context. + + Rk.: from now onwards, the functions are written in continuation passing style. + The reason is that when ending borrows we may end abstractions, which results + in synthesized code. 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 @@ -813,14 +818,16 @@ let convert_avalue_to_given_back_value (av : V.typed_avalue) : V.typed_value = book-keeping. *) let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids) - (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) - (ctx : C.eval_ctx) : C.eval_ctx = + (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) : cm_fun = + fun cf ctx -> + (* Check that we don't loop *) let chain0 = chain in let chain = add_borrow_or_abs_id_to_chain "end_borrow: " (BorrowId l) chain in log#ldebug (lazy ("end borrow: " ^ V.BorrowId.to_string l ^ ":\n- original context:\n" ^ eval_ctx_to_string ctx)); + (* Utility function for the sanity checks: check that the borrow disappeared * from the context *) let ctx0 = ctx in @@ -848,7 +855,13 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids) ^ eval_ctx_to_string ctx)); failwith "Loan not eliminated" in + let cf_check_disappeared : cm_fun = + fun cf ctx -> + check_disappeared ctx; + cf ctx + in + (* Start by getting the borrow *) match end_borrow_get_borrow allowed_abs l ctx with (* Two cases: * - error: we found outer borrows or inner loans (end them first) @@ -870,18 +883,20 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids) * 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 chain allowed_abs' bids ctx in + (* End the outer borrows *) + let cf_end_outer = end_borrows config chain allowed_abs' bids in (* Retry to end the borrow *) - end_borrow config chain0 allowed_abs l ctx + let cf_retry = end_borrow config chain0 allowed_abs l in + (* Compose *) + cf_end_outer (cf_retry cf) ctx | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> let allowed_abs' = None in - let ctx = end_borrow config chain allowed_abs' bid ctx in + (* End the outer borrow *) + let cf_end_outer = end_borrow config chain allowed_abs' bid in (* Retry to end the borrow *) - let ctx = end_borrow config chain0 allowed_abs l ctx in - (* Sanity check *) - check_disappeared ctx; - (* Return *) - ctx + let cf_retry = end_borrow config chain0 allowed_abs l in + (* Compose *) + cf_end_outer (cf_retry (cf_check_disappeared cf)) 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 @@ -895,35 +910,32 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids) enter_abs = true; } in - let ctx = + let cf_end_abs : cm_fun = + fun cf ctx -> 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 *) - end_borrow config chain0 (Some abs_id) l ctx + end_borrow config chain0 (Some abs_id) l cf 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) *) - end_abstraction config chain abs_id ctx + end_abstraction config chain abs_id cf ctx | VarId _, _ -> (* The loan is not inside the same abstraction (actually inside * a non-abstraction value): we need to end the whole abstraction *) - end_abstraction config chain abs_id ctx + end_abstraction config chain abs_id cf ctx in - (* Sanity check *) - check_disappeared ctx; - (* Return *) - ctx) + (* Compose with a sanity check *) + cf_end_abs (cf_check_disappeared cf) ctx) | Ok (ctx, None) -> log#ldebug (lazy "End borrow: borrow not found"); (* 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); - (* Sanity check *) - check_disappeared ctx; - (* Return *) - ctx + (* Do a sanity check and continue *) + cf_check_disappeared cf ctx (* We found a borrow: give it back (i.e., update the corresponding loan) *) | Ok (ctx, Some bc) -> (* Sanity check: the borrowed value shouldn't contain loans *) @@ -933,20 +945,21 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids) | _ -> ()); (* Give back the value *) let ctx = give_back config l bc ctx in - (* Sanity check *) - check_disappeared ctx; - (* Return *) - ctx + (* Do a sanity check and continue *) + cf_check_disappeared cf ctx and end_borrows (config : C.config) (chain : borrow_or_abs_ids) - (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) - (ctx : C.eval_ctx) : C.eval_ctx = + (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) : cm_fun + = + fun cf -> V.BorrowId.Set.fold - (fun id ctx -> end_borrow config chain allowed_abs id ctx) - lset ctx + (fun id cf -> end_borrow config chain allowed_abs id cf) + lset cf and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) - (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = + (abs_id : V.AbstractionId.id) : cm_fun = + fun cf ctx -> + (* Check that we don't loop *) let chain = add_borrow_or_abs_id_to_chain "end_abstraction: " (AbsId abs_id) chain in @@ -957,55 +970,78 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) ("end_abstraction: " ^ V.AbstractionId.to_string abs_id ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0)); + + (* Initialize the continuation composition *) + let cc = id_cm_fun in + (* Lookup the abstraction *) let abs = C.ctx_lookup_abs ctx abs_id in + (* End the parent abstractions first *) - let ctx = end_abstractions config chain abs.parents ctx in - log#ldebug - (lazy - ("end_abstraction: " - ^ V.AbstractionId.to_string abs_id - ^ "\n- context after parent abstractions ended:\n" - ^ eval_ctx_to_string ctx)); + let cc = comp cc (end_abstractions config chain abs.parents) in + let cc = + comp_unit cc (fun ctx -> + log#ldebug + (lazy + ("end_abstraction: " + ^ V.AbstractionId.to_string abs_id + ^ "\n- context after parent abstractions ended:\n" + ^ eval_ctx_to_string ctx))) + in + (* End the loans inside the abstraction *) - let ctx = end_abstraction_loans config chain abs_id ctx in - log#ldebug - (lazy - ("end_abstraction: " - ^ V.AbstractionId.to_string abs_id - ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)); + let cc = comp cc (end_abstraction_loans config chain abs_id) in + let cc = + comp_unit cc (fun ctx -> + log#ldebug + (lazy + ("end_abstraction: " + ^ V.AbstractionId.to_string abs_id + ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx))) + in + (* End the abstraction itself by redistributing the borrows it contains *) - let ctx = end_abstraction_borrows config chain abs_id ctx in + let cc = comp cc (end_abstraction_borrows config chain abs_id) 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; - } + let cc = + comp_update cc (fun ctx -> + let ended_regions = + T.RegionId.Set.union ctx.ended_regions abs.V.regions + in + { ctx with ended_regions }) in + (* Remove all the references to the id of the current abstraction, and remove * the abstraction itself *) - let ctx = end_abstraction_remove_from_context config abs_id ctx in + let cc = comp cc (end_abstraction_remove_from_context config abs_id) in + (* Debugging *) - log#ldebug - (lazy - ("end_abstraction: " - ^ V.AbstractionId.to_string abs_id - ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)); - (* Return *) - ctx + let cc = + comp_unit cc (fun ctx -> + log#ldebug + (lazy + ("end_abstraction: " + ^ V.AbstractionId.to_string abs_id + ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx))) + in + + (* Apply the continuation *) + cc cf ctx and end_abstractions (config : C.config) (chain : borrow_or_abs_ids) - (abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = + (abs_ids : V.AbstractionId.Set.t) : cm_fun = + fun cf -> V.AbstractionId.Set.fold - (fun id ctx -> end_abstraction config chain id ctx) - abs_ids ctx + (fun id cf -> end_abstraction config chain id cf) + abs_ids cf and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids) - (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = + (abs_id : V.AbstractionId.id) : cm_fun = + fun cf ctx -> (* Lookup the abstraction *) let abs = C.ctx_lookup_abs ctx abs_id in (* End the first loan we find *) @@ -1042,24 +1078,28 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids) (* Check if there are loans *) obj#visit_abs () abs; (* No loans: nothing to update *) - ctx + cf ctx with (* There are loans: end them, then recheck *) | FoundBorrowIds bids -> - let ctx = + (* End the outer borrows *) + let cc : cm_fun = match bids with - | Borrow bid -> end_outer_borrow config bid ctx - | Borrows bids -> end_outer_borrows config bids ctx + | Borrow bid -> end_outer_borrow config bid + | Borrows bids -> end_outer_borrows config bids in - (* Recheck *) - end_abstraction_loans config chain abs_id ctx + (* Retry *) + let cc = comp cc (end_abstraction_loans config chain abs_id) in + (* Continue *) + cc cf ctx | FoundSymbolicValue sv -> (* There is a proj_loans over a symbolic value: end the proj_borrows * which intersect this proj_loans *) - end_proj_loans_symbolic config chain abs_id abs.regions sv ctx + end_proj_loans_symbolic config chain abs_id abs.regions sv cf ctx and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) - (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = + (abs_id : V.AbstractionId.id) : cm_fun = + fun cf 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. @@ -1115,7 +1155,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* Explore the abstraction, looking for borrows *) obj#visit_abs () abs; (* No borrows: nothing to update *) - ctx + cf ctx with (* There are concrete borrows: end them, then reexplore *) | FoundABorrowContent bc -> @@ -1163,7 +1203,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) failwith "Unexpected" in (* Reexplore *) - end_abstraction_borrows config chain abs_id ctx + end_abstraction_borrows config chain abs_id cf ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> (* Generate a fresh symbolic value *) @@ -1181,11 +1221,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) give_back_symbolic_value config abs.regions proj_ty sv nsv ctx in (* Reexplore *) - end_abstraction_borrows config chain abs_id ctx + end_abstraction_borrows config chain abs_id cf 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 = + (abs_id : V.AbstractionId.id) : cm_fun = + fun cf ctx -> let map_env_elem (ev : C.env_elem) : C.env_elem option = match ev with | C.Var (_, _) | C.Frame -> Some ev @@ -1196,7 +1237,9 @@ and end_abstraction_remove_from_context (_config : C.config) Some (C.Abs { abs with V.parents }) in let env = List.filter_map map_env_elem ctx.C.env in - { ctx with C.env } + let ctx = { ctx with C.env } in + (* Continue *) + cf ctx (** End a proj_loan over a symbolic value by ending the proj_borrows which intersect this proj_loans. @@ -1214,7 +1257,8 @@ and end_abstraction_remove_from_context (_config : C.config) *) and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) (abs_id : V.AbstractionId.id) (regions : T.RegionId.Set.t) - (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = + (sv : V.symbolic_value) : cm_fun = + fun cf ctx -> (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with @@ -1224,7 +1268,9 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) * it is completely absent) *) (* Update the loans depending on the current symbolic value - it is * left unchanged *) - give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx + let ctx = give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx in + (* Continue *) + cf ctx | Some (SharedProjs projs) -> (* We found projectors over shared values - split between the projectors * which belong to the current *) @@ -1243,15 +1289,18 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) (fun s id -> V.AbstractionId.Set.add id s) V.AbstractionId.Set.empty abs_ids in - let ctx = end_abstractions config chain abs_ids ctx in (* We could end the owned projections, but it is simpler to simply return * and let the caller recheck if there are proj_loans to end *) - ctx + end_abstractions config chain abs_ids cf ctx else (* All the proj_borrows are owned: simply erase them *) let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in (* Remove the proj_loans - note that the symbolic value was left unchanged *) - give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx + let ctx = + give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx + in + (* Continue *) + cf ctx | Some (NonSharedProj (abs_id', _proj_ty)) -> (* We found one in the context: if it comes from this abstraction, we can * end it directly, otherwise we need to end the abstraction where it @@ -1267,7 +1316,12 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) in (* Replace the proj_loans - note that the loaned (symbolic) value * was left unchanged *) - give_back_symbolic_value config regions sv.V.sv_ty sv given_back_sv ctx + let ctx = + give_back_symbolic_value config regions sv.V.sv_ty sv given_back_sv + ctx + in + (* Continue *) + cf ctx else (* End the abstraction. * Don't retry ending the current proj_loans after ending the abstraction: @@ -1275,15 +1329,13 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) * or maybe not (if it is a proj over shared values): simply return, * as the caller function will recheck if there are loans to end in the * current abstraction *) - end_abstraction config chain abs_id' ctx - -and end_outer_borrow config = end_borrow config [] None + end_abstraction config chain abs_id' cf ctx -and end_outer_borrows config = end_borrows config [] None +and end_outer_borrow config : V.BorrowId.id -> cm_fun = + end_borrow config [] None -and end_inner_borrow config = end_borrow config [] None - -and end_inner_borrows config = end_borrows config [] None +and end_outer_borrows config : V.BorrowId.Set.t -> cm_fun = + end_borrows config [] None (** Helper function: see [activate_inactivated_mut_borrow]. @@ -1299,8 +1351,9 @@ and end_inner_borrows config = end_borrows config [] None 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 = +let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> (* Lookup the shared loan *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } @@ -1321,8 +1374,8 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : assert (not (inactivated_in_value sv)); (* Update the loan content *) let ctx = update_loan ek l (V.MutLoan l) ctx in - (* Return *) - (ctx, sv) + (* Continue *) + cf sv 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. *) @@ -1334,32 +1387,38 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : 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 = +let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun) + (borrowed_value : V.typed_value) : m_fun = + fun 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" + let ctx = + 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" + in + (* Continue *) + cf ctx (** 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) (l : V.BorrowId.id) - (ctx : C.eval_ctx) : C.eval_ctx = + : cm_fun = + fun cf ctx -> (* Lookup the value *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } @@ -1373,13 +1432,15 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) match get_first_loan_in_value sv with | Some lc -> (* End the loans *) - let ctx = + let cc = match lc with - | V.SharedLoan (bids, _) -> end_outer_borrows config bids ctx - | V.MutLoan bid -> end_outer_borrow config bid ctx + | V.SharedLoan (bids, _) -> end_outer_borrows config bids + | V.MutLoan bid -> end_outer_borrow config bid in (* Recursive call *) - activate_inactivated_mut_borrow config l ctx + let cc = comp cc (activate_inactivated_mut_borrow config l) in + (* Continue *) + cc cf ctx | None -> (* No loan to end inside the value *) (* Some sanity checks *) @@ -1393,13 +1454,19 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) (* 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 ctx = end_outer_borrows config bids ctx in + let cc = end_outer_borrows config bids in (* Promote the loan *) - let ctx, borrowed_value = promote_shared_loan_to_mut_loan l ctx in + let cc = comp cc (promote_shared_loan_to_mut_loan l) in + (* 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) + let cc = + comp cc (fun cf borrowed_value ctx -> + promote_inactivated_borrow_to_mut_borrow l cf borrowed_value ctx) + in + (* Continue *) + cc cf 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. *) diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index d2f8e3e3..5f73fa3a 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -616,6 +616,8 @@ type looked_up_aproj_borrows = [lookup_shared]: if `true` also explore projectors over shared values, otherwise ignore. + + This is a helper function: it might break invariants. *) let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : @@ -704,6 +706,8 @@ let lookup_intersecting_aproj_borrows_not_shared_opt (** Similar to [lookup_intersecting_aproj_borrows_opt], but updates the values. + + This is a helper function: it might break invariants. *) let update_intersecting_aproj_borrows (can_update_shared : bool) (update_shared : V.AbstractionId.id -> T.rty -> V.abstract_shared_borrows) @@ -780,6 +784,8 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) proj_borrows over a non-shared value. We check that we update exactly one proj_borrows. + + This is a helper function: it might break invariants. *) let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (nv : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = @@ -804,6 +810,8 @@ let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t) (** Simply calls [update_intersecting_aproj_borrows] to remove the proj_borrows over shared values. + + This is a helper function: it might break invariants. *) let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = @@ -817,6 +825,8 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) (** Updates the proj_loans intersecting some projection. + This is a helper function: it might break invariants. + Note that in practice, when we update a proj_loans, we always update exactly one aproj_loans, in a specific abstraction. |