diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrows.ml | 21 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 89 |
2 files changed, 86 insertions, 24 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 19e5716f..cde799d8 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -429,19 +429,18 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) 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) (sv : V.symbolic_value) +let give_back_symbolic_value (_config : C.config) + (proj_regions : T.RegionId.set_t) (proj_ty : T.rty) (sv : V.symbolic_value) (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = - let subst local_regions = + let subst local_regions local_ty = 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) + Some (mk_aproj_borrows_from_symbolic_value local_regions nsv local_ty) in V.AEndedProjLoans child_proj in - (* TODO: we need to use the regions!! *) - raise Errors.Unimplemented; - substitute_aproj_loans_with_id sv subst ctx + update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx (** Auxiliary function to end borrows. See [give_back]. @@ -1150,7 +1149,9 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) in (* Give back a fresh symbolic value *) let nsv = mk_fresh_symbolic_value proj_ty in - let ctx = give_back_symbolic_value config sv nsv ctx in + let ctx = + give_back_symbolic_value config abs.regions proj_ty sv nsv ctx + in (* Reexplore *) end_abstraction_borrows config chain abs_id ctx @@ -1195,7 +1196,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) * it is completely absent) *) (* Update the loans depending on the current symbolic value - it is * left unchanged *) - give_back_symbolic_value config sv sv ctx + give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx | Some (SharedProjs projs) -> (* We found projectors over shared values - split between the projectors * which belong to the current *) @@ -1222,7 +1223,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) (* All the proj_borrows are owned: simply erase them *) let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in (* Remove the proj_loans - note that the symbolic value was left unchanged *) - give_back_symbolic_value config sv sv ctx + give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx | Some (NonSharedProj (abs_id', _proj_ty)) -> (* We found one in the context: if it comes from this abstraction, we can * end it directly, otherwise we need to end the abstraction where it @@ -1235,7 +1236,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) in (* Replace the proj_loans - note that the loaned (symbolic) value * was left unchanged *) - give_back_symbolic_value config sv sv ctx + give_back_symbolic_value config regions sv.V.sv_ty sv sv ctx else (* End the abstraction. * Don't retry ending the current proj_loans after ending the abstraction: diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 3c39e76b..6bc31d63 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -596,14 +596,6 @@ let proj_borrows_intersects_proj_loans projections_intersect l_sv.V.sv_ty l_regions b_ty b_regions else false -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 - if same_symbolic_id sv sv' then - projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions' - else false - (** Result of looking up aproj_borrows which intersect a given aproj_loans in the context. @@ -825,14 +817,33 @@ 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 -(** 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 = +(** Updates the proj_loans intersecting some projection. + + Note that in practice, when we update a proj_loans, we always update exactly + one aproj_loans, in a specific abstraction. + + We make this function more general, by checking projection intersections + (rather than simply checking the abstraction and symbolic value ids) + 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. + + [subst]: takes as parameters the projection regions and the projection type + where we perform the substitution. + *) +let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t) + (proj_ty : T.rty) (sv : V.symbolic_value) + (subst : T.RegionId.Set.t -> T.rty -> V.aproj) (ctx : C.eval_ctx) : + C.eval_ctx = (* Small helpers for sanity checks *) let updated = ref false in - let update regions : V.aproj = + let update local_regions local_proj_ty : V.aproj = + assert (not !updated); updated := true; - subst regions + subst local_regions local_proj_ty in (* The visitor *) let obj = @@ -848,7 +859,13 @@ let substitute_aproj_loans_with_id (sv : V.symbolic_value) super#visit_aproj abs sproj | AProjLoans sv' -> let abs = Option.get abs in - if same_symbolic_id sv sv' then update abs.regions + if same_symbolic_id sv sv' then ( + assert (sv.sv_ty = sv'.sv_ty); + if + projections_intersect proj_ty proj_regions sv'.V.sv_ty + abs.regions + then update abs.regions sv'.V.sv_ty + else super#visit_aproj (Some abs) sproj) else super#visit_aproj (Some abs) sproj end in @@ -858,3 +875,47 @@ let substitute_aproj_loans_with_id (sv : V.symbolic_value) assert !updated; (* Return *) ctx + +(* +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 + if same_symbolic_id sv sv' then + projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions' + else false + +*) +(*(** 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 *) + let ctx = obj#visit_eval_ctx None ctx in + (* Check that we updated the context at least once *) + assert !updated; + (* Return *) + ctx*) |