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