From 51c43721beb1f4af1e903360c0fbc5c1790f1ab5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 May 2024 15:56:34 +0200 Subject: Start adding markers --- compiler/InterpreterBorrowsCore.ml | 66 +++++++++++++++++++++++++------------- 1 file changed, 44 insertions(+), 22 deletions(-) (limited to 'compiler/InterpreterBorrowsCore.ml') 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) -- cgit v1.2.3 From 18623d7ee894a8e21bca9ef58fb4087cb4be558b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 3 Jun 2024 12:08:36 +0200 Subject: Make minor modifications --- compiler/InterpreterBorrowsCore.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'compiler/InterpreterBorrowsCore.ml') diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 3bef7b30..0469d58e 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -256,12 +256,12 @@ let lookup_loan_opt (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) method! visit_aloan_content env lc = match lc with | AMutLoan (pm, bid, av) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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 pm bid av | ASharedLoan (pm, bids, v, av) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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)) @@ -401,11 +401,11 @@ let update_aloan (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) method! visit_aloan_content env lc = match lc with | AMutLoan (pm, bid, av) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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: projection 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 pm bids v av @@ -462,12 +462,12 @@ let lookup_borrow_opt (span : Meta.span) (ek : exploration_kind) method! visit_aborrow_content env bc = match bc with | AMutBorrow (pm, bid, av) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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 pm bid av | ASharedBorrow (pm, bid) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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 pm bid @@ -584,12 +584,12 @@ let update_aborrow (span : Meta.span) (ek : exploration_kind) (l : BorrowId.id) method! visit_ABorrow env bc = match bc with | AMutBorrow (pm, bid, av) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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 pm bid av) | ASharedBorrow (pm, bid) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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 pm bid) @@ -1199,11 +1199,11 @@ let get_first_non_ignored_aloan_in_abstraction (span : Meta.span) (abs : abs) : method! visit_aloan_content env lc = match lc with | AMutLoan (pm, bid, _) -> - (* Sanity check: markers can only appear when we're doing a join *) + (* Sanity check: projection 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: projection 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 = _ } -- cgit v1.2.3