diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 647 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 84 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 14 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 566 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 13 | ||||
| -rw-r--r-- | compiler/Values.ml | 2 | ||||
| -rw-r--r-- | compiler/ValuesUtils.ml | 18 |
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: |