summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-14 10:33:02 +0100
committerSon Ho2022-01-14 10:33:02 +0100
commite6ee5e6fda235e71283c6cccecbfc631457cc949 (patch)
tree2972d3ba00a67a0e7a282c292b8cdde536ecde75 /src
parented9122c7fc73d77aff5768b27c7f432e89a31d96 (diff)
Make good progress on end_proj_loans_symbolic
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterBorrows.ml59
-rw-r--r--src/InterpreterBorrowsCore.ml262
2 files changed, 257 insertions, 64 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 64e82edd..ecbfdc05 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -423,7 +423,8 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
(** TODO: *)
let give_back_symbolic_value (_config : C.config) (_regions : T.RegionId.set_t)
- (_sv : V.symbolic_value) (_ctx : C.eval_ctx) : C.eval_ctx =
+ (_sv : V.symbolic_value) (_nsv : V.symbolic_value) (_ctx : C.eval_ctx) :
+ C.eval_ctx =
raise Errors.Unimplemented
(** Auxiliary function to end borrows. See [give_back].
@@ -1154,22 +1155,64 @@ and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id)
C.eval_ctx =
(* Find the first proj_borrows which intersects the proj_loans *)
let explore_shared = true in
- match
- lookup_first_intersecting_aproj_borrows_opt explore_shared regions sv ctx
- with
+ match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with
| None ->
(* We couldn't find any in the context: it means that the symbolic value
* is in the concrete environment (or that we dropped it, in which case
* it is completely absent) *)
(* Update the loans depending on the current symbolic value - it is
* left unchanged *)
- give_back_symbolic_value config regions sv ctx
- | Some (abs_id', proj_ty, mutable_proj) ->
+ give_back_symbolic_value config regions sv sv ctx
+ | Some (SharedProjs projs) ->
+ (* We found projectors over shared values - split between the projectors
+ * which belong to the current *)
+ (* TODO: we might want to allow ending shared projectors/borrows in
+ * abstractions without ending the abstractions themselves, if we end
+ * those abstractions immediately after: some abstractions may be mutually
+ * dependent, which is ok when it is about shared values *)
+ let _owned_projs, external_projs =
+ List.partition (fun (abs_id', _) -> abs_id' = abs_id) projs
+ in
+ if external_projs = [] then
+ (* There are external projs: end the corresponding abstractions *)
+ let abs_ids = List.map fst external_projs in
+ let abs_ids =
+ List.fold_left
+ (fun s id -> V.AbstractionId.Set.add id s)
+ V.AbstractionId.Set.empty abs_ids
+ in
+ let ctx = end_abstractions config abs_ids ctx in
+ (* We could end the owned projections, but it is simpler to simply return
+ * and let the caller recheck if there are proj_loans to end *)
+ ctx
+ else
+ (* 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 regions 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
* came from first *)
- if abs_id' = abs_id then raise Errors.Unimplemented
- else raise Errors.Unimplemented
+ 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 ctx =
+ update_intersecting_aproj_borrows_non_shared regions sv pb_nv ctx
+ in
+ (* Replace the proj_loans - note that the loaned (symbolic) value
+ * was left unchanged *)
+ give_back_symbolic_value config regions sv sv ctx
+ else
+ (* End the abstraction.
+ * Don't retry ending the current proj_loans after ending the abstraction:
+ * it may have been eliminated (if it is a proj over mutable value),
+ * or maybe not (if it is a proj over shared values): simply return,
+ * as the caller function will recheck if there are loans to end in the
+ * current abstraction *)
+ end_abstraction config abs_id' ctx
and end_outer_borrow config = end_borrow config None
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 68b24380..18722948 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -572,37 +572,60 @@ let proj_borrows_intersects_proj_loans
projections_intersect l_sv.V.sv_ty l_regions b_ty b_regions
else false
-(** Lookup the first aproj_borrows (including aproj_shared_borrows) over a
- symbolic value which intersects a given set of regions.
-
- Note that there should be **at most one** (one reason is that we force
- the expansion of primitively copyable values before giving them to
- abstractions).
-
- Returns the id of the owning abstraction, the projection type used in
- this abstraction and a boolean indicating whether the projector is
- over a mutable value (`true` is "mutable", `false` is "shared").
+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.
+
+ Note that because we we force the expansion of primitively copyable values
+ before giving them to abstractions, we only have the following possibilities:
+ - no aproj_borrows, in which case the symbolic value was either dropped
+ or is in the context
+ - exactly one aproj_borrows over a non-shared value
+ - potentially several aproj_borrows over shared values
- [explore_shared]: if `true` also explore projectors over shared values,
+ The result contains the ids of the abstractions in which the projectors were
+ found, as well as the projection types used in those abstractions.
+*)
+type looked_up_aproj_borrows =
+ | NonSharedProj of V.AbstractionId.id * T.rty
+ | SharedProjs of (V.AbstractionId.id * T.rty) list
+
+(** Lookup the aproj_borrows (including aproj_shared_borrows) over a
+ symbolic value which intersect a given set of regions.
+
+ [lookup_shared]: if `true` also explore projectors over shared values,
otherwise ignore.
*)
-let lookup_first_intersecting_aproj_borrows_opt (explore_shared : bool)
+let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
(regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
- (V.AbstractionId.id * T.rty * bool) option =
- let found = ref None in
- let set r =
- assert (Option.is_none !found);
- found := Some r
+ looked_up_aproj_borrows option =
+ let found : looked_up_aproj_borrows option ref = ref None in
+ let set_non_shared ((id, ty) : V.AbstractionId.id * T.rty) : unit =
+ match !found with
+ | None -> found := Some (NonSharedProj (id, ty))
+ | Some _ -> failwith "Unreachable"
in
- let check_proj_borrows_and_raise abs sv' proj_ty =
+ let add_shared (x : V.AbstractionId.id * T.rty) : unit =
+ match !found with
+ | None -> found := Some (SharedProjs [ x ])
+ | Some (SharedProjs pl) -> found := Some (SharedProjs (x :: pl))
+ | Some (NonSharedProj _) -> failwith "Unreachable"
+ in
+ let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty =
if
proj_borrows_intersects_proj_loans
(abs.V.regions, sv', proj_ty)
(regions, sv)
- then (
- let is_mut = false in
- set (abs.abs_id, proj_ty, is_mut);
- raise Found)
+ then
+ let x = (abs.abs_id, proj_ty) in
+ if is_shared then add_shared x else set_non_shared x
else ()
in
let obj =
@@ -612,13 +635,19 @@ let lookup_first_intersecting_aproj_borrows_opt (explore_shared : bool)
method! visit_abs _ abs = super#visit_abs (Some abs) abs
method! visit_abstract_shared_borrows abs asb =
- if explore_shared then
+ (* Sanity check *)
+ (match !found with
+ | Some (NonSharedProj _) -> failwith "Unreachable"
+ | _ -> ());
+ (* Explore *)
+ if lookup_shared then
let abs = Option.get abs in
let check asb =
match asb with
| V.AsbBorrow _ -> ()
| V.AsbProjReborrows (sv', proj_ty) ->
- check_proj_borrows_and_raise abs sv' proj_ty
+ let is_shared = true in
+ check_add_proj_borrows is_shared abs sv' proj_ty
in
List.iter check asb
else ()
@@ -628,17 +657,14 @@ let lookup_first_intersecting_aproj_borrows_opt (explore_shared : bool)
match sproj with
| AProjLoans _ | AEndedProjLoans | AEndedProjBorrows -> ()
| AProjBorrows (sv', proj_rty) ->
- check_proj_borrows_and_raise abs sv' proj_rty
+ let is_shared = true in
+ check_add_proj_borrows false abs sv' proj_rty
end
in
- (* We use exceptions *)
- try
- obj#visit_eval_ctx None ctx;
- None
- with Found ->
- (* Return - while checking that the result is indeed `Some ...` *)
- let res = Option.get !found in
- Some res
+ (* Visit *)
+ obj#visit_eval_ctx None ctx;
+ (* Return *)
+ !found
(** Lookup the aproj_borrows (not aproj_borrows_shared!) over a symbolic
value which intersects a given set of regions.
@@ -653,27 +679,42 @@ let lookup_first_intersecting_aproj_borrows_opt (explore_shared : bool)
let lookup_intersecting_aproj_borrows_not_shared_opt
(regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
(V.AbstractionId.id * T.rty) option =
- let explore_shared = false in
- match
- lookup_first_intersecting_aproj_borrows_opt explore_shared regions sv ctx
- with
+ let lookup_shared = false in
+ match lookup_intersecting_aproj_borrows_opt lookup_shared regions sv ctx with
| None -> None
- | Some (abs_id, rty, is_mut) ->
- assert is_mut;
- Some (abs_id, rty)
+ | Some (NonSharedProj (abs_id, rty)) -> Some (abs_id, rty)
+ | _ -> failwith "Unexpected"
-(** Similar to [lookup_intersecting_aproj_borrows_not_shared_opt], but updates the
- value.
+(** 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_not_shared (regions : T.RegionId.Set.t)
- (sv : V.symbolic_value) (nv : V.typed_avalue) (ctx : C.eval_ctx) :
+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)
+ (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
C.eval_ctx =
- (* Small helpers to make sure we update the context exactly once *)
- let found = ref false in
- let set () : V.avalue =
- assert (not !found);
- found := true;
- nv.V.value
+ (* Small helpers for sanity checks *)
+ let shared = ref None in
+ let add_shared () =
+ match !shared with None -> shared := Some true | Some b -> assert b
+ in
+ let set_non_shared () =
+ match !shared with
+ | None -> shared := Some false
+ | Some _ -> failwith "Found unexpected intersecting proj_borrows"
+ in
+ let check_proj_borrows is_shared abs sv' proj_ty =
+ if
+ proj_borrows_intersects_proj_loans
+ (abs.V.regions, sv', proj_ty)
+ (regions, sv)
+ then (
+ if is_shared then add_shared () else set_non_shared ();
+ true)
+ else false
in
(* The visitor *)
let obj =
@@ -682,23 +723,132 @@ let update_intersecting_aproj_borrows_not_shared (regions : T.RegionId.Set.t)
method! visit_abs _ abs = super#visit_abs (Some abs) abs
+ method! visit_abstract_shared_borrows abs asb =
+ (* Sanity check *)
+ (match !shared with Some b -> assert b | _ -> ());
+ (* Explore *)
+ if can_update_shared then
+ let abs = Option.get abs in
+ let update (asb : V.abstract_shared_borrow) :
+ V.abstract_shared_borrows =
+ match asb with
+ | V.AsbBorrow _ -> [ asb ]
+ | V.AsbProjReborrows (sv', proj_ty) ->
+ let is_shared = true in
+ if check_proj_borrows is_shared abs sv' proj_ty then
+ update_shared abs.abs_id proj_ty
+ else [ asb ]
+ in
+ List.concat (List.map update asb)
+ else asb
+
method! visit_ASymbolic abs sproj =
match sproj with
| AProjLoans _ | AEndedProjLoans | AEndedProjBorrows ->
super#visit_ASymbolic abs sproj
| AProjBorrows (sv', proj_rty) ->
let abs = Option.get abs in
- if
- proj_borrows_intersects_proj_loans
- (abs.regions, sv', proj_rty)
- (regions, sv)
- then set ()
+ 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
+ end
+ in
+ (* Apply *)
+ let ctx = obj#visit_eval_ctx None ctx in
+ (* Check that we updated the context at least once *)
+ assert (Option.is_some !shared);
+ (* Return *)
+ ctx
+
+(** Simply calls [update_intersecting_aproj_borrows] to update a
+ proj_borrows over a non-shared value.
+
+ 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 =
+ (* Small helpers *)
+ let can_update_shared = false in
+ let update_shared _ _ = failwith "Unexpected" in
+ let updated = ref false in
+ let update_non_shared _ _ =
+ assert (not !updated);
+ updated := true;
+ nv
+ in
+ (* Update *)
+ let ctx =
+ update_intersecting_aproj_borrows can_update_shared update_shared
+ update_non_shared regions sv ctx
+ in
+ (* Check that we updated at least once *)
+ assert !updated;
+ (* Return *)
+ ctx
+
+(** Simply calls [update_intersecting_aproj_borrows] to remove the
+ proj_borrows over shared values.
+ *)
+let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
+ (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
+ (* Small helpers *)
+ let can_update_shared = true in
+ let update_shared _ _ = [] in
+ let update_non_shared _ _ = failwith "Unexpected" in
+ (* Update *)
+ 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
+ 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.
+ *)
+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 =
+ (* Small helpers for sanity checks *)
+ let updated = ref false in
+ let update ty : V.avalue =
+ assert (not !updated);
+ updated := true;
+ assert (nv.V.ty = ty);
+ nv.V.value
+ 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_ASymbolic abs sproj =
+ match sproj with
+ | AProjBorrows _ | AEndedProjLoans | AEndedProjBorrows ->
+ super#visit_ASymbolic 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
end
in
(* Apply *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check that we updated the context at least once *)
- assert !found;
+ assert !updated;
(* Return *)
ctx