summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-13 23:07:03 +0100
committerSon Ho2022-01-13 23:07:03 +0100
commited9122c7fc73d77aff5768b27c7f432e89a31d96 (patch)
tree3a1b10581b760775753df5da2fa4f207aa5dd9f4 /src
parentbdd80437c084d4b78b439bf6a7b7b138920f0003 (diff)
Make good progress on end_proj_loans_symbolic
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterBorrows.ml32
-rw-r--r--src/InterpreterBorrowsCore.ml145
-rw-r--r--src/Values.ml1
3 files changed, 173 insertions, 5 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index d8c2f3a8..64e82edd 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -421,6 +421,11 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
(* Apply the reborrows *)
apply_registered_reborrows ctx
+(** 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 =
+ raise Errors.Unimplemented
+
(** Auxiliary function to end borrows. See [give_back].
This function is similar to [give_back_value] but gives back an [avalue]
@@ -1130,8 +1135,8 @@ and end_abstraction_remove_from_context (_config : C.config)
let env = List.filter_map map_env_elem ctx.C.env in
{ ctx with C.env }
-(** End the proj_borrows which intersect a given proj_loans over a symbolic
- value.
+(** End a proj_loan over a symbolic value by ending the proj_borrows which
+ intersect this proj_loans.
Rk.:
- if this symbolic value is primitively copiable, then:
@@ -1144,10 +1149,27 @@ and end_abstraction_remove_from_context (_config : C.config)
intersecting proj_borrows, either in the concrete context or in an
abstraction
*)
-and end_proj_loans_symbolic (_config : C.config) (_abs_id : V.AbstractionId.id)
- (_regions : T.RegionId.set_t) (_sv : V.symbolic_value) (_ctx : C.eval_ctx) :
+and end_proj_loans_symbolic (config : C.config) (abs_id : V.AbstractionId.id)
+ (regions : T.RegionId.set_t) (sv : V.symbolic_value) (ctx : C.eval_ctx) :
C.eval_ctx =
- raise Errors.Unimplemented
+ (* 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
+ | 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) ->
+ (* 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
and end_outer_borrow config = end_borrow config None
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index e34a5383..68b24380 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -7,6 +7,7 @@ module V = Values
module C = Contexts
module Subst = Substitute
module L = Logging
+open Utils
open TypesUtils
open InterpreterUtils
@@ -557,3 +558,147 @@ let get_first_outer_loan_or_borrow_in_value (with_borrows : bool)
with
| FoundLoanContent lc -> Some (LoanContent lc)
| FoundBorrowContent bc -> Some (BorrowContent bc)
+
+type gproj_borrows =
+ | AProjBorrows of V.AbstractionId.id * V.symbolic_value
+ | ProjBorrows of V.symbolic_value
+
+let proj_borrows_intersects_proj_loans
+ (proj_borrows : T.RegionId.Set.t * V.symbolic_value * T.rty)
+ (proj_loans : T.RegionId.Set.t * V.symbolic_value) : bool =
+ let b_regions, b_sv, b_ty = proj_borrows in
+ let l_regions, l_sv = proj_loans in
+ if same_symbolic_id b_sv l_sv then
+ 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").
+
+ [explore_shared]: if `true` also explore projectors over shared values,
+ otherwise ignore.
+*)
+let lookup_first_intersecting_aproj_borrows_opt (explore_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
+ in
+ let check_proj_borrows_and_raise 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)
+ else ()
+ in
+ let obj =
+ object
+ inherit [_] C.iter_eval_ctx as super
+
+ method! visit_abs _ abs = super#visit_abs (Some abs) abs
+
+ method! visit_abstract_shared_borrows abs asb =
+ if explore_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
+ in
+ 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) ->
+ check_proj_borrows_and_raise 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
+
+(** Lookup the aproj_borrows (not aproj_borrows_shared!) 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, and the projection type used in
+ this abstraction.
+*)
+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
+ | None -> None
+ | Some (abs_id, rty, is_mut) ->
+ assert is_mut;
+ Some (abs_id, rty)
+
+(** Similar to [lookup_intersecting_aproj_borrows_not_shared_opt], but updates the
+ value.
+ *)
+let update_intersecting_aproj_borrows_not_shared (regions : T.RegionId.Set.t)
+ (sv : V.symbolic_value) (nv : V.typed_avalue) (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
+ 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
+ | 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 ()
+ 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;
+ (* Return *)
+ ctx
diff --git a/src/Values.ml b/src/Values.ml
index 9d25025e..50bec658 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -188,6 +188,7 @@ type aproj =
a shared loan: under a shared loan, we use [abstract_shared_borrow]. *)
| AEndedProjLoans
| AEndedProjBorrows
+(* TODO: remove AEndedProjBorrows? *)
[@@deriving show]
type region = RegionVarId.id Types.region [@@deriving show]