diff options
Diffstat (limited to 'compiler/InterpreterBorrowsCore.ml')
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 456 |
1 files changed, 228 insertions, 228 deletions
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index e7da045c..b13d545c 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -3,17 +3,15 @@ also in Invariants or InterpreterProjectors *) -module T = Types -module V = Values -module C = Contexts -module Subst = Substitute -module L = Logging +open Types +open Values +open Contexts open Utils open TypesUtils open InterpreterUtils (** The local logger *) -let log = L.borrows_log +let log = Logging.borrows_log (** TODO: cleanup this a bit, once we have a better understanding about what we need. @@ -33,19 +31,19 @@ type exploration_kind = { let ek_all : exploration_kind = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } -type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id +type borrow_ids = Borrows of BorrowId.Set.t | Borrow of BorrowId.id [@@deriving show] type borrow_ids_or_symbolic_value = | BorrowIds of borrow_ids - | SymbolicValue of V.symbolic_value + | SymbolicValue of symbolic_value [@@deriving show] exception FoundBorrowIds of borrow_ids type priority_borrows_or_abs = | OuterBorrows of borrow_ids - | OuterAbs of V.AbstractionId.id + | OuterAbs of AbstractionId.id | InnerLoans of borrow_ids [@@deriving show] @@ -55,20 +53,17 @@ let update_if_none opt x = match opt with None -> Some x | _ -> opt exception FoundPriority of priority_borrows_or_abs type loan_or_borrow_content = - | LoanContent of V.loan_content - | BorrowContent of V.borrow_content + | LoanContent of loan_content + | BorrowContent of borrow_content [@@deriving show] -type borrow_or_abs_id = - | BorrowId of V.BorrowId.id - | AbsId of V.AbstractionId.id - +type borrow_or_abs_id = BorrowId of BorrowId.id | AbsId of AbstractionId.id type borrow_or_abs_ids = borrow_or_abs_id list let borrow_or_abs_id_to_string (id : borrow_or_abs_id) : string = match id with - | AbsId id -> "abs@" ^ V.AbstractionId.to_string id - | BorrowId id -> "l@" ^ V.BorrowId.to_string id + | AbsId id -> "abs@" ^ AbstractionId.to_string id + | BorrowId id -> "l@" ^ BorrowId.to_string id let borrow_or_abs_ids_chain_to_string (ids : borrow_or_abs_ids) : string = let ids = List.rev ids in @@ -88,24 +83,29 @@ let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id) (** Helper function. This function allows to define in a generic way a comparison of **region types**. - See [projections_interesect] for instance. - + See [projections_intersect] for instance. + + Important: the regions in the types mustn't be erased. + [default]: default boolean to return, when comparing types with no regions [combine]: how to combine booleans [compare_regions]: how to compare regions TODO: is there a way of deriving such a comparison? + TODO: rename *) let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) - (compare_regions : T.RegionId.id T.region -> T.RegionId.id T.region -> bool) - (ty1 : T.rty) (ty2 : T.rty) : bool = + (compare_regions : region -> region -> bool) (ty1 : rty) (ty2 : rty) : bool + = let compare = compare_rtys default combine compare_regions in + (* Sanity check - TODO: don't do this at every recursive call *) + assert (ty_is_rty ty1 && ty_is_rty ty2); (* Normalize the associated types *) match (ty1, ty2) with - | T.Literal lit1, T.Literal lit2 -> + | TLiteral lit1, TLiteral lit2 -> assert (lit1 = lit2); default - | T.Adt (id1, generics1), T.Adt (id2, generics2) -> + | TAdt (id1, generics1), TAdt (id2, generics2) -> assert (id1 = id2); (* There are no regions in the const generics, so we ignore them, but we still check they are the same, for sanity *) @@ -141,7 +141,7 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) in (* Combine *) combine params_b tys_b - | T.Ref (r1, ty1, kind1), T.Ref (r2, ty2, kind2) -> + | TRef (r1, ty1, kind1), TRef (r2, ty2, kind2) -> (* Sanity check *) assert (kind1 = kind2); (* Explanation for the case where we check if projections intersect: @@ -150,10 +150,10 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) let regions_b = compare_regions r1 r2 in let tys_b = compare ty1 ty2 in combine regions_b tys_b - | T.TypeVar id1, T.TypeVar id2 -> + | TVar id1, TVar id2 -> assert (id1 = id2); default - | T.TraitType _, T.TraitType _ -> + | TTraitType _, TTraitType _ -> (* The types should have been normalized. If after normalization we get trait types, we can consider them as variables *) assert (ty1 = ty2); @@ -161,8 +161,8 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool) | _ -> log#lerror (lazy - ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ T.show_rty ty1 - ^ "\n- ty2: " ^ T.show_rty ty2)); + ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1 + ^ "\n- ty2: " ^ show_ty ty2)); raise (Failure "Unreachable") (** Check if two different projections intersect. This is necessary when @@ -172,8 +172,8 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> 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 (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty) - (rset2 : T.RegionId.Set.t) : bool = +let projections_intersect (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 = @@ -183,9 +183,12 @@ let projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty) (** Check if the first projection contains the second projection. We use this function when checking invariants. + + The regions in the types shouldn't be erased (this function will raise an exception + otherwise). *) -let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty) - (rset2 : T.RegionId.Set.t) : bool = +let projection_contains (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 = @@ -201,8 +204,8 @@ let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty) 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 (ek : exploration_kind) (l : V.BorrowId.id) - (ctx : C.eval_ctx) : (abs_or_var_id * g_loan_content) option = +let lookup_loan_opt (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 * and cleaner *) @@ -210,19 +213,19 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.iter_eval_ctx as super + inherit [_] iter_eval_ctx as super method! visit_borrow_content env bc = match bc with - | V.SharedBorrow bid -> + | VSharedBorrow bid -> (* Nothing specific to do *) - super#visit_SharedBorrow env bid - | V.ReservedMutBorrow bid -> + super#visit_VSharedBorrow env bid + | VReservedMutBorrow bid -> (* Nothing specific to do *) - super#visit_ReservedMutBorrow env bid - | V.MutBorrow (bid, mv) -> + super#visit_VReservedMutBorrow env bid + | VMutBorrow (bid, mv) -> (* Control the dive *) - if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv + if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv else () (** We reimplement {!visit_Loan} (rather than the more precise functions @@ -232,53 +235,53 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) *) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> (* Check if this is the loan we are looking for, and control the dive *) - if V.BorrowId.Set.mem l bids then + if BorrowId.Set.mem l bids then raise (FoundGLoanContent (Concrete lc)) else if ek.enter_shared_loans then - super#visit_SharedLoan env bids sv + super#visit_VSharedLoan env bids sv else () - | V.MutLoan bid -> + | VMutLoan bid -> (* Check if this is the loan we are looking for *) if bid = l then raise (FoundGLoanContent (Concrete lc)) - else super#visit_MutLoan env bid + else super#visit_VMutLoan env bid (** Note that we don't control diving inside the abstractions: if we allow to dive inside abstractions, we allow to go anywhere (because there are no use cases requiring finer control) *) method! visit_aloan_content env lc = match lc with - | V.AMutLoan (bid, av) -> + | AMutLoan (bid, av) -> if bid = l then raise (FoundGLoanContent (Abstract lc)) else super#visit_AMutLoan env bid av - | V.ASharedLoan (bids, v, av) -> - if V.BorrowId.Set.mem l bids then + | ASharedLoan (bids, v, av) -> + if BorrowId.Set.mem l bids then raise (FoundGLoanContent (Abstract lc)) else super#visit_ASharedLoan env bids v av - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedSharedLoan (_, _) + | AIgnoredMutLoan (_, _) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AIgnoredSharedLoan _ -> + | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc - method! visit_Var env bv v = + method! visit_EBinding env bv v = assert (Option.is_none !abs_or_var); abs_or_var := Some (match bv with - | VarBinder b -> VarId b.C.index - | DummyBinder id -> DummyVarId id); - super#visit_Var env bv v; + | BVar b -> VarId b.index + | BDummy id -> DummyVarId id); + super#visit_EBinding env bv v; abs_or_var := None - method! visit_Abs env abs = + method! visit_EAbs env abs = assert (Option.is_none !abs_or_var); if ek.enter_abs then ( - abs_or_var := Some (AbsId abs.V.abs_id); - super#visit_Abs env abs; + abs_or_var := Some (AbsId abs.abs_id); + super#visit_EAbs env abs; abs_or_var := None) else () end @@ -297,7 +300,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) The loan is referred to by a borrow id. Raises an exception if no loan was found. *) -let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) : +let lookup_loan (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : abs_or_var_id * g_loan_content = match lookup_loan_opt ek l ctx with | None -> raise (Failure "Unreachable") @@ -309,13 +312,13 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) : This is a helper function: it might break invariants. *) -let update_loan (ek : exploration_kind) (l : V.BorrowId.id) - (nlc : V.loan_content) (ctx : C.eval_ctx) : C.eval_ctx = +let update_loan (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 () : V.loan_content = + let update () : loan_content = assert (not !r); r := true; nlc @@ -323,32 +326,32 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_borrow_content env bc = match bc with - | V.SharedBorrow _ | V.ReservedMutBorrow _ -> + | VSharedBorrow _ | VReservedMutBorrow _ -> (* Nothing specific to do *) super#visit_borrow_content env bc - | V.MutBorrow (bid, mv) -> + | VMutBorrow (bid, mv) -> (* Control the dive into mutable borrows *) - if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv - else V.MutBorrow (bid, mv) + if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv + else VMutBorrow (bid, mv) (** We reimplement {!visit_loan_content} (rather than one of the sub- functions) on purpose: exhaustive matches are good for maintenance *) method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> (* Shared loan: check if this is the loan we are looking for, and control the dive. *) - if V.BorrowId.Set.mem l bids then update () + if BorrowId.Set.mem l bids then update () else if ek.enter_shared_loans then - super#visit_SharedLoan env bids sv - else V.SharedLoan (bids, sv) - | V.MutLoan bid -> + super#visit_VSharedLoan env bids sv + else VSharedLoan (bids, sv) + | VMutLoan bid -> (* Mut loan: checks if this is the loan we are looking for *) - if bid = l then update () else super#visit_MutLoan env bid + if bid = l then update () else super#visit_VMutLoan env bid (** Note that once inside the abstractions, we don't control diving (there are no use cases requiring finer control). @@ -372,13 +375,13 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) This is a helper function: it might break invariants. *) -let update_aloan (ek : exploration_kind) (l : V.BorrowId.id) - (nlc : V.aloan_content) (ctx : C.eval_ctx) : C.eval_ctx = +let update_aloan (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 () : V.aloan_content = + let update () : aloan_content = assert (not !r); r := true; nlc @@ -386,21 +389,21 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_aloan_content env lc = match lc with - | V.AMutLoan (bid, av) -> + | AMutLoan (bid, av) -> if bid = l then update () else super#visit_AMutLoan env bid av - | V.ASharedLoan (bids, v, av) -> - if V.BorrowId.Set.mem l bids then update () + | ASharedLoan (bids, v, av) -> + if BorrowId.Set.mem l bids then update () else super#visit_ASharedLoan env bids v av - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedSharedLoan (_, _) + | AIgnoredMutLoan (_, _) + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AIgnoredSharedLoan _ -> + | AIgnoredSharedLoan _ -> super#visit_aloan_content env lc (** Note that once inside the abstractions, we don't control diving @@ -416,50 +419,50 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id) ctx (** Lookup a borrow content from a borrow id. *) -let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) - (ctx : C.eval_ctx) : g_borrow_content option = +let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) + : g_borrow_content option = let obj = object - inherit [_] C.iter_eval_ctx as super + inherit [_] iter_eval_ctx as super method! visit_borrow_content env bc = match bc with - | V.MutBorrow (bid, mv) -> + | VMutBorrow (bid, mv) -> (* Check the borrow id and control the dive *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) - else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv + else if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv else () - | V.SharedBorrow bid -> + | VSharedBorrow bid -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () - | V.ReservedMutBorrow bid -> + | VReservedMutBorrow bid -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () method! visit_loan_content env lc = match lc with - | V.MutLoan bid -> - (* Nothing special to do *) super#visit_MutLoan env bid - | V.SharedLoan (bids, sv) -> + | VMutLoan bid -> + (* Nothing special to do *) super#visit_VMutLoan env bid + | VSharedLoan (bids, sv) -> (* Control the dive *) - if ek.enter_shared_loans then super#visit_SharedLoan env bids sv + if ek.enter_shared_loans then super#visit_VSharedLoan env bids sv else () method! visit_aborrow_content env bc = match bc with - | V.AMutBorrow (bid, av) -> + | AMutBorrow (bid, av) -> if bid = l then raise (FoundGBorrowContent (Abstract bc)) else super#visit_AMutBorrow env bid av - | V.ASharedBorrow bid -> + | ASharedBorrow bid -> if bid = l then raise (FoundGBorrowContent (Abstract bc)) else super#visit_ASharedBorrow env bid - | V.AIgnoredMutBorrow (_, _) - | V.AEndedMutBorrow _ - | V.AEndedIgnoredMutBorrow + | AIgnoredMutBorrow (_, _) + | AEndedMutBorrow _ + | AEndedIgnoredMutBorrow { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedBorrow -> + | AEndedSharedBorrow -> super#visit_aborrow_content env bc - | V.AProjSharedBorrow asb -> + | AProjSharedBorrow asb -> if borrow_in_asb l asb then raise (FoundGBorrowContent (Abstract bc)) else () @@ -478,8 +481,8 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) Raise an exception if no loan was found *) -let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) - : g_borrow_content = +let lookup_borrow (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : + g_borrow_content = match lookup_borrow_opt ek l ctx with | None -> raise (Failure "Unreachable") | Some lc -> lc @@ -490,13 +493,13 @@ let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) This is a helper function: it might break invariants. *) -let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) - (nbc : V.borrow_content) (ctx : C.eval_ctx) : C.eval_ctx = +let update_borrow (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 () : V.borrow_content = + let update () : borrow_content = assert (not !r); r := true; nbc @@ -504,31 +507,32 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_borrow_content env bc = match bc with - | V.MutBorrow (bid, mv) -> + | VMutBorrow (bid, mv) -> (* Check the id and control dive *) if bid = l then update () - else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv - else V.MutBorrow (bid, mv) - | V.SharedBorrow bid -> + else if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv + else VMutBorrow (bid, mv) + | VSharedBorrow bid -> (* Check the id *) - if bid = l then update () else super#visit_SharedBorrow env bid - | V.ReservedMutBorrow bid -> + if bid = l then update () else super#visit_VSharedBorrow env bid + | VReservedMutBorrow bid -> (* Check the id *) - if bid = l then update () else super#visit_ReservedMutBorrow env bid + if bid = l then update () + else super#visit_VReservedMutBorrow env bid method! visit_loan_content env lc = match lc with - | V.SharedLoan (bids, sv) -> + | VSharedLoan (bids, sv) -> (* Control the dive *) - if ek.enter_shared_loans then super#visit_SharedLoan env bids sv - else V.SharedLoan (bids, sv) - | V.MutLoan bid -> + if ek.enter_shared_loans then super#visit_VSharedLoan env bids sv + else VSharedLoan (bids, sv) + | VMutLoan bid -> (* Nothing specific to do *) - super#visit_MutLoan env bid + super#visit_VMutLoan env bid method! visit_abs env abs = if ek.enter_abs then super#visit_abs env abs else abs @@ -546,13 +550,13 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) This is a helper function: it might break invariants. *) -let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) - (ctx : C.eval_ctx) : C.eval_ctx = +let update_aborrow (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 () : V.avalue = + let update () : avalue = assert (not !r); r := true; nv @@ -560,22 +564,22 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_ABorrow env bc = match bc with - | V.AMutBorrow (bid, av) -> + | AMutBorrow (bid, av) -> if bid = l then update () - else V.ABorrow (super#visit_AMutBorrow env bid av) - | V.ASharedBorrow bid -> + else ABorrow (super#visit_AMutBorrow env bid av) + | ASharedBorrow bid -> if bid = l then update () - else V.ABorrow (super#visit_ASharedBorrow env bid) - | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedSharedBorrow - | V.AEndedIgnoredMutBorrow _ -> + else ABorrow (super#visit_ASharedBorrow env bid) + | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow + | AEndedIgnoredMutBorrow _ -> super#visit_ABorrow env bc - | V.AProjSharedBorrow asb -> + | AProjSharedBorrow asb -> if borrow_in_asb l asb then update () - else V.ABorrow (super#visit_AProjSharedBorrow env asb) + else ABorrow (super#visit_AProjSharedBorrow env asb) method! visit_abs env abs = if ek.enter_abs then super#visit_abs env abs else abs @@ -588,16 +592,16 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) ctx (** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *) -let update_outer_borrows (outer : V.AbstractionId.id option * borrow_ids option) - (x : borrow_ids) : V.AbstractionId.id option * borrow_ids option = +let update_outer_borrows (outer : AbstractionId.id option * borrow_ids option) + (x : borrow_ids) : AbstractionId.id option * borrow_ids option = let abs, opt = outer in (abs, update_if_none opt x) (** Return the first loan we find in a value *) -let get_first_loan_in_value (v : V.typed_value) : V.loan_content option = +let get_first_loan_in_value (v : typed_value) : loan_content option = let obj = object - inherit [_] V.iter_typed_value + inherit [_] iter_typed_value method! visit_loan_content _ lc = raise (FoundLoanContent lc) end in @@ -608,10 +612,10 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option = with FoundLoanContent lc -> Some lc (** Return the first loan we find in a list of values *) -let get_first_loan_in_values (vs : V.typed_value list) : V.loan_content option = +let get_first_loan_in_values (vs : typed_value list) : loan_content option = let obj = object - inherit [_] V.iter_typed_value + inherit [_] iter_typed_value method! visit_loan_content _ lc = raise (FoundLoanContent lc) end in @@ -622,10 +626,10 @@ let get_first_loan_in_values (vs : V.typed_value list) : V.loan_content option = with FoundLoanContent lc -> Some lc (** Return the first borrow we find in a value *) -let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option = +let get_first_borrow_in_value (v : typed_value) : borrow_content option = let obj = object - inherit [_] V.iter_typed_value + inherit [_] iter_typed_value method! visit_borrow_content _ bc = raise (FoundBorrowContent bc) end in @@ -643,10 +647,10 @@ let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option = - if [false]: return the first loan we find, do not dive into borrowed values *) let get_first_outer_loan_or_borrow_in_value (with_borrows : bool) - (v : V.typed_value) : loan_or_borrow_content option = + (v : typed_value) : loan_or_borrow_content option = let obj = object - inherit [_] V.iter_typed_value + inherit [_] iter_typed_value method! visit_borrow_content _ bc = if with_borrows then raise (FoundBorrowContent bc) else () @@ -662,17 +666,13 @@ let get_first_outer_loan_or_borrow_in_value (with_borrows : bool) | FoundLoanContent lc -> Some (LoanContent lc) | FoundBorrowContent bc -> Some (BorrowContent bc) -type gproj_borrows = - | AProjBorrows of V.AbstractionId.id * V.symbolic_value - | ProjBorrows of V.symbolic_value - let proj_borrows_intersects_proj_loans - (proj_borrows : T.RegionId.Set.t * V.symbolic_value * T.rty) - (proj_loans : T.RegionId.Set.t * V.symbolic_value) : bool = + (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 l_sv.V.sv_ty l_regions b_ty b_regions + projections_intersect 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 @@ -689,8 +689,8 @@ let proj_borrows_intersects_proj_loans found, as well as the projection types used in those abstractions. *) type looked_up_aproj_borrows = - | NonSharedProj of V.AbstractionId.id * T.rty - | SharedProjs of (V.AbstractionId.id * T.rty) list + | NonSharedProj of AbstractionId.id * rty + | SharedProjs of (AbstractionId.id * rty) list (** Lookup the aproj_borrows (including aproj_shared_borrows) over a symbolic value which intersect a given set of regions. @@ -701,15 +701,15 @@ type looked_up_aproj_borrows = This is a helper function. *) let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) - (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : + (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) : V.AbstractionId.id * T.rty) : unit = + let set_non_shared ((id, ty) : AbstractionId.id * rty) : unit = match !found with | None -> found := Some (NonSharedProj (id, ty)) | Some _ -> raise (Failure "Unreachable") in - let add_shared (x : V.AbstractionId.id * T.rty) : unit = + let add_shared (x : AbstractionId.id * rty) : unit = match !found with | None -> found := Some (SharedProjs [ x ]) | Some (SharedProjs pl) -> found := Some (SharedProjs (x :: pl)) @@ -718,7 +718,7 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty = if proj_borrows_intersects_proj_loans - (abs.V.regions, sv', proj_ty) + (abs.regions, sv', proj_ty) (regions, sv) then let x = (abs.abs_id, proj_ty) in @@ -727,7 +727,7 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) in let obj = object - inherit [_] C.iter_eval_ctx as super + inherit [_] iter_eval_ctx as super method! visit_abs _ abs = super#visit_abs (Some abs) abs method! visit_abstract_shared_borrow abs asb = @@ -739,8 +739,8 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) if lookup_shared then let abs = Option.get abs in match asb with - | V.AsbBorrow _ -> () - | V.AsbProjReborrows (sv', proj_ty) -> + | AsbBorrow _ -> () + | AsbProjReborrows (sv', proj_ty) -> let is_shared = true in check_add_proj_borrows is_shared abs sv' proj_ty else () @@ -772,9 +772,8 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) Returns the id of the owning abstraction, and the projection type used in this abstraction. *) -let lookup_intersecting_aproj_borrows_not_shared_opt - (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : - (V.AbstractionId.id * T.rty) option = +let lookup_intersecting_aproj_borrows_not_shared_opt (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 lookup_shared regions sv ctx with | None -> None @@ -787,10 +786,10 @@ let lookup_intersecting_aproj_borrows_not_shared_opt This is a helper function: it might break invariants. *) let update_intersecting_aproj_borrows (can_update_shared : bool) - (update_shared : V.AbstractionId.id -> T.rty -> V.abstract_shared_borrows) - (update_non_shared : V.AbstractionId.id -> T.rty -> V.aproj) - (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : - C.eval_ctx = + (update_shared : AbstractionId.id -> rty -> abstract_shared_borrows) + (update_non_shared : AbstractionId.id -> rty -> aproj) + (regions : RegionId.Set.t) (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx + = (* Small helpers for sanity checks *) let shared = ref None in let add_shared () = @@ -804,7 +803,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) let check_proj_borrows is_shared abs sv' proj_ty = if proj_borrows_intersects_proj_loans - (abs.V.regions, sv', proj_ty) + (abs.regions, sv', proj_ty) (regions, sv) then ( if is_shared then add_shared () else set_non_shared (); @@ -814,7 +813,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) (* The visitor *) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_abs _ abs = super#visit_abs (Some abs) abs method! visit_abstract_shared_borrows abs asb = @@ -823,11 +822,10 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) (* Explore *) if can_update_shared then let abs = Option.get abs in - let update (asb : V.abstract_shared_borrow) : - V.abstract_shared_borrows = + let update (asb : abstract_shared_borrow) : abstract_shared_borrows = match asb with - | V.AsbBorrow _ -> [ asb ] - | V.AsbProjReborrows (sv', proj_ty) -> + | AsbBorrow _ -> [ asb ] + | AsbProjReborrows (sv', proj_ty) -> let is_shared = true in if check_proj_borrows is_shared abs sv' proj_ty then update_shared abs.abs_id proj_ty @@ -863,8 +861,8 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) This is a helper function: it might break invariants. *) -let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t) - (sv : V.symbolic_value) (nv : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = +let update_intersecting_aproj_borrows_non_shared (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 _ _ = raise (Failure "Unexpected") in @@ -889,8 +887,8 @@ let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t) This is a helper function: it might break invariants. *) -let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) - (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = +let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t) + (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Small helpers *) let can_update_shared = true in let update_shared _ _ = [] in @@ -921,20 +919,24 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) Note that for sanity, this function checks that we update *at least* one projector of loans. + + [proj_ty]: shouldn't contain erased regions. [subst]: takes as parameters the abstraction in which we perform the substitution and the list of given back values at the projector of - loans where we perform the substitution (see the fields in {!V.AProjLoans}). + loans where we perform the substitution (see the fields in {!AProjLoans}). 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 (proj_regions : T.RegionId.Set.t) - (proj_ty : T.rty) (sv : V.symbolic_value) - (subst : V.abs -> (V.msymbolic_value * V.aproj) list -> V.aproj) - (ctx : C.eval_ctx) : C.eval_ctx = +let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t) + (proj_ty : rty) (sv : symbolic_value) + (subst : abs -> (msymbolic_value * aproj) list -> aproj) (ctx : eval_ctx) : + eval_ctx = + (* *) + assert (ty_is_rty proj_ty); (* Small helpers for sanity checks *) let updated = ref false in - let update abs local_given_back : V.aproj = + let update abs local_given_back : aproj = (* Note that we can update more than once! *) updated := true; subst abs local_given_back @@ -942,7 +944,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) (* The visitor *) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_abs _ abs = super#visit_abs (Some abs) abs method! visit_aproj abs sproj = @@ -955,8 +957,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) if same_symbolic_id sv sv' then ( assert (sv.sv_ty = sv'.sv_ty); if - projections_intersect proj_ty proj_regions sv'.V.sv_ty - abs.regions + projections_intersect proj_ty proj_regions sv'.sv_ty abs.regions then update abs given_back else super#visit_aproj (Some abs) sproj) else super#visit_aproj (Some abs) sproj @@ -969,18 +970,18 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) (* Return *) ctx -(** Helper function: lookup an {!V.AProjLoans} by using an abstraction id and a +(** Helper function: lookup an {!AProjLoans} by using an abstraction id and a symbolic value. We return the information from the looked up projector of loans. See the - fields in {!V.AProjLoans} (we don't return the symbolic value, because it + fields in {!AProjLoans} (we don't return the symbolic value, because it is equal to [sv]). Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) -let lookup_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) - (ctx : C.eval_ctx) : (V.msymbolic_value * V.aproj) list = +let lookup_aproj_loans (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 = @@ -991,12 +992,12 @@ let lookup_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) (* The visitor *) let obj = object - inherit [_] C.iter_eval_ctx as super + inherit [_] iter_eval_ctx as super method! visit_abs _ abs = if abs.abs_id = abs_id then super#visit_abs (Some abs) abs else () - method! visit_aproj (abs : V.abs option) sproj = + method! visit_aproj (abs : abs option) sproj = (match sproj with | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> @@ -1024,8 +1025,8 @@ let lookup_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) -let update_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) - (nproj : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = +let update_aproj_loans (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 () = @@ -1037,12 +1038,12 @@ let update_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) (* The visitor *) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_abs _ abs = if abs.abs_id = abs_id then super#visit_abs (Some abs) abs else abs - method! visit_aproj (abs : V.abs option) sproj = + method! visit_aproj (abs : abs option) sproj = match sproj with | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> @@ -1073,8 +1074,8 @@ let update_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) TODO: factorize with {!update_aproj_loans}? *) -let update_aproj_borrows (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) - (nproj : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = +let update_aproj_borrows (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 () = @@ -1086,12 +1087,12 @@ let update_aproj_borrows (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) (* The visitor *) let obj = object - inherit [_] C.map_eval_ctx as super + inherit [_] map_eval_ctx as super method! visit_abs _ abs = if abs.abs_id = abs_id then super#visit_abs (Some abs) abs else abs - method! visit_aproj (abs : V.abs option) sproj = + method! visit_aproj (abs : abs option) sproj = match sproj with | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> @@ -1114,26 +1115,26 @@ let update_aproj_borrows (abs_id : V.AbstractionId.id) (sv : V.symbolic_value) (** Helper function: might break invariants. - Converts an {!V.AProjLoans} to an {!V.AEndedProjLoans}. The projector is identified + Converts an {!AProjLoans} to an {!AEndedProjLoans}. The projector is identified by a symbolic value and an abstraction id. *) -let update_aproj_loans_to_ended (abs_id : V.AbstractionId.id) - (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = +let update_aproj_loans_to_ended (abs_id : AbstractionId.id) + (sv : symbolic_value) (ctx : eval_ctx) : eval_ctx = (* Lookup the projector of loans *) let given_back = lookup_aproj_loans abs_id sv ctx in (* Create the new value for the projector *) - let nproj = V.AEndedProjLoans (sv, given_back) in + let nproj = AEndedProjLoans (sv, given_back) in (* Insert it *) let ctx = update_aproj_loans abs_id sv nproj ctx in (* Return *) ctx -let no_aproj_over_symbolic_in_context (sv : V.symbolic_value) (ctx : C.eval_ctx) - : unit = +let no_aproj_over_symbolic_in_context (sv : symbolic_value) (ctx : eval_ctx) : + unit = (* The visitor *) let obj = object - inherit [_] C.iter_eval_ctx as super + inherit [_] iter_eval_ctx as super method! visit_aproj env sproj = (match sproj with @@ -1154,44 +1155,44 @@ let no_aproj_over_symbolic_in_context (sv : V.symbolic_value) (ctx : C.eval_ctx) **Remark:** we don't take the *ignored* mut/shared loans into account. *) -let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) : +let get_first_non_ignored_aloan_in_abstraction (abs : abs) : borrow_ids_or_symbolic_value option = (* Explore to find a loan *) let obj = object - inherit [_] V.iter_abs as super + inherit [_] iter_abs as super method! visit_aloan_content env lc = match lc with - | V.AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid)) - | V.ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids)) - | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AEndedSharedLoan (_, _) -> + | AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid)) + | ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids)) + | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } + | AEndedSharedLoan (_, _) -> super#visit_aloan_content env lc - | V.AIgnoredMutLoan (_, _) -> + | AIgnoredMutLoan (_, _) -> (* Ignore *) super#visit_aloan_content env lc - | V.AEndedIgnoredMutLoan + | AEndedIgnoredMutLoan { given_back = _; child = _; given_back_meta = _ } - | V.AIgnoredSharedLoan _ -> + | AIgnoredSharedLoan _ -> (* Ignore *) super#visit_aloan_content env lc (** We may need to visit loan contents because of shared values *) method! visit_loan_content _ lc = match lc with - | V.MutLoan _ -> + | VMutLoan _ -> (* The mut loan linked to the mutable borrow present in a shared * value in an abstraction should be in an AProjBorrows *) raise (Failure "Unreachable") - | V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids)) + | VSharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids)) method! visit_aproj env sproj = (match sproj with - | V.AProjBorrows (_, _) - | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> + | AProjBorrows (_, _) + | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> () - | V.AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv)); + | AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv)); super#visit_aproj env sproj end in @@ -1207,16 +1208,15 @@ let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) : (* There are loan projections over symbolic values *) Some (SymbolicValue sv) -let lookup_shared_value_opt (ctx : C.eval_ctx) (bid : V.BorrowId.id) : - V.typed_value option = +let lookup_shared_value_opt (ctx : eval_ctx) (bid : BorrowId.id) : + typed_value option = match lookup_loan_opt ek_all bid ctx with | None -> None | Some (_, lc) -> ( match lc with - | Concrete (SharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> + | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> Some sv | _ -> None) -let lookup_shared_value (ctx : C.eval_ctx) (bid : V.BorrowId.id) : V.typed_value - = +let lookup_shared_value (ctx : eval_ctx) (bid : BorrowId.id) : typed_value = Option.get (lookup_shared_value_opt ctx bid) |