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