diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 48 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 100 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 53 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 8 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 53 | ||||
| -rw-r--r-- | src/Invariants.ml | 9 | ||||
| -rw-r--r-- | src/Print.ml | 8 | ||||
| -rw-r--r-- | src/Values.ml | 57 |
10 files changed, 226 insertions, 118 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index d85c4bf8..ae5376f9 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -78,7 +78,9 @@ module Test = struct let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = (* Project over the values - we use *loan* projectors, as explained above *) let avalues = - List.map (mk_aproj_loans_from_symbolic_value abs.regions) input_svs + List.map + (mk_aproj_loans_value_from_symbolic_value abs.regions) + input_svs in (* Insert the avalues in the abstraction *) let abs = { abs with avalues } in diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index ecbfdc05..89543721 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -319,7 +319,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) let abs = Option.get opt_abs in (* The loan projector *) let given_back_loans_proj = - mk_aproj_loans_from_symbolic_value abs.regions sv + mk_aproj_loans_value_from_symbolic_value abs.regions sv in (* Continue giving back in the child value *) let child = super#visit_typed_avalue opt_abs child in @@ -421,11 +421,26 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) (* Apply the reborrows *) apply_registered_reborrows ctx -(** TODO: *) +(** Give back a symbolic value. + + When we give back a symbolic value, we replace the symbolic value with + a new symbolic value if we found an intersecting projection over the + borrows of this symbolic value inside a different abstraction. + Otherwise, we give back the same symbolic value, to signify the fact that + it was left unchanged. + *) let give_back_symbolic_value (_config : C.config) (_regions : T.RegionId.set_t) - (_sv : V.symbolic_value) (_nsv : V.symbolic_value) (_ctx : C.eval_ctx) : + (sv : V.symbolic_value) (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = - raise Errors.Unimplemented + let subst local_regions = + let child_proj = + if sv.sv_id = nsv.sv_id then None + else + Some (mk_aproj_borrows_from_symbolic_value local_regions nsv sv.V.sv_ty) + in + V.AEndedProjLoans child_proj + in + substitute_aproj_loans_with_id sv subst ctx (** Auxiliary function to end borrows. See [give_back]. @@ -983,10 +998,13 @@ and end_abstraction_loans (config : C.config) (abs_id : V.AbstractionId.id) super#visit_AEndedIgnoredMutLoan env given_back child | V.AIgnoredSharedLoan av -> super#visit_AIgnoredSharedLoan env av - method! visit_ASymbolic _ sproj = - match sproj with - | V.AProjBorrows (_, _) | V.AEndedProjLoans | V.AEndedProjBorrows -> () - | V.AProjLoans sv -> raise (FoundSymbolicValue sv) + method! visit_aproj env sproj = + (match sproj with + | V.AProjBorrows (_, _) + | V.AEndedProjLoans _ | V.AEndedProjBorrows | V.AIgnoredProjBorrows -> + () + | V.AProjLoans sv -> raise (FoundSymbolicValue sv)); + super#visit_aproj env sproj end in try @@ -1066,12 +1084,14 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id) (* Nothing to do for ignored borrows *) () - method! visit_ASymbolic _ sproj = - match sproj with + method! visit_aproj env sproj = + (match sproj with | V.AProjLoans _ -> failwith "Unexpected" | V.AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty)) - | V.AEndedProjLoans | V.AEndedProjBorrows -> () + | V.AEndedProjLoans _ | V.AEndedProjBorrows | V.AIgnoredProjBorrows -> + ()); + super#visit_aproj env sproj end in (* Lookup the abstraction *) @@ -1196,11 +1216,9 @@ and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id) * came from first *) if abs_id' = abs_id then (* Replace the proj_borrows *) - let pb_nv = - { V.value = V.ASymbolic V.AEndedProjBorrows; V.ty = sv.V.sv_ty } - in + let npb = V.AEndedProjBorrows in let ctx = - update_intersecting_aproj_borrows_non_shared regions sv pb_nv ctx + update_intersecting_aproj_borrows_non_shared regions sv npb ctx in (* Replace the proj_loans - note that the loaned (symbolic) value * was left unchanged *) diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 18722948..e3789273 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -7,7 +7,6 @@ module V = Values module C = Contexts module Subst = Substitute module L = Logging -open Utils open TypesUtils open InterpreterUtils @@ -575,7 +574,7 @@ let proj_borrows_intersects_proj_loans let proj_loans_intersect (proj_loans : T.RegionId.Set.t * V.symbolic_value) (proj_loans' : T.RegionId.Set.t * V.symbolic_value) : bool = let regions, sv = proj_loans in - let regions', sv' = proj_loans in + let regions', sv' = proj_loans' in if same_symbolic_id sv sv' then projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions' else false @@ -652,13 +651,16 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool) List.iter check asb else () - method! visit_ASymbolic abs sproj = - let abs = Option.get abs in - match sproj with - | AProjLoans _ | AEndedProjLoans | AEndedProjBorrows -> () - | AProjBorrows (sv', proj_rty) -> - let is_shared = true in - check_add_proj_borrows false abs sv' proj_rty + method! visit_aproj abs sproj = + (let abs = Option.get abs in + match sproj with + | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows + | AIgnoredProjBorrows -> + () + | AProjBorrows (sv', proj_rty) -> + let is_shared = false in + check_add_proj_borrows is_shared abs sv' proj_rty); + super#visit_aproj abs sproj end in (* Visit *) @@ -687,13 +689,10 @@ let lookup_intersecting_aproj_borrows_not_shared_opt (** Similar to [lookup_intersecting_aproj_borrows_opt], but updates the values. - - Note that the [update_non_shared] function could return a non-typed value: - we make it typed for sanity checks. *) let update_intersecting_aproj_borrows (can_update_shared : bool) (update_shared : V.AbstractionId.id -> T.rty -> V.abstract_shared_borrows) - (update_non_shared : V.AbstractionId.id -> T.rty -> V.typed_avalue) + (update_non_shared : V.AbstractionId.id -> T.rty -> V.aproj) (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = (* Small helpers for sanity checks *) @@ -742,18 +741,17 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) List.concat (List.map update asb) else asb - method! visit_ASymbolic abs sproj = + method! visit_aproj abs sproj = match sproj with - | AProjLoans _ | AEndedProjLoans | AEndedProjBorrows -> - super#visit_ASymbolic abs sproj + | AProjLoans _ | AEndedProjLoans _ | AEndedProjBorrows + | AIgnoredProjBorrows -> + super#visit_aproj abs sproj | AProjBorrows (sv', proj_rty) -> let abs = Option.get abs in let is_shared = true in - if check_proj_borrows is_shared abs sv' proj_rty then ( - let nv = update_non_shared abs.abs_id proj_rty in - assert (nv.V.ty = sv'.V.sv_ty); - nv.V.value) - else super#visit_ASymbolic (Some abs) sproj + if check_proj_borrows is_shared abs sv' proj_rty then + update_non_shared abs.abs_id proj_rty + else super#visit_aproj (Some abs) sproj end in (* Apply *) @@ -769,8 +767,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool) We check that we update exactly one proj_borrows. *) let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t) - (sv : V.symbolic_value) (nv : V.typed_avalue) (ctx : C.eval_ctx) : - C.eval_ctx = + (sv : V.symbolic_value) (nv : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = (* Small helpers *) let can_update_shared = false in let update_shared _ _ = failwith "Unexpected" in @@ -803,6 +800,7 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) update_intersecting_aproj_borrows can_update_shared update_shared update_non_shared regions sv ctx +(* (** Updates the proj_loans intersecting some projection. Note that in practice, when we update a proj_loans, we always update exactly @@ -813,20 +811,15 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t) for sanity checking: we check whether we need to update a loan based on intersection criteria, but also check at the same time that we update *exactly one* projector. - - Note that the new value [nv] with which to replace the proj_loans could - be untyped: we request a typed value for sanity checking. *) let update_intersecting_aproj_loans (regions : T.RegionId.Set.t) - (sv : V.symbolic_value) (nv : V.typed_avalue) (ctx : C.eval_ctx) : - C.eval_ctx = + (sv : V.symbolic_value) (nv : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = (* Small helpers for sanity checks *) let updated = ref false in - let update ty : V.avalue = + let update () : V.aproj = assert (not !updated); updated := true; - assert (nv.V.ty = ty); - nv.V.value + nv in (* The visitor *) let obj = @@ -835,15 +828,50 @@ let update_intersecting_aproj_loans (regions : T.RegionId.Set.t) method! visit_abs _ abs = super#visit_abs (Some abs) abs - method! visit_ASymbolic abs sproj = + method! visit_aproj abs sproj = match sproj with - | AProjBorrows _ | AEndedProjLoans | AEndedProjBorrows -> - super#visit_ASymbolic abs sproj + | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows -> + super#visit_aproj abs sproj | AProjLoans sv' -> let abs = Option.get abs in if proj_loans_intersect (regions, sv) (abs.regions, sv') then - update sv'.V.sv_ty - else super#visit_ASymbolic (Some abs) sproj + update () + else super#visit_aproj (Some abs) sproj + end + in + (* Apply *) + let ctx = obj#visit_eval_ctx None ctx in + (* Check that we updated the context at least once *) + assert !updated; + (* Return *) + ctx + *) + +(** Substitute the proj_loans based an a symbolic id *) +let substitute_aproj_loans_with_id (sv : V.symbolic_value) + (subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx = + (* Small helpers for sanity checks *) + let updated = ref false in + let update regions : V.aproj = + updated := true; + subst regions + in + (* The visitor *) + let obj = + object + inherit [_] C.map_eval_ctx as super + + method! visit_abs _ abs = super#visit_abs (Some abs) abs + + method! visit_aproj abs sproj = + match sproj with + | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows + | AIgnoredProjBorrows -> + super#visit_aproj abs sproj + | AProjLoans sv' -> + let abs = Option.get abs in + if same_symbolic_id sv sv' then update abs.regions + else super#visit_aproj (Some abs) sproj end in (* Apply *) diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 18ec1ecc..3903ca14 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -60,7 +60,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) in (* Visitor to apply the expansion *) let obj = - object + object (self) inherit [_] C.map_eval_ctx as super method! visit_abs current_abs abs = @@ -70,12 +70,31 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) (** When visiting an abstraction, we remember the regions it owns to be able to properly reduce projectors when expanding symbolic values *) + method! visit_aproj current_abs aproj = + (match aproj with + | AProjLoans sv | AProjBorrows (sv, _) -> + assert (not (same_symbolic_id sv original_sv)) + | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ()); + super#visit_aproj current_abs aproj + (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called + only on child projections (i.e., projections which appear in [AEndedProjLoans]). + The role of visit_aproj is then to check we don't have to expand symbolic + values in child projections, because it should never happen + *) + method! visit_ASymbolic current_abs aproj = let current_abs = Option.get current_abs in let proj_regions = current_abs.regions in let ancestors_regions = current_abs.ancestors_regions in + (* Explore in depth first - we won't update anything: we simply + * want to check we don't have to expand inner symbolic value *) match (aproj, proj_kind) with - | (V.AEndedProjLoans | V.AEndedProjBorrows), _ -> V.ASymbolic aproj + | V.AEndedProjLoans None, _ | V.AEndedProjBorrows, _ -> + V.ASymbolic aproj + | V.AEndedProjLoans (Some child_proj), _ -> + (* Explore the child projection to make sure we don't have to expand + * anything in there *) + V.ASymbolic (self#visit_aproj (Some current_abs) child_proj) | V.AProjLoans sv, LoanProj -> (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then @@ -111,9 +130,11 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config) else (* Not the searched symbolic value: nothing to do *) super#visit_ASymbolic (Some current_abs) aproj - | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj -> + | V.AProjLoans _, BorrowProj + | V.AProjBorrows (_, _), LoanProj + | V.AIgnoredProjBorrows, _ -> (* Nothing to do *) - super#visit_ASymbolic (Some current_abs) aproj + V.ASymbolic aproj end in (* Apply the expansion *) @@ -275,7 +296,7 @@ let expand_symbolic_value_shared_borrow (config : C.config) in (* Visitor to replace the projectors on borrows *) let obj = - object + object (self) inherit [_] C.map_eval_ctx as super method! visit_Symbolic env sv = @@ -302,17 +323,35 @@ let expand_symbolic_value_shared_borrow (config : C.config) let asb = List.concat (List.map expand_asb asb) in V.AProjSharedBorrow asb + method! visit_aproj proj_regions aproj = + (match aproj with + | AProjLoans sv | AProjBorrows (sv, _) -> + assert (not (same_symbolic_id sv original_sv)) + | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ()); + super#visit_aproj proj_regions aproj + (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called + only on child projections (i.e., projections which appear in [AEndedProjLoans]). + The role of visit_aproj is then to check we don't have to expand symbolic + values in child projections, because it should never happen + *) + method! visit_ASymbolic proj_regions aproj = match aproj with + | AEndedProjBorrows | AIgnoredProjBorrows -> + (* We ignore borrows *) V.ASymbolic aproj | AProjLoans _ -> (* Loans are handled later *) - super#visit_ASymbolic proj_regions aproj + V.ASymbolic 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)) - | AEndedProjLoans | AEndedProjBorrows -> V.ASymbolic aproj + | AEndedProjLoans None -> V.ASymbolic aproj + | AEndedProjLoans (Some child_aproj) -> + (* Sanity check: make sure there is nothing to expand inside children + * projections *) + V.ASymbolic (self#visit_aproj proj_regions child_aproj) end in (* Call the visitor *) diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index ad8c8f53..b1c61980 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -303,14 +303,16 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) | 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_symbolic_value regions) field_values + List.map + (mk_aproj_loans_value_from_symbolic_value regions) + field_values in (V.AAdt { V.variant_id; field_values }, original_sv_ty) | SeMutRef (bid, spc), T.Ref (r, ref_ty, T.Mut) -> (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_symbolic_value regions spc in + let child_av = mk_aproj_loans_value_from_symbolic_value regions 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 @@ -323,7 +325,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) (* Sanity check *) assert (spc.V.sv_ty = ref_ty); (* Apply the projector to the borrowed value *) - let child_av = mk_aproj_loans_from_symbolic_value regions spc in + let child_av = mk_aproj_loans_value_from_symbolic_value regions 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 diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 3eb7322b..d13dc515 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -883,7 +883,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) let ret_sv_ty = inst_sg.A.output in let ret_spc = mk_fresh_symbolic_value ret_sv_ty in let ret_value = mk_typed_value_from_symbolic_value ret_spc in - let ret_av regions = mk_aproj_loans_from_symbolic_value regions ret_spc in + let ret_av regions = + mk_aproj_loans_value_from_symbolic_value regions ret_spc + in (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in let args_with_rtypes = List.combine args inst_sg.A.inputs in diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 92c92807..e431aa30 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -67,12 +67,12 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : in av -(** Create a loans projector from a symbolic value. +(** Create a loans projector value from a symbolic value. Checks if the projector will actually project some regions. If not, returns [AIgnored] (`_`). *) -let mk_aproj_loans_from_symbolic_value (regions : T.RegionId.Set.t) +let mk_aproj_loans_value_from_symbolic_value (regions : T.RegionId.Set.t) (svalue : V.symbolic_value) : V.typed_avalue = if ty_has_regions_in_set regions svalue.sv_ty then let av = V.ASymbolic (V.AProjLoans svalue) in @@ -80,6 +80,13 @@ let mk_aproj_loans_from_symbolic_value (regions : T.RegionId.Set.t) av else { V.value = V.AIgnored; ty = svalue.V.sv_ty } +(** Create a borrows projector from a symbolic value *) +let mk_aproj_borrows_from_symbolic_value (proj_regions : T.RegionId.Set.t) + (svalue : V.symbolic_value) (proj_ty : T.rty) : V.aproj = + if ty_has_regions_in_set proj_regions proj_ty then + V.AProjBorrows (svalue, proj_ty) + else V.AIgnoredProjBorrows + (** TODO: move *) let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool = @@ -146,16 +153,17 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : bool = let obj = object - inherit [_] C.iter_eval_ctx + inherit [_] C.iter_eval_ctx as super method! visit_Symbolic _ sv = if sv.V.sv_id = sv_id then raise Found else () - method! visit_ASymbolic _ aproj = - match aproj with + method! visit_aproj env aproj = + (match aproj with | AProjLoans sv | AProjBorrows (sv, _) -> if sv.V.sv_id = sv_id then raise Found else () - | AEndedProjLoans | AEndedProjBorrows -> () + | AEndedProjLoans _ | AEndedProjBorrows | AIgnoredProjBorrows -> ()); + super#visit_aproj env aproj method! visit_abstract_shared_borrows _ asb = let visit (asb : V.abstract_shared_borrow) : unit = @@ -207,36 +215,3 @@ let bottom_in_value (ended_regions : T.RegionId.set_t) (v : V.typed_value) : 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 (ended_regions : T.RegionId.set_t) (v : V.typed_avalue) : - bool = - let obj = - object - inherit [_] V.iter_typed_avalue - - method! visit_Bottom _ = raise Found - - method! visit_symbolic_value _ sv = - if symbolic_value_has_ended_regions 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) -> () - | V.AEndedProjLoans | V.AEndedProjBorrows -> () - end - in - (* We use exceptions *) - try - obj#visit_typed_avalue () v; - false - with Found -> true diff --git a/src/Invariants.ml b/src/Invariants.ml index 73a18312..7664f70e 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -605,7 +605,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = * otherwise they should have been reduced to `_` *) let abs = Option.get info in assert (ty_has_regions_in_set abs.regions sv.V.sv_ty) - | V.AEndedProjLoans | V.AEndedProjBorrows -> ()) + | V.AEndedProjLoans (Some proj) -> ( + match proj with + | V.AProjBorrows (_sv, ty') -> assert (ty' = ty) + | V.AEndedProjBorrows -> () + | _ -> failwith "Unexpected") + | V.AEndedProjLoans None + | V.AEndedProjBorrows | V.AIgnoredProjBorrows -> + ()) | V.AIgnored, _ -> () | _ -> failwith "Erroneous typing"); (* Continue exploring to inspect the subterms *) diff --git a/src/Print.ml b/src/Print.ml index d7830549..d4f051f9 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -307,7 +307,7 @@ module Values = struct ^ String.concat "," (List.map (abstract_shared_borrow_to_string fmt) abs) ^ "}" - let aproj_to_string (fmt : value_formatter) (pv : V.aproj) : string = + let rec aproj_to_string (fmt : value_formatter) (pv : V.aproj) : string = match pv with | AProjLoans sv -> "proj_loans (" @@ -315,8 +315,12 @@ module Values = struct ^ ")" | AProjBorrows (sv, rty) -> "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")" - | AEndedProjLoans -> "ended_proj_loans" + | AEndedProjLoans aproj_opt -> + "ended_proj_loans (" + ^ option_to_string (aproj_to_string fmt) aproj_opt + ^ ")" | AEndedProjBorrows -> "ended_proj_borrows" + | AIgnoredProjBorrows -> "_" let rec typed_avalue_to_string (fmt : value_formatter) (v : V.typed_avalue) : string = diff --git a/src/Values.ml b/src/Values.ml index 50bec658..7ba16ae2 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -181,31 +181,66 @@ type abstract_shared_borrow = type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show] (** A set of abstract shared borrows *) +(** Ancestor for [aproj] iter visitor *) +class ['self] iter_aproj_base = + object (_self : 'self) + inherit [_] iter_typed_value + + method visit_rty : 'env -> rty -> unit = fun _ _ -> () + end + +(** Ancestor for [aproj] map visitor *) +class ['self] map_aproj_base = + object (_self : 'self) + inherit [_] map_typed_value + + method visit_rty : 'env -> rty -> rty = fun _ ty -> ty + end + type aproj = | AProjLoans of symbolic_value | AProjBorrows of symbolic_value * rty (** Note that an AProjBorrows only operates on a value which is not below a shared loan: under a shared loan, we use [abstract_shared_borrow]. *) - | AEndedProjLoans + | AEndedProjLoans of aproj option + (** When ending a proj_loans over a symbolic value, we may need to insert + (and keep track of) a proj_borrows over the given back value, if the + symbolic value was consumed by an abstraction then updated. + *) | AEndedProjBorrows -(* TODO: remove AEndedProjBorrows? *) -[@@deriving show] + (* TODO: remove AEndedProjBorrows? We might need it for synthesis, to contain + * meta values *) + | AIgnoredProjBorrows +[@@deriving + show, + visitors + { + name = "iter_aproj"; + variety = "iter"; + ancestors = [ "iter_aproj_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + }, + visitors + { + name = "map_aproj"; + variety = "map"; + ancestors = [ "map_aproj_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + }] type region = RegionVarId.id Types.region [@@deriving show] (** Ancestor for [typed_avalue] iter visitor *) class ['self] iter_typed_avalue_base = object (_self : 'self) - inherit [_] iter_typed_value + inherit [_] iter_aproj method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> () method visit_region : 'env -> region -> unit = fun _ _ -> () - method visit_aproj : 'env -> aproj -> unit = fun _ _ -> () - - method visit_rty : 'env -> rty -> unit = fun _ _ -> () - method visit_abstract_shared_borrows : 'env -> abstract_shared_borrows -> unit = fun _ _ -> () @@ -214,16 +249,12 @@ class ['self] iter_typed_avalue_base = (** Ancestor for [typed_avalue] map visitor *) class ['self] map_typed_avalue_base = object (_self : 'self) - inherit [_] map_typed_value + inherit [_] map_aproj method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id method visit_region : 'env -> region -> region = fun _ r -> r - method visit_aproj : 'env -> aproj -> aproj = fun _ p -> p - - method visit_rty : 'env -> rty -> rty = fun _ ty -> ty - method visit_abstract_shared_borrows : 'env -> abstract_shared_borrows -> abstract_shared_borrows = fun _ asb -> asb |