From 239435fc667fa0d18979e603ce3fd4caa128cd54 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 23 May 2024 23:21:12 +0200 Subject: Update the interpreter so that it is not written in CPS style (#120) * Start turning the compiler in a style which is less CPS * Update a function in InterpreterExpressions.ml * WIP work on cps * WIP * WIP, currently on InterpreterStatements.ml * WIP * Finished CPS-related modification * Fixed some warning related to documentation comments * Finished loop support, fixed a loop * fixed a typed value * Fixed check_disappeared related error * cleaned check_disappeared related error * Start cleaning up * Do more cleanup * Make some cleanup and fix an issue * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Rename a function * Do more cleanup * Cleanup the loops code and fix some bugs * Cleanup assign_to_place * Make a minor cleanup --------- Co-authored-by: Son Ho --- compiler/InterpreterBorrows.ml | 362 +++++++++++++++++++---------------------- 1 file changed, 165 insertions(+), 197 deletions(-) (limited to 'compiler/InterpreterBorrows.ml') diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index a158ed9a..f49d39d0 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -826,34 +826,29 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) craise __FILE__ __LINE__ meta "Unreachable" let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) - (l : BorrowId.id) (ctx0 : eval_ctx) : cm_fun = - let check_disappeared (ctx : eval_ctx) : unit = - let _ = - match lookup_borrow_opt ek_all l ctx with - | None -> () (* Ok *) - | Some _ -> - log#ltrace - (lazy - (fun_name ^ ": " ^ BorrowId.to_string l - ^ ": borrow didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - internal_error __FILE__ __LINE__ meta - in - match lookup_loan_opt meta ek_all l ctx with - | None -> () (* Ok *) - | Some _ -> - log#ltrace - (lazy - (fun_name ^ ": " ^ BorrowId.to_string l - ^ ": loan didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - internal_error __FILE__ __LINE__ meta - in - unit_to_cm_fun check_disappeared + (l : BorrowId.id) (ctx0 : eval_ctx) (ctx : eval_ctx) : unit = + (match lookup_borrow_opt ek_all l ctx with + | None -> () (* Ok *) + | Some _ -> + log#ltrace + (lazy + (fun_name ^ ": " ^ BorrowId.to_string l + ^ ": borrow didn't disappear:\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + internal_error __FILE__ __LINE__ meta); + match lookup_loan_opt meta ek_all l ctx with + | None -> () (* Ok *) + | Some _ -> + log#ltrace + (lazy + (fun_name ^ ": " ^ BorrowId.to_string l + ^ ": loan didn't disappear:\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + internal_error __FILE__ __LINE__ meta (** End a borrow identified by its borrow id in a context. @@ -879,7 +874,7 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Check that we don't loop *) let chain0 = chain in let chain = @@ -893,7 +888,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (* Utility function for the sanity checks: check that the borrow disappeared * from the context *) let ctx0 = ctx in - let cf_check : cm_fun = check_borrow_disappeared meta "end borrow" l ctx0 in + let check = check_borrow_disappeared meta "end borrow" l ctx0 in (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *) let allow_inner_loans = false in match end_borrow_get_borrow meta allowed_abs allow_inner_loans l ctx with @@ -925,31 +920,41 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) * inside another borrow *) let allowed_abs' = None in (* End the outer borrows *) - let cc = end_borrows_aux config meta chain allowed_abs' bids in + let ctx, cc = + end_borrows_aux config meta chain allowed_abs' bids ctx + in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in - (* Check and apply *) - comp cc cf_check cf ctx + let ctx, cc = + comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx) + in + (* Check and continue *) + check ctx; + (ctx, cc) | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> let allowed_abs' = None in (* End the outer borrow *) - let cc = end_borrow_aux config meta chain allowed_abs' bid in + let ctx, cc = end_borrow_aux config meta chain allowed_abs' bid ctx in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in - (* Check and apply *) - comp cc cf_check cf ctx + let ctx, cc = + comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx) + in + (* Check and continue *) + check ctx; + (ctx, cc) | OuterAbs abs_id -> (* The borrow is inside an abstraction: end the whole abstraction *) - let cf_end_abs = end_abstraction_aux config meta chain abs_id in - (* Compose with a sanity check *) - comp cf_end_abs cf_check cf ctx) + let ctx, end_abs = end_abstraction_aux config meta chain abs_id ctx in + (* Sanity check *) + check ctx; + (ctx, end_abs)) | 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 *) sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; (* Do a sanity check and continue *) - cf_check cf ctx + check ctx; + (ctx, fun e -> e) (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update the corresponding loan) *) | Ok (ctx, Some (_, bc)) -> @@ -963,27 +968,27 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (* Give back the value *) let ctx = give_back config meta l bc ctx in (* Do a sanity check and continue *) - let cc = cf_check in + check ctx; (* Save a snapshot of the environment for the name generation *) - let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in + let cc = SynthesizeSymbolic.save_snapshot ctx in (* Compose *) - cc cf ctx + (ctx, cc) and end_borrows_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun = - fun cf -> + fun ctx -> (* This is not necessary, but we prefer to reorder the borrow ids, - * so that we actually end from the smallest id to the highest id - just - * a matter of taste, and may make debugging easier *) + so that we actually end from the smallest id to the highest id - just + a matter of taste, and may make debugging easier *) let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in - List.fold_left - (fun cf id -> end_borrow_aux config meta chain allowed_abs id cf) - cf ids + fold_left_apply_continuation + (fun id ctx -> end_borrow_aux config meta chain allowed_abs id ctx) + ids ctx and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Check that we don't loop *) let chain = add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id) @@ -1009,7 +1014,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) ("abs not found (already ended): " ^ AbstractionId.to_string abs_id ^ "\n")); - cf ctx + (ctx, fun e -> e) | Some abs -> (* Check that we can end the abstraction *) if abs.can_end then () @@ -1020,86 +1025,78 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) ^ " as it is set as non-endable"); (* End the parent abstractions first *) - let cc = end_abstractions_aux config meta chain abs.parents in - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("end_abstraction_aux: " - ^ AbstractionId.to_string abs_id - ^ "\n- context after parent abstractions ended:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) - in + let ctx, cc = end_abstractions_aux config meta chain abs.parents ctx in + log#ldebug + (lazy + ("end_abstraction_aux: " + ^ AbstractionId.to_string abs_id + ^ "\n- context after parent abstractions ended:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* End the loans inside the abstraction *) - let cc = comp cc (end_abstraction_loans config meta chain abs_id) in - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("end_abstraction_aux: " - ^ AbstractionId.to_string abs_id - ^ "\n- context after loans ended:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) + let ctx, cc = + comp cc (end_abstraction_loans config meta chain abs_id ctx) in + log#ldebug + (lazy + ("end_abstraction_aux: " + ^ AbstractionId.to_string abs_id + ^ "\n- context after loans ended:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* End the abstraction itself by redistributing the borrows it contains *) - let cc = comp cc (end_abstraction_borrows config meta chain abs_id) in + let ctx, cc = + comp cc (end_abstraction_borrows config meta chain abs_id ctx) + in (* End the regions owned by the abstraction - note that we don't need to - * relookup the abstraction: the set of regions in an abstraction never - * changes... *) - let cc = - comp_update cc (fun ctx -> - let ended_regions = - RegionId.Set.union ctx.ended_regions abs.regions - in - { ctx with ended_regions }) + relookup the abstraction: the set of regions in an abstraction never + changes... *) + let ctx = + let ended_regions = RegionId.Set.union ctx.ended_regions abs.regions in + { ctx with ended_regions } in (* Remove all the references to the id of the current abstraction, and remove - * the abstraction itself. - * **Rk.**: this is where we synthesize the updated symbolic AST *) - let cc = - comp cc (end_abstraction_remove_from_context config meta abs_id) + the abstraction itself. + **Rk.**: this is where we synthesize the updated symbolic AST *) + let ctx, cc = + comp cc (end_abstraction_remove_from_context config meta abs_id ctx) in (* Debugging *) - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("end_abstraction_aux: " - ^ AbstractionId.to_string abs_id - ^ "\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) - in + log#ldebug + (lazy + ("end_abstraction_aux: " + ^ AbstractionId.to_string abs_id + ^ "\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Sanity check: ending an abstraction must preserve the invariants *) - let cc = comp cc (Invariants.cf_check_invariants meta) in + Invariants.check_invariants meta ctx; (* Save a snapshot of the environment for the name generation *) - let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in + let cc = cc_comp cc (SynthesizeSymbolic.save_snapshot ctx) in - (* Apply the continuation *) - cc cf ctx + (* Return *) + (ctx, cc) and end_abstractions_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_ids : AbstractionId.Set.t) : cm_fun = - fun cf -> + fun ctx -> (* This is not necessary, but we prefer to reorder the abstraction ids, * so that we actually end from the smallest id to the highest id - just * a matter of taste, and may make debugging easier *) let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in - List.fold_left - (fun cf id -> end_abstraction_aux config meta chain id cf) - cf abs_ids + fold_left_apply_continuation + (fun id ctx -> end_abstraction_aux config meta chain id ctx) + abs_ids ctx and end_abstraction_loans (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Lookup the abstraction *) let abs = ctx_lookup_abs ctx abs_id in (* End the first loan we find. @@ -1110,32 +1107,28 @@ and end_abstraction_loans (config : config) (meta : Meta.meta) match opt_loan with | None -> (* No loans: nothing to update *) - cf ctx + (ctx, fun e -> e) | Some (BorrowIds bids) -> (* There are loans: end the corresponding borrows, then recheck *) - let cc : cm_fun = + let ctx, cc = match bids with - | Borrow bid -> end_borrow_aux config meta chain None bid - | Borrows bids -> end_borrows_aux config meta chain None bids + | Borrow bid -> end_borrow_aux config meta chain None bid ctx + | Borrows bids -> end_borrows_aux config meta chain None bids ctx in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config meta chain abs_id) in - (* Continue *) - cc cf ctx + comp cc (end_abstraction_loans config meta chain abs_id ctx) | Some (SymbolicValue sv) -> (* There is a proj_loans over a symbolic value: end the proj_borrows - * which intersect this proj_loans, then end the proj_loans itself *) - let cc = - end_proj_loans_symbolic config meta chain abs_id abs.regions sv + which intersect this proj_loans, then end the proj_loans itself *) + let ctx, cc = + end_proj_loans_symbolic config meta chain abs_id abs.regions sv ctx in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config meta chain abs_id) in - (* Continue *) - cc cf ctx + comp cc (end_abstraction_loans config meta chain abs_id ctx) and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("end_abstraction_borrows: abs_id: " ^ AbstractionId.to_string abs_id)); @@ -1202,7 +1195,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (* Explore the abstraction, looking for borrows *) obj#visit_abs () abs; (* No borrows: nothing to update *) - cf ctx + (ctx, fun e -> e) with (* There are concrete (i.e., not symbolic) borrows: end them, then reexplore *) | FoundABorrowContent bc -> @@ -1256,7 +1249,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) craise __FILE__ __LINE__ meta "Unexpected" in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> log#ldebug @@ -1273,7 +1266,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) give_back_symbolic_value config meta abs.regions proj_ty sv nsv ctx in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id ctx (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *) | FoundBorrowContent bc -> log#ldebug @@ -1306,18 +1299,16 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable" in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id ctx (** Remove an abstraction from the context, as well as all its references *) and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> let ctx, abs = ctx_remove_abs meta ctx abs_id in let abs = Option.get abs in - (* Apply the continuation *) - let expr = cf ctx in (* Synthesize the symbolic AST *) - SynthesizeSymbolic.synthesize_end_abstraction ctx abs expr + (ctx, SynthesizeSymbolic.synthesize_end_abstraction ctx abs) (** End a proj_loan over a symbolic value by ending the proj_borrows which intersect this proj_loans. @@ -1336,14 +1327,9 @@ and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta) and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value) : cm_fun = - fun cf ctx -> + fun ctx -> (* Small helpers for sanity checks *) let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in - let cf_check (cf : m_fun) : m_fun = - fun ctx -> - check ctx; - cf ctx - in (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in match @@ -1358,7 +1344,7 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (* Sanity check *) check ctx; (* Continue *) - cf ctx + (ctx, fun e -> e) | Some (SharedProjs projs) -> (* We found projectors over shared values - split between the projectors which belong to the current abstraction and the others. @@ -1389,8 +1375,7 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) List.partition (fun (abs_id', _) -> abs_id' = abs_id) projs in (* End the external borrow projectors (end their abstractions) *) - let cf_end_external : cm_fun = - fun cf ctx -> + let ctx, cc = let abs_ids = List.map fst external_projs in let abs_ids = List.fold_left @@ -1398,25 +1383,20 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) AbstractionId.Set.empty abs_ids in (* End the abstractions and continue *) - end_abstractions_aux config meta chain abs_ids cf ctx + end_abstractions_aux config meta chain abs_ids ctx in (* End the internal borrows projectors and the loans projector *) - let cf_end_internal : cm_fun = - fun cf ctx -> + let ctx = (* All the proj_borrows are owned: simply erase them *) let ctx = remove_intersecting_aproj_borrows_shared meta regions sv ctx in (* End the loan itself *) - let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in - (* Sanity check *) - check ctx; - (* Continue *) - cf ctx + update_aproj_loans_to_ended meta abs_id sv ctx in - (* Compose and apply *) - let cc = comp cf_end_external cf_end_internal in - cc cf ctx + (* Sanity check *) + check ctx; + (ctx, cc) | Some (NonSharedProj (abs_id', _proj_ty)) -> (* We found one projector of borrows in an abstraction: if it comes * from this abstraction, we can end it directly, otherwise we need @@ -1452,18 +1432,19 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (* Sanity check *) check ctx; (* Continue *) - cf ctx) + (ctx, fun e -> e)) else (* The borrows proj comes from a different abstraction: end it. *) - let cc = end_abstraction_aux config meta chain abs_id' in + let ctx, cc = end_abstraction_aux config meta chain abs_id' ctx in (* Retry ending the projector of loans *) - let cc = - comp cc (end_proj_loans_symbolic config meta chain abs_id regions sv) + let ctx, cc = + comp cc + (end_proj_loans_symbolic config meta chain abs_id regions sv ctx) in (* Sanity check *) - let cc = comp cc cf_check in - (* Continue *) - cc cf ctx + check ctx; + (* Return *) + (ctx, cc) let end_borrow config (meta : Meta.meta) : BorrowId.id -> cm_fun = end_borrow_aux config meta [] None @@ -1473,18 +1454,16 @@ let end_borrows config (meta : Meta.meta) : BorrowId.Set.t -> cm_fun = let end_abstraction config meta = end_abstraction_aux config meta [] let end_abstractions config meta = end_abstractions_aux config meta [] - -let end_borrow_no_synth config meta id ctx = - get_cf_ctx_no_synth meta (end_borrow config meta id) ctx +let end_borrow_no_synth config meta id ctx = fst (end_borrow config meta id ctx) let end_borrows_no_synth config meta ids ctx = - get_cf_ctx_no_synth meta (end_borrows config meta ids) ctx + fst (end_borrows config meta ids ctx) let end_abstraction_no_synth config meta id ctx = - get_cf_ctx_no_synth meta (end_abstraction config meta id) ctx + fst (end_abstraction config meta id ctx) let end_abstractions_no_synth config meta ids ctx = - get_cf_ctx_no_synth meta (end_abstractions config meta ids) ctx + fst (end_abstractions config meta ids ctx) (** Helper function: see {!activate_reserved_mut_borrow}. @@ -1503,8 +1482,7 @@ let end_abstractions_no_synth config meta ids ctx = The loan to update mustn't be a borrowed value. *) let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : typed_value * eval_ctx = (* Debug *) log#ldebug (lazy @@ -1541,11 +1519,11 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) meta "There shouldn't be reserved borrows"; (* Update the loan content *) let ctx = update_loan meta ek l (VMutLoan l) ctx in - (* Continue *) - cf sv ctx + (* Return *) + (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. *) + returned by abstractions. I'm not sure how we could handle that anyway. *) craise __FILE__ __LINE__ meta "Can't promote a shared loan to a mutable loan if the loan is inside a \ region abstraction" @@ -1556,34 +1534,29 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) all: it doesn't touch the corresponding loan). *) let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) - (cf : m_fun) (borrowed_value : typed_value) : m_fun = - fun ctx -> + (borrowed_value : typed_value) (ctx : eval_ctx) : eval_ctx = (* Lookup the reserved borrow - note that we don't go inside borrows/loans: there can't be reserved borrows inside other borrows/loans *) let ek = { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in - let ctx = - match lookup_borrow meta ek l ctx with - | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> - craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow" - | Concrete (VReservedMutBorrow _) -> - (* Update it *) - update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx - | Abstract _ -> - (* This can't happen for sure *) - craise __FILE__ __LINE__ meta - "Can't promote a shared borrow to a mutable borrow if the borrow is \ - inside a region abstraction" - in - (* Continue *) - cf ctx + match lookup_borrow meta ek l ctx with + | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> + craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow" + | Concrete (VReservedMutBorrow _) -> + (* Update it *) + update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx + | Abstract _ -> + (* This can't happen for sure *) + craise __FILE__ __LINE__ meta + "Can't promote a shared borrow to a mutable borrow if the borrow is \ + inside a region abstraction" (** Promote a reserved mut borrow to a mut borrow. *) let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : BorrowId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Lookup the value *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } @@ -1597,15 +1570,13 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) match get_first_loan_in_value sv with | Some lc -> (* End the loans *) - let cc = + let ctx, cc = match lc with - | VSharedLoan (bids, _) -> end_borrows config meta bids - | VMutLoan bid -> end_borrow config meta bid + | VSharedLoan (bids, _) -> end_borrows config meta bids ctx + | VMutLoan bid -> end_borrow config meta bid ctx in (* Recursive call *) - let cc = comp cc (promote_reserved_mut_borrow config meta l) in - (* Continue *) - cc cf ctx + comp cc (promote_reserved_mut_borrow config meta l ctx) | None -> (* No loan to end inside the value *) (* Some sanity checks *) @@ -1621,21 +1592,18 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) let bids = BorrowId.Set.remove l bids in - let cc = end_borrows config meta bids in + let ctx, cc = end_borrows config meta bids ctx in (* Promote the loan - TODO: this will fail if the value contains * any loans. In practice, it shouldn't, but we could also * look for loans inside the value and end them before promoting * the borrow. *) - let cc = comp cc (promote_shared_loan_to_mut_loan meta l) in + let v, ctx = promote_shared_loan_to_mut_loan meta l ctx in (* Promote the borrow - the value should have been checked by {!promote_shared_loan_to_mut_loan} *) - let cc = - comp cc (fun cf borrowed_value -> - replace_reserved_borrow_with_mut_borrow meta l cf borrowed_value) - in - (* Continue *) - cc cf ctx) + let ctx = replace_reserved_borrow_with_mut_borrow meta l v ctx in + (* Return *) + (ctx, cc)) | _, 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. *) -- cgit v1.2.3 From b294639a5cbd2a51fc5bb5e55e0c386ee568ca8c Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 24 May 2024 13:28:12 +0200 Subject: Rename meta into span --- compiler/InterpreterBorrows.ml | 620 ++++++++++++++++++++--------------------- 1 file changed, 310 insertions(+), 310 deletions(-) (limited to 'compiler/InterpreterBorrows.ml') diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index f49d39d0..ef958d2c 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -30,7 +30,7 @@ let log = Logging.borrows_log loans. This is used to merge borrows with abstractions, to compute loop fixed points for instance. *) -let end_borrow_get_borrow (meta : Meta.meta) +let end_borrow_get_borrow (span : Meta.span) (allowed_abs : AbstractionId.id option) (allow_inner_loans : bool) (l : BorrowId.id) (ctx : eval_ctx) : ( eval_ctx * (AbstractionId.id option * g_borrow_content) option, @@ -43,7 +43,7 @@ let end_borrow_get_borrow (meta : Meta.meta) in let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content) = - sanity_check __FILE__ __LINE__ (Option.is_none !replaced_bc) meta; + sanity_check __FILE__ __LINE__ (Option.is_none !replaced_bc) span; replaced_bc := Some (abs_id, bc) in (* Raise an exception if: @@ -146,12 +146,12 @@ let end_borrow_get_borrow (meta : Meta.meta) let av = super#visit_typed_avalue outer av in (* Reconstruct *) ALoan (ASharedLoan (bids, v, av)) - | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan _ (* The loan has ended, so no need to update the outer borrows *) | AIgnoredMutLoan _ (* Nothing special to do *) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } (* Nothing special to do *) | AIgnoredSharedLoan _ -> (* Nothing special to do *) @@ -182,7 +182,7 @@ let end_borrow_get_borrow (meta : Meta.meta) * Also note that, as we are moving the borrowed value inside the * abstraction (and not really giving the value back to the context) * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *) - craise __FILE__ __LINE__ meta "Unimplemented" + craise __FILE__ __LINE__ span "Unimplemented" (* ABottom *)) else (* Update the outer borrows before diving into the child avalue *) @@ -203,7 +203,7 @@ let end_borrow_get_borrow (meta : Meta.meta) | AIgnoredMutBorrow (_, _) | AEndedMutBorrow _ | AEndedIgnoredMutBorrow - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AEndedSharedBorrow -> (* Nothing special to do *) super#visit_ABorrow outer bc @@ -217,7 +217,7 @@ let end_borrow_get_borrow (meta : Meta.meta) set_replaced_bc (fst outer) (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 meta l asb in + let asb = remove_borrow_from_asb span l asb in ABorrow (AProjSharedBorrow asb)) else (* Nothing special to do *) super#visit_ABorrow outer bc @@ -225,8 +225,8 @@ let end_borrow_get_borrow (meta : Meta.meta) method! visit_abs outer abs = (* Update the outer abs *) let outer_abs, outer_borrows = outer in - sanity_check __FILE__ __LINE__ (Option.is_none outer_abs) meta; - sanity_check __FILE__ __LINE__ (Option.is_none outer_borrows) meta; + sanity_check __FILE__ __LINE__ (Option.is_none outer_abs) span; + sanity_check __FILE__ __LINE__ (Option.is_none outer_borrows) span; let outer = (Some abs.abs_id, None) in super#visit_abs outer abs end @@ -246,27 +246,27 @@ let end_borrow_get_borrow (meta : Meta.meta) give the value back. TODO: this was not the case before, so some sanity checks are not useful anymore. *) -let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) +let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) (nv : typed_value) (ctx : eval_ctx) : eval_ctx = (* Sanity check *) exec_assert __FILE__ __LINE__ (not (loans_in_value nv)) - meta "Can not end a borrow because the value to give back contains bottom"; + span "Can not end a borrow because the value to give back contains bottom"; exec_assert __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions nv)) - meta "Can not end a borrow because the value to give back contains bottom"; + span "Can not end a borrow because the value to give back contains bottom"; (* Debug *) log#ldebug (lazy ("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: " - ^ typed_value_to_string ~meta:(Some meta) ctx nv + ^ typed_value_to_string ~span:(Some span) ctx nv ^ "\n- context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n")); (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - sanity_check __FILE__ __LINE__ (not !replaced) meta; + sanity_check __FILE__ __LINE__ (not !replaced) span; replaced := true in (* Whenever giving back symbolic values, they shouldn't contain already ended regions *) @@ -274,7 +274,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* 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 meta allow_reborrows + prepare_reborrows config span allow_reborrows in (* The visitor to give back the values *) let obj = @@ -304,7 +304,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* Sanity check *) let expected_ty = ty in if nv.ty <> expected_ty then - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Value given back doesn't have the proper type:\n\ - expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); @@ -338,10 +338,10 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) match nv.value with | VSymbolic sv -> let abs = Option.get opt_abs in - (* Remember the given back value as a meta-value + (* Remember the given back value as a span-value * TODO: it is a bit annoying to have to deconstruct * the value... Think about a more elegant way. *) - let given_back_meta = as_symbolic meta nv.value in + let given_back_span = as_symbolic span nv.value in (* The loan projector *) let given_back = mk_aproj_loans_value_from_symbolic_value abs.regions sv @@ -351,8 +351,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* Return *) ABorrow (AEndedIgnoredMutBorrow - { given_back; child; given_back_meta }) - | _ -> craise __FILE__ __LINE__ meta "Unreachable" + { given_back; child; given_back_span }) + | _ -> craise __FILE__ __LINE__ span "Unreachable" else (* Continue exploring *) ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child) @@ -367,7 +367,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* Preparing a bit *) let regions, ancestors_regions = match opt_abs with - | None -> craise __FILE__ __LINE__ meta "Unreachable" + | None -> craise __FILE__ __LINE__ span "Unreachable" | Some abs -> (abs.regions, abs.ancestors_regions) in (* Rk.: there is a small issue with the types of the aloan values. @@ -384,23 +384,23 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) * an ended loan *) (* Register the insertion *) set_replaced (); - (* Remember the given back value as a meta-value *) - let given_back_meta = nv in + (* Remember the given back value as a span-value *) + let given_back_span = nv in (* Apply the projection *) let given_back = - apply_proj_borrows meta check_symbolic_no_ended ctx + apply_proj_borrows span check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions nv borrowed_value_aty in (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in (* Return the new value *) - ALoan (AEndedMutLoan { child; given_back; given_back_meta })) + ALoan (AEndedMutLoan { child; given_back; given_back_span })) else (* Continue exploring *) super#visit_ALoan opt_abs lc | ASharedLoan (_, _, _) -> (* We are giving back a value to a *mutable* loan: nothing special to do *) super#visit_ALoan opt_abs lc - | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ } + | AEndedMutLoan { child = _; given_back = _; given_back_span = _ } | AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -408,23 +408,23 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* This loan is ignored, but we may have to project on a subvalue * of the value which is given back *) if opt_bid = Some bid then - (* Remember the given back value as a meta-value *) - let given_back_meta = nv in + (* Remember the given back value as a span-value *) + let given_back_span = nv in (* 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 meta check_symbolic_no_ended ctx + apply_proj_borrows span check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions nv borrowed_value_aty in (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in ALoan - (AEndedIgnoredMutLoan { given_back; child; given_back_meta }) + (AEndedIgnoredMutLoan { given_back; child; given_back_span }) else super#visit_ALoan opt_abs lc | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AIgnoredSharedLoan _ -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -433,7 +433,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* We remember in which abstraction we are before diving - * this is necessary for projecting values: we need to know * over which regions to project *) - sanity_check __FILE__ __LINE__ (Option.is_none opt_abs) meta; + sanity_check __FILE__ __LINE__ (Option.is_none opt_abs) span; super#visit_EAbs (Some abs) abs end in @@ -441,19 +441,19 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta "No loan updated"; + cassert __FILE__ __LINE__ !replaced span "No loan updated"; (* Apply the reborrows *) apply_registered_reborrows ctx (** Give back a *modified* symbolic value. *) -let give_back_symbolic_value (_config : config) (meta : Meta.meta) +let give_back_symbolic_value (_config : config) (span : Meta.span) (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Sanity checks *) sanity_check __FILE__ __LINE__ (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) - meta; - (* Store the given-back value as a meta-value for synthesis purposes *) + span; + (* Store the given-back value as a span-value for synthesis purposes *) let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) let subst (_abs : abs) local_given_back = @@ -474,11 +474,11 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) type [T]! We thus *mustn't* introduce a projector here. *) (* AProjBorrows (nsv, sv.sv_ty) *) - internal_error __FILE__ __LINE__ meta + internal_error __FILE__ __LINE__ span in AProjLoans (sv, (mv, child_proj) :: local_given_back) in - update_intersecting_aproj_loans meta proj_regions proj_ty sv subst ctx + update_intersecting_aproj_loans span proj_regions proj_ty sv subst ctx (** Auxiliary function to end borrows. See {!give_back}. @@ -493,13 +493,13 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) end abstraction when ending this abstraction. When doing this, we need to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values. *) -let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) +let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span) (bid : BorrowId.id) (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - cassert __FILE__ __LINE__ (not !replaced) meta + cassert __FILE__ __LINE__ (not !replaced) span "Exacly one loan should be updated"; replaced := true in @@ -539,7 +539,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) * {!typed_avalue} *) let _, expected_ty, _ = ty_get_ref ty in if nv.ty <> expected_ty then - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Value given back doesn't have the proper type:\n\ - expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); @@ -550,12 +550,12 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) set_replaced (); (* Return the new value *) ALoan - (AEndedMutLoan { given_back = nv; child; given_back_meta = nsv })) + (AEndedMutLoan { given_back = nv; child; given_back_span = nsv })) else (* Continue exploring *) super#visit_ALoan opt_abs lc | ASharedLoan (_, _, _) (* We are giving back a value to a *mutable* loan: nothing special to do *) - | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -568,13 +568,13 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) * we don't register the fact that we inserted the value somewhere * (i.e., we don't call {!set_replaced}) *) (* Sanity check *) - sanity_check __FILE__ __LINE__ (nv.ty = ty) meta; + sanity_check __FILE__ __LINE__ (nv.ty = ty) span; ALoan (AEndedIgnoredMutLoan - { given_back = nv; child; given_back_meta = nsv })) + { given_back = nv; child; given_back_span = nsv })) else super#visit_ALoan opt_abs lc | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AIgnoredSharedLoan _ -> (* Nothing special to do *) super#visit_ALoan opt_abs lc @@ -584,7 +584,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta "No loan updated"; + cassert __FILE__ __LINE__ !replaced span "No loan updated"; (* Return *) ctx @@ -597,12 +597,12 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) we update. TODO: this was not the case before, so some sanity checks are not useful anymore. *) -let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) +let give_back_shared _config (span : Meta.span) (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - cassert __FILE__ __LINE__ (not !replaced) meta + cassert __FILE__ __LINE__ (not !replaced) span "Exactly one loan should be updated"; replaced := true in @@ -650,14 +650,14 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) else (* Not the loan we are looking for: continue exploring *) super#visit_ALoan opt_abs lc - | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } (* Nothing special to do (the loan has ended) *) | AEndedSharedLoan (_, _) (* Nothing special to do (the loan has ended) *) | AIgnoredMutLoan (_, _) (* Nothing special to do (we are giving back a *shared* borrow) *) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } (* Nothing special to do *) | AIgnoredSharedLoan _ -> (* Nothing special to do *) @@ -668,7 +668,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - cassert __FILE__ __LINE__ !replaced meta "No loan updated"; + cassert __FILE__ __LINE__ !replaced span "No loan updated"; (* Return *) ctx @@ -677,12 +677,12 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) 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 (meta : Meta.meta) (original_bid : BorrowId.id) +let reborrow_shared (span : Meta.span) (original_bid : BorrowId.id) (new_bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = (* Keep track of changes *) let r = ref false in let set_ref () = - sanity_check __FILE__ __LINE__ (not !r) meta; + sanity_check __FILE__ __LINE__ (not !r) span; r := true in @@ -712,7 +712,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) let env = obj#visit_env () ctx.env in (* Check that we reborrowed once *) - sanity_check __FILE__ __LINE__ !r meta; + sanity_check __FILE__ __LINE__ !r span; { ctx with env } (** Convert an {!type:avalue} to a {!type:value}. @@ -731,9 +731,9 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) be expanded (because expanding this symbolic value would require expanding a reference whose region has already ended). *) -let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) : +let convert_avalue_to_given_back_value (span : Meta.span) (av : typed_avalue) : symbolic_value = - mk_fresh_symbolic_value meta av.ty + mk_fresh_symbolic_value span av.ty (** Auxiliary function: see {!end_borrow_aux}. @@ -751,19 +751,19 @@ let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) : borrows. This kind of internal reshuffling. should be similar to ending abstractions (it is tantamount to ending *sub*-abstractions). *) -let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) +let give_back (config : config) (span : Meta.span) (l : BorrowId.id) (bc : g_borrow_content) (ctx : eval_ctx) : eval_ctx = (* Debug *) log#ldebug (lazy (let bc = match bc with - | Concrete bc -> borrow_content_to_string ~meta:(Some meta) ctx bc - | Abstract bc -> aborrow_content_to_string ~meta:(Some meta) ctx bc + | Concrete bc -> borrow_content_to_string ~span:(Some span) ctx bc + | Abstract bc -> aborrow_content_to_string ~span:(Some span) ctx bc in "give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc ^ "\n- context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n")); (* This is used for sanity checks *) let sanity_ek = @@ -772,60 +772,60 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) match bc with | Concrete (VMutBorrow (l', tv)) -> (* Sanity check *) - sanity_check __FILE__ __LINE__ (l' = l) meta; - sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) meta; + sanity_check __FILE__ __LINE__ (l' = l) span; + sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) span; (* Check that the corresponding loan is somewhere - purely a sanity check *) sanity_check __FILE__ __LINE__ - (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) - meta; + (Option.is_some (lookup_loan_opt span sanity_ek l ctx)) + span; (* Update the context *) - give_back_value config meta l tv ctx + give_back_value config span l tv ctx | Concrete (VSharedBorrow l' | VReservedMutBorrow l') -> (* Sanity check *) - sanity_check __FILE__ __LINE__ (l' = l) meta; + sanity_check __FILE__ __LINE__ (l' = l) span; (* Check that the borrow is somewhere - purely a sanity check *) sanity_check __FILE__ __LINE__ - (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) - meta; + (Option.is_some (lookup_loan_opt span sanity_ek l ctx)) + span; (* Update the context *) - give_back_shared config meta l ctx + give_back_shared config span l ctx | Abstract (AMutBorrow (l', av)) -> (* Sanity check *) - sanity_check __FILE__ __LINE__ (l' = l) meta; + sanity_check __FILE__ __LINE__ (l' = l) span; (* Check that the corresponding loan is somewhere - purely a sanity check *) sanity_check __FILE__ __LINE__ - (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) - meta; + (Option.is_some (lookup_loan_opt span sanity_ek l ctx)) + span; (* Convert the avalue to a (fresh symbolic) value. Rem.: we shouldn't do this here. We should do this in a function which takes care of ending *sub*-abstractions. *) - let sv = convert_avalue_to_given_back_value meta av in + let sv = convert_avalue_to_given_back_value span av in (* Update the context *) - give_back_avalue_to_same_abstraction config meta l av + give_back_avalue_to_same_abstraction config span l av (mk_typed_value_from_symbolic_value sv) ctx | Abstract (ASharedBorrow l') -> (* Sanity check *) - sanity_check __FILE__ __LINE__ (l' = l) meta; + sanity_check __FILE__ __LINE__ (l' = l) span; (* Check that the borrow is somewhere - purely a sanity check *) sanity_check __FILE__ __LINE__ - (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) - meta; + (Option.is_some (lookup_loan_opt span sanity_ek l ctx)) + span; (* Update the context *) - give_back_shared config meta l ctx + give_back_shared config span l ctx | Abstract (AProjSharedBorrow asb) -> (* Sanity check *) - sanity_check __FILE__ __LINE__ (borrow_in_asb l asb) meta; + sanity_check __FILE__ __LINE__ (borrow_in_asb l asb) span; (* Update the context *) - give_back_shared config meta l ctx + give_back_shared config span l ctx | Abstract ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow ) -> - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" -let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) +let check_borrow_disappeared (span : Meta.span) (fun_name : string) (l : BorrowId.id) (ctx0 : eval_ctx) (ctx : eval_ctx) : unit = (match lookup_borrow_opt ek_all l ctx with | None -> () (* Ok *) @@ -834,21 +834,21 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": borrow didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ eval_ctx_to_string ~span:(Some span) ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - internal_error __FILE__ __LINE__ meta); - match lookup_loan_opt meta ek_all l ctx with + ^ eval_ctx_to_string ~span:(Some span) ctx)); + internal_error __FILE__ __LINE__ span); + match lookup_loan_opt span ek_all l ctx with | None -> () (* Ok *) | Some _ -> log#ltrace (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": loan didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ eval_ctx_to_string ~span:(Some span) ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - internal_error __FILE__ __LINE__ meta + ^ eval_ctx_to_string ~span:(Some span) ctx)); + internal_error __FILE__ __LINE__ span (** End a borrow identified by its borrow id in a context. @@ -871,27 +871,27 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) perform anything smart and is trusted, and another function for the book-keeping. *) -let rec end_borrow_aux (config : config) (meta : Meta.meta) +let rec end_borrow_aux (config : config) (span : Meta.span) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun = fun ctx -> (* Check that we don't loop *) let chain0 = chain in let chain = - add_borrow_or_abs_id_to_chain meta "end_borrow_aux: " (BorrowId l) chain + add_borrow_or_abs_id_to_chain span "end_borrow_aux: " (BorrowId l) chain in log#ldebug (lazy ("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Utility function for the sanity checks: check that the borrow disappeared * from the context *) let ctx0 = ctx in - let check = check_borrow_disappeared meta "end borrow" l ctx0 in + let check = check_borrow_disappeared span "end borrow" l ctx0 in (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *) let allow_inner_loans = false in - match end_borrow_get_borrow meta allowed_abs allow_inner_loans l ctx with + match end_borrow_get_borrow span allowed_abs allow_inner_loans l ctx with (* Two cases: - error: we found outer borrows (the borrow is inside a borrowed value) or inner loans (the borrow contains loans) @@ -921,11 +921,11 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) let allowed_abs' = None in (* End the outer borrows *) let ctx, cc = - end_borrows_aux config meta chain allowed_abs' bids ctx + end_borrows_aux config span chain allowed_abs' bids ctx in (* Retry to end the borrow *) let ctx, cc = - comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx) + comp cc (end_borrow_aux config span chain0 allowed_abs l ctx) in (* Check and continue *) check ctx; @@ -933,17 +933,17 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> let allowed_abs' = None in (* End the outer borrow *) - let ctx, cc = end_borrow_aux config meta chain allowed_abs' bid ctx in + let ctx, cc = end_borrow_aux config span chain allowed_abs' bid ctx in (* Retry to end the borrow *) let ctx, cc = - comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx) + comp cc (end_borrow_aux config span chain0 allowed_abs l ctx) in (* Check and continue *) check ctx; (ctx, cc) | OuterAbs abs_id -> (* The borrow is inside an abstraction: end the whole abstraction *) - let ctx, end_abs = end_abstraction_aux config meta chain abs_id ctx in + let ctx, end_abs = end_abstraction_aux config span chain abs_id ctx in (* Sanity check *) check ctx; (ctx, end_abs)) @@ -951,7 +951,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) 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 *) - sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) span; (* Do a sanity check and continue *) check ctx; (ctx, fun e -> e) @@ -963,10 +963,10 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) | Concrete (VMutBorrow (_, bv)) -> sanity_check __FILE__ __LINE__ (Option.is_none (get_first_loan_in_value bv)) - meta + span | _ -> ()); (* Give back the value *) - let ctx = give_back config meta l bc ctx in + let ctx = give_back config span l bc ctx in (* Do a sanity check and continue *) check ctx; (* Save a snapshot of the environment for the name generation *) @@ -974,7 +974,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (* Compose *) (ctx, cc) -and end_borrows_aux (config : config) (meta : Meta.meta) +and end_borrows_aux (config : config) (span : Meta.span) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun = fun ctx -> @@ -983,15 +983,15 @@ and end_borrows_aux (config : config) (meta : Meta.meta) a matter of taste, and may make debugging easier *) let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in fold_left_apply_continuation - (fun id ctx -> end_borrow_aux config meta chain allowed_abs id ctx) + (fun id ctx -> end_borrow_aux config span chain allowed_abs id ctx) ids ctx -and end_abstraction_aux (config : config) (meta : Meta.meta) +and end_abstraction_aux (config : config) (span : Meta.span) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun ctx -> (* Check that we don't loop *) let chain = - add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id) + add_borrow_or_abs_id_to_chain span "end_abstraction_aux: " (AbsId abs_id) chain in (* Remember the original context for printing purposes *) @@ -1001,7 +1001,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id ^ "\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0)); + ^ eval_ctx_to_string ~span:(Some span) ctx0)); (* Lookup the abstraction - note that if we end a list of abstractions, ending one abstraction may lead to the current abstraction having @@ -1019,34 +1019,34 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (* Check that we can end the abstraction *) if abs.can_end then () else - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span ("Can't end abstraction " ^ AbstractionId.to_string abs.abs_id ^ " as it is set as non-endable"); (* End the parent abstractions first *) - let ctx, cc = end_abstractions_aux config meta chain abs.parents ctx in + let ctx, cc = end_abstractions_aux config span chain abs.parents ctx in log#ldebug (lazy ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id ^ "\n- context after parent abstractions ended:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* End the loans inside the abstraction *) let ctx, cc = - comp cc (end_abstraction_loans config meta chain abs_id ctx) + comp cc (end_abstraction_loans config span chain abs_id ctx) in log#ldebug (lazy ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id ^ "\n- context after loans ended:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* End the abstraction itself by redistributing the borrows it contains *) let ctx, cc = - comp cc (end_abstraction_borrows config meta chain abs_id ctx) + comp cc (end_abstraction_borrows config span chain abs_id ctx) in (* End the regions owned by the abstraction - note that we don't need to @@ -1061,7 +1061,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) the abstraction itself. **Rk.**: this is where we synthesize the updated symbolic AST *) let ctx, cc = - comp cc (end_abstraction_remove_from_context config meta abs_id ctx) + comp cc (end_abstraction_remove_from_context config span abs_id ctx) in (* Debugging *) @@ -1070,12 +1070,12 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id ^ "\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ eval_ctx_to_string ~span:(Some span) ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Sanity check: ending an abstraction must preserve the invariants *) - Invariants.check_invariants meta ctx; + Invariants.check_invariants span ctx; (* Save a snapshot of the environment for the name generation *) let cc = cc_comp cc (SynthesizeSymbolic.save_snapshot ctx) in @@ -1083,7 +1083,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (* Return *) (ctx, cc) -and end_abstractions_aux (config : config) (meta : Meta.meta) +and end_abstractions_aux (config : config) (span : Meta.span) (chain : borrow_or_abs_ids) (abs_ids : AbstractionId.Set.t) : cm_fun = fun ctx -> (* This is not necessary, but we prefer to reorder the abstraction ids, @@ -1091,10 +1091,10 @@ and end_abstractions_aux (config : config) (meta : Meta.meta) * a matter of taste, and may make debugging easier *) let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in fold_left_apply_continuation - (fun id ctx -> end_abstraction_aux config meta chain id ctx) + (fun id ctx -> end_abstraction_aux config span chain id ctx) abs_ids ctx -and end_abstraction_loans (config : config) (meta : Meta.meta) +and end_abstraction_loans (config : config) (span : Meta.span) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun ctx -> (* Lookup the abstraction *) @@ -1103,7 +1103,7 @@ and end_abstraction_loans (config : config) (meta : Meta.meta) * * We ignore the "ignored mut/shared loans": as we should have already ended * the parent abstractions, they necessarily come from children. *) - let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in + let opt_loan = get_first_non_ignored_aloan_in_abstraction span abs in match opt_loan with | None -> (* No loans: nothing to update *) @@ -1112,21 +1112,21 @@ and end_abstraction_loans (config : config) (meta : Meta.meta) (* There are loans: end the corresponding borrows, then recheck *) let ctx, cc = match bids with - | Borrow bid -> end_borrow_aux config meta chain None bid ctx - | Borrows bids -> end_borrows_aux config meta chain None bids ctx + | Borrow bid -> end_borrow_aux config span chain None bid ctx + | Borrows bids -> end_borrows_aux config span chain None bids ctx in (* Reexplore, looking for loans *) - comp cc (end_abstraction_loans config meta chain abs_id ctx) + comp cc (end_abstraction_loans config span chain abs_id ctx) | Some (SymbolicValue sv) -> (* There is a proj_loans over a symbolic value: end the proj_borrows which intersect this proj_loans, then end the proj_loans itself *) let ctx, cc = - end_proj_loans_symbolic config meta chain abs_id abs.regions sv ctx + end_proj_loans_symbolic config span chain abs_id abs.regions sv ctx in (* Reexplore, looking for loans *) - comp cc (end_abstraction_loans config meta chain abs_id ctx) + comp cc (end_abstraction_loans config span chain abs_id ctx) -and end_abstraction_borrows (config : config) (meta : Meta.meta) +and end_abstraction_borrows (config : config) (span : Meta.span) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun ctx -> log#ldebug @@ -1177,7 +1177,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) method! visit_aproj env sproj = (match sproj with - | AProjLoans _ -> craise __FILE__ __LINE__ meta "Unexpected" + | AProjLoans _ -> craise __FILE__ __LINE__ span "Unexpected" | AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty)) | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj env sproj @@ -1186,7 +1186,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) method! visit_borrow_content _ bc = match bc with | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc) - | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable" + | VReservedMutBorrow _ -> craise __FILE__ __LINE__ span "Unreachable" end in (* Lookup the abstraction *) @@ -1202,25 +1202,25 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) log#ldebug (lazy ("end_abstraction_borrows: found aborrow content: " - ^ aborrow_content_to_string ~meta:(Some meta) ctx bc)); + ^ aborrow_content_to_string ~span:(Some span) ctx bc)); let ctx = match bc with | AMutBorrow (bid, av) -> (* First, convert the avalue to a (fresh symbolic) value *) - let sv = convert_avalue_to_given_back_value meta av in + let sv = convert_avalue_to_given_back_value span av in (* Replace the mut borrow to register the fact that we ended * it and store with it the freshly generated given back value *) let ended_borrow = ABorrow (AEndedMutBorrow (sv, av)) in - let ctx = update_aborrow meta ek_all bid ended_borrow ctx in + let ctx = update_aborrow span ek_all bid ended_borrow ctx in (* Give the value back *) let sv = mk_typed_value_from_symbolic_value sv in - give_back_value config meta bid sv ctx + give_back_value config span bid sv ctx | ASharedBorrow bid -> (* Replace the shared borrow to account for the fact it ended *) let ended_borrow = ABorrow AEndedSharedBorrow in - let ctx = update_aborrow meta ek_all bid ended_borrow ctx in + let ctx = update_aborrow span ek_all bid ended_borrow ctx in (* Give back *) - give_back_shared config meta bid ctx + give_back_shared config span bid ctx | AProjSharedBorrow asb -> (* Retrieve the borrow ids *) let bids = @@ -1235,21 +1235,21 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) * can use to identify the whole set *) let repr_bid = List.hd bids in (* Replace the shared borrow with Bottom *) - let ctx = update_aborrow meta ek_all repr_bid ABottom ctx in + let ctx = update_aborrow span ek_all repr_bid ABottom ctx in (* Give back the shared borrows *) let ctx = List.fold_left - (fun ctx bid -> give_back_shared config meta bid ctx) + (fun ctx bid -> give_back_shared config span bid ctx) ctx bids in (* Continue *) ctx | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow -> - craise __FILE__ __LINE__ meta "Unexpected" + craise __FILE__ __LINE__ span "Unexpected" in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id ctx + end_abstraction_borrows config span chain abs_id ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> log#ldebug @@ -1257,55 +1257,55 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) ("end_abstraction_borrows: found aproj borrows: " ^ aproj_to_string ctx (AProjBorrows (sv, proj_ty)))); (* Generate a fresh symbolic value *) - let nsv = mk_fresh_symbolic_value meta proj_ty in + let nsv = mk_fresh_symbolic_value span proj_ty in (* Replace the proj_borrows - there should be exactly one *) let ended_borrow = AEndedProjBorrows nsv in - let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in + let ctx = update_aproj_borrows span abs.abs_id sv ended_borrow ctx in (* Give back the symbolic value *) let ctx = - give_back_symbolic_value config meta abs.regions proj_ty sv nsv ctx + give_back_symbolic_value config span abs.regions proj_ty sv nsv ctx in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id ctx + end_abstraction_borrows config span chain abs_id ctx (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *) | FoundBorrowContent bc -> log#ldebug (lazy ("end_abstraction_borrows: found borrow content: " - ^ borrow_content_to_string ~meta:(Some meta) ctx bc)); + ^ borrow_content_to_string ~span:(Some span) ctx bc)); let ctx = match bc with | VSharedBorrow bid -> ( (* Replace the shared borrow with bottom *) let allow_inner_loans = false in match - end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx + end_borrow_get_borrow span (Some abs_id) allow_inner_loans bid ctx with - | Error _ -> craise __FILE__ __LINE__ meta "Unreachable" + | Error _ -> craise __FILE__ __LINE__ span "Unreachable" | Ok (ctx, _) -> (* Give back *) - give_back_shared config meta bid ctx) + give_back_shared config span bid ctx) | VMutBorrow (bid, v) -> ( (* Replace the mut borrow with bottom *) let allow_inner_loans = false in match - end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx + end_borrow_get_borrow span (Some abs_id) allow_inner_loans bid ctx with - | Error _ -> craise __FILE__ __LINE__ meta "Unreachable" + | Error _ -> craise __FILE__ __LINE__ span "Unreachable" | Ok (ctx, _) -> (* Give the value back - note that the mut borrow was below a * shared borrow: the value is thus unchanged *) - give_back_value config meta bid v ctx) - | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable" + give_back_value config span bid v ctx) + | VReservedMutBorrow _ -> craise __FILE__ __LINE__ span "Unreachable" in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id ctx + end_abstraction_borrows config span chain abs_id ctx (** Remove an abstraction from the context, as well as all its references *) -and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta) +and end_abstraction_remove_from_context (_config : config) (span : Meta.span) (abs_id : AbstractionId.id) : cm_fun = fun ctx -> - let ctx, abs = ctx_remove_abs meta ctx abs_id in + let ctx, abs = ctx_remove_abs span ctx abs_id in let abs = Option.get abs in (* Synthesize the symbolic AST *) (ctx, SynthesizeSymbolic.synthesize_end_abstraction ctx abs) @@ -1324,23 +1324,23 @@ and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta) intersecting proj_borrows, either in the concrete context or in an abstraction *) -and end_proj_loans_symbolic (config : config) (meta : Meta.meta) +and end_proj_loans_symbolic (config : config) (span : Meta.span) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value) : cm_fun = fun ctx -> (* Small helpers for sanity checks *) - let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in + let check ctx = no_aproj_over_symbolic_in_context span sv ctx in (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in match - lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx + lookup_intersecting_aproj_borrows_opt span explore_shared regions sv ctx with | None -> (* We couldn't find any in the context: it means that the symbolic value * is in the concrete environment (or that we dropped it, in which case * it is completely absent). We thus simply need to replace the loans * projector with an ended projector. *) - let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in + let ctx = update_aproj_loans_to_ended span abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) @@ -1383,16 +1383,16 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) AbstractionId.Set.empty abs_ids in (* End the abstractions and continue *) - end_abstractions_aux config meta chain abs_ids ctx + end_abstractions_aux config span chain abs_ids ctx in (* End the internal borrows projectors and the loans projector *) let ctx = (* All the proj_borrows are owned: simply erase them *) let ctx = - remove_intersecting_aproj_borrows_shared meta regions sv ctx + remove_intersecting_aproj_borrows_shared span regions sv ctx in (* End the loan itself *) - update_aproj_loans_to_ended meta abs_id sv ctx + update_aproj_loans_to_ended span abs_id sv ctx in (* Sanity check *) check ctx; @@ -1420,50 +1420,50 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) *) (* End the projector of borrows - TODO: not completely sure what to * replace it with... Maybe we should introduce an ABottomProj? *) - let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in + let ctx = update_aproj_borrows span abs_id sv AIgnoredProjBorrows ctx in (* Sanity check: no other occurrence of an intersecting projector of borrows *) sanity_check __FILE__ __LINE__ (Option.is_none - (lookup_intersecting_aproj_borrows_opt meta explore_shared regions + (lookup_intersecting_aproj_borrows_opt span explore_shared regions sv ctx)) - meta; + span; (* End the projector of loans *) - let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in + let ctx = update_aproj_loans_to_ended span abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) (ctx, fun e -> e)) else (* The borrows proj comes from a different abstraction: end it. *) - let ctx, cc = end_abstraction_aux config meta chain abs_id' ctx in + let ctx, cc = end_abstraction_aux config span chain abs_id' ctx in (* Retry ending the projector of loans *) let ctx, cc = comp cc - (end_proj_loans_symbolic config meta chain abs_id regions sv ctx) + (end_proj_loans_symbolic config span chain abs_id regions sv ctx) in (* Sanity check *) check ctx; (* Return *) (ctx, cc) -let end_borrow config (meta : Meta.meta) : BorrowId.id -> cm_fun = - end_borrow_aux config meta [] None +let end_borrow config (span : Meta.span) : BorrowId.id -> cm_fun = + end_borrow_aux config span [] None -let end_borrows config (meta : Meta.meta) : BorrowId.Set.t -> cm_fun = - end_borrows_aux config meta [] None +let end_borrows config (span : Meta.span) : BorrowId.Set.t -> cm_fun = + end_borrows_aux config span [] None -let end_abstraction config meta = end_abstraction_aux config meta [] -let end_abstractions config meta = end_abstractions_aux config meta [] -let end_borrow_no_synth config meta id ctx = fst (end_borrow config meta id ctx) +let end_abstraction config span = end_abstraction_aux config span [] +let end_abstractions config span = end_abstractions_aux config span [] +let end_borrow_no_synth config span id ctx = fst (end_borrow config span id ctx) -let end_borrows_no_synth config meta ids ctx = - fst (end_borrows config meta ids ctx) +let end_borrows_no_synth config span ids ctx = + fst (end_borrows config span ids ctx) -let end_abstraction_no_synth config meta id ctx = - fst (end_abstraction config meta id ctx) +let end_abstraction_no_synth config span id ctx = + fst (end_abstraction config span id ctx) -let end_abstractions_no_synth config meta ids ctx = - fst (end_abstractions config meta ids ctx) +let end_abstractions_no_synth config span ids ctx = + fst (end_abstractions config span ids ctx) (** Helper function: see {!activate_reserved_mut_borrow}. @@ -1481,14 +1481,14 @@ let end_abstractions_no_synth config meta ids ctx = The loan to update mustn't be a borrowed value. *) -let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) +let promote_shared_loan_to_mut_loan (span : Meta.span) (l : BorrowId.id) (ctx : eval_ctx) : typed_value * eval_ctx = (* Debug *) log#ldebug (lazy ("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l ^ "\n- context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n")); (* Lookup the shared loan - note that we can't promote a shared loan * in a shared value, but we can do it in a mutably borrowed value. @@ -1497,34 +1497,34 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan meta ek l ctx with + match lookup_loan span ek l ctx with | _, Concrete (VMutLoan _) -> - craise __FILE__ __LINE__ meta "Expected a shared loan, found a mut loan" + craise __FILE__ __LINE__ span "Expected a shared loan, found a mut loan" | _, Concrete (VSharedLoan (bids, sv)) -> (* Check that there is only one borrow id (l) and update the loan *) cassert __FILE__ __LINE__ (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1) - meta "There should only be one borrow id"; + span "There should only be one borrow id"; (* 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. *) - sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta; + sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) span; (* Check there isn't {!Bottom} (this is actually an invariant *) cassert __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions sv)) - meta "There shouldn't be a bottom"; + span "There shouldn't be a bottom"; (* Check there aren't reserved borrows *) cassert __FILE__ __LINE__ (not (reserved_in_value sv)) - meta "There shouldn't be reserved borrows"; + span "There shouldn't be reserved borrows"; (* Update the loan content *) - let ctx = update_loan meta ek l (VMutLoan l) ctx in + let ctx = update_loan span ek l (VMutLoan l) ctx in (* Return *) (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. *) - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Can't promote a shared loan to a mutable loan if the loan is inside a \ region abstraction" @@ -1533,7 +1533,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) This function updates a shared borrow to a mutable borrow (and that is all: it doesn't touch the corresponding loan). *) -let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) +let replace_reserved_borrow_with_mut_borrow (span : Meta.span) (l : BorrowId.id) (borrowed_value : typed_value) (ctx : eval_ctx) : eval_ctx = (* Lookup the reserved borrow - note that we don't go inside borrows/loans: there can't be reserved borrows inside other borrows/loans @@ -1541,28 +1541,28 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) let ek = { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in - match lookup_borrow meta ek l ctx with + match lookup_borrow span ek l ctx with | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> - craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow" + craise __FILE__ __LINE__ span "Expected a reserved mutable borrow" | Concrete (VReservedMutBorrow _) -> (* Update it *) - update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx + update_borrow span ek l (VMutBorrow (l, borrowed_value)) ctx | Abstract _ -> (* This can't happen for sure *) - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Can't promote a shared borrow to a mutable borrow if the borrow is \ inside a region abstraction" (** Promote a reserved mut borrow to a mut borrow. *) -let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) +let rec promote_reserved_mut_borrow (config : config) (span : Meta.span) (l : BorrowId.id) : cm_fun = fun ctx -> (* Lookup the value *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan meta ek l ctx with - | _, Concrete (VMutLoan _) -> craise __FILE__ __LINE__ meta "Unreachable" + match lookup_loan span ek l ctx with + | _, Concrete (VMutLoan _) -> craise __FILE__ __LINE__ span "Unreachable" | _, Concrete (VSharedLoan (bids, sv)) -> ( (* If there are loans inside the value, end them. Note that there can't be reserved borrows inside the value. @@ -1572,46 +1572,46 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (* End the loans *) let ctx, cc = match lc with - | VSharedLoan (bids, _) -> end_borrows config meta bids ctx - | VMutLoan bid -> end_borrow config meta bid ctx + | VSharedLoan (bids, _) -> end_borrows config span bids ctx + | VMutLoan bid -> end_borrow config span bid ctx in (* Recursive call *) - comp cc (promote_reserved_mut_borrow config meta l ctx) + comp cc (promote_reserved_mut_borrow config span l ctx) | None -> (* No loan to end inside the value *) (* Some sanity checks *) log#ldebug (lazy ("activate_reserved_mut_borrow: resulting value:\n" - ^ typed_value_to_string ~meta:(Some meta) ctx sv)); - sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta; + ^ typed_value_to_string ~span:(Some span) ctx sv)); + sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) span; sanity_check __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions sv)) - meta; - sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) meta; + span; + sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) span; (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) let bids = BorrowId.Set.remove l bids in - let ctx, cc = end_borrows config meta bids ctx in + let ctx, cc = end_borrows config span bids ctx in (* Promote the loan - TODO: this will fail if the value contains * any loans. In practice, it shouldn't, but we could also * look for loans inside the value and end them before promoting * the borrow. *) - let v, ctx = promote_shared_loan_to_mut_loan meta l ctx in + let v, ctx = promote_shared_loan_to_mut_loan span l ctx in (* Promote the borrow - the value should have been checked by {!promote_shared_loan_to_mut_loan} *) - let ctx = replace_reserved_borrow_with_mut_borrow meta l v ctx in + let ctx = replace_reserved_borrow_with_mut_borrow span l v ctx in (* Return *) (ctx, cc)) | _, 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. *) - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Can't activate a reserved mutable borrow referencing a loan inside\n\ \ a region abstraction" -let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) +let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs = (* Accumulator to store the destructured values *) let avalues = ref [] in @@ -1624,7 +1624,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) ignore the children altogether. Instead, we explore them and make sure we don't register values while doing so. *) - let push_fail _ = craise __FILE__ __LINE__ meta "Unreachable" in + let push_fail _ = craise __FILE__ __LINE__ span "Unreachable" in (* Function to explore an avalue and destructure it *) let rec list_avalues (allow_borrows : bool) (push : typed_avalue -> unit) (av : typed_avalue) : unit = @@ -1641,13 +1641,13 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) - meta "Nested borrows are not supported yet"; + span "Nested borrows are not supported yet"; (* Destructure the shared value *) let avl, sv = if destructure_shared_values then list_values sv else ([], sv) in (* Push a value *) - let ignored = mk_aignored meta child_av.ty in + let ignored = mk_aignored span child_av.ty in let value = ALoan (ASharedLoan (bids, sv, ignored)) in push { value; ty }; (* Explore the child *) @@ -1663,39 +1663,39 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (* Explore the child *) list_avalues false push_fail child_av; (* Explore the whole loan *) - let ignored = mk_aignored meta child_av.ty in + let ignored = mk_aignored span child_av.ty in let value = ALoan (AMutLoan (bid, ignored)) in push { value; ty } | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) - meta "Nested borrows are not supported yet"; - sanity_check __FILE__ __LINE__ (opt_bid = None) meta; + span "Nested borrows are not supported yet"; + sanity_check __FILE__ __LINE__ (opt_bid = None) span; (* Simply explore the child *) list_avalues false push_fail child_av | AEndedMutLoan - { child = child_av; given_back = _; given_back_meta = _ } + { child = child_av; given_back = _; given_back_span = _ } | AEndedSharedLoan (_, child_av) | AEndedIgnoredMutLoan - { child = child_av; given_back = _; given_back_meta = _ } + { child = child_av; given_back = _; given_back_span = _ } | AIgnoredSharedLoan child_av -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) - meta "Nested borrows are not supported yet"; + span "Nested borrows are not supported yet"; (* Simply explore the child *) list_avalues false push_fail child_av) | ABorrow bc -> ( (* Sanity check - rem.: may be redundant with [push_fail] *) - sanity_check __FILE__ __LINE__ allow_borrows meta; + sanity_check __FILE__ __LINE__ allow_borrows span; (* Explore the borrow content *) match bc with | AMutBorrow (bid, child_av) -> (* Explore the child *) list_avalues false push_fail child_av; (* Explore the borrow *) - let ignored = mk_aignored meta child_av.ty in + let ignored = mk_aignored span child_av.ty in let value = ABorrow (AMutBorrow (bid, ignored)) in push { value; ty } | ASharedBorrow _ -> @@ -1705,21 +1705,21 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) - meta "Nested borrows are not supported yet"; - sanity_check __FILE__ __LINE__ (opt_bid = None) meta; + span "Nested borrows are not supported yet"; + sanity_check __FILE__ __LINE__ (opt_bid = None) span; (* Just explore the child *) list_avalues false push_fail child_av | AEndedIgnoredMutBorrow - { child = child_av; given_back = _; given_back_meta = _ } -> + { child = child_av; given_back = _; given_back_span = _ } -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) - meta "Nested borrows are not supported yet"; + span "Nested borrows are not supported yet"; (* Just explore the child *) list_avalues false push_fail child_av | AProjSharedBorrow asb -> (* We don't support nested borrows *) - cassert __FILE__ __LINE__ (asb = []) meta + cassert __FILE__ __LINE__ (asb = []) span "Nested borrows are not supported yet"; (* Nothing specific to do *) () @@ -1728,13 +1728,13 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) be in the context anymore (if we end *one* borrow in an abstraction, we have to end them all and remove the abstraction from the context) *) - craise __FILE__ __LINE__ meta "Unreachable") + craise __FILE__ __LINE__ span "Unreachable") | ASymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) - meta + span and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in match v.value with @@ -1746,22 +1746,22 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) let avl = List.concat avll in let adt = { adt with field_values } in (avl, { v with value = VAdt adt }) - | VBottom -> craise __FILE__ __LINE__ meta "Unreachable" + | VBottom -> craise __FILE__ __LINE__ span "Unreachable" | VBorrow _ -> (* We don't support nested borrows for now *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | VLoan lc -> ( match lc with | VSharedLoan (bids, sv) -> let avl, sv = list_values sv in if destructure_shared_values then ( (* Rem.: the shared value can't contain loans nor borrows *) - cassert __FILE__ __LINE__ (ty_no_regions ty) meta + cassert __FILE__ __LINE__ (ty_no_regions ty) span "Nested borrows are not supported yet"; let av : typed_avalue = sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv.value)) - meta; + span; (* We introduce fresh ids for the symbolic values *) let mk_value_with_fresh_sids (v : typed_value) : typed_value = let visitor = @@ -1777,20 +1777,20 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) let sv = mk_value_with_fresh_sids sv in (* Create the new avalue *) let value = - ALoan (ASharedLoan (bids, sv, mk_aignored meta ty)) + ALoan (ASharedLoan (bids, sv, mk_aignored span ty)) in { value; ty } in let avl = List.append [ av ] avl in (avl, sv)) else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) }) - | VMutLoan _ -> craise __FILE__ __LINE__ meta "Unreachable") + | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable") | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) - meta; + span; ([], v) in @@ -1800,14 +1800,14 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) (* Update *) { abs0 with avalues; kind = abs_kind; can_end } -let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool) +let abs_is_destructured (span : Meta.span) (destructure_shared_values : bool) (ctx : eval_ctx) (abs : abs) : bool = let abs' = - destructure_abs meta abs.kind abs.can_end destructure_shared_values ctx abs + destructure_abs span abs.kind abs.can_end destructure_shared_values ctx abs in abs = abs' -let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) +let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (destructure_shared_values : bool) (ctx : eval_ctx) (v : typed_value) : abs list = (* Convert the value to a list of avalues *) @@ -1846,7 +1846,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) log#ldebug (lazy ("convert_value_to_abstractions: to_avalues:\n- value: " - ^ typed_value_to_string ~meta:(Some meta) ctx v)); + ^ typed_value_to_string ~span:(Some span) ctx v)); let ty = v.ty in match v.value with @@ -1890,14 +1890,14 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (avl, { v with value = VAdt adt }) | VBorrow bc -> ( let _, ref_ty, kind = ty_as_ref ty in - cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta + cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span "Nested borrows are not supported yet"; (* Sanity check *) - sanity_check __FILE__ __LINE__ allow_borrows meta; + sanity_check __FILE__ __LINE__ allow_borrows span; (* Convert the borrow content *) match bc with | VSharedBorrow bid -> - cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta + cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span "Nested borrows are not supported yet"; let ty = TRef (RFVar r_id, ref_ty, kind) in let value = ABorrow (ASharedBorrow bid) in @@ -1907,10 +1907,10 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (value_has_borrows ctx bv.value)) - meta "Nested borrows are not supported yet"; + span "Nested borrows are not supported yet"; (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *) let ty = TRef (RFVar r_id, ref_ty, kind) in - let ignored = mk_aignored meta ref_ty in + let ignored = mk_aignored span ref_ty in let av = ABorrow (AMutBorrow (bid, ignored)) in let av = { value = av; ty } in (* Continue exploring, looking for loans (and forbidding borrows, @@ -1920,7 +1920,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (av :: avl, value) | VReservedMutBorrow _ -> (* This borrow should have been activated *) - craise __FILE__ __LINE__ meta "Unexpected") + craise __FILE__ __LINE__ span "Unexpected") | VLoan lc -> ( match lc with | VSharedLoan (bids, sv) -> @@ -1928,13 +1928,13 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) - meta "Nested borrows are not supported yet"; + span "Nested borrows are not supported yet"; (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) - cassert __FILE__ __LINE__ (ty_no_regions ty) meta + cassert __FILE__ __LINE__ (ty_no_regions ty) span "Nested borrows are not supported yet"; let ty = mk_ref_ty (RFVar r_id) ty RShared in - let ignored = mk_aignored meta ty in + let ignored = mk_aignored span ty in (* Rem.: the shared value might contain loans *) let avl, sv = to_avalues false true true r_id sv in let av = ALoan (ASharedLoan (bids, sv, ignored)) in @@ -1950,10 +1950,10 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) | VMutLoan bid -> (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) - cassert __FILE__ __LINE__ (ty_no_regions ty) meta + cassert __FILE__ __LINE__ (ty_no_regions ty) span "Nested borrows are not supported yet"; let ty = mk_ref_ty (RFVar r_id) ty RMut in - let ignored = mk_aignored meta ty in + let ignored = mk_aignored span ty in let av = ALoan (AMutLoan (bid, ignored)) in let av = { value = av; ty } in ([ av ], v)) @@ -1962,7 +1962,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) be eagerly expanded, and we don't support nested borrows *) cassert __FILE__ __LINE__ (not (value_has_borrows ctx v.value)) - meta "Nested borrows are not supported yet"; + span "Nested borrows are not supported yet"; (* Return nothing *) ([], v) in @@ -2003,7 +2003,7 @@ type merge_abstraction_info = { - all the borrows are destructured (for instance, shared loans can't contain shared loans). *) -let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) +let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) (abs : abs) : merge_abstraction_info = let loans : loan_id_set ref = ref BorrowId.Set.empty in let borrows : borrow_id_set ref = ref BorrowId.Set.empty in @@ -2016,32 +2016,32 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) in let push_loans ids (lc : g_loan_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) meta; + sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) span; loans := BorrowId.Set.union !loans ids; BorrowId.Set.iter (fun id -> sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) - meta; + span; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans) ids in let push_loan id (lc : g_loan_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) span; loans := BorrowId.Set.add id !loans; sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) - meta; + span; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans in let push_borrow id (bc : g_borrow_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) span; borrows := BorrowId.Set.add id !borrows; sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !borrow_to_content)) - meta; + span; borrow_to_content := BorrowId.Map.add id bc !borrow_to_content; borrows_loans := BorrowId id :: !borrows_loans in @@ -2064,23 +2064,23 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) let ty = match Option.get env with | Concrete ty -> ty - | Abstract _ -> craise __FILE__ __LINE__ meta "Unreachable" + | Abstract _ -> craise __FILE__ __LINE__ span "Unreachable" in (match lc with | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc)) - | VMutLoan _ -> craise __FILE__ __LINE__ meta "Unreachable"); + | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable"); (* Continue *) super#visit_loan_content env lc method! visit_borrow_content _ _ = (* Can happen if we explore shared values which contain borrows - i.e., if we have nested borrows (we forbid this for now) *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" method! visit_aloan_content env lc = let ty = match Option.get env with - | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable" + | Concrete _ -> craise __FILE__ __LINE__ span "Unreachable" | Abstract ty -> ty in (* Register the loans *) @@ -2090,14 +2090,14 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) - craise __FILE__ __LINE__ meta "Unreachable"); + craise __FILE__ __LINE__ span "Unreachable"); (* Continue *) super#visit_aloan_content env lc method! visit_aborrow_content env bc = let ty = match Option.get env with - | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable" + | Concrete _ -> craise __FILE__ __LINE__ span "Unreachable" | Abstract ty -> ty in (* Explore the borrow content *) @@ -2111,20 +2111,20 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) | AsbProjReborrows _ -> (* Can only happen if the symbolic value (potentially) contains borrows - i.e., we have nested borrows *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in List.iter register asb | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow -> (* The abstraction has been destructured, so those shouldn't appear *) - craise __FILE__ __LINE__ meta "Unreachable"); + craise __FILE__ __LINE__ span "Unreachable"); super#visit_aborrow_content env bc method! visit_symbolic_value _ sv = (* Sanity check: no borrows *) sanity_check __FILE__ __LINE__ (not (symbolic_value_has_borrows ctx sv)) - meta + span end in @@ -2191,25 +2191,25 @@ type merge_duplicates_funcs = { Merge two abstractions into one, without updating the context. *) -let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) +let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs) (abs1 : abs) : abs = log#ldebug (lazy ("merge_into_abstraction_aux:\n- abs0:\n" - ^ abs_to_string meta ctx abs0 + ^ abs_to_string span ctx abs0 ^ "\n\n- abs1:\n" - ^ abs_to_string meta ctx abs1)); + ^ abs_to_string span ctx abs1)); (* Check that the abstractions are destructured *) if !Config.sanity_checks then ( let destructure_shared_values = true in sanity_check __FILE__ __LINE__ - (abs_is_destructured meta destructure_shared_values ctx abs0) - meta; + (abs_is_destructured span destructure_shared_values ctx abs0) + span; sanity_check __FILE__ __LINE__ - (abs_is_destructured meta destructure_shared_values ctx abs1) - meta); + (abs_is_destructured span destructure_shared_values ctx abs1) + span); (* Compute the relevant information *) let { @@ -2219,7 +2219,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) loan_to_content = loan_to_content0; borrow_to_content = borrow_to_content0; } = - compute_merge_abstraction_info meta ctx abs0 + compute_merge_abstraction_info span ctx abs0 in let { @@ -2229,7 +2229,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) loan_to_content = loan_to_content1; borrow_to_content = borrow_to_content1; } = - compute_merge_abstraction_info meta ctx abs1 + compute_merge_abstraction_info span ctx abs1 in (* Sanity check: there is no loan/borrows which appears in both abstractions, @@ -2237,8 +2237,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) if merge_funs = None then ( sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint borrows0 borrows1) - meta; - sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) meta); + span; + sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) span); (* Merge. There are several cases: @@ -2265,7 +2265,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) log#ldebug (lazy ("merge_into_abstraction_aux: push_avalue: " - ^ typed_avalue_to_string ~meta:(Some meta) ctx av)); + ^ typed_avalue_to_string ~span:(Some span) ctx av)); avalues := av :: !avalues in let push_opt_avalue av = @@ -2279,7 +2279,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) in let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t = let bids = BorrowId.Set.diff bids intersect in - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) meta; + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span; bids in let filter_bid (bid : BorrowId.id) : BorrowId.id option = @@ -2307,11 +2307,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (Option.get merge_funs).merge_ashared_borrows id ty0 ty1 | AProjSharedBorrow _, AProjSharedBorrow _ -> (* Unreachable because requires nested borrows *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) @@ -2319,12 +2319,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) match (bc0, bc1) with | Concrete _, Concrete _ -> (* This can happen only in case of nested borrows *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty0, bc0), Abstract (ty1, bc1) -> merge_aborrow_contents ty0 bc0 ty1 bc1 | Concrete _, Abstract _ | Abstract _, Concrete _ -> (* TODO: is it really unreachable? *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty) @@ -2342,7 +2342,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (* Check that the sets of ids are the same - if it is not the case, it means we actually need to merge more than 2 avalues: we ignore this case for now *) - sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) meta; + sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span; let ids = ids0 in if BorrowId.Set.is_empty ids then ( (* If the set of ids is empty, we can eliminate this shared loan. @@ -2356,12 +2356,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) *) sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) - meta; + span; sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) - meta; - sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta; - sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta; + span; + sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; + sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; None) else ( (* Register the loan ids *) @@ -2373,7 +2373,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in (* Note that because we may filter ids from a set of id, this function has @@ -2384,12 +2384,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) match (lc0, lc1) with | Concrete _, Concrete _ -> (* This can not happen: the values should have been destructured *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty0, lc0), Abstract (ty1, lc1) -> merge_aloan_contents ty0 lc0 ty1 lc1 | Concrete _, Abstract _ | Abstract _, Concrete _ -> (* TODO: is it really unreachable? *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in (* Note that we first explore the borrows/loans of [abs1], because we @@ -2430,12 +2430,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) a concrete borrow can only happen inside a shared loan *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty, bc) -> { value = ABorrow bc; ty }) | Some bc0, Some bc1 -> - sanity_check __FILE__ __LINE__ (merge_funs <> None) meta; + sanity_check __FILE__ __LINE__ (merge_funs <> None) span; merge_g_borrow_contents bc0 bc1 - | None, None -> craise __FILE__ __LINE__ meta "Unreachable" + | None, None -> craise __FILE__ __LINE__ span "Unreachable" in push_avalue av) | LoanId bid -> @@ -2468,19 +2468,19 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) | Concrete _ -> (* This shouldn't happen because the avalues should have been destructured. *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty, lc) -> ( match lc with | ASharedLoan (bids, sv, child) -> let bids = filter_bids bids in sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) - meta; + span; sanity_check __FILE__ __LINE__ - (is_aignored child.value) meta; + (is_aignored child.value) span; sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv.value)) - meta; + span; let lc = ASharedLoan (bids, sv, child) in set_loans_as_merged bids; Some { value = ALoan lc; ty } @@ -2491,11 +2491,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) - craise __FILE__ __LINE__ meta "Unreachable")) + craise __FILE__ __LINE__ span "Unreachable")) | Some lc0, Some lc1 -> - sanity_check __FILE__ __LINE__ (merge_funs <> None) meta; + sanity_check __FILE__ __LINE__ (merge_funs <> None) span; merge_g_loan_contents lc0 lc1 - | None, None -> craise __FILE__ __LINE__ meta "Unreachable" + | None, None -> craise __FILE__ __LINE__ span "Unreachable" in push_opt_avalue av)) borrows_loans; @@ -2513,7 +2513,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> craise __FILE__ __LINE__ meta "Unexpected" + | _ -> craise __FILE__ __LINE__ span "Unexpected" in let aborrows, aloans = List.partition is_borrow avalues in List.append aborrows aloans @@ -2548,7 +2548,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) in (* Sanity check *) - sanity_check __FILE__ __LINE__ (abs_is_destructured meta true ctx abs) meta; + sanity_check __FILE__ __LINE__ (abs_is_destructured span true ctx abs) span; (* Return *) abs @@ -2559,7 +2559,7 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id) let env = Substitute.env_subst_rids rsubst ctx.env in { ctx with env } -let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) +let merge_into_abstraction (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) : eval_ctx * AbstractionId.id = @@ -2569,13 +2569,13 @@ let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (* Merge them *) let nabs = - merge_into_abstraction_aux meta abs_kind can_end merge_funs ctx abs0 abs1 + merge_into_abstraction_aux span abs_kind can_end merge_funs ctx abs0 abs1 in (* Update the environment: replace the abstraction 1 with the result of the merge, remove the abstraction 0 *) - let ctx = fst (ctx_subst_abs meta ctx abs_id1 nabs) in - let ctx = fst (ctx_remove_abs meta ctx abs_id0) in + let ctx = fst (ctx_subst_abs span ctx abs_id1 nabs) in + let ctx = fst (ctx_remove_abs span ctx abs_id0) in (* Merge all the regions from the abstraction into one (the first - i.e., the one with the smallest id). Note that we need to do this in the whole -- cgit v1.2.3