diff options
| author | Son HO | 2024-06-04 14:05:44 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-04 14:05:44 +0200 |
| commit | afc4e62ce7a584da0bb0a7350533e321388be545 (patch) | |
| tree | 89f3b6999e1697595f1c3fbb2d9c4d8c60a69e49 | |
| parent | 4a31acdff7a5dfdc26bf25ad25bb8266b790f891 (diff) | |
| parent | 3ad6c4712fd41efec55f29af5ccc31f68a0e12cf (diff) | |
Merge pull request #228 from AeneasVerif/son/loops2
Add support for projection markers when joining environments
Diffstat (limited to '')
31 files changed, 2143 insertions, 1149 deletions
diff --git a/compiler/Cps.ml b/compiler/Cps.ml index 142c2b08..f7694ba2 100644 --- a/compiler/Cps.ml +++ b/compiler/Cps.ml @@ -106,6 +106,12 @@ let cc_singleton file line span cf el = | Some _ -> internal_error file line span | _ -> None +let cf_singleton file line span el = + match el with + | Some [ e ] -> Some e + | Some _ -> internal_error file line span + | _ -> None + (** It happens that we need to concatenate lists of results, for instance when evaluating the branches of a match. When applying the continuations to build the symbolic expressions, we need diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index ef958d2c..dee4903c 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,15 @@ 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 (_, _, _, _) -> + (* We get there if the projection marker is not [PNone] *) + 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 +641,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 +658,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 +712,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 +802,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 +820,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 +842,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 +1220,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 +1231,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 +1654,7 @@ 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) -> (* We don't support nested borrows for now *) cassert __FILE__ __LINE__ (not (value_has_borrows ctx sv.value)) @@ -1648,7 +1665,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 +1676,12 @@ 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) -> (* 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,12 +1708,12 @@ 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) -> (* 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 _ -> (* Nothing specific to do: keep the value as it is *) @@ -1777,7 +1794,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 +1917,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 +1928,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 +1954,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 +1971,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 _ -> @@ -1974,7 +1991,9 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind) (* Return *) List.rev !absl -type borrow_or_loan_id = BorrowId of borrow_id | LoanId of loan_id +type marker_borrow_or_loan_id = + | BorrowId of proj_marker * borrow_id + | LoanId of proj_marker * loan_id type g_loan_content_with_ty = (ety * loan_content, rty * aloan_content) concrete_or_abs @@ -1983,12 +2002,12 @@ type g_borrow_content_with_ty = (ety * borrow_content, rty * aborrow_content) concrete_or_abs type merge_abstraction_info = { - loans : loan_id_set; - borrows : borrow_id_set; - borrows_loans : borrow_or_loan_id list; + loans : MarkerBorrowId.Set.t; + borrows : MarkerBorrowId.Set.t; + borrows_loans : marker_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 BorrowId.Map.t; - borrow_to_content : g_borrow_content_with_ty BorrowId.Map.t; + loan_to_content : g_loan_content_with_ty MarkerBorrowId.Map.t; + borrow_to_content : g_borrow_content_with_ty MarkerBorrowId.Map.t; } (** Small utility to help merging abstractions. @@ -1996,7 +2015,7 @@ type merge_abstraction_info = { 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_into_abstraction]: we + Note that this function is very specific to [merge_into_first_abstraction]: we have strong assumptions about the shape of the abstraction, and in particular that: - its values don't contain nested borrows @@ -2004,46 +2023,41 @@ type merge_abstraction_info = { contain shared loans). *) let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) - (abs : abs) : merge_abstraction_info = - let loans : loan_id_set ref = ref BorrowId.Set.empty in - let borrows : borrow_id_set ref = ref BorrowId.Set.empty in - let borrows_loans : borrow_or_loan_id list ref = ref [] in - let loan_to_content : g_loan_content_with_ty BorrowId.Map.t ref = - ref BorrowId.Map.empty - in - let borrow_to_content : g_borrow_content_with_ty BorrowId.Map.t ref = - ref BorrowId.Map.empty - in - - let push_loans ids (lc : g_loan_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) span; - loans := BorrowId.Set.union !loans ids; - BorrowId.Set.iter - (fun id -> - sanity_check __FILE__ __LINE__ - (not (BorrowId.Map.mem id !loan_to_content)) - span; - loan_to_content := BorrowId.Map.add id lc !loan_to_content; - borrows_loans := LoanId id :: !borrows_loans) - ids + (avalues : typed_avalue list) : merge_abstraction_info = + let loans : MarkerBorrowId.Set.t ref = ref MarkerBorrowId.Set.empty in + let borrows : MarkerBorrowId.Set.t ref = ref MarkerBorrowId.Set.empty in + let borrows_loans : marker_borrow_or_loan_id list ref = ref [] in + let loan_to_content : g_loan_content_with_ty MarkerBorrowId.Map.t ref = + ref MarkerBorrowId.Map.empty + in + let borrow_to_content : g_borrow_content_with_ty MarkerBorrowId.Map.t ref = + ref MarkerBorrowId.Map.empty in - let push_loan id (lc : g_loan_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) span; - loans := BorrowId.Set.add id !loans; + + let push_loan pm id (lc : g_loan_content_with_ty) : unit = + sanity_check __FILE__ __LINE__ + (not (MarkerBorrowId.Set.mem (pm, id) !loans)) + span; + loans := MarkerBorrowId.Set.add (pm, id) !loans; sanity_check __FILE__ __LINE__ - (not (BorrowId.Map.mem id !loan_to_content)) + (not (MarkerBorrowId.Map.mem (pm, id) !loan_to_content)) span; - loan_to_content := BorrowId.Map.add id lc !loan_to_content; - borrows_loans := LoanId id :: !borrows_loans + loan_to_content := MarkerBorrowId.Map.add (pm, id) lc !loan_to_content; + borrows_loans := LoanId (pm, id) :: !borrows_loans + in + let push_loans pm ids lc : unit = + BorrowId.Set.iter (fun id -> push_loan pm id lc) ids in - let push_borrow id (bc : g_borrow_content_with_ty) : unit = - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) span; - borrows := BorrowId.Set.add id !borrows; + let push_borrow pm id (bc : g_borrow_content_with_ty) : unit = sanity_check __FILE__ __LINE__ - (not (BorrowId.Map.mem id !borrow_to_content)) + (not (MarkerBorrowId.Set.mem (pm, id) !borrows)) span; - borrow_to_content := BorrowId.Map.add id bc !borrow_to_content; - borrows_loans := BorrowId id :: !borrows_loans + borrows := MarkerBorrowId.Set.add (pm, id) !borrows; + sanity_check __FILE__ __LINE__ + (not (MarkerBorrowId.Map.mem (pm, id) !borrow_to_content)) + span; + borrow_to_content := MarkerBorrowId.Map.add (pm, id) bc !borrow_to_content; + borrows_loans := BorrowId (pm, id) :: !borrows_loans in let iter_avalues = @@ -2058,19 +2072,11 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) method! visit_typed_value _ (v : typed_value) = super#visit_typed_value (Some (Concrete 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 _ -> craise __FILE__ __LINE__ span "Unreachable" - in - (match lc with - | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc)) - | VMutLoan _ -> craise __FILE__ __LINE__ span "Unreachable"); - (* Continue *) - super#visit_loan_content env lc + method! visit_loan_content _ _ = + (* Could happen if we explore shared values whose sub-values are + reborrowed. We use the fact that we destructure the nested shared + loans before reducing a context or computing a join. *) + craise __FILE__ __LINE__ span "Unreachable" method! visit_borrow_content _ _ = (* Can happen if we explore shared values which contain borrows - @@ -2085,8 +2091,8 @@ 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, _, _) -> push_loans pm bids (Abstract (ty, lc)) + | AMutLoan (pm, bid, _) -> push_loan pm bid (Abstract (ty, lc)) | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) @@ -2102,12 +2108,12 @@ 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, _) | ASharedBorrow (pm, bid) -> + push_borrow pm bid (Abstract (ty, bc)) | AProjSharedBorrow asb -> let register asb = match asb with - | AsbBorrow bid -> push_borrow bid (Abstract (ty, bc)) + | AsbBorrow bid -> push_borrow PNone bid (Abstract (ty, bc)) | AsbProjReborrows _ -> (* Can only happen if the symbolic value (potentially) contains borrows - i.e., we have nested borrows *) @@ -2128,7 +2134,7 @@ let compute_merge_abstraction_info (span : Meta.span) (ctx : eval_ctx) end in - List.iter (iter_avalues#visit_typed_avalue None) abs.avalues; + List.iter (iter_avalues#visit_typed_avalue None) avalues; { loans = !loans; @@ -2140,29 +2146,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,46 +2197,128 @@ 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] *) } -(** Auxiliary function. +(** Small utility: if a value doesn't have any marker, split it into two values + with complementary markers. We use this for {!merge_abstractions}. - Merge two abstractions into one, without updating the context. + We assume the value has been destructured (there are no nested loans, + adts, the children are ignored, etc.). *) -let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) - (can_end : bool) (merge_funs : merge_duplicates_funcs option) - (ctx : eval_ctx) (abs0 : abs) (abs1 : abs) : abs = - log#ldebug - (lazy - ("merge_into_abstraction_aux:\n- abs0:\n" - ^ abs_to_string span ctx abs0 - ^ "\n\n- abs1:\n" - ^ abs_to_string span ctx abs1)); +let typed_avalue_split_marker (span : Meta.span) (ctx : eval_ctx) + (av : typed_avalue) : typed_avalue list = + let mk_split pm mk_value = + if pm = PNone then [ mk_value PLeft; mk_value PRight ] else [ av ] + in + match av.value with + | AAdt _ | ABottom | ASymbolic _ | AIgnored -> + craise __FILE__ __LINE__ span "Unexpected" + | ABorrow bc -> ( + match bc with + | AMutBorrow (pm, bid, child) -> + sanity_check __FILE__ __LINE__ (is_aignored child.value) span; + let mk_value pm = + { av with value = ABorrow (AMutBorrow (pm, bid, child)) } + in + mk_split pm mk_value + | ASharedBorrow (pm, bid) -> + let mk_value pm = + { av with value = ABorrow (ASharedBorrow (pm, bid)) } + in + mk_split pm mk_value + | _ -> craise __FILE__ __LINE__ span "Unsupported yet") + | ALoan lc -> ( + match lc with + | AMutLoan (pm, bid, child) -> + sanity_check __FILE__ __LINE__ (is_aignored child.value) span; + let mk_value pm = + { av with value = ALoan (AMutLoan (pm, bid, child)) } + in + mk_split pm mk_value + | ASharedLoan (pm, bids, sv, child) -> + sanity_check __FILE__ __LINE__ (is_aignored child.value) span; + sanity_check __FILE__ __LINE__ + (not (value_has_borrows ctx sv.value)) + span; + let mk_value pm = + { av with value = ALoan (ASharedLoan (pm, bids, sv, child)) } + in + mk_split pm mk_value + | _ -> craise __FILE__ __LINE__ span "Unsupported yet") - (* Check that the abstractions are destructured *) - if !Config.sanity_checks then ( - let destructure_shared_values = true in - sanity_check __FILE__ __LINE__ - (abs_is_destructured span destructure_shared_values ctx abs0) - span; - sanity_check __FILE__ __LINE__ - (abs_is_destructured span destructure_shared_values ctx abs1) - span); +let abs_split_markers (span : Meta.span) (ctx : eval_ctx) (abs : abs) : abs = + { + abs with + avalues = + List.concat (List.map (typed_avalue_split_marker span ctx) abs.avalues); + } + +(** Auxiliary function for {!merge_abstractions}. + + Phase 1 of the merge: we simplify all loan/borrow pairs, if a loan is + in the left abstraction and its corresponding borrow is in the right + abstraction. + + Important: this is asymmetric (the loan must be in the left abstraction). + + Example: + {[ + abs0 { ML l0, MB l1 } |><| abs1 { MB l0 } + ~~> abs1 { MB l1 } + ]} + + But: + {[ + abs1 { MB l0 } |><| abs0 { ML l0, MB l1 } + ~~> abs1 { MB l0, ML l0, MB l1 } + ]} + + We return the list of merged values. + *) +let merge_abstractions_merge_loan_borrow_pairs (span : Meta.span) + (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs) + (abs1 : abs) : typed_avalue list = + log#ldebug (lazy "merge_abstractions_merge_loan_borrow_pairs"); + + (* Split the markers inside the abstractions (if we allow using markers). + + We do so because it enables simplification later when we are in the following case: + {[ + abs0 { ML l0 } |><| abs1 { |MB l0|, MB l1 } + ]} + + If we split before merging we get: + {[ + abs0 { |ML l0|, ︙ML l0︙ } |><| abs1 { |MB l0|, |MB l1|, ︙MB l1︙ } + ~~> merge + abs2 { ︙ML l0︙, |MB l1|, ︙MB l1︙ } + ~~> simplify the complementary markers + abs2 { ︙ML l0︙, MB l1 } + ]} + *) + let abs0, abs1 = + if merge_funs = None then (abs0, abs1) + else (abs_split_markers span ctx abs0, abs_split_markers span ctx abs1) + in (* Compute the relevant information *) let { @@ -2219,7 +2328,7 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) loan_to_content = loan_to_content0; borrow_to_content = borrow_to_content0; } = - compute_merge_abstraction_info span ctx abs0 + compute_merge_abstraction_info span ctx abs0.avalues in let { @@ -2229,16 +2338,27 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) loan_to_content = loan_to_content1; borrow_to_content = borrow_to_content1; } = - compute_merge_abstraction_info span ctx abs1 + compute_merge_abstraction_info span ctx abs1.avalues in - (* Sanity check: there is no loan/borrows which appears in both abstractions, - unless we allow to merge duplicates *) + (* Sanity check: no markers appear unless we allow merging duplicates *) if merge_funs = None then ( sanity_check __FILE__ __LINE__ - (BorrowId.Set.disjoint borrows0 borrows1) + (List.for_all + (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) + borrows_loans0) span; - sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) span); + sanity_check __FILE__ __LINE__ + (List.for_all + (function LoanId (pm, _) | BorrowId (pm, _) -> pm = PNone) + borrows_loans1) + span; + sanity_check __FILE__ __LINE__ + (MarkerBorrowId.Set.disjoint borrows0 borrows1) + span; + sanity_check __FILE__ __LINE__ + (MarkerBorrowId.Set.disjoint loans0 loans1) + span); (* Merge. There are several cases: @@ -2248,23 +2368,25 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) - 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: + Note that we may need to merge strictly more than two 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. + then their sets of ids are equal, and fail if it is not the case. + Remark: a way of solving this problem would be to destructure shared loans + so that they always have exactly one id. *) - let merged_borrows = ref BorrowId.Set.empty in - let merged_loans = ref BorrowId.Set.empty in + let merged_borrows = ref MarkerBorrowId.Set.empty in + let merged_loans = ref MarkerBorrowId.Set.empty in let avalues = ref [] in let push_avalue av = log#ldebug (lazy - ("merge_into_abstraction_aux: push_avalue: " + ("merge_abstractions_merge_loan_borrow_pairs: push_avalue: " ^ typed_avalue_to_string ~span:(Some span) ctx av)); avalues := av :: !avalues in @@ -2272,139 +2394,55 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) match av with None -> () | Some av -> push_avalue av in - let intersect = - BorrowId.Set.union - (BorrowId.Set.inter loans0 borrows1) - (BorrowId.Set.inter loans1 borrows0) - in - let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t = - let bids = BorrowId.Set.diff bids intersect in - sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span; - bids + (* Compute the intersection of: + - the loans coming from the left abstraction + - the borrows coming from the right abstraction *) + let intersect = MarkerBorrowId.Set.inter loans0 borrows1 in + + (* This function is called when handling shared loans: we have to apply a projection + marker to a set of borrow ids. *) + let filter_bids (pm : proj_marker) (bids : BorrowId.Set.t) : BorrowId.Set.t = + let bids = + BorrowId.Set.to_seq bids + |> Seq.map (fun x -> (pm, x)) + |> MarkerBorrowId.Set.of_seq + in + let bids = MarkerBorrowId.Set.diff bids intersect in + sanity_check __FILE__ __LINE__ (not (MarkerBorrowId.Set.is_empty bids)) span; + MarkerBorrowId.Set.to_seq bids |> Seq.map snd |> BorrowId.Set.of_seq in - let filter_bid (bid : BorrowId.id) : BorrowId.id option = - if BorrowId.Set.mem bid intersect then None else Some bid + let filter_bid (bid : marker_borrow_id) : marker_borrow_id option = + if MarkerBorrowId.Set.mem bid intersect then None else Some bid in - let borrow_is_merged id = BorrowId.Set.mem id !merged_borrows in + let borrow_is_merged id = MarkerBorrowId.Set.mem id !merged_borrows in let set_borrow_as_merged id = - merged_borrows := BorrowId.Set.add id !merged_borrows + merged_borrows := MarkerBorrowId.Set.add id !merged_borrows in - let loan_is_merged id = BorrowId.Set.mem id !merged_loans in + let loan_is_merged id = MarkerBorrowId.Set.mem id !merged_loans in let set_loan_as_merged id = - merged_loans := BorrowId.Set.add id !merged_loans - in - let set_loans_as_merged ids = BorrowId.Set.iter set_loan_as_merged ids in - - (* Some utility functions *) - (* Merge two aborrow contents - note that those contents must have the same id *) - 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 - | AProjSharedBorrow _, AProjSharedBorrow _ -> - (* Unreachable because requires nested borrows *) - craise __FILE__ __LINE__ span "Unreachable" - | _ -> - (* Unreachable because those cases are ignored (ended/ignored borrows) - or inconsistent *) - craise __FILE__ __LINE__ span "Unreachable" - in - - let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) - (bc1 : g_borrow_content_with_ty) : typed_avalue = - match (bc0, bc1) with - | Concrete _, Concrete _ -> - (* This can happen only in case of nested borrows *) - craise __FILE__ __LINE__ span "Unreachable" - | Abstract (ty0, bc0), Abstract (ty1, bc1) -> - merge_aborrow_contents ty0 bc0 ty1 bc1 - | Concrete _, Abstract _ | Abstract _, Concrete _ -> - (* TODO: is it really unreachable? *) - craise __FILE__ __LINE__ span "Unreachable" - in - - 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) -> - (* Register the loan id *) - set_loan_as_merged id; - (* Merge *) - Some ((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 *) - sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span; - let ids = ids0 in - if BorrowId.Set.is_empty ids then ( - (* If the set of ids is empty, we can eliminate this shared loan. - For now, we check that we can eliminate the whole shared value - altogether. - A more complete approach would be to explore the value and introduce - as many shared loans/borrows/etc. as necessary for the sub-values. - For now, we check that there are no such values that we would need - to preserve (in practice it works because we destructure the - shared values in the abstractions, and forbid nested borrows). - *) - sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv0.value)) - span; - sanity_check __FILE__ __LINE__ - (not (value_has_loans_or_borrows ctx sv0.value)) - span; - sanity_check __FILE__ __LINE__ (is_aignored child0.value) span; - sanity_check __FILE__ __LINE__ (is_aignored child1.value) span; - None) - else ( - (* Register the loan ids *) - set_loans_as_merged ids; - (* Merge *) - Some - ((Option.get merge_funs).merge_ashared_loans ids ty0 sv0 child0 ty1 - sv1 child1)) - | _ -> - (* Unreachable because those cases are ignored (ended/ignored borrows) - or inconsistent *) - craise __FILE__ __LINE__ span "Unreachable" + merged_loans := MarkerBorrowId.Set.add id !merged_loans in - - (* 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) : typed_avalue option = - match (lc0, lc1) with - | Concrete _, Concrete _ -> - (* This can not happen: the values should have been destructured *) - craise __FILE__ __LINE__ span "Unreachable" - | Abstract (ty0, lc0), Abstract (ty1, lc1) -> - merge_aloan_contents ty0 lc0 ty1 lc1 - | Concrete _, Abstract _ | Abstract _, Concrete _ -> - (* TODO: is it really unreachable? *) - craise __FILE__ __LINE__ span "Unreachable" + let set_loans_as_merged pm ids = + BorrowId.Set.elements ids + |> List.map (fun x -> (pm, x)) + |> List.iter set_loan_as_merged in - (* Note that we first explore the borrows/loans of [abs1], because we + (* Note that we first explore the borrows/loans of [abs0], because we want to merge *into* this abstraction, and as a consequence we want to preserve its structure as much as we can *) - let borrows_loans = List.append borrows_loans1 borrows_loans0 in + let borrows_loans = List.append borrows_loans0 borrows_loans1 in (* Iterate over all the borrows/loans ids found in the abstractions *) List.iter (fun bl -> match bl with - | BorrowId bid -> + | BorrowId (pm, bid) -> + let bid = (pm, bid) in log#ldebug (lazy - ("merge_into_abstraction_aux: merging borrow " - ^ BorrowId.to_string bid)); + ("merge_abstractions: merging borrow " + ^ MarkerBorrowId.to_string bid)); (* Check if the borrow has already been merged - this can happen because we go through all the borrows/loans in [abs0] *then* @@ -2418,8 +2456,8 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) | None -> () | Some bid -> (* Lookup the contents *) - let bc0 = BorrowId.Map.find_opt bid borrow_to_content0 in - let bc1 = BorrowId.Map.find_opt bid borrow_to_content1 in + let bc0 = MarkerBorrowId.Map.find_opt bid borrow_to_content0 in + let bc1 = MarkerBorrowId.Map.find_opt bid borrow_to_content1 in (* Merge *) let av : typed_avalue = match (bc0, bc1) with @@ -2432,13 +2470,17 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) *) craise __FILE__ __LINE__ span "Unreachable" | Abstract (ty, bc) -> { value = ABorrow bc; ty }) - | Some bc0, Some bc1 -> - sanity_check __FILE__ __LINE__ (merge_funs <> None) span; - merge_g_borrow_contents bc0 bc1 + | Some _, Some _ -> + (* Because of markers, the case where the same borrow is duplicated should + be unreachable. Note, this is due to all shared borrows currently + taking different ids, this will not be the case anymore when shared loans + will take a unique id instead of a set *) + craise __FILE__ __LINE__ span "Unreachable" | None, None -> craise __FILE__ __LINE__ span "Unreachable" in push_avalue av) - | LoanId bid -> + | LoanId (pm, bid) -> + let bid = (pm, bid) in if (* Check if the loan has already been treated - it can happen for the same reason as for borrows, and also because shared @@ -2450,16 +2492,16 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) else ( log#ldebug (lazy - ("merge_into_abstraction_aux: merging loan " - ^ BorrowId.to_string bid)); + ("merge_abstractions: merging loan " + ^ MarkerBorrowId.to_string bid)); (* Check if we need to filter it *) match filter_bid bid with | None -> () | Some bid -> (* Lookup the contents *) - let lc0 = BorrowId.Map.find_opt bid loan_to_content0 in - let lc1 = BorrowId.Map.find_opt bid loan_to_content1 in + let lc0 = MarkerBorrowId.Map.find_opt bid loan_to_content0 in + let lc1 = MarkerBorrowId.Map.find_opt bid loan_to_content1 in (* Merge *) let av : typed_avalue option = match (lc0, lc1) with @@ -2471,8 +2513,8 @@ 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) -> - let bids = filter_bids bids in + | ASharedLoan (pm, bids, sv, child) -> + let bids = filter_bids pm bids in sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) span; @@ -2481,8 +2523,8 @@ 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 - set_loans_as_merged bids; + let lc = ASharedLoan (pm, bids, sv, child) in + set_loans_as_merged pm bids; Some { value = ALoan lc; ty } | AMutLoan _ -> set_loan_as_merged bid; @@ -2492,9 +2534,9 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) | AIgnoredSharedLoan _ -> (* The abstraction has been destructured, so those shouldn't appear *) craise __FILE__ __LINE__ span "Unreachable")) - | Some lc0, Some lc1 -> - sanity_check __FILE__ __LINE__ (merge_funs <> None) span; - merge_g_loan_contents lc0 lc1 + | Some _, Some _ -> + (* With projection markers, shared loans should not be duplicated *) + craise __FILE__ __LINE__ span "Unreachable" | None, None -> craise __FILE__ __LINE__ span "Unreachable" in push_opt_avalue av)) @@ -2502,24 +2544,342 @@ let merge_into_abstraction_aux (span : Meta.span) (abs_kind : abs_kind) (* Reverse the avalues (we visited the loans/borrows in order, but pushed new values at the beggining of the stack of avalues) *) + List.rev !avalues + +(** Auxiliary function for {!merge_abstractions}. + + Phase 2 of the merge: we remove markers, by merging pairs of the same + element with different markers into one element without markers. + + Example: + {[ + |MB l0|, MB l1, ︙MB l0︙ + ~~> + MB l0, MB l1 + ]} + *) +let merge_abstractions_merge_markers (span : Meta.span) + (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) + (abs_values : typed_avalue list) : typed_avalue list = + log#ldebug + (lazy + ("merge_abstractions_merge_markers:\n- avalues:\n" + ^ String.concat ", " (List.map (typed_avalue_to_string ctx) abs_values))); + + (* We linearly traverse the list of avalues created through the first phase. *) + + (* Utilities to accumulate the list of values resulting from the merge *) + let avalues = ref [] in + let push_avalue av = + log#ldebug + (lazy + ("merge_abstractions_merge_markers: push_avalue: " + ^ typed_avalue_to_string ~span:(Some span) ctx av)); + avalues := av :: !avalues + in + + (* Compute some relevant information *) + let { + loans = _; + borrows = _; + borrows_loans; + loan_to_content; + borrow_to_content; + } = + compute_merge_abstraction_info span ctx abs_values + in + + (* We will merge elements with the same borrow/loan id, but with different markers. + Hence, we only keep track of the id here: if [Borrow PLeft bid] has been merged + and we see [Borrow PRight bid], we should ignore [Borrow PRight bid] (because + when seeing [Borrow PLeft bid] we stored [Borrow PNone bid] into the list + of values to insert in the resulting abstraction). *) + let merged_borrows = ref BorrowId.Set.empty in + let merged_loans = ref BorrowId.Set.empty in + + let borrow_is_merged id = BorrowId.Set.mem id !merged_borrows in + let set_borrow_as_merged id = + merged_borrows := BorrowId.Set.add id !merged_borrows + in + + let loan_is_merged id = BorrowId.Set.mem id !merged_loans in + let set_loan_as_merged id = + merged_loans := BorrowId.Set.add id !merged_loans + in + let set_loans_as_merged ids = BorrowId.Set.iter set_loan_as_merged ids in + + (* Recreates an avalue from a borrow_content. *) + let avalue_from_bc = function + | Concrete (_, _) -> + (* This can happen only in case of nested borrows, and should have been filtered during phase 1 *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty, bc) -> { value = ABorrow bc; ty } + in + + (* Recreates an avalue from a loan_content, and adds the set of loan ids as merged. + See the comment in the loop below for a detailed explanation *) + let avalue_from_lc = function + | Concrete (_, _) -> + (* This can happen only in case of nested borrows, and should have been filtered + during phase 1 *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty, bc) -> + (match bc with + | AMutLoan (_, id, _) -> set_loan_as_merged id + | ASharedLoan (_, ids, _, _) -> set_loans_as_merged ids + | _ -> craise __FILE__ __LINE__ span "Unreachable"); + { value = ALoan bc; ty } + in + + let complementary_markers pm0 pm1 = + (pm0 = PLeft && pm1 = PRight) || (pm0 = PRight && pm1 = PLeft) + in + + (* Some utility functions *) + (* Merge two aborrow contents - note that those contents must have the same id *) + let merge_aborrow_contents (ty0 : rty) (bc0 : aborrow_content) (ty1 : rty) + (bc1 : aborrow_content) : typed_avalue = + match (bc0, bc1) with + | AMutBorrow (pm0, id0, child0), AMutBorrow (pm1, id1, child1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + sanity_check __FILE__ __LINE__ (complementary_markers pm0 pm1) 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; + sanity_check __FILE__ __LINE__ (complementary_markers pm0 pm1) 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" + | _ -> + (* Unreachable because those cases are ignored (ended/ignored borrows) + or inconsistent *) + craise __FILE__ __LINE__ span "Unreachable" + in + + let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty) + (bc1 : g_borrow_content_with_ty) : typed_avalue = + match (bc0, bc1) with + | Concrete _, Concrete _ -> + (* This can happen only in case of nested borrows - the borrow has + to appear inside a shared loan. *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty0, bc0), Abstract (ty1, bc1) -> + merge_aborrow_contents ty0 bc0 ty1 bc1 + | Concrete _, Abstract _ | Abstract _, Concrete _ -> + (* TODO: is it really unreachable? *) + craise __FILE__ __LINE__ span "Unreachable" + in + + let loan_content_to_ids (lc : g_loan_content_with_ty) : BorrowId.Set.t = + match lc with + | Abstract (_, lc) -> ( + match lc with + | AMutLoan (_, id, _) -> BorrowId.Set.singleton id + | ASharedLoan (_, ids, _, _) -> ids + | _ -> + (* Unreachable because those cases are ignored (ended/ignored borrows) + or inconsistent *) + craise __FILE__ __LINE__ span "Unreachable") + | Concrete _ -> + (* Can only happen with nested borrows *) + craise __FILE__ __LINE__ span "Unreachable" + in + + let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty) + (lc1 : aloan_content) : typed_avalue = + match (lc0, lc1) with + | AMutLoan (pm0, id0, child0), AMutLoan (pm1, id1, child1) -> + (* Sanity-check of the precondition *) + sanity_check __FILE__ __LINE__ (id0 = id1) span; + sanity_check __FILE__ __LINE__ (complementary_markers pm0 pm1) span; + (* Merge *) + (Option.get merge_funs).merge_amut_loans id0 ty0 pm0 child0 ty1 pm1 + child1 + | ASharedLoan (pm0, ids0, sv0, child0), ASharedLoan (pm1, ids1, sv1, child1) + -> + sanity_check __FILE__ __LINE__ (complementary_markers pm0 pm1) span; + (* 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 *) + sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) span; + let ids = ids0 in + (* Merge *) + (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 *) + craise __FILE__ __LINE__ span "Unreachable" + in + + (* 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) : typed_avalue = + match (lc0, lc1) with + | Concrete _, Concrete _ -> + (* This can not happen: the values should have been destructured *) + craise __FILE__ __LINE__ span "Unreachable" + | Abstract (ty0, lc0), Abstract (ty1, lc1) -> + merge_aloan_contents ty0 lc0 ty1 lc1 + | Concrete _, Abstract _ | Abstract _, Concrete _ -> + (* TODO: is it really unreachable? *) + craise __FILE__ __LINE__ span "Unreachable" + in + + let invert_proj_marker = function + | PNone -> craise __FILE__ __LINE__ span "Unreachable" + | PLeft -> PRight + | PRight -> PLeft + in + + (* We now iter over all the accumulated elements. For each element with a marker + (i.e., not [PNone]), we attempt to find the dual element in the rest of the list. If so, + we remove both elements, and insert the same element but with no marker. + + Importantly, attempting the merge when first seeing a marked element allows us to preserve + the structure of the abstraction we are merging into (abs0). During phase 1, we traversed + the borrow_loans of the abs 0 first, and hence these elements are at the top of the list *) + List.iter + (function + | BorrowId (PNone, bid) -> + sanity_check __FILE__ __LINE__ (not (borrow_is_merged bid)) span; + (* This element has no marker. We do not filter it, hence we retrieve the + contents and inject it into the avalues list *) + let bc = MarkerBorrowId.Map.find (PNone, bid) borrow_to_content in + push_avalue (avalue_from_bc bc); + (* Setting the borrow as merged is not really necessary but we do it + for consistency, and this allows us to do some sanity checks. *) + set_borrow_as_merged bid + | BorrowId (pm, bid) -> + (* Check if the borrow has already been merged. If so, it means we already + added the merged value to the avalues list, and we can thus skip it *) + if borrow_is_merged bid then () + else ( + (* Not merged: set it as merged *) + set_borrow_as_merged bid; + (* Lookup the content of the borrow *) + let bc0 = MarkerBorrowId.Map.find (pm, bid) borrow_to_content in + (* Check if there exists the same borrow but with the complementary marker *) + let obc1 = + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + borrow_to_content + in + match obc1 with + | None -> + (* No dual element found, we keep the current one in the list of avalues, + with the same marker *) + push_avalue (avalue_from_bc bc0) + | Some bc1 -> + (* We have borrows with left and right markers in the environment. + We merge their values, and push the result to the list of avalues. + The merge will also remove the projection marker *) + push_avalue (merge_g_borrow_contents bc0 bc1)) + | LoanId (PNone, bid) -> + (* Since we currently have a set of loan ids associated to a shared_borrow, we can + have several loan ids associated to the same element. Hence, we need to ensure + that we did not add the corresponding element previously. + + To do so, we use the loan id merged set for both marked and unmarked values. + The assumption is that we should not have the same loan id for both an unmarked + element and a marked element. It might be better to sanity-check this. + + Adding the loan id to the merged set will be done inside avalue_from_lc. + + Rem: Once we move to a single loan id per shared_loan, this should not be needed + anymore. + *) + if loan_is_merged bid then () + else + let lc = MarkerBorrowId.Map.find (PNone, bid) loan_to_content in + push_avalue (avalue_from_lc lc); + (* Mark as merged *) + let ids = loan_content_to_ids lc in + set_loans_as_merged ids + | LoanId (pm, bid) -> ( + if + (* Check if the loan has already been merged. If so, we skip it. *) + loan_is_merged bid + then () + else + let lc0 = MarkerBorrowId.Map.find (pm, bid) loan_to_content in + let olc1 = + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + loan_to_content + in + (* Mark as merged *) + let ids0 = loan_content_to_ids lc0 in + set_loans_as_merged ids0; + match olc1 with + | None -> + (* No dual element found, we keep the current one with the same marker *) + push_avalue (avalue_from_lc lc0) + | Some lc1 -> + push_avalue (merge_g_loan_contents lc0 lc1); + (* Mark as merged *) + let ids1 = loan_content_to_ids lc1 in + set_loans_as_merged ids1)) + borrows_loans; + let avalues = List.rev !avalues in (* Reorder the avalues. We want the avalues to have the borrows first, then the loans (this structure is more stable when we merge abstractions together, meaning it is easier to find fixed points). *) + let is_borrow (av : typed_avalue) : bool = + match av.value with + | ABorrow _ -> true + | ALoan _ -> false + | _ -> craise __FILE__ __LINE__ span "Unexpected" + in + let aborrows, aloans = List.partition is_borrow avalues in + List.append aborrows aloans + +(** Auxiliary function. + + Merge two abstractions into one, without updating the context. + *) +let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) + (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs) + (abs1 : abs) : abs = + log#ldebug + (lazy + ("merge_abstractions:\n- abs0:\n" + ^ abs_to_string span ctx abs0 + ^ "\n\n- abs1:\n" + ^ abs_to_string span ctx abs1)); + (* Sanity check: we can't merge an abstraction with itself *) + sanity_check __FILE__ __LINE__ (abs0.abs_id <> abs1.abs_id) span; + + (* Check that the abstractions are destructured (i.e., there are no nested + values, etc.) *) + if !Config.sanity_checks then ( + let destructure_shared_values = true in + sanity_check __FILE__ __LINE__ + (abs_is_destructured span destructure_shared_values ctx abs0) + span; + sanity_check __FILE__ __LINE__ + (abs_is_destructured span destructure_shared_values ctx abs1) + span); + + (* Phase 1: simplify the loans coming from the left abstraction with + the borrows coming from the right abstraction. *) let avalues = - let is_borrow (av : typed_avalue) : bool = - match av.value with - | ABorrow _ -> true - | ALoan _ -> false - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - let aborrows, aloans = List.partition is_borrow avalues in - List.append aborrows aloans + merge_abstractions_merge_loan_borrow_pairs span merge_funs ctx abs0 abs1 in - (* Filter the regions *) + (* Phase 2: we now remove markers, by merging pairs of the same element with + different markers into one element. To do so, we linearly traverse the list + of avalues created through the first phase. *) + let avalues = merge_abstractions_merge_markers span merge_funs ctx avalues in (* Create the new abstraction *) let abs_id = fresh_abstraction_id () in @@ -2559,7 +2919,7 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id) let env = Substitute.env_subst_rids rsubst ctx.env in { ctx with env } -let merge_into_abstraction (span : Meta.span) (abs_kind : abs_kind) +let merge_into_first_abstraction (span : Meta.span) (abs_kind : abs_kind) (can_end : bool) (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) : eval_ctx * AbstractionId.id = @@ -2569,13 +2929,13 @@ let merge_into_abstraction (span : Meta.span) (abs_kind : abs_kind) (* Merge them *) let nabs = - merge_into_abstraction_aux span abs_kind can_end merge_funs ctx abs0 abs1 + merge_abstractions span abs_kind can_end merge_funs ctx abs0 abs1 in - (* Update the environment: replace the abstraction 1 with the result of the merge, - remove the abstraction 0 *) - let ctx = fst (ctx_subst_abs span ctx abs_id1 nabs) in - let ctx = fst (ctx_remove_abs span ctx abs_id0) in + (* Update the environment: replace the abstraction 0 with the result of the merge, + remove the abstraction 1 *) + let ctx = fst (ctx_subst_abs span ctx abs_id0 nabs) in + let ctx = fst (ctx_remove_abs span ctx abs_id1) in (* Merge all the regions from the abstraction into one (the first - i.e., the one with the smallest id). Note that we need to do this in the whole @@ -2596,3 +2956,63 @@ let merge_into_abstraction (span : Meta.span) (abs_kind : abs_kind) (* Return *) (ctx, nabs.abs_id) + +let reorder_loans_borrows_in_fresh_abs (span : Meta.span) (allow_markers : bool) + (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = + let reorder_in_fresh_abs (abs : abs) : abs = + (* Split between the loans and borrows *) + let is_borrow (av : typed_avalue) : bool = + match av.value with + | ABorrow _ -> true + | ALoan _ -> false + | _ -> craise __FILE__ __LINE__ span "Unexpected" + in + let aborrows, aloans = List.partition is_borrow abs.avalues in + + (* Reoder the borrows, and the loans. + + After experimenting, it seems that a good way of reordering the loans + and the borrows to find fixed points is simply to sort them by increasing + order of id (taking the smallest id of a set of ids, in case of sets). + + This is actually not as arbitrary as it might seem, because the ids give + us the order in which we introduced those borrows/loans. + *) + let get_borrow_id (av : typed_avalue) : BorrowId.id = + match av.value with + | ABorrow (AMutBorrow (pm, bid, _) | ASharedBorrow (pm, bid)) -> + sanity_check __FILE__ __LINE__ (allow_markers || 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 (pm, lid, _)) -> + sanity_check __FILE__ __LINE__ (allow_markers || pm = PNone) span; + lid + | ALoan (ASharedLoan (pm, lids, _, _)) -> + sanity_check __FILE__ __LINE__ (allow_markers || pm = PNone) span; + BorrowId.Set.min_elt lids + | _ -> craise __FILE__ __LINE__ span "Unexpected" + in + (* We use ordered maps to reorder the borrows and loans *) + let reorder (get_bid : typed_avalue -> BorrowId.id) + (values : typed_avalue list) : typed_avalue list = + List.map snd + (BorrowId.Map.bindings + (BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values))) + in + let aborrows = reorder get_borrow_id aborrows in + let aloans = reorder get_loan_id aloans in + let avalues = List.append aborrows aloans in + { abs with avalues } + in + + let reorder_in_abs (abs : abs) = + if AbstractionId.Set.mem abs.abs_id old_abs_ids then abs + else reorder_in_fresh_abs abs + in + + let env = env_map_abs reorder_in_abs ctx.env in + + { ctx with env } diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index 56df9344..cf14e94b 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] *) @@ -187,24 +212,36 @@ type merge_duplicates_funcs = { (** Merge an abstraction into another abstraction. - We insert the result of the merge in place of the second abstraction (and in + We insert the result of the merge in place of the first abstraction (and in particular, we don't simply push the merged abstraction at the end of the environment: this helps preserving the structure of the environment, when computing loop fixed points for instance). - 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: + When we merge two abstractions together, we remove the loans which appear + in the *left* abstraction and whose corresponding borrows appear in the + **right** abstraction. + For instance: {[ abs'0 { mut_borrow l0, mut_loan l1 } // Rem.: mut_loan l1 abs'1 { mut_borrow l1, mut_borrow l2 } // Rem.: mut_borrow l1 ~~> - abs'01 { mut_borrow l0, mut_borrow l2 } + abs'2 { mut_borrow l0, mut_borrow l2 } + ]} + + We also simplify the markers, when the same value appears in both abstractions + but with different markers. For instance: + {[ + abs'0 { |mut_borrow l0|, mut_loan l1 } + abs'1 { ︙mut_borrow l0︙, mut_borrow l1 } + + ~~> + + abs'2 { mut_borrow l0 } ]} - Also, we merge all their regions together. For instance, if [abs'0] projects + Finally, we merge all their regions together. For instance, if [abs'0] projects region [r0] and [abs'1] projects region [r1], we pick one of the two, say [r0] (the one with the smallest index in practice) and substitute [r1] with [r0] in the whole context. @@ -212,22 +249,10 @@ type merge_duplicates_funcs = { Parameters: - [kind] - [can_end] - - [merge_funs]: Those functions are used to merge borrows/loans with the - *same ids*. For instance, when performing environment joins we may introduce - abstractions which both contain loans/borrows with the same ids. When we - later merge those abstractions together, we need to call a merge function - to reconcile the borrows/loans. For instance, if both abstractions contain - the same shared loan [l0], we will call {!merge_ashared_borrows} to derive - a shared value for the merged shared loans. - - For instance, this happens for the following abstractions: - {[ - 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_into_abstraction] - actually simply performs some sort of a union. - + - [merge_funs]: those functions are used to merge borrows/loans with the + *same ids* but different markers. This is necessary when doing a collapse + (see the computation of joins). + If [merge_funs] are not provided, we check that there are no markers. - [ctx] - [abs_id0] - [abs_id1] @@ -235,7 +260,7 @@ type merge_duplicates_funcs = { We return the updated context as well as the id of the new abstraction which results from the merge. *) -val merge_into_abstraction : +val merge_into_first_abstraction : Meta.span -> abs_kind -> bool -> @@ -244,3 +269,20 @@ val merge_into_abstraction : AbstractionId.id -> AbstractionId.id -> eval_ctx * AbstractionId.id + +(** Reorder the loans and borrows in the fresh abstractions. + + We do this in order to enforce some structure in the environments: this + allows us to find fixed-points. Note that this function needs to be + called typically after we merge abstractions together (see {!reduce_ctx} + and {!collapse_ctx} for instance). + + Inputs: + - [span] + - [allow_markers]: disables some sanity checks (which check that projection + markers don't appear). + - [old_abs_ids] + - [eval_ctx] + *) +val reorder_loans_borrows_in_fresh_abs : + Meta.span -> bool -> AbstractionId.Set.t -> eval_ctx -> eval_ctx diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 2628b26a..0469d58e 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: 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 bid av - | ASharedLoan (bids, v, av) -> + else super#visit_AMutLoan env pm bid av + | ASharedLoan (pm, bids, v, av) -> + (* 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)) - 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: 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: 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 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: 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 bid av - | ASharedBorrow bid -> + else super#visit_AMutBorrow env pm bid av + | ASharedBorrow (pm, bid) -> + (* 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 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: 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 bid av) - | ASharedBorrow bid -> + else ABorrow (super#visit_AMutBorrow env pm bid av) + | ASharedBorrow (pm, bid) -> + (* 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 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: 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: 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 = _ } | 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/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 388d7382..4393e89f 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -478,7 +478,7 @@ let expand_symbolic_value_no_branching (config : config) (span : Meta.span) (* Debug *) log#ldebug (lazy - ("expand_symbolic_value_no_branching:" ^ symbolic_value_to_string ctx sv)); + ("expand_symbolic_value_no_branching: " ^ symbolic_value_to_string ctx sv)); (* Remember the initial context for printing purposes *) let ctx0 = ctx in (* Compute the expanded value - note that when doing so, we may introduce @@ -631,6 +631,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : (* We reverse the environment before exploring it - this way the values get expanded in a more "logical" order (this is only for convenience) *) obj#visit_env () (List.rev ctx.env); + log#ldebug + (lazy "greedy_expand_symbolics_with_borrows: no value to expand\n"); (* Nothing to expand: continue *) (ctx, fun e -> e) with FoundSymbolicValue sv -> @@ -674,6 +676,12 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> craise __FILE__ __LINE__ span "Unreachable" in + (* *) + log#ldebug + (lazy + ("\ngreedy_expand_symbolics_with_borrows: after expansion:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n")); (* Compose and continue *) comp cc (expand ctx) in diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 776cb6fa..90161196 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -70,6 +70,202 @@ let eval_loop_concrete (span : Meta.span) (eval_loop_body : stl_cm_fun) : in (ctx_resl, cf) +(** Auxiliary function for {!eval_loop_symbolic}. + + Match the context upon entering the loop with the loop fixed-point to + compute how to "apply" the fixed-point. Compute the correspondance from + the borrow ids in the current context to the loans which appear in the + loop context (we need this in order to know how to introduce the region + abstractions of the loop). + + We check the fixed-point at the same time to make sure the loans and borrows + inside the region abstractions are properly ordered (this is necessary for the + synthesis). + Ex.: if in the fixed point we have: + {[ + abs { MB l0, MB l1, ML l2, ML l3 } + ]} + we want to make sure that borrow l0 actually corresponds to loan l2, and + borrow l1 to loan l3. + *) +let eval_loop_symbolic_synthesize_fun_end (config : config) (span : span) + (loop_id : LoopId.id) (init_ctx : eval_ctx) (fixed_ids : ids_sets) + (fp_ctx : eval_ctx) (fp_input_svalues : SymbolicValueId.id list) + (rg_to_abs : AbstractionId.id RegionGroupId.Map.t) : + ((eval_ctx * statement_eval_res) * (eval_result -> eval_result)) + * borrow_loan_corresp = + (* First, preemptively end borrows/move values by matching the current + context with the target context *) + let ctx, cf_prepare = + log#ldebug + (lazy + ("eval_loop_symbolic_synthesize_fun_end: about to reorganize the \ + original context to match the fixed-point ctx with it:\n\ + - src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx + ^ "\n\n-tgt ctx (original context):\n" + ^ eval_ctx_to_string init_ctx)); + + prepare_match_ctx_with_target config span loop_id fixed_ids fp_ctx init_ctx + in + + (* Actually match *) + log#ldebug + (lazy + ("eval_loop_symbolic_synthesize_fun_end: about to compute the id \ + correspondance between the fixed-point ctx and the original ctx:\n\ + - src ctx (fixed-point ctx)\n" ^ eval_ctx_to_string fp_ctx + ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); + + (* Compute the id correspondance between the contexts *) + let fp_bl_corresp = + compute_fixed_point_id_correspondance span fixed_ids ctx fp_ctx + in + log#ldebug + (lazy + ("eval_loop_symbolic_synthesize_fun_end: about to match the fixed-point \ + context with the original context:\n\ + - src ctx (fixed-point ctx)" + ^ eval_ctx_to_string ~span:(Some span) fp_ctx + ^ "\n\n-tgt ctx (original context):\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n- fp_bl_corresp:\n" + ^ show_borrow_loan_corresp fp_bl_corresp + ^ "\n")); + + (* Compute the end expression, that is the expresion corresponding to the + 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 + (match_ctx_with_target config span loop_id true fp_bl_corresp + fp_input_svalues fixed_ids fp_ctx ctx) + in + + (* Sanity check: the mutable borrows/loans are properly ordered. + TODO: it seems that the way the fixed points are computed makes this check + always succeed. If it happens to fail we can reorder the borrows/loans + inside the region abstractions. *) + let check_abs (abs_id : AbstractionId.id) = + let abs = ctx_lookup_abs fp_ctx abs_id in + let is_borrow (av : typed_avalue) : bool = + match av.value with + | ABorrow _ -> true + | ALoan _ -> false + | _ -> craise __FILE__ __LINE__ span "Unreachable" + in + let borrows, loans = List.partition is_borrow abs.avalues in + + let mut_borrows = + List.filter_map + (fun (av : typed_avalue) -> + match av.value with + | 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 + | ABorrow (ASharedBorrow (pm, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + None + | _ -> craise __FILE__ __LINE__ span "Unreachable") + borrows + in + + let mut_loans = + List.filter_map + (fun (av : typed_avalue) -> + match av.value with + | 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 (pm, _, _, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + None + | _ -> craise __FILE__ __LINE__ span "Unreachable") + loans + in + + sanity_check __FILE__ __LINE__ + (List.length mut_borrows = List.length mut_loans) + span; + + let borrows_loans = List.combine mut_borrows mut_loans in + List.iter + (fun (bid, lid) -> + let lid_of_bid = + BorrowId.InjSubst.find bid fp_bl_corresp.borrow_to_loan_id_map + in + sanity_check __FILE__ __LINE__ (lid_of_bid = lid) span) + borrows_loans + in + List.iter check_abs (RegionGroupId.Map.values rg_to_abs); + + (* Return *) + (res_fun_end, fp_bl_corresp) + +(** Auxiliary function for {!eval_loop_symbolic}. + + Synthesize the body of the loop. + *) +let eval_loop_symbolic_synthesize_loop_body (config : config) (span : span) + (eval_loop_body : stl_cm_fun) (loop_id : LoopId.id) (fixed_ids : ids_sets) + (fp_ctx : eval_ctx) (fp_input_svalues : SymbolicValueId.id list) + (fp_bl_corresp : borrow_loan_corresp) : + (eval_ctx * statement_eval_res) list + * (SymbolicAst.expression list option -> eval_result) = + (* First, evaluate the loop body starting from the **fixed-point** context *) + let ctx_resl, cf_loop = eval_loop_body fp_ctx in + + (* Then, do a special treatment of the break and continue cases. + For now, we forbid having breaks in loops (and eliminate breaks + in the prepasses) *) + let eval_after_loop_iter (ctx, res) = + log#ldebug (lazy "eval_loop_symbolic: eval_after_loop_iter"); + match res with + | Return -> + (* We replace the [Return] with a [LoopReturn] *) + ((ctx, LoopReturn loop_id), fun e -> e) + | Panic -> ((ctx, res), fun e -> e) + | Break _ -> + (* Breaks should have been eliminated in the prepasses *) + craise __FILE__ __LINE__ span "Unexpected break" + | Continue i -> + (* We don't support nested loops for now *) + cassert __FILE__ __LINE__ (i = 0) span + "Nested loops are not supported yet"; + log#ldebug + (lazy + ("eval_loop_symbolic: about to match the fixed-point context with \ + the context at a continue:\n\ + - src ctx (fixed-point ctx)" + ^ eval_ctx_to_string ~span:(Some span) fp_ctx + ^ "\n\n-tgt ctx (ctx at continue):\n" + ^ eval_ctx_to_string ~span:(Some span) ctx)); + match_ctx_with_target config span loop_id false fp_bl_corresp + fp_input_svalues fixed_ids fp_ctx ctx + | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> + (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. + For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. + *) + craise __FILE__ __LINE__ span "Unreachable" + in + + (* Apply and compose *) + let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in + let cc (el : SymbolicAst.expression list option) : eval_result = + match el with + | None -> None + | Some el -> + let el = + List.map + (fun (cf, e) -> Option.get (cf (Some e))) + (List.combine cfl el) + in + cf_loop (Some el) + in + + (ctx_resl, cc) + (** Evaluate a loop in symbolic mode *) let eval_loop_symbolic (config : config) (span : span) (eval_loop_body : stl_cm_fun) : stl_cm_fun = @@ -105,115 +301,25 @@ let eval_loop_symbolic (config : config) (span : span) (* Synthesize the end of the function - we simply match the context at the loop entry with the fixed point: in the synthesized code, the function - will end with a call to the loop translation - *) - let ((res_fun_end, cf_fun_end), fp_bl_corresp) : - ((eval_ctx * statement_eval_res) * (eval_result -> eval_result)) * _ = - (* First, preemptively end borrows/move values by matching the current - context with the target context *) - let ctx, cf_prepare = - log#ldebug - (lazy - ("eval_loop_symbolic: about to reorganize the original context to \ - match the fixed-point ctx with it:\n\ - - src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx - ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); - - prepare_match_ctx_with_target config span loop_id fixed_ids fp_ctx ctx - in + will end with a call to the loop translation. - (* Actually match *) - log#ldebug - (lazy - ("eval_loop_symbolic: about to compute the id correspondance between \ - the fixed-point ctx and the original ctx:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx - ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); - - (* Compute the id correspondance between the contexts *) - let fp_bl_corresp = - compute_fixed_point_id_correspondance span fixed_ids ctx fp_ctx - in - log#ldebug - (lazy - ("eval_loop_symbolic: about to match the fixed-point context with the \ - original context:\n\ - - src ctx (fixed-point ctx)" - ^ eval_ctx_to_string ~span:(Some span) fp_ctx - ^ "\n\n-tgt ctx (original context):\n" - ^ 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 - we never get out) *) - let res_fun_end = - comp cf_prepare - (match_ctx_with_target config span loop_id true fp_bl_corresp - fp_input_svalues fixed_ids fp_ctx ctx) - in - (res_fun_end, fp_bl_corresp) + We update the loop fixed point at the same time by reordering the borrows/ + loans which appear inside it. + *) + let (res_fun_end, cf_fun_end), fp_bl_corresp = + eval_loop_symbolic_synthesize_fun_end config span loop_id ctx fixed_ids + fp_ctx fp_input_svalues rg_to_abs in + log#ldebug (lazy "eval_loop_symbolic: matched the fixed-point context with the original \ - context"); + context."); (* Synthesize the loop body *) - let (resl_loop_body, cf_loop_body) : - (eval_ctx * statement_eval_res) list - * (SymbolicAst.expression list option -> eval_result) = - (* First, evaluate the loop body starting from the **fixed-point** context *) - let ctx_resl, cf_loop = eval_loop_body fp_ctx in - - (* Then, do a special treatment of the break and continue cases. - For now, we forbid having breaks in loops (and eliminate breaks - in the prepasses) *) - let eval_after_loop_iter (ctx, res) = - log#ldebug (lazy "eval_loop_symbolic: eval_after_loop_iter"); - match res with - | Return -> - (* We replace the [Return] with a [LoopReturn] *) - ((ctx, LoopReturn loop_id), fun e -> e) - | Panic -> ((ctx, res), fun e -> e) - | Break _ -> - (* Breaks should have been eliminated in the prepasses *) - craise __FILE__ __LINE__ span "Unexpected break" - | Continue i -> - (* We don't support nested loops for now *) - cassert __FILE__ __LINE__ (i = 0) span - "Nested loops are not supported yet"; - log#ldebug - (lazy - ("eval_loop_symbolic: about to match the fixed-point context \ - with the context at a continue:\n\ - - src ctx (fixed-point ctx)" - ^ eval_ctx_to_string ~span:(Some span) fp_ctx - ^ "\n\n-tgt ctx (ctx at continue):\n" - ^ eval_ctx_to_string ~span:(Some span) ctx)); - match_ctx_with_target config span loop_id false fp_bl_corresp - fp_input_svalues fixed_ids fp_ctx ctx - | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> - (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. - For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. - *) - craise __FILE__ __LINE__ span "Unreachable" - in - - (* Apply and compose *) - let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in - let cc (el : SymbolicAst.expression list option) : eval_result = - match el with - | None -> None - | Some el -> - let el = - List.map - (fun (cf, e) -> Option.get (cf (Some e))) - (List.combine cfl el) - in - cf_loop (Some el) - in - - (ctx_resl, cc) + let resl_loop_body, cf_loop_body = + eval_loop_symbolic_synthesize_loop_body config span eval_loop_body loop_id + fixed_ids fp_ctx fp_input_svalues fp_bl_corresp in log#ldebug @@ -242,55 +348,33 @@ let eval_loop_symbolic (config : config) (span : span) return nothing. *) let rg_to_given_back = - let compute_abs_given_back_tys (abs : abs) : rty list = + let compute_abs_given_back_tys (abs_id : AbstractionId.id) : rty list = + let abs = ctx_lookup_abs fp_ctx abs_id in + log#ldebug + (lazy + ("eval_loop_symbolic: compute_abs_given_back_tys:\n- abs:\n" + ^ abs_to_string span ctx abs ^ "\n")); + let is_borrow (av : typed_avalue) : bool = match av.value with | ABorrow _ -> true | ALoan _ -> false | _ -> craise __FILE__ __LINE__ span "Unreachable" in - let borrows, loans = List.partition is_borrow abs.avalues in - - let borrows = - List.filter_map - (fun (av : typed_avalue) -> - match av.value with - | ABorrow (AMutBorrow (bid, child_av)) -> - sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span; - Some (bid, child_av.ty) - | ABorrow (ASharedBorrow _) -> None - | _ -> craise __FILE__ __LINE__ span "Unreachable") - borrows - in - let borrows = ref (BorrowId.Map.of_list borrows) in - - let loan_ids = - List.filter_map - (fun (av : typed_avalue) -> - match av.value with - | ALoan (AMutLoan (bid, child_av)) -> - sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span; - Some bid - | ALoan (ASharedLoan _) -> None - | _ -> craise __FILE__ __LINE__ span "Unreachable") - loans - in - - (* List the given back types, in the order given by the loans *) - let given_back_tys = - List.map - (fun lid -> - let bid = - BorrowId.InjSubst.find lid fp_bl_corresp.loan_to_borrow_id_map - in - let ty = BorrowId.Map.find bid !borrows in - borrows := BorrowId.Map.remove bid !borrows; - ty) - loan_ids - in - sanity_check __FILE__ __LINE__ (BorrowId.Map.is_empty !borrows) span; - - given_back_tys + let borrows, _ = List.partition is_borrow abs.avalues in + + List.filter_map + (fun (av : typed_avalue) -> + match av.value with + | ABorrow (AMutBorrow (pm, _, child_av)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span; + Some child_av.ty + | ABorrow (ASharedBorrow (pm, _)) -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; + None + | _ -> craise __FILE__ __LINE__ span "Unreachable") + borrows in RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs in diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 991f259f..df808385 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -26,21 +26,21 @@ type ctx_or_update = (eval_ctx, updt_env_kind) result (** Union Find *) module UF = UnionFind.Make (UnionFind.StoreMap) -(** 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). +(** A small utility. + + Remark: we use projection markers, meaning we compute maps from/to + pairs of (projection marker, borrow/loan id). This allows us to use + this utility during a reduce phase (when we simplify the environment + and all markers should be [PNone]) as well as during a collapse (where + we actually have markers because we performed a join and are progressively + transforming the environment to get rid of those markers). *) type abs_borrows_loans_maps = { abs_ids : AbstractionId.id list; - abs_to_borrows : BorrowId.Set.t AbstractionId.Map.t; - abs_to_loans : BorrowId.Set.t AbstractionId.Map.t; - abs_to_borrows_loans : BorrowId.Set.t AbstractionId.Map.t; - borrow_to_abs : AbstractionId.Set.t BorrowId.Map.t; - loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; - borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; + abs_to_borrows : MarkerBorrowId.Set.t AbstractionId.Map.t; + abs_to_loans : MarkerBorrowId.Set.t AbstractionId.Map.t; + borrow_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; + loan_to_abs : AbstractionId.Set.t MarkerBorrowId.Map.t; } (** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher]. @@ -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 -> @@ -413,3 +429,57 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = } in ids + +(** Small utility: add a projection marker to a typed avalue. + This can be used in combination with List.map to add markers to an entire abstraction + *) +let typed_avalue_add_marker (span : Meta.span) (ctx : eval_ctx) + (pm : proj_marker) (av : typed_avalue) : typed_avalue = + let obj = + object + inherit [_] map_typed_avalue as super + + method! visit_borrow_content _ _ = + craise __FILE__ __LINE__ span "Unexpected borrow" + + method! visit_loan_content _ _ = + craise __FILE__ __LINE__ span "Unexpected loan" + + method! visit_symbolic_value _ sv = + sanity_check __FILE__ __LINE__ + (not (symbolic_value_has_borrows ctx sv)) + span; + sv + + method! visit_aloan_content env lc = + match lc with + | AMutLoan (pm0, bid, av) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aloan_content env (AMutLoan (pm, bid, av)) + | ASharedLoan (pm0, bids, av, child) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aloan_content env (ASharedLoan (pm, bids, av, child)) + | _ -> craise __FILE__ __LINE__ span "Unsupported yet" + + method! visit_aborrow_content env bc = + match bc with + | AMutBorrow (pm0, bid, av) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aborrow_content env (AMutBorrow (pm, bid, av)) + | ASharedBorrow (pm0, bid) -> + sanity_check __FILE__ __LINE__ (pm0 = PNone) span; + super#visit_aborrow_content env (ASharedBorrow (pm, bid)) + | _ -> craise __FILE__ __LINE__ span "Unsupported yet" + end + in + obj#visit_typed_avalue () av + +(** Small utility: add a projection marker to an abstraction. + This can be used in combination with List.map to add markers to an entire abstraction + *) +let abs_add_marker (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker) + (abs : abs) : abs = + { + abs with + avalues = List.map (typed_avalue_add_marker span ctx pm) abs.avalues; + } diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 1a0bb090..b68f2a4d 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -126,64 +126,6 @@ let cleanup_fresh_values_and_abs (config : config) (span : Meta.span) let ctx = cleanup_fresh_values fixed_ids ctx in (ctx, cc) -(** Reorder the loans and borrows in the fresh abstractions. - - We do this in order to enforce some structure in the environments: this - allows us to find fixed-points. Note that this function needs to be - called typically after we merge abstractions together (see {!collapse_ctx} - for instance). - *) -let reorder_loans_borrows_in_fresh_abs (span : Meta.span) - (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = - let reorder_in_fresh_abs (abs : abs) : abs = - (* Split between the loans and borrows *) - let is_borrow (av : typed_avalue) : bool = - match av.value with - | ABorrow _ -> true - | ALoan _ -> false - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - let aborrows, aloans = List.partition is_borrow abs.avalues in - - (* Reoder the borrows, and the loans. - - After experimenting, it seems that a good way of reordering the loans - and the borrows to find fixed points is simply to sort them by increasing - order of id (taking the smallest id of a set of ids, in case of sets). - *) - let get_borrow_id (av : typed_avalue) : BorrowId.id = - match av.value with - | 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 - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - (* We use ordered maps to reorder the borrows and loans *) - let reorder (get_bid : typed_avalue -> BorrowId.id) - (values : typed_avalue list) : typed_avalue list = - List.map snd - (BorrowId.Map.bindings - (BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values))) - in - let aborrows = reorder get_borrow_id aborrows in - let aloans = reorder get_loan_id aloans in - let avalues = List.append aborrows aloans in - { abs with avalues } - in - - let reorder_in_abs (abs : abs) = - if AbstractionId.Set.mem abs.abs_id old_abs_ids then abs - else reorder_in_fresh_abs abs - in - - let env = env_map_abs reorder_in_abs ctx.env in - - { ctx with env } - let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) : cm_fun = fun ctx0 -> @@ -245,10 +187,14 @@ 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 abstractions for the borrows l0 and l1: {[ - abs'2 { SB l0, SL {l2} s2 } + abs'2 { SB l0, SL {l0'} s1 } // Reborrow for l0 + abs'3 { SB l1, SL {l1'} s2 } // Reborrow for l1 ]} + + Remark: of course we also need to replace the [SB l0] and the [SB l1] + values we find in the environments with [SB l0'] and [SB l1']. *) let push_abs_for_shared_value (abs : abs) (sv : typed_value) (lid : BorrowId.id) : unit = @@ -283,13 +229,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 +290,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 @@ -447,7 +393,7 @@ let prepare_ashared_loans_no_synth (span : Meta.span) (loop_id : LoopId.id) let compute_loop_entry_fixed_point (config : config) (span : Meta.span) (loop_id : LoopId.id) (eval_loop_body : stl_cm_fun) (ctx0 : eval_ctx) : - eval_ctx * ids_sets * abs RegionGroupId.Map.t = + eval_ctx * ids_sets * AbstractionId.id RegionGroupId.Map.t = (* Introduce "reborrows" for the shared values in the abstractions, so that the shared values in the fixed abstractions never get modified (technically, they are immutable, but in practice we can introduce more shared loans, or @@ -750,10 +696,24 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) region id to abstraction id *) let fp = ref fp in let rg_to_abs = ref RegionGroupId.Map.empty in + (* List the ids of all the abstractions in the context, in the order in + which they appear (this is important to preserve some structure: + we will explore them in this order) *) + let all_abs_ids = + List.filter_map + (function EAbs abs -> Some abs.abs_id | _ -> None) + (* TODO: we may want to use a different order, for instance the order + in which the regions were ended. *) + (List.rev !fp.env) + in let _ = RegionGroupId.Map.iter (fun rg_id ids -> - let ids = AbstractionId.Set.elements ids in + (* Make sure we explore the ids in the order in which they appear + in the context *) + let ids = + List.filter (fun id -> AbstractionId.Set.mem id ids) all_abs_ids + in (* Retrieve the first id of the group *) match ids with | [] -> @@ -796,8 +756,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) ^ AbstractionId.to_string !id0)); (* Note that we merge *into* [id0] *) let fp', id0' = - merge_into_abstraction span loop_id abs_kind false !fp id - !id0 + merge_into_first_abstraction span loop_id abs_kind false + !fp !id0 id in fp := fp'; id0 := id0'; @@ -806,15 +766,15 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span) craise __FILE__ __LINE__ span "Unexpected") ids; (* Register the mapping *) - let abs = ctx_lookup_abs !fp !id0 in - rg_to_abs := RegionGroupId.Map.add_strict rg_id abs !rg_to_abs) + rg_to_abs := RegionGroupId.Map.add_strict rg_id !id0 !rg_to_abs) !fp_ended_aids in let rg_to_abs = !rg_to_abs in (* Reorder the loans and borrows in the fresh abstractions in the fixed-point *) let fp = - reorder_loans_borrows_in_fresh_abs span (Option.get !fixed_ids).aids !fp + reorder_loans_borrows_in_fresh_abs span false (Option.get !fixed_ids).aids + !fp in (* Update the abstraction's [can_end] field and their kinds. @@ -905,7 +865,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 +1006,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 +1056,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/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli index 59d42812..8db7b973 100644 --- a/compiler/InterpreterLoopsFixedPoint.mli +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -81,10 +81,11 @@ val compute_loop_entry_fixed_point : Meta.span -> loop_id -> (* This function is the function to evaluate the loop body (eval_statement applied - to the proper arguments) *) + to the proper arguments). We need to take it as input because [compute_loop_entry_fixed_point] + is mutually recursive with [eval_statement], but doesn't live in the same module. *) Cps.stl_cm_fun -> eval_ctx -> - eval_ctx * ids_sets * abs SymbolicAst.region_group_id_map + eval_ctx * ids_sets * AbstractionId.id SymbolicAst.region_group_id_map (** For the abstractions in the fixed point, compute the correspondance between the borrows ids and the loans ids, if we want to introduce equivalent diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index c67869ac..dbb4e5e9 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -1,6 +1,7 @@ open Types open Values open Contexts +open Utils open TypesUtils open ValuesUtils open InterpreterUtils @@ -12,65 +13,125 @@ open Errors (** The local logger *) let log = Logging.loops_join_ctxs_log -(** Reorder the loans and borrows in the fresh abstractions. - - We do this in order to enforce some structure in the environments: this - allows us to find fixed-points. Note that this function needs to be - called typically after we merge abstractions together (see {!collapse_ctx} - for instance). - *) -let reorder_loans_borrows_in_fresh_abs (span : Meta.span) - (old_abs_ids : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx = - let reorder_in_fresh_abs (abs : abs) : abs = - (* Split between the loans and borrows *) - let is_borrow (av : typed_avalue) : bool = - match av.value with - | ABorrow _ -> true - | ALoan _ -> false - | _ -> craise __FILE__ __LINE__ span "Unexpected" - in - let aborrows, aloans = List.partition is_borrow abs.avalues in - - (* Reoder the borrows, and the loans. - - After experimenting, it seems that a good way of reordering the loans - and the borrows to find fixed points is simply to sort them by increasing - order of id (taking the smallest id of a set of ids, in case of sets). - *) - let get_borrow_id (av : typed_avalue) : BorrowId.id = - match av.value with - | ABorrow (AMutBorrow (bid, _) | ASharedBorrow bid) -> bid - | _ -> craise __FILE__ __LINE__ span "Unexpected" +(** Utility. + + An environment augmented with information about its borrows/loans/abstractions + for the purpose of merging abstractions together. + We provide functions to update this information when merging two abstractions + together. We use it in {!reduce_ctx} and {!collapse_ctx}. +*) +type ctx_with_info = { ctx : eval_ctx; info : abs_borrows_loans_maps } + +let ctx_with_info_merge_into_first_abs (span : Meta.span) (abs_kind : abs_kind) + (can_end : bool) (merge_funs : merge_duplicates_funcs option) + (ctx : ctx_with_info) (abs_id0 : AbstractionId.id) + (abs_id1 : AbstractionId.id) : ctx_with_info = + (* Compute the new context and the new abstraction id *) + let nctx, nabs_id = + merge_into_first_abstraction span abs_kind can_end merge_funs ctx.ctx + abs_id0 abs_id1 + in + let nabs = ctx_lookup_abs nctx nabs_id in + (* Update the information *) + let { + abs_to_borrows = nabs_to_borrows; + abs_to_loans = nabs_to_loans; + borrow_to_abs = borrow_to_nabs; + loan_to_abs = loan_to_nabs; + _; + } = + compute_abs_borrows_loans_maps span (fun _ -> true) [ EAbs nabs ] + in + let { abs_ids; abs_to_borrows; abs_to_loans; borrow_to_abs; loan_to_abs } = + ctx.info + in + let abs_ids = + List.filter_map + (fun id -> + if id = abs_id0 then Some nabs_id + else if id = abs_id1 then None + else Some id) + abs_ids + in + (* Update the maps from makred borrows/loans to abstractions *) + let update_to_abs abs_to to_nabs to_abs = + (* Remove the old bindings *) + let abs0_elems = AbstractionId.Map.find abs_id0 abs_to in + let abs1_elems = AbstractionId.Map.find abs_id1 abs_to in + let abs01_elems = MarkerBorrowId.Set.union abs0_elems abs1_elems in + let to_abs = + MarkerBorrowId.Map.filter + (fun id _ -> not (MarkerBorrowId.Set.mem id abs01_elems)) + to_abs 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 - | _ -> craise __FILE__ __LINE__ span "Unexpected" + (* Add the new ones *) + let merge _ _ _ = + (* We shouldn't have twice the same key *) + craise __FILE__ __LINE__ span "Unreachable" in - (* We use ordered maps to reorder the borrows and loans *) - let reorder (get_bid : typed_avalue -> BorrowId.id) - (values : typed_avalue list) : typed_avalue list = - List.map snd - (BorrowId.Map.bindings - (BorrowId.Map.of_list (List.map (fun v -> (get_bid v, v)) values))) + MarkerBorrowId.Map.union merge to_nabs to_abs + in + let borrow_to_abs = + update_to_abs abs_to_borrows borrow_to_nabs borrow_to_abs + in + let loan_to_abs = update_to_abs abs_to_loans loan_to_nabs loan_to_abs in + + (* Update the maps from abstractions to marked borrows/loans *) + let update_abs_to nabs_to abs_to = + AbstractionId.Map.add_strict nabs_id + (AbstractionId.Map.find nabs_id nabs_to) + (AbstractionId.Map.remove abs_id0 + (AbstractionId.Map.remove abs_id1 abs_to)) + in + let abs_to_borrows = update_abs_to nabs_to_borrows abs_to_borrows in + let abs_to_loans = update_abs_to nabs_to_loans abs_to_loans in + let info = + { abs_ids; abs_to_borrows; abs_to_loans; borrow_to_abs; loan_to_abs } + in + { ctx = nctx; info } + +exception AbsToMerge of abstraction_id * abstraction_id + +(** Repeatedly iterate through the borrows/loans in an environment and merge the + abstractions that have to be merged according to a user-provided policy. *) +let repeat_iter_borrows_merge (span : Meta.span) (old_ids : ids_sets) + (abs_kind : abs_kind) (can_end : bool) + (merge_funs : merge_duplicates_funcs option) + (iter : ctx_with_info -> ('a -> unit) -> unit) + (policy : ctx_with_info -> 'a -> (abstraction_id * abstraction_id) option) + (ctx : eval_ctx) : eval_ctx = + (* Compute the information *) + let ctx = + let is_fresh_abs_id (id : AbstractionId.id) : bool = + not (AbstractionId.Set.mem id old_ids.aids) in - let aborrows = reorder get_borrow_id aborrows in - let aloans = reorder get_loan_id aloans in - let avalues = List.append aborrows aloans in - { abs with avalues } + let explore (abs : abs) = is_fresh_abs_id abs.abs_id in + let info = compute_abs_borrows_loans_maps span explore ctx.env in + { ctx; info } in - - let reorder_in_abs (abs : abs) = - if AbstractionId.Set.mem abs.abs_id old_abs_ids then abs - else reorder_in_fresh_abs abs + (* Explore and merge *) + let rec explore_merge (ctx : ctx_with_info) : eval_ctx = + try + iter ctx (fun x -> + (* Check if we need to merge some abstractions *) + match policy ctx x with + | None -> (* No *) () + | Some (abs_id0, abs_id1) -> + (* Yes: raise an exception *) + raise (AbsToMerge (abs_id0, abs_id1))); + (* No exception raise: return the current context *) + ctx.ctx + with AbsToMerge (abs_id0, abs_id1) -> + (* Merge and recurse *) + let ctx = + ctx_with_info_merge_into_first_abs span abs_kind can_end merge_funs ctx + abs_id0 abs_id1 + in + explore_merge ctx in + explore_merge ctx - let env = env_map_abs reorder_in_abs ctx.env in - - { ctx with env } - -(** Collapse an environment. +(** Reduce an environment. We do this to simplify an environment, for the purpose of finding a loop fixed point. @@ -84,8 +145,8 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) In effect, this allows us to merge newly introduced abstractions/borrows with their parent abstractions. - For instance, when evaluating the first loop iteration, we start in the - following environment: + For instance, looking at the [list_nth_mut] example, when evaluating the + first loop iteration, we start in the following environment: {[ abs@0 { ML l0 } ls -> MB l0 (s2 : loops::List<T>) @@ -115,7 +176,8 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) abs@3 { MB l1 } ]} - We finally merge the new abstractions together. It gives: + We finally merge the new abstractions together (abs@1 and abs@2 because + of l2, and abs@1 and abs@3 because of l1). It gives: {[ abs@0 { ML l0 } ls -> MB l4 (s@6 : loops::List<T>) @@ -123,29 +185,39 @@ let reorder_loans_borrows_in_fresh_abs (span : Meta.span) abs@4 { MB l0, ML l4 } ]} - [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). + - If [merge_funs] is [None], we check that there are no markers in the environments. + This is the "reduce" operation. + - If [merge_funs] is [Some _], when merging abstractions together, we merge the pairs + of borrows and the pairs of loans with the same markers **if this marker is not** + [PNone]. This is useful to reuse the reduce operation to implement the collapse. + Note that we ignore borrows/loans with the [PNone] marker: the goal of the collapse + operation is to *eliminate* markers, not to simplify the environment. + + For instance, when merging: + {[ + abs@0 { ML l0, |MB l1| } + abs@1 { MB l0, ︙MB l1︙ } + ]} + We get: + {[ + abs@2 { MB l1 } + ]} *) -let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) - (merge_funs : merge_duplicates_funcs option) (old_ids : ids_sets) +let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option) + (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (ctx0 : eval_ctx) : eval_ctx = (* Debug *) log#ldebug (lazy - ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids - ^ "\n\n- ctx0:\n" + ("reduce_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ~span:(Some span) ctx0 ^ "\n\n")); + let with_markers = merge_funs <> None in + let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in let destructure_shared_values = true in - let is_fresh_abs_id (id : AbstractionId.id) : bool = - not (AbstractionId.Set.mem id old_ids.aids) - in let is_fresh_did (id : DummyVarId.id) : bool = not (DummyVarId.Set.mem id old_ids.dids) in @@ -172,117 +244,226 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) let ctx = { ctx0 with env } in log#ldebug (lazy - ("collapse_ctx: after converting values to abstractions:\n" + ("reduce_ctx: after converting values to abstractions:\n" ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); log#ldebug (lazy - ("collapse_ctx: after decomposing the shared values in the abstractions:\n" + ("reduce_ctx: after decomposing the shared values in the abstractions:\n" ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); - (* Explore all the *new* abstractions, and compute various maps *) - let explore (abs : abs) = is_fresh_abs_id abs.abs_id in - let ids_maps = - compute_abs_borrows_loans_maps span (merge_funs = None) explore env + (* + * Merge all the mergeable abs. + *) + (* We iterate over the *new* abstractions, then over the loans in the abstractions. + We do this because we want to control the order in which abstractions + are merged (the ids are iterated in increasing order). Otherwise, we + could simply iterate over all the borrows in [loan_to_abs]... *) + let iterate ctx f = + List.iter + (fun abs_id0 -> + let lids = AbstractionId.Map.find abs_id0 ctx.info.abs_to_loans in + MarkerBorrowId.Set.iter (fun lid -> f (abs_id0, lid)) lids) + ctx.info.abs_ids 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 + (* Given a loan, check if there is a fresh abstraction with the corresponding borrow *) + let merge_policy ctx (abs_id0, lid) = + if not with_markers then + sanity_check __FILE__ __LINE__ (fst lid = PNone) span; + (* If we use markers: we are doing a collapse, which means we attempt + to eliminate markers (and this is the only goal of the operation). + We thus ignore the non-marked values (we merge non-marked values + when doing a "real" reduce, to simplify the environment in order + to converge to a fixed-point, for instance). *) + if with_markers && fst lid = PNone then None + else + (* Find the borrow corresponding to the loan we want to eliminate *) + match MarkerBorrowId.Map.find_opt lid ctx.info.borrow_to_abs with + | None -> (* Nothing to to *) None + | Some abs_ids1 -> ( + (* We need to merge *) + match AbstractionId.Set.elements abs_ids1 with + | [] -> None + | abs_id1 :: _ -> + log#ldebug + (lazy + ("reduce_ctx: merging abstraction " + ^ AbstractionId.to_string abs_id1 + ^ " into " + ^ AbstractionId.to_string abs_id0 + ^ ":\n\n" + ^ eval_ctx_to_string ~span:(Some span) ctx.ctx)); + Some (abs_id0, abs_id1)) in - - (* 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) + (* Iterate and merge *) + let ctx = + repeat_iter_borrows_merge span old_ids abs_kind can_end merge_funs iterate + merge_policy ctx in - (* Merge the abstractions together *) - let merged_abs : AbstractionId.id UnionFind.elem AbstractionId.Map.t = - AbstractionId.Map.of_list - (List.map (fun id -> (id, UnionFind.make id)) abs_ids) - in + log#ldebug + (lazy + ("reduce_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- after reduce:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n")); - let ctx = ref ctx in + (* Reorder the loans and borrows in the fresh abstractions - note that we may + not have eliminated all the markers at this point. *) + let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids ctx in - (* Merge all the mergeable abs. + log#ldebug + (lazy + ("reduce_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- after reduce and reorder borrows/loans:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n")); - We iterate over the abstractions, then over the borrows in the abstractions. - We do this because we want to control the order in which abstractions - are merged (the ids are iterated in increasing order). Otherwise, we - could simply iterate over all the borrows in [borrow_to_abs]... + (* Return the new context *) + ctx + +(** Reduce_ctx can only be called in a context with no markers *) +let reduce_ctx = reduce_ctx_with_markers None + +(** Auxiliary function for collapse (see below). + + We traverse all abstractions, and merge abstractions when they contain the same element, + but with dual markers (i.e., [PLeft] and [PRight]). + + For instance, if we have the abstractions + + {[ + abs@0 { | MB l0 _ |, ML l1 } + abs@1 { ︙MB l0 _ ︙, ML l2 } + ]} + + We merge abs@0 and abs@1 into a new abstraction abs@2. This allows us to + eliminate the markers used for [MB l0]: + {[ + abs@2 { MB l0 _, ML l1, ML l2 } + ]} +*) +let collapse_ctx_collapse (span : Meta.span) (loop_id : LoopId.id) + (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx : eval_ctx) + : eval_ctx = + (* Debug *) + log#ldebug + (lazy + ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids + ^ "\n\n- initial ctx:\n" + ^ eval_ctx_to_string ~span:(Some span) ctx + ^ "\n\n")); + + let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in + let can_end = true in + + let invert_proj_marker = function + | PNone -> craise __FILE__ __LINE__ span "Unreachable" + | PLeft -> PRight + | PRight -> PLeft + in + + (* Merge all the mergeable abs where the same element in present in both abs, + but with left and right markers respectively. + *) + (* The iter function: iterate over the abstractions, and inside an abstraction + over the borrows then the loans *) + let iter ctx f = + List.iter + (fun abs_id0 -> + (* Small helper *) + let iterate is_borrow = + let m = + if is_borrow then ctx.info.abs_to_borrows else ctx.info.abs_to_loans + in + let ids = AbstractionId.Map.find abs_id0 m in + MarkerBorrowId.Set.iter (fun id -> f (abs_id0, is_borrow, id)) ids + in + (* Iterate over the borrows *) + iterate true; + (* Iterate over the loans *) + iterate false) + ctx.info.abs_ids + in + (* Small utility: check if we need to swap two region abstractions before + merging them. + + We might have to swap the order to make sure that if there + are loans in one abstraction and the corresponding borrows + in the other they get properly merged (if we merge them in the wrong + order, we might introduce borrowing cycles). + + Example: + If we are merging abs0 and abs1 because of the marked value + [MB l0]: + {[ + abs0 { |MB l0|, MB l1 } + abs1 { ︙MB l0︙, ML l1 } + ]} + we want to make sure that we swap them (abs1 goes to the + left) to make sure [MB l1] and [ML l1] get properly eliminated. + + Remark: in case there is a borrowing cycle between the two abstractions + (which shouldn't happen) then there isn't much we can do, and whatever + the order in which we merge, we will preserve the cycle. *) - List.iter - (fun abs_id0 -> - let bids = AbstractionId.Map.find abs_id0 abs_to_borrows in - let bids = BorrowId.Set.elements bids in - List.iter - (fun bid -> - match BorrowId.Map.find_opt bid loan_to_abs with - | None -> (* Nothing to do *) () - | Some abs_ids1 -> - 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 = - UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs) - in - let abs_id0 = UnionFind.get abs_ref0 in - let abs_ref1 = - UnionFind.find (AbstractionId.Map.find abs_id1 merged_abs) - in - let abs_id1 = UnionFind.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 *) - - (* Debug *) - log#ldebug - (lazy - ("collapse_ctx: merging abstraction " - ^ AbstractionId.to_string abs_id1 - ^ " into " - ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx)); - - (* Update the environment - pay attention to the order: we - we merge [abs_id1] *into* [abs_id0] *) - let nctx, abs_id = - merge_into_abstraction span abs_kind can_end merge_funs - !ctx abs_id1 abs_id0 - in - ctx := nctx; - - (* Update the union find *) - let abs_ref_merged = UnionFind.union abs_ref0 abs_ref1 in - UnionFind.set abs_ref_merged abs_id)) - abs_ids1) - bids) - abs_ids; + let swap_abs info abs_id0 abs_id1 = + let abs0_borrows = + BorrowId.Set.of_list + (List.map snd + (MarkerBorrowId.Set.elements + (AbstractionId.Map.find abs_id0 info.abs_to_borrows))) + in + let abs1_loans = + BorrowId.Set.of_list + (List.map snd + (MarkerBorrowId.Set.elements + (AbstractionId.Map.find abs_id1 info.abs_to_loans))) + in + not (BorrowId.Set.disjoint abs0_borrows abs1_loans) + in + (* Check if there is an abstraction with the same borrow/loan id and the dual + marker, and merge them if it is the case. *) + let merge_policy ctx (abs_id0, is_borrow, (pm, bid)) = + if pm = PNone then None + else + (* Look for an element with the dual marker *) + match + MarkerBorrowId.Map.find_opt + (invert_proj_marker pm, bid) + (if is_borrow then ctx.info.borrow_to_abs else ctx.info.loan_to_abs) + with + | None -> (* Nothing to do *) None + | Some abs_ids1 -> ( + (* We need to merge *) + match AbstractionId.Set.elements abs_ids1 with + | [] -> None + | abs_id1 :: _ -> + (* Check if we need to swap *) + Some + (if swap_abs ctx.info abs_id0 abs_id1 then (abs_id1, abs_id0) + else (abs_id0, abs_id1))) + in + (* Iterate and merge *) + let ctx = + repeat_iter_borrows_merge span old_ids abs_kind can_end (Some merge_funs) + iter merge_policy ctx + in log#ldebug (lazy ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids ^ "\n\n- after collapse:\n" - ^ eval_ctx_to_string ~span:(Some span) !ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); - (* Reorder the loans and borrows in the fresh abstractions *) - let ctx = reorder_loans_borrows_in_fresh_abs span old_ids.aids !ctx in + (* Reorder the loans and borrows in the fresh abstractions - note that we may + not have eliminated all the markers yet *) + let ctx = reorder_loans_borrows_in_fresh_abs span true old_ids.aids ctx in log#ldebug (lazy @@ -294,6 +475,67 @@ let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) (* Return the new context *) ctx +(** Small utility: check whether an environment contains markers *) +let eval_ctx_has_markers (ctx : eval_ctx) : bool = + let visitor = + object + inherit [_] iter_eval_ctx + + method! visit_proj_marker _ pm = + match pm with PNone -> () | PLeft | PRight -> raise Found + end + in + try + visitor#visit_eval_ctx () ctx; + false + with Found -> true + +(** Collapse two environments containing projection markers; this function is called after + joining environments. + + The collapse is done in two steps. + + First, we reduce the environment, merging any two pair of fresh abstractions + which contain a loan (in one) and its corresponding borrow (in the other). + For instance, we merge abs@0 and abs@1 below: + {[ + abs@0 { |ML l0|, ML l1 } + abs@1 { |MB l0 _|, ML l2 } + ~~> + abs@2 { ML l1, ML l2 } + ]} + Note that we also merge abstractions when the loan/borrow don't have the same + markers. For instance, below: + {[ + abs@0 { ML l0, ML l1 } // ML l0 doesn't have markers + abs@1 { |MB l0 _|, ML l2 } + ~~> + abs@2 { ︙ML l0︙, ML l1, ML l2 } + ]} + + Second, we merge abstractions containing the same element with left and right markers + respectively. For instance: + {[ + abs@0 { | MB l0 _ |, ML l1 } + abs@1 { ︙MB l0 _ ︙, ML l2 } + ~~> + abs@2 { MB l0 _, ML l1, ML l2 } + ]} + + At the end of the second step, all markers should have been removed from the resulting + environment. +*) +let collapse_ctx (span : Meta.span) (loop_id : LoopId.id) + (merge_funs : merge_duplicates_funcs) (old_ids : ids_sets) (ctx0 : eval_ctx) + : eval_ctx = + let ctx = + reduce_ctx_with_markers (Some merge_funs) span loop_id old_ids ctx0 + in + let ctx = collapse_ctx_collapse span loop_id merge_funs old_ids ctx in + (* Sanity check: there are no markers remaining *) + sanity_check __FILE__ __LINE__ (not (eval_ctx_has_markers ctx)) span; + ctx + let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) (loop_id : LoopId.id) (ctx : eval_ctx) : merge_duplicates_funcs = (* Rem.: the merge functions raise exceptions (that we catch). *) @@ -314,7 +556,7 @@ 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; @@ -322,15 +564,15 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.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 - anyway (see the comments for {!merge_into_abstraction}). + anyway (see the comments for {!merge_into_first_abstraction}). *) 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 @@ -345,21 +587,22 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.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; + (* 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 +618,11 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv1.value)) 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 { @@ -388,12 +632,13 @@ let mk_collapse_ctx_merge_duplicate_funs (span : Meta.span) merge_ashared_loans; } -let merge_into_abstraction (span : Meta.span) (loop_id : LoopId.id) +let merge_into_first_abstraction (span : Meta.span) (loop_id : LoopId.id) (abs_kind : abs_kind) (can_end : bool) (ctx : eval_ctx) (aid0 : AbstractionId.id) (aid1 : AbstractionId.id) : eval_ctx * AbstractionId.id = let merge_funs = mk_collapse_ctx_merge_duplicate_funs span loop_id ctx in - merge_into_abstraction span abs_kind can_end (Some merge_funs) ctx aid0 aid1 + merge_into_first_abstraction span abs_kind can_end (Some merge_funs) ctx aid0 + aid1 (** Collapse an environment, merging the duplicated borrows/loans. @@ -405,7 +650,7 @@ let merge_into_abstraction (span : Meta.span) (loop_id : LoopId.id) let collapse_ctx_with_merge (span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = let merge_funs = mk_collapse_ctx_merge_duplicate_funs span loop_id ctx in - try collapse_ctx span loop_id (Some merge_funs) old_ids ctx + try collapse_ctx span loop_id merge_funs old_ids ctx with ValueMatchFailure _ -> craise __FILE__ __LINE__ span "Unexpected" let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) @@ -456,6 +701,17 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets) (* This should have been eliminated *) craise __FILE__ __LINE__ span "Unreachable" in + + (* Add projection marker to all abstractions in the left and right environments *) + let add_marker (pm : proj_marker) (ee : env_elem) : env_elem = + match ee with + | EAbs abs -> EAbs (abs_add_marker span ctx0 pm abs) + | x -> x + in + + let env0 = List.map (add_marker PLeft) env0 in + let env1 = List.map (add_marker PRight) env1 in + List.iter check_valid env0; List.iter check_valid env1; (* Concatenate the suffixes and append the abstractions introduced while @@ -706,11 +962,11 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span) ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); - (* Collapse the context we want to add to the join *) - let ctx = collapse_ctx span loop_id None fixed_ids ctx in + (* Reduce the context we want to add to the join *) + let ctx = reduce_ctx span loop_id fixed_ids ctx in log#ldebug (lazy - ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n" + ("loop_join_origin_with_continue_ctxs:join_one: after reduce:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); (* Refresh the fresh abstractions *) @@ -723,15 +979,20 @@ let loop_join_origin_with_continue_ctxs (config : config) (span : Meta.span) ("loop_join_origin_with_continue_ctxs:join_one: after join:\n" ^ eval_ctx_to_string ~span:(Some span) ctx1)); - (* Collapse again - the join might have introduce abstractions we want - to merge with the others (note that those abstractions may actually - lead to borrows/loans duplications) *) + (* Collapse to eliminate the markers *) joined_ctx := collapse_ctx_with_merge span loop_id fixed_ids !joined_ctx; log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n" ^ eval_ctx_to_string ~span:(Some span) !joined_ctx)); + (* Reduce again to reach a fixed point *) + joined_ctx := reduce_ctx span loop_id fixed_ids !joined_ctx; + log#ldebug + (lazy + ("loop_join_origin_with_continue_ctxs:join_one: after last reduce:\n" + ^ eval_ctx_to_string ~span:(Some span) !joined_ctx)); + (* Sanity check *) if !Config.sanity_checks then Invariants.check_invariants span !joined_ctx; (* Return *) diff --git a/compiler/InterpreterLoopsJoinCtxs.mli b/compiler/InterpreterLoopsJoinCtxs.mli index f4b5194a..a194e25b 100644 --- a/compiler/InterpreterLoopsJoinCtxs.mli +++ b/compiler/InterpreterLoopsJoinCtxs.mli @@ -15,7 +15,7 @@ open InterpreterLoopsCore - [aid0] - [aid1] *) -val merge_into_abstraction : +val merge_into_first_abstraction : Meta.span -> loop_id -> abs_kind -> diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index e25adb2c..3f7c023e 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -20,65 +20,54 @@ module S = SynthesizeSymbolic (** The local logger *) let log = Logging.loops_match_ctxs_log -let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool) - (explore : abs -> bool) (env : env) : abs_borrows_loans_maps = +let compute_abs_borrows_loans_maps (span : Meta.span) (explore : abs -> bool) + (env : env) : abs_borrows_loans_maps = let abs_ids = ref [] in let abs_to_borrows = ref AbstractionId.Map.empty in let abs_to_loans = ref AbstractionId.Map.empty in - let abs_to_borrows_loans = ref AbstractionId.Map.empty in - let borrow_to_abs = ref BorrowId.Map.empty in - let loan_to_abs = ref BorrowId.Map.empty in - let borrow_loan_to_abs = ref BorrowId.Map.empty in + let borrow_to_abs = ref MarkerBorrowId.Map.empty in + let loan_to_abs = ref MarkerBorrowId.Map.empty in - let module R (Id0 : Identifiers.Id) (Id1 : Identifiers.Id) = struct + let module R (M : Collections.Map) (S : Collections.Set) = struct (* - [check_singleton_sets]: check that the mapping maps to a singletong. - [check_not_already_registered]: check if the mapping was not already registered. + [check_singleton_sets]: check that the mapping maps to a singleton. + We need this because to tweak the behavior of the sanity checks because + of the following cases: + - when computing the map from borrow ids (with marker) to the region + abstractions they belong to, the marked borrow ids can map to a single + region abstraction, i.e., to a singleton set of region abstraction ids + - however, when computing the mapping from region abstractions to + the borrow ids they contain, this time we do map abstraction ids + to sets which can compute strictly more than one value *) - 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 -> - sanity_check __FILE__ __LINE__ - ((not check_not_already_registered) || not (Id1.Set.mem id1 set)) - span); + let register_mapping (check_singleton_sets : bool) (map : S.t M.t ref) + (id0 : M.key) (id1 : S.elt) : unit = (* Update the mapping *) map := - Id0.Map.update id0 + M.update id0 (fun ids -> match ids with - | None -> Some (Id1.Set.singleton id1) + | None -> Some (S.singleton id1) | Some ids -> - (* Sanity check *) + (* Check that we are allowed to map id0 to a set which is not + a singleton *) sanity_check __FILE__ __LINE__ (not check_singleton_sets) span; - sanity_check __FILE__ __LINE__ - ((not check_not_already_registered) - || not (Id1.Set.mem id1 ids)) - span; + (* Check that the mapping was not already registered *) + sanity_check __FILE__ __LINE__ (not (S.mem id1 ids)) span; (* Update *) - Some (Id1.Set.add id1 ids)) + Some (S.add id1 ids)) !map end in - let module RAbsBorrow = R (AbstractionId) (BorrowId) in - let module RBorrowAbs = R (BorrowId) (AbstractionId) in - let register_borrow_id abs_id bid = - 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 + let module RAbsBorrow = R (AbstractionId.Map) (MarkerBorrowId.Set) in + let module RBorrowAbs = R (MarkerBorrowId.Map) (AbstractionId.Set) in + let register_borrow_id abs_id pm bid = + RAbsBorrow.register_mapping false abs_to_borrows abs_id (pm, bid); + RBorrowAbs.register_mapping true borrow_to_abs (pm, bid) abs_id in - let register_loan_id abs_id bid = - 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 + let register_loan_id abs_id pm bid = + RAbsBorrow.register_mapping false abs_to_loans abs_id (pm, bid); + RBorrowAbs.register_mapping true loan_to_abs (pm, bid) abs_id in let explore_abs = @@ -86,35 +75,58 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool) inherit [_] iter_typed_avalue as super (** Make sure we don't register the ignored ids *) - method! visit_aloan_content abs_id lc = + method! visit_aloan_content (abs_id, pm) lc = + sanity_check __FILE__ __LINE__ (pm = PNone) span; match lc with - | AMutLoan _ | ASharedLoan _ -> - (* Process those normally *) - super#visit_aloan_content abs_id lc + | AMutLoan (npm, lid, child) -> + (* Add the current marker when visiting the loan id *) + self#visit_loan_id (abs_id, npm) lid; + (* Recurse with the old marker *) + super#visit_typed_avalue (abs_id, pm) child + | ASharedLoan (npm, lids, sv, child) -> + (* Add the current marker when visiting the loan ids and the shared value *) + self#visit_loan_id_set (abs_id, npm) lids; + self#visit_typed_value (abs_id, npm) sv; + (* Recurse with the old marker *) + self#visit_typed_avalue (abs_id, pm) child | AIgnoredMutLoan (_, child) | AEndedIgnoredMutLoan { child; given_back = _; given_back_span = _ } | AIgnoredSharedLoan child -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Ignore the id of the loan, if there is *) - self#visit_typed_avalue abs_id child + self#visit_typed_avalue (abs_id, pm) child | AEndedMutLoan _ | AEndedSharedLoan _ -> craise __FILE__ __LINE__ span "Unreachable" (** Make sure we don't register the ignored ids *) - method! visit_aborrow_content abs_id bc = + method! visit_aborrow_content (abs_id, pm) bc = + sanity_check __FILE__ __LINE__ (pm = PNone) span; match bc with - | AMutBorrow _ | ASharedBorrow _ | AProjSharedBorrow _ -> + | AMutBorrow (npm, bid, child) -> + (* Add the current marker when visiting the borrow id *) + self#visit_borrow_id (abs_id, npm) bid; + (* Recurse with the old marker *) + self#visit_typed_avalue (abs_id, pm) child + | ASharedBorrow (npm, bid) -> + (* Add the current marker when visiting the borrow id *) + self#visit_borrow_id (abs_id, npm) bid + | AProjSharedBorrow _ -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Process those normally *) - super#visit_aborrow_content abs_id bc + super#visit_aborrow_content (abs_id, pm) bc | AIgnoredMutBorrow (_, child) | AEndedIgnoredMutBorrow { child; given_back = _; given_back_span = _ } -> + sanity_check __FILE__ __LINE__ (pm = PNone) span; (* Ignore the id of the borrow, if there is *) - self#visit_typed_avalue abs_id child + self#visit_typed_avalue (abs_id, pm) child | AEndedMutBorrow _ | AEndedSharedBorrow -> craise __FILE__ __LINE__ span "Unreachable" - method! visit_borrow_id abs_id bid = register_borrow_id abs_id bid - method! visit_loan_id abs_id lid = register_loan_id abs_id lid + method! visit_borrow_id (abs_id, pm) bid = + register_borrow_id abs_id pm bid + + method! visit_loan_id (abs_id, pm) lid = register_loan_id abs_id pm lid end in @@ -123,11 +135,13 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool) let abs_id = abs.abs_id in if explore abs then ( abs_to_borrows := - AbstractionId.Map.add abs_id BorrowId.Set.empty !abs_to_borrows; + AbstractionId.Map.add abs_id MarkerBorrowId.Set.empty !abs_to_borrows; abs_to_loans := - AbstractionId.Map.add abs_id BorrowId.Set.empty !abs_to_loans; + AbstractionId.Map.add abs_id MarkerBorrowId.Set.empty !abs_to_loans; abs_ids := abs.abs_id :: !abs_ids; - List.iter (explore_abs#visit_typed_avalue abs.abs_id) abs.avalues) + List.iter + (explore_abs#visit_typed_avalue (abs.abs_id, PNone)) + abs.avalues) else ()) env; @@ -137,10 +151,8 @@ let compute_abs_borrows_loans_maps (span : Meta.span) (no_duplicates : bool) abs_ids = !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; } (** Match two types during a join. @@ -353,10 +365,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 +376,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 +406,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 - @@ -503,14 +518,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in (* Generate the avalues for the abstraction *) - let mk_aborrow (bid : borrow_id) : typed_avalue = - let value = ABorrow (ASharedBorrow bid) in + let mk_aborrow (pm : proj_marker) (bid : borrow_id) : typed_avalue = + let value = ABorrow (ASharedBorrow (pm, bid)) in { value; ty = borrow_ty } in - let borrows = [ mk_aborrow bid0; mk_aborrow bid1 ] in + let borrows = [ mk_aborrow PLeft bid0; mk_aborrow PRight 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 @@ -543,7 +559,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct an abstraction: {[ - { MB bid0, ML nbid } // where nbid fresh + { MB bid0, ML bid' } // where bid' fresh ]} and we use bid' for the borrow id that we return. @@ -551,7 +567,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct We do this because we want to make sure that, whenever a mutably borrowed value is modified in a loop iteration, then there is a fresh abstraction between this borrowed value and the fixed - abstractions. + abstractions (this is tantamount to introducing a reborrow). Example: ======== @@ -582,6 +598,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct to say [unit]) while the backward loop function gives back a new value for [v] (i.e., a new symbolic value which will replace [s0]). + By introducing the fresh region abstraction wet get: + {[ + abs'0 { ML l0 } // input abstraction + abs'1 { MB l0, ML l1 } // fresh abstraction + v -> MB l1 s1 + i -> 0 + ]} + + In the future, we will also compute joins at the *loop exits*: when we do so, we won't introduce reborrows like above: the forward loop function will update [v], while the backward loop function will return nothing. @@ -599,18 +624,21 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let kind = RMut in let bv_ty = bv.ty in - sanity_check __FILE__ __LINE__ (ty_no_regions bv_ty) span; + cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span + "Nested borrows are not supported yet"; let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in 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 @@ -635,9 +663,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (nbid, bv)) else (* We replace bid0 and bid1 with a fresh borrow id, and introduce - an abstraction which links all of them: + an abstraction which links all of them. This time we have to introduce + markers: {[ - { MB bid0, MB bid1, ML bid2 } + { |MB bid0|, ︙MB bid1︙, ML bid2 } ]} *) let rid = fresh_region_id () in @@ -650,16 +679,17 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in (* Generate the avalues for the abstraction *) - let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = + let mk_aborrow (pm : proj_marker) (bid : borrow_id) (bv : typed_value) : + typed_avalue = 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 (pm, bid, mk_aignored span bv_ty)) in { value; ty = borrow_ty } in - let borrows = [ mk_aborrow bid0 bv0; mk_aborrow bid1 bv1 ] in + let borrows = [ mk_aborrow PLeft bid0 bv0; mk_aborrow PRight 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 @@ -744,24 +774,16 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Check that: - there are no borrows in the symbolic value - there are no borrows in the "regular" value - If there are loans in the regular value, raise an exception. *) let type_infos = ctx0.type_ctx.type_infos in - cassert __FILE__ __LINE__ + sanity_check __FILE__ __LINE__ (not (ty_has_borrows type_infos sv.sv_ty)) - span - "Check that:\n\ - \ - there are no borrows in the symbolic value\n\ - \ - there are no borrows in the \"regular\" value\n\ - \ If there are loans in the regular value, raise an exception."; - cassert __FILE__ __LINE__ + span; + sanity_check __FILE__ __LINE__ (not (ValuesUtils.value_has_borrows type_infos v.value)) - span - "Check that:\n\ - \ - there are no borrows in the symbolic value\n\ - \ - there are no borrows in the \"regular\" value\n\ - \ If there are loans in the regular value, raise an exception."; + span; let value_is_left = not left in + (* If there are loans in the regular value, raise an exception. *) (match InterpreterBorrowsCore.get_first_loan_in_value v with | None -> () | Some (VSharedLoan (ids, _)) -> @@ -781,13 +803,13 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct then mk_bottom span sv.sv_ty else mk_fresh_symbolic_typed_value span sv.sv_ty - let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) - (v : typed_value) : typed_value = + let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) + (bottom_is_left : bool) (v : typed_value) : typed_value = + let value_is_left = not bottom_is_left in (* If there are outer loans in the non-bottom value, raise an exception. Otherwise, convert it to an abstraction and return [Bottom]. *) let with_borrows = false in - let value_is_left = not left in match InterpreterBorrowsCore.get_first_outer_loan_or_borrow_in_value with_borrows v @@ -804,8 +826,6 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) else raise (ValueMatchFailure (LoanInRight id))) | None -> - (* *) - (* Convert the value to an abstraction *) let abs_kind : abs_kind = Loop (S.loop_id, None, LoopSynthInput) in let can_end = true in @@ -815,6 +835,9 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct convert_value_to_abstractions span abs_kind can_end destructure_shared_values ctx v in + (* Add a marker to the abstraction indicating the provenance of the value *) + let pm = if value_is_left then PLeft else PRight in + let absl = List.map (abs_add_marker span ctx0 pm) absl in push_absl absl; (* Return [Bottom] *) mk_bottom span v.ty @@ -1213,26 +1236,38 @@ 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 = + (* We are checking whether that two environments are equivalent: + there shouldn't be any projection markers *) + 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 = + (* We are checking whether that two environments are equivalent: + there shouldn't be any projection markers *) + 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 = + (* We are checking whether that two environments are equivalent: + there shouldn't be any projection markers *) + 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 = + (* We are checking whether that two environments are equivalent: + there shouldn't be any projection markers *) + sanity_check __FILE__ __LINE__ (pm0 = PNone && pm1 = PNone) span; log#ldebug (lazy ("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: " @@ -1241,7 +1276,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 +1741,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/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli index ab585220..cd807358 100644 --- a/compiler/InterpreterLoopsMatchCtxs.mli +++ b/compiler/InterpreterLoopsMatchCtxs.mli @@ -13,13 +13,11 @@ open InterpreterLoopsCore (** Compute various maps linking the abstractions and the borrows/loans they contain. Parameters: - - [no_duplicates]: checks that borrows/loans are not referenced more than once - (see the documentation for {!type:InterpreterLoopsCore.abs_borrows_loans_maps}). - [explore]: this function is used to filter abstractions. - [env] *) val compute_abs_borrows_loans_maps : - Meta.span -> bool -> (abs -> bool) -> env -> abs_borrows_loans_maps + Meta.span -> (abs -> bool) -> env -> abs_borrows_loans_maps (** Generic functor to implement matching functions between values, environments, etc. @@ -188,7 +186,7 @@ val prepare_match_ctx_with_target : We want to introduce an abstraction [abs@2], which has the same shape as [abs@fp] above (the fixed-point abstraction), and which is actually the identity. If we do so, - we get an environment which is actually also a fixed point (we can collapse + we get an environment which is actually also a fixed point (we can reduce the dummy variables and [abs@1] to actually retrieve the fixed point we computed, and we use the fact that those values and abstractions can't be *directly* manipulated unless we end this newly introduced [abs@2], which we diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index faba1088..b2de3b22 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: projection 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/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index c60be905..5ddc1ed8 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -914,117 +914,113 @@ let rec eval_statement (config : config) (st : statement) : stl_cm_fun = (* Sanity check *) Invariants.check_invariants st.span ctx; - (* Evaluate *) - let stl, cf_eval_st = - log#ldebug - (lazy - ("\neval_statement: cf_eval_st: statement:\n" - ^ statement_to_string_with_tab ctx st - ^ "\n\n")); - match st.content with - | Assign (p, rvalue) -> ( - (* We handle global assignments separately *) - match rvalue with - | Global (gid, generics) -> - (* Evaluate the global *) - eval_global config st.span p gid generics ctx - | _ -> - (* Evaluate the rvalue *) - let res, ctx, cc = - eval_rvalue_not_global config st.span rvalue ctx - in - (* Assign *) - log#ldebug - (lazy - ("about to assign to place: " ^ place_to_string ctx p - ^ "\n- Context:\n" - ^ eval_ctx_to_string ~span:(Some st.span) ctx)); - let (ctx, res), cf_assign = - match res with - | Error EPanic -> ((ctx, Panic), fun e -> e) - | Ok rv -> - (* Update the synthesized AST - here we store additional span-information. - * We do it only in specific cases (it is not always useful, and - * also it can lead to issues - for instance, if we borrow a - * reserved borrow, we later can't translate it to pure values...) *) - let cc = - match rvalue with - | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" - | Len _ -> craise __FILE__ __LINE__ st.span "Unhandled Len" - | Use _ - | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) - | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> - let rp = rvalue_get_place rvalue in - let rp = - match rp with - | Some rp -> Some (S.mk_mplace st.span rp ctx) - | None -> None - in - S.synthesize_assignment ctx - (S.mk_mplace st.span p ctx) - rv rp - in - let ctx, cc = - comp cc (assign_to_place config st.span rv p ctx) - in - ((ctx, Unit), cc) - in - let cc = cc_comp cc cf_assign in - (* Compose and apply *) - ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc)) - | FakeRead p -> - let ctx, cc = eval_fake_read config st.span p ctx in - ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) - | SetDiscriminant (p, variant_id) -> - let (ctx, res), cc = set_discriminant config st.span p variant_id ctx in - ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Drop p -> - let ctx, cc = drop_value config st.span p ctx in - ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Assert assertion -> - let (ctx, res), cc = eval_assertion config st.span assertion ctx in - ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Call call -> eval_function_call config st.span call ctx - | Panic -> ([ (ctx, Panic) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Return -> ([ (ctx, Return) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Break i -> ([ (ctx, Break i) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Continue i -> - ([ (ctx, Continue i) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Nop -> ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) - | Sequence (st1, st2) -> - (* Evaluate the first statement *) - let ctx_resl, cf_st1 = eval_statement config st1 ctx in - (* Evaluate the sequence (evaluate the second statement if the first - statement successfully evaluated, otherwise transfmit the control-flow - break) *) - let ctx_res_cfl = - List.map - (fun (ctx, res) -> - match res with - (* Evaluation successful: evaluate the second statement *) - | Unit -> eval_statement config st2 ctx - (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Panic | Break _ | Continue _ | Return | LoopReturn _ - | EndEnterLoop _ | EndContinue _ -> - ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc)) - ctx_resl - in - (* Put everything together: - - we return the flattened list of contexts and results - - we need to build the continuation which will build the whole - expression from the continuations for the individual branches - *) - let ctx_resl, cf_st2 = - comp_seqs __FILE__ __LINE__ st.span ctx_res_cfl - in - (ctx_resl, cc_comp cf_st1 cf_st2) - | Loop loop_body -> - let eval_loop_body = eval_statement config loop_body in - InterpreterLoops.eval_loop config st.span eval_loop_body ctx - | Switch switch -> eval_switch config st.span switch ctx - in - (* Compose and apply *) - (stl, cc_comp cc cf_eval_st) + (* Evaluate the statement *) + comp cc (eval_statement_raw config st ctx) + +and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = + fun ctx -> + log#ldebug + (lazy + ("\neval_statement_raw: statement:\n" + ^ statement_to_string_with_tab ctx st + ^ "\n\n")); + match st.content with + | Assign (p, rvalue) -> ( + (* We handle global assignments separately *) + match rvalue with + | Global (gid, generics) -> + (* Evaluate the global *) + eval_global config st.span p gid generics ctx + | _ -> + (* Evaluate the rvalue *) + let res, ctx, cc = eval_rvalue_not_global config st.span rvalue ctx in + (* Assign *) + log#ldebug + (lazy + ("about to assign to place: " ^ place_to_string ctx p + ^ "\n- Context:\n" + ^ eval_ctx_to_string ~span:(Some st.span) ctx)); + let (ctx, res), cf_assign = + match res with + | Error EPanic -> ((ctx, Panic), fun e -> e) + | Ok rv -> + (* Update the synthesized AST - here we store additional span-information. + * We do it only in specific cases (it is not always useful, and + * also it can lead to issues - for instance, if we borrow a + * reserved borrow, we later can't translate it to pure values...) *) + let cc = + match rvalue with + | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" + | Len _ -> + craise __FILE__ __LINE__ st.span "Len is not handled yet" + | Use _ + | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) + | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> + let rp = rvalue_get_place rvalue in + let rp = + match rp with + | Some rp -> Some (S.mk_mplace st.span rp ctx) + | None -> None + in + S.synthesize_assignment ctx + (S.mk_mplace st.span p ctx) + rv rp + in + let ctx, cc = + comp cc (assign_to_place config st.span rv p ctx) + in + ((ctx, Unit), cc) + in + let cc = cc_comp cc cf_assign in + (* Compose and apply *) + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc)) + | FakeRead p -> + let ctx, cc = eval_fake_read config st.span p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) + | SetDiscriminant (p, variant_id) -> + let (ctx, res), cc = set_discriminant config st.span p variant_id ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Drop p -> + let ctx, cc = drop_value config st.span p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Assert assertion -> + let (ctx, res), cc = eval_assertion config st.span assertion ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.span cc) + | Call call -> eval_function_call config st.span call ctx + | Panic -> ([ (ctx, Panic) ], cf_singleton __FILE__ __LINE__ st.span) + | Return -> ([ (ctx, Return) ], cf_singleton __FILE__ __LINE__ st.span) + | Break i -> ([ (ctx, Break i) ], cf_singleton __FILE__ __LINE__ st.span) + | Continue i -> ([ (ctx, Continue i) ], cf_singleton __FILE__ __LINE__ st.span) + | Nop -> ([ (ctx, Unit) ], cf_singleton __FILE__ __LINE__ st.span) + | Sequence (st1, st2) -> + (* Evaluate the first statement *) + let ctx_resl, cf_st1 = eval_statement config st1 ctx in + (* Evaluate the sequence (evaluate the second statement if the first + statement successfully evaluated, otherwise transfmit the control-flow + break) *) + let ctx_res_cfl = + List.map + (fun (ctx, res) -> + match res with + (* Evaluation successful: evaluate the second statement *) + | Unit -> eval_statement config st2 ctx + (* Control-flow break: transmit. We enumerate the cases on purpose *) + | Panic | Break _ | Continue _ | Return | LoopReturn _ + | EndEnterLoop _ | EndContinue _ -> + ([ (ctx, res) ], cf_singleton __FILE__ __LINE__ st.span)) + ctx_resl + in + (* Put everything together: + - we return the flattened list of contexts and results + - we need to build the continuation which will build the whole + expression from the continuations for the individual branches + *) + let ctx_resl, cf_st2 = comp_seqs __FILE__ __LINE__ st.span ctx_res_cfl in + (ctx_resl, cc_comp cf_st1 cf_st2) + | Loop loop_body -> + let eval_loop_body = eval_statement config loop_body in + InterpreterLoops.eval_loop config st.span eval_loop_body ctx + | Switch switch -> eval_switch config st.span switch ctx and eval_global (config : config) (span : Meta.span) (dest : place) (gid : GlobalDeclId.id) (generics : generic_args) : stl_cm_fun = @@ -1610,11 +1606,11 @@ and eval_function_body (config : config) (body : statement) : stl_cm_fun = let ctx_res_cfl = List.map (fun (ctx, res) -> - log#ldebug (lazy "eval_function_body: cf_finish"); (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we - * delegate the check to the caller. *) + delegate the check to the caller. *) + log#ldebug (lazy "eval_function_body: cf_finish"); (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) + checking the invariants *) let ctx, cf = greedy_expand_symbolic_values config body.span ctx in (* Sanity check *) Invariants.check_invariants body.span ctx; diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 51be02c8..50e6e87f 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 _ @@ -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 _ -> @@ -497,11 +497,13 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | VBorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with | VSharedBorrow bid, RShared | VReservedMutBorrow bid, RMut -> ( - (* Lookup the borrowed value to check it has the proper type *) + (* Lookup the borrowed value to check it has the proper type. + Note that we ignore the marker: we will check it when + checking the loan itself. *) 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 = ref_ty) span | _ -> craise __FILE__ __LINE__ span "Inconsistent context") | VMutBorrow (_, bv), RMut -> @@ -515,12 +517,14 @@ let check_typing_invariant (span : Meta.span) (ctx : eval_ctx) : unit = | VSharedLoan (_, sv) -> sanity_check __FILE__ __LINE__ (sv.ty = ty) span | VMutLoan bid -> ( - (* Lookup the borrowed value to check it has the proper type *) + (* Lookup the borrowed value to check it has the proper type. *) let glc = lookup_borrow span ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> sanity_check __FILE__ __LINE__ (bv.ty = ty) span - | Abstract (AMutBorrow (_, sv)) -> + | Abstract (AMutBorrow (pm, _, sv)) -> + (* The marker check is redundant, but doesn't cost much *) + sanity_check __FILE__ __LINE__ (pm = PNone) span; sanity_check __FILE__ __LINE__ (Substitute.erase_regions sv.ty = ty) span @@ -610,15 +614,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 @@ -633,8 +639,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 *) @@ -644,22 +650,29 @@ 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 (_, _, _) -> + (* We get there if the projection marker is not [PNone] *) + 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 (_, _, _, _) -> + (* We get there if the projection marker is not [PNone] *) + 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/Print.ml b/compiler/Print.ml index f7f1f54b..7495d6bf 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -148,6 +148,13 @@ module Values = struct | AEndedProjBorrows _mv -> "_" | AIgnoredProjBorrows -> "_" + (** Wrap a value inside its marker, if there is one *) + 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 +204,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 +247,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/Substitute.ml b/compiler/Substitute.ml index 37ef6987..6ea460db 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -138,10 +138,10 @@ let subst_ids_visitor (r_subst : RegionId.id -> RegionId.id) method! visit_loan_id _ bid = bsubst bid method! visit_symbolic_value_id _ id = ssubst id - (** We *do* visit span-values *) + (** We *do* visit meta-values *) method! visit_msymbolic_value env sv = self#visit_symbolic_value env sv - (** We *do* visit span-values *) + (** We *do* visit meta-values *) method! visit_mvalue env v = self#visit_typed_value env v method! visit_abstraction_id _ id = asubst id diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index e9143ab5..750297e4 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -37,7 +37,7 @@ type call_id = type call = { call_id : call_id; - ctx : Contexts.eval_ctx; + ctx : (Contexts.eval_ctx[@opaque]); (** The context upon calling the function (after the operands have been evaluated). We need it to compute the translated values for shared borrows (we need to perform lookups). @@ -123,9 +123,9 @@ class ['self] iter_expression_base = (** **Rem.:** here, {!expression} is not at all equivalent to the expressions used in LLBC or in lambda-calculus: they are simply a first step towards lambda-calculus expressions. - *) +*) type expression = - | Return of Contexts.eval_ctx * typed_value option + | Return of (Contexts.eval_ctx[@opaque]) * typed_value option (** There are two cases: - the AST is for a forward function: the typed value should contain the value which was in the return variable @@ -137,7 +137,7 @@ type expression = *) | Panic | FunCall of call * expression - | EndAbstraction of Contexts.eval_ctx * abs * expression + | EndAbstraction of (Contexts.eval_ctx[@opaque]) * abs * expression (** The context is the evaluation context upon ending the abstraction, just after we removed the abstraction from the context. @@ -146,7 +146,7 @@ type expression = *) | EvalGlobal of global_decl_id * generic_args * symbolic_value * expression (** Evaluate a global to a fresh symbolic value *) - | Assertion of Contexts.eval_ctx * typed_value * expression + | Assertion of (Contexts.eval_ctx[@opaque]) * typed_value * expression (** An assertion. The context is the evaluation context from after evaluating the asserted @@ -162,7 +162,7 @@ type expression = to prettify the generated code. *) | IntroSymbolic of - Contexts.eval_ctx + (Contexts.eval_ctx[@opaque]) * mplace option * symbolic_value * value_aggregate @@ -179,7 +179,7 @@ type expression = value. It has the same purpose as for the {!Return} case. *) | ForwardEnd of - Contexts.eval_ctx + (Contexts.eval_ctx[@opaque]) * typed_value symbolic_value_id_map option * expression * expression region_group_id_map @@ -211,7 +211,7 @@ type expression = The boolean is [true]. TODO: merge this with Return. *) - | Meta of espan * expression (** Meta information *) + | Meta of (espan[@opaque]) * expression (** Meta information *) | Error of Meta.span option * string and loop = { diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index cc203040..848bfe50 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 e7b96051..c32cbc6e 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] @@ -176,6 +176,41 @@ 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] + +type marker_borrow_id = proj_marker * BorrowId.id [@@deriving show, ord] + +module MarkerBorrowIdOrd = struct + type t = marker_borrow_id + + let compare = compare_marker_borrow_id + let to_string = show_marker_borrow_id + let pp_t = pp_marker_borrow_id + let show_t = show_marker_borrow_id +end + +module MarkerBorrowIdSet = Collections.MakeSet (MarkerBorrowIdOrd) +module MarkerBorrowIdMap = Collections.MakeMap (MarkerBorrowIdOrd) + +module MarkerBorrowId : sig + type t + + val to_string : t -> string + + module Set : Collections.Set with type elt = t + module Map : Collections.Map with type key = t +end +with type t = marker_borrow_id = struct + type t = marker_borrow_id + + let to_string = show_marker_borrow_id + + module Set = MarkerBorrowIdSet + module Map = MarkerBorrowIdMap +end + (** Ancestor for {!typed_avalue} iter visitor *) class ['self] iter_typed_avalue_base = object (self : 'self) @@ -192,6 +227,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 +249,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 @@ -270,7 +309,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 @@ -282,14 +321,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 @@ -333,7 +372,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 +393,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 +546,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 +567,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: @@ -613,7 +652,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 diff --git a/tests/coq/arrays/_CoqProject b/tests/coq/arrays/_CoqProject index a4e82408..4ccc7663 100644 --- a/tests/coq/arrays/_CoqProject +++ b/tests/coq/arrays/_CoqProject @@ -3,5 +3,5 @@ -arg -w -arg all -Arrays.v +Arrays.v Primitives.v diff --git a/tests/coq/demo/_CoqProject b/tests/coq/demo/_CoqProject index 62554699..67e4f2a4 100644 --- a/tests/coq/demo/_CoqProject +++ b/tests/coq/demo/_CoqProject @@ -3,5 +3,5 @@ -arg -w -arg all -Demo.v +Demo.v Primitives.v diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject index 7f80afbf..5d98662a 100644 --- a/tests/coq/hashmap/_CoqProject +++ b/tests/coq/hashmap/_CoqProject @@ -3,6 +3,6 @@ -arg -w -arg all -Hashmap_Types.v +Hashmap_Funs.v +Hashmap_Types.v Primitives.v -Hashmap_Funs.v diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 2cc6af6c..b3e59172 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -243,14 +243,19 @@ Check (choose_test )%return. Definition test_char : result char := Ok (char_of_byte Coq.Init.Byte.x61). +(** [no_nested_borrows::panic_mut_borrow]: + Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:36 *) +Definition panic_mut_borrow (i : u32) : result u32 := + Fail_ Failure. + (** [no_nested_borrows::Tree] - Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:16 *) + Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:16 *) Inductive Tree_t (T : Type) := | Tree_Leaf : T -> Tree_t T | Tree_Node : T -> NodeElem_t T -> Tree_t T -> Tree_t T (** [no_nested_borrows::NodeElem] - Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:20 *) + Source: 'tests/src/no_nested_borrows.rs', lines 230:0-230:20 *) with NodeElem_t (T : Type) := | NodeElem_Cons : Tree_t T -> NodeElem_t T -> NodeElem_t T | NodeElem_Nil : NodeElem_t T @@ -263,7 +268,7 @@ Arguments NodeElem_Cons { _ }. Arguments NodeElem_Nil { _ }. (** [no_nested_borrows::list_length]: - Source: 'tests/src/no_nested_borrows.rs', lines 260:0-260:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 265:0-265:48 *) Fixpoint list_length (T : Type) (l : List_t T) : result u32 := match l with | List_Cons _ l1 => i <- list_length T l1; u32_add 1%u32 i @@ -272,7 +277,7 @@ Fixpoint list_length (T : Type) (l : List_t T) : result u32 := . (** [no_nested_borrows::list_nth_shared]: - Source: 'tests/src/no_nested_borrows.rs', lines 268:0-268:62 *) + Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 *) Fixpoint list_nth_shared (T : Type) (l : List_t T) (i : u32) : result T := match l with | List_Cons x tl => @@ -284,7 +289,7 @@ Fixpoint list_nth_shared (T : Type) (l : List_t T) (i : u32) : result T := . (** [no_nested_borrows::list_nth_mut]: - Source: 'tests/src/no_nested_borrows.rs', lines 284:0-284:67 *) + Source: 'tests/src/no_nested_borrows.rs', lines 289:0-289:67 *) Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result (T * (T -> result (List_t T))) @@ -305,7 +310,7 @@ Fixpoint list_nth_mut . (** [no_nested_borrows::list_rev_aux]: - Source: 'tests/src/no_nested_borrows.rs', lines 300:0-300:63 *) + Source: 'tests/src/no_nested_borrows.rs', lines 305:0-305:63 *) Fixpoint list_rev_aux (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) := match li with @@ -315,14 +320,14 @@ Fixpoint list_rev_aux . (** [no_nested_borrows::list_rev]: - Source: 'tests/src/no_nested_borrows.rs', lines 314:0-314:42 *) + Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 *) Definition list_rev (T : Type) (l : List_t T) : result (List_t T) := let (li, _) := core_mem_replace (List_t T) l List_Nil in list_rev_aux T li List_Nil . (** [no_nested_borrows::test_list_functions]: - Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:28 *) + Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 *) Definition test_list_functions : result unit := let l := List_Cons 2%i32 List_Nil in let l1 := List_Cons 1%i32 l in @@ -361,7 +366,7 @@ Definition test_list_functions : result unit := Check (test_list_functions )%return. (** [no_nested_borrows::id_mut_pair1]: - Source: 'tests/src/no_nested_borrows.rs', lines 335:0-335:89 *) + Source: 'tests/src/no_nested_borrows.rs', lines 340:0-340:89 *) Definition id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) @@ -370,7 +375,7 @@ Definition id_mut_pair1 . (** [no_nested_borrows::id_mut_pair2]: - Source: 'tests/src/no_nested_borrows.rs', lines 339:0-339:88 *) + Source: 'tests/src/no_nested_borrows.rs', lines 344:0-344:88 *) Definition id_mut_pair2 (T1 T2 : Type) (p : (T1 * T2)) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) @@ -379,7 +384,7 @@ Definition id_mut_pair2 . (** [no_nested_borrows::id_mut_pair3]: - Source: 'tests/src/no_nested_borrows.rs', lines 343:0-343:93 *) + Source: 'tests/src/no_nested_borrows.rs', lines 348:0-348:93 *) Definition id_mut_pair3 (T1 T2 : Type) (x : T1) (y : T2) : result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2)) @@ -388,7 +393,7 @@ Definition id_mut_pair3 . (** [no_nested_borrows::id_mut_pair4]: - Source: 'tests/src/no_nested_borrows.rs', lines 347:0-347:92 *) + Source: 'tests/src/no_nested_borrows.rs', lines 352:0-352:92 *) Definition id_mut_pair4 (T1 T2 : Type) (p : (T1 * T2)) : result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2)) @@ -397,7 +402,7 @@ Definition id_mut_pair4 . (** [no_nested_borrows::StructWithTuple] - Source: 'tests/src/no_nested_borrows.rs', lines 354:0-354:34 *) + Source: 'tests/src/no_nested_borrows.rs', lines 359:0-359:34 *) Record StructWithTuple_t (T1 T2 : Type) := mkStructWithTuple_t { structWithTuple_p : (T1 * T2); @@ -408,25 +413,25 @@ Arguments mkStructWithTuple_t { _ _ }. Arguments structWithTuple_p { _ _ }. (** [no_nested_borrows::new_tuple1]: - Source: 'tests/src/no_nested_borrows.rs', lines 358:0-358:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 *) Definition new_tuple1 : result (StructWithTuple_t u32 u32) := Ok {| structWithTuple_p := (1%u32, 2%u32) |} . (** [no_nested_borrows::new_tuple2]: - Source: 'tests/src/no_nested_borrows.rs', lines 362:0-362:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 *) Definition new_tuple2 : result (StructWithTuple_t i16 i16) := Ok {| structWithTuple_p := (1%i16, 2%i16) |} . (** [no_nested_borrows::new_tuple3]: - Source: 'tests/src/no_nested_borrows.rs', lines 366:0-366:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 *) Definition new_tuple3 : result (StructWithTuple_t u64 i64) := Ok {| structWithTuple_p := (1%u64, 2%i64) |} . (** [no_nested_borrows::StructWithPair] - Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:33 *) + Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 *) Record StructWithPair_t (T1 T2 : Type) := mkStructWithPair_t { structWithPair_p : Pair_t T1 T2; @@ -437,13 +442,13 @@ Arguments mkStructWithPair_t { _ _ }. Arguments structWithPair_p { _ _ }. (** [no_nested_borrows::new_pair1]: - Source: 'tests/src/no_nested_borrows.rs', lines 375:0-375:46 *) + Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 *) Definition new_pair1 : result (StructWithPair_t u32 u32) := Ok {| structWithPair_p := {| pair_x := 1%u32; pair_y := 2%u32 |} |} . (** [no_nested_borrows::test_constants]: - Source: 'tests/src/no_nested_borrows.rs', lines 383:0-383:23 *) + Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 *) Definition test_constants : result unit := swt <- new_tuple1; let (i, _) := swt.(structWithTuple_p) in @@ -470,7 +475,7 @@ Definition test_constants : result unit := Check (test_constants )%return. (** [no_nested_borrows::test_weird_borrows1]: - Source: 'tests/src/no_nested_borrows.rs', lines 392:0-392:28 *) + Source: 'tests/src/no_nested_borrows.rs', lines 397:0-397:28 *) Definition test_weird_borrows1 : result unit := Ok tt. @@ -478,78 +483,78 @@ Definition test_weird_borrows1 : result unit := Check (test_weird_borrows1 )%return. (** [no_nested_borrows::test_mem_replace]: - Source: 'tests/src/no_nested_borrows.rs', lines 402:0-402:37 *) + Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 *) Definition test_mem_replace (px : u32) : result u32 := let (y, _) := core_mem_replace u32 px 1%u32 in if negb (y s= 0%u32) then Fail_ Failure else Ok 2%u32 . (** [no_nested_borrows::test_shared_borrow_bool1]: - Source: 'tests/src/no_nested_borrows.rs', lines 409:0-409:47 *) + Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 *) Definition test_shared_borrow_bool1 (b : bool) : result u32 := if b then Ok 0%u32 else Ok 1%u32 . (** [no_nested_borrows::test_shared_borrow_bool2]: - Source: 'tests/src/no_nested_borrows.rs', lines 422:0-422:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 *) Definition test_shared_borrow_bool2 : result u32 := Ok 0%u32. (** [no_nested_borrows::test_shared_borrow_enum1]: - Source: 'tests/src/no_nested_borrows.rs', lines 437:0-437:52 *) + Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 *) Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 := match l with | List_Cons _ _ => Ok 1%u32 | List_Nil => Ok 0%u32 end . (** [no_nested_borrows::test_shared_borrow_enum2]: - Source: 'tests/src/no_nested_borrows.rs', lines 449:0-449:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 *) Definition test_shared_borrow_enum2 : result u32 := Ok 0%u32. (** [no_nested_borrows::incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 460:0-460:24 *) + Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 *) Definition incr (x : u32) : result u32 := u32_add x 1%u32. (** [no_nested_borrows::call_incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 464:0-464:35 *) + Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 *) Definition call_incr (x : u32) : result u32 := incr x. (** [no_nested_borrows::read_then_incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:41 *) + Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 *) Definition read_then_incr (x : u32) : result (u32 * u32) := x1 <- u32_add x 1%u32; Ok (x, x1) . (** [no_nested_borrows::Tuple] - Source: 'tests/src/no_nested_borrows.rs', lines 475:0-475:24 *) + Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 *) Definition Tuple_t (T1 T2 : Type) : Type := T1 * T2. (** [no_nested_borrows::use_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 477:0-477:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 *) Definition use_tuple_struct (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) := let (_, i) := x in Ok (1%u32, i) . (** [no_nested_borrows::create_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 481:0-481:61 *) + Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 *) Definition create_tuple_struct (x : u32) (y : u64) : result (Tuple_t u32 u64) := Ok (x, y) . (** [no_nested_borrows::IdType] - Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:20 *) + Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 *) Definition IdType_t (T : Type) : Type := T. (** [no_nested_borrows::use_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 488:0-488:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 *) Definition use_id_type (T : Type) (x : IdType_t T) : result T := Ok x. (** [no_nested_borrows::create_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 492:0-492:43 *) + Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 *) Definition create_id_type (T : Type) (x : T) : result (IdType_t T) := Ok x. diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 308de4f4..bffb6699 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -3,16 +3,16 @@ -arg -w -arg all -External_FunsExternal_Template.v -Loops.v -External_Types.v +Bitwise.v +Constants.v +External_Funs.v +External_FunsExternal.v +External_FunsExternal_Template.v +External_Types.v +External_TypesExternal.v +External_TypesExternal_Template.v +Loops.v +NoNestedBorrows.v +Paper.v +PoloniusList.v Primitives.v -External_Funs.v -External_TypesExternal.v -Constants.v -PoloniusList.v -NoNestedBorrows.v -External_FunsExternal.v -Bitwise.v -External_TypesExternal_Template.v -Paper.v diff --git a/tests/coq/traits/_CoqProject b/tests/coq/traits/_CoqProject index 5b6199fc..14a91aa8 100644 --- a/tests/coq/traits/_CoqProject +++ b/tests/coq/traits/_CoqProject @@ -3,5 +3,5 @@ -arg -w -arg all +Primitives.v Traits.v -Primitives.v diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index 7e333b56..7506a13b 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -211,20 +211,25 @@ let _ = assert_norm (choose_test = Ok ()) let test_char : result char = Ok 'a' +(** [no_nested_borrows::panic_mut_borrow]: + Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:36 *) +let panic_mut_borrow (i : u32) : result u32 = + Fail Failure + (** [no_nested_borrows::Tree] - Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:16 *) + Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:16 *) type tree_t (t : Type0) = | Tree_Leaf : t -> tree_t t | Tree_Node : t -> nodeElem_t t -> tree_t t -> tree_t t (** [no_nested_borrows::NodeElem] - Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:20 *) + Source: 'tests/src/no_nested_borrows.rs', lines 230:0-230:20 *) and nodeElem_t (t : Type0) = | NodeElem_Cons : tree_t t -> nodeElem_t t -> nodeElem_t t | NodeElem_Nil : nodeElem_t t (** [no_nested_borrows::list_length]: - Source: 'tests/src/no_nested_borrows.rs', lines 260:0-260:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 265:0-265:48 *) let rec list_length (t : Type0) (l : list_t t) : result u32 = begin match l with | List_Cons _ l1 -> let* i = list_length t l1 in u32_add 1 i @@ -232,7 +237,7 @@ let rec list_length (t : Type0) (l : list_t t) : result u32 = end (** [no_nested_borrows::list_nth_shared]: - Source: 'tests/src/no_nested_borrows.rs', lines 268:0-268:62 *) + Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 *) let rec list_nth_shared (t : Type0) (l : list_t t) (i : u32) : result t = begin match l with | List_Cons x tl -> @@ -241,7 +246,7 @@ let rec list_nth_shared (t : Type0) (l : list_t t) (i : u32) : result t = end (** [no_nested_borrows::list_nth_mut]: - Source: 'tests/src/no_nested_borrows.rs', lines 284:0-284:67 *) + Source: 'tests/src/no_nested_borrows.rs', lines 289:0-289:67 *) let rec list_nth_mut (t : Type0) (l : list_t t) (i : u32) : result (t & (t -> result (list_t t))) @@ -260,7 +265,7 @@ let rec list_nth_mut end (** [no_nested_borrows::list_rev_aux]: - Source: 'tests/src/no_nested_borrows.rs', lines 300:0-300:63 *) + Source: 'tests/src/no_nested_borrows.rs', lines 305:0-305:63 *) let rec list_rev_aux (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) = begin match li with @@ -269,13 +274,13 @@ let rec list_rev_aux end (** [no_nested_borrows::list_rev]: - Source: 'tests/src/no_nested_borrows.rs', lines 314:0-314:42 *) + Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 *) let list_rev (t : Type0) (l : list_t t) : result (list_t t) = let (li, _) = core_mem_replace (list_t t) l List_Nil in list_rev_aux t li List_Nil (** [no_nested_borrows::test_list_functions]: - Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:28 *) + Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 *) let test_list_functions : result unit = let l = List_Cons 2 List_Nil in let l1 = List_Cons 1 l in @@ -312,7 +317,7 @@ let test_list_functions : result unit = let _ = assert_norm (test_list_functions = Ok ()) (** [no_nested_borrows::id_mut_pair1]: - Source: 'tests/src/no_nested_borrows.rs', lines 335:0-335:89 *) + Source: 'tests/src/no_nested_borrows.rs', lines 340:0-340:89 *) let id_mut_pair1 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) @@ -320,7 +325,7 @@ let id_mut_pair1 Ok ((x, y), Ok) (** [no_nested_borrows::id_mut_pair2]: - Source: 'tests/src/no_nested_borrows.rs', lines 339:0-339:88 *) + Source: 'tests/src/no_nested_borrows.rs', lines 344:0-344:88 *) let id_mut_pair2 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) @@ -328,7 +333,7 @@ let id_mut_pair2 let (x, x1) = p in Ok ((x, x1), Ok) (** [no_nested_borrows::id_mut_pair3]: - Source: 'tests/src/no_nested_borrows.rs', lines 343:0-343:93 *) + Source: 'tests/src/no_nested_borrows.rs', lines 348:0-348:93 *) let id_mut_pair3 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2)) @@ -336,7 +341,7 @@ let id_mut_pair3 Ok ((x, y), Ok, Ok) (** [no_nested_borrows::id_mut_pair4]: - Source: 'tests/src/no_nested_borrows.rs', lines 347:0-347:92 *) + Source: 'tests/src/no_nested_borrows.rs', lines 352:0-352:92 *) let id_mut_pair4 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2)) @@ -344,35 +349,35 @@ let id_mut_pair4 let (x, x1) = p in Ok ((x, x1), Ok, Ok) (** [no_nested_borrows::StructWithTuple] - Source: 'tests/src/no_nested_borrows.rs', lines 354:0-354:34 *) + Source: 'tests/src/no_nested_borrows.rs', lines 359:0-359:34 *) type structWithTuple_t (t1 t2 : Type0) = { p : (t1 & t2); } (** [no_nested_borrows::new_tuple1]: - Source: 'tests/src/no_nested_borrows.rs', lines 358:0-358:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 *) let new_tuple1 : result (structWithTuple_t u32 u32) = Ok { p = (1, 2) } (** [no_nested_borrows::new_tuple2]: - Source: 'tests/src/no_nested_borrows.rs', lines 362:0-362:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 *) let new_tuple2 : result (structWithTuple_t i16 i16) = Ok { p = (1, 2) } (** [no_nested_borrows::new_tuple3]: - Source: 'tests/src/no_nested_borrows.rs', lines 366:0-366:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 *) let new_tuple3 : result (structWithTuple_t u64 i64) = Ok { p = (1, 2) } (** [no_nested_borrows::StructWithPair] - Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:33 *) + Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 *) type structWithPair_t (t1 t2 : Type0) = { p : pair_t t1 t2; } (** [no_nested_borrows::new_pair1]: - Source: 'tests/src/no_nested_borrows.rs', lines 375:0-375:46 *) + Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 *) let new_pair1 : result (structWithPair_t u32 u32) = Ok { p = { x = 1; y = 2 } } (** [no_nested_borrows::test_constants]: - Source: 'tests/src/no_nested_borrows.rs', lines 383:0-383:23 *) + Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 *) let test_constants : result unit = let* swt = new_tuple1 in let (i, _) = swt.p in @@ -396,7 +401,7 @@ let test_constants : result unit = let _ = assert_norm (test_constants = Ok ()) (** [no_nested_borrows::test_weird_borrows1]: - Source: 'tests/src/no_nested_borrows.rs', lines 392:0-392:28 *) + Source: 'tests/src/no_nested_borrows.rs', lines 397:0-397:28 *) let test_weird_borrows1 : result unit = Ok () @@ -404,71 +409,71 @@ let test_weird_borrows1 : result unit = let _ = assert_norm (test_weird_borrows1 = Ok ()) (** [no_nested_borrows::test_mem_replace]: - Source: 'tests/src/no_nested_borrows.rs', lines 402:0-402:37 *) + Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 *) let test_mem_replace (px : u32) : result u32 = let (y, _) = core_mem_replace u32 px 1 in if not (y = 0) then Fail Failure else Ok 2 (** [no_nested_borrows::test_shared_borrow_bool1]: - Source: 'tests/src/no_nested_borrows.rs', lines 409:0-409:47 *) + Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 *) let test_shared_borrow_bool1 (b : bool) : result u32 = if b then Ok 0 else Ok 1 (** [no_nested_borrows::test_shared_borrow_bool2]: - Source: 'tests/src/no_nested_borrows.rs', lines 422:0-422:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 *) let test_shared_borrow_bool2 : result u32 = Ok 0 (** [no_nested_borrows::test_shared_borrow_enum1]: - Source: 'tests/src/no_nested_borrows.rs', lines 437:0-437:52 *) + Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 *) let test_shared_borrow_enum1 (l : list_t u32) : result u32 = begin match l with | List_Cons _ _ -> Ok 1 | List_Nil -> Ok 0 end (** [no_nested_borrows::test_shared_borrow_enum2]: - Source: 'tests/src/no_nested_borrows.rs', lines 449:0-449:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 *) let test_shared_borrow_enum2 : result u32 = Ok 0 (** [no_nested_borrows::incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 460:0-460:24 *) + Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 *) let incr (x : u32) : result u32 = u32_add x 1 (** [no_nested_borrows::call_incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 464:0-464:35 *) + Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 *) let call_incr (x : u32) : result u32 = incr x (** [no_nested_borrows::read_then_incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:41 *) + Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 *) let read_then_incr (x : u32) : result (u32 & u32) = let* x1 = u32_add x 1 in Ok (x, x1) (** [no_nested_borrows::Tuple] - Source: 'tests/src/no_nested_borrows.rs', lines 475:0-475:24 *) + Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 *) type tuple_t (t1 t2 : Type0) = t1 * t2 (** [no_nested_borrows::use_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 477:0-477:48 *) + Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 *) let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) = let (_, i) = x in Ok (1, i) (** [no_nested_borrows::create_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 481:0-481:61 *) + Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 *) let create_tuple_struct (x : u32) (y : u64) : result (tuple_t u32 u64) = Ok (x, y) (** [no_nested_borrows::IdType] - Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:20 *) + Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 *) type idType_t (t : Type0) = t (** [no_nested_borrows::use_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 488:0-488:40 *) + Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 *) let use_id_type (t : Type0) (x : idType_t t) : result t = Ok x (** [no_nested_borrows::create_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 492:0-492:43 *) + Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 *) let create_id_type (t : Type0) (x : t) : result (idType_t t) = Ok x diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 022b32fb..aa782009 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -258,16 +258,21 @@ def choose_test : Result Unit := def test_char : Result Char := Result.ok 'a' +/- [no_nested_borrows::panic_mut_borrow]: + Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:36 -/ +def panic_mut_borrow (i : U32) : Result U32 := + Result.fail .panic + mutual /- [no_nested_borrows::Tree] - Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:16 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:16 -/ inductive Tree (T : Type) := | Leaf : T → Tree T | Node : T → NodeElem T → Tree T → Tree T /- [no_nested_borrows::NodeElem] - Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:20 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 230:0-230:20 -/ inductive NodeElem (T : Type) := | Cons : Tree T → NodeElem T → NodeElem T | Nil : NodeElem T @@ -275,7 +280,7 @@ inductive NodeElem (T : Type) := end /- [no_nested_borrows::list_length]: - Source: 'tests/src/no_nested_borrows.rs', lines 260:0-260:48 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 265:0-265:48 -/ divergent def list_length (T : Type) (l : List T) : Result U32 := match l with | List.Cons _ l1 => do @@ -284,7 +289,7 @@ divergent def list_length (T : Type) (l : List T) : Result U32 := | List.Nil => Result.ok 0#u32 /- [no_nested_borrows::list_nth_shared]: - Source: 'tests/src/no_nested_borrows.rs', lines 268:0-268:62 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 -/ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := match l with | List.Cons x tl => @@ -296,7 +301,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := | List.Nil => Result.fail .panic /- [no_nested_borrows::list_nth_mut]: - Source: 'tests/src/no_nested_borrows.rs', lines 284:0-284:67 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 289:0-289:67 -/ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with @@ -318,7 +323,7 @@ divergent def list_nth_mut | List.Nil => Result.fail .panic /- [no_nested_borrows::list_rev_aux]: - Source: 'tests/src/no_nested_borrows.rs', lines 300:0-300:63 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 305:0-305:63 -/ divergent def list_rev_aux (T : Type) (li : List T) (lo : List T) : Result (List T) := match li with @@ -326,13 +331,13 @@ divergent def list_rev_aux | List.Nil => Result.ok lo /- [no_nested_borrows::list_rev]: - Source: 'tests/src/no_nested_borrows.rs', lines 314:0-314:42 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 -/ def list_rev (T : Type) (l : List T) : Result (List T) := let (li, _) := core.mem.replace (List T) l List.Nil list_rev_aux T li List.Nil /- [no_nested_borrows::test_list_functions]: - Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:28 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 -/ def test_list_functions : Result Unit := do let l := List.Cons 2#i32 List.Nil @@ -379,7 +384,7 @@ def test_list_functions : Result Unit := #assert (test_list_functions == Result.ok ()) /- [no_nested_borrows::id_mut_pair1]: - Source: 'tests/src/no_nested_borrows.rs', lines 335:0-335:89 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 340:0-340:89 -/ def id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) @@ -387,7 +392,7 @@ def id_mut_pair1 Result.ok ((x, y), Result.ok) /- [no_nested_borrows::id_mut_pair2]: - Source: 'tests/src/no_nested_borrows.rs', lines 339:0-339:88 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 344:0-344:88 -/ def id_mut_pair2 (T1 T2 : Type) (p : (T1 × T2)) : Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2))) @@ -396,7 +401,7 @@ def id_mut_pair2 Result.ok ((t, t1), Result.ok) /- [no_nested_borrows::id_mut_pair3]: - Source: 'tests/src/no_nested_borrows.rs', lines 343:0-343:93 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 348:0-348:93 -/ def id_mut_pair3 (T1 T2 : Type) (x : T1) (y : T2) : Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2)) @@ -404,7 +409,7 @@ def id_mut_pair3 Result.ok ((x, y), Result.ok, Result.ok) /- [no_nested_borrows::id_mut_pair4]: - Source: 'tests/src/no_nested_borrows.rs', lines 347:0-347:92 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 352:0-352:92 -/ def id_mut_pair4 (T1 T2 : Type) (p : (T1 × T2)) : Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2)) @@ -413,37 +418,37 @@ def id_mut_pair4 Result.ok ((t, t1), Result.ok, Result.ok) /- [no_nested_borrows::StructWithTuple] - Source: 'tests/src/no_nested_borrows.rs', lines 354:0-354:34 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 359:0-359:34 -/ structure StructWithTuple (T1 T2 : Type) where p : (T1 × T2) /- [no_nested_borrows::new_tuple1]: - Source: 'tests/src/no_nested_borrows.rs', lines 358:0-358:48 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/ def new_tuple1 : Result (StructWithTuple U32 U32) := Result.ok { p := (1#u32, 2#u32) } /- [no_nested_borrows::new_tuple2]: - Source: 'tests/src/no_nested_borrows.rs', lines 362:0-362:48 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 -/ def new_tuple2 : Result (StructWithTuple I16 I16) := Result.ok { p := (1#i16, 2#i16) } /- [no_nested_borrows::new_tuple3]: - Source: 'tests/src/no_nested_borrows.rs', lines 366:0-366:48 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 -/ def new_tuple3 : Result (StructWithTuple U64 I64) := Result.ok { p := (1#u64, 2#i64) } /- [no_nested_borrows::StructWithPair] - Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:33 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 -/ structure StructWithPair (T1 T2 : Type) where p : Pair T1 T2 /- [no_nested_borrows::new_pair1]: - Source: 'tests/src/no_nested_borrows.rs', lines 375:0-375:46 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 -/ def new_pair1 : Result (StructWithPair U32 U32) := Result.ok { p := { x := 1#u32, y := 2#u32 } } /- [no_nested_borrows::test_constants]: - Source: 'tests/src/no_nested_borrows.rs', lines 383:0-383:23 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 -/ def test_constants : Result Unit := do let swt ← new_tuple1 @@ -473,7 +478,7 @@ def test_constants : Result Unit := #assert (test_constants == Result.ok ()) /- [no_nested_borrows::test_weird_borrows1]: - Source: 'tests/src/no_nested_borrows.rs', lines 392:0-392:28 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 397:0-397:28 -/ def test_weird_borrows1 : Result Unit := Result.ok () @@ -481,7 +486,7 @@ def test_weird_borrows1 : Result Unit := #assert (test_weird_borrows1 == Result.ok ()) /- [no_nested_borrows::test_mem_replace]: - Source: 'tests/src/no_nested_borrows.rs', lines 402:0-402:37 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 -/ def test_mem_replace (px : U32) : Result U32 := let (y, _) := core.mem.replace U32 px 1#u32 if ¬ (y = 0#u32) @@ -489,71 +494,71 @@ def test_mem_replace (px : U32) : Result U32 := else Result.ok 2#u32 /- [no_nested_borrows::test_shared_borrow_bool1]: - Source: 'tests/src/no_nested_borrows.rs', lines 409:0-409:47 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 -/ def test_shared_borrow_bool1 (b : Bool) : Result U32 := if b then Result.ok 0#u32 else Result.ok 1#u32 /- [no_nested_borrows::test_shared_borrow_bool2]: - Source: 'tests/src/no_nested_borrows.rs', lines 422:0-422:40 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 -/ def test_shared_borrow_bool2 : Result U32 := Result.ok 0#u32 /- [no_nested_borrows::test_shared_borrow_enum1]: - Source: 'tests/src/no_nested_borrows.rs', lines 437:0-437:52 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 -/ def test_shared_borrow_enum1 (l : List U32) : Result U32 := match l with | List.Cons _ _ => Result.ok 1#u32 | List.Nil => Result.ok 0#u32 /- [no_nested_borrows::test_shared_borrow_enum2]: - Source: 'tests/src/no_nested_borrows.rs', lines 449:0-449:40 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 -/ def test_shared_borrow_enum2 : Result U32 := Result.ok 0#u32 /- [no_nested_borrows::incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 460:0-460:24 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/ def incr (x : U32) : Result U32 := x + 1#u32 /- [no_nested_borrows::call_incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 464:0-464:35 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 -/ def call_incr (x : U32) : Result U32 := incr x /- [no_nested_borrows::read_then_incr]: - Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:41 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 -/ def read_then_incr (x : U32) : Result (U32 × U32) := do let x1 ← x + 1#u32 Result.ok (x, x1) /- [no_nested_borrows::Tuple] - Source: 'tests/src/no_nested_borrows.rs', lines 475:0-475:24 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 -/ def Tuple (T1 T2 : Type) := T1 × T2 /- [no_nested_borrows::use_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 477:0-477:48 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 -/ def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) := Result.ok (1#u32, x.#1) /- [no_nested_borrows::create_tuple_struct]: - Source: 'tests/src/no_nested_borrows.rs', lines 481:0-481:61 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 -/ def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) := Result.ok (x, y) /- [no_nested_borrows::IdType] - Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:20 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 -/ @[reducible] def IdType (T : Type) := T /- [no_nested_borrows::use_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 488:0-488:40 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 -/ def use_id_type (T : Type) (x : IdType T) : Result T := Result.ok x /- [no_nested_borrows::create_id_type]: - Source: 'tests/src/no_nested_borrows.rs', lines 492:0-492:43 -/ + Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 -/ def create_id_type (T : Type) (x : T) : Result (IdType T) := Result.ok x diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index a250748c..6d3074ef 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -216,6 +216,11 @@ pub fn test_char() -> char { 'a' } +/// This triggered a bug at some point +pub fn panic_mut_borrow(_: &mut u32) { + panic!() +} + /// Mutually recursive types pub enum Tree<T> { Leaf(T), @@ -228,7 +233,7 @@ pub enum NodeElem<T> { } /* -// TODO: those definitions requires semantic termination (breaks the Coq backend +// TODO: those definitions require semantic termination (breaks the Coq backend // because we don't use fuel in this case). /// Mutually recursive functions |