diff options
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 66 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 10 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 18 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 16 | ||||
| -rw-r--r-- | compiler/Print.ml | 18 | ||||
| -rw-r--r-- | compiler/Values.ml | 16 |
6 files changed, 94 insertions, 50 deletions
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 2628b26a..3bef7b30 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -255,13 +255,17 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (because there are no use cases requiring finer control) *) method! visit_aloan_content env lc = match lc with - | AMutLoan (bid, av) -> + | AMutLoan (pm, bid, av) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid = l then raise (FoundGLoanContent (Abstract lc)) - else super#visit_AMutLoan env bid av - | ASharedLoan (bids, v, av) -> + else super#visit_AMutLoan env pm bid av + | ASharedLoan (pm, bids, v, av) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; if BorrowId.Set.mem l bids then raise (FoundGLoanContent (Abstract lc)) - else super#visit_ASharedLoan env bids v av + else super#visit_ASharedLoan env pm bids v av | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) @@ -396,11 +400,15 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) method! visit_aloan_content env lc = match lc with - | AMutLoan (bid, av) -> - if bid = l then update () else super#visit_AMutLoan env bid av - | ASharedLoan (bids, v, av) -> + | AMutLoan (pm, bid, av) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; + if bid = l then update () else super#visit_AMutLoan env pm bid av + | ASharedLoan (pm, bids, v, av) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; if BorrowId.Set.mem l bids then update () - else super#visit_ASharedLoan env bids v av + else super#visit_ASharedLoan env pm bids v av | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) @@ -422,8 +430,8 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) ctx (** Lookup a borrow content from a borrow id. *) -let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) - : g_borrow_content option = +let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind) + (l : BorrowId.id) (ctx : eval_ctx) : g_borrow_content option = let obj = object inherit [_] iter_eval_ctx as super @@ -453,12 +461,16 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) method! visit_aborrow_content env bc = match bc with - | AMutBorrow (bid, av) -> + | AMutBorrow (pm, bid, av) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid = l then raise (FoundGBorrowContent (Abstract bc)) - else super#visit_AMutBorrow env bid av - | ASharedBorrow bid -> + else super#visit_AMutBorrow env pm bid av + | ASharedBorrow (pm, bid) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid = l then raise (FoundGBorrowContent (Abstract bc)) - else super#visit_ASharedBorrow env bid + else super#visit_ASharedBorrow env pm bid | AIgnoredMutBorrow (_, _) | AEndedMutBorrow _ | AEndedIgnoredMutBorrow @@ -486,7 +498,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) *) let lookup_borrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) (ctx : eval_ctx) : g_borrow_content = - match lookup_borrow_opt ek l ctx with + match lookup_borrow_opt span ek l ctx with | None -> craise __FILE__ __LINE__ span "Unreachable" | Some lc -> lc @@ -571,12 +583,16 @@ let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) method! visit_ABorrow env bc = match bc with - | AMutBorrow (bid, av) -> + | AMutBorrow (pm, bid, av) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid = l then update () - else ABorrow (super#visit_AMutBorrow env bid av) - | ASharedBorrow bid -> + else ABorrow (super#visit_AMutBorrow env pm bid av) + | ASharedBorrow (pm, bid) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid = l then update () - else ABorrow (super#visit_ASharedBorrow env bid) + else ABorrow (super#visit_ASharedBorrow env pm bid) | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedSharedBorrow | AEndedIgnoredMutBorrow _ -> super#visit_ABorrow env bc @@ -1182,8 +1198,14 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) : method! visit_aloan_content env lc = match lc with - | AMutLoan (bid, _) -> raise (FoundBorrowIds (Borrow bid)) - | ASharedLoan (bids, _, _) -> raise (FoundBorrowIds (Borrows bids)) + | AMutLoan (pm, bid, _) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; + raise (FoundBorrowIds (Borrow bid)) + | ASharedLoan (pm, bids, _, _) -> + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; + raise (FoundBorrowIds (Borrows bids)) | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) -> super#visit_aloan_content env lc @@ -1232,7 +1254,7 @@ let lookup_shared_value_opt (span : Meta.span) (ctx : eval_ctx) | None -> None | Some (_, lc) -> ( match lc with - | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> + | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, _, sv, _)) -> Some sv | _ -> None) diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index faba1088..a74017d1 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -187,7 +187,7 @@ let rec access_projection (span : Meta.span) (access : projection_access) Ok (ctx, { res with updated = v })) | ( _, Abstract - ( AMutLoan (_, _) + ( AMutLoan (_, _, _) | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) @@ -197,7 +197,9 @@ let rec access_projection (span : Meta.span) (access : projection_access) | AIgnoredSharedLoan _ ) ) -> craise __FILE__ __LINE__ span "Expected a shared (abstraction) loan" - | _, Abstract (ASharedLoan (bids, sv, _av)) -> ( + | _, Abstract (ASharedLoan (pm, bids, sv, _av)) -> ( + (* Sanity check: markers can only appear when we're doing a join *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Explore the shared value *) match access_projection span access ctx update p' sv with | Error err -> Error err @@ -205,14 +207,14 @@ let rec access_projection (span : Meta.span) (access : projection_access) (* Relookup the child avalue *) let av = match lookup_loan span ek bid ctx with - | _, Abstract (ASharedLoan (_, _, av)) -> av + | _, Abstract (ASharedLoan (_, _, _, av)) -> av | _ -> craise __FILE__ __LINE__ span "Unexpected" in (* Update the shared loan with the new value returned by {!access_projection} *) let ctx = update_aloan span ek bid - (ASharedLoan (bids, res.updated, av)) + (ASharedLoan (pm, bids, res.updated, av)) ctx in (* Return - note that we don't need to update the borrow itself *) diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index a887c44c..0e820982 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -61,7 +61,7 @@ let rec apply_proj_borrows_on_shared_borrow (span : Meta.span) (ctx : eval_ctx) let asb = match sv with | _, Concrete (VSharedLoan (_, sv)) - | _, Abstract (ASharedLoan (_, sv, _)) -> + | _, Abstract (ASharedLoan (_, _, sv, _)) -> apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow regions sv ref_ty | _ -> craise __FILE__ __LINE__ span "Unexpected" @@ -137,7 +137,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool) apply_proj_borrows span check_symbolic_no_ended ctx fresh_reborrow regions ancestors_regions bv ref_ty in - AMutBorrow (bid, bv) + AMutBorrow (PNone, bid, bv) | VSharedBorrow bid, RShared -> (* Rem.: we don't need to also apply the projection on the borrowed value, because for as long as the abstraction @@ -150,7 +150,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool) need to lookup the shared value and project it (see the other branch of the [if then else]). *) - ASharedBorrow bid + ASharedBorrow (PNone, bid) | VReservedMutBorrow _, _ -> craise __FILE__ __LINE__ span "Can't apply a proj_borrow over a reserved mutable borrow" @@ -183,7 +183,7 @@ let rec apply_proj_borrows (span : Meta.span) (check_symbolic_no_ended : bool) let asb = match sv with | _, Concrete (VSharedLoan (_, sv)) - | _, Abstract (ASharedLoan (_, sv, _)) -> + | _, Abstract (ASharedLoan (_, _, sv, _)) -> apply_proj_borrows_on_shared_borrow span ctx fresh_reborrow regions sv ref_ty | _ -> craise __FILE__ __LINE__ span "Unexpected" @@ -288,7 +288,7 @@ let apply_proj_loans_on_symbolic_expansion (span : Meta.span) * we never project over static regions) *) if region_in_set r regions then (* In the set: keep *) - (ALoan (AMutLoan (bid, child_av)), ref_ty) + (ALoan (AMutLoan (PNone, bid, child_av)), ref_ty) else (* Not in the set: ignore *) (* If the borrow id is in the ancestor's regions, we still need @@ -307,7 +307,7 @@ let apply_proj_loans_on_symbolic_expansion (span : Meta.span) if region_in_set r regions then (* In the set: keep *) let shared_value = mk_typed_value_from_symbolic_value spc in - (ALoan (ASharedLoan (bids, shared_value, child_av)), ref_ty) + (ALoan (ASharedLoan (PNone, bids, shared_value, child_av)), ref_ty) else (* Not in the set: ignore *) (ALoan (AIgnoredSharedLoan child_av), ref_ty) @@ -441,7 +441,7 @@ let apply_reborrows (span : Meta.span) method! visit_aloan_content env lc = match lc with - | ASharedLoan (bids, sv, av) -> + | ASharedLoan (pm, bids, sv, av) -> (* Insert the reborrows *) let bids = insert_reborrows bids in (* Similarly to the non-abstraction case: check if the shared @@ -453,9 +453,9 @@ let apply_reborrows (span : Meta.span) | Some bid -> insert_reborrows_for_bid bids bid in (* Update and explore *) - super#visit_ASharedLoan env bids sv av + super#visit_ASharedLoan env pm bids sv av | AIgnoredSharedLoan _ - | AMutLoan (_, _) + | AMutLoan (_, _, _) | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) | AIgnoredMutLoan (_, _) diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 51be02c8..bcf92b25 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -246,8 +246,8 @@ let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) : method! visit_aborrow_content env bc = let _ = match bc with - | AMutBorrow (bid, _) -> register_borrow BMut bid - | ASharedBorrow bid -> register_borrow BShared bid + | AMutBorrow (_, bid, _) -> register_borrow BMut bid + | ASharedBorrow (_, bid) -> register_borrow BShared bid | AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow RMut bid | AIgnoredMutBorrow (None, _) | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow @@ -341,8 +341,8 @@ let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit = (* Update the info *) let info = match lc with - | AMutLoan (_, _) -> set_outer_mut info - | ASharedLoan (_, _, _) -> set_outer_shared info + | AMutLoan (_, _, _) -> set_outer_mut info + | ASharedLoan (_, _, _, _) -> set_outer_shared info | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } -> set_outer_mut info | AEndedSharedLoan (_, _) -> set_outer_shared info @@ -359,7 +359,7 @@ let check_borrowed_values_invariant (span : Meta.span) (ctx : eval_ctx) : unit = (* Update the info *) let info = match bc with - | AMutBorrow (_, _) -> set_outer_mut info + | AMutBorrow (_, _, _) -> set_outer_mut info | ASharedBorrow _ | AEndedSharedBorrow -> set_outer_shared info | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ -> @@ -500,9 +500,11 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan span ek_all bid ctx in match glc with - | Concrete (VSharedLoan (_, sv)) - | Abstract (ASharedLoan (_, sv, _)) -> + | Concrete (VSharedLoan (_, sv)) -> sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span + | Abstract (ASharedLoan (pm, _, sv, _)) -> + sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) span; + sanity_check __FILE__ __LINE__ (pm = PNone) span | _ -> craise __FILE__ __LINE__ span "Inconsistent context") | VMutBorrow (_, bv), RMut -> sanity_check __FILE__ __LINE__ diff --git a/compiler/Print.ml b/compiler/Print.ml index f7f1f54b..12506274 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -148,6 +148,12 @@ module Values = struct | AEndedProjBorrows _mv -> "_" | AIgnoredProjBorrows -> "_" + let add_proj_marker (pm : proj_marker) (s : string) : string = + match pm with + | PNone -> s + | PLeft -> "|" ^ s ^ "|" + | PRight -> "┊" ^ s ^ "┊" + let rec typed_avalue_to_string ?(span : Meta.span option = None) (env : fmt_env) (v : typed_avalue) : string = match v.value with @@ -197,17 +203,19 @@ module Values = struct and aloan_content_to_string ?(span : Meta.span option = None) (env : fmt_env) (lc : aloan_content) : string = match lc with - | AMutLoan (bid, av) -> + | AMutLoan (pm, bid, av) -> "@mut_loan(" ^ BorrowId.to_string bid ^ ", " ^ typed_avalue_to_string ~span env av ^ ")" - | ASharedLoan (loans, v, av) -> + |> add_proj_marker pm + | ASharedLoan (pm, loans, v, av) -> let loans = BorrowId.Set.to_string None loans in "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string ~span env v ^ ", " ^ typed_avalue_to_string ~span env av ^ ")" + |> add_proj_marker pm | AEndedMutLoan ml -> "@ended_mut_loan{" ^ typed_avalue_to_string ~span env ml.child @@ -238,11 +246,13 @@ module Values = struct and aborrow_content_to_string ?(span : Meta.span option = None) (env : fmt_env) (bc : aborrow_content) : string = match bc with - | AMutBorrow (bid, av) -> + | AMutBorrow (pm, bid, av) -> "mb@" ^ BorrowId.to_string bid ^ " (" ^ typed_avalue_to_string ~span env av ^ ")" - | ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid + |> add_proj_marker pm + | ASharedBorrow (pm, bid) -> + "sb@" ^ BorrowId.to_string bid |> add_proj_marker pm | AIgnoredMutBorrow (opt_bid, av) -> "@ignored_mut_borrow(" ^ option_to_string BorrowId.to_string opt_bid diff --git a/compiler/Values.ml b/compiler/Values.ml index e7b96051..96d61f88 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -176,6 +176,10 @@ type region_id_set = RegionId.Set.t [@@deriving show, ord] type abstraction_id = AbstractionId.id [@@deriving show, ord] type abstraction_id_set = AbstractionId.Set.t [@@deriving show, ord] +(** Projection markers: those are used in the joins. + For additional explanations see: https://arxiv.org/pdf/2404.02680#section.5 *) +type proj_marker = PNone | PLeft | PRight [@@deriving show, ord] + (** Ancestor for {!typed_avalue} iter visitor *) class ['self] iter_typed_avalue_base = object (self : 'self) @@ -192,6 +196,8 @@ class ['self] iter_typed_avalue_base = method visit_abstraction_id_set : 'env -> abstraction_id_set -> unit = fun env ids -> AbstractionId.Set.iter (self#visit_abstraction_id env) ids + + method visit_proj_marker : 'env -> proj_marker -> unit = fun _ _ -> () end (** Ancestor for {!typed_avalue} map visitor *) @@ -212,6 +218,8 @@ class ['self] map_typed_avalue_base = method visit_abstraction_id_set : 'env -> abstraction_id_set -> abstraction_id_set = fun env ids -> AbstractionId.Set.map (self#visit_abstraction_id env) ids + + method visit_proj_marker : 'env -> proj_marker -> proj_marker = fun _ x -> x end (** When giving shared borrows to functions (i.e., inserting shared borrows inside @@ -333,7 +341,7 @@ and adt_avalue = { contain other, independent loans. *) and aloan_content = - | AMutLoan of loan_id * typed_avalue + | AMutLoan of proj_marker * loan_id * typed_avalue (** A mutable loan owned by an abstraction. The avalue is the child avalue. @@ -354,7 +362,7 @@ and aloan_content = px -> mut_borrow l0 (mut_borrow @s1) ]} *) - | ASharedLoan of loan_id_set * typed_value * typed_avalue + | ASharedLoan of proj_marker * loan_id_set * typed_value * typed_avalue (** A shared loan owned by an abstraction. The avalue is the child avalue. @@ -507,7 +515,7 @@ and aloan_content = ids)? *) and aborrow_content = - | AMutBorrow of borrow_id * typed_avalue + | AMutBorrow of proj_marker * borrow_id * typed_avalue (** A mutable borrow owned by an abstraction. Is used when an abstraction "consumes" borrows, when giving borrows @@ -528,7 +536,7 @@ and aborrow_content = > abs0 { a_mut_borrow l0 (U32 0) _ } ]} *) - | ASharedBorrow of borrow_id + | ASharedBorrow of proj_marker * borrow_id (** A shared borrow owned by an abstraction. Example: |