Add invariant checks at the end of [end_borrow] and [end_abstraction]

2 files changed, 14 insertions, 6 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 477cba9b..8aafff30 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -838,6 +838,11 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
         failwith "Loan not eliminated"
   in
   let cf_check_disappeared : cm_fun = unit_to_cm_fun check_disappeared in
+  (* The complete sanity check: also check that after we ended a borrow,
+   * the invariant is preserved *)
+  let cf_check : cm_fun =
+    comp cf_check_disappeared (Invariants.cf_check_invariants config)
+  in
 
   (* Start by getting the borrow *)
   match end_borrow_get_borrow allowed_abs l ctx with
@@ -866,7 +871,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
           (* Retry to end the borrow *)
           let cc = comp cc (end_borrow config chain0 allowed_abs l) in
           (* Check and apply *)
-          comp cc cf_check_disappeared cf ctx
+          comp cc cf_check cf ctx
       | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
           let allowed_abs' = None in
           (* End the outer borrow *)
@@ -874,7 +879,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
           (* Retry to end the borrow *)
           let cc = comp cc (end_borrow config chain0 allowed_abs l) in
           (* Check and apply *)
-          comp cc cf_check_disappeared cf ctx
+          comp cc cf_check cf ctx
       | OuterAbs abs_id ->
           (* The borrow is inside an asbtraction: check if the corresponding
            * loan is inside the same abstraction. If this is the case, we end
@@ -905,14 +910,14 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
                 end_abstraction config chain abs_id
           in
           (* Compose with a sanity check *)
-          comp cf_end_abs cf_check_disappeared cf ctx)
+          comp cf_end_abs cf_check cf ctx)
   | Ok (ctx, None) ->
       log#ldebug (lazy "End borrow: borrow not found");
       (* It is possible that we can't find a borrow in symbolic mode (ending
        * an abstraction may end several borrows at once *)
       assert (config.mode = SymbolicMode);
       (* Do a sanity check and continue *)
-      cf_check_disappeared cf ctx
+      cf_check cf ctx
   (* We found a borrow: give it back (i.e., update the corresponding loan) *)
   | Ok (ctx, Some bc) ->
       (* Sanity check: the borrowed value shouldn't contain loans *)
@@ -923,7 +928,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
       (* Give back the value *)
       let ctx = give_back config l bc ctx in
       (* Do a sanity check and continue *)
-      cf_check_disappeared cf ctx
+      cf_check cf ctx
 
 and end_borrows (config : C.config) (chain : borrow_or_abs_ids)
     (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) : cm_fun
@@ -1005,6 +1010,9 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
   in
 
+  (* Sanity check: ending an abstraction must preserve the invariants *)
+  let cc = comp cc (Invariants.cf_check_invariants config) in
+
   (* Apply the continuation *)
   cc cf ctx
 
diff --git a/src/main.ml b/src/main.ml
index 54536503..062a1bd0 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -53,7 +53,7 @@ let () =
   expressions_log#set_level EL.Debug;
   expansion_log#set_level EL.Debug;
   borrows_log#set_level EL.Debug;
-  invariants_log#set_level EL.Debug;
+  invariants_log#set_level EL.Warning;
   (* Load the module *)
   let json = Yojson.Basic.from_file !filename in
   match cfim_module_of_json json with