diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 757 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 31 |
2 files changed, 451 insertions, 337 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 17810705..e593ae75 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -7,6 +7,7 @@ open TypesUtils open InterpreterUtils open InterpreterBorrowsCore open InterpreterProjectors +open Errors (** The local logger *) let log = Logging.borrows_log @@ -29,8 +30,9 @@ 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 (allowed_abs : AbstractionId.id option) - (allow_inner_loans : bool) (l : BorrowId.id) (ctx : eval_ctx) : +let end_borrow_get_borrow (meta : Meta.meta) + (allowed_abs : AbstractionId.id option) (allow_inner_loans : bool) + (l : BorrowId.id) (ctx : eval_ctx) : ( eval_ctx * (AbstractionId.id option * g_borrow_content) option, priority_borrows_or_abs ) result = @@ -41,7 +43,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) in let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content) = - assert (Option.is_none !replaced_bc); + sanity_check __FILE__ __LINE__ (Option.is_none !replaced_bc) meta; replaced_bc := Some (abs_id, bc) in (* Raise an exception if: @@ -180,7 +182,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) * 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} *) - raise (Failure "Unimplemented") + craise __FILE__ __LINE__ meta "Unimplemented" (* ABottom *)) else (* Update the outer borrows before diving into the child avalue *) @@ -215,7 +217,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) 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 l asb in + let asb = remove_borrow_from_asb meta l asb in ABorrow (AProjSharedBorrow asb)) else (* Nothing special to do *) super#visit_ABorrow outer bc @@ -223,8 +225,8 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) method! visit_abs outer abs = (* Update the outer abs *) let outer_abs, outer_borrows = outer in - assert (Option.is_none outer_abs); - assert (Option.is_none outer_borrows); + sanity_check __FILE__ __LINE__ (Option.is_none outer_abs) meta; + sanity_check __FILE__ __LINE__ (Option.is_none outer_borrows) meta; let outer = (Some abs.abs_id, None) in super#visit_abs outer abs end @@ -244,21 +246,27 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option) 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) (bid : BorrowId.id) (nv : typed_value) - (ctx : eval_ctx) : eval_ctx = +let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) + (nv : typed_value) (ctx : eval_ctx) : eval_ctx = (* Sanity check *) - assert (not (loans_in_value nv)); - assert (not (bottom_in_value ctx.ended_regions nv)); + exec_assert __FILE__ __LINE__ + (not (loans_in_value nv)) + meta "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"; (* Debug *) log#ldebug (lazy ("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: " - ^ typed_value_to_string ctx nv - ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); + ^ typed_value_to_string ~meta:(Some meta) ctx nv + ^ "\n- context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n")); (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - assert (not !replaced); + sanity_check __FILE__ __LINE__ (not !replaced) meta; replaced := true in (* Whenever giving back symbolic values, they shouldn't contain already ended regions *) @@ -266,7 +274,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* We sometimes need to reborrow values while giving a value back due: prepare that *) let allow_reborrows = true in let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows + prepare_reborrows config meta allow_reborrows in (* The visitor to give back the values *) let obj = @@ -300,7 +308,8 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) ("give_back_value: improper type:\n- expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); - raise (Failure "Value given back doesn't have the proper type")); + craise __FILE__ __LINE__ meta + "Value given back doesn't have the proper type"); (* Replace *) set_replaced (); nv.value) @@ -334,7 +343,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* Remember the given back value as a meta-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 nv.value in + let given_back_meta = as_symbolic meta nv.value in (* The loan projector *) let given_back = mk_aproj_loans_value_from_symbolic_value abs.regions sv @@ -345,7 +354,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) ABorrow (AEndedIgnoredMutBorrow { given_back; child; given_back_meta }) - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Unreachable" else (* Continue exploring *) ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child) @@ -360,7 +369,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* Preparing a bit *) let regions, ancestors_regions = match opt_abs with - | None -> raise (Failure "Unreachable") + | None -> craise __FILE__ __LINE__ meta "Unreachable" | Some abs -> (abs.regions, abs.ancestors_regions) in (* Rk.: there is a small issue with the types of the aloan values. @@ -381,8 +390,8 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) let given_back_meta = nv in (* Apply the projection *) let given_back = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions ancestors_regions nv borrowed_value_aty + apply_proj_borrows meta 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 @@ -408,8 +417,8 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) * we don't register the fact that we inserted the value somewhere * (i.e., we don't call {!set_replaced}) *) let given_back = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions ancestors_regions nv borrowed_value_aty + apply_proj_borrows meta 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 @@ -426,7 +435,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* We remember in which abstraction we are before diving - * this is necessary for projecting values: we need to know * over which regions to project *) - assert (Option.is_none opt_abs); + sanity_check __FILE__ __LINE__ (Option.is_none opt_abs) meta; super#visit_EAbs (Some abs) abs end in @@ -434,16 +443,18 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - assert !replaced; + cassert __FILE__ __LINE__ !replaced meta "No loan updated"; (* Apply the reborrows *) apply_registered_reborrows ctx (** Give back a *modified* symbolic value. *) -let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) - (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value) - (ctx : eval_ctx) : eval_ctx = +let give_back_symbolic_value (_config : config) (meta : Meta.meta) + (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value) + (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Sanity checks *) - assert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty); + 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 *) let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) @@ -465,11 +476,11 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) type [T]! We thus *mustn't* introduce a projector here. *) (* AProjBorrows (nsv, sv.sv_ty) *) - raise (Failure "TODO") + internal_error __FILE__ __LINE__ meta in AProjLoans (sv, (mv, child_proj) :: local_given_back) in - update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx + update_intersecting_aproj_loans meta proj_regions proj_ty sv subst ctx (** Auxiliary function to end borrows. See {!give_back}. @@ -484,12 +495,14 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) 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) (bid : BorrowId.id) - (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx = +let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) + (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 () = - assert (not !replaced); + cassert __FILE__ __LINE__ (not !replaced) meta + "Exacly one loan should be updated"; replaced := true in let obj = @@ -532,7 +545,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) ("give_back_avalue_to_same_abstraction: improper type:\n\ - expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); - raise (Failure "Value given back doesn't have the proper type")); + craise __FILE__ __LINE__ meta + "Value given back doesn't have the proper type"); (* This is the loan we are looking for: apply the projection to * the value we give back and replaced this mutable loan with * an ended loan *) @@ -558,7 +572,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) * we don't register the fact that we inserted the value somewhere * (i.e., we don't call {!set_replaced}) *) (* Sanity check *) - assert (nv.ty = ty); + sanity_check __FILE__ __LINE__ (nv.ty = ty) meta; ALoan (AEndedIgnoredMutLoan { given_back = nv; child; given_back_meta = nsv })) @@ -574,7 +588,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - assert !replaced; + cassert __FILE__ __LINE__ !replaced meta "No loan updated"; (* Return *) ctx @@ -587,11 +601,13 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id) we update. TODO: this was not the case before, so some sanity checks are not useful anymore. *) -let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = +let give_back_shared _config (meta : Meta.meta) (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 () = - assert (not !replaced); + cassert __FILE__ __LINE__ (not !replaced) meta + "Exactly one loan should be updated"; replaced := true in let obj = @@ -656,7 +672,7 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = (* Explore the environment *) let ctx = obj#visit_eval_ctx None ctx in (* Check we gave back to exactly one loan *) - assert !replaced; + cassert __FILE__ __LINE__ !replaced meta "No loan updated"; (* Return *) ctx @@ -665,12 +681,12 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx = to an environment by inserting a new borrow id in the set of borrows tracked by a shared value, referenced by the [original_bid] argument. *) -let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id) - (ctx : eval_ctx) : eval_ctx = +let reborrow_shared (meta : Meta.meta) (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 () = - assert (not !r); + sanity_check __FILE__ __LINE__ (not !r) meta; r := true in @@ -700,7 +716,7 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id) let env = obj#visit_env () ctx.env in (* Check that we reborrowed once *) - assert !r; + sanity_check __FILE__ __LINE__ !r meta; { ctx with env } (** Convert an {!type:avalue} to a {!type:value}. @@ -719,8 +735,9 @@ let reborrow_shared (original_bid : BorrowId.id) (new_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 (av : typed_avalue) : symbolic_value = - mk_fresh_symbolic_value av.ty +let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) : + symbolic_value = + mk_fresh_symbolic_value meta av.ty (** Auxiliary function: see {!end_borrow_aux}. @@ -738,18 +755,20 @@ let convert_avalue_to_given_back_value (av : typed_avalue) : symbolic_value = borrows. This kind of internal reshuffling. should be similar to ending abstractions (it is tantamount to ending *sub*-abstractions). *) -let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content) - (ctx : eval_ctx) : eval_ctx = +let give_back (config : config) (meta : Meta.meta) (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 ctx bc - | Abstract bc -> aborrow_content_to_string ctx bc + | Concrete bc -> borrow_content_to_string ~meta:(Some meta) ctx bc + | Abstract bc -> aborrow_content_to_string ~meta:(Some meta) ctx bc in "give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc - ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); + ^ "\n- context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n")); (* This is used for sanity checks *) let sanity_ek = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } @@ -757,53 +776,61 @@ let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content) match bc with | Concrete (VMutBorrow (l', tv)) -> (* Sanity check *) - assert (l' = l); - assert (not (loans_in_value tv)); + sanity_check __FILE__ __LINE__ (l' = l) meta; + sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) meta; (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* Update the context *) - give_back_value config l tv ctx + give_back_value config meta l tv ctx | Concrete (VSharedBorrow l' | VReservedMutBorrow l') -> (* Sanity check *) - assert (l' = l); + sanity_check __FILE__ __LINE__ (l' = l) meta; (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* Update the context *) - give_back_shared config l ctx + give_back_shared config meta l ctx | Abstract (AMutBorrow (l', av)) -> (* Sanity check *) - assert (l' = l); + sanity_check __FILE__ __LINE__ (l' = l) meta; (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* 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 av in + let sv = convert_avalue_to_given_back_value meta av in (* Update the context *) - give_back_avalue_to_same_abstraction config l av + give_back_avalue_to_same_abstraction config meta l av (mk_typed_value_from_symbolic_value sv) ctx | Abstract (ASharedBorrow l') -> (* Sanity check *) - assert (l' = l); + sanity_check __FILE__ __LINE__ (l' = l) meta; (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); + sanity_check __FILE__ __LINE__ + (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) + meta; (* Update the context *) - give_back_shared config l ctx + give_back_shared config meta l ctx | Abstract (AProjSharedBorrow asb) -> (* Sanity check *) - assert (borrow_in_asb l asb); + sanity_check __FILE__ __LINE__ (borrow_in_asb l asb) meta; (* Update the context *) - give_back_shared config l ctx + give_back_shared config meta l ctx | Abstract ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow ) -> - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" -let check_borrow_disappeared (fun_name : string) (l : BorrowId.id) - (ctx0 : eval_ctx) : cm_fun = +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 @@ -813,20 +840,22 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id) (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": borrow didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ctx)); - raise (Failure "Borrow not eliminated") + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + craise __FILE__ __LINE__ meta "Borrow not eliminated" in - match lookup_loan_opt ek_all l ctx with + match lookup_loan_opt meta ek_all l ctx with | None -> () (* Ok *) | Some _ -> log#lerror (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": loan didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ctx)); - raise (Failure "Loan not eliminated") + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + craise __FILE__ __LINE__ meta "Loan not eliminated" in unit_to_cm_fun check_disappeared @@ -851,26 +880,27 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id) perform anything smart and is trusted, and another function for the book-keeping. *) -let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) - (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun = +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 -> (* Check that we don't loop *) let chain0 = chain in let chain = - add_borrow_or_abs_id_to_chain "end_borrow_aux: " (BorrowId l) chain + add_borrow_or_abs_id_to_chain meta "end_borrow_aux: " (BorrowId l) chain in log#ldebug (lazy ("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n" - ^ eval_ctx_to_string ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* 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 "end borrow" l ctx0 in + let cf_check : cm_fun = 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 allowed_abs allow_inner_loans l ctx with + match end_borrow_get_borrow meta 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) @@ -899,29 +929,29 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) * inside another borrow *) let allowed_abs' = None in (* End the outer borrows *) - let cc = end_borrows_aux config chain allowed_abs' bids in + let cc = end_borrows_aux config meta chain allowed_abs' bids in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in + let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in (* Check and apply *) comp cc cf_check cf ctx | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> let allowed_abs' = None in (* End the outer borrow *) - let cc = end_borrow_aux config chain allowed_abs' bid in + let cc = end_borrow_aux config meta chain allowed_abs' bid in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in + let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in (* Check and apply *) comp cc cf_check cf ctx | OuterAbs abs_id -> (* The borrow is inside an abstraction: end the whole abstraction *) - let cf_end_abs = end_abstraction_aux config chain abs_id in + 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) | Ok (ctx, None) -> log#ldebug (lazy "End borrow: borrow not found"); (* It is possible that we can't find a borrow in symbolic mode (ending * an abstraction may end several borrows at once *) - assert (config.mode = SymbolicMode); + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; (* Do a sanity check and continue *) cf_check cf ctx (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update @@ -930,10 +960,12 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) (* Sanity check: the borrowed value shouldn't contain loans *) (match bc with | Concrete (VMutBorrow (_, bv)) -> - assert (Option.is_none (get_first_loan_in_value bv)) + sanity_check __FILE__ __LINE__ + (Option.is_none (get_first_loan_in_value bv)) + meta | _ -> ()); (* Give back the value *) - let ctx = give_back config l bc ctx in + let ctx = give_back config meta l bc ctx in (* Do a sanity check and continue *) let cc = cf_check in (* Save a snapshot of the environment for the name generation *) @@ -941,23 +973,25 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) (* Compose *) cc cf ctx -and end_borrows_aux (config : config) (chain : borrow_or_abs_ids) - (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun = +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 -> (* 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 *) let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in List.fold_left - (fun cf id -> end_borrow_aux config chain allowed_abs id cf) + (fun cf id -> end_borrow_aux config meta chain allowed_abs id cf) cf ids -and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) - (abs_id : AbstractionId.id) : cm_fun = +and end_abstraction_aux (config : config) (meta : Meta.meta) + (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun cf ctx -> (* Check that we don't loop *) let chain = - add_borrow_or_abs_id_to_chain "end_abstraction_aux: " (AbsId abs_id) chain + add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id) + chain in (* Remember the original context for printing purposes *) let ctx0 = ctx in @@ -965,7 +999,8 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (lazy ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id - ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0)); + ^ "\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0)); (* Lookup the abstraction - note that if we end a list of abstractions, ending one abstraction may lead to the current abstraction having @@ -983,14 +1018,13 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (* Check that we can end the abstraction *) if abs.can_end then () else - raise - (Failure - ("Can't end abstraction " - ^ AbstractionId.to_string abs.abs_id - ^ " as it is set as non-endable")); + craise __FILE__ __LINE__ meta + ("Can't end abstraction " + ^ AbstractionId.to_string abs.abs_id + ^ " as it is set as non-endable"); (* End the parent abstractions first *) - let cc = end_abstractions_aux config chain abs.parents in + let cc = end_abstractions_aux config meta chain abs.parents in let cc = comp_unit cc (fun ctx -> log#ldebug @@ -998,22 +1032,23 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id ^ "\n- context after parent abstractions ended:\n" - ^ eval_ctx_to_string ctx))) + ^ eval_ctx_to_string ~meta:(Some meta) ctx))) in (* End the loans inside the abstraction *) - let cc = comp cc (end_abstraction_loans config chain abs_id) in + 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 ctx))) + ^ "\n- context after loans ended:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx))) in (* End the abstraction itself by redistributing the borrows it contains *) - let cc = comp cc (end_abstraction_borrows config chain abs_id) in + let cc = comp cc (end_abstraction_borrows config meta chain abs_id) in (* End the regions owned by the abstraction - note that we don't need to * relookup the abstraction: the set of regions in an abstraction never @@ -1029,7 +1064,9 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (* 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 abs_id) in + let cc = + comp cc (end_abstraction_remove_from_context config meta abs_id) + in (* Debugging *) let cc = @@ -1038,12 +1075,14 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (lazy ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id - ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx))) + ^ "\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 (* Sanity check: ending an abstraction must preserve the invariants *) - let cc = comp cc Invariants.cf_check_invariants in + let cc = comp cc (Invariants.cf_check_invariants meta) in (* Save a snapshot of the environment for the name generation *) let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in @@ -1051,19 +1090,19 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids) (* Apply the continuation *) cc cf ctx -and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids) - (abs_ids : AbstractionId.Set.t) : cm_fun = +and end_abstractions_aux (config : config) (meta : Meta.meta) + (chain : borrow_or_abs_ids) (abs_ids : AbstractionId.Set.t) : cm_fun = fun cf -> (* 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 chain id cf) + (fun cf id -> end_abstraction_aux config meta chain id cf) cf abs_ids -and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids) - (abs_id : AbstractionId.id) : cm_fun = +and end_abstraction_loans (config : config) (meta : Meta.meta) + (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun cf ctx -> (* Lookup the abstraction *) let abs = ctx_lookup_abs ctx abs_id in @@ -1071,7 +1110,7 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids) * * 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 abs in + let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in match opt_loan with | None -> (* No loans: nothing to update *) @@ -1080,24 +1119,26 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids) (* There are loans: end the corresponding borrows, then recheck *) let cc : cm_fun = match bids with - | Borrow bid -> end_borrow_aux config chain None bid - | Borrows bids -> end_borrows_aux config chain None bids + | Borrow bid -> end_borrow_aux config meta chain None bid + | Borrows bids -> end_borrows_aux config meta chain None bids in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config chain abs_id) in + let cc = comp cc (end_abstraction_loans config meta chain abs_id) in (* Continue *) cc cf 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 chain abs_id abs.regions sv in + let cc = + end_proj_loans_symbolic config meta chain abs_id abs.regions sv + in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config chain abs_id) in + let cc = comp cc (end_abstraction_loans config meta chain abs_id) in (* Continue *) cc cf ctx -and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) - (abs_id : AbstractionId.id) : cm_fun = +and end_abstraction_borrows (config : config) (meta : Meta.meta) + (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = fun cf ctx -> log#ldebug (lazy @@ -1147,7 +1188,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) method! visit_aproj env sproj = (match sproj with - | AProjLoans _ -> raise (Failure "Unexpected") + | AProjLoans _ -> craise __FILE__ __LINE__ meta "Unexpected" | AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty)) | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj env sproj @@ -1156,7 +1197,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) method! visit_borrow_content _ bc = match bc with | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc) - | VReservedMutBorrow _ -> raise (Failure "Unreachable") + | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable" end in (* Lookup the abstraction *) @@ -1172,25 +1213,25 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) log#ldebug (lazy ("end_abstraction_borrows: found aborrow content: " - ^ aborrow_content_to_string ctx bc)); + ^ aborrow_content_to_string ~meta:(Some meta) 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 av in + let sv = convert_avalue_to_given_back_value meta 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 ek_all bid ended_borrow ctx in + let ctx = update_aborrow meta 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 bid sv ctx + give_back_value config meta 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 ek_all bid ended_borrow ctx in + let ctx = update_aborrow meta ek_all bid ended_borrow ctx in (* Give back *) - give_back_shared config bid ctx + give_back_shared config meta bid ctx | AProjSharedBorrow asb -> (* Retrieve the borrow ids *) let bids = @@ -1205,21 +1246,21 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) * can use to identify the whole set *) let repr_bid = List.hd bids in (* Replace the shared borrow with Bottom *) - let ctx = update_aborrow ek_all repr_bid ABottom ctx in + let ctx = update_aborrow meta ek_all repr_bid ABottom ctx in (* Give back the shared borrows *) let ctx = List.fold_left - (fun ctx bid -> give_back_shared config bid ctx) + (fun ctx bid -> give_back_shared config meta bid ctx) ctx bids in (* Continue *) ctx | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow -> - raise (Failure "Unexpected") + craise __FILE__ __LINE__ meta "Unexpected" in (* Reexplore *) - end_abstraction_borrows config chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id cf ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> log#ldebug @@ -1227,55 +1268,55 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) ("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 proj_ty in + let nsv = mk_fresh_symbolic_value meta proj_ty in (* Replace the proj_borrows - there should be exactly one *) let ended_borrow = AEndedProjBorrows nsv in - let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in + let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in (* Give back the symbolic value *) let ctx = - give_back_symbolic_value config abs.regions proj_ty sv nsv ctx + give_back_symbolic_value config meta abs.regions proj_ty sv nsv ctx in (* Reexplore *) - end_abstraction_borrows config chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id cf 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 ctx bc)); + ^ borrow_content_to_string ~meta:(Some meta) 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 (Some abs_id) allow_inner_loans bid ctx + end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx with - | Error _ -> raise (Failure "Unreachable") + | Error _ -> craise __FILE__ __LINE__ meta "Unreachable" | Ok (ctx, _) -> (* Give back *) - give_back_shared config bid ctx) + give_back_shared config meta bid ctx) | VMutBorrow (bid, v) -> ( (* Replace the mut borrow with bottom *) let allow_inner_loans = false in match - end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx + end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx with - | Error _ -> raise (Failure "Unreachable") + | Error _ -> craise __FILE__ __LINE__ meta "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 bid v ctx) - | VReservedMutBorrow _ -> raise (Failure "Unreachable") + give_back_value config meta bid v ctx) + | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable" in (* Reexplore *) - end_abstraction_borrows config chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id cf ctx (** Remove an abstraction from the context, as well as all its references *) -and end_abstraction_remove_from_context (_config : config) +and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta) (abs_id : AbstractionId.id) : cm_fun = fun cf ctx -> - let ctx, abs = ctx_remove_abs ctx abs_id in + 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 @@ -1296,12 +1337,12 @@ and end_abstraction_remove_from_context (_config : config) intersecting proj_borrows, either in the concrete context or in an abstraction *) -and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) - (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value) - : cm_fun = +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 -> (* Small helpers for sanity checks *) - let check ctx = no_aproj_over_symbolic_in_context sv ctx in + 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; @@ -1309,13 +1350,15 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) in (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in - match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with + match + lookup_intersecting_aproj_borrows_opt meta 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 abs_id sv ctx in + let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) @@ -1359,15 +1402,17 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) AbstractionId.Set.empty abs_ids in (* End the abstractions and continue *) - end_abstractions_aux config chain abs_ids cf ctx + end_abstractions_aux config meta chain abs_ids cf ctx in (* End the internal borrows projectors and the loans projector *) let cf_end_internal : cm_fun = fun cf ctx -> (* All the proj_borrows are owned: simply erase them *) - let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in + let ctx = + remove_intersecting_aproj_borrows_shared meta regions sv ctx + in (* End the loan itself *) - let ctx = update_aproj_loans_to_ended abs_id sv ctx in + let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) @@ -1399,48 +1444,51 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids) *) (* 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 abs_id sv AIgnoredProjBorrows ctx in + let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in (* Sanity check: no other occurrence of an intersecting projector of borrows *) - assert ( - Option.is_none - (lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx)); + sanity_check __FILE__ __LINE__ + (Option.is_none + (lookup_intersecting_aproj_borrows_opt meta explore_shared regions + sv ctx)) + meta; (* End the projector of loans *) - let ctx = update_aproj_loans_to_ended abs_id sv ctx in + let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in (* Sanity check *) check ctx; (* Continue *) cf ctx) else (* The borrows proj comes from a different abstraction: end it. *) - let cc = end_abstraction_aux config chain abs_id' in + let cc = end_abstraction_aux config meta chain abs_id' in (* Retry ending the projector of loans *) let cc = - comp cc (end_proj_loans_symbolic config chain abs_id regions sv) + comp cc (end_proj_loans_symbolic config meta chain abs_id regions sv) in (* Sanity check *) let cc = comp cc cf_check in (* Continue *) cc cf ctx -let end_borrow config : BorrowId.id -> cm_fun = end_borrow_aux config [] None +let end_borrow config (meta : Meta.meta) : BorrowId.id -> cm_fun = + end_borrow_aux config meta [] None -let end_borrows config : BorrowId.Set.t -> cm_fun = - end_borrows_aux config [] None +let end_borrows config (meta : Meta.meta) : BorrowId.Set.t -> cm_fun = + end_borrows_aux config meta [] None -let end_abstraction config = end_abstraction_aux config [] -let end_abstractions config = end_abstractions_aux config [] +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 id ctx = - get_cf_ctx_no_synth (end_borrow config id) ctx +let end_borrow_no_synth config meta id ctx = + get_cf_ctx_no_synth meta (end_borrow config meta id) ctx -let end_borrows_no_synth config ids ctx = - get_cf_ctx_no_synth (end_borrows config ids) ctx +let end_borrows_no_synth config meta ids ctx = + get_cf_ctx_no_synth meta (end_borrows config meta ids) ctx -let end_abstraction_no_synth config id ctx = - get_cf_ctx_no_synth (end_abstraction config id) ctx +let end_abstraction_no_synth config meta id ctx = + get_cf_ctx_no_synth meta (end_abstraction config meta id) ctx -let end_abstractions_no_synth config ids ctx = - get_cf_ctx_no_synth (end_abstractions config ids) ctx +let end_abstractions_no_synth config meta ids ctx = + get_cf_ctx_no_synth meta (end_abstractions config meta ids) ctx (** Helper function: see {!activate_reserved_mut_borrow}. @@ -1458,14 +1506,16 @@ let end_abstractions_no_synth config ids ctx = The loan to update mustn't be a borrowed value. *) -let promote_shared_loan_to_mut_loan (l : BorrowId.id) +let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) (cf : typed_value -> m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug (lazy ("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l - ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); + ^ "\n- context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) 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. * This is important because we can do: [let y = &two-phase ( *x );] @@ -1473,39 +1523,44 @@ let promote_shared_loan_to_mut_loan (l : BorrowId.id) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan ek l ctx with + match lookup_loan meta ek l ctx with | _, Concrete (VMutLoan _) -> - raise (Failure "Expected a shared loan, found a mut loan") + craise __FILE__ __LINE__ meta "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 *) - assert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1); + cassert __FILE__ __LINE__ + (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1) + meta "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. *) - assert (not (loans_in_value sv)); + sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta; (* Check there isn't {!Bottom} (this is actually an invariant *) - assert (not (bottom_in_value ctx.ended_regions sv)); + cassert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions sv)) + meta "There shouldn't be a bottom"; (* Check there aren't reserved borrows *) - assert (not (reserved_in_value sv)); + cassert __FILE__ __LINE__ + (not (reserved_in_value sv)) + meta "There shouldn't be reserved borrows"; (* Update the loan content *) - let ctx = update_loan ek l (VMutLoan l) ctx in + let ctx = update_loan meta ek l (VMutLoan l) ctx in (* Continue *) cf sv ctx | _, Abstract _ -> (* I don't think it is possible to have two-phase borrows involving borrows * returned by abstractions. I'm not sure how we could handle that anyway. *) - raise - (Failure - "Can't promote a shared loan to a mutable loan if the loan is \ - inside an abstraction") + craise __FILE__ __LINE__ meta + "Can't promote a shared loan to a mutable loan if the loan is inside a \ + region abstraction" (** Helper function: see {!activate_reserved_mut_borrow}. 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 (l : BorrowId.id) (cf : m_fun) - (borrowed_value : typed_value) : m_fun = +let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) + (cf : m_fun) (borrowed_value : typed_value) : m_fun = fun ctx -> (* Lookup the reserved borrow - note that we don't go inside borrows/loans: there can't be reserved borrows inside other borrows/loans @@ -1514,32 +1569,31 @@ let replace_reserved_borrow_with_mut_borrow (l : BorrowId.id) (cf : m_fun) { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in let ctx = - match lookup_borrow ek l ctx with + match lookup_borrow meta ek l ctx with | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> - raise (Failure "Expected a reserved mutable borrow") + craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow" | Concrete (VReservedMutBorrow _) -> (* Update it *) - update_borrow ek l (VMutBorrow (l, borrowed_value)) ctx + update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx | Abstract _ -> (* This can't happen for sure *) - raise - (Failure - "Can't promote a shared borrow to a mutable borrow if the borrow \ - is inside an abstraction") + 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 (** Promote a reserved mut borrow to a mut borrow. *) -let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun - = +let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) + (l : BorrowId.id) : cm_fun = fun cf ctx -> (* Lookup the value *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in - match lookup_loan ek l ctx with - | _, Concrete (VMutLoan _) -> raise (Failure "Unreachable") + match lookup_loan meta ek l ctx with + | _, Concrete (VMutLoan _) -> craise __FILE__ __LINE__ meta "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. @@ -1549,11 +1603,11 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun (* End the loans *) let cc = match lc with - | VSharedLoan (bids, _) -> end_borrows config bids - | VMutLoan bid -> end_borrow config bid + | VSharedLoan (bids, _) -> end_borrows config meta bids + | VMutLoan bid -> end_borrow config meta bid in (* Recursive call *) - let cc = comp cc (promote_reserved_mut_borrow config l) in + let cc = comp cc (promote_reserved_mut_borrow config meta l) in (* Continue *) cc cf ctx | None -> @@ -1562,37 +1616,38 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun log#ldebug (lazy ("activate_reserved_mut_borrow: resulting value:\n" - ^ typed_value_to_string ctx sv)); - assert (not (loans_in_value sv)); - assert (not (bottom_in_value ctx.ended_regions sv)); - assert (not (reserved_in_value sv)); + ^ typed_value_to_string ~meta:(Some meta) ctx sv)); + sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta; + sanity_check __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions sv)) + meta; + sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) 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 bids in + let cc = end_borrows config meta bids 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 l) in + let cc = comp cc (promote_shared_loan_to_mut_loan meta l) 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 l cf borrowed_value) + replace_reserved_borrow_with_mut_borrow meta l cf borrowed_value) in (* Continue *) cc cf ctx) | _, Abstract _ -> (* I don't think it is possible to have two-phase borrows involving borrows * returned by abstractions. I'm not sure how we could handle that anyway. *) - raise - (Failure - "Can't activate a reserved mutable borrow referencing a loan inside\n\ - \ an abstraction") + craise __FILE__ __LINE__ meta + "Can't activate a reserved mutable borrow referencing a loan inside\n\ + \ a region abstraction" -let destructure_abs (abs_kind : abs_kind) (can_end : bool) +let destructure_abs (meta : Meta.meta) (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 @@ -1605,7 +1660,7 @@ let destructure_abs (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 _ = raise (Failure "Unreachable") in + let push_fail _ = craise __FILE__ __LINE__ meta "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 = @@ -1620,13 +1675,15 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) match lc with | ASharedLoan (bids, sv, child_av) -> (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.value)); + cassert __FILE__ __LINE__ + (not (value_has_borrows ctx sv.value)) + meta "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 child_av.ty in + let ignored = mk_aignored meta child_av.ty in let value = ALoan (ASharedLoan (bids, sv, ignored)) in push { value; ty }; (* Explore the child *) @@ -1642,13 +1699,15 @@ let destructure_abs (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 child_av.ty in + let ignored = mk_aignored meta 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 *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); - assert (opt_bid = None); + 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; (* Simply explore the child *) list_avalues false push_fail child_av | AEndedMutLoan @@ -1658,19 +1717,21 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) { child = child_av; given_back = _; given_back_meta = _ } | AIgnoredSharedLoan child_av -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); + cassert __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) + meta "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] *) - assert allow_borrows; + sanity_check __FILE__ __LINE__ allow_borrows meta; (* 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 child_av.ty in + let ignored = mk_aignored meta child_av.ty in let value = ABorrow (AMutBorrow (bid, ignored)) in push { value; ty } | ASharedBorrow _ -> @@ -1678,19 +1739,24 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) push av | AIgnoredMutBorrow (opt_bid, child_av) -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); - assert (opt_bid = None); + 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; (* Just explore the child *) list_avalues false push_fail child_av | AEndedIgnoredMutBorrow { child = child_av; given_back = _; given_back_meta = _ } -> (* We don't support nested borrows for now *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)); + cassert __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) + meta "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 *) - assert (asb = []); + cassert __FILE__ __LINE__ (asb = []) meta + "Nested borrows are not supported yet"; (* Nothing specific to do *) () | AEndedMutBorrow _ | AEndedSharedBorrow -> @@ -1698,11 +1764,13 @@ let destructure_abs (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) *) - raise (Failure "Unreachable")) + craise __FILE__ __LINE__ meta "Unreachable") | ASymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) + sanity_check __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos ty)) + meta and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in match v.value with @@ -1714,19 +1782,22 @@ let destructure_abs (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 -> raise (Failure "Unreachable") + | VBottom -> craise __FILE__ __LINE__ meta "Unreachable" | VBorrow _ -> (* We don't support nested borrows for now *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "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 *) - assert (ty_no_regions ty); + cassert __FILE__ __LINE__ (ty_no_regions ty) meta + "Nested borrows are not supported yet"; let av : typed_avalue = - assert (not (value_has_loans_or_borrows ctx sv.value)); + sanity_check __FILE__ __LINE__ + (not (value_has_loans_or_borrows ctx sv.value)) + meta; (* We introduce fresh ids for the symbolic values *) let mk_value_with_fresh_sids (v : typed_value) : typed_value = let visitor = @@ -1741,17 +1812,21 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) in let sv = mk_value_with_fresh_sids sv in (* Create the new avalue *) - let value = ALoan (ASharedLoan (bids, sv, mk_aignored ty)) in + let value = + ALoan (ASharedLoan (bids, sv, mk_aignored meta ty)) + in { value; ty } in let avl = List.append [ av ] avl in (avl, sv)) else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) }) - | VMutLoan _ -> raise (Failure "Unreachable")) + | VMutLoan _ -> craise __FILE__ __LINE__ meta "Unreachable") | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - assert (not (ty_has_borrows ctx.type_ctx.type_infos ty)); + sanity_check __FILE__ __LINE__ + (not (ty_has_borrows ctx.type_ctx.type_infos ty)) + meta; ([], v) in @@ -1761,16 +1836,16 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool) (* Update *) { abs0 with avalues; kind = abs_kind; can_end } -let abs_is_destructured (destructure_shared_values : bool) (ctx : eval_ctx) - (abs : abs) : bool = +let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool) + (ctx : eval_ctx) (abs : abs) : bool = let abs' = - destructure_abs abs.kind abs.can_end destructure_shared_values ctx abs + destructure_abs meta abs.kind abs.can_end destructure_shared_values ctx abs in abs = abs' -let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) - (destructure_shared_values : bool) (ctx : eval_ctx) (v : typed_value) : - abs list = +let convert_value_to_abstractions (meta : Meta.meta) (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 *) let absl = ref [] in let push_abs (r_id : RegionId.id) (avalues : typed_avalue list) : unit = @@ -1807,7 +1882,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) log#ldebug (lazy ("convert_value_to_abstractions: to_avalues:\n- value: " - ^ typed_value_to_string ctx v)); + ^ typed_value_to_string ~meta:(Some meta) ctx v)); let ty = v.ty in match v.value with @@ -1851,23 +1926,27 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) (avl, { v with value = VAdt adt }) | VBorrow bc -> ( let _, ref_ty, kind = ty_as_ref ty in - assert (ty_no_regions ref_ty); + cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta + "Nested borrows are not supported yet"; (* Sanity check *) - assert allow_borrows; + sanity_check __FILE__ __LINE__ allow_borrows meta; (* Convert the borrow content *) match bc with | VSharedBorrow bid -> - assert (ty_no_regions ref_ty); + cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta + "Nested borrows are not supported yet"; let ty = TRef (RFVar r_id, ref_ty, kind) in let value = ABorrow (ASharedBorrow bid) in ([ { value; ty } ], v) | VMutBorrow (bid, bv) -> let r_id = if group then r_id else fresh_region_id () in (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx bv.value)); + cassert __FILE__ __LINE__ + (not (value_has_borrows ctx bv.value)) + meta "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 ref_ty in + let ignored = mk_aignored meta ref_ty in let av = ABorrow (AMutBorrow (bid, ignored)) in let av = { value = av; ty } in (* Continue exploring, looking for loans (and forbidding borrows, @@ -1877,18 +1956,21 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) (av :: avl, value) | VReservedMutBorrow _ -> (* This borrow should have been activated *) - raise (Failure "Unexpected")) + craise __FILE__ __LINE__ meta "Unexpected") | VLoan lc -> ( match lc with | VSharedLoan (bids, sv) -> let r_id = if group then r_id else fresh_region_id () in (* We don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.value)); + cassert __FILE__ __LINE__ + (not (value_has_borrows ctx sv.value)) + meta "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 *) - assert (ty_no_regions ty); + cassert __FILE__ __LINE__ (ty_no_regions ty) meta + "Nested borrows are not supported yet"; let ty = mk_ref_ty (RFVar r_id) ty RShared in - let ignored = mk_aignored ty in + let ignored = mk_aignored meta 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 @@ -1904,16 +1986,19 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool) | VMutLoan bid -> (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) - assert (ty_no_regions ty); + cassert __FILE__ __LINE__ (ty_no_regions ty) meta + "Nested borrows are not supported yet"; let ty = mk_ref_ty (RFVar r_id) ty RMut in - let ignored = mk_aignored ty in + let ignored = mk_aignored meta ty in let av = ALoan (AMutLoan (bid, ignored)) in let av = { value = av; ty } in ([ av ], v)) | VSymbolic _ -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - assert (not (value_has_borrows ctx v.value)); + cassert __FILE__ __LINE__ + (not (value_has_borrows ctx v.value)) + meta "Nested borrows are not supported yet"; (* Return nothing *) ([], v) in @@ -1954,8 +2039,8 @@ type merge_abstraction_info = { - all the borrows are destructured (for instance, shared loans can't contain shared loans). *) -let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : - merge_abstraction_info = +let compute_merge_abstraction_info (meta : Meta.meta) (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 let borrows_loans : borrow_or_loan_id list ref = ref [] in @@ -1967,26 +2052,32 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : in let push_loans ids (lc : g_loan_content_with_ty) : unit = - assert (BorrowId.Set.disjoint !loans ids); + sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) meta; loans := BorrowId.Set.union !loans ids; BorrowId.Set.iter (fun id -> - assert (not (BorrowId.Map.mem id !loan_to_content)); + sanity_check __FILE__ __LINE__ + (not (BorrowId.Map.mem id !loan_to_content)) + meta; 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 = - assert (not (BorrowId.Set.mem id !loans)); + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) meta; loans := BorrowId.Set.add id !loans; - assert (not (BorrowId.Map.mem id !loan_to_content)); + sanity_check __FILE__ __LINE__ + (not (BorrowId.Map.mem id !loan_to_content)) + meta; 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 = - assert (not (BorrowId.Set.mem id !borrows)); + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) meta; borrows := BorrowId.Set.add id !borrows; - assert (not (BorrowId.Map.mem id !borrow_to_content)); + sanity_check __FILE__ __LINE__ + (not (BorrowId.Map.mem id !borrow_to_content)) + meta; borrow_to_content := BorrowId.Map.add id bc !borrow_to_content; borrows_loans := BorrowId id :: !borrows_loans in @@ -2009,23 +2100,23 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : let ty = match Option.get env with | Concrete ty -> ty - | Abstract _ -> raise (Failure "Unreachable") + | Abstract _ -> craise __FILE__ __LINE__ meta "Unreachable" in (match lc with | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc)) - | VMutLoan _ -> raise (Failure "Unreachable")); + | VMutLoan _ -> craise __FILE__ __LINE__ meta "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) *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" method! visit_aloan_content env lc = let ty = match Option.get env with - | Concrete _ -> raise (Failure "Unreachable") + | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable" | Abstract ty -> ty in (* Register the loans *) @@ -2035,14 +2126,14 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) - raise (Failure "Unreachable")); + craise __FILE__ __LINE__ meta "Unreachable"); (* Continue *) super#visit_aloan_content env lc method! visit_aborrow_content env bc = let ty = match Option.get env with - | Concrete _ -> raise (Failure "Unreachable") + | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable" | Abstract ty -> ty in (* Explore the borrow content *) @@ -2056,18 +2147,20 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) : | AsbProjReborrows _ -> (* Can only happen if the symbolic value (potentially) contains borrows - i.e., we have nested borrows *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" in List.iter register asb | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow -> (* The abstraction has been destructured, so those shouldn't appear *) - raise (Failure "Unreachable")); + craise __FILE__ __LINE__ meta "Unreachable"); super#visit_aborrow_content env bc method! visit_symbolic_value _ sv = (* Sanity check: no borrows *) - assert (not (symbolic_value_has_borrows ctx sv)) + sanity_check __FILE__ __LINE__ + (not (symbolic_value_has_borrows ctx sv)) + meta end in @@ -2134,19 +2227,25 @@ type merge_duplicates_funcs = { Merge two abstractions into one, without updating the context. *) -let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) - (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs) - (abs1 : abs) : abs = +let merge_into_abstraction_aux (meta : Meta.meta) (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 ctx abs0 - ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1)); + ("merge_into_abstraction_aux:\n- abs0:\n" + ^ abs_to_string meta ctx abs0 + ^ "\n\n- abs1:\n" + ^ abs_to_string meta ctx abs1)); (* Check that the abstractions are destructured *) if !Config.sanity_checks then ( let destructure_shared_values = true in - assert (abs_is_destructured destructure_shared_values ctx abs0); - assert (abs_is_destructured destructure_shared_values ctx abs1)); + sanity_check __FILE__ __LINE__ + (abs_is_destructured meta destructure_shared_values ctx abs0) + meta; + sanity_check __FILE__ __LINE__ + (abs_is_destructured meta destructure_shared_values ctx abs1) + meta); (* Compute the relevant information *) let { @@ -2156,7 +2255,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) loan_to_content = loan_to_content0; borrow_to_content = borrow_to_content0; } = - compute_merge_abstraction_info ctx abs0 + compute_merge_abstraction_info meta ctx abs0 in let { @@ -2166,14 +2265,16 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) loan_to_content = loan_to_content1; borrow_to_content = borrow_to_content1; } = - compute_merge_abstraction_info ctx abs1 + compute_merge_abstraction_info meta ctx abs1 in (* Sanity check: there is no loan/borrows which appears in both abstractions, unless we allow to merge duplicates *) if merge_funs = None then ( - assert (BorrowId.Set.disjoint borrows0 borrows1); - assert (BorrowId.Set.disjoint loans0 loans1)); + sanity_check __FILE__ __LINE__ + (BorrowId.Set.disjoint borrows0 borrows1) + meta; + sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) meta); (* Merge. There are several cases: @@ -2200,7 +2301,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) log#ldebug (lazy ("merge_into_abstraction_aux: push_avalue: " - ^ typed_avalue_to_string ctx av)); + ^ typed_avalue_to_string ~meta:(Some meta) ctx av)); avalues := av :: !avalues in let push_opt_avalue av = @@ -2214,7 +2315,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) in let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t = let bids = BorrowId.Set.diff bids intersect in - assert (not (BorrowId.Set.is_empty bids)); + sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) meta; bids in let filter_bid (bid : BorrowId.id) : BorrowId.id option = @@ -2242,11 +2343,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) (Option.get merge_funs).merge_ashared_borrows id ty0 ty1 | AProjSharedBorrow _, AProjSharedBorrow _ -> (* Unreachable because requires nested borrows *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" in let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) @@ -2254,12 +2355,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) match (bc0, bc1) with | Concrete _, Concrete _ -> (* This can happen only in case of nested borrows *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | Abstract (ty0, bc0), Abstract (ty1, bc1) -> merge_aborrow_contents ty0 bc0 ty1 bc1 | Concrete _, Abstract _ | Abstract _, Concrete _ -> (* TODO: is it really unreachable? *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" in let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty) @@ -2277,7 +2378,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) (* 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 *) - assert (BorrowId.Set.equal ids0 ids1); + sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) meta; let ids = ids0 in if BorrowId.Set.is_empty ids then ( (* If the set of ids is empty, we can eliminate this shared loan. @@ -2289,10 +2390,14 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) to preserve (in practice it works because we destructure the shared values in the abstractions, and forbid nested borrows). *) - assert (not (value_has_loans_or_borrows ctx sv0.value)); - assert (not (value_has_loans_or_borrows ctx sv0.value)); - assert (is_aignored child0.value); - assert (is_aignored child1.value); + sanity_check __FILE__ __LINE__ + (not (value_has_loans_or_borrows ctx sv0.value)) + meta; + 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; None) else ( (* Register the loan ids *) @@ -2304,7 +2409,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" in (* Note that because we may filter ids from a set of id, this function has @@ -2315,12 +2420,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) match (lc0, lc1) with | Concrete _, Concrete _ -> (* This can not happen: the values should have been destructured *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | Abstract (ty0, lc0), Abstract (ty1, lc1) -> merge_aloan_contents ty0 lc0 ty1 lc1 | Concrete _, Abstract _ | Abstract _, Concrete _ -> (* TODO: is it really unreachable? *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" in (* Note that we first explore the borrows/loans of [abs1], because we @@ -2361,12 +2466,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) a concrete borrow can only happen inside a shared loan *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | Abstract (ty, bc) -> { value = ABorrow bc; ty }) | Some bc0, Some bc1 -> - assert (merge_funs <> None); + sanity_check __FILE__ __LINE__ (merge_funs <> None) meta; merge_g_borrow_contents bc0 bc1 - | None, None -> raise (Failure "Unreachable") + | None, None -> craise __FILE__ __LINE__ meta "Unreachable" in push_avalue av) | LoanId bid -> @@ -2399,15 +2504,19 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) | Concrete _ -> (* This shouldn't happen because the avalues should have been destructured. *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" | Abstract (ty, lc) -> ( match lc with | ASharedLoan (bids, sv, child) -> let bids = filter_bids bids in - assert (not (BorrowId.Set.is_empty bids)); - assert (is_aignored child.value); - assert ( - not (value_has_loans_or_borrows ctx sv.value)); + sanity_check __FILE__ __LINE__ + (not (BorrowId.Set.is_empty bids)) + meta; + sanity_check __FILE__ __LINE__ + (is_aignored child.value) meta; + sanity_check __FILE__ __LINE__ + (not (value_has_loans_or_borrows ctx sv.value)) + meta; let lc = ASharedLoan (bids, sv, child) in set_loans_as_merged bids; Some { value = ALoan lc; ty } @@ -2418,11 +2527,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) - raise (Failure "Unreachable"))) + craise __FILE__ __LINE__ meta "Unreachable")) | Some lc0, Some lc1 -> - assert (merge_funs <> None); + sanity_check __FILE__ __LINE__ (merge_funs <> None) meta; merge_g_loan_contents lc0 lc1 - | None, None -> raise (Failure "Unreachable") + | None, None -> craise __FILE__ __LINE__ meta "Unreachable" in push_opt_avalue av)) borrows_loans; @@ -2440,7 +2549,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> raise (Failure "Unexpected") + | _ -> craise __FILE__ __LINE__ meta "Unexpected" in let aborrows, aloans = List.partition is_borrow avalues in List.append aborrows aloans @@ -2475,7 +2584,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) in (* Sanity check *) - if !Config.sanity_checks then assert (abs_is_destructured true ctx abs); + sanity_check __FILE__ __LINE__ (abs_is_destructured meta true ctx abs) meta; (* Return *) abs @@ -2486,9 +2595,9 @@ 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 (abs_kind : abs_kind) (can_end : bool) - (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) - (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) : +let merge_into_abstraction (meta : Meta.meta) (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 = (* Lookup the abstractions *) let abs0 = ctx_lookup_abs ctx abs_id0 in @@ -2496,13 +2605,13 @@ let merge_into_abstraction (abs_kind : abs_kind) (can_end : bool) (* Merge them *) let nabs = - merge_into_abstraction_aux abs_kind can_end merge_funs ctx abs0 abs1 + merge_into_abstraction_aux meta 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 ctx abs_id1 nabs) in - let ctx = fst (ctx_remove_abs ctx abs_id0) in + let ctx = fst (ctx_subst_abs meta ctx abs_id1 nabs) in + let ctx = fst (ctx_remove_abs meta 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 diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index e47ba82d..30b75790 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -8,37 +8,40 @@ open Cps applies this change to an environment [ctx] by inserting a new borrow id in the set of borrows tracked by a shared value, referenced by the [original_bid] argument. *) -val reborrow_shared : BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx +val reborrow_shared : + Meta.meta -> BorrowId.id -> BorrowId.id -> eval_ctx -> eval_ctx (** End a borrow identified by its id, while preserving the invariants. If the borrow is inside another borrow/an abstraction or contains loans, [end_borrow] will end those borrows/abstractions/loans first. *) -val end_borrow : config -> BorrowId.id -> cm_fun +val end_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun (** End a set of borrows identified by their ids, while preserving the invariants. *) -val end_borrows : config -> BorrowId.Set.t -> cm_fun +val end_borrows : config -> Meta.meta -> BorrowId.Set.t -> cm_fun (** End an abstraction while preserving the invariants. *) -val end_abstraction : config -> AbstractionId.id -> cm_fun +val end_abstraction : config -> Meta.meta -> AbstractionId.id -> cm_fun (** End a set of abstractions while preserving the invariants. *) -val end_abstractions : config -> AbstractionId.Set.t -> cm_fun +val end_abstractions : config -> Meta.meta -> AbstractionId.Set.t -> cm_fun (** End a borrow and return the resulting environment, ignoring synthesis *) -val end_borrow_no_synth : config -> BorrowId.id -> eval_ctx -> eval_ctx +val end_borrow_no_synth : + config -> Meta.meta -> BorrowId.id -> eval_ctx -> eval_ctx (** End a set of borrows and return the resulting environment, ignoring synthesis *) -val end_borrows_no_synth : config -> BorrowId.Set.t -> eval_ctx -> eval_ctx +val end_borrows_no_synth : + config -> Meta.meta -> BorrowId.Set.t -> eval_ctx -> eval_ctx (** End an abstraction and return the resulting environment, ignoring synthesis *) val end_abstraction_no_synth : - config -> AbstractionId.id -> eval_ctx -> eval_ctx + config -> Meta.meta -> AbstractionId.id -> eval_ctx -> eval_ctx (** End a set of abstractions and return the resulting environment, ignoring synthesis *) val end_abstractions_no_synth : - config -> AbstractionId.Set.t -> eval_ctx -> eval_ctx + config -> Meta.meta -> AbstractionId.Set.t -> eval_ctx -> eval_ctx (** Promote a reserved mut borrow to a mut borrow, while preserving the invariants. @@ -49,7 +52,7 @@ val end_abstractions_no_synth : the corresponding shared loan with a mutable loan (after having ended the other shared borrows which point to this loan). *) -val promote_reserved_mut_borrow : config -> BorrowId.id -> cm_fun +val promote_reserved_mut_borrow : config -> Meta.meta -> BorrowId.id -> cm_fun (** Transform an abstraction to an abstraction where the values are not structured. @@ -91,7 +94,8 @@ val promote_reserved_mut_borrow : config -> BorrowId.id -> cm_fun - [ctx] - [abs] *) -val destructure_abs : abs_kind -> bool -> bool -> eval_ctx -> abs -> abs +val destructure_abs : + Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> abs -> abs (** Return [true] if the values in an abstraction are destructured. @@ -99,7 +103,7 @@ val destructure_abs : abs_kind -> bool -> bool -> eval_ctx -> abs -> abs The input boolean is [destructure_shared_value]. See {!destructure_abs}. *) -val abs_is_destructured : bool -> eval_ctx -> abs -> bool +val abs_is_destructured : Meta.meta -> bool -> eval_ctx -> abs -> bool (** Turn a value into a abstractions. @@ -125,7 +129,7 @@ val abs_is_destructured : bool -> eval_ctx -> abs -> bool - [v] *) val convert_value_to_abstractions : - abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list + Meta.meta -> abs_kind -> bool -> bool -> eval_ctx -> typed_value -> abs list (** See {!merge_into_abstraction}. @@ -232,6 +236,7 @@ type merge_duplicates_funcs = { results from the merge. *) val merge_into_abstraction : + Meta.meta -> abs_kind -> bool -> merge_duplicates_funcs option -> |