summaryrefslogtreecommitdiff
path: root/compiler/Invariants.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Invariants.ml')
-rw-r--r--compiler/Invariants.ml49
1 files changed, 31 insertions, 18 deletions
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