summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/InterpreterBorrows.ml647
-rw-r--r--compiler/InterpreterBorrows.mli84
-rw-r--r--compiler/InterpreterBorrowsCore.ml14
-rw-r--r--compiler/InterpreterLoops.ml566
-rw-r--r--compiler/InterpreterUtils.ml13
-rw-r--r--compiler/Values.ml2
-rw-r--r--compiler/ValuesUtils.ml18
7 files changed, 1104 insertions, 240 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 28caf6e6..d20a02a2 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -444,7 +444,7 @@ let give_back_symbolic_value (_config : C.config)
| V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
->
()
- | FunCallRet | SynthInput | Global | LoopOutput ->
+ | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin ->
raise (Failure "Unrechable"));
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in
@@ -1573,8 +1573,9 @@ let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) :
"Can't activate a reserved mutable borrow referencing a loan inside\n\
\ an abstraction")
-let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (ctx : C.eval_ctx)
- (abs0 : V.abs) : V.abs =
+let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
+ (destructure_shared_values : bool) (ctx : C.eval_ctx) (abs0 : V.abs) : V.abs
+ =
(* Accumulator to store the destructured values *)
let avalues = ref [] in
(* Utility function to store a value in the accumulator *)
@@ -1602,10 +1603,21 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (ctx : C.eval_ctx)
| V.ASharedLoan (bids, sv, child_av) ->
(* We don't support nested borrows for now *)
assert (not (value_has_borrows ctx sv.V.value));
+ (* Destructure the shared value *)
+ let avl, sv =
+ if destructure_shared_values then list_values sv else ([], sv)
+ in
(* Push a value *)
let ignored = mk_aignored child_av.V.ty in
let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
push { V.value; ty };
+ (* Push the avalues introduced because we decomposed the inner loans -
+ note that we pay attention to the order in which we introduce
+ the avalues: we want to push them *after* the outer loan. If we
+ didn't want that, we would have implemented [list_values] in
+ exactly the same way as [list_avalues] (i.e., with a similar
+ signature) *)
+ List.iter push avl;
(* Explore the child *)
list_avalues false push_fail child_av
| V.AMutLoan (bid, child_av) ->
@@ -1660,19 +1672,62 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (ctx : C.eval_ctx)
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
assert (not (ty_has_borrows ctx.type_context.type_infos ty))
+ and list_values (v : V.typed_value) : V.typed_avalue list * V.typed_value =
+ let ty = v.V.ty in
+ match v.V.value with
+ | Primitive _ -> ([], v)
+ | Adt adt ->
+ let avll, field_values =
+ List.split (List.map list_values adt.field_values)
+ in
+ let avl = List.concat avll in
+ let adt = { adt with V.field_values } in
+ (avl, { v with V.value = Adt adt })
+ | Bottom -> raise (Failure "Unreachable")
+ | Borrow _ ->
+ (* We don't support nested borrows for now *)
+ raise (Failure "Unreachable")
+ | Loan lc -> (
+ match lc with
+ | SharedLoan (bids, sv) ->
+ let avl, sv = list_values sv in
+ if destructure_shared_values then
+ (* Rem.: the shared value can't contain loans nor borrows *)
+ let rty = ety_no_regions_to_rty ty in
+ let av : V.typed_avalue =
+ assert (not (value_has_loans_or_borrows ctx sv.V.value));
+ let value =
+ V.ALoan (V.ASharedLoan (bids, sv, mk_aignored rty))
+ in
+ { V.value; ty = rty }
+ in
+ let avl = List.append avl [ av ] in
+ (avl, sv)
+ else (avl, { v with V.value = V.Loan (V.SharedLoan (bids, sv)) })
+ | MutLoan _ -> raise (Failure "Unreachable"))
+ | Symbolic _ ->
+ (* For now, we fore all symbolic values containing borrows to be eagerly
+ expanded *)
+ assert (not (ty_has_borrows ctx.type_context.type_infos ty));
+ ([], v)
in
+
(* Destructure the avalues *)
List.iter (list_avalues true push_avalue) abs0.V.avalues;
let avalues = List.rev !avalues in
(* Update *)
{ abs0 with V.avalues; kind = abs_kind; can_end }
-let abs_is_destructured (ctx : C.eval_ctx) (abs : V.abs) : bool =
- let abs' = destructure_abs abs.kind abs.can_end ctx abs in
+let abs_is_destructured (destructure_shared_values : bool) (ctx : C.eval_ctx)
+ (abs : V.abs) : bool =
+ let abs' =
+ destructure_abs abs.kind abs.can_end destructure_shared_values ctx abs
+ in
abs = abs'
let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
- (ctx : C.eval_ctx) (v : V.typed_value) : V.abs list =
+ (destructure_shared_values : bool) (ctx : C.eval_ctx) (v : V.typed_value) :
+ V.abs list =
(* Convert the value to a list of avalues *)
let absl = ref [] in
let push_abs (r_id : T.RegionId.id) (avalues : V.typed_avalue list) : unit =
@@ -1697,32 +1752,52 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
absl := abs :: !absl
in
- (* [group]: group in one abstraction (because we dived into a borrow/loan) *)
- let rec to_avalues (allow_borrows : bool) (group : bool)
- (r_id : T.RegionId.id) (v : V.typed_value) : V.typed_avalue list =
+ (* [group]: group in one abstraction (because we dived into a borrow/loan)
+
+ We return one typed-value for the shared values: when we encounter a shared
+ loan, we need to compute the value which will be shared. If [destructure_shared_values]
+ is [true], this shared value will be stripped of its shared loans.
+ *)
+ let rec to_avalues (allow_borrows : bool) (inside_borrowed : bool)
+ (group : bool) (r_id : T.RegionId.id) (v : V.typed_value) :
+ V.typed_avalue list * V.typed_value =
let ty = v.V.ty in
match v.V.value with
- | V.Primitive _ -> []
+ | V.Primitive _ -> ([], v)
| V.Bottom ->
(* Can happen: we *do* convert dummy values to abstractions, and dummy
values can contain bottoms *)
- []
+ ([], v)
| V.Adt adt ->
(* Two cases, depending on whether we have to group all the borrows/loans
inside one abstraction or not *)
- if group then
- (* Convert to avalues, and transmit to the parent *)
- List.concat
- (List.map (to_avalues allow_borrows group r_id) adt.field_values)
- else (
- (* Create one abstraction per field, and transmit nothing to the parent *)
- List.iter
- (fun fv ->
- let r_id = C.fresh_region_id () in
- let values = to_avalues allow_borrows group r_id fv in
- push_abs r_id values)
- adt.field_values;
- [])
+ let avl, field_values =
+ if group then
+ (* Convert to avalues, and transmit to the parent *)
+ let avl, field_values =
+ List.split
+ (List.map
+ (to_avalues allow_borrows inside_borrowed group r_id)
+ adt.field_values)
+ in
+ (List.concat avl, field_values)
+ else
+ (* Create one abstraction per field, and transmit nothing to the parent *)
+ let field_values =
+ List.map
+ (fun fv ->
+ let r_id = C.fresh_region_id () in
+ let avl, fv =
+ to_avalues allow_borrows inside_borrowed group r_id fv
+ in
+ push_abs r_id avl;
+ fv)
+ adt.field_values
+ in
+ ([], field_values)
+ in
+ let adt = { adt with field_values } in
+ (avl, { v with V.value = V.Adt adt })
| V.Borrow bc -> (
let _, ref_ty, kind = ty_as_ref ty in
(* Sanity check *)
@@ -1733,21 +1808,30 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
let ref_ty = ety_no_regions_to_rty ref_ty in
let ty = T.Ref (T.Var r_id, ref_ty, kind) in
let value = V.ABorrow (V.ASharedBorrow bid) in
- [ { V.value; ty } ]
+ ([ { V.value; ty } ], v)
| MutBorrow (bid, bv) ->
let r_id = if group then r_id else C.fresh_region_id () in
(* We don't support nested borrows for now *)
assert (not (value_has_borrows ctx bv.V.value));
- (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+ (* We don't allow shared borrows inside mutably borrowed values -
+ note that destructuring those is unsoud: if we immutably borrow
+ a value inside a mutably borrowed value, we have to make sure
+ the immutably borrowed value isn't modified for as long as the
+ immutable borrow lives. In case of shared values it is not
+ a problem, because this is enforced by the outer shared loan. *)
+ assert (not (value_has_loans bv.V.value));
+ (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
let mv = bv in
let ref_ty = ety_no_regions_to_rty ref_ty in
let ty = T.Ref (T.Var r_id, ref_ty, kind) in
let ignored = mk_aignored ref_ty in
- let value = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
- let value = { V.value; ty } in
+ let av = V.ABorrow (V.AMutBorrow (mv, bid, ignored)) in
+ let av = { V.value = av; ty } in
(* Continue exploring, looking for loans (and forbidding borrows,
because we don't support nested borrows for now) *)
- value :: to_avalues false true r_id bv
+ let avl, bv = to_avalues false true true r_id bv in
+ let value = { v with V.value = V.Borrow (V.MutBorrow (bid, bv)) } in
+ (av :: avl, value)
| ReservedMutBorrow _ ->
(* This borrow should have been activated *)
raise (Failure "Unexpected"))
@@ -1758,58 +1842,134 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
(* We don't support nested borrows for now *)
assert (not (value_has_borrows ctx sv.V.value));
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+ (* For avalues, a loan has the borrow type *)
let ty = ety_no_regions_to_rty ty in
+ let ty = mk_ref_ty (T.Var r_id) ty T.Shared in
let ignored = mk_aignored ty in
- let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
- let value = { V.value; ty } in
+ (* Rem.: the shared value might contain loans *)
+ let avl, sv = to_avalues false true true r_id sv in
+ let av = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
+ let av = { V.value = av; ty } in
(* Continue exploring, looking for loans (and forbidding borrows,
because we don't support nested borrows for now) *)
- value :: to_avalues false true r_id sv
+ let value : V.value =
+ if destructure_shared_values then sv.V.value
+ else V.Loan (V.SharedLoan (bids, sv))
+ in
+ let value = { v with V.value } in
+ (av :: avl, value)
| V.MutLoan bid ->
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
+ (* For avalues, a loan has the borrow type *)
let ty = ety_no_regions_to_rty ty in
+ let ty = mk_ref_ty (T.Var r_id) ty T.Mut in
let ignored = mk_aignored ty in
- let value = V.ALoan (V.AMutLoan (bid, ignored)) in
- [ { V.value; ty } ])
+ let av = V.ALoan (V.AMutLoan (bid, ignored)) in
+ let av = { V.value = av; ty } in
+ ([ av ], v))
| V.Symbolic _ ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
assert (not (value_has_borrows ctx v.V.value));
(* Return nothing *)
- []
+ ([], v)
in
(* Generate the avalues *)
let r_id = C.fresh_region_id () in
- let values = to_avalues true false r_id v in
+ let values, _ = to_avalues true false false r_id v in
(* Introduce an abstraction for the returned values *)
push_abs r_id values;
(* Return *)
List.rev !absl
-let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
- (ctx : C.eval_ctx) (abs0 : V.abs) (abs1 : V.abs) : V.abs =
- (* Check that the abstractions are destructured *)
- if !Config.check_invariants then (
- assert (abs_is_destructured ctx abs0);
- assert (abs_is_destructured ctx abs1));
+type borrow_or_loan_id = BorrowId of V.borrow_id | LoanId of V.loan_id
+
+type g_loan_content_with_ty =
+ (T.ety * V.loan_content, T.rty * V.aloan_content) concrete_or_abs
+
+type g_borrow_content_with_ty =
+ (T.ety * V.borrow_content, T.rty * V.aborrow_content) concrete_or_abs
+
+type merge_abstraction_info = {
+ loans : V.loan_id_set;
+ borrows : V.borrow_id_set;
+ borrows_loans : borrow_or_loan_id list;
+ (** We use a list to preserve the order in which the borrows were found *)
+ loan_to_content : g_loan_content_with_ty V.BorrowId.Map.t;
+ borrow_to_content : g_borrow_content_with_ty V.BorrowId.Map.t;
+}
- (* Visit the abstractions, list their borrows and loans *)
- let borrows = ref V.BorrowId.Set.empty in
- let loans = ref V.BorrowId.Set.empty in
+(** Small utility to help merging abstractions.
- let push_loans ids = loans := V.BorrowId.Set.union !loans ids in
- let push_loan id = loans := V.BorrowId.Set.add id !loans in
- let push_borrow id = borrows := V.BorrowId.Set.add id !borrows in
+ We compute the list of loan/borrow contents, maps from borrow/loan ids
+ to borrow/loan contents, etc.
+
+ Note that this function is very specific to [merge_abstractions]: we
+ have strong assumptions about the shape of the abstraction, and in
+ particular that:
+ - its values don't contain nested borrows
+ - all the borrows are destructured (for instance, shared loans can't
+ contain shared loans).
+ *)
+let compute_merge_abstractions_info (ctx : C.eval_ctx) (abs : V.abs) :
+ merge_abstraction_info =
+ let loans : V.loan_id_set ref = ref V.BorrowId.Set.empty in
+ let borrows : V.borrow_id_set ref = ref V.BorrowId.Set.empty in
+ let borrows_loans : borrow_or_loan_id list ref = ref [] in
+ let loan_to_content : g_loan_content_with_ty V.BorrowId.Map.t ref =
+ ref V.BorrowId.Map.empty
+ in
+ let borrow_to_content : g_borrow_content_with_ty V.BorrowId.Map.t ref =
+ ref V.BorrowId.Map.empty
+ in
+
+ let push_loans ids (lc : g_loan_content_with_ty) : unit =
+ assert (V.BorrowId.Set.disjoint !loans ids);
+ loans := V.BorrowId.Set.union !loans ids;
+ V.BorrowId.Set.iter
+ (fun id ->
+ assert (not (V.BorrowId.Map.mem id !loan_to_content));
+ loan_to_content := V.BorrowId.Map.add id lc !loan_to_content;
+ borrows_loans := LoanId id :: !borrows_loans)
+ ids
+ in
+ let push_loan id (lc : g_loan_content_with_ty) : unit =
+ assert (not (V.BorrowId.Set.mem id !loans));
+ loans := V.BorrowId.Set.add id !loans;
+ assert (not (V.BorrowId.Map.mem id !loan_to_content));
+ loan_to_content := V.BorrowId.Map.add id lc !loan_to_content;
+ borrows_loans := LoanId id :: !borrows_loans
+ in
+ let push_borrow id (bc : g_borrow_content_with_ty) : unit =
+ assert (not (V.BorrowId.Set.mem id !borrows));
+ borrows := V.BorrowId.Set.add id !borrows;
+ assert (not (V.BorrowId.Map.mem id !borrow_to_content));
+ borrow_to_content := V.BorrowId.Map.add id bc !borrow_to_content;
+ borrows_loans := BorrowId id :: !borrows_loans
+ in
let iter_avalues =
object
inherit [_] V.iter_typed_avalue as super
+ (** We redefine this to track the types *)
+ method! visit_typed_avalue _ v =
+ super#visit_typed_avalue (Some (Abstract v.V.ty)) v
+
+ (** We redefine this to track the types *)
+ method! visit_typed_value _ (v : V.typed_value) =
+ super#visit_typed_value (Some (Concrete v.V.ty)) v
+
method! visit_loan_content env lc =
(* Can happen if we explore shared values whose sub-values are
reborrowed *)
+ let ty =
+ match Option.get env with
+ | Concrete ty -> ty
+ | Abstract _ -> raise (Failure "Unreachable")
+ in
(match lc with
- | SharedLoan (bids, _) -> push_loans bids
+ | SharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
| MutLoan _ -> raise (Failure "Unreachable"));
(* Continue *)
super#visit_loan_content env lc
@@ -1820,10 +1980,15 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
raise (Failure "Unreachable")
method! visit_aloan_content env lc =
+ let ty =
+ match Option.get env with
+ | Concrete _ -> raise (Failure "Unreachable")
+ | Abstract ty -> ty
+ in
(* Register the loans *)
(match lc with
- | V.ASharedLoan (bids, _, _) -> push_loans bids
- | V.AMutLoan (bid, _) -> push_loan bid
+ | V.ASharedLoan (bids, _, _) -> push_loans bids (Abstract (ty, lc))
+ | V.AMutLoan (bid, _) -> push_loan bid (Abstract (ty, lc))
| V.AEndedMutLoan _ | V.AEndedSharedLoan _ | V.AIgnoredMutLoan _
| V.AEndedIgnoredMutLoan _ | V.AIgnoredSharedLoan _ ->
(* The abstraction has been destructured, so those shouldn't appear *)
@@ -1832,14 +1997,19 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
super#visit_aloan_content env lc
method! visit_aborrow_content env bc =
+ let ty =
+ match Option.get env with
+ | Concrete _ -> raise (Failure "Unreachable")
+ | Abstract ty -> ty
+ in
(* Explore the borrow content *)
(match bc with
- | V.AMutBorrow (_, bid, _) -> push_borrow bid
- | V.ASharedBorrow bid -> push_borrow bid
+ | V.AMutBorrow (_, bid, _) -> push_borrow bid (Abstract (ty, bc))
+ | V.ASharedBorrow bid -> push_borrow bid (Abstract (ty, bc))
| V.AProjSharedBorrow asb ->
let register asb =
match asb with
- | V.AsbBorrow bid -> push_borrow bid
+ | V.AsbBorrow bid -> push_borrow bid (Abstract (ty, bc))
| V.AsbProjReborrows _ ->
(* Can only happen if the symbolic value (potentially) contains
borrows - i.e., we have nested borrows *)
@@ -1854,131 +2024,290 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
method! visit_symbolic_value _ _ =
(* Sanity check *)
- raise (Failure "Unrechable")
+ raise (Failure "Unreachable")
end
in
- List.iter (iter_avalues#visit_typed_avalue ()) abs0.V.avalues;
- List.iter (iter_avalues#visit_typed_avalue ()) abs1.V.avalues;
+ List.iter (iter_avalues#visit_typed_avalue None) abs.V.avalues;
+
+ {
+ loans = !loans;
+ borrows = !borrows;
+ borrows_loans = List.rev !borrows_loans;
+ loan_to_content = !loan_to_content;
+ borrow_to_content = !borrow_to_content;
+ }
+
+type merge_duplicates_funcs = {
+ merge_amut_borrows :
+ V.borrow_id ->
+ T.rty ->
+ V.mvalue ->
+ V.typed_avalue ->
+ T.rty ->
+ V.mvalue ->
+ V.typed_avalue ->
+ V.typed_avalue;
+ merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+ merge_amut_loans :
+ V.loan_id ->
+ T.rty ->
+ V.typed_avalue ->
+ T.rty ->
+ V.typed_avalue ->
+ V.typed_avalue;
+ merge_ashared_loans :
+ V.loan_id_set ->
+ T.rty ->
+ V.typed_value ->
+ T.rty ->
+ V.typed_value ->
+ V.typed_avalue;
+}
+
+let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
+ (merge_funs : merge_duplicates_funcs option) (ctx : C.eval_ctx)
+ (abs0 : V.abs) (abs1 : V.abs) : V.abs =
+ (* Check that the abstractions are destructured *)
+ if !Config.check_invariants then (
+ let destructure_shared_values = true in
+ assert (abs_is_destructured destructure_shared_values ctx abs0);
+ assert (abs_is_destructured destructure_shared_values ctx abs1));
+
+ (* Compute the relevant information *)
+ let {
+ loans = loans0;
+ borrows = borrows0;
+ borrows_loans = borrows_loans0;
+ loan_to_content = loan_to_content0;
+ borrow_to_content = borrow_to_content0;
+ } =
+ compute_merge_abstractions_info ctx abs0
+ in
- (* List the values, ignoring the loans/borrows which whose associated
- borrows/loans are in the other abstraction already - note that we
- take advantage of the fact that the values are destructured.
+ let {
+ loans = loans1;
+ borrows = borrows1;
+ borrows_loans = borrows_loans1;
+ loan_to_content = loan_to_content1;
+ borrow_to_content = borrow_to_content1;
+ } =
+ compute_merge_abstractions_info ctx abs1
+ in
- We convert the loans/borrows we want to ignore to [Ignored] values,
- then filter them.
+ (* Sanity check: there is no loan/borrows which appears in both abstractions,
+ unless we allow to merge duplicates *)
+ if merge_funs = None then (
+ assert (V.BorrowId.Set.disjoint borrows0 borrows1);
+ assert (V.BorrowId.Set.disjoint loans0 loans1));
+
+ (* Merge.
+ There are several cases:
+ - if a borrow/loan is only in one abstraction, we simply check if we need
+ to filter it (because its associated loan/borrow is in the other
+ abstraction).
+ - if a borrow/loan is present in both abstractions, we need to merge its
+ content.
+
+ Note that it is possible that we may need to merge strictly more than 2 avalues,
+ because of shared loans. For instance, if we have:
+ {[
+ abs'0 { shared_loan { l0, l1 } ... }
+ abs'1 { shared_loan { l0 } ..., shared_loan { l1 } ... }
+ ]}
+
+ We ignore this case for now: we check that whenever we merge two shared loans,
+ then their sets of ids are equal.
*)
- let intersect = V.BorrowId.Set.inter !loans !borrows in
- let filter_bids (bids : V.BorrowId.Set.t) : V.BorrowId.Set.t option =
+ let merged_borrows = ref V.BorrowId.Set.empty in
+ let merged_loans = ref V.BorrowId.Set.empty in
+ let avalues = ref [] in
+ let push_avalue av = avalues := av :: !avalues in
+
+ let intersect =
+ V.BorrowId.Set.union
+ (V.BorrowId.Set.inter loans0 borrows1)
+ (V.BorrowId.Set.inter loans1 borrows0)
+ in
+ let filter_bids (bids : V.BorrowId.Set.t) : V.BorrowId.Set.t =
let bids = V.BorrowId.Set.diff bids intersect in
- if V.BorrowId.Set.is_empty bids then None else Some bids
+ assert (not (V.BorrowId.Set.is_empty bids));
+ bids
in
let filter_bid (bid : V.BorrowId.id) : V.BorrowId.id option =
if V.BorrowId.Set.mem bid intersect then None else Some bid
in
- let map_avalues =
- object (self : 'self)
- inherit [_] V.map_typed_avalue as super
-
- method! visit_Loan env lc =
- (* Can happen if we explore shared values whose sub-values are
- reborrowed *)
- match lc with
- | SharedLoan (bids, sv) -> (
- match filter_bids bids with
- | None -> (self#visit_typed_value env sv).V.value
- | Some bids -> super#visit_Loan env (SharedLoan (bids, sv)))
- | MutLoan _ -> raise (Failure "Unreachable")
+ let borrow_is_merged id = V.BorrowId.Set.mem id !merged_borrows in
+ let set_borrow_as_merged id =
+ merged_borrows := V.BorrowId.Set.add id !merged_borrows
+ in
+ let loan_is_merged id = V.BorrowId.Set.mem id !merged_loans in
+ let set_loan_as_merged id =
+ merged_loans := V.BorrowId.Set.add id !merged_loans
+ in
- method! visit_borrow_content _ _ =
- (* Can happen if we explore shared values which contain borrows -
- i.e., if we have nested borrows (we forbid this for now) *)
+ (* Some utility functions *)
+ (* Merge two aborrow contents - note that those contents must have the same id *)
+ let merge_aborrow_contents (ty0 : T.rty) (bc0 : V.aborrow_content)
+ (ty1 : T.rty) (bc1 : V.aborrow_content) : V.typed_avalue =
+ match (bc0, bc1) with
+ | V.AMutBorrow (mv0, id, child0), V.AMutBorrow (mv1, _, child1) ->
+ (Option.get merge_funs).merge_amut_borrows id ty0 mv0 child0 ty1 mv1
+ child1
+ | ASharedBorrow id, ASharedBorrow _ ->
+ (Option.get merge_funs).merge_ashared_borrows id ty0 ty1
+ | AProjSharedBorrow _, AProjSharedBorrow _ ->
+ (* Unreachable because requires nested borrows *)
raise (Failure "Unreachable")
+ | _ ->
+ (* Unreachable because those cases are ignored (ended/ignored borrows)
+ or inconsistent *)
+ raise (Failure "Unreachable")
+ in
- method! visit_ALoan env lc =
- (* Register the loans *)
- match lc with
- | V.ASharedLoan (bids, sv, asv) -> (
- match filter_bids bids with
- | None ->
- let sv = super#visit_typed_value env sv in
- assert (is_aignored asv.V.value);
- (* Check if the shared value contains loans or borrows - rem.: there shouldn't
- be borrows actually, because for now we forbid nested borrows.
-
- If it doesn't, we can ignore the value altogether.
- *)
- if
- loans_in_value sv
- || ty_has_borrows ctx.type_context.type_infos sv.V.ty
- then
- (* The value is not shared anymore, but it contains shared sub-values.
-
- It would be good to deconstruct the sub-values. For now, let's fail
- (rem.: it would be sound to have a shared aloan with an empty set
- of borrow ids).
- *)
- raise (Failure "Unimplemented")
- else V.AIgnored
- | Some bids -> super#visit_ALoan env (ASharedLoan (bids, sv, asv)))
- | V.AMutLoan (bid, child) -> (
- assert (is_aignored child.V.value);
- match filter_bid bid with
- | None -> V.AIgnored
- | Some _ -> super#visit_ALoan env lc)
- | V.AEndedMutLoan _ | V.AEndedSharedLoan _ | V.AIgnoredMutLoan _
- | V.AEndedIgnoredMutLoan _ | V.AIgnoredSharedLoan _ ->
- (* The abstraction has been destructured, so those shouldn't appear *)
- raise (Failure "Unreachable")
-
- method! visit_ABorrow env bc =
- (* Explore the borrow content *)
- match bc with
- | V.AMutBorrow (_, bid, child) -> (
- assert (is_aignored child.V.value);
- match filter_bid bid with
- | None -> V.AIgnored
- | Some _ -> super#visit_ABorrow env bc)
- | V.ASharedBorrow bid -> (
- match filter_bid bid with
- | None -> V.AIgnored
- | Some _ -> super#visit_ABorrow env bc)
- | V.AProjSharedBorrow asb ->
- let filter asb =
- match asb with
- | V.AsbBorrow bid -> (
- match filter_bid bid with None -> None | Some _ -> Some asb)
- | V.AsbProjReborrows _ ->
- (* Can only happen if the symbolic value (potentially) contains
- borrows - i.e., we have nested borrows *)
- raise (Failure "Unreachable")
- in
- let asb = List.filter_map filter asb in
- V.ABorrow (V.AProjSharedBorrow asb)
- | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
- | V.AEndedMutBorrow _ | V.AEndedSharedBorrow ->
- (* The abstraction has been destructured, so those shouldn't appear *)
- raise (Failure "Unreachable")
-
- method! visit_symbolic_value _ _ =
- (* Sanity check *)
- raise (Failure "Unrechable")
- end
+ let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
+ (bc1 : g_borrow_content_with_ty) : V.typed_avalue =
+ match (bc0, bc1) with
+ | Concrete (ty0, bc0), Concrete (ty1, bc1) ->
+ (* This can happen only in case of nested borrows *)
+ raise (Failure "Unreachable")
+ | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
+ merge_aborrow_contents ty0 bc0 ty1 bc1
+ | Concrete _, Abstract _ | Abstract _, Concrete _ ->
+ (* TODO: is it really unreachable? *)
+ raise (Failure "Unreachable")
in
- (* Apply the transformation *)
- let avalues =
- List.map
- (map_avalues#visit_typed_avalue ())
- (List.append abs0.avalues abs1.avalues)
+ let merge_aloan_contents (ty0 : T.rty) (lc0 : V.aloan_content) (ty1 : T.rty)
+ (lc1 : V.aloan_content) : V.typed_avalue =
+ match (lc0, lc1) with
+ | V.AMutLoan (id, child0), V.AMutLoan (_, child1) ->
+ (* Register the loan id *)
+ set_loan_as_merged id;
+ (* Merge *)
+ (Option.get merge_funs).merge_amut_loans id ty0 child0 ty1 child1
+ | ASharedLoan (ids0, sv0, child0), ASharedLoan (ids1, sv1, child1) ->
+ (* Filter the ids *)
+ let ids0 = filter_bids ids0 in
+ let ids1 = filter_bids ids1 in
+ (* Check that the sets of ids are the same - if it is not the case, it
+ means we actually need to merge more than 2 avalues: we ignore this
+ case for now *)
+ assert (ids0 = ids1);
+ let ids = ids0 in
+ assert (not (V.BorrowId.Set.is_empty ids));
+ (* Register the loan ids *)
+ V.BorrowId.Set.iter set_loan_as_merged ids;
+ (* Merge *)
+ (Option.get merge_funs).merge_ashared_loans ids ty0 sv0 ty1 sv1
+ | _ ->
+ (* Unreachable because those cases are ignored (ended/ignored borrows)
+ or inconsistent *)
+ raise (Failure "Unreachable")
in
- (* Filter the ignored values *)
- let avalues =
- List.filter (fun (v : V.typed_avalue) -> not (is_aignored v.value)) avalues
+ (* Note that because we may filter ids from a set of id, this function has
+ to register the merged loan ids: the caller doesn't do it (contrary to
+ the borrow case) *)
+ let merge_g_loan_contents (lc0 : g_loan_content_with_ty)
+ (lc1 : g_loan_content_with_ty) : V.typed_avalue =
+ match (lc0, lc1) with
+ | Concrete _, Concrete _ ->
+ (* This can not happen: the values should have been destructured *)
+ raise (Failure "Unreachable")
+ | Abstract (ty0, lc0), Abstract (ty1, lc1) ->
+ merge_aloan_contents ty0 lc0 ty1 lc1
+ | Concrete _, Abstract _ | Abstract _, Concrete _ ->
+ (* TODO: is it really unreachable? *)
+ raise (Failure "Unreachable")
in
+ let borrows_loans = List.append borrows_loans0 borrows_loans1 in
+ (* Iterate over all the borrows/loans ids found in teh abstractions *)
+ List.iter
+ (fun bl ->
+ match bl with
+ | BorrowId bid -> (
+ (* Check if the borrow has already been merged *)
+ assert (not (borrow_is_merged bid));
+ set_borrow_as_merged bid;
+ (* Check if we need to filter it *)
+ match filter_bid bid with
+ | None -> ()
+ | Some bid ->
+ (* Lookup the contents *)
+ let bc0 = V.BorrowId.Map.find_opt bid borrow_to_content0 in
+ let bc1 = V.BorrowId.Map.find_opt bid borrow_to_content1 in
+ (* Merge *)
+ let av : V.typed_avalue =
+ match (bc0, bc1) with
+ | None, Some bc | Some bc, None -> (
+ match bc with
+ | Concrete (_, _) ->
+ (* This can happen only in case of nested borrows -
+ a concrete borrow can only happen inside a shared
+ loan
+ *)
+ raise (Failure "Unreachable")
+ | Abstract (ty, bc) -> { V.value = V.ABorrow bc; ty })
+ | Some bc0, Some bc1 ->
+ assert (merge_funs <> None);
+ merge_g_borrow_contents bc0 bc1
+ | None, None -> raise (Failure "Unreachable")
+ in
+ push_avalue av)
+ | LoanId bid -> (
+ if
+ (* Check if the loan has already been treated - it can happen
+ because shared loans contain sets of borrows.
+ *)
+ loan_is_merged bid
+ then ()
+ else
+ (* Check if we need to filter it *)
+ match filter_bid bid with
+ | None -> ()
+ | Some bid ->
+ (* Lookup the contents *)
+ let lc0 = V.BorrowId.Map.find_opt bid loan_to_content0 in
+ let lc1 = V.BorrowId.Map.find_opt bid loan_to_content1 in
+ (* Merge *)
+ let av : V.typed_avalue =
+ match (lc0, lc1) with
+ | None, Some lc | Some lc, None -> (
+ match lc with
+ | Concrete _ ->
+ (* This shouldn't happen because the avalues should
+ have been destructured. *)
+ raise (Failure "Unreachable")
+ | Abstract (ty, lc) -> (
+ match lc with
+ | V.ASharedLoan (bids, sv, child) ->
+ let bids = filter_bids bids in
+ assert (not (V.BorrowId.Set.is_empty bids));
+ assert (is_aignored child.V.value);
+ assert (
+ not (value_has_loans_or_borrows ctx sv.V.value));
+ let lc = V.ASharedLoan (bids, sv, child) in
+ { V.value = V.ALoan lc; ty }
+ | V.AMutLoan _ -> { V.value = V.ALoan lc; ty }
+ | V.AEndedMutLoan _ | V.AEndedSharedLoan _
+ | V.AIgnoredMutLoan _ | V.AEndedIgnoredMutLoan _
+ | V.AIgnoredSharedLoan _ ->
+ (* The abstraction has been destructured, so those shouldn't appear *)
+ raise (Failure "Unreachable")))
+ | Some lc0, Some lc1 ->
+ assert (merge_funs <> None);
+ merge_g_loan_contents lc0 lc1
+ | None, None -> raise (Failure "Unreachable")
+ in
+ push_avalue av))
+ borrows_loans;
+
+ (* Reverse the values *)
+ let avalues = List.rev !avalues in
+
(* Create the new abstraction *)
let abs_id = C.fresh_abstraction_id () in
(* Note that one of the two abstractions might a parent of the other *)
@@ -2005,6 +2334,6 @@ let merge_abstractions (abs_kind : V.abs_kind) (can_end : bool)
}
in
(* Sanity check *)
- if !Config.check_invariants then assert (abs_is_destructured ctx abs);
+ if !Config.check_invariants then assert (abs_is_destructured true ctx abs);
(* Return *)
abs
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 0d1be9c2..8b8b76d9 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -70,21 +70,37 @@ val promote_reserved_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
]}
Rem.: we do this to simplify the merging of abstractions. We can do this
- because for now, we don't support nested borrows.
+ because for now we don't support nested borrows. In order to implement
+ support for nested borrows, we will probably need to maintain the structure
+ of the avalues.
Paramters:
- [abs_kind]
- [can_end]
+ - [destructure_shared_values]: if [true], explore shared values and whenever we find
+ a shared loan, move it elsewhere by replacing it with the same value without
+ the shared loan, and adding another ashared loan in the abstraction.
+ For instance:
+ {[
+ ML {l0} (0, ML {l1} 1)
+
+ ~~>
+
+ ML {l0} (0, 1)
+ ML {l1} 1
+ ]}
- [ctx]
- [abs]
*)
-val destructure_abs : V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs
+val destructure_abs : V.abs_kind -> bool -> bool -> C.eval_ctx -> V.abs -> V.abs
(** Return [true] if the values in an abstraction are destructured.
We simply destructure it and check that it gives the identity.
+
+ The input boolean is [destructure_shared_value]. See {!destructure_abs}.
*)
-val abs_is_destructured : C.eval_ctx -> V.abs -> bool
+val abs_is_destructured : bool -> C.eval_ctx -> V.abs -> bool
(** Turn a value into a abstractions.
@@ -104,20 +120,54 @@ val abs_is_destructured : C.eval_ctx -> V.abs -> bool
Parameters:
- [abs_kind]
- [can_end]
+ - [destructure_shared_values]: this is similar to [destructure_shared_values]
+ for {!destructure_abs}.
- [ctx]
- [v]
*)
val convert_value_to_abstractions :
- V.abs_kind -> bool -> C.eval_ctx -> V.typed_value -> V.abs list
+ V.abs_kind -> bool -> bool -> C.eval_ctx -> V.typed_value -> V.abs list
+
+(** See {!merge_abstractions}.
+
+ Rem.: it may be more idiomatic to have a functor, but this seems a bit
+ heavyweight, though.
+ *)
+type merge_duplicates_funcs = {
+ merge_amut_borrows :
+ V.borrow_id ->
+ T.rty ->
+ V.mvalue ->
+ V.typed_avalue ->
+ T.rty ->
+ V.mvalue ->
+ V.typed_avalue ->
+ V.typed_avalue;
+ merge_ashared_borrows : V.borrow_id -> T.rty -> T.rty -> V.typed_avalue;
+ merge_amut_loans :
+ V.loan_id ->
+ T.rty ->
+ V.typed_avalue ->
+ T.rty ->
+ V.typed_avalue ->
+ V.typed_avalue;
+ merge_ashared_loans :
+ V.loan_id_set ->
+ T.rty ->
+ V.typed_value ->
+ T.rty ->
+ V.typed_value ->
+ V.typed_avalue;
+}
(** Merge two abstractions together.
- Merging two abstractions together implies removing the loans/borrows
+ When we merge two abstractions together, we remove the loans/borrows
which appear in one and whose associated loans/borrows appear in the
other. For instance:
{[
- abs'0 { mut_borrow l0, mut_loan l1 }
- abs'1 { mut_borrow l1, mut_borrow l2 }
+ abs'0 { mut_borrow l0, mut_loan l1 } // Rem.: mut_loan l1
+ abs'1 { mut_borrow l1, mut_borrow l2 } // Rem.: mut_borrow l1
~~>
@@ -127,9 +177,27 @@ val convert_value_to_abstractions :
Parameters:
- [kind]
- [can_end]
+ - [merge_funs]: in the case it can happen that a loan or a borrow appears in
+ both abstractions, we use those functions to merge the different occurrences
+ (such things can happen when joining environments: we might temporarily
+ duplicate borrows during the join, before merging those borrows together).
+ For instance, this happens for the following abstractions is forbidden:
+ {[
+ abs'0 { mut_borrow l0, mut_loan l1 } // mut_borrow l0 !
+ abs'1 { mut_borrow l0, mut_loan l2 } // mut_borrow l0 !
+ ]}
+ If you want to forbid this, provide [None]. In that case, [merge_abstractions]
+ actually simply performs some sort of a union.
+
- [ctx]
- [abs0]
- [abs1]
*)
val merge_abstractions :
- V.abs_kind -> bool -> C.eval_ctx -> V.abs -> V.abs -> V.abs
+ V.abs_kind ->
+ bool ->
+ merge_duplicates_funcs option ->
+ C.eval_ctx ->
+ V.abs ->
+ V.abs ->
+ V.abs
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 8d23e4da..54949d3f 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -617,6 +617,20 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
None
with FoundLoanContent lc -> Some lc
+(** Return the first loan we find in a list of values *)
+let get_first_loan_in_values (vs : V.typed_value list) : V.loan_content option =
+ let obj =
+ object
+ inherit [_] V.iter_typed_value
+ method! visit_loan_content _ lc = raise (FoundLoanContent lc)
+ end
+ in
+ (* We use exceptions *)
+ try
+ List.iter (obj#visit_typed_value ()) vs;
+ None
+ with FoundLoanContent lc -> Some lc
+
(** Return the first borrow we find in a value *)
let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option =
let obj =
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 08607deb..002abfb5 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -49,11 +49,11 @@ let mk_match_ctx (ctx : C.eval_ctx) : match_ctx =
{ ctx; aids; sids; bids }
type updt_env_kind =
- | EndAbsInSrc of V.AbstractionId.id
- | EndBorrowsInSrc of V.BorrowId.Set.t
- | EndBorrowInSrc of V.BorrowId.id
- | EndBorrowInTgt of V.BorrowId.id
- | EndBorrowsInTgt of V.BorrowId.Set.t
+ | AbsInLeft of V.AbstractionId.id
+ | LoanInLeft of V.BorrowId.id
+ | LoansInLeft of V.BorrowId.Set.t
+ | LoanInRight of V.BorrowId.id
+ | LoansInRight of V.BorrowId.Set.t
(** Utility exception *)
exception ValueMatchFailure of updt_env_kind
@@ -63,43 +63,87 @@ type joined_ctx_or_update = (match_ctx, updt_env_kind) result
(** Union Find *)
module UnionFind = UF.Make (UF.StoreMap)
-(** A small utility *)
+(** A small utility -
+
+ Rem.: some environments may be ill-formed (they may contain several times
+ the same loan or borrow - this happens for instance when merging
+ environments). This is the reason why we use sets in some places (for
+ instance, [borrow_to_abs] maps to a *set* of ids).
+*)
type abs_borrows_loans_maps = {
abs_ids : V.AbstractionId.id list;
abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t;
abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
- borrow_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
- loan_to_abs : V.AbstractionId.id V.BorrowId.Map.t;
+ abs_to_borrows_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
+ borrow_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
+ loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
+ borrow_loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
}
(** Compute various maps linking the abstractions and the borrows/loans they contain.
The [explore] function is used to filter abstractions.
+
+ [no_duplicates] checks that borrows/loans are not referenced more than once
+ (see the documentation for {!abs_borrows_loans_maps}).
*)
-let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
- abs_borrows_loans_maps =
+let compute_abs_borrows_loans_maps (no_duplicates : bool)
+ (explore : V.abs -> bool) (env : C.env) : abs_borrows_loans_maps =
let abs_ids = ref [] in
let abs_to_borrows = ref V.AbstractionId.Map.empty in
let abs_to_loans = ref V.AbstractionId.Map.empty in
+ let abs_to_borrows_loans = ref V.AbstractionId.Map.empty in
let borrow_to_abs = ref V.BorrowId.Map.empty in
let loan_to_abs = ref V.BorrowId.Map.empty in
+ let borrow_loan_to_abs = ref V.BorrowId.Map.empty in
+ let module R (Id0 : Identifiers.Id) (Id1 : Identifiers.Id) = struct
+ (*
+ [check_singleton_sets]: check that the mapping maps to a singletong.
+ [check_not_already_registered]: check if the mapping was not already registered.
+ *)
+ let register_mapping (check_singleton_sets : bool)
+ (check_not_already_registered : bool) (map : Id1.Set.t Id0.Map.t ref)
+ (id0 : Id0.id) (id1 : Id1.id) : unit =
+ (* Sanity check *)
+ (if check_singleton_sets || check_not_already_registered then
+ match Id0.Map.find_opt id0 !map with
+ | None -> ()
+ | Some set ->
+ assert (
+ (not check_not_already_registered) || not (Id1.Set.mem id1 set)));
+ (* Update the mapping *)
+ map :=
+ Id0.Map.update id0
+ (fun ids ->
+ match ids with
+ | None -> Some (Id1.Set.singleton id1)
+ | Some ids ->
+ (* Sanity check *)
+ assert (not check_singleton_sets);
+ assert (
+ (not check_not_already_registered)
+ || not (Id1.Set.mem id1 ids));
+ (* Update *)
+ Some (Id1.Set.add id1 ids))
+ !map
+ end in
+ let module RAbsBorrow = R (V.AbstractionId) (V.BorrowId) in
+ let module RBorrowAbs = R (V.BorrowId) (V.AbstractionId) in
let register_borrow_id abs_id bid =
- abs_to_borrows :=
- V.AbstractionId.Map.update abs_id
- (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
- !abs_to_borrows;
- assert (not (V.BorrowId.Map.mem bid !borrow_to_abs));
- borrow_to_abs := V.BorrowId.Map.add bid abs_id !borrow_to_abs
+ RAbsBorrow.register_mapping false no_duplicates abs_to_borrows abs_id bid;
+ RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid;
+ RBorrowAbs.register_mapping no_duplicates no_duplicates borrow_to_abs bid
+ abs_id;
+ RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id
in
let register_loan_id abs_id bid =
- abs_to_loans :=
- V.AbstractionId.Map.update abs_id
- (fun bids -> Some (V.BorrowId.Set.add bid (Option.get bids)))
- !abs_to_loans;
- assert (not (V.BorrowId.Map.mem bid !loan_to_abs));
- loan_to_abs := V.BorrowId.Map.add bid abs_id !loan_to_abs
+ RAbsBorrow.register_mapping false no_duplicates abs_to_loans abs_id bid;
+ RAbsBorrow.register_mapping false false abs_to_borrows_loans abs_id bid;
+ RBorrowAbs.register_mapping no_duplicates no_duplicates loan_to_abs bid
+ abs_id;
+ RBorrowAbs.register_mapping false false borrow_loan_to_abs bid abs_id
in
let explore_abs =
@@ -159,8 +203,10 @@ let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
abs_ids = List.rev !abs_ids;
abs_to_borrows = !abs_to_borrows;
abs_to_loans = !abs_to_loans;
+ abs_to_borrows_loans = !abs_to_borrows_loans;
borrow_to_abs = !borrow_to_abs;
loan_to_abs = !loan_to_abs;
+ borrow_loan_to_abs = !borrow_loan_to_abs;
}
(** Collapse an environment.
@@ -178,11 +224,19 @@ let compute_abs_borrows_loans_maps (explore : V.abs -> bool) (env : C.env) :
merge them.
In effect, this allows us to merge newly introduced abstractions/borrows
with their parent abstractions.
+
+ [merge_funs]: those are used to merge loans or borrows which appear in both
+ abstractions (rem.: here we mean that, for instance, both abstractions
+ contain a shared loan with id l0).
+ This can happen when merging environments (note that such environments are not well-formed -
+ they become well formed again after collapsing).
*)
-let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
+let collapse_ctx (loop_id : V.LoopId.id)
+ (merge_funs : merge_duplicates_funcs option) (thresh : cnt_thresholds)
(ctx0 : C.eval_ctx) : C.eval_ctx =
let abs_kind = V.Loop loop_id in
- let can_end = true in
+ let can_end = false in
+ let destructure_shared_values = true in
let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
V.AbstractionId.Ord.compare thresh.aid id >= 0
in
@@ -201,7 +255,8 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
| C.Var (DummyBinder id, v) ->
if is_fresh_did id then
let absl =
- convert_value_to_abstractions abs_kind can_end ctx0 v
+ convert_value_to_abstractions abs_kind can_end
+ destructure_shared_values ctx0 v
in
List.map (fun abs -> C.Abs abs) absl
else [ ee ])
@@ -210,18 +265,28 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
(* Explore all the *new* abstractions, and compute various maps *)
let explore (abs : V.abs) = is_fresh_abs_id abs.abs_id in
- let ids_maps = compute_abs_borrows_loans_maps explore env in
+ let ids_maps =
+ compute_abs_borrows_loans_maps (merge_funs = None) explore env
+ in
let {
abs_ids;
abs_to_borrows;
abs_to_loans = _;
+ abs_to_borrows_loans;
borrow_to_abs = _;
loan_to_abs;
+ borrow_loan_to_abs;
} =
ids_maps
in
- (* Use the maps to merge the abstractions together *)
+ (* Change the merging behaviour depending on the input parameters *)
+ let abs_to_borrows, loan_to_abs =
+ if merge_funs <> None then (abs_to_borrows_loans, borrow_loan_to_abs)
+ else (abs_to_borrows, loan_to_abs)
+ in
+
+ (* Merge the abstractions together *)
let merged_abs : V.AbstractionId.id UF.elem V.AbstractionId.Map.t =
V.AbstractionId.Map.of_list (List.map (fun id -> (id, UF.make id)) abs_ids)
in
@@ -243,35 +308,41 @@ let collapse_ctx (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
(fun bid ->
match V.BorrowId.Map.find_opt bid loan_to_abs with
| None -> (* Nothing to do *) ()
- | Some abs_id1 ->
- (* We need to merge - unless we have already merged *)
- (* First, find the representatives for the two abstractions (the
- representative is the abstraction into which we merged) *)
- let abs_ref0 =
- UF.find (V.AbstractionId.Map.find abs_id0 merged_abs)
- in
- let abs_id0 = UF.get abs_ref0 in
- let abs_ref1 =
- UF.find (V.AbstractionId.Map.find abs_id1 merged_abs)
- in
- let abs_id1 = UF.get abs_ref1 in
- (* If the two ids are the same, it means the abstractions were already merged *)
- if abs_id0 = abs_id1 then ()
- else
- (* We actually need to merge the abstractions *)
- (* Lookup the abstractions *)
- let abs0 = C.ctx_lookup_abs !ctx abs_id0 in
- let abs1 = C.ctx_lookup_abs !ctx abs_id1 in
- (* Merge them - note that we take care to merge [abs0] into [abs1]
- (the order is important).
- *)
- let nabs = merge_abstractions abs_kind can_end !ctx abs1 abs0 in
- (* Update the environment *)
- ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs);
- ctx := fst (C.ctx_remove_abs !ctx abs_id0);
- (* Update the union find *)
- let abs_ref_merged = UF.union abs_ref0 abs_ref1 in
- UF.set abs_ref_merged nabs.abs_id)
+ | Some abs_ids1 ->
+ V.AbstractionId.Set.iter
+ (fun abs_id1 ->
+ (* We need to merge - unless we have already merged *)
+ (* First, find the representatives for the two abstractions (the
+ representative is the abstraction into which we merged) *)
+ let abs_ref0 =
+ UF.find (V.AbstractionId.Map.find abs_id0 merged_abs)
+ in
+ let abs_id0 = UF.get abs_ref0 in
+ let abs_ref1 =
+ UF.find (V.AbstractionId.Map.find abs_id1 merged_abs)
+ in
+ let abs_id1 = UF.get abs_ref1 in
+ (* If the two ids are the same, it means the abstractions were already merged *)
+ if abs_id0 = abs_id1 then ()
+ else
+ (* We actually need to merge the abstractions *)
+ (* Lookup the abstractions *)
+ let abs0 = C.ctx_lookup_abs !ctx abs_id0 in
+ let abs1 = C.ctx_lookup_abs !ctx abs_id1 in
+ (* Merge them - note that we take care to merge [abs0] into [abs1]
+ (the order is important).
+ *)
+ let nabs =
+ merge_abstractions abs_kind can_end merge_funs !ctx abs1
+ abs0
+ in
+ (* Update the environment *)
+ ctx := fst (C.ctx_subst_abs !ctx abs_id1 nabs);
+ ctx := fst (C.ctx_remove_abs !ctx abs_id0);
+ (* Update the union find *)
+ let abs_ref_merged = UF.union abs_ref0 abs_ref1 in
+ UF.set abs_ref_merged nabs.abs_id)
+ abs_ids1)
bids)
abs_ids;
@@ -313,6 +384,355 @@ let match_rtypes (rid_map : T.RegionId.InjSubst.t ref) (ctx : C.eval_ctx)
in
match_types check_regions ctx ty0 ty1
+(** See {!Match} *)
+module type Matcher = sig
+ (** The input primitive values are not equal *)
+ val match_distinct_primitive_values :
+ T.ety -> V.primitive_value -> V.primitive_value -> V.typed_value
+
+ (** The input ADTs don't have the same variant *)
+ val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value
+
+ (** The meta-value is the result of a match *)
+ val match_shared_borrows :
+ T.ety -> V.mvalue -> V.borrow_id -> V.borrow_id -> V.mvalue * V.borrow_id
+
+ (** The input parameters are:
+ - [ty]
+ - [bid0]: first borrow id
+ - [bv0]: first borrowed value
+ - [bid1]
+ - [bv1]
+ - [bv]: the result of matching [bv0] with [bv1]
+ *)
+ val match_mut_borrows :
+ T.ety ->
+ V.borrow_id ->
+ V.typed_value ->
+ V.borrow_id ->
+ V.typed_value ->
+ V.typed_value ->
+ V.borrow_id * V.typed_value
+
+ (** The shared value is the result of a match *)
+ val match_shared_loans :
+ T.ety ->
+ V.loan_id_set ->
+ V.loan_id_set ->
+ V.typed_value ->
+ V.loan_id_set * V.typed_value
+
+ val match_mut_loans : T.ety -> V.loan_id -> V.loan_id -> V.loan_id
+
+ (** There are no constraints on the input symbolic values *)
+ val match_symbolic_values :
+ V.symbolic_value -> V.symbolic_value -> V.symbolic_value
+end
+
+(** Generic functor to implement matching functions between values, environments,
+ etc.
+
+ We use it for joins, to check if two environments are convertible, etc.
+ *)
+module Match (M : Matcher) = struct
+ (** Match two values *)
+ let rec match_typed_values (ctx : C.eval_ctx) (v0 : V.typed_value)
+ (v1 : V.typed_value) : V.typed_value =
+ let match_rec = match_typed_values ctx in
+ assert (v0.V.ty = v1.V.ty);
+ match (v0.V.value, v1.V.value) with
+ | V.Primitive pv0, V.Primitive pv1 ->
+ if pv0 = pv1 then v1
+ else (
+ assert (v0.V.ty = v1.V.ty);
+ M.match_distinct_primitive_values v0.V.ty pv0 pv1)
+ | V.Adt av0, V.Adt av1 ->
+ if av0.variant_id = av1.variant_id then
+ let fields = List.combine av0.field_values av1.field_values in
+ let field_values =
+ List.map (fun (f0, f1) -> match_rec f0 f1) fields
+ in
+ let value : V.value =
+ V.Adt { variant_id = av0.variant_id; field_values }
+ in
+ { V.value; ty = v1.V.ty }
+ else (
+ (* For now, we don't merge ADTs which contain borrows *)
+ assert (not (value_has_borrows ctx v0.V.value));
+ assert (not (value_has_borrows ctx v1.V.value));
+ (* Merge *)
+ M.match_distinct_adts v0.V.ty av0 av1)
+ | Bottom, Bottom -> v1
+ | Borrow bc0, Borrow bc1 ->
+ let bc =
+ match (bc0, bc1) with
+ | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
+ (* Not completely sure what to do with the meta-value. If a shared
+ symbolic value gets expanded in a branch, it may be simplified
+ (by being folded back to a symbolic value) upon doing the join,
+ which as a result would lead to code where it is considered as
+ mutable (which is sound). On the other hand, if we access a
+ symbolic value in a loop, the translated loop should take it as
+ input anyway, so maybe this actually leads to equivalent
+ code.
+ *)
+ let mv = match_rec mv0 mv1 in
+ assert (not (value_has_borrows ctx mv.V.value));
+ let mv, bid = M.match_shared_borrows v0.V.ty mv bid0 bid1 in
+ V.SharedBorrow (mv, bid)
+ | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
+ let bv = match_rec bv0 bv1 in
+ assert (not (value_has_borrows ctx bv.V.value));
+ let bid, bv = M.match_mut_borrows v0.V.ty bid0 bv0 bid1 bv1 bv in
+ V.MutBorrow (bid, bv)
+ | ReservedMutBorrow _, _
+ | _, ReservedMutBorrow _
+ | SharedBorrow _, MutBorrow _
+ | MutBorrow _, SharedBorrow _ ->
+ (* If we get here, either there is a typing inconsistency, or we are
+ trying to match a reserved borrow, which shouldn't happen because
+ reserved borrow should be eliminated very quickly - they are introduced
+ just before function calls which activate them *)
+ raise (Failure "Unexpected")
+ in
+ { V.value = V.Borrow bc; V.ty = v1.V.ty }
+ | Loan lc0, Loan lc1 ->
+ (* TODO: maybe we should enforce that the ids are always exactly the same -
+ without matching *)
+ let lc =
+ match (lc0, lc1) with
+ | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) ->
+ let sv = match_rec sv0 sv1 in
+ assert (not (value_has_borrows ctx sv.V.value));
+ let ids, sv = M.match_shared_loans v0.V.ty ids0 ids1 sv in
+ V.SharedLoan (ids, sv)
+ | MutLoan id0, MutLoan id1 ->
+ let id = M.match_mut_loans v0.V.ty id0 id1 in
+ V.MutLoan id
+ | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ ->
+ raise (Failure "Unreachable")
+ in
+ { V.value = Loan lc; ty = v1.V.ty }
+ | Symbolic sv0, Symbolic sv1 ->
+ let sv = M.match_symbolic_values sv0 sv1 in
+ { v1 with V.value = V.Symbolic sv }
+ (* (* TODO: id check mapping *)
+ let id0 = lookup_sid sv0.sv_id in
+ let id1 = sv1.sv_id in
+ if id0 = id1 then (
+ assert (sv0.sv_kind = sv1.sv_kind);
+ (* Sanity check: the types should be the same *)
+ match_rtypes rid_map ctx sv0.sv_ty sv1.sv_ty;
+ (* Return *)
+ v1)
+ else (
+ (* For now, we force all the symbolic values containing borrows to
+ be eagerly expanded, and we don't support nested borrows *)
+ assert (not (value_has_borrows ctx v0.V.value));
+ assert (not (value_has_borrows ctx v1.V.value));
+ raise (Failure "Unimplemented")
+ *)
+ | Loan lc, _ -> (
+ match lc with
+ | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
+ | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
+ | _, Loan lc -> (
+ match lc with
+ | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
+ | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
+ | Symbolic _, _ -> raise (Failure "Unimplemented")
+ | _, Symbolic _ -> raise (Failure "Unimplemented")
+ | _ -> raise (Failure "Unreachable")
+end
+
+(* Very annoying: functors only take modules as inputs... *)
+module type MatchJoinState = sig
+ (** The current context *)
+ val ctx : C.eval_ctx
+
+ (** The current loop *)
+ val loop_id : V.LoopId.id
+
+ (** The abstractions introduced when performing the matches *)
+ val nabs : V.abs list ref
+end
+
+module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
+ (** Small utility *)
+ let push_abs (abs : V.abs) : unit = S.nabs := abs :: !S.nabs
+
+ let match_distinct_primitive_values (ty : T.ety) (_ : V.primitive_value)
+ (_ : V.primitive_value) : V.typed_value =
+ mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty
+
+ let match_distinct_adts (ty : T.ety) (adt0 : V.adt_value) (adt1 : V.adt_value)
+ : V.typed_value =
+ (* Check that the ADTs don't contain borrows - this is redundant with checks
+ performed by the caller, but we prefer to be safe with regards to future
+ updates
+ *)
+ let check_no_borrows (v : V.typed_value) =
+ assert (not (value_has_borrows S.ctx v.V.value))
+ in
+ List.iter check_no_borrows adt0.field_values;
+ List.iter check_no_borrows adt1.field_values;
+
+ (* Check if there are loans: we request to end them *)
+ let check_loans (left : bool) (fields : V.typed_value list) : unit =
+ match InterpreterBorrowsCore.get_first_loan_in_values fields with
+ | Some (V.SharedLoan (ids, _)) ->
+ if left then raise (ValueMatchFailure (LoansInLeft ids))
+ else raise (ValueMatchFailure (LoansInRight ids))
+ | Some (V.MutLoan id) ->
+ if left then raise (ValueMatchFailure (LoanInLeft id))
+ else raise (ValueMatchFailure (LoanInRight id))
+ | None -> ()
+ in
+ check_loans true adt0.field_values;
+ check_loans false adt1.field_values;
+
+ (* No borrows, no loans: we can introduce a symbolic value *)
+ mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty
+
+ let match_shared_borrows (ty : T.ety) (mv : V.mvalue) (bid0 : V.borrow_id)
+ (bid1 : V.borrow_id) : V.mvalue * V.borrow_id =
+ if bid0 = bid1 then (mv, bid0)
+ else
+ (* We replace bid0 and bid1 with a fresh borrow id, and introduce
+ an abstraction which links all of them:
+ {[
+ { SB bid0, SB bid1, SL {bid2} }
+ ]}
+ *)
+ let rid = C.fresh_region_id () in
+ let bid2 = C.fresh_borrow_id () in
+
+ (* Generate a fresh symbolic value for the shared value *)
+ let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty in
+
+ let _, bv_ty, kind = ty_as_ref ty in
+ let borrow_ty =
+ mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind
+ in
+
+ (* Generate the avalues for the abstraction *)
+ let mk_aborrow (bid : V.borrow_id) : V.typed_avalue =
+ let value = V.ABorrow (V.ASharedBorrow bid) in
+ { V.value; ty = borrow_ty }
+ in
+ let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in
+
+ let loan =
+ V.ASharedLoan
+ ( V.BorrowId.Set.singleton bid2,
+ sv,
+ mk_aignored (ety_no_regions_to_rty bv_ty) )
+ in
+ (* Note that an aloan has a borrow type *)
+ let loan = { V.value = V.ALoan loan; ty = borrow_ty } in
+
+ let avalues = List.append borrows [ loan ] in
+
+ (* Generate the abstraction *)
+ let abs =
+ {
+ V.abs_id = C.fresh_abstraction_id ();
+ kind = V.Loop S.loop_id;
+ can_end = false;
+ parents = V.AbstractionId.Set.empty;
+ original_parents = [];
+ regions = T.RegionId.Set.singleton rid;
+ ancestors_regions = T.RegionId.Set.empty;
+ avalues;
+ }
+ in
+ push_abs abs;
+
+ (* Return the new borrow *)
+ (sv, bid2)
+
+ let match_mut_borrows (ty : T.ety) (bid0 : V.borrow_id) (bv0 : V.typed_value)
+ (bid1 : V.borrow_id) (bv1 : V.typed_value) (bv : V.typed_value) :
+ V.borrow_id * V.typed_value =
+ if bid0 = bid1 then (bid0, bv)
+ else
+ (* We replace bid0 and bid1 with a fresh borrow id, and introduce
+ an abstraction which links all of them:
+ {[
+ { MB bid0, MB bid1, ML bid2 }
+ ]}
+ *)
+ let rid = C.fresh_region_id () in
+ let bid2 = C.fresh_borrow_id () in
+
+ (* Generate a fresh symbolic value for the borrowed value *)
+ let sv = mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty in
+
+ let _, bv_ty, kind = ty_as_ref ty in
+ let borrow_ty =
+ mk_ref_ty (T.Var rid) (ety_no_regions_to_rty bv_ty) kind
+ in
+
+ (* Generate the avalues for the abstraction *)
+ let mk_aborrow (bid : V.borrow_id) (bv : V.typed_value) : V.typed_avalue =
+ let bv_ty = ety_no_regions_to_rty bv.V.ty in
+ let value = V.ABorrow (V.AMutBorrow (bv, bid, mk_aignored bv_ty)) in
+ { V.value; ty = borrow_ty }
+ in
+ let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in
+
+ let loan = V.AMutLoan (bid2, mk_aignored (ety_no_regions_to_rty bv_ty)) in
+ (* Note that an aloan has a borrow type *)
+ let loan = { V.value = V.ALoan loan; ty = borrow_ty } in
+
+ let avalues = List.append borrows [ loan ] in
+
+ (* Generate the abstraction *)
+ let abs =
+ {
+ V.abs_id = C.fresh_abstraction_id ();
+ kind = V.Loop S.loop_id;
+ can_end = false;
+ parents = V.AbstractionId.Set.empty;
+ original_parents = [];
+ regions = T.RegionId.Set.singleton rid;
+ ancestors_regions = T.RegionId.Set.empty;
+ avalues;
+ }
+ in
+ push_abs abs;
+
+ (* Return the new borrow *)
+ (bid2, sv)
+
+ let match_shared_loans (ty : T.ety) (ids0 : V.loan_id_set)
+ (ids1 : V.loan_id_set) (sv : V.typed_value) :
+ V.loan_id_set * V.typed_value =
+ (* Check if the ids are the same - Rem.: we forbid the loans to a value
+ to vary. However, we allow to dive inside a data-structure: in this
+ case,
+ *)
+ let extra_ids_left = V.BorrowId.Set.diff ids0 ids1 in
+ let extra_ids_right = V.BorrowId.Set.diff ids1 ids0 in
+ if not (V.BorrowId.Set.is_empty extra_ids_left) then
+ raise (ValueMatchFailure (LoansInLeft extra_ids_left));
+ if not (V.BorrowId.Set.is_empty extra_ids_right) then
+ raise (ValueMatchFailure (LoansInRight extra_ids_right));
+
+ (* *)
+ raise (Failure "Unimplemented")
+
+ let match_mut_loans (ty : T.ety) (id0 : V.loan_id) (id1 : V.loan_id) :
+ V.loan_id =
+ raise (Failure "Unimplemented")
+
+ (** There are no constraints on the input symbolic values *)
+ let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) :
+ V.symbolic_value =
+ raise (Failure "Unimplemented")
+end
+
+(*
(** This function raises exceptions of kind {!ValueMatchFailue}.
[convertible]: the function updates it to [false] if the result of the
@@ -439,15 +859,16 @@ let rec match_typed_values (config : C.config) (thresh : cnt_thresholds)
raise (Failure "Unimplemented"))
| Loan lc, _ -> (
match lc with
- | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids))
- | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id)))
+ | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
+ | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
| _, Loan lc -> (
match lc with
- | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids))
- | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id)))
+ | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
+ | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
| Symbolic _, _ -> raise (Failure "Unimplemented")
| _, Symbolic _ -> raise (Failure "Unimplemented")
| _ -> raise (Failure "Unreachable")
+ *)
(*(** This function raises exceptions of kind {!ValueMatchFailue} *)
let rec match_typed_avalues (config : C.config) (thresh : cnt_thresholds)
@@ -563,16 +984,19 @@ let rec match_typed_values (config : C.config) (thresh : cnt_thresholds)
raise (Failure "Unimplemented"))
| Loan lc, _ -> (
match lc with
- | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInSrc ids))
- | MutLoan id -> raise (ValueMatchFailure (EndBorrowInSrc id)))
+ | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
+ | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
| _, Loan lc -> (
match lc with
- | SharedLoan (ids, _) -> raise (ValueMatchFailure (EndBorrowsInTgt ids))
- | MutLoan id -> raise (ValueMatchFailure (EndBorrowInTgt id)))
+ | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
+ | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
| _ -> raise (Failure "Unreachable")*)
-(** Apply substitutions in the first abstraction, then merge the abstractions together. *)
-let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
+(** Apply substitutions in the first abstraction, then join the abstractions together.
+
+ TODO: remove?
+ *)
+let subst_join_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
(rid_map : T.RegionId.InjSubst.t) (bid_map : V.BorrowId.InjSubst.t)
(sid_map : V.SymbolicValueId.InjSubst.t) (ctx : C.eval_ctx) (abs0 : V.abs)
(abs1 : V.abs) : V.abs =
@@ -599,7 +1023,7 @@ let subst_merge_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
(* Merge the two abstractions *)
let abs_kind = V.Loop loop_id in
let can_end = false in
- merge_abstractions abs_kind can_end ctx abs0 abs1
+ merge_abstractions abs_kind can_end None ctx abs0 abs1
(** Merge a borrow with the abstraction containing the associated loan, where
the abstraction must be a *loop abstraction* (we don't synthesize code during
@@ -750,22 +1174,22 @@ let compute_loop_entry_fixed_point (config : C.config)
(* Check if the join succeeded, or if we need to end abstractions/borrows
in the original environment first *)
match join_ctxs mctx with
- | Error (EndAbsInSrc id) ->
+ | Error (AbsInLeft id) ->
let ctx1 =
InterpreterBorrows.end_abstraction_no_synth config id mctx.ctx
in
eval_iteration_then_join { mctx with ctx = ctx1 }
- | Error (EndBorrowInSrc id) ->
+ | Error (LoanInLeft id) ->
let ctx1 =
InterpreterBorrows.end_borrow_no_synth config id mctx.ctx
in
eval_iteration_then_join { mctx with ctx = ctx1 }
- | Error (EndBorrowsInSrc ids) ->
+ | Error (LoansInLeft ids) ->
let ctx1 =
InterpreterBorrows.end_borrows_no_synth config ids mctx.ctx
in
eval_iteration_then_join { mctx with ctx = ctx1 }
- | Error (EndBorrowInTgt _ | EndBorrowsInTgt _) ->
+ | Error (LoanInRight _ | LoansInRight _) ->
(* Shouldn't happen here *)
raise (Failure "Unreachable")
| Ok mctx1 ->
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 62dce004..b287de27 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -54,6 +54,12 @@ let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.rty) :
let value = V.Symbolic value in
{ V.value; V.ty }
+(** Create a fresh symbolic value *)
+let mk_fresh_symbolic_typed_value_from_ety (sv_kind : V.sv_kind) (ety : T.ety) :
+ V.typed_value =
+ let ty = TypesUtils.ety_no_regions_to_rty ety in
+ mk_fresh_symbolic_typed_value sv_kind ty
+
(** Create a typed value from a symbolic value. *)
let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
V.typed_value =
@@ -115,7 +121,10 @@ let remove_borrow_from_asb (bid : V.BorrowId.id)
(** We sometimes need to return a value whose type may vary depending on
whether we find it in a "concrete" value or an abstraction (ex.: loan
- contents when we perform environment lookups by using borrow ids) *)
+ contents when we perform environment lookups by using borrow ids)
+
+ TODO: change the name "abstract"
+ *)
type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b
(** Generic loan content: concrete or abstract *)
@@ -221,7 +230,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
method! visit_symbolic_value _ s =
match s.sv_kind with
- | V.FunCallRet | V.LoopOutput ->
+ | V.FunCallRet | V.LoopOutput | V.LoopJoin ->
if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
raise Found
else ()
diff --git a/compiler/Values.ml b/compiler/Values.ml
index f206f65a..efb0bb67 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -45,6 +45,8 @@ type sv_kind =
| LoopOutput (** The output of a loop (seen as a forward computation) *)
| LoopGivenBack
(** A value given back by a loop (when ending abstractions while going backwards) *)
+ | LoopJoin
+ (** The result of a loop join (when computing loop fixed points) *)
[@@deriving show, ord]
(** A symbolic value *)
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index df00bfb2..470f40ac 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -170,6 +170,24 @@ let value_has_borrows (infos : TA.type_infos) (v : value) : bool =
false
with Found -> true
+(** Check if a value has loans.
+
+ Note that loans are necessarily concrete (there can't be loans hidden
+ inside symbolic values).
+ *)
+let value_has_loans (v : value) : bool =
+ let obj =
+ object
+ inherit [_] iter_typed_value
+ method! visit_loan_content _env _ = raise Found
+ end
+ in
+ (* We use exceptions *)
+ try
+ obj#visit_value () v;
+ false
+ with Found -> true
+
(** Check if a value has loans or borrows in **a general sense**.
It checks if: