Update the invariant checks to take into account ignored borrows/loans

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