diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 4496 |
1 files changed, 137 insertions, 4359 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b105c97b..2789517e 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,16 +1,10 @@ +module L = Logging module T = Types -module V = Values -open Scalars -module E = Expressions -open Errors -module C = Contexts -module Subst = Substitute module A = CfimAst -module L = Logging -open TypesUtils -open ValuesUtils -module Inv = Invariants +open Utils open InterpreterUtils +open InterpreterExpressions +open InterpreterStatements (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -27,4342 +21,93 @@ open InterpreterUtils (* TODO: remove the config parameters when they are useless *) -(** TODO: change the name *) -type eval_error = Panic - -type 'a eval_result = ('a, eval_error) result - -(** TODO: move *) -let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool - = - match asb with - | V.AsbBorrow bid' -> bid' = bid - | V.AsbProjReborrows _ -> false - -(** TODO: move *) -let borrow_in_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrows) : bool - = - List.exists (borrow_is_asb bid) asb - -(** TODO: move *) -let remove_borrow_from_asb (bid : V.BorrowId.id) - (asb : V.abstract_shared_borrows) : V.abstract_shared_borrows = - let removed = ref 0 in - let asb = - List.filter - (fun asb -> - if not (borrow_is_asb bid asb) then true - else ( - removed := !removed + 1; - false)) - asb - in - assert (!removed = 1); - asb - -(* TODO: cleanup this a bit, once we have a better understanding about what we need *) -type exploration_kind = { - enter_shared_loans : bool; - enter_mut_borrows : bool; - enter_abs : bool; - (** Note that if we allow to enter abs, we don't check whether we enter - mutable/shared loans or borrows: there are no use cases requiring - a finer control. *) -} -(** This record controls how some generic helper lookup/update - functions behave, by restraining the kind of therms they can enter. -*) - -let ek_all : exploration_kind = - { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } - -(** We sometimes need to return a value whose type may vary depending on - whether we find it in a "concrete" value or an abstraction (ex.: loan - contents when we perform environment lookups by using borrow ids) *) -type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b - -type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs -(** Generic loan content: concrete or abstract *) - -type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs -(** Generic borrow content: concrete or abstract *) - -type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id - -exception Found -(** Utility exception - - When looking for something while exploring a term, it can be easier to - just throw an exception to signal we found what we were looking for. - *) - -exception FoundBorrowContent of V.borrow_content -(** Utility exception *) - -exception FoundLoanContent of V.loan_content -(** Utility exception *) - -exception FoundABorrowContent of V.aborrow_content -(** Utility exception *) - -exception FoundGBorrowContent of g_borrow_content -(** Utility exception *) - -exception FoundGLoanContent of g_loan_content -(** Utility exception *) - -(** Check if a value contains a borrow *) -let borrows_in_value (v : V.typed_value) : bool = - let obj = - object - inherit [_] V.iter_typed_value - - method! visit_borrow_content _env _ = raise Found - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - false - with Found -> true - -(** Check if a value contains inactivated mutable borrows *) -let inactivated_in_value (v : V.typed_value) : bool = - let obj = - object - inherit [_] V.iter_typed_value - - method! visit_InactivatedMutBorrow _env _ = raise Found - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - false - with Found -> true - -(** Check if a value contains a loan *) -let loans_in_value (v : V.typed_value) : bool = - let obj = - object - inherit [_] V.iter_typed_value - - method! visit_loan_content _env _ = raise Found - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - false - with Found -> true - -let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : - bool = - let obj = - object - inherit [_] C.iter_eval_ctx - - method! visit_Symbolic _ sv = - if sv.V.svalue.V.sv_id = sv_id then raise Found else () - - method! visit_ASymbolic _ aproj = - match aproj with - | AProjLoans sv | AProjBorrows (sv, _) -> - if sv.V.sv_id = sv_id then raise Found else () - - method! visit_abstract_shared_borrows _ asb = - let visit (asb : V.abstract_shared_borrow) : unit = - match asb with - | V.AsbBorrow _ -> () - | V.AsbProjReborrows (sv, _) -> - if sv.V.sv_id = sv_id then raise Found else () - in - List.iter visit asb - end - in - (* We use exceptions *) - try - obj#visit_eval_ctx () ctx; - false - with Found -> true - -(** Lookup a loan content. - - The loan is referred to by a borrow id. - - TODO: group abs_or_var_id and g_loan_content. - *) -let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) - (ctx : C.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 *) - let abs_or_var : abs_or_var_id option ref = ref None in - - let obj = - object - inherit [_] C.iter_eval_ctx as super - - method! visit_borrow_content env bc = - match bc with - | V.SharedBorrow bid -> - (* Nothing specific to do *) - super#visit_SharedBorrow env bid - | V.InactivatedMutBorrow bid -> - (* Nothing specific to do *) - super#visit_InactivatedMutBorrow env bid - | V.MutBorrow (bid, mv) -> - (* Control the dive *) - if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv - else () - - method! visit_loan_content env lc = - match lc with - | V.SharedLoan (bids, sv) -> - (* Check if this is the loan we are looking for, and control the dive *) - if V.BorrowId.Set.mem l bids then - raise (FoundGLoanContent (Concrete lc)) - else if ek.enter_shared_loans then - super#visit_SharedLoan env bids sv - else () - | V.MutLoan 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 - (** We reimplement [visit_Loan] (rather than the more precise functions - [visit_SharedLoan], etc.) on purpose: as we have an exhaustive match - below, we are more resilient to definition updates (the compiler - is our friend). - *) - - method! visit_aloan_content env lc = - match lc with - | V.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 - raise (FoundGLoanContent (Abstract lc)) - else super#visit_ASharedLoan env bids v av - | V.AEndedMutLoan { given_back; child } -> - super#visit_AEndedMutLoan env given_back child - | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av - | V.AIgnoredMutLoan (bid, av) -> super#visit_AIgnoredMutLoan env bid av - | V.AEndedIgnoredMutLoan { given_back; child } -> - super#visit_AEndedIgnoredMutLoan env given_back child - | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av - (** 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_Var env bv v = - assert (Option.is_none !abs_or_var); - abs_or_var := Some (VarId bv.C.index); - super#visit_Var env bv v; - abs_or_var := None - - method! visit_Abs 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) - else () - end - in - (* We use exceptions *) - try - obj#visit_eval_ctx () ctx; - None - with FoundGLoanContent lc -> ( - match !abs_or_var with - | Some abs_or_var -> Some (abs_or_var, lc) - | None -> failwith "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 (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) : - abs_or_var_id * g_loan_content = - match lookup_loan_opt ek l ctx with - | None -> failwith "Unreachable" - | Some res -> res - -(** Update a loan content. - - The loan is referred to by a borrow id. - - 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 = - (* 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 = - assert (not !r); - r := true; - nlc - in - - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_borrow_content env bc = - match bc with - | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> - (* Nothing specific to do *) - super#visit_borrow_content env bc - | V.MutBorrow (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) - - method! visit_loan_content env lc = - match lc with - | V.SharedLoan (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 () - else if ek.enter_shared_loans then - super#visit_SharedLoan env bids sv - else V.SharedLoan (bids, sv) - | V.MutLoan bid -> - (* Mut loan: checks if this is the loan we are looking for *) - if bid = l then update () else super#visit_MutLoan env bid - (** We reimplement [visit_loan_content] (rather than one of the sub- - functions) on purpose: exhaustive matches are good for maintenance *) - - method! visit_abs env abs = - if ek.enter_abs then super#visit_abs env abs else abs - (** Note that once inside the abstractions, we don't control diving - (there are no use cases requiring finer control). - Also, as we give back a [loan_content] (and not an [aloan_content]) - we don't need to do reimplement the visit functions for the values - inside the abstractions (rk.: there may be "concrete" values inside - abstractions, so there is a utility in diving inside). *) - end - in - - let ctx = obj#visit_eval_ctx () ctx in - (* Check that we updated at least one loan *) - assert !r; - ctx - -(** Update a abstraction loan content. - - The loan is referred to by a borrow 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 = - (* 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 = - assert (not !r); - r := true; - nlc - in - - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_aloan_content env lc = - match lc with - | V.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 () - else super#visit_ASharedLoan env bids v av - | V.AEndedMutLoan { given_back; child } -> - super#visit_AEndedMutLoan env given_back child - | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av - | V.AIgnoredMutLoan (bid, av) -> super#visit_AIgnoredMutLoan env bid av - | V.AEndedIgnoredMutLoan { given_back; child } -> - super#visit_AEndedIgnoredMutLoan env given_back child - | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av - - method! visit_abs env abs = - if ek.enter_abs then super#visit_abs env abs else abs - (** Note that once inside the abstractions, we don't control diving - (there are no use cases requiring finer control). *) - end - in - - let ctx = obj#visit_eval_ctx () ctx in - (* Check that we updated at least one loan *) - assert !r; - 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 obj = - object - inherit [_] C.iter_eval_ctx as super - - method! visit_borrow_content env bc = - match bc with - | V.MutBorrow (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 () - | V.SharedBorrow bid -> - (* Check the borrow id *) - if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () - | V.InactivatedMutBorrow 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) -> - (* Control the dive *) - if ek.enter_shared_loans then super#visit_SharedLoan env bids sv - else () - - method! visit_aborrow_content env bc = - match bc with - | V.AMutBorrow (bid, av) -> - if bid = l then raise (FoundGBorrowContent (Abstract bc)) - else super#visit_AMutBorrow env bid av - | V.ASharedBorrow bid -> - if bid = l then raise (FoundGBorrowContent (Abstract bc)) - else super#visit_ASharedBorrow env bid - | V.AIgnoredMutBorrow av -> super#visit_AIgnoredMutBorrow env av - | V.AProjSharedBorrow asb -> - if borrow_in_asb l asb then - raise (FoundGBorrowContent (Abstract bc)) - else () - - method! visit_abs env abs = - if ek.enter_abs then super#visit_abs env abs else () - end - in - (* We use exceptions *) - try - obj#visit_eval_ctx () ctx; - None - with FoundGBorrowContent lc -> Some lc - -(** Lookup a borrow content from a borrow 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 = - match lookup_borrow_opt ek l ctx with - | None -> failwith "Unreachable" - | Some lc -> lc - -(** Update a borrow content. - - The borrow is referred to by a borrow id. - - 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 = - (* 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 = - assert (not !r); - r := true; - nbc - in - - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_borrow_content env bc = - match bc with - | V.MutBorrow (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 -> - (* Check the id *) - if bid = l then update () else super#visit_SharedBorrow env bid - | V.InactivatedMutBorrow bid -> - (* Check the id *) - if bid = l then update () - else super#visit_InactivatedMutBorrow env bid - - method! visit_loan_content env lc = - match lc with - | V.SharedLoan (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 -> - (* Nothing specific to do *) - super#visit_MutLoan env bid - - method! visit_abs env abs = - if ek.enter_abs then super#visit_abs env abs else abs - end - in - - let ctx = obj#visit_eval_ctx () ctx in - (* Check that we updated at least one borrow *) - assert !r; - ctx - -(** Update an abstraction borrow content. - - The borrow is referred to by a borrow 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 = - (* 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 = - assert (not !r); - r := true; - nv - in - - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_ABorrow env bc = - match bc with - | V.AMutBorrow (bid, av) -> - if bid = l then update () - else V.ABorrow (super#visit_AMutBorrow env bid av) - | V.ASharedBorrow bid -> - if bid = l then update () - else V.ABorrow (super#visit_ASharedBorrow env bid) - | V.AIgnoredMutBorrow av -> - V.ABorrow (super#visit_AIgnoredMutBorrow env av) - | V.AProjSharedBorrow asb -> - if borrow_in_asb l asb then update () - else V.ABorrow (super#visit_AProjSharedBorrow env asb) - - method! visit_abs env abs = - if ek.enter_abs then super#visit_abs env abs else abs - end - in - - let ctx = obj#visit_eval_ctx () ctx in - (* Check that we updated at least one borrow *) - assert !r; - ctx - -(** The following type identifies the relative position of expressions (in - particular borrows) in other expressions. - - For instance, it is used to control [end_borrow]: we usually only allow - to end "outer" borrows, unless we perform a drop. -*) -type inner_outer = Inner | Outer - -type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id - -exception FoundBorrowIds of borrow_ids - -let update_if_none opt x = match opt with None -> Some x | _ -> opt - -(** Auxiliary function: see its usage in [end_borrow_get_borrow_in_value] *) -let update_outer_borrows (io : inner_outer) - (outer : V.AbstractionId.id option * borrow_ids option) (x : borrow_ids) : - V.AbstractionId.id option * borrow_ids option = - match io with - | Inner -> - (* If we can end inner borrows, we don't keep track of the outer borrows *) - outer - | Outer -> - 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 obj = - object - inherit [_] V.iter_typed_value - - method! visit_loan_content _ lc = raise (FoundLoanContent lc) - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - None - with FoundLoanContent lc -> Some lc - -(** Check if a region is in a set of regions *) -let region_in_set (r : T.RegionId.id T.region) (rset : T.RegionId.set_t) : bool - = - match r with T.Static -> false | T.Var id -> T.RegionId.Set.mem id rset - -(** Return the set of regions in an rty *) -let rty_regions (ty : T.rty) : T.RegionId.set_t = - let s = ref T.RegionId.Set.empty in - let add_region (r : T.RegionId.id T.region) = - match r with T.Static -> () | T.Var rid -> s := T.RegionId.Set.add rid !s - in - let obj = - object - inherit [_] T.iter_ty - - method! visit_'r _env r = add_region r - end - in - (* Explore the type *) - obj#visit_ty () ty; - (* Return the set of accumulated regions *) - !s - -let rty_regions_intersect (ty : T.rty) (regions : T.RegionId.set_t) : bool = - let ty_regions = rty_regions ty in - not (T.RegionId.Set.disjoint ty_regions regions) - -(** Check if two different projections intersect. This is necessary when - giving a symbolic value to an abstraction: we need to check that - the regions which are already ended inside the abstraction don't - intersect the regions over which we project in the new abstraction. - Note that the two abstractions have different views (in terms of regions) - of the symbolic value (hence the two region types). -*) -let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t) - (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool = - match (ty1, ty2) with - | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false - | T.Integer int_ty1, T.Integer int_ty2 -> - assert (int_ty1 = int_ty2); - false - | T.Adt (id1, regions1, tys1), T.Adt (id2, regions2, tys2) -> - assert (id1 = id2); - (* The intersection check for the ADTs is very crude: - * we check if some arguments intersect. As all the type and region - * parameters should be used somewhere in the ADT (otherwise rustc - * generates an error), it means that it should be equivalent to checking - * whether two fields intersect (and anyway comparing the field types is - * difficult in case of enumerations...). - * If we didn't have the above property enforced by the rust compiler, - * this check would still be a reasonable conservative approximation. *) - let regions = List.combine regions1 regions2 in - let tys = List.combine tys1 tys2 in - List.exists - (fun (r1, r2) -> region_in_set r1 rset1 && region_in_set r2 rset2) - regions - || List.exists - (fun (ty1, ty2) -> projections_intersect ty1 rset1 ty2 rset2) - tys - | T.Array ty1, T.Array ty2 | T.Slice ty1, T.Slice ty2 -> - projections_intersect ty1 rset1 ty2 rset2 - | T.Ref (r1, ty1, kind1), T.Ref (r2, ty2, kind2) -> - (* Sanity check *) - assert (kind1 = kind2); - (* The projections intersect if the borrows intersect or their contents - * intersect *) - (region_in_set r1 rset1 && region_in_set r2 rset2) - || projections_intersect ty1 rset1 ty2 rset2 - | _ -> failwith "Unreachable" - -(** Check if the ended regions of a comp projector over a symbolic value - intersect the regions listed in another projection *) -let symbolic_proj_comp_ended_regions_intersect_proj (s : V.symbolic_proj_comp) - (ty : T.rty) (regions : T.RegionId.set_t) : bool = - projections_intersect s.V.svalue.V.sv_ty s.V.rset_ended ty regions - -(** Check that a symbolic value doesn't contain ended regions. - - Note that we don't check that the set of ended regions is empty: we - check that the set of ended regions doesn't intersect the set of - regions used in the type (this is more general). -*) -let symbolic_proj_comp_ended_regions (s : V.symbolic_proj_comp) : bool = - let regions = rty_regions s.V.svalue.V.sv_ty in - not (T.RegionId.Set.disjoint regions s.rset_ended) - -(** Check if a [value] contains ⊥. - - Note that this function is very general: it also checks wether - symbolic values contain already ended regions. - *) -let bottom_in_value (v : V.typed_value) : bool = - let obj = - object - inherit [_] V.iter_typed_value - - method! visit_Bottom _ = raise Found - - method! visit_symbolic_proj_comp _ s = - if symbolic_proj_comp_ended_regions s then raise Found else () - end - in - (* We use exceptions *) - try - obj#visit_typed_value () v; - false - with Found -> true - -(** Check if an [avalue] contains ⊥. - - Note that this function is very general: it also checks wether - symbolic values contain already ended regions. - - TODO: remove? -*) -let bottom_in_avalue (v : V.typed_avalue) (_abs_regions : T.RegionId.set_t) : - bool = - let obj = - object - inherit [_] V.iter_typed_avalue - - method! visit_Bottom _ = raise Found - - method! visit_symbolic_proj_comp _ sv = - if symbolic_proj_comp_ended_regions sv then raise Found else () - - method! visit_aproj _ ap = - (* Nothing to do actually *) - match ap with - | V.AProjLoans _sv -> () - | V.AProjBorrows (_sv, _rty) -> () - end - in - (* We use exceptions *) - try - obj#visit_typed_avalue () v; - false - with Found -> true - -type outer_borrows_or_abs = - | OuterBorrows of borrow_ids - | OuterAbs of V.AbstractionId.id - -exception FoundOuter of outer_borrows_or_abs -(** Utility exception *) - -(** Auxiliary function. - - Apply a proj_borrows on a shared borrow. - In the case of shared borrows, we return [abstract_shared_borrows], - not avalues. -*) -let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) - (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) - (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : - V.abstract_shared_borrows = - (* Sanity check - TODO: move this elsewhere (here we perform the check at every - * recursive call which is a bit overkill...) *) - let ety = Substitute.erase_regions ty in - assert (ety = v.V.ty); - (* Project *) - match (v.V.value, ty) with - | V.Concrete _, (T.Bool | T.Char | T.Integer _ | T.Str) -> [] - | V.Adt adt, T.Adt (id, region_params, tys) -> - (* Retrieve the types of the fields *) - let field_types = - Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id - region_params tys - in - (* Project over the field values *) - let fields_types = List.combine adt.V.field_values field_types in - let proj_fields = - List.map - (fun (fv, fty) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions fv - fty) - fields_types - in - List.concat proj_fields - | V.Bottom, _ -> failwith "Unreachable" - | V.Borrow bc, T.Ref (r, ref_ty, kind) -> - (* Retrieve the bid of the borrow and the asb of the projected borrowed value *) - let bid, asb = - (* Not in the set: dive *) - match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> - (* Apply the projection on the borrowed value *) - let asb = - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions bv - ref_ty - in - (bid, asb) - | V.SharedBorrow bid, T.Shared -> - (* Lookup the shared value *) - let ek = ek_all in - let sv = lookup_loan ek bid ctx in - let asb = - match sv with - | _, Concrete (V.SharedLoan (_, sv)) - | _, Abstract (V.ASharedLoan (_, sv, _)) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions - sv ref_ty - | _ -> failwith "Unexpected" - in - (bid, asb) - | V.InactivatedMutBorrow _, _ -> - failwith - "Can't apply a proj_borrow over an inactivated mutable borrow" - | _ -> failwith "Unreachable" - in - let asb = - (* Check if the region is in the set of projected regions (note that - * we never project over static regions) *) - if region_in_set r regions then - let bid' = fresh_reborrow bid in - V.AsbBorrow bid' :: asb - else asb - in - asb - | V.Loan _, _ -> failwith "Unreachable" - | V.Symbolic s, _ -> - assert (not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions)); - [ V.AsbProjReborrows (s.V.svalue, ty) ] - | _ -> failwith "Unreachable" - -(** Apply (and reduce) a projector over borrows to a value. - - - [regions]: the regions we project - - [v]: the value over which we project - - [ty]: the projection type (is used to map borrows to regions, or to - interpret the borrows as belonging to some regions...). Remember that - `v` doesn't contain region information. - For instance, if we have: - `v <: ty` where: - - `v = mut_borrow l ...` - - `ty = Ref (r, ...)` - then we interpret the borrow `l` as belonging to region `r` - - Also, when applying projections on shared values, we need to apply - reborrows. This is a bit annoying because, with the way we compute - the projection on borrows, we can't update the context immediately. - Instead, we remember the list of borrows we have to insert in the - context *afterwards*. - - [check_symbolic_no_ended] controls whether we check or not whether - symbolic values don't contain already ended regions. - This check is activated when applying projectors upon calling a function - (because we need to check that function arguments don't contain ⊥), - but deactivated when expanding symbolic values: - ``` - fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32); - - let p = f(&mut x, &mut y); // p -> @s0 - assert(x == ...); // end 'a - let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions - ``` -*) -let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) - (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) - (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : - V.typed_avalue = - (* Sanity check - TODO: move this elsewhere (here we perform the check at every - * recursive call which is a bit overkill...) *) - let ety = Substitute.erase_regions ty in - assert (ety = v.V.ty); - (* Match *) - let value : V.avalue = - match (v.V.value, ty) with - | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv - | V.Adt adt, T.Adt (id, region_params, tys) -> - (* Retrieve the types of the fields *) - let field_types = - Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id - region_params tys - in - (* Project over the field values *) - let fields_types = List.combine adt.V.field_values field_types in - let proj_fields = - List.map - (fun (fv, fty) -> - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions fv fty) - fields_types - in - V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields } - | V.Bottom, _ -> failwith "Unreachable" - | V.Borrow bc, T.Ref (r, ref_ty, kind) -> - if - (* Check if the region is in the set of projected regions (note that - * we never project over static regions) *) - region_in_set r regions - then - (* In the set *) - let bc = - match (bc, kind) with - | V.MutBorrow (bid, bv), T.Mut -> - (* Apply the projection on the borrowed value *) - let bv = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions bv ref_ty - in - V.AMutBorrow (bid, bv) - | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid - | V.InactivatedMutBorrow _, _ -> - failwith - "Can't apply a proj_borrow over an inactivated mutable borrow" - | _ -> failwith "Unreachable" - in - V.ABorrow bc - else - (* Not in the set: ignore *) - let bc = - match (bc, kind) with - | V.MutBorrow (_bid, bv), T.Mut -> - (* Apply the projection on the borrowed value *) - let bv = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions bv ref_ty - in - V.AIgnoredMutBorrow bv - | V.SharedBorrow bid, T.Shared -> - (* Lookup the shared value *) - let ek = ek_all in - let sv = lookup_loan ek bid ctx in - let asb = - match sv with - | _, Concrete (V.SharedLoan (_, sv)) - | _, Abstract (V.ASharedLoan (_, sv, _)) -> - apply_proj_borrows_on_shared_borrow ctx fresh_reborrow - regions sv ref_ty - | _ -> failwith "Unexpected" - in - V.AProjSharedBorrow asb - | V.InactivatedMutBorrow _, _ -> - failwith - "Can't apply a proj_borrow over an inactivated mutable borrow" - | _ -> failwith "Unreachable" - in - V.ABorrow bc - | V.Loan _, _ -> failwith "Unreachable" - | V.Symbolic s, _ -> - (* Check that the symbolic value doesn't contain already ended regions, - * if necessary *) - if check_symbolic_no_ended then - assert ( - not (symbolic_proj_comp_ended_regions_intersect_proj s ty regions)); - V.ASymbolic (V.AProjBorrows (s.V.svalue, ty)) - | _ -> failwith "Unreachable" - in - { V.value; V.ty } - -type symbolic_expansion = - | SeConcrete of V.constant_value - | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list) - | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp - | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp - -(** Convert a symbolic expansion *which is not a borrow* to a value *) -let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) - (see : symbolic_expansion) : V.typed_value = - let ty = Subst.erase_regions sv.V.sv_ty in - let value = - match see with - | SeConcrete cv -> V.Concrete cv - | SeAdt (variant_id, field_values) -> - let field_values = - List.map mk_typed_value_from_proj_comp field_values - in - V.Adt { V.variant_id; V.field_values } - | SeMutRef (_, _) | SeSharedRef (_, _) -> - failwith "Unexpected symbolic reference expansion" - in - { V.value; V.ty } - -(** Convert a symbolic expansion to a value. - - If the expansion is a mutable reference expansion, it converts it to a borrow. - This function is meant to be used when reducing projectors over borrows, - during a symbolic expansion. - *) -let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) - (see : symbolic_expansion) : V.typed_value = - match see with - | SeMutRef (bid, bv) -> - let ty = Subst.erase_regions sv.V.sv_ty in - let bv = mk_typed_value_from_proj_comp bv in - let value = V.Borrow (V.MutBorrow (bid, bv)) in - { V.value; ty } - | SeSharedRef (_, _) -> - failwith "Unexpected symbolic shared reference expansion" - | _ -> symbolic_expansion_non_borrow_to_value sv see - -(** Apply (and reduce) a projector over loans to a value. - - TODO: detailed comments. See [apply_proj_borrows] -*) -let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) - (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue = - (* Match *) - let (value, ty) : V.avalue * T.rty = - match (see, original_sv_ty) with - | SeConcrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> - (V.AConcrete cv, original_sv_ty) - | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) -> - (* Project over the field values *) - let field_values = - List.map mk_aproj_loans_from_proj_comp field_values - in - (V.AAdt { V.variant_id; field_values }, original_sv_ty) - | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) -> - (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_proj_comp spc in - (* Check if the region is in the set of projected regions (note that - * we never project over static regions) *) - if region_in_set r regions then - (* In the set: keep *) - (V.ALoan (V.AMutLoan (bid, child_av)), ref_ty) - else - (* Not in the set: ignore *) - (V.ALoan (V.AIgnoredMutLoan (bid, child_av)), ref_ty) - | SeSharedRef (bids, spc), T.Ref (r, ref_ty, T.Shared) -> - (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_proj_comp spc in - (* Check if the region is in the set of projected regions (note that - * we never project over static regions) *) - if region_in_set r regions then - (* In the set: keep *) - let shared_value = mk_typed_value_from_proj_comp spc in - (V.ALoan (V.ASharedLoan (bids, shared_value, child_av)), ref_ty) - else - (* Not in the set: ignore *) - (V.ALoan (V.AIgnoredSharedLoan child_av), ref_ty) - | _ -> failwith "Unreachable" - in - { V.value; V.ty } - -(** Auxiliary function to end borrows: lookup a borrow in the environment, - update it (by returning an updated environment where the borrow has been - replaced by [Bottom])) if we can end the borrow (for instance, it is not - an outer borrow...) or return the reason why we couldn't update the borrow. - - [end_borrow] then simply performs a loop: as long as we need to end (outer) - borrows, we end them, before finally ending the borrow we wanted to end in the - first place. - - Note that it is possible to end a borrow in an abstraction, without ending - the whole abstraction, if the corresponding loan is inside the abstraction - as well. The [allowed_abs] parameter controls whether we allow to end borrows - in an abstraction or not, and in which abstraction. -*) -let end_borrow_get_borrow (io : inner_outer) - (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) - (ctx : C.eval_ctx) : - (C.eval_ctx * g_borrow_content option, outer_borrows_or_abs) result = - (* We use a reference to communicate the kind of borrow we found, if we - * find one *) - let replaced_bc : g_borrow_content option ref = ref None in - let set_replaced_bc (bc : g_borrow_content) = - assert (Option.is_none !replaced_bc); - replaced_bc := Some bc - in - (* Raise an exception if there are outer borrows or if we are inside an - * abstraction: this exception is caught in a wrapper function *) - let raise_if_outer (outer : V.AbstractionId.id option * borrow_ids option) = - let outer_abs, outer_borrows = outer in - match outer_abs with - | Some abs -> ( - if - (* Check if we can end borrows inside this abstraction *) - Some abs <> allowed_abs - then raise (FoundOuter (OuterAbs abs)) - else - match outer_borrows with - | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) - | None -> ()) - | None -> ( - match outer_borrows with - | Some borrows -> raise (FoundOuter (OuterBorrows borrows)) - | None -> ()) - in - - (* The environment is used to keep track of the outer loans *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option) - lc = - match lc with - | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer bid) - | V.SharedLoan (bids, v) -> - (* Update the outer borrows before diving into the shared value *) - let outer = update_outer_borrows io outer (Borrows bids) in - V.Loan (super#visit_SharedLoan outer bids v) - (** We reimplement [visit_Loan] because we may have to update the - outer borrows *) - - method! visit_Borrow outer bc = - match bc with - | SharedBorrow l' | InactivatedMutBorrow l' -> - (* Check if this is the borrow we are looking for *) - if l = l' then ( - (* Check if there are outer borrows or if we are inside an abstraction *) - raise_if_outer outer; - (* Register the update *) - set_replaced_bc (Concrete bc); - (* Update the value *) - V.Bottom) - else super#visit_Borrow outer bc - | V.MutBorrow (l', bv) -> - (* Check if this is the borrow we are looking for *) - if l = l' then ( - (* Check if there are outer borrows or if we are inside an abstraction *) - raise_if_outer outer; - (* Register the update *) - set_replaced_bc (Concrete bc); - (* Update the value *) - V.Bottom) - else - (* Update the outer borrows before diving into the borrowed value *) - let outer = update_outer_borrows io outer (Borrow l') in - V.Borrow (super#visit_MutBorrow outer l' bv) - - method! visit_ALoan outer lc = - (* Note that the children avalues are just other, independent loans, - * so we don't need to update the outer borrows when diving in. - * We keep track of the parents/children relationship only because we - * need it to properly instantiate the backward functions when generating - * the pure translation. *) - match lc with - | V.AMutLoan (bid, av) -> - (* Nothing special to do *) - V.ALoan (super#visit_AMutLoan outer bid av) - | V.ASharedLoan (bids, v, av) -> - (* Explore the shared value - we need to update the outer borrows *) - let souter = update_outer_borrows io outer (Borrows bids) in - let v = super#visit_typed_value souter v in - (* Explore the child avalue - we keep the same outer borrows *) - let av = super#visit_typed_avalue outer av in - (* Reconstruct *) - V.ALoan (V.ASharedLoan (bids, v, av)) - | V.AEndedMutLoan { given_back; child } -> - (* The loan has ended, so no need to update the outer borrows *) - V.ALoan (super#visit_AEndedMutLoan outer given_back child) - | V.AEndedSharedLoan (v, av) -> - (* The loan has ended, so no need to update the outer borrows *) - V.ALoan (super#visit_AEndedSharedLoan outer v av) - | V.AIgnoredMutLoan (bid, av) -> - (* Nothing special to do *) - V.ALoan (super#visit_AIgnoredMutLoan outer bid av) - | V.AEndedIgnoredMutLoan { given_back; child } -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedIgnoredMutLoan outer given_back child) - | V.AIgnoredSharedLoan av -> - (* Nothing special to do *) - V.ALoan (super#visit_AIgnoredSharedLoan outer av) - (** We reimplement [visit_ALoan] because we may have to update the - outer borrows *) - - method! visit_ABorrow outer bc = - match bc with - | V.AMutBorrow (bid, av) -> - (* Check if this is the borrow we are looking for *) - if bid = l then ( - (* When ending a mut borrow, there are two cases: - * - in the general case, we have to end the whole abstraction - * (and thus raise an exception to signal that to the caller) - * - in some situations, the associated loan is inside the same - * abstraction as the borrow. In this situation, we can end - * the borrow without ending the whole abstraction, and we - * simply move the child avalue around. - *) - (* Check there are outer borrows, or if we need to end the whole - * abstraction *) - raise_if_outer outer; - (* Register the update *) - set_replaced_bc (Abstract bc); - (* Update the value - note that we are necessarily in the second - * of the two cases described above *) - V.ABottom) - else - (* Update the outer borrows before diving into the child avalue *) - let outer = update_outer_borrows io outer (Borrow bid) in - V.ABorrow (super#visit_AMutBorrow outer bid av) - | V.ASharedBorrow bid -> - (* Check if this is the borrow we are looking for *) - if bid = l then ( - (* Check there are outer borrows, or if we need to end the whole - * abstraction *) - raise_if_outer outer; - (* Register the update *) - set_replaced_bc (Abstract bc); - (* Update the value - note that we are necessarily in the second - * of the two cases described above *) - V.ABottom) - else V.ABorrow (super#visit_ASharedBorrow outer bid) - | V.AIgnoredMutBorrow av -> - (* Nothing special to do *) - V.ABorrow (super#visit_AIgnoredMutBorrow outer av) - | V.AProjSharedBorrow asb -> - (* Check if the borrow we are looking for is in the asb *) - if borrow_in_asb l asb then ( - (* Check there are outer borrows, or if we need to end the whole - * abstraction *) - raise_if_outer outer; - (* Register the update *) - set_replaced_bc (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 - V.ABorrow (V.AProjSharedBorrow asb)) - else - (* Nothing special to do *) - V.ABorrow (super#visit_AProjSharedBorrow outer asb) - - 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); - let outer = (Some abs.V.abs_id, None) in - super#visit_abs outer abs - end - in - (* Catch the exceptions - raised if there are outer borrows *) - try - let ctx = obj#visit_eval_ctx (None, None) ctx in - Ok (ctx, !replaced_bc) - with FoundOuter outers -> Error outers - -(** Auxiliary function. See [give_back_value]. - - Apply reborrows to a context. - - The [reborrows] input is a list of pairs (shared loan id, id to insert in the shared loan). -*) -let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) - (ctx : C.eval_ctx) : C.eval_ctx = - (* This is a bit brutal, but whenever we insert a reborrow, we remove - * it from the list. This allows us to check that all the reborrows were - * applied before returning. - * We might reimplement that in a more efficient manner by using maps. *) - let reborrows = ref reborrows in - - (* Check if a value is a mutable borrow, and return its identifier if - it is the case *) - let get_borrow_in_mut_borrow (v : V.typed_value) : V.BorrowId.id option = - match v.V.value with - | V.Borrow lc -> ( - match lc with - | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None - | V.MutBorrow (id, _) -> Some id) - | _ -> None - in - - (* Add the proper reborrows to a set of borrow ids (for a shared loan) *) - let insert_reborrows bids = - (* Find the reborrows to apply *) - let insert, reborrows' = - List.partition (fun (bid, _) -> V.BorrowId.Set.mem bid bids) !reborrows - in - reborrows := reborrows'; - let insert = List.map snd insert in - (* Insert the borrows *) - List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert - in - - (* Get the list of reborrows for a given borrow id *) - let get_reborrows_for_bid bid = - (* Find the reborrows to apply *) - let insert, reborrows' = - List.partition (fun (bid', _) -> bid' = bid) !reborrows - in - reborrows := reborrows'; - List.map snd insert - in - - let borrows_to_set bids = - List.fold_left - (fun bids bid -> V.BorrowId.Set.add bid bids) - V.BorrowId.Set.empty bids - in - - (* Insert reborrows for a given borrow id into a given set of borrows *) - let insert_reborrows_for_bid bids bid = - (* Find the reborrows to apply *) - let insert = get_reborrows_for_bid bid in - (* Insert the borrows *) - List.fold_left (fun bids bid -> V.BorrowId.Set.add bid bids) bids insert - in - - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_typed_value env v = - match v.V.value with - | V.Borrow (V.MutBorrow (bid, bv)) -> - let insert = get_reborrows_for_bid bid in - let nbc = super#visit_MutBorrow env bid bv in - let nbc = { v with V.value = V.Borrow nbc } in - if insert = [] then (* No reborrows: do nothing special *) - nbc - else - (* There are reborrows: insert a shared loan *) - let insert = borrows_to_set insert in - let value = V.Loan (V.SharedLoan (insert, nbc)) in - let ty = v.V.ty in - { V.value; ty } - | _ -> super#visit_typed_value env v - (** We may need to reborrow mutable borrows. Note that this doesn't - happen for aborrows *) - - method! visit_loan_content env lc = - match lc with - | V.SharedLoan (bids, sv) -> - (* Insert the reborrows *) - let bids = insert_reborrows bids in - (* Check if the contained value is a mutable borrow, in which - * case we might need to reborrow it by adding more borrow ids - * to the current set of borrows - by doing this small - * manipulation here, we accumulate the borrow ids in the same - * shared loan, right above the mutable borrow, and avoid - * stacking shared loans (note that doing this is not a problem - * from a soundness point of view, but it is a bit ugly...) *) - let bids = - match get_borrow_in_mut_borrow sv with - | None -> bids - | Some bid -> insert_reborrows_for_bid bids bid - in - (* Update and explore *) - super#visit_SharedLoan env bids sv - | V.MutLoan bid -> - (* Nothing special to do *) - super#visit_MutLoan env bid - (** We reimplement [visit_loan_content] (rather than one of the sub- - functions) on purpose: exhaustive matches are good for maintenance *) - - method! visit_aloan_content env lc = - (* TODO: ashared_loan (amut_loan ) case *) - match lc with - | V.ASharedLoan (bids, v, av) -> - (* Insert the reborrows *) - let bids = insert_reborrows bids in - (* Update and explore *) - super#visit_ASharedLoan env bids v av - | V.AIgnoredSharedLoan _ - | V.AMutLoan (_, _) - | V.AEndedMutLoan { given_back = _; child = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan { given_back = _; child = _ } -> - (* Nothing particular to do *) - super#visit_aloan_content env lc - end - in - - (* Visit *) - let ctx = obj#visit_eval_ctx () ctx in - (* Check that there are no reborrows remaining *) - assert (!reborrows = []); - (* Return *) - ctx - -(** Auxiliary function to prepare reborrowing operations (used when - applying projectors). - - Returns two functions: - - a function to generate fresh re-borrow ids, and register the reborrows - - a function to apply the reborrows in a context - Those functions are of course stateful. - *) -let prepare_reborrows (config : C.config) (allow_reborrows : bool) - (ctx : C.eval_ctx) : - (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) = - let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in - let borrow_counter = ref ctx.C.borrow_counter in - (* The function to generate and register fresh reborrows *) - let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id = - if allow_reborrows then ( - let bid', cnt' = V.BorrowId.fresh !borrow_counter in - borrow_counter := cnt'; - reborrows := (bid, bid') :: !reborrows; - bid') - else failwith "Unexpected reborrow" - in - (* The function to apply the reborrows in a context *) - let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx = - match config.C.mode with - | C.ConcreteMode -> - (* Reborrows are introduced when applying projections in symbolic mode *) - assert (!borrow_counter = ctx.C.borrow_counter); - assert (!reborrows = []); - ctx - | C.SymbolicMode -> - (* Update the borrow counter *) - let ctx = { ctx with C.borrow_counter = !borrow_counter } in - (* Apply the reborrows *) - apply_reborrows !reborrows ctx - in - (fresh_reborrow, apply_registered_reborrows) - -(** Auxiliary function to end borrows. See [give_back]. - - When we end a mutable borrow, we need to "give back" the value it contained - to its original owner by reinserting it at the proper position. - - Note that this function checks that there is exactly one loan to which we - give the value back. - TODO: this was not the case before, so some sanity checks are not useful anymore. - *) -let give_back_value (config : C.config) (bid : V.BorrowId.id) - (nv : V.typed_value) (ctx : C.eval_ctx) : C.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); - replaced := true - in - (* Whenever giving back symbolic values, they shouldn't contain already ended regions *) - let check_symbolic_no_ended = true in - (* 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 ctx - in - (* The visitor to give back the values *) - let obj = - object (self) - inherit [_] C.map_eval_ctx as super - - method! visit_Loan opt_abs lc = - match lc with - | V.SharedLoan (bids, v) -> - (* We are giving back a value (i.e., the content of a *mutable* - * borrow): nothing special to do *) - V.Loan (super#visit_SharedLoan opt_abs bids v) - | V.MutLoan bid' -> - (* Check if this is the loan we are looking for *) - if bid' = bid then ( - set_replaced (); - nv.V.value) - else V.Loan (super#visit_MutLoan opt_abs bid') - - method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue - = - match av.V.value with - | V.ALoan lc -> - let value = self#visit_typed_ALoan opt_abs av.V.ty lc in - ({ av with V.value } : V.typed_avalue) - | _ -> super#visit_typed_avalue opt_abs av - (** This is a bit annoying, but as we need the type of the avalue we - are exploring, in order to be able to project the value we give - back, we need to reimplement [visit_typed_avalue] instead of - [visit_ALoan] *) - - method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty) - (lc : V.aloan_content) : V.avalue = - (* Preparing a bit *) - let regions = - match opt_abs with - | None -> failwith "Unreachable" - | Some abs -> abs.V.regions - in - match lc with - | V.AMutLoan (bid', child) -> - if bid' = bid then ( - (* 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 *) - (* Register the insertion *) - set_replaced (); - (* Apply the projection *) - let given_back = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions nv ty - in - (* Return the new value *) - V.ALoan (V.AEndedMutLoan { given_back; child })) - else - (* Continue exploring *) - V.ALoan (super#visit_AMutLoan opt_abs bid' child) - | V.ASharedLoan (bids, v, av) -> - (* We are giving back a value to a *mutable* loan: nothing special to do *) - V.ALoan (super#visit_ASharedLoan opt_abs bids v av) - | V.AEndedMutLoan { given_back; child } -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child) - | V.AEndedSharedLoan (v, av) -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedSharedLoan opt_abs v av) - | V.AIgnoredMutLoan (bid', child) -> - (* This loan is ignored, but we may have to project on a subvalue - * of the value which is given back *) - if bid' = bid then - (* Note that we replace the ignored mut loan by an *ended* ignored - * mut loan. Also, this is not the loan we are looking for *per se*: - * we don't register the fact that we inserted the value somewhere - * (i.e., we don't call [set_replaced]) *) - let given_back = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - regions nv ty - in - V.ALoan (V.AEndedIgnoredMutLoan { given_back; child }) - else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child) - | V.AEndedIgnoredMutLoan { given_back; child } -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child) - | V.AIgnoredSharedLoan av -> - (* Nothing special to do *) - V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av) - (** We are not specializing an already existing method, but adding a - new method (for projections, we need type information) *) - - method! visit_Abs opt_abs abs = - (* 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); - super#visit_Abs (Some abs) abs - end - in - - (* Explore the environment *) - let ctx = obj#visit_eval_ctx None ctx in - (* Check we gave back to exactly one loan *) - assert !replaced; - (* Apply the reborrows *) - apply_registered_reborrows ctx - -(** Auxiliary function to end borrows. See [give_back]. - - This function is similar to [give_back_value] but gives back an [avalue] - (coming from an abstraction). - - It is used when ending a borrow inside an abstraction, when the corresponding - loan is inside the same abstraction (in which case we don't need to end the whole - abstraction). - - REMARK: this function can't be used to give back the values borrowed by - end abstraction when ending this abstraction. When doing this, we need - to convert the [avalue] to a [value] by introducing the proper symbolic values. - *) -let give_back_avalue (_config : C.config) (bid : V.BorrowId.id) - (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.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); - replaced := true - in - let obj = - object (self) - inherit [_] C.map_eval_ctx as super - - method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue - = - match av.V.value with - | V.ALoan lc -> - let value = self#visit_typed_ALoan opt_abs av.V.ty lc in - ({ av with V.value } : V.typed_avalue) - | _ -> super#visit_typed_avalue opt_abs av - (** This is a bit annoying, but as we need the type of the avalue we - are exploring, in order to be able to project the value we give - back, we need to reimplement [visit_typed_avalue] instead of - [visit_ALoan] *) - - method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty) - (lc : V.aloan_content) : V.avalue = - match lc with - | V.AMutLoan (bid', child) -> - if bid' = bid then ( - (* 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 *) - (* Register the insertion *) - set_replaced (); - (* Sanity check *) - assert (nv.V.ty = ty); - (* Return the new value *) - V.ALoan (V.AEndedMutLoan { given_back = nv; child })) - else - (* Continue exploring *) - V.ALoan (super#visit_AMutLoan opt_abs bid' child) - | V.ASharedLoan (bids, v, av) -> - (* We are giving back a value to a *mutable* loan: nothing special to do *) - V.ALoan (super#visit_ASharedLoan opt_abs bids v av) - | V.AEndedMutLoan { given_back; child } -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child) - | V.AEndedSharedLoan (v, av) -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedSharedLoan opt_abs v av) - | V.AIgnoredMutLoan (bid', child) -> - (* This loan is ignored, but we may have to project on a subvalue - * of the value which is given back *) - if bid' = bid then ( - (* Note that we replace the ignored mut loan by an *ended* ignored - * mut loan. Also, this is not the loan we are looking for *per se*: - * we don't register the fact that we inserted the value somewhere - * (i.e., we don't call [set_replaced]) *) - (* Sanity check *) - assert (nv.V.ty = ty); - V.ALoan (V.AEndedIgnoredMutLoan { given_back = nv; child })) - else V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid' child) - | V.AEndedIgnoredMutLoan { given_back; child } -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child) - | V.AIgnoredSharedLoan av -> - (* Nothing special to do *) - V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av) - (** We are not specializing an already existing method, but adding a - new method (for projections, we need type information) *) - end - in - - (* Explore the environment *) - let ctx = obj#visit_eval_ctx None ctx in - (* Check we gave back to exactly one loan *) - assert !replaced; - (* Return *) - ctx - -(** Auxiliary function to end borrows. See [give_back]. - - When we end a shared borrow, we need to remove the borrow id from the list - of borrows to the shared value. - - Note that this function checks that there is exactly one shared loan that - we update. - TODO: this was not the case before, so some sanity checks are not useful anymore. - *) -let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) : - C.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); - replaced := true - in - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Loan opt_abs lc = - match lc with - | V.SharedLoan (bids, shared_value) -> - if V.BorrowId.Set.mem bid bids then ( - (* This is the loan we are looking for *) - set_replaced (); - (* If there remains exactly one borrow identifier, we need - * to end the loan. Otherwise, we just remove the current - * loan identifier *) - if V.BorrowId.Set.cardinal bids = 1 then shared_value.V.value - else - V.Loan - (V.SharedLoan (V.BorrowId.Set.remove bid bids, shared_value))) - else - (* Not the loan we are looking for: continue exploring *) - V.Loan (super#visit_SharedLoan opt_abs bids shared_value) - | V.MutLoan bid' -> - (* We are giving back a *shared* borrow: nothing special to do *) - V.Loan (super#visit_MutLoan opt_abs bid') - - method! visit_ALoan opt_abs lc = - match lc with - | V.AMutLoan (bid, av) -> - (* Nothing special to do (we are giving back a *shared* borrow) *) - V.ALoan (super#visit_AMutLoan opt_abs bid av) - | V.ASharedLoan (bids, shared_value, child) -> - if V.BorrowId.Set.mem bid bids then ( - (* This is the loan we are looking for *) - set_replaced (); - (* If there remains exactly one borrow identifier, we need - * to end the loan. Otherwise, we just remove the current - * loan identifier *) - if V.BorrowId.Set.cardinal bids = 1 then - V.ALoan (V.AEndedSharedLoan (shared_value, child)) - else - V.ALoan - (V.ASharedLoan - (V.BorrowId.Set.remove bid bids, shared_value, child))) - else - (* Not the loan we are looking for: continue exploring *) - V.ALoan (super#visit_ASharedLoan opt_abs bids shared_value child) - | V.AEndedMutLoan { given_back; child } -> - (* Nothing special to do (the loan has ended) *) - V.ALoan (super#visit_AEndedMutLoan opt_abs given_back child) - | V.AEndedSharedLoan (v, av) -> - (* Nothing special to do (the loan has ended) *) - V.ALoan (super#visit_AEndedSharedLoan opt_abs v av) - | V.AIgnoredMutLoan (bid, av) -> - (* Nothing special to do (we are giving back a *shared* borrow) *) - V.ALoan (super#visit_AIgnoredMutLoan opt_abs bid av) - | V.AEndedIgnoredMutLoan { given_back; child } -> - (* Nothing special to do *) - V.ALoan (super#visit_AEndedIgnoredMutLoan opt_abs given_back child) - | V.AIgnoredSharedLoan av -> - (* Nothing special to do *) - V.ALoan (super#visit_AIgnoredSharedLoan opt_abs av) - end - in - - (* Explore the environment *) - let ctx = obj#visit_eval_ctx None ctx in - (* Check we gave back to exactly one loan *) - assert !replaced; - (* Return *) - ctx - -(** When copying values, we duplicate the shared borrows. This is tantamount - to reborrowing the shared value. The following function applies this change - 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 : V.BorrowId.id) (new_bid : V.BorrowId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Keep track of changes *) - let r = ref false in - let set_ref () = - assert (not !r); - r := true - in - - let obj = - object - inherit [_] C.map_env as super - - method! visit_SharedLoan env bids sv = - (* Shared loan: check if the borrow id we are looking for is in the - set of borrow ids. If yes, insert the new borrow id, otherwise - explore inside the shared value *) - if V.BorrowId.Set.mem original_bid bids then ( - set_ref (); - let bids' = V.BorrowId.Set.add new_bid bids in - V.SharedLoan (bids', sv)) - else super#visit_SharedLoan env bids sv - - method! visit_ASharedLoan env bids v av = - (* This case is similar to the [SharedLoan] case *) - if V.BorrowId.Set.mem original_bid bids then ( - set_ref (); - let bids' = V.BorrowId.Set.add new_bid bids in - V.ASharedLoan (bids', v, av)) - else super#visit_ASharedLoan env bids v av - end - in - - let env = obj#visit_env () ctx.env in - (* Check that we reborrowed once *) - assert !r; - { ctx with env } - -(** Auxiliary function: see [end_borrow_in_env] *) -let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) - (ctx : C.eval_ctx) : C.eval_ctx = - (* This is used for sanity checks *) - let sanity_ek = - { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } - in - match bc with - | Concrete (V.MutBorrow (l', tv)) -> - (* Sanity check *) - assert (l' = l); - (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); - (* Update the context *) - give_back_value config l tv ctx - | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') -> - (* Sanity check *) - assert (l' = l); - (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); - (* Update the context *) - give_back_shared config l ctx - | Abstract (V.AMutBorrow (l', av)) -> - (* Sanity check *) - assert (l' = l); - (* Check that the corresponding loan is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); - (* Update the context *) - give_back_avalue config l av ctx - | Abstract (V.ASharedBorrow l') -> - (* Sanity check *) - assert (l' = l); - (* Check that the borrow is somewhere - purely a sanity check *) - assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); - (* Update the context *) - give_back_shared config l ctx - | Abstract (V.AProjSharedBorrow asb) -> - (* Sanity check *) - assert (borrow_in_asb l asb); - (* Update the context *) - give_back_shared config l ctx - | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable" - -(** Convert an [avalue] to a [value]. - - This function is used when ending abstractions: whenever we end a borrow - in an abstraction, we converted the borrowed [avalue] to a [value], then give - back this [value] to the context. - - There are two possibilities: - - either the borrowed [avalue] contains ended regions, in which case we return ⊥ - - or it doesn't contain ⊥, in which case we simply return a newly introduced - symbolic value. - We return a new context because we may have to introduce a symbolic value. - - The `ended_regions` parameter is for the regions contained in the current - abstraction. - *) -let convert_avalue_to_value (ended_regions : T.RegionId.set_t) - (av : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - (* Convert the type *) - let ty = Subst.erase_regions av.V.ty in - (* Check if the avalue contains ended regions *) - if rty_regions_intersect av.V.ty ended_regions then - (* Contains ended regions: return ⊥ *) - (ctx, { V.value = V.Bottom; V.ty }) - else - (* Doesn't contain ended regions: return a symbolic value *) - let ctx, sv_id = C.fresh_symbolic_value_id ctx in - let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in - let value : V.symbolic_proj_comp = - (* Note that the set of ended regions is empty: we shouldn't have to take - * into account any ended regions at this point, otherwise we would be in - * the first case where we should return ⊥ *) - { V.svalue; V.rset_ended = T.RegionId.Set.empty } - in - let value = V.Symbolic value in - (ctx, { V.value; V.ty }) - -(** End a borrow identified by its borrow id in a context - - First lookup the borrow in the context and replace it with [Bottom]. - Then, check that there is an associated loan in the context. When moving - values, before putting the value in its destination, we get an - intermediate state where some values are "outside" the context and thus - inaccessible. As [give_back_value] just performs a map for instance (TODO: - not the case anymore), we need to check independently that there is indeed a - loan ready to receive the value we give back (note that we also have other - invariants like: there is exacly one mutable loan associated to a mutable - borrow, etc. but they are more easily maintained). - Note that in theory, we shouldn't never reach a problematic state as the - one we describe above, because when we move a value we need to end all the - loans inside before moving it. Still, it is a very useful sanity check. - Finally, give the values back. - - Of course, we end outer borrows before updating the target borrow if it - proves necessary: this is controled by the [io] parameter. If it is [Inner], - we allow ending inner borrows (without ending the outer borrows first), - otherwise we only allow ending outer borrows. - If a borrow is inside an abstraction, we need to end the whole abstraction, - at the exception of the case where the loan corresponding to the borrow is - inside the same abstraction. We control this with the [allowed_abs] parameter: - if it is not `None`, we allow ending a borrow if it is inside the given - abstraction. In practice, if the value is `Some abs_id`, we should have - checked that the corresponding loan is inside the abstraction given by - `abs_id` before. In practice, only [end_borrow] should call itself - with `allowed_abs = Some ...`, all the other calls should use `allowed_abs = None`: - if you look ath the implementation details, `end_borrow` performs - all tne necessary checks in case a borrow is inside an abstraction. - *) -let rec end_borrow (config : C.config) (io : inner_outer) - (allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - match end_borrow_get_borrow io allowed_abs l ctx with - (* Two cases: - * - error: we found outer borrows (end them first) - * - success: we didn't find outer borrows when updating (but maybe we actually - didn't find the borrow we were looking for...) +module Test = struct + let initialize_context (type_context : C.type_context) + (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx = + C.reset_global_counters (); + { + C.type_context; + C.fun_context = fun_defs; + C.type_vars; + C.env = []; + C.ended_regions = T.RegionId.Set.empty; + } + + (** Initialize an evaluation context to execute a function. + + Introduces local variables initialized in the following manner: + - input arguments are initialized as symbolic values + - the remaining locals are initialized as ⊥ + "Dummy" abstractions are introduced for the regions present in the + function signature. *) - | Error outer -> ( - (* End the outer borrows, abstraction, then try again to end the target - * borrow (if necessary) *) - match outer with - | OuterBorrows (Borrows bids) -> - (* Note that when ending outer borrows, we use io=Outer. However, - * we shouldn't need to end outer borrows if io=Inner, so we just - * add the following assertion *) - assert (io = Outer); - (* Note that we might get there with `allowed_abs <> None`: we might - * be trying to end a borrow inside an abstraction, but which is actually - * inside another borrow *) - let allowed_abs' = None in - let ctx = end_borrows config io allowed_abs' bids ctx in - (* Retry to end the borrow *) - end_borrow config io allowed_abs l ctx - | OuterBorrows (Borrow bid) -> - (* See the comments for the previous case *) - assert (io = Outer); - let allowed_abs' = None in - let ctx = end_borrow config io allowed_abs' bid ctx in - (* Retry to end the borrow *) - end_borrow config io allowed_abs l ctx - | OuterAbs abs_id -> ( - (* The borrow is inside an asbtraction: check if the corresponding - * loan is inside the same abstraction. If this is the case, we end - * the borrow without ending the abstraction. If not, we need to - * end the whole abstraction *) - (* Note that we can lookup the loan anywhere *) - let ek = - { - enter_shared_loans = true; - enter_mut_borrows = true; - enter_abs = true; - } - in - match lookup_loan ek l ctx with - | AbsId loan_abs_id, _ -> - if loan_abs_id = abs_id then ( - (* Same abstraction! We can end the borrow *) - let ctx = end_borrow config io (Some abs_id) l ctx in - (* Sanity check *) - assert (Option.is_none (lookup_borrow_opt ek l ctx)); - ctx) - else - (* Not the same abstraction: we need to end the whole abstraction. - * By doing that we should have ended the target borrow (see the - * below sanity check) *) - let ctx = end_abstraction config abs_id ctx in - (* Sanity check: we ended the target borrow *) - assert (Option.is_none (lookup_borrow_opt ek l ctx)); - ctx - | VarId _, _ -> - (* The loan is not inside the same abstraction (actually inside - * a non-abstraction value): we need to end the whole abstraction *) - let ctx = end_abstraction config abs_id ctx in - (* Sanity check: we ended the target borrow *) - assert (Option.is_none (lookup_borrow_opt ek l ctx)); - ctx)) - | Ok (ctx, None) -> - (* 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); - ctx - (* We found a borrow: give the value back (i.e., update the corresponding loan) *) - | Ok (ctx, Some bc) -> give_back config l bc ctx - -and end_borrows (config : C.config) (io : inner_outer) - (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) - (ctx : C.eval_ctx) : C.eval_ctx = - V.BorrowId.Set.fold - (fun id ctx -> end_borrow config io allowed_abs id ctx) - lset ctx - -and end_abstraction (config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Lookup the abstraction *) - let abs = C.ctx_lookup_abs ctx abs_id in - (* End the parent abstractions first *) - let ctx = end_abstractions config abs.parents ctx in - (* End the loans inside the abstraction *) - let ctx = end_abstraction_loans config abs_id ctx in - (* End the abstraction itself by redistributing the borrows it contains *) - let ctx = end_abstraction_borrows config abs_id ctx in - (* End the regions owned by the abstraction *) - let ctx = end_abstraction_regions config abs_id ctx in - (* Remove all the references to the id of the current abstraction, and remove - * the abstraction itself *) - end_abstraction_remove_from_context config abs_id ctx - -and end_abstractions (config : C.config) (abs_ids : V.AbstractionId.set_t) - (ctx : C.eval_ctx) : C.eval_ctx = - V.AbstractionId.Set.fold - (fun id ctx -> end_abstraction config id ctx) - abs_ids ctx - -and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Lookup the abstraction *) - let abs = C.ctx_lookup_abs ctx abs_id in - (* End the first loan we find *) - let obj = - object - inherit [_] V.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 } -> - super#visit_AEndedMutLoan env given_back child - | V.AEndedSharedLoan (v, av) -> super#visit_AEndedSharedLoan env v av - | V.AIgnoredMutLoan (bid, av) -> - (* Note that this loan can't come from a parent abstraction, because - * we should have ended them already) *) - super#visit_AIgnoredMutLoan env bid av - | V.AEndedIgnoredMutLoan { given_back; child } -> - super#visit_AEndedIgnoredMutLoan env given_back child - | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av - end - in - try - (* Check if there are loans *) - obj#visit_abs () abs; - (* No loans: nothing to update *) - ctx - with (* There are loans: end them, then recheck *) - | FoundBorrowIds bids -> - let ctx = - match bids with - | Borrow bid -> end_outer_borrow config bid ctx - | Borrows bids -> end_outer_borrows config bids ctx - in - (* Recheck *) - end_abstraction_loans config abs_id ctx - -and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Note that the abstraction mustn't contain any loans *) - (* We end the borrows, starting with the *inner* ones. This is important - when considering nested borrows which have the same lifetime. - - For instance: - ``` - x -> mut_loan l1 - px -> mut_loan l0 - abs0 { a_mut_borrow l0 (a_mut_borrow l1 (U32 3)) } - ``` - - becomes (`U32 3` doesn't contain ⊥, so we give back a symbolic value): - ``` - x -> @s0 - px -> mut_loan l0 - abs0 { a_mut_borrow l0 ⊥ } - ``` - - then (the borrowed value contains ⊥, we give back ⊥): - ``` - x -> @s0 - px -> ⊥ - abs0 { ⊥ } - ``` - *) - (* We explore in-depth and use exceptions. When exploring a borrow, if - * the exploration didn't trigger an exception, it means there are no - * inner borrows to end: we can thus trigger an exception for the current - * borrow. *) - let obj = - object - inherit [_] V.iter_abs as super - - method! visit_aborrow_content env bc = - (* In-depth exploration *) - super#visit_aborrow_content env bc; - (* No exception was raise: we can raise an exception for the - * current borrow *) - match bc with - | V.AMutBorrow (_, _) | V.ASharedBorrow _ -> - (* Raise an exception *) - raise (FoundABorrowContent bc) - | V.AProjSharedBorrow asb -> - (* Raise an exception only if the asb contains borrows *) - if - List.exists - (fun x -> match x with V.AsbBorrow _ -> true | _ -> false) - asb - then raise (FoundABorrowContent bc) - else () - | V.AIgnoredMutBorrow _ -> - (* Nothing to do for ignored borrows *) - () - end - in - (* Lookup the abstraction *) - let abs = C.ctx_lookup_abs ctx abs_id in - try - (* Explore the abstraction, looking for borrows *) - obj#visit_abs () abs; - (* No borrows: nothing to update *) - ctx - with - (* There are borrows: end them, then reexplore *) - | FoundABorrowContent bc -> - (* First, replace the borrow by ⊥ *) - let bid = - match bc with - | V.AMutBorrow (bid, _) | V.ASharedBorrow bid -> bid - | V.AProjSharedBorrow asb -> ( - (* There should be at least one borrow identifier in the set, which we - * can use to identify the whole set *) - match - List.find - (fun x -> match x with V.AsbBorrow _ -> true | _ -> false) - asb - with - | V.AsbBorrow bid -> bid - | _ -> failwith "Unexpected") - | V.AIgnoredMutBorrow _ -> failwith "Unexpected" + let initialize_symbolic_context_for_fun (type_context : C.type_context) + (fun_defs : A.fun_def list) (fdef : A.fun_def) : C.eval_ctx = + (* The abstractions are not initialized the same way as for function + * calls: they contain *loan* projectors, because they "provide" us + * with the input values (which behave as if they had been returned + * by some function calls...). + * Also, note that we properly set the set of parents of every abstraction: + * this should not be necessary, as those abstractions should never be + * *automatically* ended (because ending some borrows requires to end + * one of them), but rather selectively ended when generating code + * for each of the backward functions. We do it only because we can + * do it, and because it gives a bit of sanity. + * *) + let sg = fdef.signature in + (* Create the context *) + let ctx = initialize_context type_context fun_defs sg.type_params in + (* Instantiate the signature *) + let type_params = + List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in - let ctx = update_aborrow ek_all bid V.ABottom ctx in - (* Then give back the value *) - let ctx = - match bc with - | V.AMutBorrow (bid, av) -> - (* First, convert the avalue to a value (by introducing the proper - * symbolic values). Note that we should probably use the regions owned - * by the abstraction for the ended_regions parameter, but for safety - * I'm using the accumulated regions (which include the ancestors' - * regions). Think a bit about that... *) - let ctx, v = convert_avalue_to_value abs.acc_regions av ctx in - give_back_value config bid v ctx - | V.ASharedBorrow bid -> give_back_shared config bid ctx - | V.AProjSharedBorrow _ -> - (* Nothing to do *) - ctx - | V.AIgnoredMutBorrow _ -> failwith "Unexpected" + let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in + (* Create fresh symbolic values for the inputs *) + let input_svs = + List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs in - (* Reexplore *) - end_abstraction_borrows config abs_id ctx - -(** Update the symbolic values in a context to register the regions in the - abstraction we are ending as already ended. - Note that this function also checks that no symbolic value in an abstraction - contains regions which we are ending. - Of course, we ignore the abstraction we are currently ending... - *) -and end_abstraction_regions (_config : C.config) (abs_id : V.AbstractionId.id) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Lookup the abstraction to retrieve the set of owned regions *) - let abs = C.ctx_lookup_abs ctx abs_id in - let ended_regions = abs.V.regions in - (* Update all the symbolic values in the context *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic _ sproj = - let sproj = - { - sproj with - V.rset_ended = T.RegionId.Set.union sproj.V.rset_ended ended_regions; - } - in - V.Symbolic sproj - - method! visit_aproj (abs_regions : T.RegionId.set_t option) aproj = - (* Sanity check *) - (match aproj with - | V.AProjLoans _ -> () - | V.AProjBorrows (sv, ty) -> ( - match abs_regions with - | None -> failwith "Unexpected" - | Some abs_regions -> - assert ( - not - (projections_intersect sv.V.sv_ty ended_regions ty - abs_regions)))); - (* Return - nothing to update *) - aproj - - method! visit_abs (regions : T.RegionId.set_t option) abs = - if abs.V.abs_id = abs_id then abs - else ( - assert (Option.is_none regions); - (* Check that we don't project over already ended regions *) - assert (T.RegionId.Set.disjoint ended_regions abs.V.regions); - (* Remember the set of regions owned by the abstraction *) - let regions = Some abs.V.regions in - super#visit_abs regions abs) - (** Whenever we dive in an abstraction, we need to keep track of the - set of regions owned by the abstraction. - Also: we don't dive in the abstraction we are currently ending... *) - end - in - (* Update the context *) - obj#visit_eval_ctx None ctx - -(** Remove an abstraction from the context, as well as all its references *) -and end_abstraction_remove_from_context (_config : C.config) - (abs_id : V.AbstractionId.id) (ctx : C.eval_ctx) : C.eval_ctx = - let map_env_elem (ev : C.env_elem) : C.env_elem option = - match ev with - | C.Var (_, _) | C.Frame -> Some ev - | C.Abs abs -> - if abs.abs_id = abs_id then None - else - let parents = V.AbstractionId.Set.remove abs_id abs.parents in - Some (C.Abs { abs with V.parents }) - in - let env = List.filter_map map_env_elem ctx.C.env in - { ctx with C.env } - -and end_outer_borrow config = end_borrow config Outer None - -and end_outer_borrows config = end_borrows config Outer None - -and end_inner_borrow config = end_borrow config Inner None - -and end_inner_borrows config = end_borrows config Inner None - -(** Helper function: see [activate_inactivated_mut_borrow]. - - This function updates the shared loan to a mutable loan (we then update - the borrow with another helper). Of course, the shared loan must contain - exactly one borrow id (the one we give as parameter), otherwise we can't - promote it. Also, the shared value mustn't contain any loan. - - The returned value (previously shared) is checked: - - it mustn't contain loans - - it mustn't contain [Bottom] - - it mustn't contain inactivated borrows - TODO: this kind of checks should be put in an auxiliary helper, because - they are redundant - *) -let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) : - C.eval_ctx * V.typed_value = - (* Lookup the shared loan *) - let ek = - { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } - in - match lookup_loan ek l ctx with - | _, Concrete (V.MutLoan _) -> - failwith "Expected a shared loan, found a mut loan" - | _, Concrete (V.SharedLoan (bids, sv)) -> - (* Check that there is only one borrow id (l) and update the loan *) - assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1); - (* 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)); - (* Check there isn't [Bottom] (this is actually an invariant *) - assert (not (bottom_in_value sv)); - (* Check there aren't inactivated borrows *) - assert (not (inactivated_in_value sv)); - (* Update the loan content *) - let ctx = update_loan ek l (V.MutLoan l) ctx in - (* Return *) - (ctx, sv) - | _, 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. *) - failwith - "Can't promote a shared loan to a mutable loan if the loan is inside \ - an abstraction" - -(** Helper function: see [activate_inactivated_mut_borrow]. - - This function updates a shared borrow to a mutable borrow. - *) -let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) - (borrowed_value : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = - (* Lookup the inactivated borrow - note that we don't go inside borrows/loans: - there can't be inactivated borrows inside other borrows/loans - *) - let ek = - { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } - in - match lookup_borrow ek l ctx with - | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) -> - failwith "Expected an inactivated mutable borrow" - | Concrete (V.InactivatedMutBorrow _) -> - (* Update it *) - update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx - | Abstract _ -> - (* This can't happen for sure *) - failwith - "Can't promote a shared borrow to a mutable borrow if the borrow is \ - inside an abstraction" - -(** Promote an inactivated mut borrow to a mut borrow. - - The borrow must point to a shared value which is borrowed exactly once. - *) -let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) - (l : V.BorrowId.id) (ctx : C.eval_ctx) : C.eval_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 (V.MutLoan _) -> failwith "Unreachable" - | _, Concrete (V.SharedLoan (bids, sv)) -> ( - (* If there are loans inside the value, end them. Note that there can't be - inactivated borrows inside the value. - If we perform an update, do a recursive call to lookup the updated value *) - match get_first_loan_in_value sv with - | Some lc -> - (* End the loans *) - let ctx = - match lc with - | V.SharedLoan (bids, _) -> end_outer_borrows config bids ctx - | V.MutLoan bid -> end_outer_borrow config bid ctx - in - (* Recursive call *) - activate_inactivated_mut_borrow config io l ctx - | None -> - (* No loan to end inside the value *) - (* Some sanity checks *) - L.log#ldebug - (lazy - ("activate_inactivated_mut_borrow: resulting value:\n" - ^ V.show_typed_value sv)); - assert (not (loans_in_value sv)); - assert (not (bottom_in_value sv)); - assert (not (inactivated_in_value sv)); - (* End the borrows which borrow from the value, at the exception of - the borrow we want to promote *) - let bids = V.BorrowId.Set.remove l bids in - let allowed_abs = None in - let ctx = end_borrows config io allowed_abs bids ctx in - (* Promote the loan *) - let ctx, borrowed_value = promote_shared_loan_to_mut_loan l ctx in - (* Promote the borrow - the value should have been checked by - [promote_shared_loan_to_mut_loan] - *) - promote_inactivated_borrow_to_mut_borrow l borrowed_value ctx) - | _, 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. *) - failwith - "Can't activate an inactivated mutable borrow referencing a loan inside\n\ - \ an abstraction" - -(** Paths *) - -(** When we fail reading from or writing to a path, it might be because we - need to update the environment by ending borrows, expanding symbolic - values, etc. The following type is used to convey this information. - - TODO: compare with borrow_lres? -*) -type path_fail_kind = - | FailSharedLoan of V.BorrowId.Set.t - (** Failure because we couldn't go inside a shared loan *) - | FailMutLoan of V.BorrowId.id - (** Failure because we couldn't go inside a mutable loan *) - | FailInactivatedMutBorrow of V.BorrowId.id - (** Failure because we couldn't go inside an inactivated mutable borrow - (which should get activated) *) - | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp) - (** Failure because we need to enter a symbolic value (and thus need to expand it) *) - (* TODO: Remove the parentheses *) - | FailBottom of (int * E.projection_elem * T.ety) - (** Failure because we need to enter an any value - we can expand Bottom - values if they are left values. We return the number of elements which - were remaining in the path when we reached the error - this allows to - properly update the Bottom value, if needs be. - *) - | FailBorrow of V.borrow_content - (** We got stuck because we couldn't enter a borrow *) - -(** Result of evaluating a path (reading from a path/writing to a path) - - Note that when we fail, we return information used to update the - environment, as well as the -*) -type 'a path_access_result = ('a, path_fail_kind) result -(** The result of reading from/writing to a place *) - -type updated_read_value = { read : V.typed_value; updated : V.typed_value } - -type projection_access = { - enter_shared_loans : bool; - enter_mut_borrows : bool; - lookup_shared_borrows : bool; -} - -(** Generic function to access (read/write) the value at the end of a projection. - - We return the (eventually) updated value, the value we read at the end of - the place and the (eventually) updated environment. - - TODO: use exceptions? - *) -let rec access_projection (access : projection_access) (ctx : C.eval_ctx) - (* Function to (eventually) update the value we find *) - (update : V.typed_value -> V.typed_value) (p : E.projection) - (v : V.typed_value) : (C.eval_ctx * updated_read_value) path_access_result = - (* For looking up/updating shared loans *) - let ek : exploration_kind = - { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } - in - match p with - | [] -> - let nv = update v in - (* Type checking *) - if nv.ty <> v.ty then ( - L.log#lerror - (lazy - ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: " - ^ T.show_ety v.ty)); - failwith - "Assertion failed: new value doesn't have the same type as its \ - destination"); - Ok (ctx, { read = v; updated = nv }) - | pe :: p' -> ( - (* Match on the projection element and the value *) - match (pe, v.V.value, v.V.ty) with - (* Field projection - ADTs *) - | ( Field (ProjAdt (def_id, opt_variant_id), field_id), - V.Adt adt, - T.Adt (T.AdtId def_id', _, _) ) -> ( - assert (def_id = def_id'); - (* Check that the projection is consistent with the current value *) - (match (opt_variant_id, adt.variant_id) with - | None, None -> () - | Some vid, Some vid' -> if vid <> vid' then failwith "Unreachable" - | _ -> failwith "Unreachable"); - (* Actually project *) - let fv = T.FieldId.nth adt.field_values field_id in - match access_projection access ctx update p' fv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the field value *) - let nvalues = - T.FieldId.update_nth adt.field_values field_id res.updated - in - let nadt = V.Adt { adt with V.field_values = nvalues } in - let updated = { v with value = nadt } in - Ok (ctx, { res with updated })) - (* Tuples *) - | Field (ProjTuple arity, field_id), V.Adt adt, T.Adt (T.Tuple, _, _) -> ( - assert (arity = List.length adt.field_values); - let fv = T.FieldId.nth adt.field_values field_id in - (* Project *) - match access_projection access ctx update p' fv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the field value *) - let nvalues = - T.FieldId.update_nth adt.field_values field_id res.updated - in - let ntuple = V.Adt { adt with field_values = nvalues } in - let updated = { v with value = ntuple } in - Ok (ctx, { res with updated }) - (* If we reach Bottom, it may mean we need to expand an uninitialized - * enumeration value *)) - | Field (ProjAdt (_, _), _), V.Bottom, _ -> - Error (FailBottom (1 + List.length p', pe, v.ty)) - | Field (ProjTuple _, _), V.Bottom, _ -> - Error (FailBottom (1 + List.length p', pe, v.ty)) - (* Symbolic value: needs to be expanded *) - | _, Symbolic sp, _ -> - (* Expand the symbolic value *) - Error (FailSymbolic (pe, sp)) - (* Box dereferencement *) - | ( DerefBox, - Adt { variant_id = None; field_values = [ bv ] }, - T.Adt (T.Assumed T.Box, _, _) ) -> ( - (* We allow moving inside of boxes. In practice, this kind of - * manipulations should happen only inside unsage code, so - * it shouldn't happen due to user code, and we leverage it - * when implementing box dereferencement for the concrete - * interpreter *) - match access_projection access ctx update p' bv with - | Error err -> Error err - | Ok (ctx, res) -> - let nv = - { - v with - value = - V.Adt { variant_id = None; field_values = [ res.updated ] }; - } - in - Ok (ctx, { res with updated = nv })) - (* Borrows *) - | Deref, V.Borrow bc, _ -> ( - match bc with - | V.SharedBorrow bid -> - (* Lookup the loan content, and explore from there *) - if access.lookup_shared_borrows then - match lookup_loan ek bid ctx with - | _, Concrete (V.MutLoan _) -> failwith "Expected a shared loan" - | _, Concrete (V.SharedLoan (bids, sv)) -> ( - (* Explore the shared value *) - match access_projection access ctx update p' sv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the shared loan with the new value returned - by [access_projection] *) - let ctx = - update_loan ek bid - (V.SharedLoan (bids, res.updated)) - ctx - in - (* Return - note that we don't need to update the borrow itself *) - Ok (ctx, { res with updated = v })) - | ( _, - Abstract - ( V.AMutLoan (_, _) - | V.AEndedMutLoan { given_back = _; child = _ } - | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) - | V.AEndedIgnoredMutLoan { given_back = _; child = _ } - | V.AIgnoredSharedLoan _ ) ) -> - failwith "Expected a shared (abstraction) loan" - | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> ( - (* Explore the shared value *) - match access_projection access ctx update p' sv with - | Error err -> Error err - | Ok (ctx, res) -> - (* Relookup the child avalue *) - let av = - match lookup_loan ek bid ctx with - | _, Abstract (V.ASharedLoan (_, _, av)) -> av - | _ -> failwith "Unexpected" - in - (* Update the shared loan with the new value returned - by [access_projection] *) - let ctx = - update_aloan ek bid - (V.ASharedLoan (bids, res.updated, av)) - ctx - in - (* Return - note that we don't need to update the borrow itself *) - Ok (ctx, { res with updated = v })) - else Error (FailBorrow bc) - | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) - | V.MutBorrow (bid, bv) -> - if access.enter_mut_borrows then - match access_projection access ctx update p' bv with - | Error err -> Error err - | Ok (ctx, res) -> - let nv = - { - v with - value = V.Borrow (V.MutBorrow (bid, res.updated)); - } - in - Ok (ctx, { res with updated = nv }) - else Error (FailBorrow bc)) - | _, V.Loan lc, _ -> ( - match lc with - | V.MutLoan bid -> Error (FailMutLoan bid) - | V.SharedLoan (bids, sv) -> - (* If we can enter shared loan, we ignore the loan. Pay attention - to the fact that we need to reexplore the *whole* place (i.e, - we mustn't ignore the current projection element *) - if access.enter_shared_loans then - match access_projection access ctx update (pe :: p') sv with - | Error err -> Error err - | Ok (ctx, res) -> - let nv = - { - v with - value = V.Loan (V.SharedLoan (bids, res.updated)); - } - in - Ok (ctx, { res with updated = nv }) - else Error (FailSharedLoan bids)) - | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r -> - let pe, v, ty = r in - let pe = "- pe: " ^ E.show_projection_elem pe in - let v = "- v:\n" ^ V.show_value v in - let ty = "- ty:\n" ^ T.show_ety ty in - L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); - failwith "Inconsistent projection") - -(** Generic function to access (read/write) the value at a given place. - - We return the value we read at the place and the (eventually) updated - environment, if we managed to access the place, or the precise reason - why we failed. - *) -let access_place (access : projection_access) - (* Function to (eventually) update the value we find *) - (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx) - : (C.eval_ctx * V.typed_value) path_access_result = - (* Lookup the variable's value *) - let value = C.ctx_lookup_var_value ctx p.var_id in - (* Apply the projection *) - match access_projection access ctx update p.projection value with - | Error err -> Error err - | Ok (ctx, res) -> - (* Update the value *) - let ctx = C.ctx_update_var_value ctx p.var_id res.updated in + (* Create the abstractions and insert them in the context *) + let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = + let abs_id = rg.A.id in + let parents = + List.fold_left + (fun s pid -> V.AbstractionId.Set.add pid s) + V.AbstractionId.Set.empty rg.A.parents + in + let regions = + List.fold_left + (fun s rid -> T.RegionId.Set.add rid s) + T.RegionId.Set.empty rg.A.regions + in + (* Project over the values - we use *loan* projectors, as explained above *) + let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in + (* Create the abstraction *) + let abs = { V.abs_id; parents; regions; avalues } in + (* Insert the abstraction in the context *) + let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) - Ok (ctx, res.read) - -type access_kind = - | Read (** We can go inside borrows and loans *) - | Write (** Don't enter shared borrows or shared loans *) - | Move (** Don't enter borrows or loans *) - -let access_kind_to_projection_access (access : access_kind) : projection_access - = - match access with - | Read -> - { - enter_shared_loans = true; - enter_mut_borrows = true; - lookup_shared_borrows = true; - } - | Write -> - { - enter_shared_loans = false; - enter_mut_borrows = true; - lookup_shared_borrows = false; - } - | Move -> - { - enter_shared_loans = false; - enter_mut_borrows = false; - lookup_shared_borrows = false; - } - -(** Read the value at a given place *) -let read_place (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : V.typed_value path_access_result = - let access = access_kind_to_projection_access access in - (* The update function is the identity *) - let update v = v in - match access_place access update p ctx with - | Error err -> Error err - | Ok (ctx1, read_value) -> - (* Note that we ignore the new environment: it should be the same as the - original one. - *) - if config.check_invariants then - if ctx1 <> ctx then ( - let msg = - "Unexpected environment update:\nNew environment:\n" - ^ C.show_env ctx1.env ^ "\n\nOld environment:\n" - ^ C.show_env ctx.env - in - L.log#serror msg; - failwith "Unexpected environment update"); - Ok read_value - -let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : V.typed_value = - match read_place config access p ctx with - | Error _ -> failwith "Unreachable" - | Ok v -> v - -(** Update the value at a given place *) -let write_place (_config : C.config) (access : access_kind) (p : E.place) - (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx path_access_result = - let access = access_kind_to_projection_access access in - (* The update function substitutes the value with the new value *) - let update _ = nv in - match access_place access update p ctx with - | Error err -> Error err - | Ok (ctx, _) -> - (* We ignore the read value *) - Ok ctx - -let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place) - (nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx = - match write_place config access p nv ctx with - | Error _ -> failwith "Unreachable" - | Ok ctx -> ctx - -(** Projector kind *) -type proj_kind = LoanProj | BorrowProj - -(** Auxiliary function. - Apply a symbolic expansion to avalues in a context, targetting a specific - kind of projectors. - - [proj_kind] controls whether we apply the expansion to projectors - on loans or projectors on borrows. - - When dealing with reference expansion, it is necessary to first apply the - expansion on loan projectors, then on borrow projectors. The reason is - that reducing the borrow projectors might require to perform some reborrows, - in which case we need to lookup the corresponding loans in the context. - - [allow_reborrows] controls whether we allow reborrows or not. It is useful - only if we target borrow projectors. - - Also, if this function is called on an expansion for *shared references*, - the proj borrows should already have been expanded. - - TODO: the way this function is used is a bit complex, especially because of - the above condition. Maybe we should have: - 1. a generic function to expand the loan projectors - 2. a function to expand the borrow projectors for non-borrows - 3. specialized functions for mut borrows and shared borrows - Note that 2. and 3. may have a little bit of duplicated code, but hopefully - it would make things clearer. -*) -let apply_symbolic_expansion_to_target_avalues (config : C.config) - (allow_reborrows : bool) (proj_kind : proj_kind) - (original_sv : V.symbolic_value) (expansion : symbolic_expansion) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Symbolic values contained in the expansion might contain already ended regions *) - let check_symbolic_no_ended = false in - (* Prepare reborrows registration *) - let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows ctx - in - (* Visitor to apply the expansion *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_abs proj_regions abs = - assert (Option.is_none proj_regions); - let proj_regions = Some abs.V.regions in - super#visit_abs proj_regions abs - (** When visiting an abstraction, we remember the regions it owns to be - able to properly reduce projectors when expanding symbolic values *) - - method! visit_ASymbolic proj_regions aproj = - let proj_regions = Option.get proj_regions in - match (aproj, proj_kind) with - | V.AProjLoans sv, LoanProj -> - (* Check if this is the symbolic value we are looking for *) - if same_symbolic_id sv original_sv then - (* Apply the projector *) - let projected_value = - apply_proj_loans_on_symbolic_expansion proj_regions expansion - original_sv.V.sv_ty - in - (* Replace *) - projected_value.V.value - else - (* Not the searched symbolic value: nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj - | V.AProjBorrows (sv, proj_ty), BorrowProj -> - (* Check if this is the symbolic value we are looking for *) - if same_symbolic_id sv original_sv then - (* Convert the symbolic expansion to a value on which we can - * apply a projector (if the expansion is a reference expansion, - * convert it to a borrow) *) - (* WARNING: we mustn't get there if the expansion is for a shared - * reference. *) - let expansion = - symbolic_expansion_non_shared_borrow_to_value original_sv - expansion - in - (* Apply the projector *) - let projected_value = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow - proj_regions expansion proj_ty - in - (* Replace *) - projected_value.V.value - else - (* Not the searched symbolic value: nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj - | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj -> - (* Nothing to do *) - super#visit_ASymbolic (Some proj_regions) aproj - end - in - (* Apply the expansion *) - let ctx = obj#visit_eval_ctx None ctx in - (* Apply the reborrows *) - apply_registered_reborrows ctx - -(** Auxiliary function. - Apply a symbolic expansion to avalues in a context. -*) -let apply_symbolic_expansion_to_avalues (config : C.config) - (allow_reborrows : bool) (original_sv : V.symbolic_value) - (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = - let apply_expansion proj_kind ctx = - apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind - original_sv expansion ctx - in - (* First target the loan projectors, then the borrow projectors *) - let ctx = apply_expansion LoanProj ctx in - let ctx = apply_expansion BorrowProj ctx in - ctx - -(** Auxiliary function. - - Simply replace the symbolic values (*not avalues*) in the context with - a given value. Will break invariants if not used properly. -*) -let replace_symbolic_values (at_most_once : bool) - (original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) : - C.eval_ctx = - (* Count *) - let replaced = ref false in - let replace () = - if at_most_once then assert (not !replaced); - replaced := true; - nv - in - (* Visitor to apply the substitution *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic env spc = - if same_symbolic_id spc.V.svalue original_sv then replace () - else super#visit_Symbolic env spc - end - in - (* Apply the substitution *) - let ctx = obj#visit_eval_ctx None ctx in - (* Check that we substituted *) - assert !replaced; - (* Return *) - ctx - -(** Apply a symbolic expansion to a context, by replacing the original - symbolic value with its expanded value. Is valid only if the expansion - is not a borrow (i.e., an adt...). -*) -let apply_symbolic_expansion_non_borrow (config : C.config) - (original_sv : V.symbolic_value) (expansion : symbolic_expansion) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Apply the expansion to non-abstraction values *) - let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in - let at_most_once = false in - let ctx = replace_symbolic_values at_most_once original_sv nv.V.value ctx in - (* Apply the expansion to abstraction values *) - let allow_reborrows = false in - apply_symbolic_expansion_to_avalues config allow_reborrows original_sv - expansion ctx - -(** Compute an expanded ADT bottom value *) -let compute_expanded_bottom_adt_value (tyctx : T.type_def list) - (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option) - (regions : T.erased_region list) (types : T.ety list) : V.typed_value = - (* Lookup the definition and check if it is an enumeration - it - should be an enumeration if and only if the projection element - is a field projection with *some* variant id. Retrieve the list - of fields at the same time. *) - let def = T.TypeDefId.nth tyctx def_id in - assert (List.length regions = List.length def.T.region_params); - (* Compute the field types *) - let field_types = - Subst.type_def_get_instantiated_field_etypes def opt_variant_id types - in - (* Initialize the expanded value *) - let fields = - List.map - (fun ty : V.typed_value -> ({ V.value = V.Bottom; ty } : V.typed_value)) - field_types - in - let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in - let ty = T.Adt (T.AdtId def_id, regions, types) in - { V.value = av; V.ty } - -(** Compute an expanded tuple bottom value *) -let compute_expanded_bottom_tuple_value (field_types : T.ety list) : - V.typed_value = - (* Generate the field values *) - let fields = - List.map (fun ty : V.typed_value -> { V.value = Bottom; ty }) field_types - in - let v = V.Adt { variant_id = None; field_values = fields } in - let ty = T.Adt (T.Tuple, [], field_types) in - { V.value = v; V.ty } - -(** Auxiliary helper to expand [Bottom] values. - - During compilation, rustc desaggregates the ADT initializations. The - consequence is that the following rust code: - ``` - let x = Cons a b; - ``` - - Looks like this in MIR: - ``` - (x as Cons).0 = a; - (x as Cons).1 = b; - set_discriminant(x, 0); // If `Cons` is the variant of index 0 - ``` - - The consequence is that we may sometimes need to write fields to values - which are currently [Bottom]. When doing this, we first expand the value - to, say, [Cons Bottom Bottom] (note that field projection contains information - about which variant we should project to, which is why we *can* set the - variant index when writing one of its fields). -*) -let expand_bottom_value_from_projection (config : C.config) - (access : access_kind) (p : E.place) (remaining_pes : int) - (pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx = - (* Debugging *) - L.log#ldebug - (lazy - ("expand_bottom_value_from_projection:\n" ^ "pe: " - ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty)); - (* Prepare the update: we need to take the proper prefix of the place - during whose evaluation we got stuck *) - let projection' = - fst - (Utilities.list_split_at p.projection - (List.length p.projection - remaining_pes)) - in - let p' = { p with projection = projection' } in - (* Compute the expanded value. - The type of the [Bottom] value should be a tuple or an ADT. - Note that the projection element we got stuck at should be a - field projection, and gives the variant id if the [Bottom] value - is an enumeration value. - Also, the expanded value should be the proper ADT variant or a tuple - with the proper arity, with all the fields initialized to [Bottom] - *) - let nv = - match (pe, ty) with - (* "Regular" ADTs *) - | ( Field (ProjAdt (def_id, opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types) ) -> - assert (def_id = def_id'); - compute_expanded_bottom_adt_value ctx.type_context def_id opt_variant_id - regions types - (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> - assert (arity = List.length tys); - (* Generate the field values *) - compute_expanded_bottom_tuple_value tys - | _ -> - failwith - ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty) - in - (* Update the context by inserting the expanded value at the proper place *) - match write_place config access p' nv ctx with - | Ok ctx -> ctx - | Error _ -> failwith "Unreachable" - -(** Compute the expansion of an adt value. - - The function might return a list of contexts and values if the symbolic - value to expand is an enumeration. - - `expand_enumerations` controls the expansion of enumerations: if false, it - doesn't allow the expansion of enumerations *containing several variants*. - *) -let compute_expanded_symbolic_adt_value (expand_enumerations : bool) - (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id) - (regions : T.RegionId.id T.region list) (types : T.rty list) - (ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list = - (* Lookup the definition and check if it is an enumeration with several - * variants *) - let def = T.TypeDefId.nth ctx.type_context def_id in - assert (List.length regions = List.length def.T.region_params); - (* Retrieve, for every variant, the list of its instantiated field types *) - let variants_fields_types = - Subst.type_def_get_instantiated_variants_fields_rtypes def regions types - in - (* Check if there is strictly more than one variant *) - if List.length variants_fields_types > 1 && not expand_enumerations then - failwith "Not allowed to expand enumerations with several variants"; - (* Initialize the expanded value for a given variant *) - let initialize (ctx : C.eval_ctx) - ((variant_id, field_types) : T.VariantId.id option * T.rty list) : - C.eval_ctx * symbolic_expansion = - let ctx, field_values = - List.fold_left_map - (fun ctx (ty : T.rty) -> - mk_fresh_symbolic_proj_comp ended_regions ty ctx) - ctx field_types + ctx in - let see = SeAdt (variant_id, field_values) in - (ctx, see) - in - (* Initialize all the expanded values of all the variants *) - List.map (initialize ctx) variants_fields_types - -let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t) - (field_types : T.rty list) (ctx : C.eval_ctx) : - C.eval_ctx * symbolic_expansion = - (* Generate the field values *) - let ctx, field_values = - List.fold_left_map - (fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx) - ctx field_types - in - let variant_id = None in - let see = SeAdt (variant_id, field_values) in - (ctx, see) - -let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t) - (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion = - (* Introduce a fresh symbolic value *) - let ctx, boxed_value = - mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx - in - let see = SeAdt (None, [ boxed_value ]) in - (ctx, see) - -let expand_symbolic_value_shared_borrow (config : C.config) - (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t) - (ref_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx = - (* First, replace the projectors on borrows (AProjBorrow and proj_comp) - * The important point is that the symbolic value to expand may appear - * several times, if it has been copied. In this case, we need to introduce - * one fresh borrow id per instance. - *) - let borrows = ref V.BorrowId.Set.empty in - let borrow_counter = ref ctx.C.borrow_counter in - let fresh_borrow () = - let bid', cnt' = V.BorrowId.fresh !borrow_counter in - borrow_counter := cnt'; - borrows := V.BorrowId.Set.add bid' !borrows; - bid' - in - (* Small utility used on shared borrows in abstractions (regular borrow - * projector and asb). - * Returns `Some` if the symbolic value has been expanded to an asb list, - * `None` otherwise *) - let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) : - V.abstract_shared_borrows option = - if same_symbolic_id sv original_sv then - match proj_ty with - | T.Ref (r, ref_ty, T.Shared) -> - (* Projector over the shared value *) - let shared_asb = V.AsbProjReborrows (sv, ref_ty) in - (* Check if the region is in the set of projected regions *) - if region_in_set r proj_regions then - (* In the set: we need to reborrow *) - let bid = fresh_borrow () in - Some [ V.AsbBorrow bid; shared_asb ] - else (* Not in the set: ignore *) - Some [ shared_asb ] - | _ -> failwith "Unexpected" - else None - in - (* Visitor to replace the projectors on borrows *) - let obj = - object - inherit [_] C.map_eval_ctx as super - - method! visit_Symbolic env sv = - if same_symbolic_id sv.V.svalue original_sv then - let bid = fresh_borrow () in - V.Borrow (V.SharedBorrow bid) - else super#visit_Symbolic env sv - - method! visit_Abs proj_regions abs = - assert (Option.is_none proj_regions); - let proj_regions = Some abs.V.regions in - super#visit_Abs proj_regions abs - - method! visit_AProjSharedBorrow proj_regions asb = - let expand_asb (asb : V.abstract_shared_borrow) : - V.abstract_shared_borrows = - match asb with - | V.AsbBorrow _ -> [ asb ] - | V.AsbProjReborrows (sv, proj_ty) -> ( - match reborrow_ashared (Option.get proj_regions) sv proj_ty with - | None -> [ asb ] - | Some asb -> asb) - in - let asb = List.concat (List.map expand_asb asb) in - V.AProjSharedBorrow asb - - method! visit_ASymbolic proj_regions aproj = - match aproj with - | AProjLoans _ -> - (* Loans are handled later *) - super#visit_ASymbolic proj_regions aproj - | AProjBorrows (sv, proj_ty) -> ( - (* Check if we need to reborrow *) - match reborrow_ashared (Option.get proj_regions) sv proj_ty with - | None -> super#visit_ASymbolic proj_regions aproj - | Some asb -> V.ABorrow (V.AProjSharedBorrow asb)) - end - in - (* Call the visitor *) - let ctx = obj#visit_eval_ctx None ctx in - let ctx = { ctx with C.borrow_counter = !borrow_counter } in - (* Finally, replace the projectors on loans *) - let bids = !borrows in - assert (not (V.BorrowId.Set.is_empty bids)); - let ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in - let see = SeSharedRef (bids, shared_sv) in - let allow_reborrows = true in - apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see ctx - -let expand_symbolic_value_borrow (config : C.config) - (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t) - (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Check that we are allowed to expand the reference *) - assert (not (region_in_set region ended_regions)); - (* Match on the reference kind *) - match rkind with - | T.Mut -> - (* Simple case: simply create a fresh symbolic value and a fresh - * borrow id *) - let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in - let ctx, bid = C.fresh_borrow_id ctx in - let see = SeMutRef (bid, sv) in - (* Expand the symbolic values - we simply perform a substitution (and - * check that we perform exactly one substitution) *) - let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in - let at_most_once = true in - let ctx = - replace_symbolic_values at_most_once original_sv nv.V.value ctx - in - (* Expand the symbolic avalues *) - let allow_reborrows = true in - apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see - ctx - | T.Shared -> - expand_symbolic_value_shared_borrow config original_sv ended_regions - ref_ty ctx - -(** Expand a symbolic value which is not an enumeration with several variants. - - This function is used when exploring a path. - *) -let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem) - (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) : C.eval_ctx = - (* Compute the expanded value - note that when doing so, we may introduce - * fresh symbolic values in the context (which thus gets updated) *) - let rty = sp.V.svalue.V.sv_ty in - let ended_regions = sp.V.rset_ended in - let ctx = - match (pe, rty) with - (* "Regular" ADTs *) - | ( Field (ProjAdt (def_id, _opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types) ) -> ( - assert (def_id = def_id'); - (* Compute the expanded value - there should be exactly one because we - * don't allow to expand enumerations with strictly more than one variant *) - let expand_enumerations = false in - match - compute_expanded_symbolic_adt_value expand_enumerations ended_regions - def_id regions types ctx - with - | [ (ctx, nv) ] -> - (* Apply in the context *) - apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx - | _ -> failwith "Unexpected") - (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> - assert (arity = List.length tys); - (* Generate the field values *) - let ctx, nv = - compute_expanded_symbolic_tuple_value ended_regions tys ctx - in - (* Apply in the context *) - apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx - (* Boxes *) - | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> - let ctx, nv = - compute_expanded_symbolic_box_value ended_regions boxed_ty ctx - in - (* Apply in the context *) - apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx - (* Borrows *) - | Deref, T.Ref (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config sp.V.svalue ended_regions region - ref_ty rkind ctx - | _ -> - failwith - ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) - in - (* Sanity check: the symbolic value has disappeared *) - assert (not (symbolic_value_id_in_ctx sp.V.svalue.V.sv_id ctx)); - (* Return *) - ctx - -(** Update the environment to be able to read a place. - - When reading a place, we may be stuck along the way because some value - is borrowed, we reach a symbolic value, etc. In this situation [read_place] - fails while returning precise information about the failure. This function - uses this information to update the environment (by ending borrows, - expanding symbolic values) until we manage to fully read the place. - *) -let rec update_ctx_along_read_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Attempt to read the place: if it fails, update the environment and retry *) - match read_place config access p ctx with - | Ok _ -> ctx - | Error err -> - let ctx = - match err with - | FailSharedLoan bids -> end_outer_borrows config bids ctx - | FailMutLoan bid -> end_outer_borrow config bid ctx - | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config Outer bid ctx - | FailSymbolic (pe, sp) -> - (* Expand the symbolic value *) - expand_symbolic_value_non_enum config pe sp ctx - | FailBottom (_, _, _) -> - (* We can't expand [Bottom] values while reading them *) - failwith "Found [Bottom] while reading a place" - | FailBorrow _ -> failwith "Could not read a borrow" - in - update_ctx_along_read_place config access p ctx - -(** Update the environment to be able to write to a place. - - See [update_env_alond_read_place]. -*) -let rec update_ctx_along_write_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Attempt to *read* (yes, "read": we check the access to the place, and - write to it later) the place: if it fails, update the environment and retry *) - match read_place config access p ctx with - | Ok _ -> ctx - | Error err -> - let ctx = - match err with - | FailSharedLoan bids -> end_outer_borrows config bids ctx - | FailMutLoan bid -> end_outer_borrow config bid ctx - | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config Outer bid ctx - | FailSymbolic (pe, sp) -> - (* Expand the symbolic value *) - expand_symbolic_value_non_enum config pe sp ctx - | FailBottom (remaining_pes, pe, ty) -> - (* Expand the [Bottom] value *) - expand_bottom_value_from_projection config access p remaining_pes pe - ty ctx - | FailBorrow _ -> failwith "Could not write to a borrow" - in - update_ctx_along_write_place config access p ctx - -exception UpdateCtx of C.eval_ctx -(** Small utility used to break control-flow *) - -(** End the loans at a given place: read the value, if it contains a loan, - end this loan, repeat. - - This is used when reading, borrowing, writing to a value. We typically - first call [update_ctx_along_read_place] or [update_ctx_along_write_place] - to get access to the value, then call this function to "prepare" the value: - when moving values, we can't move a value which contains loans and thus need - to end them, etc. - *) -let rec end_loans_at_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Iterator to explore a value and update the context whenever we find - * loans. - * We use exceptions to make it handy: whenever we update the - * context, we raise an exception wrapping the updated context. - * *) - let obj = - object - inherit [_] V.iter_typed_value as super - - method! visit_borrow_content env bc = - match bc with - | V.SharedBorrow _ | V.MutBorrow (_, _) -> - (* Nothing special to do *) super#visit_borrow_content env bc - | V.InactivatedMutBorrow bid -> - (* We need to activate inactivated borrows *) - let ctx = activate_inactivated_mut_borrow config Inner bid ctx in - raise (UpdateCtx ctx) - - method! visit_loan_content env lc = - match lc with - | V.SharedLoan (bids, v) -> ( - (* End the loans if we need a modification access, otherwise dive into - the shared value *) - match access with - | Read -> super#visit_SharedLoan env bids v - | Write | Move -> - let ctx = end_outer_borrows config bids ctx in - raise (UpdateCtx ctx)) - | V.MutLoan bid -> - (* We always need to end mutable borrows *) - let ctx = end_outer_borrow config bid ctx in - raise (UpdateCtx ctx) - end - in - - (* First, retrieve the value *) - match read_place config access p ctx with - | Error _ -> failwith "Unreachable" - | Ok v -> ( - (* Inspect the value and update the context while doing so. - If the context gets updated: perform a recursive call (many things - may have been updated in the context: we need to re-read the value - at place [p] - and this value may actually not be accessible - anymore...) - *) - try - obj#visit_typed_value () v; - (* No context update required: return the current context *) - ctx - with UpdateCtx ctx -> - (* The context was updated: do a recursive call to reinspect the value *) - end_loans_at_place config access p ctx) - -(** Drop (end) all the loans and borrows at a given place, which should be - seen as an l-value (we will write to it later, but need to drop the borrows - before writing). - - We start by only dropping the borrows, then we end the loans. The reason - is that some loan we find may be borrowed by another part of the subvalue. - In order to correctly handle the "outer borrow" priority (we should end - the outer borrows first) which is not really applied here (we are preparing - the value for override: we can end the borrows inside, without ending the - borrows we traversed to actually access the value) we first end the borrows - we find in the place, to make sure all the "local" loans are taken care of. - Then, if we find a loan, it means it is "externally" borrowed (the associated - borrow is not in a subvalue of the place under inspection). - Also note that whenever we end a loan, we might propagate back a value inside - the place under inspection: we must re-end all the borrows we find there, - before reconsidering loans. - - Repeat: - - read the value at a given place - - as long as we find a loan or a borrow, end it - - This is used to drop values (when we need to write to a place, we first - drop the value there to properly propagate back values which are not/can't - be borrowed anymore). - *) -let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place) - (ctx : C.eval_ctx) : C.eval_ctx = - (* Iterator to explore a value and update the context whenever we find - borrows/loans. - We use exceptions to make it handy: whenever we update the - context, we raise an exception wrapping the updated context. - - Note that we can end the borrows which are inside the value (while the - value itself might be inside a borrow/loan: we are thus ending inner - borrows). Because a loan inside the value may be linked to a borrow - somewhere else *also inside* the value (it's possible with adts), - we first end all the borrows we find - by using [Inner] to allow - ending inner borrows - then end all the loans we find. - - It is really important to do this in two steps: the borrow linked to a - loan may be inside the value at place p, in which case this borrow may be - an inner borrow that we *can* end, but it may also be outside this - value, in which case we need to end all the outer borrows first... - Also, whenever the context is updated, we need to re-inspect - the value at place p *in two steps* again (end borrows, then end - loans). - - Example: - ======= - We want to end the borrows/loans at `*x` in the following environment: - ``` - x -> mut_borrow l0 (mut_loan l1, mut_borrow l1 (Int 3), mut_loan l2) - y -> mut_borrow l2 (Bool true) - ``` - - We have to consider two things: - - the borrow `mut_borrow l1 (Int 3)` borrows a subvalue of `*x` - - the borrow corresponding to the loan `mut_loan l2` is outside of `*x` - - We first end all the *borrows* (not the loans) inside of `*x`, which gives: - ``` - x -> mut_borrow l0 (Int 3, ⊥, mut_loan l2) - y -> mut_borrow l2 (Bool true) - ``` - - Note that when ending the borrows, we can (and have to) ignore the outer - borrows (in this case `mut_borrow l0 ...`). Otherwise, we would have to end - the borrow `l0` which is incorrect (note that we might have to drop the - borrows/loans at `*x` if we evaluate, for instance, `*x = ...`). - It is ok to ignore outer borrows in this case because whenever - we end a borrow, it is an outer borrow locally to `*x` (i.e., we ignore - the outer borrows when accessing `*x`, but once examining the value at - `*x` we never dive into borrows: whenever we find one, we end it - it is thus - an outer borrow, in some way). - - Then, we end the loans at `*x`. Note that as at this point `*x` doesn't - contain borrows (only loans), the borrows corresponding to those loans - are thus necessarily outside of `*x`: we mustn't ignore outer borrows this - time. This gives: - ``` - x -> mut_borrow l0 (Int 3, ⊥, Bool true) - y -> ⊥ - ``` - *) - let obj = - object - inherit [_] V.iter_typed_value as super - - method! visit_borrow_content end_loans bc = - (* Sanity check: we should have ended all the borrows before starting - to end loans *) - assert (not end_loans); - - (* We need to end all borrows. Note that we ignore the outer borrows - when ending the borrows we find here (we call [end_inner_borrow(s)]: - the value at place p might be below a borrow/loan). Note however - that if we restrain ourselves at the value at place p, the borrow we - found here can be considered as an outer borrow. - *) - match bc with - | V.SharedBorrow bid | V.MutBorrow (bid, _) -> - raise (UpdateCtx (end_inner_borrow config bid ctx)) - | V.InactivatedMutBorrow bid -> - (* We need to activate ithe nactivated borrow - later, we will - * actually end it - Rk.: we could actually end it straight away - * (this is not really important) *) - let ctx = activate_inactivated_mut_borrow config Inner bid ctx in - raise (UpdateCtx ctx) - - method! visit_loan_content end_loans lc = - if - (* If we can, end the loans, otherwise ignore: keep for later *) - end_loans - then - (* We need to end all loans. Note that as all the borrows inside - the value at place p should already have ended, the borrows - associated to the loans we find here should be borrows from - outside this value: we need to call [end_outer_borrow(s)] - (we can't ignore outer borrows this time). - *) - match lc with - | V.SharedLoan (bids, _) -> - raise (UpdateCtx (end_outer_borrows config bids ctx)) - | V.MutLoan bid -> raise (UpdateCtx (end_outer_borrow config bid ctx)) - else super#visit_loan_content end_loans lc - end - in - - (* We do something similar to [end_loans_at_place]. - First, retrieve the value *) - match read_place config Write p ctx with - | Error _ -> failwith "Unreachable" - | Ok v -> ( - (* Inspect the value and update the context while doing so. - If the context gets updated: perform a recursive call (many things - may have been updated in the context: first we need to retrieve the - proper updated value - and this value may actually not be accessible - anymore - *) - try - (* Inspect the value: end the borrows only *) - obj#visit_typed_value false v; - (* Inspect the value: end the loans *) - obj#visit_typed_value true v; - (* No context update required: return the current context *) - ctx - with UpdateCtx ctx -> drop_borrows_loans_at_lplace config p ctx) - -(** Copy a value, and return the resulting value. - - Note that copying values might update the context. For instance, when - copying shared borrows, we need to insert new shared borrows in the context. - *) -let rec copy_value (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) : - C.eval_ctx * V.typed_value = - (* Remark: at some point we rewrote this function to use iterators, but then - * we reverted the changes: the result was less clear actually. In particular, - * the fact that we have exhaustive matches below makes very obvious the cases - * in which we need to fail *) - match v.V.value with - | V.Concrete _ -> (ctx, v) - | V.Adt av -> - (* Sanity check *) - (match v.V.ty with - | T.Adt (T.Assumed _, _, _) -> failwith "Can't copy an assumed value" - | T.Adt ((T.AdtId _ | T.Tuple), _, _) -> () (* Ok *) - | _ -> failwith "Unreachable"); - let ctx, fields = - List.fold_left_map (copy_value config) ctx av.field_values - in - (ctx, { v with V.value = V.Adt { av with field_values = fields } }) - | V.Bottom -> failwith "Can't copy ⊥" - | V.Borrow bc -> ( - (* We can only copy shared borrows *) - match bc with - | SharedBorrow bid -> - (* We need to create a new borrow id for the copied borrow, and - * update the context accordingly *) - let ctx, bid' = C.fresh_borrow_id ctx in - let ctx = reborrow_shared bid bid' ctx in - (ctx, { v with V.value = V.Borrow (SharedBorrow bid') }) - | MutBorrow (_, _) -> failwith "Can't copy a mutable borrow" - | V.InactivatedMutBorrow _ -> - failwith "Can't copy an inactivated mut borrow") - | V.Loan lc -> ( - (* We can only copy shared loans *) - match lc with - | V.MutLoan _ -> failwith "Can't copy a mutable loan" - | V.SharedLoan (_, sv) -> - (* We don't copy the shared loan: only the shared value inside *) - copy_value config ctx sv) - | V.Symbolic _sp -> - (* TODO: check that the value is copyable *) - raise Unimplemented - -(** Convert a constant operand value to a typed value *) -let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) - (cv : E.operand_constant_value) : V.typed_value = - (* Check the type while converting *) - match (ty, cv) with - (* Unit *) - | T.Adt (T.Tuple, [], []), Unit -> mk_unit_value - (* Adt with one variant and no fields *) - | T.Adt (T.AdtId def_id, [], []), ConstantAdt def_id' -> - assert (def_id = def_id'); - (* Check that the adt definition only has one variant with no fields, - compute the variant id at the same time. *) - let def = T.TypeDefId.nth ctx.type_context def_id in - assert (List.length def.region_params = 0); - assert (List.length def.type_params = 0); - let variant_id = - match def.kind with - | Struct fields -> - assert (List.length fields = 0); - None - | Enum variants -> - assert (List.length variants = 1); - let variant_id = T.VariantId.zero in - let variant = T.VariantId.nth variants variant_id in - assert (List.length variant.fields = 0); - Some variant_id - in - let value = V.Adt { variant_id; field_values = [] } in - { value; ty } - (* Scalar, boolean... *) - | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty } - | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty } - | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty } - | T.Integer int_ty, ConstantValue (V.Scalar v) -> - (* Check the type and the ranges *) - assert (int_ty == v.int_ty); - assert (check_scalar_value_in_range v); - { V.value = V.Concrete (V.Scalar v); ty } - (* Remaining cases (invalid) - listing as much as we can on purpose - (allows to catch errors at compilation if the definitions change) *) - | _, Unit | _, ConstantAdt _ | _, ConstantValue _ -> - failwith "Improperly typed constant value" - -(** Small utility *) -let prepare_rplace (config : C.config) (access : access_kind) (p : E.place) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - let ctx = update_ctx_along_read_place config access p ctx in - let ctx = end_loans_at_place config access p ctx in - let v = read_place_unwrap config access p ctx in - (ctx, v) - -(** Evaluate an operand. *) -let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : - C.eval_ctx * V.typed_value = - (* Debug *) - L.log#ldebug - (lazy - ("eval_operand:\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n\n- op:\n" - ^ operand_to_string ctx op ^ "\n")); - (* Evaluate *) - match op with - | Expressions.Constant (ty, cv) -> - let v = constant_value_to_typed_value ctx ty cv in - (ctx, v) - | Expressions.Copy p -> - (* Access the value *) - let access = Read in - let ctx, v = prepare_rplace config access p ctx in - (* Copy the value *) - L.log#ldebug (lazy ("Value to copy:\n" ^ typed_value_to_string ctx v)); - assert (not (bottom_in_value v)); - copy_value config ctx v - | Expressions.Move p -> ( - (* Access the value *) - let access = Move in - let ctx, v = prepare_rplace config access p ctx in - (* Move the value *) - L.log#ldebug (lazy ("Value to move:\n" ^ typed_value_to_string ctx v)); - assert (not (bottom_in_value v)); - let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in - match write_place config access p bottom ctx with - | Error _ -> failwith "Unreachable" - | Ok ctx -> (ctx, v)) - -(** Evaluate several operands. *) -let eval_operands (config : C.config) (ctx : C.eval_ctx) (ops : E.operand list) - : C.eval_ctx * V.typed_value list = - List.fold_left_map (fun ctx op -> eval_operand config ctx op) ctx ops - -let eval_two_operands (config : C.config) (ctx : C.eval_ctx) (op1 : E.operand) - (op2 : E.operand) : C.eval_ctx * V.typed_value * V.typed_value = - match eval_operands config ctx [ op1; op2 ] with - | ctx, [ v1; v2 ] -> (ctx, v1, v2) - | _ -> failwith "Unreachable" - -let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : E.unop) - (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result = - (* Evaluate the operand *) - let ctx, v = eval_operand config ctx op in - (* Apply the unop *) - match (unop, v.V.value) with - | E.Not, V.Concrete (Bool b) -> - Ok (ctx, { v with V.value = V.Concrete (Bool (not b)) }) - | E.Neg, V.Concrete (V.Scalar sv) -> ( - let i = Z.neg sv.V.value in - match mk_scalar sv.int_ty i with - | Error _ -> Error Panic - | Ok sv -> Ok (ctx, { v with V.value = V.Concrete (V.Scalar sv) })) - | (E.Not | E.Neg), Symbolic _ -> raise Unimplemented (* TODO *) - | _ -> failwith "Invalid value for unop" - -let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop) - (op1 : E.operand) (op2 : E.operand) : - (C.eval_ctx * V.typed_value) eval_result = - (* Evaluate the operands *) - let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in - if - (* Binary operations only apply on integer values, but when we check for - * equality *) - binop = Eq || binop = Ne - then ( - (* Equality/inequality check is primitive only on primitive types *) - assert (v1.ty = v2.ty); - let b = v1 = v2 in - Ok (ctx, { V.value = V.Concrete (Bool b); ty = T.Bool })) - else - match (v1.V.value, v2.V.value) with - | V.Concrete (V.Scalar sv1), V.Concrete (V.Scalar sv2) -> ( - let res = - (* There are binops which require the two operands to have the same - type, and binops for which it is not the case. - There are also binops which return booleans, and binops which - return integers. - *) - match binop with - | E.Lt | E.Le | E.Ge | E.Gt -> - (* The two operands must have the same type and the result is a boolean *) - assert (sv1.int_ty = sv2.int_ty); - let b = - match binop with - | E.Lt -> Z.lt sv1.V.value sv2.V.value - | E.Le -> Z.leq sv1.V.value sv2.V.value - | E.Ge -> Z.geq sv1.V.value sv2.V.value - | E.Gt -> Z.gt sv1.V.value sv2.V.value - | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd - | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq -> - failwith "Unreachable" - in - Ok - ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value) - | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd - | E.BitOr -> ( - (* The two operands must have the same type and the result is an integer *) - assert (sv1.int_ty = sv2.int_ty); - let res = - match binop with - | E.Div -> - if sv2.V.value = Z.zero then Error () - else mk_scalar sv1.int_ty (Z.div sv1.V.value sv2.V.value) - | E.Rem -> - (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *) - if sv2.V.value = Z.zero then Error () - else mk_scalar sv1.int_ty (Z.rem sv1.V.value sv2.V.value) - | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.V.value sv2.V.value) - | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.V.value sv2.V.value) - | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.V.value sv2.V.value) - | E.BitXor -> raise Unimplemented - | E.BitAnd -> raise Unimplemented - | E.BitOr -> raise Unimplemented - | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq -> - failwith "Unreachable" - in - match res with - | Error err -> Error err - | Ok sv -> - Ok - { - V.value = V.Concrete (V.Scalar sv); - ty = Integer sv1.int_ty; - }) - | E.Shl | E.Shr -> raise Unimplemented - | E.Ne | E.Eq -> failwith "Unreachable" - in - match res with Error _ -> Error Panic | Ok v -> Ok (ctx, v)) - | _ -> failwith "Invalid inputs for binop" - -(** Evaluate an rvalue in a given context: return the updated context and - the computed value -*) -let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) : - (C.eval_ctx * V.typed_value) eval_result = - match rvalue with - | E.Use op -> Ok (eval_operand config ctx op) - | E.Ref (p, bkind) -> ( - match bkind with - | E.Shared | E.TwoPhaseMut -> - (* Access the value *) - let access = if bkind = E.Shared then Read else Write in - let ctx, v = prepare_rplace config access p ctx in - (* Compute the rvalue - simply a shared borrow with a fresh id *) - let ctx, bid = C.fresh_borrow_id ctx in - (* Note that the reference is *mutable* if we do a two-phase borrow *) - let rv_ty = - T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut) - in - let bc = - if bkind = E.Shared then V.SharedBorrow bid - else V.InactivatedMutBorrow bid - in - let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in - (* Compute the value with which to replace the value at place p *) - let nv = - match v.V.value with - | V.Loan (V.SharedLoan (bids, sv)) -> - (* Shared loan: insert the new borrow id *) - let bids1 = V.BorrowId.Set.add bid bids in - { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) } - | _ -> - (* Not a shared loan: add a wrapper *) - let v' = - V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) - in - { v with V.value = v' } - in - (* Update the value in the context *) - let ctx = write_place_unwrap config access p nv ctx in - (* Return *) - Ok (ctx, rv) - | E.Mut -> - (* Access the value *) - let access = Write in - let ctx, v = prepare_rplace config access p ctx in - (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) - let ctx, bid = C.fresh_borrow_id ctx in - let rv_ty = T.Ref (T.Erased, v.ty, Mut) in - let rv : V.typed_value = - { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty } - in - (* Compute the value with which to replace the value at place p *) - let nv = { v with V.value = V.Loan (V.MutLoan bid) } in - (* Update the value in the context *) - let ctx = write_place_unwrap config access p nv ctx in - (* Return *) - Ok (ctx, rv)) - | E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op - | E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2 - | E.Discriminant p -> ( - (* Note that discriminant values have type `isize` *) - (* Access the value *) - let access = Read in - let ctx, v = prepare_rplace config access p ctx in - match v.V.value with - | Adt av -> ( - match av.variant_id with - | None -> - failwith - "Invalid input for `discriminant`: structure instead of enum" - | Some variant_id -> ( - let id = Z.of_int (T.VariantId.to_int variant_id) in - match mk_scalar Isize id with - | Error _ -> - failwith "Disciminant id out of range" - (* Should really never happen *) - | Ok sv -> - Ok - ( ctx, - { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize } - ))) - | Symbolic _ -> raise Unimplemented - | _ -> failwith "Invalid input for `discriminant`") - | E.Aggregate (aggregate_kind, ops) -> ( - (* Evaluate the operands *) - let ctx, values = eval_operands config ctx ops in - (* Match on the aggregate kind *) - match aggregate_kind with - | E.AggregatedTuple -> - let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in - let v = V.Adt { variant_id = None; field_values = values } in - let ty = T.Adt (T.Tuple, [], tys) in - Ok (ctx, { V.value = v; ty }) - | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> - (* Sanity checks *) - let type_def = C.ctx_lookup_type_def ctx def_id in - assert (List.length type_def.region_params = List.length regions); - let expected_field_types = - Subst.ctx_adt_get_instantiated_field_etypes ctx def_id - opt_variant_id types - in - assert ( - expected_field_types - = List.map (fun (v : V.typed_value) -> v.V.ty) values); - (* Construct the value *) - let av : V.adt_value = - { V.variant_id = opt_variant_id; V.field_values = values } - in - let aty = T.Adt (T.AdtId def_id, regions, types) in - Ok (ctx, { V.value = Adt av; ty = aty })) - -(** Result of evaluating a statement *) -type statement_eval_res = Unit | Break of int | Continue of int | Return - -(** Small utility. - - Prepare a place which is to be used as the destination of an assignment: - update the environment along the paths, end the borrows and loans at - this place, etc. - - Return the updated context and the (updated) value at the end of the - place. This value should not contain any loan or borrow (and we check - it is the case). Note that it is very likely to contain [Bottom] values. - *) -let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) : - C.eval_ctx * V.typed_value = - (* TODO *) - let access = Write in - let ctx = update_ctx_along_write_place config access p ctx in - (* End the borrows and loans, starting with the borrows *) - let ctx = drop_borrows_loans_at_lplace config p ctx in - (* Read the value and check it *) - let v = read_place_unwrap config access p ctx in - (* Sanity checks *) - assert (not (loans_in_value v)); - assert (not (borrows_in_value v)); - (* Return *) - (ctx, v) - -(** Read the value at a given place. - As long as it is a loan, end the loan. - This function doesn't perform a recursive exploration: - it won't dive into the value to end all the inner - loans (contrary to [drop_borrows_loans_at_lplace] for - instance). - *) -let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - let v = read_place_unwrap config access p ctx in - match v.V.value with - | V.Loan (V.SharedLoan (bids, _)) -> - let ctx = end_outer_borrows config bids ctx in - end_loan_exactly_at_place config access p ctx - | V.Loan (V.MutLoan bid) -> - let ctx = end_outer_borrow config bid ctx in - end_loan_exactly_at_place config access p ctx - | _ -> ctx - -(** Updates the discriminant of a value at a given place. - - There are two situations: - - either the discriminant is already the proper one (in which case we - don't do anything) - - or it is not the proper one (because the variant is not the proper - one, or the value is actually [Bottom] - this happens when - initializing ADT values), in which case we replace the value with - a variant with all its fields set to [Bottom]. - For instance, something like: `Cons Bottom Bottom`. - *) -let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) - (variant_id : T.VariantId.id) : - (C.eval_ctx * statement_eval_res) eval_result = - (* Access the value *) - let access = Write in - let ctx = update_ctx_along_read_place config access p ctx in - let ctx = end_loan_exactly_at_place config access p ctx in - let v = read_place_unwrap config access p ctx in - (* Update the value *) - match (v.V.ty, v.V.value) with - | T.Adt (T.AdtId def_id, regions, types), V.Adt av -> ( - (* There are two situations: - - either the discriminant is already the proper one (in which case we - don't do anything) - - or it is not the proper one, in which case we replace the value with - a variant with all its fields set to [Bottom] - *) - match av.variant_id with - | None -> failwith "Found a struct value while expected an enum" - | Some variant_id' -> - if variant_id' = variant_id then (* Nothing to do *) - Ok (ctx, Unit) - else - (* Replace the value *) - let bottom_v = - compute_expanded_bottom_adt_value ctx.type_context def_id - (Some variant_id) regions types - in - let ctx = write_place_unwrap config access p bottom_v ctx in - Ok (ctx, Unit)) - | T.Adt (T.AdtId def_id, regions, types), V.Bottom -> - let bottom_v = - compute_expanded_bottom_adt_value ctx.type_context def_id - (Some variant_id) regions types - in - let ctx = write_place_unwrap config access p bottom_v ctx in - Ok (ctx, Unit) - | _, V.Symbolic _ -> - assert (config.mode = SymbolicMode); - (* TODO *) raise Unimplemented - | _, (V.Adt _ | V.Bottom) -> failwith "Inconsistent state" - | _, (V.Concrete _ | V.Borrow _ | V.Loan _) -> failwith "Unexpected value" - -(** Push a frame delimiter in the context's environment *) -let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx = - { ctx with env = Frame :: ctx.env } - -(** Drop a value at a given place *) -let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx - = - L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); - (* Prepare the place (by ending the loans, then the borrows) *) - let ctx, v = prepare_lplace config p ctx in - (* Replace the value with [Bottom] *) - let nv = { v with value = V.Bottom } in - let ctx = write_place_unwrap config Write p nv ctx in - ctx - -(** Small helper: compute the type of the return value for a specific - instantiation of a non-local function. - *) -let get_non_local_function_return_type (fid : A.assumed_fun_id) - (region_params : T.erased_region list) (type_params : T.ety list) : T.ety = - match (fid, region_params, type_params) with - | A.BoxNew, [], [ bty ] -> T.Adt (T.Assumed T.Box, [], [ bty ]) - | A.BoxDeref, [], [ bty ] -> T.Ref (T.Erased, bty, T.Shared) - | A.BoxDerefMut, [], [ bty ] -> T.Ref (T.Erased, bty, T.Mut) - | A.BoxFree, [], [ _ ] -> mk_unit_ty - | _ -> failwith "Inconsistent state" - -(** Pop the current frame. - - Drop all the local variables but the return variable, move the return - value out of the return variable, remove all the local variables (but not the - abstractions!) from the context, remove the [Frame] indicator delimiting the - current frame and return the return value and the updated context. - *) -let ctx_pop_frame (config : C.config) (ctx : C.eval_ctx) : - C.eval_ctx * V.typed_value = - (* Debug *) - L.log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx)); - (* Eval *) - let ret_vid = V.VarId.zero in - (* List the local variables, but the return variable *) - let rec list_locals env = - match env with - | [] -> failwith "Inconsistent environment" - | C.Abs _ :: env -> list_locals env - | C.Var (var, _) :: env -> - let locals = list_locals env in - if var.index <> ret_vid then var.index :: locals else locals - | C.Frame :: _ -> [] - in - let locals = list_locals ctx.env in - (* Debug *) - L.log#ldebug - (lazy - ("ctx_pop_frame: locals to drop: [" - ^ String.concat "," (List.map V.VarId.to_string locals) - ^ "]")); - (* Drop the local variables *) - let ctx = - List.fold_left - (fun ctx lid -> drop_value config ctx (mk_place_from_var_id lid)) - ctx locals - in - (* Debug *) - L.log#ldebug - (lazy - ("ctx_pop_frame: after dropping local variables:\n" - ^ eval_ctx_to_string ctx)); - (* Move the return value out of the return variable *) - let ctx, ret_value = - eval_operand config ctx (E.Move (mk_place_from_var_id ret_vid)) - in - (* Pop the frame *) - let rec pop env = - match env with - | [] -> failwith "Inconsistent environment" - | C.Abs abs :: env -> C.Abs abs :: pop env - | C.Var (_, _) :: env -> pop env - | C.Frame :: env -> env - in - let env = pop ctx.env in - let ctx = { ctx with env } in - (ctx, ret_value) - -(** Assign a value to a given place *) -let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) - (p : E.place) : C.eval_ctx = - (* Prepare the destination *) - let ctx, _ = prepare_lplace config p ctx in - (* Update the destination *) - let ctx = write_place_unwrap config Write p v ctx in - ctx - -(** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_new (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = - (* Check and retrieve the arguments *) - match (region_params, type_params, ctx.env) with - | ( [], - [ boxed_ty ], - Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> - (* Required type checking *) - assert (input_value.V.ty = boxed_ty); - - (* Move the input value *) - let ctx, moved_input_value = - eval_operand config ctx - (E.Move (mk_place_from_var_id input_var.C.index)) - in - - (* Create the box value *) - let box_ty = T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) in - let box_v = - V.Adt { variant_id = None; field_values = [ moved_input_value ] } - in - let box_v = mk_typed_value box_ty box_v in - - (* Move this value to the return variable *) - let dest = mk_place_from_var_id V.VarId.zero in - let ctx = assign_to_place config ctx box_v dest in - - (* Return *) - Ok ctx - | _ -> failwith "Inconsistent state" - -(** Auxiliary function which factorizes code to evaluate `std::Deref::deref` - and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *) -let eval_box_deref_mut_or_shared (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx eval_result = - (* Check the arguments *) - match (region_params, type_params, ctx.env) with - | ( [], - [ boxed_ty ], - Var (input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ ) -> ( - (* Required type checking. We must have: - - input_value.ty == & (mut) Box<ty> - - boxed_ty == ty - for some ty - *) - (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in - assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut); - let input_ty = ty_get_box input_ty in - assert (input_ty = boxed_ty)); - - (* Borrow the boxed value *) - let p = - { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] } - in - let borrow_kind = if is_mut then E.Mut else E.Shared in - let rv = E.Ref (p, borrow_kind) in - match eval_rvalue config ctx rv with - | Error err -> Error err - | Ok (ctx, borrowed_value) -> - (* Move the borrowed value to its destination *) - let destp = mk_place_from_var_id V.VarId.zero in - let ctx = assign_to_place config ctx borrowed_value destp in - Ok ctx) - | _ -> failwith "Inconsistent state" - -(** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_deref (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (ctx : C.eval_ctx) : C.eval_ctx eval_result = - let is_mut = false in - eval_box_deref_mut_or_shared config region_params type_params is_mut ctx - -(** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_deref_mut (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (ctx : C.eval_ctx) : C.eval_ctx eval_result = - let is_mut = true in - eval_box_deref_mut_or_shared config region_params type_params is_mut ctx - -(** Auxiliary function - see [eval_non_local_function_call]. - - `Box::free` is not handled the same way as the other assumed functions: - - in the regular case, whenever we need to evaluate an assumed function, - we evaluate the operands, push a frame, call a dedicated function - to correctly update the variables in the frame (and mimic the execution - of a body) and finally pop the frame - - in the case of `Box::free`: the value given to this function is often - of the form `Box(⊥)` because we can move the value out of the - box before freeing the box. It makes it invalid to see box_free as a - "regular" function: it is not valid to call a function with arguments - which contain `⊥`. For this reason, we execute `Box::free` as drop_value, - but this is a bit annoying with regards to the semantics... - - Followingly this function doesn't behave like the others: it does not expect - a stack frame to have been pushed, but rather simply behaves like [drop_value]. - It thus updates the box value (by calling [drop_value]) and updates - the destination (by setting it to `()`). -*) -let eval_box_free (config : C.config) (region_params : T.erased_region list) - (type_params : T.ety list) (args : E.operand list) (dest : E.place) - (ctx : C.eval_ctx) : C.eval_ctx eval_result = - match (region_params, type_params, args) with - | [], [ boxed_ty ], [ E.Move input_box_place ] -> - (* Required type checking *) - let input_box = read_place_unwrap config Write input_box_place ctx in - (let input_ty = ty_get_box input_box.V.ty in - assert (input_ty = boxed_ty)); - - (* Drop the value *) - let ctx = drop_value config ctx input_box_place in - - (* Update the destination by setting it to `()` *) - let ctx = assign_to_place config ctx mk_unit_value dest in - - (* Return *) - Ok ctx - | _ -> failwith "Inconsistent state" - -(** Evaluate a non-local (i.e, assumed) function call such as `Box::deref` - (auxiliary helper for [eval_statement]) *) -let eval_non_local_function_call (config : C.config) (ctx : C.eval_ctx) - (fid : A.assumed_fun_id) (region_params : T.erased_region list) - (type_params : T.ety list) (args : E.operand list) (dest : E.place) : - C.eval_ctx eval_result = - (* Debug *) - L.log#ldebug - (lazy - (let type_params = - "[" - ^ String.concat ", " (List.map (ety_to_string ctx) type_params) - ^ "]" - in - let args = - "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]" - in - let dest = place_to_string ctx dest in - "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid - ^ "\n- type_params: " ^ type_params ^ "\n- args: " ^ args ^ "\n- dest: " - ^ dest)); - - (* There are two cases (and this is extremely annoying): - - the function is not box_free - - the function is box_free - See [eval_box_free] - *) - match fid with - | A.BoxFree -> - (* Degenerate case: box_free *) - eval_box_free config region_params type_params args dest ctx - | _ -> ( - (* "Normal" case: not box_free *) - (* Evaluate the operands *) - let ctx, args_vl = eval_operands config ctx args in - - (* Push the stack frame: we initialize the frame with the return variable, - and one variable per input argument *) - let ctx = ctx_push_frame ctx in - - (* Create and push the return variable *) - let ret_vid = V.VarId.zero in - let ret_ty = - get_non_local_function_return_type fid region_params type_params - in - let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let ctx = C.ctx_push_uninitialized_var ctx ret_var in - - (* Create and push the input variables *) - let input_vars = - V.VarId.mapi_from1 - (fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v)) - args_vl - in - let ctx = C.ctx_push_vars ctx input_vars in - - (* "Execute" the function body. As the functions are assumed, here we call - custom functions to perform the proper manipulations: we don't have - access to a body. *) - let res = - match fid with - | A.BoxNew -> eval_box_new config region_params type_params ctx - | A.BoxDeref -> eval_box_deref config region_params type_params ctx - | A.BoxDerefMut -> - eval_box_deref_mut config region_params type_params ctx - | A.BoxFree -> failwith "Unreachable" - (* should have been treated above *) - in - - (* Check if the function body evaluated correctly *) - match res with - | Error err -> Error err - | Ok ctx -> - (* Pop the stack frame and retrieve the return value *) - let ctx, ret_value = ctx_pop_frame config ctx in - - (* Move the return value to its destination *) - let ctx = assign_to_place config ctx ret_value dest in - - (* Return *) - Ok ctx) - -(** Evaluate a statement *) -let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) - : (C.eval_ctx * statement_eval_res) eval_result = - (* Debugging *) - L.log#ldebug - (lazy - ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate statement: " - ^ statement_to_string ctx st ^ "\n")); - (* Sanity check *) - if config.C.check_invariants then Inv.check_invariants ctx; - (* Evaluate *) - match st with - | A.Assign (p, rvalue) -> ( - (* Evaluate the rvalue *) - match eval_rvalue config ctx rvalue with - | Error err -> Error err - | Ok (ctx, rvalue) -> - (* Assign *) - let ctx = assign_to_place config ctx rvalue p in - Ok (ctx, Unit)) - | A.FakeRead p -> - let ctx, _ = prepare_rplace config Read p ctx in - Ok (ctx, Unit) - | A.SetDiscriminant (p, variant_id) -> - set_discriminant config ctx p variant_id - | A.Drop p -> Ok (drop_value config ctx p, Unit) - | A.Assert assertion -> ( - let ctx, v = eval_operand config ctx assertion.cond in - assert (v.ty = T.Bool); - match v.value with - | Concrete (Bool b) -> - if b = assertion.expected then Ok (ctx, Unit) else Error Panic - | _ -> failwith "Expected a boolean") - | A.Call call -> eval_function_call config ctx call - | A.Panic -> Error Panic - | A.Return -> Ok (ctx, Return) - | A.Break i -> Ok (ctx, Break i) - | A.Continue i -> Ok (ctx, Continue i) - | A.Nop -> Ok (ctx, Unit) - | A.Sequence (st1, st2) -> ( - (* Evaluate the first statement *) - match eval_statement config ctx st1 with - | Error err -> Error err - | Ok (ctx, Unit) -> - (* Evaluate the second statement *) - eval_statement config ctx st2 - (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Ok (ctx, Break i) -> Ok (ctx, Break i) - | Ok (ctx, Continue i) -> Ok (ctx, Continue i) - | Ok (ctx, Return) -> Ok (ctx, Return)) - | A.Loop loop_body -> - (* Evaluate a loop body - - We need a specific function for the [Continue] case: in case we continue, - we might have to reevaluate the current loop body with the new context - (and repeat this an indefinite number of times). - *) - let rec eval_loop_body (ctx : C.eval_ctx) : - (C.eval_ctx * statement_eval_res) eval_result = - (* Evaluate the loop body *) - match eval_statement config ctx loop_body with - | Error err -> Error err - | Ok (ctx, Unit) -> - (* We finished evaluating the statement in a "normal" manner *) - Ok (ctx, Unit) - (* Control-flow breaks *) - | Ok (ctx, Break i) -> - (* Decrease the break index *) - if i = 0 then Ok (ctx, Unit) else Ok (ctx, Break (i - 1)) - | Ok (ctx, Continue i) -> - (* Decrease the continue index *) - if i = 0 then - (* We stop there. When we continue, we go back to the beginning - of the loop: we must thus reevaluate the loop body (and - recheck the result to know whether we must reevaluate again, - etc. *) - eval_loop_body ctx - else (* We don't stop there: transmit *) - Ok (ctx, Continue (i - 1)) - | Ok (ctx, Return) -> Ok (ctx, Return) - in - (* Apply *) - eval_loop_body ctx - | A.Switch (op, tgts) -> ( - (* Evaluate the operand *) - let ctx, op_v = eval_operand config ctx op in - match tgts with - | A.If (st1, st2) -> ( - match op_v.value with - | V.Concrete (V.Bool b) -> - if b then eval_statement config ctx st1 - else eval_statement config ctx st2 - | _ -> failwith "Inconsistent state") - | A.SwitchInt (int_ty, tgts, otherwise) -> ( - match op_v.value with - | V.Concrete (V.Scalar sv) -> ( - assert (sv.V.int_ty = int_ty); - match List.find_opt (fun (sv', _) -> sv = sv') tgts with - | None -> eval_statement config ctx otherwise - | Some (_, tgt) -> eval_statement config ctx tgt) - | _ -> failwith "Inconsistent state")) - -(** Evaluate a function call (auxiliary helper for [eval_statement]) *) -and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) : - (C.eval_ctx * statement_eval_res) eval_result = - (* There are two cases * - - this is a local function, in which case we execute its body - - this is a non-local function, in which case there is a special treatment - *) - let res = - match call.func with - | A.Local fid -> - eval_local_function_call config ctx fid call.region_params - call.type_params call.args call.dest - | A.Assumed fid -> - eval_non_local_function_call config ctx fid call.region_params - call.type_params call.args call.dest - in - match res with Error err -> Error err | Ok ctx -> Ok (ctx, Unit) - -(** Evaluate a local (i.e, not assumed) function call (auxiliary helper for - [eval_statement]) *) -and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) - (fid : A.FunDefId.id) (_region_params : T.erased_region list) - (type_params : T.ety list) (args : E.operand list) (dest : E.place) : - C.eval_ctx eval_result = - (* Retrieve the (correctly instantiated) body *) - let def = C.ctx_lookup_fun_def ctx fid in - match config.mode with - | ConcreteMode -> ( - let tsubst = - Subst.make_type_subst - (List.map (fun v -> v.T.index) def.A.signature.type_params) - type_params - in - let locals, body = Subst.fun_def_substitute_in_body tsubst def in - - (* Evaluate the input operands *) - let ctx, args = eval_operands config ctx args in - assert (List.length args = def.A.arg_count); - - (* Push a frame delimiter *) - let ctx = ctx_push_frame ctx in - - (* Compute the initial values for the local variables *) - (* 1. Push the return value *) - let ret_var, locals = - match locals with - | ret_ty :: locals -> (ret_ty, locals) - | _ -> failwith "Unreachable" - in - let ctx = C.ctx_push_var ctx ret_var (C.mk_bottom ret_var.var_ty) in - - (* 2. Push the input values *) - let input_locals, locals = - Utilities.list_split_at locals def.A.arg_count - in - let inputs = List.combine input_locals args in - (* Note that this function checks that the variables and their values - have the same type (this is important) *) - let ctx = C.ctx_push_vars ctx inputs in - - (* 3. Push the remaining local variables (initialized as [Bottom]) *) - let ctx = C.ctx_push_uninitialized_vars ctx locals in - - (* Execute the function body *) - match eval_function_body config ctx body with - | Error Panic -> Error Panic - | Ok ctx -> - (* Pop the stack frame and retrieve the return value *) - let ctx, ret_value = ctx_pop_frame config ctx in - - (* Move the return value to its destination *) - let ctx = assign_to_place config ctx ret_value dest in - - (* Return *) - Ok ctx) - | SymbolicMode -> raise Unimplemented - -(** Evaluate a statement seen as a function body (auxiliary helper for - [eval_statement]) *) -and eval_function_body (config : C.config) (ctx : C.eval_ctx) - (body : A.statement) : (C.eval_ctx, eval_error) result = - match eval_statement config ctx body with - | Error err -> Error err - | Ok (ctx, res) -> ( - (* Sanity check *) - if config.C.check_invariants then Inv.check_invariants ctx; - match res with - | Unit | Break _ | Continue _ -> failwith "Inconsistent state" - | Return -> Ok ctx) + let ctx = List.fold_left create_abs ctx inst_sg.regions_hierarchy in + (* Split the variables between return var, inputs and remaining locals *) + let ret_var = List.hd fdef.locals in + let input_vars, local_vars = + list_split_at (List.tl fdef.locals) fdef.arg_count + in + (* Push the return variable (initialized with ⊥) *) + let ctx = C.ctx_push_uninitialized_var ctx ret_var in + (* Push the input variables (initialized with symbolic values) *) + let input_values = List.map mk_typed_value_from_symbolic_value input_svs in + let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in + (* Push the remaining local variables (initialized with ⊥) *) + let ctx = C.ctx_push_uninitialized_vars ctx local_vars in + (* Return *) + ctx -module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty - environment - *) - let test_unit_function (type_defs : T.type_def list) + environment. + *) + let test_unit_function (type_context : C.type_context) (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth fun_defs fid in @@ -4377,25 +122,19 @@ module Test = struct assert (fdef.A.arg_count = 0); (* Create the evaluation context *) - let ctx = - { - C.type_context = type_defs; - C.fun_context = fun_defs; - C.type_vars = []; - C.env = []; - C.symbolic_counter = V.SymbolicValueId.generator_zero; - C.borrow_counter = V.BorrowId.generator_zero; - } - in + let ctx = initialize_context type_context fun_defs [] in - (* Put the (uninitialized) local variables *) + (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in (* Evaluate the function *) let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in match eval_function_body config ctx fdef.A.body with - | Error err -> Error err - | Ok _ -> Ok () + | [ Ok _ ] -> Ok () + | [ Error err ] -> Error err + | _ -> + (* We execute the concrete interpreter: there shouldn't be any branching *) + failwith "Unreachable" (** Small helper: return true if the function is a unit function (no parameters, no arguments) - TODO: move *) @@ -4406,14 +145,53 @@ module Test = struct && List.length def.A.signature.inputs = 0 (** Test all the unit functions in a list of function definitions *) - let test_all_unit_functions (type_defs : T.type_def list) + let test_unit_functions (type_defs : T.type_def list) + (fun_defs : A.fun_def list) : unit = + let unit_funs = List.filter fun_def_is_unit fun_defs in + let test_unit_fun (def : A.fun_def) : unit = + let type_ctx = { C.type_defs } in + match test_unit_function type_ctx fun_defs def.A.def_id with + | Error _ -> failwith "Unit test failed (concrete execution)" + | Ok _ -> () + in + List.iter test_unit_fun unit_funs + + (** Execute the symbolic interpreter on a function. *) + let test_function_symbolic (type_context : C.type_context) + (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : + C.eval_ctx eval_result list = + (* Retrieve the function declaration *) + let fdef = A.FunDefId.nth fun_defs fid in + + (* Debug *) + L.log#ldebug + (lazy + ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name)); + + (* Create the evaluation context *) + let ctx = initialize_symbolic_context_for_fun type_context fun_defs fdef in + + (* Evaluate the function *) + let config = { C.mode = C.SymbolicMode; C.check_invariants = true } in + eval_function_body config ctx fdef.A.body + + (** Execute the symbolic interpreter on a list of functions. + + TODO: for now we ignore the functions which contain loops, because + they are not supported by the symbolic interpreter. + *) + let test_functions_symbolic (type_defs : T.type_def list) (fun_defs : A.fun_def list) : unit = + let no_loop_funs = + List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) fun_defs + in let test_fun (def : A.fun_def) : unit = - if fun_def_is_unit def then - match test_unit_function type_defs fun_defs def.A.def_id with - | Error _ -> failwith "Unit test failed" - | Ok _ -> () - else () + let type_ctx = { C.type_defs } in + (* Execute the function - note that as the symbolic interpreter explores + * all the path, some executions are expected to "panic": we thus don't + * check the return value *) + let _ = test_function_symbolic type_ctx fun_defs def.A.def_id in + () in - List.iter test_fun fun_defs + List.iter test_fun no_loop_funs end |