diff options
Diffstat (limited to '')
| -rw-r--r-- | TODO.md | 2 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 32 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 145 | ||||
| -rw-r--r-- | src/Values.ml | 1 |
4 files changed, 175 insertions, 5 deletions
@@ -7,6 +7,8 @@ (but always disallow borrow overwrites on returned values) at the level of abstractions (not at the level of loans!) +* check that no borrow_overwrites upon ending abstractions + * set of types with mutable borrows (what to do when type variables appear under shared borrows?) necessary to know what to return. 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] |