diff options
Diffstat (limited to 'src/Invariants.ml')
| -rw-r--r-- | src/Invariants.ml | 39 |
1 files changed, 33 insertions, 6 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index be5f3ed3..3fc390b5 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -78,9 +78,18 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = ^ "\n- info:\n" ^ borrows_infos_to_string " " !borrows_infos in + (* Ignored loans - when we find an ignored loan while building the borrows_infos + * map, we register it in this list; once the borrows_infos map is completely + * built, we check that all the borrow ids of the ignored loans are in this + * map *) + let ignored_loans : (T.ref_kind * V.BorrowId.id) list ref = ref [] in (* first, register all the loans *) (* Some utilities to register the loans *) + let register_ignored_loan (rkind : T.ref_kind) (bid : V.BorrowId.id) : unit = + ignored_loans := (rkind, bid) :: !ignored_loans + in + let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.set_t) : unit = let reprs = !ids_reprs in @@ -161,11 +170,11 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match lc with | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids + | V.AIgnoredMutLoan (bid, _) -> register_ignored_loan T.Mut bid + | V.AIgnoredSharedLoan _ | V.AEndedMutLoan { given_back = _; child = _ } | V.AEndedSharedLoan (_, _) - | V.AIgnoredMutLoan (_, _) (* We might want to do something here *) - | V.AEndedIgnoredMutLoan { given_back = _; child = _ } - | V.AIgnoredSharedLoan _ -> + | V.AEndedIgnoredMutLoan { given_back = _; child = _ } -> (* Do nothing *) () in @@ -208,6 +217,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = borrows_infos := infos in + let register_ignored_borrow = register_ignored_loan in + let register_borrow (kind : borrow_kind) (bid : V.BorrowId.id) : unit = (* Lookup the info *) let info = find_info bid in @@ -253,8 +264,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match bc with | V.AMutBorrow (bid, _) -> register_borrow Mut bid | V.ASharedBorrow bid -> register_borrow Shared bid - | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _ - | V.AProjSharedBorrow _ -> + | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid + | V.AIgnoredMutBorrow (None, _) + | V.AEndedIgnoredMutBorrow _ | V.AProjSharedBorrow _ -> (* Do nothing *) () in @@ -271,6 +283,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = (lazy ("\nAbout to check context invariant:\n" ^ context_to_string ())); (* Finally, check that everything is consistant *) + (* First, check all the ignored loans are present at the proper place *) + List.iter + (fun (rkind, bid) -> + let info = find_info bid in + assert (info.loan_kind = rkind)) + !ignored_loans; + + (* Then, check the borrow infos *) V.BorrowId.Map.iter (fun _ info -> (* Note that we can't directly compare the sets - I guess they are @@ -466,6 +486,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv + (* TODO: there is a lot of duplication with [visit_typed_value] + * which is quite annoying. There might be a way of factorizing + * that by factorizing the definitions of value and avalue, but + * the generation of visitors then doesn't work properly (TODO: + * report that). Still, it is actually not that problematic + * because this code shouldn't change a lot in the future, + * so the cost of maintenance should be pretty low. + * *) method! visit_typed_avalue info atv = (* Check the current pair (value, type) *) (match (atv.V.value, atv.V.ty) with @@ -576,7 +604,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | _ -> failwith "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv - (** TODO: there is a lot of duplication with [visit_typed_value]... *) end in visitor#visit_eval_ctx () ctx |