From c794ffc73738393850fc257a7916d0fd2c87d87f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 10:21:39 +0100 Subject: Move some functions from Interpreter to InterpreterProjectors --- src/Interpreter.ml | 637 +------------------------------------------ src/InterpreterProjectors.ml | 505 ++++++++++++++++++++++++++++++++++ src/InterpreterUtils.ml | 160 +++++++++++ 3 files changed, 667 insertions(+), 635 deletions(-) create mode 100644 src/InterpreterProjectors.ml diff --git a/src/Interpreter.ml b/src/Interpreter.ml index a3f22660..afe513be 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -10,9 +10,10 @@ module L = Logging open TypesUtils open ValuesUtils module Inv = Invariants -open InterpreterUtils module S = Synthesis open Utils +open InterpreterUtils +open InterpreterProjectors (* TODO: check that the value types are correct when evaluating *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere @@ -34,450 +35,6 @@ type eval_error = Panic type 'a eval_result = ('a, eval_error) result -(** 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 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 } - -(** 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 @@ -672,196 +229,6 @@ let end_borrow_get_borrow (io : inner_outer) 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) - -let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) - (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : - C.eval_ctx * V.typed_avalue = - let check_symbolic_no_ended = true in - let allow_reborrows = true in - (* Prepare the reborrows *) - let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows ctx - in - (* Apply the projector *) - let av = - apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty - in - (* Apply the reborrows *) - let ctx = apply_registered_reborrows ctx in - (* Return *) - (ctx, av) - (** Auxiliary function to end borrows. See [give_back]. When we end a mutable borrow, we need to "give back" the value it contained diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml new file mode 100644 index 00000000..9c99f8c9 --- /dev/null +++ b/src/InterpreterProjectors.ml @@ -0,0 +1,505 @@ +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 +module S = Synthesis +open Utils +open InterpreterUtils + +(** 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 } + +(** 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. 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). + This function is used when applying projectors on shared borrows: when + doing so, we might need to reborrow subvalues from the shared value. + For instance: + ``` + fn f<'a,'b,'c>(x : &'a 'b 'c u32) + ``` + When introducing the abstractions for 'a, 'b and 'c, we apply a projector + on some value `shared_borrow l : &'a &'b &'c u32`. + In the 'a abstraction, this shared borrow gets projected. However, when + reducing the projectors for the 'b and 'c abstractions, we need to make + sure that the borrows living in regions 'b and 'c live as long as those + regions. This is done by looking up the shared value and applying reborrows + on the borrows we find there (note that those reborrows apply on shared + borrows - easy - and mutable borrows - in this case, we reborrow the whole + borrow: `mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)`). +*) +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) + +let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) + (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : + C.eval_ctx * V.typed_avalue = + let check_symbolic_no_ended = true in + let allow_reborrows = true in + (* Prepare the reborrows *) + let fresh_reborrow, apply_registered_reborrows = + prepare_reborrows config allow_reborrows ctx + in + (* Apply the projector *) + let av = + apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow regions v ty + in + (* Apply the reborrows *) + let ctx = apply_registered_reborrows ctx in + (* Return *) + (ctx, av) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index edc8594c..c652a1d3 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -632,3 +632,163 @@ type symbolic_expansion = | 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 + +(** 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 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 *) -- cgit v1.2.3