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/InterpreterBorrowsCore.ml | 194 ++++++++++++++++++------------------- 1 file changed, 97 insertions(+), 97 deletions(-) (limited to 'compiler/InterpreterBorrowsCore.ml') diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index a01be046..2628b26a 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -72,10 +72,10 @@ let borrow_or_abs_ids_chain_to_string (ids : borrow_or_abs_ids) : string = String.concat " -> " ids (** Add a borrow or abs id to a chain of ids, while checking that we don't loop *) -let add_borrow_or_abs_id_to_chain (meta : Meta.meta) (msg : string) +let add_borrow_or_abs_id_to_chain (span : Meta.span) (msg : string) (id : borrow_or_abs_id) (ids : borrow_or_abs_ids) : borrow_or_abs_ids = if List.mem id ids then - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span (msg ^ "detected a loop in the chain of ids: " ^ borrow_or_abs_ids_chain_to_string (id :: ids)) else id :: ids @@ -94,25 +94,25 @@ let add_borrow_or_abs_id_to_chain (meta : Meta.meta) (msg : string) TODO: is there a way of deriving such a comparison? TODO: rename *) -let rec compare_rtys (meta : Meta.meta) (default : bool) +let rec compare_rtys (span : Meta.span) (default : bool) (combine : bool -> bool -> bool) (compare_regions : region -> region -> bool) (ty1 : rty) (ty2 : rty) : bool = - let compare = compare_rtys meta default combine compare_regions in + let compare = compare_rtys span default combine compare_regions in (* Sanity check - TODO: don't do this at every recursive call *) - sanity_check __FILE__ __LINE__ (ty_is_rty ty1 && ty_is_rty ty2) meta; + sanity_check __FILE__ __LINE__ (ty_is_rty ty1 && ty_is_rty ty2) span; (* Normalize the associated types *) match (ty1, ty2) with | TLiteral lit1, TLiteral lit2 -> - sanity_check __FILE__ __LINE__ (lit1 = lit2) meta; + sanity_check __FILE__ __LINE__ (lit1 = lit2) span; default | TAdt (id1, generics1), TAdt (id2, generics2) -> - sanity_check __FILE__ __LINE__ (id1 = id2) meta; + sanity_check __FILE__ __LINE__ (id1 = id2) span; (* There are no regions in the const generics, so we ignore them, but we still check they are the same, for sanity *) sanity_check __FILE__ __LINE__ (generics1.const_generics = generics2.const_generics) - meta; + span; (* We also ignore the trait refs *) @@ -146,7 +146,7 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) combine params_b tys_b | TRef (r1, ty1, kind1), TRef (r2, ty2, kind2) -> (* Sanity check *) - sanity_check __FILE__ __LINE__ (kind1 = kind2) meta; + sanity_check __FILE__ __LINE__ (kind1 = kind2) span; (* Explanation for the case where we check if projections intersect: * the projections intersect if the borrows intersect or their contents * intersect. *) @@ -154,19 +154,19 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) let tys_b = compare ty1 ty2 in combine regions_b tys_b | TVar id1, TVar id2 -> - sanity_check __FILE__ __LINE__ (id1 = id2) meta; + sanity_check __FILE__ __LINE__ (id1 = id2) span; default | TTraitType _, TTraitType _ -> (* The types should have been normalized. If after normalization we get trait types, we can consider them as variables *) - sanity_check __FILE__ __LINE__ (ty1 = ty2) meta; + sanity_check __FILE__ __LINE__ (ty1 = ty2) span; default | _ -> log#ltrace (lazy ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1 ^ "\n- ty2: " ^ show_ty ty2)); - internal_error __FILE__ __LINE__ meta + internal_error __FILE__ __LINE__ span (** Check if two different projections intersect. This is necessary when giving a symbolic value to an abstraction: we need to check that @@ -175,14 +175,14 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) Note that the two abstractions have different views (in terms of regions) of the symbolic value (hence the two region types). *) -let projections_intersect (meta : Meta.meta) (ty1 : rty) +let projections_intersect (span : Meta.span) (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) (rset2 : RegionId.Set.t) : bool = let default = false in let combine b1 b2 = b1 || b2 in let compare_regions r1 r2 = region_in_set r1 rset1 && region_in_set r2 rset2 in - compare_rtys meta default combine compare_regions ty1 ty2 + compare_rtys span default combine compare_regions ty1 ty2 (** Check if the first projection contains the second projection. We use this function when checking invariants. @@ -190,14 +190,14 @@ let projections_intersect (meta : Meta.meta) (ty1 : rty) The regions in the types shouldn't be erased (this function will raise an exception otherwise). *) -let projection_contains (meta : Meta.meta) (ty1 : rty) (rset1 : RegionId.Set.t) +let projection_contains (span : Meta.span) (ty1 : rty) (rset1 : RegionId.Set.t) (ty2 : rty) (rset2 : RegionId.Set.t) : bool = let default = true in let combine b1 b2 = b1 && b2 in let compare_regions r1 r2 = region_in_set r1 rset1 || not (region_in_set r2 rset2) in - compare_rtys meta default combine compare_regions ty1 ty2 + compare_rtys span default combine compare_regions ty1 ty2 (** Lookup a loan content. @@ -207,7 +207,7 @@ let projection_contains (meta : Meta.meta) (ty1 : rty) (rset1 : RegionId.Set.t) the {!InterpreterUtils.abs_or_var_id} is not necessarily {!constructor:Aeneas.InterpreterUtils.abs_or_var_id.VarId} or {!constructor:Aeneas.InterpreterUtils.abs_or_var_id.DummyVarId}: there can be concrete loans in abstractions (in the shared values). *) -let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) +let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : (abs_or_var_id * g_loan_content) option = (* We store here whether we are inside an abstraction or a value - note that we * could also track that with the environment, it would probably be more idiomatic @@ -262,16 +262,16 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) if BorrowId.Set.mem l bids then raise (FoundGLoanContent (Abstract lc)) else super#visit_ASharedLoan env bids v av - | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc method! visit_EBinding env bv v = - sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) meta; + sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) span; abs_or_var := Some (match bv with @@ -281,7 +281,7 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) abs_or_var := None method! visit_EAbs env abs = - sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) meta; + sanity_check __FILE__ __LINE__ (Option.is_none !abs_or_var) span; if ek.enter_abs then ( abs_or_var := Some (AbsId abs.abs_id); super#visit_EAbs env abs; @@ -296,17 +296,17 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) with FoundGLoanContent lc -> ( match !abs_or_var with | Some abs_or_var -> Some (abs_or_var, lc) - | None -> craise __FILE__ __LINE__ meta "Inconsistent state") + | None -> craise __FILE__ __LINE__ span "Inconsistent state") (** Lookup a loan content. The loan is referred to by a borrow id. Raises an exception if no loan was found. *) -let lookup_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) +let lookup_loan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : abs_or_var_id * g_loan_content = - match lookup_loan_opt meta ek l ctx with - | None -> craise __FILE__ __LINE__ meta "Unreachable" + match lookup_loan_opt span ek l ctx with + | None -> craise __FILE__ __LINE__ span "Unreachable" | Some res -> res (** Update a loan content. @@ -315,14 +315,14 @@ let lookup_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) This is a helper function: it might break invariants. *) -let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) +let update_loan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (nlc : loan_content) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one loan: when updating * inside values, we check we don't update more than one loan. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : loan_content = - sanity_check __FILE__ __LINE__ (not !r) meta; + sanity_check __FILE__ __LINE__ (not !r) span; r := true; nlc in @@ -369,7 +369,7 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) - sanity_check __FILE__ __LINE__ !r meta; + sanity_check __FILE__ __LINE__ !r span; ctx (** Update a abstraction loan content. @@ -378,14 +378,14 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) This is a helper function: it might break invariants. *) -let update_aloan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) +let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (nlc : aloan_content) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one loan: when updating * inside values, we check we don't update more than one loan. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : aloan_content = - sanity_check __FILE__ __LINE__ (not !r) meta; + sanity_check __FILE__ __LINE__ (not !r) span; r := true; nlc in @@ -401,11 +401,11 @@ let update_aloan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) | ASharedLoan (bids, v, av) -> if BorrowId.Set.mem l bids then update () else super#visit_ASharedLoan env bids v av - | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc @@ -418,7 +418,7 @@ let update_aloan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) - sanity_check __FILE__ __LINE__ !r meta; + sanity_check __FILE__ __LINE__ !r span; ctx (** Lookup a borrow content from a borrow id. *) @@ -462,7 +462,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) | AIgnoredMutBorrow (_, _) | AEndedMutBorrow _ | AEndedIgnoredMutBorrow - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AEndedSharedBorrow -> super#visit_aborrow_content env bc | AProjSharedBorrow asb -> @@ -484,10 +484,10 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) Raise an exception if no loan was found *) -let lookup_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) +let lookup_borrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : g_borrow_content = match lookup_borrow_opt ek l ctx with - | None -> craise __FILE__ __LINE__ meta "Unreachable" + | None -> craise __FILE__ __LINE__ span "Unreachable" | Some lc -> lc (** Update a borrow content. @@ -496,14 +496,14 @@ let lookup_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) This is a helper function: it might break invariants. *) -let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) +let update_borrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (nbc : borrow_content) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one borrow: when updating * inside values, we check we don't update more than one borrow. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : borrow_content = - sanity_check __FILE__ __LINE__ (not !r) meta; + sanity_check __FILE__ __LINE__ (not !r) span; r := true; nbc in @@ -544,7 +544,7 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one borrow *) - sanity_check __FILE__ __LINE__ !r meta; + sanity_check __FILE__ __LINE__ !r span; ctx (** Update an abstraction borrow content. @@ -553,14 +553,14 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) This is a helper function: it might break invariants. *) -let update_aborrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) +let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (nv : avalue) (ctx : eval_ctx) : eval_ctx = (* We use a reference to check that we update exactly one borrow: when updating * inside values, we check we don't update more than one borrow. Then, upon * returning we check that we updated at least once. *) let r = ref false in let update () : avalue = - sanity_check __FILE__ __LINE__ (not !r) meta; + sanity_check __FILE__ __LINE__ (not !r) span; r := true; nv in @@ -591,7 +591,7 @@ let update_aborrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one borrow *) - cassert __FILE__ __LINE__ !r meta "No borrow was updated"; + cassert __FILE__ __LINE__ !r span "No borrow was updated"; ctx (** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *) @@ -669,13 +669,13 @@ let get_first_outer_loan_or_borrow_in_value (with_borrows : bool) | FoundLoanContent lc -> Some (LoanContent lc) | FoundBorrowContent bc -> Some (BorrowContent bc) -let proj_borrows_intersects_proj_loans (meta : Meta.meta) +let proj_borrows_intersects_proj_loans (span : Meta.span) (proj_borrows : RegionId.Set.t * symbolic_value * rty) (proj_loans : RegionId.Set.t * symbolic_value) : bool = let b_regions, b_sv, b_ty = proj_borrows in let l_regions, l_sv = proj_loans in if same_symbolic_id b_sv l_sv then - projections_intersect meta l_sv.sv_ty l_regions b_ty b_regions + projections_intersect span l_sv.sv_ty l_regions b_ty b_regions else false (** Result of looking up aproj_borrows which intersect a given aproj_loans in @@ -703,24 +703,24 @@ type looked_up_aproj_borrows = This is a helper function. *) -let lookup_intersecting_aproj_borrows_opt (meta : Meta.meta) +let lookup_intersecting_aproj_borrows_opt (span : Meta.span) (lookup_shared : bool) (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : looked_up_aproj_borrows option = let found : looked_up_aproj_borrows option ref = ref None in let set_non_shared ((id, ty) : AbstractionId.id * rty) : unit = match !found with | None -> found := Some (NonSharedProj (id, ty)) - | Some _ -> craise __FILE__ __LINE__ meta "Unreachable" + | Some _ -> craise __FILE__ __LINE__ span "Unreachable" in let add_shared (x : AbstractionId.id * rty) : unit = match !found with | None -> found := Some (SharedProjs [ x ]) | Some (SharedProjs pl) -> found := Some (SharedProjs (x :: pl)) - | Some (NonSharedProj _) -> craise __FILE__ __LINE__ meta "Unreachable" + | Some (NonSharedProj _) -> craise __FILE__ __LINE__ span "Unreachable" in let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty = if - proj_borrows_intersects_proj_loans meta + proj_borrows_intersects_proj_loans span (abs.regions, sv', proj_ty) (regions, sv) then @@ -736,7 +736,7 @@ let lookup_intersecting_aproj_borrows_opt (meta : Meta.meta) method! visit_abstract_shared_borrow abs asb = (* Sanity check *) (match !found with - | Some (NonSharedProj _) -> craise __FILE__ __LINE__ meta "Unreachable" + | Some (NonSharedProj _) -> craise __FILE__ __LINE__ span "Unreachable" | _ -> ()); (* Explore *) if lookup_shared then @@ -775,23 +775,23 @@ let lookup_intersecting_aproj_borrows_opt (meta : Meta.meta) Returns the id of the owning abstraction, and the projection type used in this abstraction. *) -let lookup_intersecting_aproj_borrows_not_shared_opt (meta : Meta.meta) +let lookup_intersecting_aproj_borrows_not_shared_opt (span : Meta.span) (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : (AbstractionId.id * rty) option = let lookup_shared = false in match - lookup_intersecting_aproj_borrows_opt meta lookup_shared regions sv ctx + lookup_intersecting_aproj_borrows_opt span lookup_shared regions sv ctx with | None -> None | Some (NonSharedProj (abs_id, rty)) -> Some (abs_id, rty) - | _ -> craise __FILE__ __LINE__ meta "Unexpected" + | _ -> craise __FILE__ __LINE__ span "Unexpected" (** Similar to {!lookup_intersecting_aproj_borrows_opt}, but updates the values. This is a helper function: it might break invariants. *) -let update_intersecting_aproj_borrows (meta : Meta.meta) +let update_intersecting_aproj_borrows (span : Meta.span) (can_update_shared : bool) (update_shared : AbstractionId.id -> rty -> abstract_shared_borrows) (update_non_shared : AbstractionId.id -> rty -> aproj) @@ -802,18 +802,18 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) let add_shared () = match !shared with | None -> shared := Some true - | Some b -> sanity_check __FILE__ __LINE__ b meta + | Some b -> sanity_check __FILE__ __LINE__ b span in let set_non_shared () = match !shared with | None -> shared := Some false | Some _ -> - craise __FILE__ __LINE__ meta + craise __FILE__ __LINE__ span "Found unexpected intersecting proj_borrows" in let check_proj_borrows is_shared abs sv' proj_ty = if - proj_borrows_intersects_proj_loans meta + proj_borrows_intersects_proj_loans span (abs.regions, sv', proj_ty) (regions, sv) then ( @@ -830,7 +830,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) method! visit_abstract_shared_borrows abs asb = (* Sanity check *) (match !shared with - | Some b -> sanity_check __FILE__ __LINE__ b meta + | Some b -> sanity_check __FILE__ __LINE__ b span | _ -> ()); (* Explore *) if can_update_shared then @@ -863,7 +863,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Check that we updated the context at least once *) - cassert __FILE__ __LINE__ (Option.is_some !shared) meta + cassert __FILE__ __LINE__ (Option.is_some !shared) span "Context was not updated"; (* Return *) ctx @@ -875,12 +875,12 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) This is a helper function: it might break invariants. *) -let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta) +let update_intersecting_aproj_borrows_non_shared (span : Meta.span) (regions : RegionId.Set.t) (sv : symbolic_value) (nv : aproj) (ctx : eval_ctx) : eval_ctx = (* Small helpers *) let can_update_shared = false in - let update_shared _ _ = craise __FILE__ __LINE__ meta "Unexpected" in + let update_shared _ _ = craise __FILE__ __LINE__ span "Unexpected" in let updated = ref false in let update_non_shared _ _ = (* We can update more than one borrow! *) @@ -889,11 +889,11 @@ let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta) in (* Update *) let ctx = - update_intersecting_aproj_borrows meta can_update_shared update_shared + update_intersecting_aproj_borrows span can_update_shared update_shared update_non_shared regions sv ctx in (* Check that we updated at least once *) - sanity_check __FILE__ __LINE__ !updated meta; + sanity_check __FILE__ __LINE__ !updated span; (* Return *) ctx @@ -902,15 +902,15 @@ let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta) This is a helper function: it might break invariants. *) -let remove_intersecting_aproj_borrows_shared (meta : Meta.meta) +let remove_intersecting_aproj_borrows_shared (span : Meta.span) (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Small helpers *) let can_update_shared = true in let update_shared _ _ = [] in - let update_non_shared _ _ = craise __FILE__ __LINE__ meta "Unexpected" in + let update_non_shared _ _ = craise __FILE__ __LINE__ span "Unexpected" in (* Update *) - update_intersecting_aproj_borrows meta can_update_shared update_shared + update_intersecting_aproj_borrows span can_update_shared update_shared update_non_shared regions sv ctx (** Updates the proj_loans intersecting some projection. @@ -944,12 +944,12 @@ let remove_intersecting_aproj_borrows_shared (meta : Meta.meta) Note that the symbolic value at this place is necessarily equal to [sv], which is why we don't give it as parameters. *) -let update_intersecting_aproj_loans (meta : Meta.meta) +let update_intersecting_aproj_loans (span : Meta.span) (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value) (subst : abs -> (msymbolic_value * aproj) list -> aproj) (ctx : eval_ctx) : eval_ctx = (* *) - sanity_check __FILE__ __LINE__ (ty_is_rty proj_ty) meta; + sanity_check __FILE__ __LINE__ (ty_is_rty proj_ty) span; (* Small helpers for sanity checks *) let updated = ref false in let update abs local_given_back : aproj = @@ -971,9 +971,9 @@ let update_intersecting_aproj_loans (meta : Meta.meta) | AProjLoans (sv', given_back) -> let abs = Option.get abs in if same_symbolic_id sv sv' then ( - sanity_check __FILE__ __LINE__ (sv.sv_ty = sv'.sv_ty) meta; + sanity_check __FILE__ __LINE__ (sv.sv_ty = sv'.sv_ty) span; if - projections_intersect meta proj_ty proj_regions sv'.sv_ty + projections_intersect span proj_ty proj_regions sv'.sv_ty abs.regions then update abs given_back else super#visit_aproj (Some abs) sproj) @@ -983,7 +983,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Check that we updated the context at least once *) - sanity_check __FILE__ __LINE__ !updated meta; + sanity_check __FILE__ __LINE__ !updated span; (* Return *) ctx @@ -997,13 +997,13 @@ let update_intersecting_aproj_loans (meta : Meta.meta) Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) -let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) +let lookup_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id) (sv : symbolic_value) (ctx : eval_ctx) : (msymbolic_value * aproj) list = (* Small helpers for sanity checks *) let found = ref None in let set_found x = (* There is at most one projector which corresponds to the description *) - sanity_check __FILE__ __LINE__ (Option.is_none !found) meta; + sanity_check __FILE__ __LINE__ (Option.is_none !found) span; found := Some x in (* The visitor *) @@ -1021,9 +1021,9 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) super#visit_aproj abs sproj | AProjLoans (sv', given_back) -> let abs = Option.get abs in - sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) meta; + sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span; if sv'.sv_id = sv.sv_id then ( - sanity_check __FILE__ __LINE__ (sv' = sv) meta; + sanity_check __FILE__ __LINE__ (sv' = sv) span; set_found given_back) else ()); super#visit_aproj abs sproj @@ -1042,13 +1042,13 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) -let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) +let update_aproj_loans (span : Meta.span) (abs_id : AbstractionId.id) (sv : symbolic_value) (nproj : aproj) (ctx : eval_ctx) : eval_ctx = (* Small helpers for sanity checks *) let found = ref false in let update () = (* We update at most once *) - sanity_check __FILE__ __LINE__ (not !found) meta; + sanity_check __FILE__ __LINE__ (not !found) span; found := true; nproj in @@ -1067,9 +1067,9 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) super#visit_aproj abs sproj | AProjLoans (sv', _) -> let abs = Option.get abs in - sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) meta; + sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span; if sv'.sv_id = sv.sv_id then ( - sanity_check __FILE__ __LINE__ (sv' = sv) meta; + sanity_check __FILE__ __LINE__ (sv' = sv) span; update ()) else super#visit_aproj (Some abs) sproj end @@ -1077,7 +1077,7 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Sanity check *) - sanity_check __FILE__ __LINE__ !found meta; + sanity_check __FILE__ __LINE__ !found span; (* Return *) ctx @@ -1091,13 +1091,13 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) TODO: factorize with {!update_aproj_loans}? *) -let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) +let update_aproj_borrows (span : Meta.span) (abs_id : AbstractionId.id) (sv : symbolic_value) (nproj : aproj) (ctx : eval_ctx) : eval_ctx = (* Small helpers for sanity checks *) let found = ref false in let update () = (* We update at most once *) - sanity_check __FILE__ __LINE__ (not !found) meta; + sanity_check __FILE__ __LINE__ (not !found) span; found := true; nproj in @@ -1116,9 +1116,9 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) super#visit_aproj abs sproj | AProjBorrows (sv', _proj_ty) -> let abs = Option.get abs in - sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) meta; + sanity_check __FILE__ __LINE__ (abs.abs_id = abs_id) span; if sv'.sv_id = sv.sv_id then ( - sanity_check __FILE__ __LINE__ (sv' = sv) meta; + sanity_check __FILE__ __LINE__ (sv' = sv) span; update ()) else super#visit_aproj (Some abs) sproj end @@ -1126,7 +1126,7 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Sanity check *) - sanity_check __FILE__ __LINE__ !found meta; + sanity_check __FILE__ __LINE__ !found span; (* Return *) ctx @@ -1135,18 +1135,18 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified by a symbolic value and an abstraction id. *) -let update_aproj_loans_to_ended (meta : Meta.meta) (abs_id : AbstractionId.id) +let update_aproj_loans_to_ended (span : Meta.span) (abs_id : AbstractionId.id) (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Lookup the projector of loans *) - let given_back = lookup_aproj_loans meta abs_id sv ctx in + let given_back = lookup_aproj_loans span abs_id sv ctx in (* Create the new value for the projector *) let nproj = AEndedProjLoans (sv, given_back) in (* Insert it *) - let ctx = update_aproj_loans meta abs_id sv nproj ctx in + let ctx = update_aproj_loans span abs_id sv nproj ctx in (* Return *) ctx -let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value) +let no_aproj_over_symbolic_in_context (span : Meta.span) (sv : symbolic_value) (ctx : eval_ctx) : unit = (* The visitor *) let obj = @@ -1164,7 +1164,7 @@ let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value) (* Apply *) try obj#visit_eval_ctx () ctx with Found -> - craise __FILE__ __LINE__ meta "update_aproj_loans_to_ended: failed" + craise __FILE__ __LINE__ span "update_aproj_loans_to_ended: failed" (** Helper function @@ -1173,7 +1173,7 @@ let no_aproj_over_symbolic_in_context (meta : Meta.meta) (sv : symbolic_value) **Remark:** we don't take the *ignored* mut/shared loans into account. *) -let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) : +let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) : borrow_ids_or_symbolic_value option = (* Explore to find a loan *) let obj = @@ -1184,14 +1184,14 @@ let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) : match lc with | AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid)) | ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids)) - | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) -> super#visit_aloan_content env lc | AIgnoredMutLoan (_, _) -> (* Ignore *) super#visit_aloan_content env lc | AEndedIgnoredMutLoan - { given_back = _; child = _; given_back_meta = _ } + { given_back = _; child = _; given_back_span = _ } | AIgnoredSharedLoan _ -> (* Ignore *) super#visit_aloan_content env lc @@ -1202,7 +1202,7 @@ let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) : | VMutLoan _ -> (* The mut loan linked to the mutable borrow present in a shared * value in an abstraction should be in an AProjBorrows *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | VSharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids)) method! visit_aproj env sproj = @@ -1226,9 +1226,9 @@ let get_first_non_ignored_aloan_in_abstraction (meta : Meta.meta) (abs : abs) : (* There are loan projections over symbolic values *) Some (SymbolicValue sv) -let lookup_shared_value_opt (meta : Meta.meta) (ctx : eval_ctx) +let lookup_shared_value_opt (span : Meta.span) (ctx : eval_ctx) (bid : BorrowId.id) : typed_value option = - match lookup_loan_opt meta ek_all bid ctx with + match lookup_loan_opt span ek_all bid ctx with | None -> None | Some (_, lc) -> ( match lc with @@ -1236,6 +1236,6 @@ let lookup_shared_value_opt (meta : Meta.meta) (ctx : eval_ctx) Some sv | _ -> None) -let lookup_shared_value (meta : Meta.meta) (ctx : eval_ctx) (bid : BorrowId.id) +let lookup_shared_value (span : Meta.span) (ctx : eval_ctx) (bid : BorrowId.id) : typed_value = - Option.get (lookup_shared_value_opt meta ctx bid) + Option.get (lookup_shared_value_opt span ctx bid) -- cgit v1.2.3