diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 188 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 31 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 16 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 18 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 33 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 33 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 68 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 26 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 16 | ||||
| -rw-r--r-- | compiler/Values.ml | 12 |
10 files changed, 302 insertions, 139 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index ef958d2c..93238729 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -135,17 +135,19 @@ let end_borrow_get_borrow (span : Meta.span) * need it to properly instantiate the backward functions when generating * the pure translation. *) match lc with - | AMutLoan (_, _) -> + | AMutLoan (pm, _, _) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Nothing special to do *) super#visit_ALoan outer lc - | ASharedLoan (bids, v, av) -> + | ASharedLoan (pm, bids, v, av) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Explore the shared value - we need to update the outer borrows *) let souter = update_outer_borrows outer (Borrows bids) in let v = super#visit_typed_value souter v in (* Explore the child avalue - we keep the same outer borrows *) let av = super#visit_typed_avalue outer av in (* Reconstruct *) - ALoan (ASharedLoan (bids, v, av)) + ALoan (ASharedLoan (pm, bids, v, av)) | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan _ (* The loan has ended, so no need to update the outer borrows *) @@ -159,7 +161,8 @@ let end_borrow_get_borrow (span : Meta.span) method! visit_ABorrow outer bc = match bc with - | AMutBorrow (bid, _) -> + | AMutBorrow (pm, bid, _) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Check if this is the borrow we are looking for *) if bid = l then ( (* TODO: treat this case differently. We should not introduce @@ -188,7 +191,8 @@ let end_borrow_get_borrow (span : Meta.span) (* Update the outer borrows before diving into the child avalue *) let outer = update_outer_borrows outer (Borrow bid) in super#visit_ABorrow outer bc - | ASharedBorrow bid -> + | ASharedBorrow (pm, bid) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Check if this is the borrow we are looking for *) if bid = l then ( (* Check there are outer borrows, or if we need to end the whole @@ -338,7 +342,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) match nv.value with | VSymbolic sv -> let abs = Option.get opt_abs in - (* Remember the given back value as a span-value + (* Remember the given back value as a meta-value * TODO: it is a bit annoying to have to deconstruct * the value... Think about a more elegant way. *) let given_back_span = as_symbolic span nv.value in @@ -377,14 +381,15 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) ty in match lc with - | AMutLoan (bid', child) -> + | AMutLoan (pm, bid', child) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid' = bid then ( (* This is the loan we are looking for: apply the projection to * the value we give back and replaced this mutable loan with * an ended loan *) (* Register the insertion *) set_replaced (); - (* Remember the given back value as a span-value *) + (* Remember the given back value as a meta-value *) let given_back_span = nv in (* Apply the projection *) let given_back = @@ -397,7 +402,8 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) ALoan (AEndedMutLoan { child; given_back; given_back_span })) else (* Continue exploring *) super#visit_ALoan opt_abs lc - | ASharedLoan (_, _, _) -> + | ASharedLoan (pm, _, _, _) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* We are giving back a value to a *mutable* loan: nothing special to do *) super#visit_ALoan opt_abs lc | AEndedMutLoan { child = _; given_back = _; given_back_span = _ } @@ -408,7 +414,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id) (* This loan is ignored, but we may have to project on a subvalue * of the value which is given back *) if opt_bid = Some bid then - (* Remember the given back value as a span-value *) + (* Remember the given back value as a meta-value *) let given_back_span = nv in (* Note that we replace the ignored mut loan by an *ended* ignored * mut loan. Also, this is not the loan we are looking for *per se*: @@ -453,7 +459,7 @@ let give_back_symbolic_value (_config : config) (span : Meta.span) sanity_check __FILE__ __LINE__ (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) span; - (* Store the given-back value as a span-value for synthesis purposes *) + (* Store the given-back value as a meta-value for synthesis purposes *) let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) let subst (_abs : abs) local_given_back = @@ -531,7 +537,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span) method visit_typed_ALoan (opt_abs : abs option) (ty : rty) (lc : aloan_content) : avalue = match lc with - | AMutLoan (bid', child) -> + | AMutLoan (pm, bid', child) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; if bid' = bid then ( (* Sanity check - about why we need to call {!ty_get_ref} * (and don't do the same thing as in {!give_back_value}) @@ -553,12 +560,13 @@ let give_back_avalue_to_same_abstraction (_config : config) (span : Meta.span) (AEndedMutLoan { given_back = nv; child; given_back_span = nsv })) else (* Continue exploring *) super#visit_ALoan opt_abs lc - | ASharedLoan (_, _, _) + | ASharedLoan (PNone, _, _, _) (* We are giving back a value to a *mutable* loan: nothing special to do *) | AEndedMutLoan { given_back = _; child = _; given_back_span = _ } | AEndedSharedLoan (_, _) -> (* Nothing special to do *) super#visit_ALoan opt_abs lc + | ASharedLoan (_, _, _, _) -> internal_error __FILE__ __LINE__ span | AIgnoredMutLoan (bid_opt, child) -> (* This loan is ignored, but we may have to project on a subvalue * of the value which is given back *) @@ -631,10 +639,12 @@ let give_back_shared _config (span : Meta.span) (bid : BorrowId.id) method! visit_ALoan opt_abs lc = match lc with - | AMutLoan (bid, av) -> + | AMutLoan (pm, bid, av) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Nothing special to do (we are giving back a *shared* borrow) *) - ALoan (super#visit_AMutLoan opt_abs bid av) - | ASharedLoan (bids, shared_value, child) -> + ALoan (super#visit_AMutLoan opt_abs pm bid av) + | ASharedLoan (pm, bids, shared_value, child) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; if BorrowId.Set.mem bid bids then ( (* This is the loan we are looking for *) set_replaced (); @@ -646,7 +656,7 @@ let give_back_shared _config (span : Meta.span) (bid : BorrowId.id) else ALoan (ASharedLoan - (BorrowId.Set.remove bid bids, shared_value, child))) + (pm, BorrowId.Set.remove bid bids, shared_value, child))) else (* Not the loan we are looking for: continue exploring *) super#visit_ALoan opt_abs lc @@ -700,13 +710,14 @@ let reborrow_shared (span : Meta.span) (original_bid : BorrowId.id) VSharedLoan (bids', sv)) else super#visit_VSharedLoan env bids sv - method! visit_ASharedLoan env bids v av = + method! visit_ASharedLoan env pm bids v av = + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* This case is similar to the {!SharedLoan} case *) if BorrowId.Set.mem original_bid bids then ( set_ref (); let bids' = BorrowId.Set.add new_bid bids in - ASharedLoan (bids', v, av)) - else super#visit_ASharedLoan env bids v av + ASharedLoan (pm, bids', v, av)) + else super#visit_ASharedLoan env pm bids v av end in @@ -789,8 +800,9 @@ let give_back (config : config) (span : Meta.span) (l : BorrowId.id) span; (* Update the context *) give_back_shared config span l ctx - | Abstract (AMutBorrow (l', av)) -> + | Abstract (AMutBorrow (pm, l', av)) -> (* Sanity check *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; sanity_check __FILE__ __LINE__ (l' = l) span; (* Check that the corresponding loan is somewhere - purely a sanity check *) sanity_check __FILE__ __LINE__ @@ -806,8 +818,9 @@ let give_back (config : config) (span : Meta.span) (l : BorrowId.id) give_back_avalue_to_same_abstraction config span l av (mk_typed_value_from_symbolic_value sv) ctx - | Abstract (ASharedBorrow l') -> + | Abstract (ASharedBorrow (pm, l')) -> (* Sanity check *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; sanity_check __FILE__ __LINE__ (l' = l) span; (* Check that the borrow is somewhere - purely a sanity check *) sanity_check __FILE__ __LINE__ @@ -827,7 +840,7 @@ let give_back (config : config) (span : Meta.span) (l : BorrowId.id) let check_borrow_disappeared (span : Meta.span) (fun_name : string) (l : BorrowId.id) (ctx0 : eval_ctx) (ctx : eval_ctx) : unit = - (match lookup_borrow_opt ek_all l ctx with + (match lookup_borrow_opt span ek_all l ctx with | None -> () (* Ok *) | Some _ -> log#ltrace @@ -1205,7 +1218,8 @@ and end_abstraction_borrows (config : config) (span : Meta.span) ^ aborrow_content_to_string ~span:(Some span) ctx bc)); let ctx = match bc with - | AMutBorrow (bid, av) -> + | AMutBorrow (pm, bid, av) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* First, convert the avalue to a (fresh symbolic) value *) let sv = convert_avalue_to_given_back_value span av in (* Replace the mut borrow to register the fact that we ended @@ -1215,7 +1229,8 @@ and end_abstraction_borrows (config : config) (span : Meta.span) (* Give the value back *) let sv = mk_typed_value_from_symbolic_value sv in give_back_value config span bid sv ctx - | ASharedBorrow bid -> + | ASharedBorrow (pm, bid) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Replace the shared borrow to account for the fact it ended *) let ended_borrow = ABorrow AEndedSharedBorrow in let ctx = update_aborrow span ek_all bid ended_borrow ctx in @@ -1637,7 +1652,8 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) | ALoan lc -> ( (* Explore the loan content *) match lc with - | ASharedLoan (bids, sv, child_av) -> + | ASharedLoan (pm, bids, sv, child_av) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) @@ -1648,7 +1664,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) in (* Push a value *) let ignored = mk_aignored span child_av.ty in - let value = ALoan (ASharedLoan (bids, sv, ignored)) in + let value = ALoan (ASharedLoan (pm, bids, sv, ignored)) in push { value; ty }; (* Explore the child *) list_avalues false push_fail child_av; @@ -1659,12 +1675,13 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) exactly the same way as [list_avalues] (i.e., with a similar signature) *) List.iter push avl - | AMutLoan (bid, child_av) -> + | AMutLoan (pm, bid, child_av) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Explore the child *) list_avalues false push_fail child_av; (* Explore the whole loan *) let ignored = mk_aignored span child_av.ty in - let value = ALoan (AMutLoan (bid, ignored)) in + let value = ALoan (AMutLoan (pm, bid, ignored)) in push { value; ty } | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) @@ -1691,14 +1708,16 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) sanity_check __FILE__ __LINE__ allow_borrows span; (* Explore the borrow content *) match bc with - | AMutBorrow (bid, child_av) -> + | AMutBorrow (pm, bid, child_av) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Explore the child *) list_avalues false push_fail child_av; (* Explore the borrow *) let ignored = mk_aignored span child_av.ty in - let value = ABorrow (AMutBorrow (bid, ignored)) in + let value = ABorrow (AMutBorrow (pm, bid, ignored)) in push { value; ty } - | ASharedBorrow _ -> + | ASharedBorrow (pm, _) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Nothing specific to do: keep the value as it is *) push av | AIgnoredMutBorrow (opt_bid, child_av) -> @@ -1777,7 +1796,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) let sv = mk_value_with_fresh_sids sv in (* Create the new avalue *) let value = - ALoan (ASharedLoan (bids, sv, mk_aignored span ty)) + ALoan (ASharedLoan (PNone, bids, sv, mk_aignored span ty)) in { value; ty } in @@ -1900,7 +1919,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span "Nested borrows are not supported yet"; let ty = TRef (RFVar r_id, ref_ty, kind) in - let value = ABorrow (ASharedBorrow bid) in + let value = ABorrow (ASharedBorrow (PNone, bid)) in ([ { value; ty } ], v) | VMutBorrow (bid, bv) -> let r_id = if group then r_id else fresh_region_id () in @@ -1911,7 +1930,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *) let ty = TRef (RFVar r_id, ref_ty, kind) in let ignored = mk_aignored span ref_ty in - let av = ABorrow (AMutBorrow (bid, ignored)) in + let av = ABorrow (AMutBorrow (PNone, bid, ignored)) in let av = { value = av; ty } in (* Continue exploring, looking for loans (and forbidding borrows, because we don't support nested borrows for now) *) @@ -1937,7 +1956,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) let ignored = mk_aignored span ty in (* Rem.: the shared value might contain loans *) let avl, sv = to_avalues false true true r_id sv in - let av = ALoan (ASharedLoan (bids, sv, ignored)) in + let av = ALoan (ASharedLoan (PNone, bids, sv, ignored)) in let av = { value = av; ty } in (* Continue exploring, looking for loans (and forbidding borrows, because we don't support nested borrows for now) *) @@ -1954,7 +1973,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) "Nested borrows are not supported yet"; let ty = mk_ref_ty (RFVar r_id) ty RMut in let ignored = mk_aignored span ty in - let av = ALoan (AMutLoan (bid, ignored)) in + let av = ALoan (AMutLoan (PNone, bid, ignored)) in let av = { value = av; ty } in ([ av ], v)) | VSymbolic _ -> @@ -2085,8 +2104,14 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) in (* Register the loans *) (match lc with - | ASharedLoan (bids, _, _) -> push_loans bids (Abstract (ty, lc)) - | AMutLoan (bid, _) -> push_loan bid (Abstract (ty, lc)) + | ASharedLoan (pm, bids, _, _) -> + (* TODO: We should keep track of the marker here *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; + push_loans bids (Abstract (ty, lc)) + | AMutLoan (pm, bid, _) -> + (* TODO: We should keep track of the marker here *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; + push_loan bid (Abstract (ty, lc)) | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) @@ -2102,8 +2127,14 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) in (* Explore the borrow content *) (match bc with - | AMutBorrow (bid, _) -> push_borrow bid (Abstract (ty, bc)) - | ASharedBorrow bid -> push_borrow bid (Abstract (ty, bc)) + | AMutBorrow (pm, bid, _) -> + (* TODO: We should keep track of the marker here *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; + push_borrow bid (Abstract (ty, bc)) + | ASharedBorrow (pm, bid) -> + (* TODO: We should keep track of the marker here *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; + push_borrow bid (Abstract (ty, bc)) | AProjSharedBorrow asb -> let register asb = match asb with @@ -2140,29 +2171,50 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) type merge_duplicates_funcs = { merge_amut_borrows : - borrow_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue; + borrow_id -> + rty -> + proj_marker -> + typed_avalue -> + rty -> + proj_marker -> + typed_avalue -> + typed_avalue; (** Parameters: - [id] - [ty0] + - [pm0] - [child0] - [ty1] + - [pm1] - [child1] The children should be [AIgnored]. *) - merge_ashared_borrows : borrow_id -> rty -> rty -> typed_avalue; + merge_ashared_borrows : + borrow_id -> rty -> proj_marker -> rty -> proj_marker -> typed_avalue; (** Parameters: - [id] - [ty0] + - [pm0] - [ty1] + - [pm1] *) merge_amut_loans : - loan_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue; + loan_id -> + rty -> + proj_marker -> + typed_avalue -> + rty -> + proj_marker -> + typed_avalue -> + typed_avalue; (** Parameters: - [id] - [ty0] + - [pm0] - [child0] - [ty1] + - [pm1] - [child1] The children should be [AIgnored]. @@ -2170,18 +2222,22 @@ type merge_duplicates_funcs = { merge_ashared_loans : loan_id_set -> rty -> + proj_marker -> typed_value -> typed_avalue -> rty -> + proj_marker -> typed_value -> typed_avalue -> typed_avalue; (** Parameters: - [ids] - [ty0] + - [pm0] - [sv0] - [child0] - [ty1] + - [pm1] - [sv1] - [child1] *) @@ -2301,10 +2357,19 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) let merge_aborrow_contents (ty0 : rty) (bc0 : aborrow_content) (ty1 : rty) (bc1 : aborrow_content) : typed_avalue = match (bc0, bc1) with - | AMutBorrow (id, child0), AMutBorrow (_, child1) -> - (Option.get merge_funs).merge_amut_borrows id ty0 child0 ty1 child1 - | ASharedBorrow id, ASharedBorrow _ -> - (Option.get merge_funs).merge_ashared_borrows id ty0 ty1 + | AMutBorrow (pm0, id0, child0), AMutBorrow (pm1, id1, child1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + (* TODO: We should handle the markers here *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + (Option.get merge_funs).merge_amut_borrows id0 ty0 pm0 child0 ty1 pm1 + child1 + | ASharedBorrow (pm0, id0), ASharedBorrow (pm1, id1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + (* TODO: We should handle the markers here *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + (Option.get merge_funs).merge_ashared_borrows id0 ty0 pm0 ty1 pm1 | AProjSharedBorrow _, AProjSharedBorrow _ -> (* Unreachable because requires nested borrows *) craise __FILE__ __LINE__ span "Unreachable" @@ -2330,12 +2395,21 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty) (lc1 : aloan_content) : typed_avalue option = match (lc0, lc1) with - | AMutLoan (id, child0), AMutLoan (_, child1) -> + | AMutLoan (pm0, id0, child0), AMutLoan (pm1, id1, child1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + (* TODO: We should handle the markers here *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; (* Register the loan id *) - set_loan_as_merged id; + set_loan_as_merged id0; (* Merge *) - Some ((Option.get merge_funs).merge_amut_loans id ty0 child0 ty1 child1) - | ASharedLoan (ids0, sv0, child0), ASharedLoan (ids1, sv1, child1) -> + Some + ((Option.get merge_funs).merge_amut_loans id0 ty0 pm0 child0 ty1 pm1 + child1) + | ASharedLoan (pm0, ids0, sv0, child0), ASharedLoan (pm1, ids1, sv1, child1) + -> + (* TODO: We should handle the markers here *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; (* Filter the ids *) let ids0 = filter_bids ids0 in let ids1 = filter_bids ids1 in @@ -2368,8 +2442,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) set_loans_as_merged ids; (* Merge *) Some - ((Option.get merge_funs).merge_ashared_loans ids ty0 sv0 child0 ty1 - sv1 child1)) + ((Option.get merge_funs).merge_ashared_loans ids ty0 pm0 sv0 child0 + ty1 pm1 sv1 child1)) | _ -> (* Unreachable because those cases are ignored (ended/ignored borrows) or inconsistent *) @@ -2471,7 +2545,9 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty, lc) -> ( match lc with - | ASharedLoan (bids, sv, child) -> + | ASharedLoan (pm, bids, sv, child) -> + (* TODO: We should handle the markers here *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; let bids = filter_bids bids in sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) @@ -2481,7 +2557,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv.value)) span; - let lc = ASharedLoan (bids, sv, child) in + let lc = ASharedLoan (pm, bids, sv, child) in set_loans_as_merged bids; Some { value = ALoan lc; ty } | AMutLoan _ -> diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 56df9344..c119311f 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -138,29 +138,50 @@ val convert_value_to_abstractions : *) type merge_duplicates_funcs = { merge_amut_borrows : - borrow_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue; + borrow_id -> + rty -> + proj_marker -> + typed_avalue -> + rty -> + proj_marker -> + typed_avalue -> + typed_avalue; (** Parameters: - [id] - [ty0] + - [pm0] - [child0] - [ty1] + - [pm1] - [child1] The children should be [AIgnored]. *) - merge_ashared_borrows : borrow_id -> rty -> rty -> typed_avalue; + merge_ashared_borrows : + borrow_id -> rty -> proj_marker -> rty -> proj_marker -> typed_avalue; (** Parameters: - [id] - [ty0] + - [pm0] - [ty1] + - [pm1] *) merge_amut_loans : - loan_id -> rty -> typed_avalue -> rty -> typed_avalue -> typed_avalue; + loan_id -> + rty -> + proj_marker -> + typed_avalue -> + rty -> + proj_marker -> + typed_avalue -> + typed_avalue; (** Parameters: - [id] - [ty0] + - [pm0] - [child0] - [ty1] + - [pm1] - [child1] The children should be [AIgnored]. @@ -168,18 +189,22 @@ type merge_duplicates_funcs = { merge_ashared_loans : loan_id_set -> rty -> + proj_marker -> typed_value -> typed_avalue -> rty -> + proj_marker -> typed_value -> typed_avalue -> typed_avalue; (** Parameters: - [ids] - [ty0] + - [pm0] - [sv0] - [child0] - [ty1] + - [pm1] - [sv1] - [child1] *) diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 776cb6fa..7714f5bb 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -144,7 +144,7 @@ let eval_loop_symbolic (config : config) (span : span) ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Compute the end expression, that is the expresion corresponding to the - end of the functin where we call the loop (for now, when calling a loop + end of the function where we call the loop (for now, when calling a loop we never get out) *) let res_fun_end = comp cf_prepare @@ -255,10 +255,13 @@ let eval_loop_symbolic (config : config) (span : span) List.filter_map (fun (av : typed_avalue) -> match av.value with - | ABorrow (AMutBorrow (bid, child_av)) -> + | ABorrow (AMutBorrow (pm, bid, child_av)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span; Some (bid, child_av.ty) - | ABorrow (ASharedBorrow _) -> None + | ABorrow (ASharedBorrow (pm, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + None | _ -> craise __FILE__ __LINE__ span "Unreachable") borrows in @@ -268,10 +271,13 @@ let eval_loop_symbolic (config : config) (span : span) List.filter_map (fun (av : typed_avalue) -> match av.value with - | ALoan (AMutLoan (bid, child_av)) -> + | ALoan (AMutLoan (pm, bid, child_av)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span; Some bid - | ALoan (ASharedLoan _) -> None + | ALoan (ASharedLoan (pm, _, _, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + None | _ -> craise __FILE__ __LINE__ span "Unreachable") loans in diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 991f259f..675dc544 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -65,7 +65,7 @@ module type PrimMatcher = sig val match_distinct_adts : eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value - (** The span-value is the result of a match. + (** The meta-value is the result of a match. We take an additional function as input, which acts as a matcher over typed values, to be able to lookup the shared values and match them. @@ -158,8 +158,10 @@ module type PrimMatcher = sig (** Parameters: [ty0] + [pm0] [bid0] [ty1] + [pm1] [bid1] [ty]: result of matching ty0 and ty1 *) @@ -167,17 +169,21 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> borrow_id -> rty -> + proj_marker -> borrow_id -> rty -> typed_avalue (** Parameters: [ty0] + [pm0] [bid0] [av0] [ty1] + [pm1] [bid1] [av1] [ty]: result of matching ty0 and ty1 @@ -187,9 +193,11 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> @@ -198,10 +206,12 @@ module type PrimMatcher = sig (** Parameters: [ty0] + [pm0] [ids0] [v0] [av0] [ty1] + [pm1] [ids1] [v1] [av1] @@ -213,10 +223,12 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> loan_id_set -> typed_value -> typed_avalue -> rty -> + proj_marker -> loan_id_set -> typed_value -> typed_avalue -> @@ -227,9 +239,11 @@ module type PrimMatcher = sig (** Parameters: [ty0] + [pm0] [id0] [av0] [ty1] + [pm1] [id1] [av1] [ty]: result of matching ty0 and ty1 @@ -239,9 +253,11 @@ module type PrimMatcher = sig eval_ctx -> eval_ctx -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> + proj_marker -> borrow_id -> typed_avalue -> rty -> diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 1a0bb090..599fabfd 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -153,13 +153,19 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) *) let get_borrow_id (av : typed_avalue) : BorrowId.id = match av.value with - | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid + | ABorrow (AMutBorrow (pm, bid, _) | ASharedBorrow (pm, bid)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + bid | _ -> craise __FILE__ __LINE__ span "Unexpected" in let get_loan_id (av : typed_avalue) : BorrowId.id = match av.value with - | ALoan (AMutLoan (lid, _)) -> lid - | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids + | ALoan (AMutLoan (pm, lid, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + lid + | ALoan (ASharedLoan (pm, lids, _, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + BorrowId.Set.min_elt lids | _ -> craise __FILE__ __LINE__ span "Unexpected" in (* We use ordered maps to reorder the borrows and loans *) @@ -245,7 +251,8 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : SL {l0, l1} s0 ]} - and introduce the corresponding abstraction: + and introduce the corresponding abstraction for the borrow l0 + (and we do something similar for l1): {[ abs'2 { SB l0, SL {l2} s2 } ]} @@ -283,13 +290,13 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : (* Create the shared loan *) let loan_rty = TRef (RFVar nrid, rty, RShared) in let loan_value = - ALoan (ASharedLoan (BorrowId.Set.singleton nlid, nsv, child_av)) + ALoan (ASharedLoan (PNone, BorrowId.Set.singleton nlid, nsv, child_av)) in let loan_value = mk_typed_avalue span loan_rty loan_value in (* Create the shared borrow *) let borrow_rty = loan_rty in - let borrow_value = ABorrow (ASharedBorrow lid) in + let borrow_value = ABorrow (ASharedBorrow (PNone, lid)) in let borrow_value = mk_typed_avalue span borrow_rty borrow_value in (* Create the abstraction *) @@ -344,11 +351,11 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : (* Continue the exploration *) super#visit_VSharedLoan env lids sv - method! visit_ASharedLoan env lids sv av = + method! visit_ASharedLoan env pm lids sv av = collect_shared_value lids sv; (* Continue the exploration *) - super#visit_ASharedLoan env lids sv av + super#visit_ASharedLoan env pm lids sv av (** Check that there are no symbolic values with *borrows* inside the abstraction - shouldn't happen if the symbolic values are greedily @@ -905,7 +912,9 @@ let compute_fixed_point_id_correspondance (span : Meta.span) let lookup_shared_loan lid ctx : typed_value = match snd (lookup_loan span ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v - | Abstract (ASharedLoan (_, v, _)) -> v + | Abstract (ASharedLoan (pm, _, v, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + v | _ -> craise __FILE__ __LINE__ span "Unreachable" in let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in @@ -1044,7 +1053,7 @@ let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx) object (self) inherit [_] iter_env - method! visit_ASharedLoan inside_shared _ sv child_av = + method! visit_ASharedLoan inside_shared _ _ sv child_av = self#visit_typed_value true sv; self#visit_typed_avalue inside_shared child_av @@ -1094,7 +1103,9 @@ let compute_fp_ctx_symbolic_values (span : Meta.span) (ctx : eval_ctx) let v = match snd (lookup_loan span ek_all bid fp_ctx) with | Concrete (VSharedLoan (_, v)) -> v - | Abstract (ASharedLoan (_, v, _)) -> v + | Abstract (ASharedLoan (pm, _, v, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + v | _ -> craise __FILE__ __LINE__ span "Unreachable" in self#visit_typed_value env v diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index c67869ac..7ea442db 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -39,13 +39,13 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) *) let get_borrow_id (av : typed_avalue) : BorrowId.id = match av.value with - | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid + | ABorrow (AMutBorrow (_, bid, _) | ASharedBorrow (_, bid)) -> bid | _ -> craise __FILE__ __LINE__ span "Unexpected" in let get_loan_id (av : typed_avalue) : BorrowId.id = match av.value with - | ALoan (AMutLoan (lid, _)) -> lid - | ALoan (ASharedLoan (lids, _, _)) -> BorrowId.Set.min_elt lids + | ALoan (AMutLoan (_, lid, _)) -> lid + | ALoan (ASharedLoan (_, lids, _, _)) -> BorrowId.Set.min_elt lids | _ -> craise __FILE__ __LINE__ span "Unexpected" in (* We use ordered maps to reorder the borrows and loans *) @@ -314,11 +314,14 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) Note that the join matcher doesn't implement match functions for avalues (see the comments in {!MakeJoinMatcher}. *) - let merge_amut_borrows id ty0 child0 _ty1 child1 = + let merge_amut_borrows id ty0 pm0 child0 _ty1 pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + (* We need to pick a type for the avalue. The types on the left and on the right may use different regions: it doesn't really matter (here, we pick the one from the left), because we will merge those regions together @@ -326,11 +329,11 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) *) let ty = ty0 in let child = child0 in - let value = ABorrow (AMutBorrow (id, child)) in + let value = ABorrow (AMutBorrow (PNone, id, child)) in { value; ty } in - let merge_ashared_borrows id ty0 ty1 = + let merge_ashared_borrows id ty0 pm0 ty1 pm1 = (* Sanity checks *) let _ = let _, ty0, _ = ty_as_ref ty0 in @@ -343,23 +346,28 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) span in + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + (* Same remarks as for [merge_amut_borrows] *) let ty = ty0 in - let value = ABorrow (ASharedBorrow id) in + let value = ABorrow (ASharedBorrow (PNone, id)) in { value; ty } in - let merge_amut_loans id ty0 child0 _ty1 child1 = + let merge_amut_loans id ty0 pm0 child0 _ty1 pm1 child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; (* Same remarks as for [merge_amut_borrows] *) let ty = ty0 in let child = child0 in - let value = ALoan (AMutLoan (id, child)) in + let value = ALoan (AMutLoan (PNone, id, child)) in { value; ty } in - let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1 + let merge_ashared_loans ids ty0 pm0 (sv0 : typed_value) child0 _ty1 pm1 (sv1 : typed_value) child1 = (* Sanity checks *) sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; @@ -375,10 +383,13 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv1.value)) span; + (* TODO: Handle markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; + let ty = ty0 in let child = child0 in let sv = M.match_typed_values ctx ctx sv0 sv1 in - let value = ALoan (ASharedLoan (ids, sv, child)) in + let value = ALoan (ASharedLoan (PNone, ids, sv, child)) in { value; ty } in { diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index e25adb2c..729b248f 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -353,10 +353,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct | ABorrow bc0, ABorrow bc1 -> ( log#ldebug (lazy "match_typed_avalues: borrows"); match (bc0, bc1) with - | ASharedBorrow bid0, ASharedBorrow bid1 -> + | ASharedBorrow (pm0, bid0), ASharedBorrow (pm1, bid1) -> log#ldebug (lazy "match_typed_avalues: shared borrows"); - M.match_ashared_borrows ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty - | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) -> + M.match_ashared_borrows ctx0 ctx1 v0.ty pm0 bid0 v1.ty pm1 bid1 ty + | AMutBorrow (pm0, bid0, av0), AMutBorrow (pm1, bid1, av1) -> log#ldebug (lazy "match_typed_avalues: mut borrows"); log#ldebug (lazy @@ -364,7 +364,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut borrows: matched children values"); - M.match_amut_borrows ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av + M.match_amut_borrows ctx0 ctx1 v0.ty pm0 bid0 av0 v1.ty pm1 bid1 av1 + ty av | AIgnoredMutBorrow _, AIgnoredMutBorrow _ -> (* The abstractions are destructured: we shouldn't get there *) craise __FILE__ __LINE__ M.span "Unexpected" @@ -393,23 +394,25 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct (* TODO: maybe we should enforce that the ids are always exactly the same - without matching *) match (lc0, lc1) with - | ASharedLoan (ids0, sv0, av0), ASharedLoan (ids1, sv1, av1) -> + | ASharedLoan (pm0, ids0, sv0, av0), ASharedLoan (pm1, ids1, sv1, av1) + -> log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in sanity_check __FILE__ __LINE__ (not (value_has_borrows sv.value)) M.span; - M.match_ashared_loans ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 - av1 ty sv av - | AMutLoan (id0, av0), AMutLoan (id1, av1) -> + M.match_ashared_loans ctx0 ctx1 v0.ty pm0 ids0 sv0 av0 v1.ty pm1 + ids1 sv1 av1 ty sv av + | AMutLoan (pm0, id0, av0), AMutLoan (pm1, id1, av1) -> log#ldebug (lazy "match_typed_avalues: mut loans"); log#ldebug (lazy "match_typed_avalues: mut loans: matching children values"); let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut loans: matched children values"); - M.match_amut_loans ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av + M.match_amut_loans ctx0 ctx1 v0.ty pm0 id0 av0 v1.ty pm1 id1 av1 ty + av | AIgnoredMutLoan _, AIgnoredMutLoan _ | AIgnoredSharedLoan _, AIgnoredSharedLoan _ -> (* Those should have been filtered when destructuring the abstractions - @@ -504,13 +507,14 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) : typed_avalue = - let value = ABorrow (ASharedBorrow bid) in + let value = ABorrow (ASharedBorrow (PNone, bid)) in { value; ty = borrow_ty } in let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in let loan = - ASharedLoan (BorrowId.Set.singleton bid2, sv, mk_aignored span bv_ty) + ASharedLoan + (PNone, BorrowId.Set.singleton bid2, sv, mk_aignored span bv_ty) in (* Note that an aloan has a borrow type *) let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in @@ -604,13 +608,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let borrow_av = let ty = borrow_ty in - let value = ABorrow (AMutBorrow (bid0, mk_aignored span bv_ty)) in + let value = + ABorrow (AMutBorrow (PNone, bid0, mk_aignored span bv_ty)) + in mk_typed_avalue span ty value in let loan_av = let ty = borrow_ty in - let value = ALoan (AMutLoan (nbid, mk_aignored span bv_ty)) in + let value = ALoan (AMutLoan (PNone, nbid, mk_aignored span bv_ty)) in mk_typed_avalue span ty value in @@ -654,12 +660,12 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let bv_ty = bv.ty in cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span "Nested borrows are not supported yet"; - let value = ABorrow (AMutBorrow (bid, mk_aignored span bv_ty)) in + let value = ABorrow (AMutBorrow (PNone, bid, mk_aignored span bv_ty)) in { value; ty = borrow_ty } in let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in - let loan = AMutLoan (bid2, mk_aignored span bv_ty) in + let loan = AMutLoan (PNone, bid2, mk_aignored span bv_ty) in (* Note that an aloan has a borrow type *) let loan : typed_avalue = { value = ALoan loan; ty = borrow_ty } in @@ -1213,26 +1219,30 @@ struct let match_distinct_aadts _ _ _ _ _ _ _ = raise (Distinct "match_distinct_adts") - let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty - = + let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _ty1 pm1 + bid1 ty = + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; let bid = match_borrow_id bid0 bid1 in - let value = ABorrow (ASharedBorrow bid) in + let value = ABorrow (ASharedBorrow (PNone, bid)) in { value; ty } - let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1 - _av1 ty av = + let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 bid0 _av0 _ty1 + pm1 bid1 _av1 ty av = + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; let bid = match_borrow_id bid0 bid1 in - let value = ABorrow (AMutBorrow (bid, av)) in + let value = ABorrow (AMutBorrow (PNone, bid, av)) in { value; ty } - let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1 - ids1 _v1 _av1 ty v av = + let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 pm0 ids0 _v0 _av0 + _ty1 pm1 ids1 _v1 _av1 ty v av = + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; let bids = match_loan_ids ids0 ids1 in - let value = ALoan (ASharedLoan (bids, v, av)) in + let value = ALoan (ASharedLoan (PNone, bids, v, av)) in { value; ty } - let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 - id1 _av1 ty av = + let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 pm0 id0 _av0 + _ty1 pm1 id1 _av1 ty av = + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; log#ldebug (lazy ("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: " @@ -1241,7 +1251,7 @@ struct ^ typed_avalue_to_string ~span:(Some span) ctx1 av)); let id = match_loan_id id0 id1 in - let value = ALoan (AMutLoan (id, av)) in + let value = ALoan (AMutLoan (PNone, id, av)) in { value; ty } let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = @@ -1706,7 +1716,9 @@ let match_ctx_with_target (config : config) (span : Meta.span) let lookup_shared_loan lid ctx : typed_value = match snd (lookup_loan span ek_all lid ctx) with | Concrete (VSharedLoan (_, v)) -> v - | Abstract (ASharedLoan (_, v, _)) -> v + | Abstract (ASharedLoan (pm, _, v, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + v | _ -> craise __FILE__ __LINE__ span "Unreachable" in let lookup_in_src id = lookup_shared_loan id src_ctx in diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index bcf92b25..fc882423 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -150,8 +150,8 @@ let check_loans_borrows_relation_invariant (span : Meta.span) (ctx : eval_ctx) : method! visit_aloan_content inside_abs lc = let _ = match lc with - | AMutLoan (bid, _) -> register_mut_loan inside_abs bid - | ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids + | AMutLoan (_, bid, _) -> register_mut_loan inside_abs bid + | ASharedLoan (_, bids, _, _) -> register_shared_loan inside_abs bids | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan RMut bid | AIgnoredMutLoan (None, _) | AIgnoredSharedLoan _ @@ -522,7 +522,8 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = match glc with | Concrete (VMutBorrow (_, bv)) -> sanity_check __FILE__ __LINE__ (bv.ty = ty) span - | Abstract (AMutBorrow (_, sv)) -> + | Abstract (AMutBorrow (pm, _, sv)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = ty) span @@ -612,15 +613,17 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | ABottom, _ -> (* Nothing to check *) () | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with - | AMutBorrow (_, av), RMut -> + | AMutBorrow (pm, _, av), RMut -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Check that the child value has the proper type *) sanity_check __FILE__ __LINE__ (av.ty = ref_ty) span - | ASharedBorrow bid, RShared -> ( + | ASharedBorrow (pm, bid), RShared -> ( + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* 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, _)) -> + | Abstract (ASharedLoan (_, _, sv, _)) -> sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions ref_ty) span @@ -635,8 +638,8 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | _ -> craise __FILE__ __LINE__ span "Inconsistent context") | ALoan lc, aty -> ( match lc with - | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) - -> ( + | AMutLoan (PNone, bid, child_av) + | AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span; (* Lookup the borrowed value to check it has the proper type *) @@ -646,22 +649,25 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = sanity_check __FILE__ __LINE__ (bv.ty = Substitute.erase_regions borrowed_aty) span - | Abstract (AMutBorrow (_, sv)) -> + | Abstract (AMutBorrow (_, _, sv)) -> sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = Substitute.erase_regions borrowed_aty) span | _ -> craise __FILE__ __LINE__ span "Inconsistent context") + | AMutLoan (_, _, _) -> internal_error __FILE__ __LINE__ span | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span - | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> + | ASharedLoan (PNone, _, sv, child_av) + | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in sanity_check __FILE__ __LINE__ (sv.ty = Substitute.erase_regions borrowed_aty) span; (* TODO: the type of aloans doesn't make sense, see above *) sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) span + | ASharedLoan (_, _, _, _) -> internal_error __FILE__ __LINE__ span | AEndedMutLoan { given_back; child; given_back_span = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_span = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 8dfe0abe..71f8e4fc 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1666,7 +1666,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) value (** Explore an abstraction value and convert it to a consumed value - by collecting all the span-values from the ended *loans*. + by collecting all the meta-values from the ended *loans*. Consumed values are rvalues because when an abstraction ends we introduce a call to a backward function in the synthesized program, @@ -1720,10 +1720,10 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (lc : V.aloan_content) : texpression option = match lc with - | AMutLoan (_, _) | ASharedLoan (_, _, _) -> + | AMutLoan (_, _, _) | ASharedLoan (_, _, _, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_span } -> - (* Return the span-value *) + (* Return the meta-value *) Some (typed_value_to_texpression ctx ectx given_back_span) | AEndedSharedLoan (_, _) -> (* We don't dive into shared loans: there is nothing to give back @@ -1744,7 +1744,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : texpression option = match bc with - | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> + | V.AMutBorrow (_, _, _) | ASharedBorrow (_, _) | AIgnoredMutBorrow (_, _) -> craise __FILE__ __LINE__ _ctx.span "Unreachable" | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) @@ -1804,7 +1804,7 @@ let translate_opt_mplace (p : S.mplace option) : mplace option = match p with None -> None | Some p -> Some (translate_mplace p) (** Explore an abstraction value and convert it to a given back value - by collecting all the span-values from the ended *borrows*. + by collecting all the meta-values from the ended *borrows*. Given back values are patterns, because when an abstraction ends, we introduce a call to a backward function in the synthesized program, @@ -1867,7 +1867,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match lc with - | AMutLoan (_, _) | ASharedLoan (_, _, _) -> + | AMutLoan (_, _, _) | ASharedLoan (_, _, _, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_span = _ } | AEndedSharedLoan (_, _) -> @@ -1886,7 +1886,7 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match bc with - | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> + | V.AMutBorrow (_, _, _) | ASharedBorrow (_, _) | AIgnoredMutBorrow (_, _) -> craise __FILE__ __LINE__ ctx.span "Unreachable" | AEndedMutBorrow (msv, _) -> (* Return the span-symbolic-value *) @@ -1912,7 +1912,7 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : ctx.span "Nested borrows are not supported yet"; (ctx, None) | AEndedProjBorrows mv -> - (* Return the span-value *) + (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in (ctx, Some (mk_typed_pattern_from_var var mp)) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> diff --git a/compiler/Values.ml b/compiler/Values.ml index 96d61f88..ca33604d 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -153,7 +153,7 @@ and typed_value = { value : value; ty : ty } (** "Meta"-value: information we store for the synthesis. - Note that we never automatically visit the span-values with the + Note that we never automatically visit the meta-values with the visitors: they really are span information, and shouldn't be considered as part of the environment during a symbolic execution. @@ -166,7 +166,7 @@ type mvalue = typed_value [@@deriving show, ord] See the explanations for {!mvalue} - TODO: we may want to create wrappers, to prevent mixing span values + TODO: we may want to create wrappers, to prevent mixing meta values and regular values. *) type msymbolic_value = symbolic_value [@@deriving show, ord] @@ -278,7 +278,7 @@ and aproj = 'a and one for 'b. We accumulate those values in the list of projections (note that - the span value stores the value which was given back). + the meta value stores the value which was given back). We can later end the projector of loans if [s@0] is not referenced anywhere in the context below a projector of borrows which intersects @@ -290,14 +290,14 @@ and aproj = Also note that once given to a borrow projection, a symbolic value can't get updated/expanded: this means that we don't need to save - any span-value here. + any meta-value here. *) | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list (** An ended projector of loans over a symbolic value. See the explanations for {!AProjLoans} - Note that we keep the original symbolic value as a span-value. + Note that we keep the original symbolic value as a meta-value. *) | AEndedProjBorrows of msymbolic_value (** The only purpose of {!AEndedProjBorrows} is to store, for synthesis @@ -621,7 +621,7 @@ and aborrow_content = *) | AEndedMutBorrow of msymbolic_value * typed_avalue (** The sole purpose of {!AEndedMutBorrow} is to store the (symbolic) value - that we gave back as a span-value, to help with the synthesis. + that we gave back as a meta-value, to help with the synthesis. *) | AEndedSharedBorrow (** We don't really need {!AEndedSharedBorrow}: we simply want to be |