summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-14 23:04:25 +0100
committerSon Ho2022-01-14 23:04:25 +0100
commit47f308eb25475533c1614240ecc4bd5c03bc5b3f (patch)
treefba23522fa403356fd8fd525c4a0b2b187d06f2c /src
parent0e86ecb77a79e791c18861dbc63ae773b2f00d1f (diff)
Fix give_back_symbolic_value
Diffstat (limited to '')
-rw-r--r--src/InterpreterBorrows.ml21
-rw-r--r--src/InterpreterBorrowsCore.ml89
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*)