From a64fdc8b1be70de43afe35ff788ba3240318daac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 15:02:17 +0100
Subject: WIP Beginning working on better errors: began replacing raise
 (Failure) and assert by craise and cassert. Does not compile yet, still need
 to propagate the meta variable where it's relevant

---
 compiler/InterpreterBorrows.ml | 487 +++++++++++++++++++++--------------------
 1 file changed, 244 insertions(+), 243 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 17810705..ae251fbf 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -7,6 +7,7 @@ open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
 open InterpreterProjectors
+open Errors
 
 (** The local logger *)
 let log = Logging.borrows_log
@@ -29,7 +30,7 @@ let log = Logging.borrows_log
       loans. This is used to merge borrows with abstractions, to compute loop
       fixed points for instance.
 *)
-let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
+let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id option)
     (allow_inner_loans : bool) (l : BorrowId.id) (ctx : eval_ctx) :
     ( eval_ctx * (AbstractionId.id option * g_borrow_content) option,
       priority_borrows_or_abs )
@@ -41,7 +42,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
   in
   let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content)
       =
-    assert (Option.is_none !replaced_bc);
+    cassert (Option.is_none !replaced_bc) meta "TODO: error message";
     replaced_bc := Some (abs_id, bc)
   in
   (* Raise an exception if:
@@ -180,7 +181,7 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
                * Also note that, as we are moving the borrowed value inside the
                * abstraction (and not really giving the value back to the context)
                * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *)
-              raise (Failure "Unimplemented")
+              craise meta "Unimplemented"
               (* ABottom *))
             else
               (* Update the outer borrows before diving into the child avalue *)
@@ -223,8 +224,8 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
       method! visit_abs outer abs =
         (* Update the outer abs *)
         let outer_abs, outer_borrows = outer in
-        assert (Option.is_none outer_abs);
-        assert (Option.is_none outer_borrows);
+        cassert (Option.is_none outer_abs) meta "TODO: error message";
+        cassert (Option.is_none outer_borrows) meta "TODO: error message";
         let outer = (Some abs.abs_id, None) in
         super#visit_abs outer abs
     end
@@ -244,11 +245,11 @@ let end_borrow_get_borrow (allowed_abs : AbstractionId.id option)
     give the value back.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
+let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv : typed_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
-  assert (not (loans_in_value nv));
-  assert (not (bottom_in_value ctx.ended_regions nv));
+  cassert (not (loans_in_value nv)) meta "TODO: error message";
+  cassert (not (bottom_in_value ctx.ended_regions nv)) meta "TODO: error message";
   (* Debug *)
   log#ldebug
     (lazy
@@ -258,7 +259,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    assert (not !replaced);
+    cassert (not !replaced) meta "Exactly one loan should have been updated";
     replaced := true
   in
   (* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
@@ -300,7 +301,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
                   ("give_back_value: improper type:\n- expected: "
                  ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                raise (Failure "Value given back doesn't have the proper type"));
+                craise meta "Value given back doesn't have the proper type");
               (* Replace *)
               set_replaced ();
               nv.value)
@@ -345,7 +346,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
                   ABorrow
                     (AEndedIgnoredMutBorrow
                        { given_back; child; given_back_meta })
-              | _ -> raise (Failure "Unreachable")
+              | _ -> craise meta "Unreachable"
             else
               (* Continue exploring *)
               ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child)
@@ -360,7 +361,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
         (* Preparing a bit *)
         let regions, ancestors_regions =
           match opt_abs with
-          | None -> raise (Failure "Unreachable")
+          | None -> craise meta "Unreachable"
           | Some abs -> (abs.regions, abs.ancestors_regions)
         in
         (* Rk.: there is a small issue with the types of the aloan values.
@@ -426,7 +427,7 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
         (* We remember in which abstraction we are before diving -
          * this is necessary for projecting values: we need to know
          * over which regions to project *)
-        assert (Option.is_none opt_abs);
+        cassert (Option.is_none opt_abs) meta "TODO: error message";
         super#visit_EAbs (Some abs) abs
     end
   in
@@ -434,16 +435,16 @@ let give_back_value (config : config) (bid : BorrowId.id) (nv : typed_value)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  assert !replaced;
+  cassert !replaced meta "Only one loan should have been given back";
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
 (** Give back a *modified* symbolic value. *)
-let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
+let give_back_symbolic_value (meta : Meta.meta) (_config : config) (proj_regions : RegionId.Set.t)
     (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
-  assert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty);
+  cassert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta "TODO: error message";
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -465,11 +466,11 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
          type [T]! We thus *mustn't* introduce a projector here.
       *)
       (* AProjBorrows (nsv, sv.sv_ty) *)
-      raise (Failure "TODO")
+      craise meta "TODO: error message"
     in
     AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
-  update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
+  update_intersecting_aproj_loans meta proj_regions proj_ty sv subst ctx
 
 (** Auxiliary function to end borrows. See {!give_back}.
 
@@ -484,12 +485,12 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
     end abstraction when ending this abstraction. When doing this, we need
     to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values.
  *)
-let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
+let give_back_avalue_to_same_abstraction (meta : Meta.meta) (_config : config) (bid : BorrowId.id)
     (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    assert (not !replaced);
+    cassert (not !replaced) meta "Only one loan should have been updated";
     replaced := true
   in
   let obj =
@@ -532,7 +533,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
                   ("give_back_avalue_to_same_abstraction: improper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                raise (Failure "Value given back doesn't have the proper type"));
+                craise meta "Value given back doesn't have the proper type");
               (* This is the loan we are looking for: apply the projection to
                * the value we give back and replaced this mutable loan with
                * an ended loan *)
@@ -558,7 +559,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
                * we don't register the fact that we inserted the value somewhere
                * (i.e., we don't call {!set_replaced}) *)
               (* Sanity check *)
-              assert (nv.ty = ty);
+              cassert (nv.ty = ty) meta "TODO: error message";
               ALoan
                 (AEndedIgnoredMutLoan
                    { given_back = nv; child; given_back_meta = nsv }))
@@ -574,7 +575,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  assert !replaced;
+  cassert !replaced meta "Only one loan should be given back";
   (* Return *)
   ctx
 
@@ -587,11 +588,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (bid : BorrowId.id)
     we update.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
+let give_back_shared (meta : Meta.meta) _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    assert (not !replaced);
+    cassert (not !replaced) meta "Only one loan should be updated";
     replaced := true
   in
   let obj =
@@ -656,7 +657,7 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  assert !replaced;
+  cassert !replaced meta "Exactly one loan should be given back";
   (* Return *)
   ctx
 
@@ -665,12 +666,12 @@ let give_back_shared _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
     to an environment by inserting a new borrow id in the set of borrows tracked
     by a shared value, referenced by the [original_bid] argument.
  *)
-let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id)
+let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : BorrowId.id)
     (ctx : eval_ctx) : eval_ctx =
   (* Keep track of changes *)
   let r = ref false in
   let set_ref () =
-    assert (not !r);
+    cassert (not !r) meta "TODO: error message";
     r := true
   in
 
@@ -700,7 +701,7 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id)
 
   let env = obj#visit_env () ctx.env in
   (* Check that we reborrowed once *)
-  assert !r;
+  cassert !r meta "Not reborrowed once";
   { ctx with env }
 
 (** Convert an {!type:avalue} to a {!type:value}.
@@ -738,7 +739,7 @@ let convert_avalue_to_given_back_value (av : typed_avalue) : symbolic_value =
     borrows. This kind of internal reshuffling. should be similar to ending
     abstractions (it is tantamount to ending *sub*-abstractions).
  *)
-let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content)
+let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_borrow_content)
     (ctx : eval_ctx) : eval_ctx =
   (* Debug *)
   log#ldebug
@@ -757,24 +758,24 @@ let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content)
   match bc with
   | Concrete (VMutBorrow (l', tv)) ->
       (* Sanity check *)
-      assert (l' = l);
-      assert (not (loans_in_value tv));
+      cassert (l' = l) meta "TODO: error message";
+      cassert (not (loans_in_value tv)) meta "TODO: error message";
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
       (* Update the context *)
-      give_back_value config l tv ctx
+      give_back_value meta config l tv ctx
   | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
       (* Sanity check *)
-      assert (l' = l);
+      cassert (l' = l) meta "TODO: error message";
       (* Check that the borrow is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
       (* Update the context *)
-      give_back_shared config l ctx
+      give_back_shared meta config l ctx
   | Abstract (AMutBorrow (l', av)) ->
       (* Sanity check *)
-      assert (l' = l);
+      cassert (l' = l) meta "TODO: error message";
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
       (* Convert the avalue to a (fresh symbolic) value.
 
          Rem.: we shouldn't do this here. We should do this in a function
@@ -782,27 +783,27 @@ let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content)
       *)
       let sv = convert_avalue_to_given_back_value av in
       (* Update the context *)
-      give_back_avalue_to_same_abstraction config l av
+      give_back_avalue_to_same_abstraction meta config l av
         (mk_typed_value_from_symbolic_value sv)
         ctx
   | Abstract (ASharedBorrow l') ->
       (* Sanity check *)
-      assert (l' = l);
+      cassert (l' = l) meta "TODO: error message";
       (* Check that the borrow is somewhere - purely a sanity check *)
-      assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
+      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
       (* Update the context *)
-      give_back_shared config l ctx
+      give_back_shared meta config l ctx
   | Abstract (AProjSharedBorrow asb) ->
       (* Sanity check *)
-      assert (borrow_in_asb l asb);
+      cassert (borrow_in_asb l asb) meta "TODO: error message";
       (* Update the context *)
-      give_back_shared config l ctx
+      give_back_shared meta config l ctx
   | Abstract
       ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
       | AEndedSharedBorrow ) ->
-      raise (Failure "Unreachable")
+      craise meta "Unreachable"
 
-let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
+let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowId.id)
     (ctx0 : eval_ctx) : cm_fun =
   let check_disappeared (ctx : eval_ctx) : unit =
     let _ =
@@ -815,9 +816,9 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
              ^ ": borrow didn't disappear:\n- original context:\n"
              ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
              ^ eval_ctx_to_string ctx));
-          raise (Failure "Borrow not eliminated")
+          craise meta "Borrow not eliminated"
     in
-    match lookup_loan_opt ek_all l ctx with
+    match lookup_loan_opt meta ek_all l ctx with
     | None -> () (* Ok *)
     | Some _ ->
         log#lerror
@@ -826,7 +827,7 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
            ^ ": loan didn't disappear:\n- original context:\n"
            ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
            ^ eval_ctx_to_string ctx));
-        raise (Failure "Loan not eliminated")
+        craise meta "Loan not eliminated"
   in
   unit_to_cm_fun check_disappeared
 
@@ -851,7 +852,7 @@ let check_borrow_disappeared (fun_name : string) (l : BorrowId.id)
     perform anything smart and is trusted, and another function for the
     book-keeping.
  *)
-let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
+let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
     (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
@@ -867,10 +868,10 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
   (* Utility function for the sanity checks: check that the borrow disappeared
    * from the context *)
   let ctx0 = ctx in
-  let cf_check : cm_fun = check_borrow_disappeared "end borrow" l ctx0 in
+  let cf_check : cm_fun = check_borrow_disappeared meta "end borrow" l ctx0 in
   (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *)
   let allow_inner_loans = false in
-  match end_borrow_get_borrow allowed_abs allow_inner_loans l ctx with
+  match end_borrow_get_borrow meta allowed_abs allow_inner_loans l ctx with
   (* Two cases:
      - error: we found outer borrows (the borrow is inside a borrowed value) or
        inner loans (the borrow contains loans)
@@ -899,29 +900,29 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
            * inside another borrow *)
           let allowed_abs' = None in
           (* End the outer borrows *)
-          let cc = end_borrows_aux config chain allowed_abs' bids in
+          let cc = end_borrows_aux meta config chain allowed_abs' bids in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
           let allowed_abs' = None in
           (* End the outer borrow *)
-          let cc = end_borrow_aux config chain allowed_abs' bid in
+          let cc = end_borrow_aux meta config chain allowed_abs' bid in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterAbs abs_id ->
           (* The borrow is inside an abstraction: end the whole abstraction *)
-          let cf_end_abs = end_abstraction_aux config chain abs_id in
+          let cf_end_abs = end_abstraction_aux meta config chain abs_id in
           (* Compose with a sanity check *)
           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);
+      cassert (config.mode = SymbolicMode) meta "Borrow should be in symbolic mode";
       (* Do a sanity check and continue *)
       cf_check cf ctx
   (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update
@@ -930,10 +931,10 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
       (* Sanity check: the borrowed value shouldn't contain loans *)
       (match bc with
       | Concrete (VMutBorrow (_, bv)) ->
-          assert (Option.is_none (get_first_loan_in_value bv))
+          cassert (Option.is_none (get_first_loan_in_value bv)) meta "Borrowed value shouldn't contain loans"
       | _ -> ());
       (* Give back the value *)
-      let ctx = give_back config l bc ctx in
+      let ctx = give_back meta config l bc ctx in
       (* Do a sanity check and continue *)
       let cc = cf_check in
       (* Save a snapshot of the environment for the name generation *)
@@ -941,7 +942,7 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids)
       (* Compose *)
       cc cf ctx
 
-and end_borrows_aux (config : config) (chain : borrow_or_abs_ids)
+and end_borrows_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
     (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the borrow ids,
@@ -949,10 +950,10 @@ and end_borrows_aux (config : config) (chain : borrow_or_abs_ids)
    * a matter of taste, and may make debugging easier *)
   let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
   List.fold_left
-    (fun cf id -> end_borrow_aux config chain allowed_abs id cf)
+    (fun cf id -> end_borrow_aux meta config chain allowed_abs id cf)
     cf ids
 
-and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
@@ -983,14 +984,14 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
       (* Check that we can end the abstraction *)
       if abs.can_end then ()
       else
-        raise
-          (Failure
+        craise
+          meta
              ("Can't end abstraction "
              ^ AbstractionId.to_string abs.abs_id
-             ^ " as it is set as non-endable"));
+             ^ " as it is set as non-endable");
 
       (* End the parent abstractions first *)
-      let cc = end_abstractions_aux config chain abs.parents in
+      let cc = end_abstractions_aux meta config chain abs.parents in
       let cc =
         comp_unit cc (fun ctx ->
             log#ldebug
@@ -1002,7 +1003,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
       in
 
       (* End the loans inside the abstraction *)
-      let cc = comp cc (end_abstraction_loans config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
       let cc =
         comp_unit cc (fun ctx ->
             log#ldebug
@@ -1013,7 +1014,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
       in
 
       (* End the abstraction itself by redistributing the borrows it contains *)
-      let cc = comp cc (end_abstraction_borrows config chain abs_id) in
+      let cc = comp cc (end_abstraction_borrows meta config chain abs_id) in
 
       (* End the regions owned by the abstraction - note that we don't need to
        * relookup the abstraction: the set of regions in an abstraction never
@@ -1043,7 +1044,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
       in
 
       (* Sanity check: ending an abstraction must preserve the invariants *)
-      let cc = comp cc Invariants.cf_check_invariants in
+      let cc = comp cc (Invariants.cf_check_invariants meta) in
 
       (* Save a snapshot of the environment for the name generation *)
       let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in
@@ -1051,7 +1052,7 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
       (* Apply the continuation *)
       cc cf ctx
 
-and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids)
+and end_abstractions_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
     (abs_ids : AbstractionId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the abstraction ids,
@@ -1059,10 +1060,10 @@ and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids)
    * a matter of taste, and may make debugging easier *)
   let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
   List.fold_left
-    (fun cf id -> end_abstraction_aux config chain id cf)
+    (fun cf id -> end_abstraction_aux meta config chain id cf)
     cf abs_ids
 
-and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_loans (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Lookup the abstraction *)
@@ -1071,7 +1072,7 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids)
    *
    * We ignore the "ignored mut/shared loans": as we should have already ended
    * the parent abstractions, they necessarily come from children. *)
-  let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in
+  let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in
   match opt_loan with
   | None ->
       (* No loans: nothing to update *)
@@ -1080,23 +1081,23 @@ and end_abstraction_loans (config : config) (chain : borrow_or_abs_ids)
       (* There are loans: end the corresponding borrows, then recheck *)
       let cc : cm_fun =
         match bids with
-        | Borrow bid -> end_borrow_aux config chain None bid
-        | Borrows bids -> end_borrows_aux config chain None bids
+        | Borrow bid -> end_borrow_aux meta config chain None bid
+        | Borrows bids -> end_borrows_aux meta config chain None bids
       in
       (* Reexplore, looking for loans *)
-      let cc = comp cc (end_abstraction_loans config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
       (* Continue *)
       cc cf ctx
   | Some (SymbolicValue sv) ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
        * which intersect this proj_loans, then end the proj_loans itself *)
-      let cc = end_proj_loans_symbolic config chain abs_id abs.regions sv in
+      let cc = end_proj_loans_symbolic meta config chain abs_id abs.regions sv in
       (* Reexplore, looking for loans *)
-      let cc = comp cc (end_abstraction_loans config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
       (* Continue *)
       cc cf ctx
 
-and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   log#ldebug
@@ -1147,7 +1148,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
 
       method! visit_aproj env sproj =
         (match sproj with
-        | AProjLoans _ -> raise (Failure "Unexpected")
+        | AProjLoans _ -> craise meta "Unexpected"
         | AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty))
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj env sproj
@@ -1156,7 +1157,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
       method! visit_borrow_content _ bc =
         match bc with
         | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc)
-        | VReservedMutBorrow _ -> raise (Failure "Unreachable")
+        | VReservedMutBorrow _ -> craise meta "Unreachable"
     end
   in
   (* Lookup the abstraction *)
@@ -1181,16 +1182,16 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
             (* Replace the mut borrow to register the fact that we ended
              * it and store with it the freshly generated given back value *)
             let ended_borrow = ABorrow (AEndedMutBorrow (sv, av)) in
-            let ctx = update_aborrow ek_all bid ended_borrow ctx in
+            let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
             (* Give the value back *)
             let sv = mk_typed_value_from_symbolic_value sv in
-            give_back_value config bid sv ctx
+            give_back_value meta config bid sv ctx
         | ASharedBorrow bid ->
             (* Replace the shared borrow to account for the fact it ended *)
             let ended_borrow = ABorrow AEndedSharedBorrow in
-            let ctx = update_aborrow ek_all bid ended_borrow ctx in
+            let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
             (* Give back *)
-            give_back_shared config bid ctx
+            give_back_shared meta config bid ctx
         | AProjSharedBorrow asb ->
             (* Retrieve the borrow ids *)
             let bids =
@@ -1205,21 +1206,21 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
              * can use to identify the whole set *)
             let repr_bid = List.hd bids in
             (* Replace the shared borrow with Bottom *)
-            let ctx = update_aborrow ek_all repr_bid ABottom ctx in
+            let ctx = update_aborrow meta ek_all repr_bid ABottom ctx in
             (* Give back the shared borrows *)
             let ctx =
               List.fold_left
-                (fun ctx bid -> give_back_shared config bid ctx)
+                (fun ctx bid -> give_back_shared meta config bid ctx)
                 ctx bids
             in
             (* Continue *)
             ctx
         | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
         | AEndedSharedBorrow ->
-            raise (Failure "Unexpected")
+            craise meta "Unexpected"
       in
       (* Reexplore *)
-      end_abstraction_borrows config chain abs_id cf ctx
+      end_abstraction_borrows meta config chain abs_id cf ctx
   (* There are symbolic borrows: end them, then reexplore *)
   | FoundAProjBorrows (sv, proj_ty) ->
       log#ldebug
@@ -1230,13 +1231,13 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
       let nsv = mk_fresh_symbolic_value proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
       let ended_borrow = AEndedProjBorrows nsv in
-      let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
+      let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
-        give_back_symbolic_value config abs.regions proj_ty sv nsv ctx
+        give_back_symbolic_value meta config abs.regions proj_ty sv nsv ctx
       in
       (* Reexplore *)
-      end_abstraction_borrows config chain abs_id cf ctx
+      end_abstraction_borrows meta config chain abs_id cf ctx
   (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
   | FoundBorrowContent bc ->
       log#ldebug
@@ -1249,27 +1250,27 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
             (* Replace the shared borrow with bottom *)
             let allow_inner_loans = false in
             match
-              end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx
+              end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
             with
-            | Error _ -> raise (Failure "Unreachable")
+            | Error _ -> craise meta "Unreachable"
             | Ok (ctx, _) ->
                 (* Give back *)
-                give_back_shared config bid ctx)
+                give_back_shared meta config bid ctx)
         | VMutBorrow (bid, v) -> (
             (* Replace the mut borrow with bottom *)
             let allow_inner_loans = false in
             match
-              end_borrow_get_borrow (Some abs_id) allow_inner_loans bid ctx
+              end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
             with
-            | Error _ -> raise (Failure "Unreachable")
+            | Error _ -> craise meta "Unreachable"
             | Ok (ctx, _) ->
                 (* Give the value back - note that the mut borrow was below a
                  * shared borrow: the value is thus unchanged *)
-                give_back_value config bid v ctx)
-        | VReservedMutBorrow _ -> raise (Failure "Unreachable")
+                give_back_value meta config bid v ctx)
+        | VReservedMutBorrow _ -> craise meta "Unreachable"
       in
       (* Reexplore *)
-      end_abstraction_borrows config chain abs_id cf ctx
+      end_abstraction_borrows meta config chain abs_id cf ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
 and end_abstraction_remove_from_context (_config : config)
@@ -1296,12 +1297,12 @@ and end_abstraction_remove_from_context (_config : config)
         intersecting proj_borrows, either in the concrete context or in an
         abstraction
 *)
-and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
+and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value)
     : cm_fun =
  fun cf ctx ->
   (* Small helpers for sanity checks *)
-  let check ctx = no_aproj_over_symbolic_in_context sv ctx in
+  let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in
   let cf_check (cf : m_fun) : m_fun =
    fun ctx ->
     check ctx;
@@ -1309,13 +1310,13 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
   in
   (* Find the first proj_borrows which intersects the proj_loans *)
   let explore_shared = true in
-  match lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx with
+  match lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx with
   | None ->
       (* We couldn't find any in the context: it means that the symbolic value
        * is in the concrete environment (or that we dropped it, in which case
        * it is completely absent). We thus simply need to replace the loans
        * projector with an ended projector. *)
-      let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+      let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
       (* Sanity check *)
       check ctx;
       (* Continue *)
@@ -1359,15 +1360,15 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
             AbstractionId.Set.empty abs_ids
         in
         (* End the abstractions and continue *)
-        end_abstractions_aux config chain abs_ids cf ctx
+        end_abstractions_aux meta config chain abs_ids cf ctx
       in
       (* End the internal borrows projectors and the loans projector *)
       let cf_end_internal : cm_fun =
        fun cf ctx ->
         (* All the proj_borrows are owned: simply erase them *)
-        let ctx = remove_intersecting_aproj_borrows_shared regions sv ctx in
+        let ctx = remove_intersecting_aproj_borrows_shared meta regions sv ctx in
         (* End the loan itself *)
-        let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+        let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
         (* Sanity check *)
         check ctx;
         (* Continue *)
@@ -1399,48 +1400,48 @@ and end_proj_loans_symbolic (config : config) (chain : borrow_or_abs_ids)
         *)
         (* End the projector of borrows - TODO: not completely sure what to
          * replace it with... Maybe we should introduce an ABottomProj? *)
-        let ctx = update_aproj_borrows abs_id sv AIgnoredProjBorrows ctx in
+        let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in
         (* Sanity check: no other occurrence of an intersecting projector of borrows *)
-        assert (
+        cassert (
           Option.is_none
-            (lookup_intersecting_aproj_borrows_opt explore_shared regions sv ctx));
+            (lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx)) meta "no other occurrence of an intersecting projector of borrows";
         (* End the projector of loans *)
-        let ctx = update_aproj_loans_to_ended abs_id sv ctx in
+        let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
         (* Sanity check *)
         check ctx;
         (* Continue *)
         cf ctx)
       else
         (* The borrows proj comes from a different abstraction: end it. *)
-        let cc = end_abstraction_aux config chain abs_id' in
+        let cc = end_abstraction_aux meta config chain abs_id' in
         (* Retry ending the projector of loans *)
         let cc =
-          comp cc (end_proj_loans_symbolic config chain abs_id regions sv)
+          comp cc (end_proj_loans_symbolic meta config chain abs_id regions sv)
         in
         (* Sanity check *)
         let cc = comp cc cf_check in
         (* Continue *)
         cc cf ctx
 
-let end_borrow config : BorrowId.id -> cm_fun = end_borrow_aux config [] None
+let end_borrow (meta : Meta.meta ) config : BorrowId.id -> cm_fun = end_borrow_aux meta config [] None
 
-let end_borrows config : BorrowId.Set.t -> cm_fun =
-  end_borrows_aux config [] None
+let end_borrows (meta : Meta.meta ) config : BorrowId.Set.t -> cm_fun =
+  end_borrows_aux meta config [] None
 
-let end_abstraction config = end_abstraction_aux config []
-let end_abstractions config = end_abstractions_aux config []
+let end_abstraction meta config = end_abstraction_aux meta config []
+let end_abstractions meta config = end_abstractions_aux meta config []
 
-let end_borrow_no_synth config id ctx =
-  get_cf_ctx_no_synth (end_borrow config id) ctx
+let end_borrow_no_synth meta config id ctx =
+  get_cf_ctx_no_synth (end_borrow meta config id) ctx
 
-let end_borrows_no_synth config ids ctx =
-  get_cf_ctx_no_synth (end_borrows config ids) ctx
+let end_borrows_no_synth meta config ids ctx =
+  get_cf_ctx_no_synth (end_borrows meta config ids) ctx
 
-let end_abstraction_no_synth config id ctx =
-  get_cf_ctx_no_synth (end_abstraction config id) ctx
+let end_abstraction_no_synth meta config id ctx =
+  get_cf_ctx_no_synth (end_abstraction meta config id) ctx
 
-let end_abstractions_no_synth config ids ctx =
-  get_cf_ctx_no_synth (end_abstractions config ids) ctx
+let end_abstractions_no_synth meta config ids ctx =
+  get_cf_ctx_no_synth (end_abstractions meta config ids) ctx
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
@@ -1458,7 +1459,7 @@ let end_abstractions_no_synth config ids ctx =
 
     The loan to update mustn't be a borrowed value.
  *)
-let promote_shared_loan_to_mut_loan (l : BorrowId.id)
+let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
     (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
@@ -1473,38 +1474,38 @@ let promote_shared_loan_to_mut_loan (l : BorrowId.id)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
-  match lookup_loan ek l ctx with
+  match lookup_loan meta ek l ctx with
   | _, Concrete (VMutLoan _) ->
-      raise (Failure "Expected a shared loan, found a mut loan")
+      craise meta "Expected a shared loan, found a mut loan"
   | _, Concrete (VSharedLoan (bids, sv)) ->
       (* Check that there is only one borrow id (l) and update the loan *)
-      assert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1);
+      cassert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1) meta "There should only be one borrow id";
       (* We need to check that there aren't any loans in the value:
          we should have gotten rid of those already, but it is better
          to do a sanity check. *)
-      assert (not (loans_in_value sv));
+      cassert (not (loans_in_value sv)) meta "There shouldn't be any loans in the value";
       (* Check there isn't {!Bottom} (this is actually an invariant *)
-      assert (not (bottom_in_value ctx.ended_regions sv));
+      cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a !Bottom";
       (* Check there aren't reserved borrows *)
-      assert (not (reserved_in_value sv));
+      cassert (not (reserved_in_value sv)) meta "There shouldn't have reserved borrows";
       (* Update the loan content *)
-      let ctx = update_loan ek l (VMutLoan l) ctx in
+      let ctx = update_loan meta ek l (VMutLoan l) ctx in
       (* Continue *)
       cf sv ctx
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      raise
-        (Failure
+      craise
+        meta
            "Can't promote a shared loan to a mutable loan if the loan is \
-            inside an abstraction")
+            inside an abstraction"
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
     This function updates a shared borrow to a mutable borrow (and that is
     all: it doesn't touch the corresponding loan).
  *)
-let replace_reserved_borrow_with_mut_borrow (l : BorrowId.id) (cf : m_fun)
+let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) (cf : m_fun)
     (borrowed_value : typed_value) : m_fun =
  fun ctx ->
   (* Lookup the reserved borrow - note that we don't go inside borrows/loans:
@@ -1514,32 +1515,32 @@ let replace_reserved_borrow_with_mut_borrow (l : BorrowId.id) (cf : m_fun)
     { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
   in
   let ctx =
-    match lookup_borrow ek l ctx with
+    match lookup_borrow meta ek l ctx with
     | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) ->
-        raise (Failure "Expected a reserved mutable borrow")
+        craise meta "Expected a reserved mutable borrow"
     | Concrete (VReservedMutBorrow _) ->
         (* Update it *)
-        update_borrow ek l (VMutBorrow (l, borrowed_value)) ctx
+        update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx
     | Abstract _ ->
         (* This can't happen for sure *)
-        raise
-          (Failure
+        craise
+          meta
              "Can't promote a shared borrow to a mutable borrow if the borrow \
-              is inside an abstraction")
+              is inside an abstraction"
   in
   (* Continue *)
   cf ctx
 
 (** Promote a reserved mut borrow to a mut borrow. *)
-let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun
+let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : BorrowId.id) : cm_fun
     =
  fun cf ctx ->
   (* Lookup the value *)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
-  match lookup_loan ek l ctx with
-  | _, Concrete (VMutLoan _) -> raise (Failure "Unreachable")
+  match lookup_loan meta ek l ctx with
+  | _, Concrete (VMutLoan _) -> craise meta "Unreachable"
   | _, Concrete (VSharedLoan (bids, sv)) -> (
       (* If there are loans inside the value, end them. Note that there can't be
          reserved borrows inside the value.
@@ -1549,11 +1550,11 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun
           (* End the loans *)
           let cc =
             match lc with
-            | VSharedLoan (bids, _) -> end_borrows config bids
-            | VMutLoan bid -> end_borrow config bid
+            | VSharedLoan (bids, _) -> end_borrows meta config bids
+            | VMutLoan bid -> end_borrow meta config bid
           in
           (* Recursive call *)
-          let cc = comp cc (promote_reserved_mut_borrow config l) in
+          let cc = comp cc (promote_reserved_mut_borrow meta config l) in
           (* Continue *)
           cc cf ctx
       | None ->
@@ -1563,36 +1564,36 @@ let rec promote_reserved_mut_borrow (config : config) (l : BorrowId.id) : cm_fun
             (lazy
               ("activate_reserved_mut_borrow: resulting value:\n"
               ^ typed_value_to_string ctx sv));
-          assert (not (loans_in_value sv));
-          assert (not (bottom_in_value ctx.ended_regions sv));
-          assert (not (reserved_in_value sv));
+          cassert (not (loans_in_value sv)) meta "TODO: error message";
+          cassert (not (bottom_in_value ctx.ended_regions sv)) meta "TODO: error message";
+          cassert (not (reserved_in_value sv)) meta "TODO: error message";
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = BorrowId.Set.remove l bids in
-          let cc = end_borrows config bids in
+          let cc = end_borrows meta config bids in
           (* Promote the loan - TODO: this will fail if the value contains
            * any loans. In practice, it shouldn't, but we could also
            * look for loans inside the value and end them before promoting
            * the borrow. *)
-          let cc = comp cc (promote_shared_loan_to_mut_loan l) in
+          let cc = comp cc (promote_shared_loan_to_mut_loan meta l) in
           (* Promote the borrow - the value should have been checked by
              {!promote_shared_loan_to_mut_loan}
           *)
           let cc =
             comp cc (fun cf borrowed_value ->
-                replace_reserved_borrow_with_mut_borrow l cf borrowed_value)
+                replace_reserved_borrow_with_mut_borrow meta l cf borrowed_value)
           in
           (* Continue *)
           cc cf ctx)
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      raise
-        (Failure
+      craise
+        meta
            "Can't activate a reserved mutable borrow referencing a loan inside\n\
-           \         an abstraction")
+           \         an abstraction"
 
-let destructure_abs (abs_kind : abs_kind) (can_end : bool)
+let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs =
   (* Accumulator to store the destructured values *)
   let avalues = ref [] in
@@ -1605,7 +1606,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
      ignore the children altogether. Instead, we explore them and make sure
      we don't register values while doing so.
   *)
-  let push_fail _ = raise (Failure "Unreachable") in
+  let push_fail _ = craise meta "Unreachable" in
   (* Function to explore an avalue and destructure it *)
   let rec list_avalues (allow_borrows : bool) (push : typed_avalue -> unit)
       (av : typed_avalue) : unit =
@@ -1620,7 +1621,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
         match lc with
         | ASharedLoan (bids, sv, child_av) ->
             (* We don't support nested borrows for now *)
-            assert (not (value_has_borrows ctx sv.value));
+            cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
             (* Destructure the shared value *)
             let avl, sv =
               if destructure_shared_values then list_values sv else ([], sv)
@@ -1647,8 +1648,8 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
             push { value; ty }
         | AIgnoredMutLoan (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
-            assert (opt_bid = None);
+            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+            cassert (opt_bid = None) meta "TODO: error message";
             (* Simply explore the child *)
             list_avalues false push_fail child_av
         | AEndedMutLoan
@@ -1658,12 +1659,12 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
             { child = child_av; given_back = _; given_back_meta = _ }
         | AIgnoredSharedLoan child_av ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
+            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
             (* Simply explore the child *)
             list_avalues false push_fail child_av)
     | ABorrow bc -> (
         (* Sanity check - rem.: may be redundant with [push_fail] *)
-        assert allow_borrows;
+        cassert allow_borrows meta "TODO: error message";
         (* Explore the borrow content *)
         match bc with
         | AMutBorrow (bid, child_av) ->
@@ -1678,19 +1679,19 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
             push av
         | AIgnoredMutBorrow (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
-            assert (opt_bid = None);
+            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+            cassert (opt_bid = None) meta "TODO: error message";
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AEndedIgnoredMutBorrow
             { child = child_av; given_back = _; given_back_meta = _ } ->
             (* We don't support nested borrows for now *)
-            assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
+            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AProjSharedBorrow asb ->
             (* We don't support nested borrows *)
-            assert (asb = []);
+            cassert (asb = []) meta "Nested borrows are not supported yet";
             (* Nothing specific to do *)
             ()
         | AEndedMutBorrow _ | AEndedSharedBorrow ->
@@ -1698,11 +1699,11 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
                be in the context anymore (if we end *one* borrow in an abstraction,
                we have to end them all and remove the abstraction from the context)
             *)
-            raise (Failure "Unreachable"))
+            craise meta "Unreachable")
     | ASymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        assert (not (ty_has_borrows ctx.type_ctx.type_infos ty))
+        cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message"
   and list_values (v : typed_value) : typed_avalue list * typed_value =
     let ty = v.ty in
     match v.value with
@@ -1714,19 +1715,19 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
         let avl = List.concat avll in
         let adt = { adt with field_values } in
         (avl, { v with value = VAdt adt })
-    | VBottom -> raise (Failure "Unreachable")
+    | VBottom -> craise meta "Unreachable"
     | VBorrow _ ->
         (* We don't support nested borrows for now *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
     | VLoan lc -> (
         match lc with
         | VSharedLoan (bids, sv) ->
             let avl, sv = list_values sv in
             if destructure_shared_values then (
               (* Rem.: the shared value can't contain loans nor borrows *)
-              assert (ty_no_regions ty);
+              cassert (ty_no_regions ty) meta "The shared value can't contain loans nor borrows";
               let av : typed_avalue =
-                assert (not (value_has_loans_or_borrows ctx sv.value));
+                cassert (not (value_has_loans_or_borrows ctx sv.value)) meta "The shared value can't contain loans nor borrows";
                 (* We introduce fresh ids for the symbolic values *)
                 let mk_value_with_fresh_sids (v : typed_value) : typed_value =
                   let visitor =
@@ -1747,11 +1748,11 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
               let avl = List.append [ av ] avl in
               (avl, sv))
             else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) })
-        | VMutLoan _ -> raise (Failure "Unreachable"))
+        | VMutLoan _ -> craise meta "Unreachable")
     | VSymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        assert (not (ty_has_borrows ctx.type_ctx.type_infos ty));
+        cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message";
         ([], v)
   in
 
@@ -1761,14 +1762,14 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
   (* Update *)
   { abs0 with avalues; kind = abs_kind; can_end }
 
-let abs_is_destructured (destructure_shared_values : bool) (ctx : eval_ctx)
+let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool) (ctx : eval_ctx)
     (abs : abs) : bool =
   let abs' =
-    destructure_abs abs.kind abs.can_end destructure_shared_values ctx abs
+    destructure_abs meta abs.kind abs.can_end destructure_shared_values ctx abs
   in
   abs = abs'
 
-let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
+let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     (destructure_shared_values : bool) (ctx : eval_ctx) (v : typed_value) :
     abs list =
   (* Convert the value to a list of avalues *)
@@ -1851,20 +1852,20 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
         (avl, { v with value = VAdt adt })
     | VBorrow bc -> (
         let _, ref_ty, kind = ty_as_ref ty in
-        assert (ty_no_regions ref_ty);
+        cassert (ty_no_regions ref_ty) meta "TODO: error message";
         (* Sanity check *)
-        assert allow_borrows;
+        cassert allow_borrows meta "TODO: error message";
         (* Convert the borrow content *)
         match bc with
         | VSharedBorrow bid ->
-            assert (ty_no_regions ref_ty);
+            cassert (ty_no_regions ref_ty) meta "TODO: error message";
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let value = ABorrow (ASharedBorrow bid) in
             ([ { value; ty } ], v)
         | VMutBorrow (bid, bv) ->
             let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
-            assert (not (value_has_borrows ctx bv.value));
+            cassert (not (value_has_borrows ctx bv.value)) meta "Nested borrows are not supported yet";
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let ignored = mk_aignored ref_ty in
@@ -1877,16 +1878,16 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
             (av :: avl, value)
         | VReservedMutBorrow _ ->
             (* This borrow should have been activated *)
-            raise (Failure "Unexpected"))
+            craise meta "Unexpected")
     | VLoan lc -> (
         match lc with
         | VSharedLoan (bids, sv) ->
             let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
-            assert (not (value_has_borrows ctx sv.value));
+            cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            assert (ty_no_regions ty);
+            cassert (ty_no_regions ty) meta "TODO: error message";
             let ty = mk_ref_ty (RFVar r_id) ty RShared in
             let ignored = mk_aignored ty in
             (* Rem.: the shared value might contain loans *)
@@ -1904,7 +1905,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
         | VMutLoan bid ->
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            assert (ty_no_regions ty);
+            cassert (ty_no_regions ty) meta "TODO: error message";
             let ty = mk_ref_ty (RFVar r_id) ty RMut in
             let ignored = mk_aignored ty in
             let av = ALoan (AMutLoan (bid, ignored)) in
@@ -1913,7 +1914,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
     | VSymbolic _ ->
         (* For now, we force all the symbolic values containing borrows to
            be eagerly expanded, and we don't support nested borrows *)
-        assert (not (value_has_borrows ctx v.value));
+        cassert (not (value_has_borrows ctx v.value)) meta "TODO: error message";
         (* Return nothing *)
         ([], v)
   in
@@ -1954,7 +1955,7 @@ type merge_abstraction_info = {
     - all the borrows are destructured (for instance, shared loans can't
       contain shared loans).
  *)
-let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
+let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : abs) :
     merge_abstraction_info =
   let loans : loan_id_set ref = ref BorrowId.Set.empty in
   let borrows : borrow_id_set ref = ref BorrowId.Set.empty in
@@ -1967,26 +1968,26 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
   in
 
   let push_loans ids (lc : g_loan_content_with_ty) : unit =
-    assert (BorrowId.Set.disjoint !loans ids);
+    cassert (BorrowId.Set.disjoint !loans ids) meta "TODO: error message";
     loans := BorrowId.Set.union !loans ids;
     BorrowId.Set.iter
       (fun id ->
-        assert (not (BorrowId.Map.mem id !loan_to_content));
+        cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
         loan_to_content := BorrowId.Map.add id lc !loan_to_content;
         borrows_loans := LoanId id :: !borrows_loans)
       ids
   in
   let push_loan id (lc : g_loan_content_with_ty) : unit =
-    assert (not (BorrowId.Set.mem id !loans));
+    cassert (not (BorrowId.Set.mem id !loans)) meta "TODO: error message";
     loans := BorrowId.Set.add id !loans;
-    assert (not (BorrowId.Map.mem id !loan_to_content));
+    cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
     loan_to_content := BorrowId.Map.add id lc !loan_to_content;
     borrows_loans := LoanId id :: !borrows_loans
   in
   let push_borrow id (bc : g_borrow_content_with_ty) : unit =
-    assert (not (BorrowId.Set.mem id !borrows));
+    cassert (not (BorrowId.Set.mem id !borrows)) meta "TODO: error message";
     borrows := BorrowId.Set.add id !borrows;
-    assert (not (BorrowId.Map.mem id !borrow_to_content));
+    cassert (not (BorrowId.Map.mem id !borrow_to_content)) meta "TODO: error message";
     borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
     borrows_loans := BorrowId id :: !borrows_loans
   in
@@ -2009,23 +2010,23 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
         let ty =
           match Option.get env with
           | Concrete ty -> ty
-          | Abstract _ -> raise (Failure "Unreachable")
+          | Abstract _ -> craise meta "Unreachable"
         in
         (match lc with
         | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
-        | VMutLoan _ -> raise (Failure "Unreachable"));
+        | VMutLoan _ -> craise meta "Unreachable");
         (* Continue *)
         super#visit_loan_content env lc
 
       method! visit_borrow_content _ _ =
         (* Can happen if we explore shared values which contain borrows -
            i.e., if we have nested borrows (we forbid this for now) *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
 
       method! visit_aloan_content env lc =
         let ty =
           match Option.get env with
-          | Concrete _ -> raise (Failure "Unreachable")
+          | Concrete _ -> craise meta "Unreachable"
           | Abstract ty -> ty
         in
         (* Register the loans *)
@@ -2035,14 +2036,14 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
         | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ ->
             (* The abstraction has been destructured, so those shouldn't appear *)
-            raise (Failure "Unreachable"));
+            craise meta "Unreachable");
         (* Continue *)
         super#visit_aloan_content env lc
 
       method! visit_aborrow_content env bc =
         let ty =
           match Option.get env with
-          | Concrete _ -> raise (Failure "Unreachable")
+          | Concrete _ -> craise meta "Unreachable"
           | Abstract ty -> ty
         in
         (* Explore the borrow content *)
@@ -2056,18 +2057,18 @@ let compute_merge_abstraction_info (ctx : eval_ctx) (abs : abs) :
               | AsbProjReborrows _ ->
                   (* Can only happen if the symbolic value (potentially) contains
                      borrows - i.e., we have nested borrows *)
-                  raise (Failure "Unreachable")
+                  craise meta "Unreachable"
             in
             List.iter register asb
         | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _
         | AEndedSharedBorrow ->
             (* The abstraction has been destructured, so those shouldn't appear *)
-            raise (Failure "Unreachable"));
+            craise meta "Unreachable");
         super#visit_aborrow_content env bc
 
       method! visit_symbolic_value _ sv =
         (* Sanity check: no borrows *)
-        assert (not (symbolic_value_has_borrows ctx sv))
+        cassert (not (symbolic_value_has_borrows ctx sv)) meta "TODO: error message" 
     end
   in
 
@@ -2134,7 +2135,7 @@ type merge_duplicates_funcs = {
 
     Merge two abstractions into one, without updating the context.
  *)
-let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
+let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs)
     (abs1 : abs) : abs =
   log#ldebug
@@ -2145,8 +2146,8 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
   (* Check that the abstractions are destructured *)
   if !Config.sanity_checks then (
     let destructure_shared_values = true in
-    assert (abs_is_destructured destructure_shared_values ctx abs0);
-    assert (abs_is_destructured destructure_shared_values ctx abs1));
+    cassert (abs_is_destructured meta destructure_shared_values ctx abs0) meta "Abstractions should be destructured";
+    cassert (abs_is_destructured meta destructure_shared_values ctx abs1) meta "Abstractions should be destructured");
 
   (* Compute the relevant information *)
   let {
@@ -2156,7 +2157,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
     loan_to_content = loan_to_content0;
     borrow_to_content = borrow_to_content0;
   } =
-    compute_merge_abstraction_info ctx abs0
+    compute_merge_abstraction_info meta ctx abs0
   in
 
   let {
@@ -2166,14 +2167,14 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
     loan_to_content = loan_to_content1;
     borrow_to_content = borrow_to_content1;
   } =
-    compute_merge_abstraction_info ctx abs1
+    compute_merge_abstraction_info meta ctx abs1
   in
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
   if merge_funs = None then (
-    assert (BorrowId.Set.disjoint borrows0 borrows1);
-    assert (BorrowId.Set.disjoint loans0 loans1));
+    cassert (BorrowId.Set.disjoint borrows0 borrows1) meta "TODO: error message";
+    cassert (BorrowId.Set.disjoint loans0 loans1)) meta "TODO: error message";
 
   (* Merge.
      There are several cases:
@@ -2214,7 +2215,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
   in
   let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t =
     let bids = BorrowId.Set.diff bids intersect in
-    assert (not (BorrowId.Set.is_empty bids));
+    cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
     bids
   in
   let filter_bid (bid : BorrowId.id) : BorrowId.id option =
@@ -2242,11 +2243,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
         (Option.get merge_funs).merge_ashared_borrows id ty0 ty1
     | AProjSharedBorrow _, AProjSharedBorrow _ ->
         (* Unreachable because requires nested borrows *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
   in
 
   let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
@@ -2254,12 +2255,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
     match (bc0, bc1) with
     | Concrete _, Concrete _ ->
         (* This can happen only in case of nested borrows *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
     | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
         merge_aborrow_contents ty0 bc0 ty1 bc1
     | Concrete _, Abstract _ | Abstract _, Concrete _ ->
         (* TODO: is it really unreachable? *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
   in
 
   let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty)
@@ -2277,7 +2278,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
         (* Check that the sets of ids are the same - if it is not the case, it
            means we actually need to merge more than 2 avalues: we ignore this
            case for now *)
-        assert (BorrowId.Set.equal ids0 ids1);
+        cassert (BorrowId.Set.equal ids0 ids1) meta "Ids are not the same - Case ignored for now";
         let ids = ids0 in
         if BorrowId.Set.is_empty ids then (
           (* If the set of ids is empty, we can eliminate this shared loan.
@@ -2289,10 +2290,10 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
              to preserve (in practice it works because we destructure the
              shared values in the abstractions, and forbid nested borrows).
           *)
-          assert (not (value_has_loans_or_borrows ctx sv0.value));
-          assert (not (value_has_loans_or_borrows ctx sv0.value));
-          assert (is_aignored child0.value);
-          assert (is_aignored child1.value);
+          cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
+          cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
+          cassert (is_aignored child0.value) meta "TODO: error message";
+          cassert (is_aignored child1.value) meta "TODO: error message";
           None)
         else (
           (* Register the loan ids *)
@@ -2304,7 +2305,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
   in
 
   (* Note that because we may filter ids from a set of id, this function has
@@ -2315,12 +2316,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
     match (lc0, lc1) with
     | Concrete _, Concrete _ ->
         (* This can not happen: the values should have been destructured *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
     | Abstract (ty0, lc0), Abstract (ty1, lc1) ->
         merge_aloan_contents ty0 lc0 ty1 lc1
     | Concrete _, Abstract _ | Abstract _, Concrete _ ->
         (* TODO: is it really unreachable? *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
   in
 
   (* Note that we first explore the borrows/loans of [abs1], because we
@@ -2361,12 +2362,12 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
                              a concrete borrow can only happen inside a shared
                              loan
                           *)
-                          raise (Failure "Unreachable")
+                          craise meta "Unreachable"
                       | Abstract (ty, bc) -> { value = ABorrow bc; ty })
                   | Some bc0, Some bc1 ->
-                      assert (merge_funs <> None);
+                      cassert (merge_funs <> None) meta "TODO: error message";
                       merge_g_borrow_contents bc0 bc1
-                  | None, None -> raise (Failure "Unreachable")
+                  | None, None -> craise meta "Unreachable"
                 in
                 push_avalue av)
       | LoanId bid ->
@@ -2399,15 +2400,15 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
                       | Concrete _ ->
                           (* This shouldn't happen because the avalues should
                              have been destructured. *)
-                          raise (Failure "Unreachable")
+                          craise meta "Unreachable"
                       | Abstract (ty, lc) -> (
                           match lc with
                           | ASharedLoan (bids, sv, child) ->
                               let bids = filter_bids bids in
-                              assert (not (BorrowId.Set.is_empty bids));
-                              assert (is_aignored child.value);
-                              assert (
-                                not (value_has_loans_or_borrows ctx sv.value));
+                              cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
+                              cassert (is_aignored child.value) meta "TODO: error message";
+                              cassert (
+                                not (value_has_loans_or_borrows ctx sv.value)) meta "TODO: error message";
                               let lc = ASharedLoan (bids, sv, child) in
                               set_loans_as_merged bids;
                               Some { value = ALoan lc; ty }
@@ -2418,11 +2419,11 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
                           | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _
                           | AIgnoredSharedLoan _ ->
                               (* The abstraction has been destructured, so those shouldn't appear *)
-                              raise (Failure "Unreachable")))
+                              craise meta "Unreachable"))
                   | Some lc0, Some lc1 ->
-                      assert (merge_funs <> None);
+                      cassert (merge_funs <> None) meta "TODO: error message";
                       merge_g_loan_contents lc0 lc1
-                  | None, None -> raise (Failure "Unreachable")
+                  | None, None -> craise meta "Unreachable"
                 in
                 push_opt_avalue av))
     borrows_loans;
@@ -2440,7 +2441,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> raise (Failure "Unexpected")
+      | _ -> craise meta "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow avalues in
     List.append aborrows aloans
@@ -2475,7 +2476,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
   in
 
   (* Sanity check *)
-  if !Config.sanity_checks then assert (abs_is_destructured true ctx abs);
+  if !Config.sanity_checks then cassert (abs_is_destructured meta true ctx abs) meta "TODO: error message";
   (* Return *)
   abs
 
@@ -2486,7 +2487,7 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id)
   let env = Substitute.env_subst_rids rsubst ctx.env in
   { ctx with env }
 
-let merge_into_abstraction (abs_kind : abs_kind) (can_end : bool)
+let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx)
     (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) :
     eval_ctx * AbstractionId.id =
@@ -2496,7 +2497,7 @@ let merge_into_abstraction (abs_kind : abs_kind) (can_end : bool)
 
   (* Merge them *)
   let nabs =
-    merge_into_abstraction_aux abs_kind can_end merge_funs ctx abs0 abs1
+    merge_into_abstraction_aux meta abs_kind can_end merge_funs ctx abs0 abs1
   in
 
   (* Update the environment: replace the abstraction 1 with the result of the merge,
-- 
cgit v1.2.3


From 8f89bd8df9f382284eabb5a2020a2fa634f92fac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 17:19:14 +0100
Subject: WIP: does not compile yet because we need to propagate the meta
 variable.

---
 compiler/InterpreterBorrows.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index ae251fbf..e37a67b7 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1030,7 +1030,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       (* Remove all the references to the id of the current abstraction, and remove
        * the abstraction itself.
        * **Rk.**: this is where we synthesize the updated symbolic AST *)
-      let cc = comp cc (end_abstraction_remove_from_context config abs_id) in
+      let cc = comp cc (end_abstraction_remove_from_context meta config abs_id) in
 
       (* Debugging *)
       let cc =
@@ -1273,10 +1273,10 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
       end_abstraction_borrows meta config chain abs_id cf ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
-and end_abstraction_remove_from_context (_config : config)
+and end_abstraction_remove_from_context (meta : Meta.meta)  (_config : config)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
-  let ctx, abs = ctx_remove_abs ctx abs_id in
+  let ctx, abs = ctx_remove_abs meta ctx abs_id in
   let abs = Option.get abs in
   (* Apply the continuation *)
   let expr = cf ctx in
@@ -2502,8 +2502,8 @@ let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (can_end : b
 
   (* Update the environment: replace the abstraction 1 with the result of the merge,
      remove the abstraction 0 *)
-  let ctx = fst (ctx_subst_abs ctx abs_id1 nabs) in
-  let ctx = fst (ctx_remove_abs ctx abs_id0) in
+  let ctx = fst (ctx_subst_abs meta ctx abs_id1 nabs) in
+  let ctx = fst (ctx_remove_abs meta ctx abs_id0) in
 
   (* Merge all the regions from the abstraction into one (the first - i.e., the
      one with the smallest id). Note that we need to do this in the whole
-- 
cgit v1.2.3


From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 21 Mar 2024 12:34:40 +0100
Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to
 do and we need to see how translate_crate can give meta to the functions it
 calls

---
 compiler/InterpreterBorrows.ml | 92 +++++++++++++++++++++---------------------
 1 file changed, 46 insertions(+), 46 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e37a67b7..be31d865 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -216,7 +216,7 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
               set_replaced_bc (fst outer) (Abstract bc);
               (* Update the value - note that we are necessarily in the second
                * of the two cases described above *)
-              let asb = remove_borrow_from_asb l asb in
+              let asb = remove_borrow_from_asb meta l asb in
               ABorrow (AProjSharedBorrow asb))
             else (* Nothing special to do *)
               super#visit_ABorrow outer bc
@@ -254,8 +254,8 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
   log#ldebug
     (lazy
       ("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: "
-      ^ typed_value_to_string ctx nv
-      ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+      ^ typed_value_to_string meta ctx nv
+      ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -267,7 +267,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
   (* We sometimes need to reborrow values while giving a value back due: prepare that *)
   let allow_reborrows = true in
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows
+    prepare_reborrows meta config allow_reborrows
   in
   (* The visitor to give back the values *)
   let obj =
@@ -335,7 +335,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
                   (* Remember the given back value as a meta-value
                    * TODO: it is a bit annoying to have to deconstruct
                    * the value... Think about a more elegant way. *)
-                  let given_back_meta = as_symbolic nv.value in
+                  let given_back_meta = as_symbolic meta nv.value in
                   (* The loan projector *)
                   let given_back =
                     mk_aproj_loans_value_from_symbolic_value abs.regions sv
@@ -382,7 +382,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
               let given_back_meta = nv in
               (* Apply the projection *)
               let given_back =
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
                   regions ancestors_regions nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
@@ -409,7 +409,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
                * we don't register the fact that we inserted the value somewhere
                * (i.e., we don't call {!set_replaced}) *)
               let given_back =
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
                   regions ancestors_regions nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
@@ -720,8 +720,8 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B
     be expanded (because expanding this symbolic value would require expanding
     a reference whose region has already ended).
  *)
-let convert_avalue_to_given_back_value (av : typed_avalue) : symbolic_value =
-  mk_fresh_symbolic_value av.ty
+let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) : symbolic_value =
+  mk_fresh_symbolic_value meta av.ty
 
 (** Auxiliary function: see {!end_borrow_aux}.
 
@@ -746,11 +746,11 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
     (lazy
       (let bc =
          match bc with
-         | Concrete bc -> borrow_content_to_string ctx bc
-         | Abstract bc -> aborrow_content_to_string ctx bc
+         | Concrete bc -> borrow_content_to_string meta ctx bc
+         | Abstract bc -> aborrow_content_to_string meta ctx bc
        in
        "give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc
-       ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+       ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
   (* This is used for sanity checks *)
   let sanity_ek =
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -781,7 +781,7 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
          Rem.: we shouldn't do this here. We should do this in a function
          which takes care of ending *sub*-abstractions.
       *)
-      let sv = convert_avalue_to_given_back_value av in
+      let sv = convert_avalue_to_given_back_value meta av in
       (* Update the context *)
       give_back_avalue_to_same_abstraction meta config l av
         (mk_typed_value_from_symbolic_value sv)
@@ -814,8 +814,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
             (lazy
               (fun_name ^ ": " ^ BorrowId.to_string l
              ^ ": borrow didn't disappear:\n- original context:\n"
-             ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
-             ^ eval_ctx_to_string ctx));
+             ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n"
+             ^ eval_ctx_to_string meta ctx));
           craise meta "Borrow not eliminated"
     in
     match lookup_loan_opt meta ek_all l ctx with
@@ -825,8 +825,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
           (lazy
             (fun_name ^ ": " ^ BorrowId.to_string l
            ^ ": loan didn't disappear:\n- original context:\n"
-           ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
-           ^ eval_ctx_to_string ctx));
+           ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n"
+           ^ eval_ctx_to_string meta ctx));
         craise meta "Loan not eliminated"
   in
   unit_to_cm_fun check_disappeared
@@ -858,12 +858,12 @@ let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_a
   (* Check that we don't loop *)
   let chain0 = chain in
   let chain =
-    add_borrow_or_abs_id_to_chain "end_borrow_aux: " (BorrowId l) chain
+    add_borrow_or_abs_id_to_chain meta "end_borrow_aux: " (BorrowId l) chain
   in
   log#ldebug
     (lazy
       ("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n"
-     ^ eval_ctx_to_string ctx));
+     ^ eval_ctx_to_string meta ctx));
 
   (* Utility function for the sanity checks: check that the borrow disappeared
    * from the context *)
@@ -958,7 +958,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
  fun cf ctx ->
   (* Check that we don't loop *)
   let chain =
-    add_borrow_or_abs_id_to_chain "end_abstraction_aux: " (AbsId abs_id) chain
+    add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id) chain
   in
   (* Remember the original context for printing purposes *)
   let ctx0 = ctx in
@@ -966,7 +966,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
     (lazy
       ("end_abstraction_aux: "
       ^ AbstractionId.to_string abs_id
-      ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0));
+      ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0));
 
   (* Lookup the abstraction - note that if we end a list of abstractions,
      ending one abstraction may lead to the current abstraction having
@@ -999,7 +999,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
                 ^ "\n- context after parent abstractions ended:\n"
-                ^ eval_ctx_to_string ctx)))
+                ^ eval_ctx_to_string meta ctx)))
       in
 
       (* End the loans inside the abstraction *)
@@ -1010,7 +1010,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
               (lazy
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
-                ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)))
+                ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string meta ctx)))
       in
 
       (* End the abstraction itself by redistributing the borrows it contains *)
@@ -1039,8 +1039,8 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
               (lazy
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
-                ^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
-                ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
+                ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0
+                ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx)))
       in
 
       (* Sanity check: ending an abstraction must preserve the invariants *)
@@ -1173,12 +1173,12 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
       log#ldebug
         (lazy
           ("end_abstraction_borrows: found aborrow content: "
-          ^ aborrow_content_to_string ctx bc));
+          ^ aborrow_content_to_string meta ctx bc));
       let ctx =
         match bc with
         | AMutBorrow (bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
-            let sv = convert_avalue_to_given_back_value av in
+            let sv = convert_avalue_to_given_back_value meta av in
             (* Replace the mut borrow to register the fact that we ended
              * it and store with it the freshly generated given back value *)
             let ended_borrow = ABorrow (AEndedMutBorrow (sv, av)) in
@@ -1228,7 +1228,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
           ("end_abstraction_borrows: found aproj borrows: "
           ^ aproj_to_string ctx (AProjBorrows (sv, proj_ty))));
       (* Generate a fresh symbolic value *)
-      let nsv = mk_fresh_symbolic_value proj_ty in
+      let nsv = mk_fresh_symbolic_value meta proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
       let ended_borrow = AEndedProjBorrows nsv in
       let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in
@@ -1243,7 +1243,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
       log#ldebug
         (lazy
           ("end_abstraction_borrows: found borrow content: "
-          ^ borrow_content_to_string ctx bc));
+          ^ borrow_content_to_string meta ctx bc));
       let ctx =
         match bc with
         | VSharedBorrow bid -> (
@@ -1432,16 +1432,16 @@ let end_abstraction meta config = end_abstraction_aux meta config []
 let end_abstractions meta config = end_abstractions_aux meta config []
 
 let end_borrow_no_synth meta config id ctx =
-  get_cf_ctx_no_synth (end_borrow meta config id) ctx
+  get_cf_ctx_no_synth meta (end_borrow meta config id) ctx
 
 let end_borrows_no_synth meta config ids ctx =
-  get_cf_ctx_no_synth (end_borrows meta config ids) ctx
+  get_cf_ctx_no_synth meta (end_borrows meta config ids) ctx
 
 let end_abstraction_no_synth meta config id ctx =
-  get_cf_ctx_no_synth (end_abstraction meta config id) ctx
+  get_cf_ctx_no_synth meta (end_abstraction meta config id) ctx
 
 let end_abstractions_no_synth meta config ids ctx =
-  get_cf_ctx_no_synth (end_abstractions meta config ids) ctx
+  get_cf_ctx_no_synth meta (end_abstractions meta config ids) ctx
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
@@ -1466,7 +1466,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
   log#ldebug
     (lazy
       ("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l
-     ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+     ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
   (* Lookup the shared loan - note that we can't promote a shared loan
    * in a shared value, but we can do it in a mutably borrowed value.
    * This is important because we can do: [let y = &two-phase ( *x );]
@@ -1563,7 +1563,7 @@ let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : Bo
           log#ldebug
             (lazy
               ("activate_reserved_mut_borrow: resulting value:\n"
-              ^ typed_value_to_string ctx sv));
+              ^ typed_value_to_string meta ctx sv));
           cassert (not (loans_in_value sv)) meta "TODO: error message";
           cassert (not (bottom_in_value ctx.ended_regions sv)) meta "TODO: error message";
           cassert (not (reserved_in_value sv)) meta "TODO: error message";
@@ -1627,7 +1627,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
               if destructure_shared_values then list_values sv else ([], sv)
             in
             (* Push a value *)
-            let ignored = mk_aignored child_av.ty in
+            let ignored = mk_aignored meta child_av.ty in
             let value = ALoan (ASharedLoan (bids, sv, ignored)) in
             push { value; ty };
             (* Explore the child *)
@@ -1643,7 +1643,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             (* Explore the child *)
             list_avalues false push_fail child_av;
             (* Explore the whole loan *)
-            let ignored = mk_aignored child_av.ty in
+            let ignored = mk_aignored meta child_av.ty in
             let value = ALoan (AMutLoan (bid, ignored)) in
             push { value; ty }
         | AIgnoredMutLoan (opt_bid, child_av) ->
@@ -1671,7 +1671,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             (* Explore the child *)
             list_avalues false push_fail child_av;
             (* Explore the borrow *)
-            let ignored = mk_aignored child_av.ty in
+            let ignored = mk_aignored meta child_av.ty in
             let value = ABorrow (AMutBorrow (bid, ignored)) in
             push { value; ty }
         | ASharedBorrow _ ->
@@ -1742,7 +1742,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
                 in
                 let sv = mk_value_with_fresh_sids sv in
                 (* Create the new avalue *)
-                let value = ALoan (ASharedLoan (bids, sv, mk_aignored ty)) in
+                let value = ALoan (ASharedLoan (bids, sv, mk_aignored meta ty)) in
                 { value; ty }
               in
               let avl = List.append [ av ] avl in
@@ -1808,7 +1808,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
     log#ldebug
       (lazy
         ("convert_value_to_abstractions: to_avalues:\n- value: "
-        ^ typed_value_to_string ctx v));
+        ^ typed_value_to_string meta ctx v));
 
     let ty = v.ty in
     match v.value with
@@ -1868,7 +1868,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
             cassert (not (value_has_borrows ctx bv.value)) meta "Nested borrows are not supported yet";
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
             let ty = TRef (RFVar r_id, ref_ty, kind) in
-            let ignored = mk_aignored ref_ty in
+            let ignored = mk_aignored meta ref_ty in
             let av = ABorrow (AMutBorrow (bid, ignored)) in
             let av = { value = av; ty } in
             (* Continue exploring, looking for loans (and forbidding borrows,
@@ -1889,7 +1889,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
             (* For avalues, a loan has the borrow type *)
             cassert (ty_no_regions ty) meta "TODO: error message";
             let ty = mk_ref_ty (RFVar r_id) ty RShared in
-            let ignored = mk_aignored ty in
+            let ignored = mk_aignored meta ty in
             (* Rem.: the shared value might contain loans *)
             let avl, sv = to_avalues false true true r_id sv in
             let av = ALoan (ASharedLoan (bids, sv, ignored)) in
@@ -1907,7 +1907,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
             (* For avalues, a loan has the borrow type *)
             cassert (ty_no_regions ty) meta "TODO: error message";
             let ty = mk_ref_ty (RFVar r_id) ty RMut in
-            let ignored = mk_aignored ty in
+            let ignored = mk_aignored meta ty in
             let av = ALoan (AMutLoan (bid, ignored)) in
             let av = { value = av; ty } in
             ([ av ], v))
@@ -2140,8 +2140,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
     (abs1 : abs) : abs =
   log#ldebug
     (lazy
-      ("merge_into_abstraction_aux:\n- abs0:\n" ^ abs_to_string ctx abs0
-     ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1));
+      ("merge_into_abstraction_aux:\n- abs0:\n" ^ abs_to_string meta ctx abs0
+     ^ "\n\n- abs1:\n" ^ abs_to_string meta ctx abs1));
 
   (* Check that the abstractions are destructured *)
   if !Config.sanity_checks then (
@@ -2201,7 +2201,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
     log#ldebug
       (lazy
         ("merge_into_abstraction_aux: push_avalue: "
-        ^ typed_avalue_to_string ctx av));
+        ^ typed_avalue_to_string meta ctx av));
     avalues := av :: !avalues
   in
   let push_opt_avalue av =
-- 
cgit v1.2.3


From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Mon, 25 Mar 2024 12:06:05 +0100
Subject: Inverted meta and config argument orders (from meta -> config to
 config -> meta)

---
 compiler/InterpreterBorrows.ml | 132 ++++++++++++++++++++---------------------
 1 file changed, 66 insertions(+), 66 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index be31d865..c7df2eca 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -245,7 +245,7 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
     give the value back.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv : typed_value)
+let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv : typed_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
   cassert (not (loans_in_value nv)) meta "TODO: error message";
@@ -267,7 +267,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
   (* We sometimes need to reborrow values while giving a value back due: prepare that *)
   let allow_reborrows = true in
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows meta config allow_reborrows
+    prepare_reborrows config meta allow_reborrows
   in
   (* The visitor to give back the values *)
   let obj =
@@ -440,7 +440,7 @@ let give_back_value (meta : Meta.meta) (config : config) (bid : BorrowId.id) (nv
   apply_registered_reborrows ctx
 
 (** Give back a *modified* symbolic value. *)
-let give_back_symbolic_value (meta : Meta.meta) (_config : config) (proj_regions : RegionId.Set.t)
+let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions : RegionId.Set.t)
     (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
@@ -485,7 +485,7 @@ let give_back_symbolic_value (meta : Meta.meta) (_config : config) (proj_regions
     end abstraction when ending this abstraction. When doing this, we need
     to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values.
  *)
-let give_back_avalue_to_same_abstraction (meta : Meta.meta) (_config : config) (bid : BorrowId.id)
+let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (bid : BorrowId.id)
     (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
@@ -588,7 +588,7 @@ let give_back_avalue_to_same_abstraction (meta : Meta.meta) (_config : config) (
     we update.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_shared (meta : Meta.meta) _config (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
+let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -739,7 +739,7 @@ let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) :
     borrows. This kind of internal reshuffling. should be similar to ending
     abstractions (it is tantamount to ending *sub*-abstractions).
  *)
-let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_borrow_content)
+let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_borrow_content)
     (ctx : eval_ctx) : eval_ctx =
   (* Debug *)
   log#ldebug
@@ -763,14 +763,14 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
       cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
       (* Update the context *)
-      give_back_value meta config l tv ctx
+      give_back_value config meta l tv ctx
   | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
       (* Sanity check *)
       cassert (l' = l) meta "TODO: error message";
       (* Check that the borrow is somewhere - purely a sanity check *)
       cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
       (* Update the context *)
-      give_back_shared meta config l ctx
+      give_back_shared config meta l ctx
   | Abstract (AMutBorrow (l', av)) ->
       (* Sanity check *)
       cassert (l' = l) meta "TODO: error message";
@@ -783,7 +783,7 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
       *)
       let sv = convert_avalue_to_given_back_value meta av in
       (* Update the context *)
-      give_back_avalue_to_same_abstraction meta config l av
+      give_back_avalue_to_same_abstraction config meta l av
         (mk_typed_value_from_symbolic_value sv)
         ctx
   | Abstract (ASharedBorrow l') ->
@@ -792,12 +792,12 @@ let give_back (meta : Meta.meta) (config : config) (l : BorrowId.id) (bc : g_bor
       (* Check that the borrow is somewhere - purely a sanity check *)
       cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
       (* Update the context *)
-      give_back_shared meta config l ctx
+      give_back_shared config meta l ctx
   | Abstract (AProjSharedBorrow asb) ->
       (* Sanity check *)
       cassert (borrow_in_asb l asb) meta "TODO: error message";
       (* Update the context *)
-      give_back_shared meta config l ctx
+      give_back_shared config meta l ctx
   | Abstract
       ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
       | AEndedSharedBorrow ) ->
@@ -852,7 +852,7 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
     perform anything smart and is trusted, and another function for the
     book-keeping.
  *)
-let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
@@ -900,22 +900,22 @@ let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_a
            * inside another borrow *)
           let allowed_abs' = None in
           (* End the outer borrows *)
-          let cc = end_borrows_aux meta config chain allowed_abs' bids in
+          let cc = end_borrows_aux config meta chain allowed_abs' bids in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
           let allowed_abs' = None in
           (* End the outer borrow *)
-          let cc = end_borrow_aux meta config chain allowed_abs' bid in
+          let cc = end_borrow_aux config meta chain allowed_abs' bid in
           (* Retry to end the borrow *)
-          let cc = comp cc (end_borrow_aux meta config chain0 allowed_abs l) in
+          let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in
           (* Check and apply *)
           comp cc cf_check cf ctx
       | OuterAbs abs_id ->
           (* The borrow is inside an abstraction: end the whole abstraction *)
-          let cf_end_abs = end_abstraction_aux meta config chain abs_id in
+          let cf_end_abs = end_abstraction_aux config meta chain abs_id in
           (* Compose with a sanity check *)
           comp cf_end_abs cf_check cf ctx)
   | Ok (ctx, None) ->
@@ -934,7 +934,7 @@ let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_a
           cassert (Option.is_none (get_first_loan_in_value bv)) meta "Borrowed value shouldn't contain loans"
       | _ -> ());
       (* Give back the value *)
-      let ctx = give_back meta config l bc ctx in
+      let ctx = give_back config meta l bc ctx in
       (* Do a sanity check and continue *)
       let cc = cf_check in
       (* Save a snapshot of the environment for the name generation *)
@@ -942,7 +942,7 @@ let rec end_borrow_aux (meta : Meta.meta) (config : config) (chain : borrow_or_a
       (* Compose *)
       cc cf ctx
 
-and end_borrows_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_borrows_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the borrow ids,
@@ -950,10 +950,10 @@ and end_borrows_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_
    * a matter of taste, and may make debugging easier *)
   let ids = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
   List.fold_left
-    (fun cf id -> end_borrow_aux meta config chain allowed_abs id cf)
+    (fun cf id -> end_borrow_aux config meta chain allowed_abs id cf)
     cf ids
 
-and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
@@ -991,7 +991,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
              ^ " as it is set as non-endable");
 
       (* End the parent abstractions first *)
-      let cc = end_abstractions_aux meta config chain abs.parents in
+      let cc = end_abstractions_aux config meta chain abs.parents in
       let cc =
         comp_unit cc (fun ctx ->
             log#ldebug
@@ -1003,7 +1003,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       in
 
       (* End the loans inside the abstraction *)
-      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans config meta chain abs_id) in
       let cc =
         comp_unit cc (fun ctx ->
             log#ldebug
@@ -1014,7 +1014,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       in
 
       (* End the abstraction itself by redistributing the borrows it contains *)
-      let cc = comp cc (end_abstraction_borrows meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_borrows config meta chain abs_id) in
 
       (* End the regions owned by the abstraction - note that we don't need to
        * relookup the abstraction: the set of regions in an abstraction never
@@ -1030,7 +1030,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       (* Remove all the references to the id of the current abstraction, and remove
        * the abstraction itself.
        * **Rk.**: this is where we synthesize the updated symbolic AST *)
-      let cc = comp cc (end_abstraction_remove_from_context meta config abs_id) in
+      let cc = comp cc (end_abstraction_remove_from_context config meta abs_id) in
 
       (* Debugging *)
       let cc =
@@ -1052,7 +1052,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
       (* Apply the continuation *)
       cc cf ctx
 
-and end_abstractions_aux (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstractions_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_ids : AbstractionId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the abstraction ids,
@@ -1060,10 +1060,10 @@ and end_abstractions_aux (meta : Meta.meta) (config : config) (chain : borrow_or
    * a matter of taste, and may make debugging easier *)
   let abs_ids = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
   List.fold_left
-    (fun cf id -> end_abstraction_aux meta config chain id cf)
+    (fun cf id -> end_abstraction_aux config meta chain id cf)
     cf abs_ids
 
-and end_abstraction_loans (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_loans (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Lookup the abstraction *)
@@ -1081,23 +1081,23 @@ and end_abstraction_loans (meta : Meta.meta) (config : config) (chain : borrow_o
       (* There are loans: end the corresponding borrows, then recheck *)
       let cc : cm_fun =
         match bids with
-        | Borrow bid -> end_borrow_aux meta config chain None bid
-        | Borrows bids -> end_borrows_aux meta config chain None bids
+        | Borrow bid -> end_borrow_aux config meta chain None bid
+        | Borrows bids -> end_borrows_aux config meta chain None bids
       in
       (* Reexplore, looking for loans *)
-      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans config meta chain abs_id) in
       (* Continue *)
       cc cf ctx
   | Some (SymbolicValue sv) ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
        * which intersect this proj_loans, then end the proj_loans itself *)
-      let cc = end_proj_loans_symbolic meta config chain abs_id abs.regions sv in
+      let cc = end_proj_loans_symbolic config meta chain abs_id abs.regions sv in
       (* Reexplore, looking for loans *)
-      let cc = comp cc (end_abstraction_loans meta config chain abs_id) in
+      let cc = comp cc (end_abstraction_loans config meta chain abs_id) in
       (* Continue *)
       cc cf ctx
 
-and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   log#ldebug
@@ -1185,13 +1185,13 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
             (* Give the value back *)
             let sv = mk_typed_value_from_symbolic_value sv in
-            give_back_value meta config bid sv ctx
+            give_back_value config meta bid sv ctx
         | ASharedBorrow bid ->
             (* Replace the shared borrow to account for the fact it ended *)
             let ended_borrow = ABorrow AEndedSharedBorrow in
             let ctx = update_aborrow meta ek_all bid ended_borrow ctx in
             (* Give back *)
-            give_back_shared meta config bid ctx
+            give_back_shared config meta bid ctx
         | AProjSharedBorrow asb ->
             (* Retrieve the borrow ids *)
             let bids =
@@ -1210,7 +1210,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             (* Give back the shared borrows *)
             let ctx =
               List.fold_left
-                (fun ctx bid -> give_back_shared meta config bid ctx)
+                (fun ctx bid -> give_back_shared config meta bid ctx)
                 ctx bids
             in
             (* Continue *)
@@ -1220,7 +1220,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             craise meta "Unexpected"
       in
       (* Reexplore *)
-      end_abstraction_borrows meta config chain abs_id cf ctx
+      end_abstraction_borrows config meta chain abs_id cf ctx
   (* There are symbolic borrows: end them, then reexplore *)
   | FoundAProjBorrows (sv, proj_ty) ->
       log#ldebug
@@ -1234,10 +1234,10 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
       let ctx = update_aproj_borrows meta abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
-        give_back_symbolic_value meta config abs.regions proj_ty sv nsv ctx
+        give_back_symbolic_value config meta abs.regions proj_ty sv nsv ctx
       in
       (* Reexplore *)
-      end_abstraction_borrows meta config chain abs_id cf ctx
+      end_abstraction_borrows config meta chain abs_id cf ctx
   (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *)
   | FoundBorrowContent bc ->
       log#ldebug
@@ -1255,7 +1255,7 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             | Error _ -> craise meta "Unreachable"
             | Ok (ctx, _) ->
                 (* Give back *)
-                give_back_shared meta config bid ctx)
+                give_back_shared config meta bid ctx)
         | VMutBorrow (bid, v) -> (
             (* Replace the mut borrow with bottom *)
             let allow_inner_loans = false in
@@ -1266,14 +1266,14 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
             | Ok (ctx, _) ->
                 (* Give the value back - note that the mut borrow was below a
                  * shared borrow: the value is thus unchanged *)
-                give_back_value meta config bid v ctx)
+                give_back_value config meta bid v ctx)
         | VReservedMutBorrow _ -> craise meta "Unreachable"
       in
       (* Reexplore *)
-      end_abstraction_borrows meta config chain abs_id cf ctx
+      end_abstraction_borrows config meta chain abs_id cf ctx
 
 (** Remove an abstraction from the context, as well as all its references *)
-and end_abstraction_remove_from_context (meta : Meta.meta)  (_config : config)
+and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta)
     (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   let ctx, abs = ctx_remove_abs meta ctx abs_id in
@@ -1297,7 +1297,7 @@ and end_abstraction_remove_from_context (meta : Meta.meta)  (_config : config)
         intersecting proj_borrows, either in the concrete context or in an
         abstraction
 *)
-and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow_or_abs_ids)
+and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
     (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value)
     : cm_fun =
  fun cf ctx ->
@@ -1360,7 +1360,7 @@ and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow
             AbstractionId.Set.empty abs_ids
         in
         (* End the abstractions and continue *)
-        end_abstractions_aux meta config chain abs_ids cf ctx
+        end_abstractions_aux config meta chain abs_ids cf ctx
       in
       (* End the internal borrows projectors and the loans projector *)
       let cf_end_internal : cm_fun =
@@ -1413,35 +1413,35 @@ and end_proj_loans_symbolic (meta : Meta.meta) (config : config) (chain : borrow
         cf ctx)
       else
         (* The borrows proj comes from a different abstraction: end it. *)
-        let cc = end_abstraction_aux meta config chain abs_id' in
+        let cc = end_abstraction_aux config meta chain abs_id' in
         (* Retry ending the projector of loans *)
         let cc =
-          comp cc (end_proj_loans_symbolic meta config chain abs_id regions sv)
+          comp cc (end_proj_loans_symbolic config meta chain abs_id regions sv)
         in
         (* Sanity check *)
         let cc = comp cc cf_check in
         (* Continue *)
         cc cf ctx
 
-let end_borrow (meta : Meta.meta ) config : BorrowId.id -> cm_fun = end_borrow_aux meta config [] None
+let end_borrow config (meta : Meta.meta ) : BorrowId.id -> cm_fun = end_borrow_aux config meta [] None
 
-let end_borrows (meta : Meta.meta ) config : BorrowId.Set.t -> cm_fun =
-  end_borrows_aux meta config [] None
+let end_borrows config (meta : Meta.meta ) : BorrowId.Set.t -> cm_fun =
+  end_borrows_aux config meta [] None
 
-let end_abstraction meta config = end_abstraction_aux meta config []
-let end_abstractions meta config = end_abstractions_aux meta config []
+let end_abstraction config meta = end_abstraction_aux config meta []
+let end_abstractions config meta = end_abstractions_aux config meta []
 
-let end_borrow_no_synth meta config id ctx =
-  get_cf_ctx_no_synth meta (end_borrow meta config id) ctx
+let end_borrow_no_synth config meta id ctx =
+  get_cf_ctx_no_synth meta (end_borrow config meta id) ctx
 
-let end_borrows_no_synth meta config ids ctx =
-  get_cf_ctx_no_synth meta (end_borrows meta config ids) ctx
+let end_borrows_no_synth config meta ids ctx =
+  get_cf_ctx_no_synth meta (end_borrows config meta ids) ctx
 
-let end_abstraction_no_synth meta config id ctx =
-  get_cf_ctx_no_synth meta (end_abstraction meta config id) ctx
+let end_abstraction_no_synth config meta id ctx =
+  get_cf_ctx_no_synth meta (end_abstraction config meta id) ctx
 
-let end_abstractions_no_synth meta config ids ctx =
-  get_cf_ctx_no_synth meta (end_abstractions meta config ids) ctx
+let end_abstractions_no_synth config meta ids ctx =
+  get_cf_ctx_no_synth meta (end_abstractions config meta ids) ctx
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
@@ -1532,7 +1532,7 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
   cf ctx
 
 (** Promote a reserved mut borrow to a mut borrow. *)
-let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : BorrowId.id) : cm_fun
+let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : BorrowId.id) : cm_fun
     =
  fun cf ctx ->
   (* Lookup the value *)
@@ -1550,11 +1550,11 @@ let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : Bo
           (* End the loans *)
           let cc =
             match lc with
-            | VSharedLoan (bids, _) -> end_borrows meta config bids
-            | VMutLoan bid -> end_borrow meta config bid
+            | VSharedLoan (bids, _) -> end_borrows config meta bids
+            | VMutLoan bid -> end_borrow config meta bid
           in
           (* Recursive call *)
-          let cc = comp cc (promote_reserved_mut_borrow meta config l) in
+          let cc = comp cc (promote_reserved_mut_borrow config meta l) in
           (* Continue *)
           cc cf ctx
       | None ->
@@ -1570,7 +1570,7 @@ let rec promote_reserved_mut_borrow (meta : Meta.meta) (config : config) (l : Bo
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = BorrowId.Set.remove l bids in
-          let cc = end_borrows meta config bids in
+          let cc = end_borrows config meta bids in
           (* Promote the loan - TODO: this will fail if the value contains
            * any loans. In practice, it shouldn't, but we could also
            * look for loans inside the value and end them before promoting
-- 
cgit v1.2.3


From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 27 Mar 2024 10:22:06 +0100
Subject: Added sanity_check and sanity_check_opt_meta helpers and changed
 sanity checks related cassert to these helpers to have a proper error message

---
 compiler/InterpreterBorrows.ml | 54 +++++++++++++++++++++---------------------
 1 file changed, 27 insertions(+), 27 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index c7df2eca..ab2639ad 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -248,8 +248,8 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
 let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv : typed_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
-  cassert (not (loans_in_value nv)) meta "TODO: error message";
-  cassert (not (bottom_in_value ctx.ended_regions nv)) meta "TODO: error message";
+  sanity_check (not (loans_in_value nv)) meta;
+  sanity_check (not (bottom_in_value ctx.ended_regions nv)) meta;
   (* Debug *)
   log#ldebug
     (lazy
@@ -444,7 +444,7 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions
     (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
-  cassert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta "TODO: error message";
+  sanity_check (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta;
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -559,7 +559,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (
                * we don't register the fact that we inserted the value somewhere
                * (i.e., we don't call {!set_replaced}) *)
               (* Sanity check *)
-              cassert (nv.ty = ty) meta "TODO: error message";
+              sanity_check (nv.ty = ty) meta;
               ALoan
                 (AEndedIgnoredMutLoan
                    { given_back = nv; child; given_back_meta = nsv }))
@@ -758,24 +758,24 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_bor
   match bc with
   | Concrete (VMutBorrow (l', tv)) ->
       (* Sanity check *)
-      cassert (l' = l) meta "TODO: error message";
-      cassert (not (loans_in_value tv)) meta "TODO: error message";
+      sanity_check (l' = l) meta;
+      sanity_check (not (loans_in_value tv)) meta;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
+      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Update the context *)
       give_back_value config meta l tv ctx
   | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
       (* Sanity check *)
-      cassert (l' = l) meta "TODO: error message";
+      sanity_check (l' = l) meta;
       (* Check that the borrow is somewhere - purely a sanity check *)
-      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
+      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract (AMutBorrow (l', av)) ->
       (* Sanity check *)
-      cassert (l' = l) meta "TODO: error message";
+      sanity_check (l' = l) meta;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The corresponding loan should be somewhere";
+      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Convert the avalue to a (fresh symbolic) value.
 
          Rem.: we shouldn't do this here. We should do this in a function
@@ -788,14 +788,14 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_bor
         ctx
   | Abstract (ASharedBorrow l') ->
       (* Sanity check *)
-      cassert (l' = l) meta "TODO: error message";
+      sanity_check (l' = l) meta;
       (* Check that the borrow is somewhere - purely a sanity check *)
-      cassert (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta "The borrow should be somewhere";
+      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract (AProjSharedBorrow asb) ->
       (* Sanity check *)
-      cassert (borrow_in_asb l asb) meta "TODO: error message";
+      sanity_check (borrow_in_asb l asb) meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract
@@ -931,7 +931,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a
       (* Sanity check: the borrowed value shouldn't contain loans *)
       (match bc with
       | Concrete (VMutBorrow (_, bv)) ->
-          cassert (Option.is_none (get_first_loan_in_value bv)) meta "Borrowed value shouldn't contain loans"
+          sanity_check (Option.is_none (get_first_loan_in_value bv)) meta
       | _ -> ());
       (* Give back the value *)
       let ctx = give_back config meta l bc ctx in
@@ -1402,9 +1402,9 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow
          * replace it with... Maybe we should introduce an ABottomProj? *)
         let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in
         (* Sanity check: no other occurrence of an intersecting projector of borrows *)
-        cassert (
+        sanity_check (
           Option.is_none
-            (lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx)) meta "no other occurrence of an intersecting projector of borrows";
+            (lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx)) meta ;
         (* End the projector of loans *)
         let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
         (* Sanity check *)
@@ -1483,7 +1483,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
       (* We need to check that there aren't any loans in the value:
          we should have gotten rid of those already, but it is better
          to do a sanity check. *)
-      cassert (not (loans_in_value sv)) meta "There shouldn't be any loans in the value";
+      sanity_check (not (loans_in_value sv)) meta;
       (* Check there isn't {!Bottom} (this is actually an invariant *)
       cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a !Bottom";
       (* Check there aren't reserved borrows *)
@@ -1564,9 +1564,9 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : Bo
             (lazy
               ("activate_reserved_mut_borrow: resulting value:\n"
               ^ typed_value_to_string meta ctx sv));
-          cassert (not (loans_in_value sv)) meta "TODO: error message";
-          cassert (not (bottom_in_value ctx.ended_regions sv)) meta "TODO: error message";
-          cassert (not (reserved_in_value sv)) meta "TODO: error message";
+          sanity_check (not (loans_in_value sv)) meta;
+          sanity_check (not (bottom_in_value ctx.ended_regions sv)) meta;
+          sanity_check (not (reserved_in_value sv)) meta;
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = BorrowId.Set.remove l bids in
@@ -1664,7 +1664,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             list_avalues false push_fail child_av)
     | ABorrow bc -> (
         (* Sanity check - rem.: may be redundant with [push_fail] *)
-        cassert allow_borrows meta "TODO: error message";
+        sanity_check allow_borrows meta;
         (* Explore the borrow content *)
         match bc with
         | AMutBorrow (bid, child_av) ->
@@ -1854,7 +1854,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
         let _, ref_ty, kind = ty_as_ref ty in
         cassert (ty_no_regions ref_ty) meta "TODO: error message";
         (* Sanity check *)
-        cassert allow_borrows meta "TODO: error message";
+        sanity_check allow_borrows meta;
         (* Convert the borrow content *)
         match bc with
         | VSharedBorrow bid ->
@@ -2068,7 +2068,7 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : ab
 
       method! visit_symbolic_value _ sv =
         (* Sanity check: no borrows *)
-        cassert (not (symbolic_value_has_borrows ctx sv)) meta "TODO: error message" 
+        sanity_check (not (symbolic_value_has_borrows ctx sv)) meta 
     end
   in
 
@@ -2173,8 +2173,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
   if merge_funs = None then (
-    cassert (BorrowId.Set.disjoint borrows0 borrows1) meta "TODO: error message";
-    cassert (BorrowId.Set.disjoint loans0 loans1)) meta "TODO: error message";
+    sanity_check (BorrowId.Set.disjoint borrows0 borrows1) meta;
+    sanity_check (BorrowId.Set.disjoint loans0 loans1)) meta;
 
   (* Merge.
      There are several cases:
@@ -2476,7 +2476,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
   in
 
   (* Sanity check *)
-  if !Config.sanity_checks then cassert (abs_is_destructured meta true ctx abs) meta "TODO: error message";
+  if !Config.sanity_checks then sanity_check (abs_is_destructured meta true ctx abs) meta;
   (* Return *)
   abs
 
-- 
cgit v1.2.3


From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 13:56:31 +0100
Subject: Should answer all comments, there are still some TODO: error message
 left

---
 compiler/InterpreterBorrows.ml | 132 ++++++++++++++++++++---------------------
 1 file changed, 66 insertions(+), 66 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index ab2639ad..c1cf8441 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -42,7 +42,7 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
   in
   let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content)
       =
-    cassert (Option.is_none !replaced_bc) meta "TODO: error message";
+    sanity_check (Option.is_none !replaced_bc) meta;
     replaced_bc := Some (abs_id, bc)
   in
   (* Raise an exception if:
@@ -224,8 +224,8 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
       method! visit_abs outer abs =
         (* Update the outer abs *)
         let outer_abs, outer_borrows = outer in
-        cassert (Option.is_none outer_abs) meta "TODO: error message";
-        cassert (Option.is_none outer_borrows) meta "TODO: error message";
+        sanity_check (Option.is_none outer_abs) meta;
+        sanity_check (Option.is_none outer_borrows) meta;
         let outer = (Some abs.abs_id, None) in
         super#visit_abs outer abs
     end
@@ -248,18 +248,18 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
 let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv : typed_value)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
-  sanity_check (not (loans_in_value nv)) meta;
-  sanity_check (not (bottom_in_value ctx.ended_regions nv)) meta;
+  exec_assert (not (loans_in_value nv)) meta "Can not end a borrow because the value to give back contains bottom";
+  exec_assert (not (bottom_in_value ctx.ended_regions nv)) meta "Can not end a borrow because the value to give back contains bottom";
   (* Debug *)
   log#ldebug
     (lazy
       ("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: "
-      ^ typed_value_to_string meta ctx nv
-      ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+      ^ typed_value_to_string ~meta:(Some meta) ctx nv
+      ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    cassert (not !replaced) meta "Exactly one loan should have been updated";
+    sanity_check (not !replaced) meta;
     replaced := true
   in
   (* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
@@ -427,7 +427,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv
         (* We remember in which abstraction we are before diving -
          * this is necessary for projecting values: we need to know
          * over which regions to project *)
-        cassert (Option.is_none opt_abs) meta "TODO: error message";
+        sanity_check (Option.is_none opt_abs) meta;
         super#visit_EAbs (Some abs) abs
     end
   in
@@ -466,7 +466,7 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions
          type [T]! We thus *mustn't* introduce a projector here.
       *)
       (* AProjBorrows (nsv, sv.sv_ty) *)
-      craise meta "TODO: error message"
+      internal_error meta
     in
     AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
@@ -671,7 +671,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B
   (* Keep track of changes *)
   let r = ref false in
   let set_ref () =
-    cassert (not !r) meta "TODO: error message";
+    sanity_check (not !r) meta;
     r := true
   in
 
@@ -701,7 +701,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B
 
   let env = obj#visit_env () ctx.env in
   (* Check that we reborrowed once *)
-  cassert !r meta "Not reborrowed once";
+  sanity_check !r meta;
   { ctx with env }
 
 (** Convert an {!type:avalue} to a {!type:value}.
@@ -746,11 +746,11 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_bor
     (lazy
       (let bc =
          match bc with
-         | Concrete bc -> borrow_content_to_string meta ctx bc
-         | Abstract bc -> aborrow_content_to_string meta ctx bc
+         | Concrete bc -> borrow_content_to_string ~meta:(Some meta) ctx bc
+         | Abstract bc -> aborrow_content_to_string ~meta:(Some meta) ctx bc
        in
        "give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc
-       ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+       ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
   (* This is used for sanity checks *)
   let sanity_ek =
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -814,8 +814,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
             (lazy
               (fun_name ^ ": " ^ BorrowId.to_string l
              ^ ": borrow didn't disappear:\n- original context:\n"
-             ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n"
-             ^ eval_ctx_to_string meta ctx));
+             ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n"
+             ^ eval_ctx_to_string ~meta:(Some meta) ctx));
           craise meta "Borrow not eliminated"
     in
     match lookup_loan_opt meta ek_all l ctx with
@@ -825,8 +825,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
           (lazy
             (fun_name ^ ": " ^ BorrowId.to_string l
            ^ ": loan didn't disappear:\n- original context:\n"
-           ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n"
-           ^ eval_ctx_to_string meta ctx));
+           ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n"
+           ^ eval_ctx_to_string ~meta:(Some meta) ctx));
         craise meta "Loan not eliminated"
   in
   unit_to_cm_fun check_disappeared
@@ -863,7 +863,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a
   log#ldebug
     (lazy
       ("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n"
-     ^ eval_ctx_to_string meta ctx));
+     ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
   (* Utility function for the sanity checks: check that the borrow disappeared
    * from the context *)
@@ -922,7 +922,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a
       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 *)
-      cassert (config.mode = SymbolicMode) meta "Borrow should be in symbolic mode";
+      sanity_check (config.mode = SymbolicMode) meta;
       (* Do a sanity check and continue *)
       cf_check cf ctx
   (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update
@@ -966,7 +966,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
     (lazy
       ("end_abstraction_aux: "
       ^ AbstractionId.to_string abs_id
-      ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0));
+      ^ "\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0));
 
   (* Lookup the abstraction - note that if we end a list of abstractions,
      ending one abstraction may lead to the current abstraction having
@@ -999,7 +999,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
                 ^ "\n- context after parent abstractions ended:\n"
-                ^ eval_ctx_to_string meta ctx)))
+                ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
       in
 
       (* End the loans inside the abstraction *)
@@ -1010,7 +1010,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
               (lazy
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
-                ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string meta ctx)))
+                ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
       in
 
       (* End the abstraction itself by redistributing the borrows it contains *)
@@ -1039,8 +1039,8 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
               (lazy
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
-                ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0
-                ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx)))
+                ^ "\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+                ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
       in
 
       (* Sanity check: ending an abstraction must preserve the invariants *)
@@ -1173,7 +1173,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow
       log#ldebug
         (lazy
           ("end_abstraction_borrows: found aborrow content: "
-          ^ aborrow_content_to_string meta ctx bc));
+          ^ aborrow_content_to_string ~meta:(Some meta) ctx bc));
       let ctx =
         match bc with
         | AMutBorrow (bid, av) ->
@@ -1243,7 +1243,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow
       log#ldebug
         (lazy
           ("end_abstraction_borrows: found borrow content: "
-          ^ borrow_content_to_string meta ctx bc));
+          ^ borrow_content_to_string ~meta:(Some meta) ctx bc));
       let ctx =
         match bc with
         | VSharedBorrow bid -> (
@@ -1466,7 +1466,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
   log#ldebug
     (lazy
       ("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l
-     ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+     ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
   (* Lookup the shared loan - note that we can't promote a shared loan
    * in a shared value, but we can do it in a mutably borrowed value.
    * This is important because we can do: [let y = &two-phase ( *x );]
@@ -1485,9 +1485,9 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
          to do a sanity check. *)
       sanity_check (not (loans_in_value sv)) meta;
       (* Check there isn't {!Bottom} (this is actually an invariant *)
-      cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a !Bottom";
+      cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a bottom";
       (* Check there aren't reserved borrows *)
-      cassert (not (reserved_in_value sv)) meta "There shouldn't have reserved borrows";
+      cassert (not (reserved_in_value sv)) meta "There shouldn't be reserved borrows";
       (* Update the loan content *)
       let ctx = update_loan meta ek l (VMutLoan l) ctx in
       (* Continue *)
@@ -1563,7 +1563,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : Bo
           log#ldebug
             (lazy
               ("activate_reserved_mut_borrow: resulting value:\n"
-              ^ typed_value_to_string meta ctx sv));
+              ^ typed_value_to_string ~meta:(Some meta) ctx sv));
           sanity_check (not (loans_in_value sv)) meta;
           sanity_check (not (bottom_in_value ctx.ended_regions sv)) meta;
           sanity_check (not (reserved_in_value sv)) meta;
@@ -1649,7 +1649,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
         | AIgnoredMutLoan (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
             cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
-            cassert (opt_bid = None) meta "TODO: error message";
+            sanity_check (opt_bid = None) meta;
             (* Simply explore the child *)
             list_avalues false push_fail child_av
         | AEndedMutLoan
@@ -1680,7 +1680,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
         | AIgnoredMutBorrow (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
             cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
-            cassert (opt_bid = None) meta "TODO: error message";
+            sanity_check (opt_bid = None) meta;
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AEndedIgnoredMutBorrow
@@ -1703,7 +1703,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     | ASymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message"
+        sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta
   and list_values (v : typed_value) : typed_avalue list * typed_value =
     let ty = v.ty in
     match v.value with
@@ -1725,9 +1725,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             let avl, sv = list_values sv in
             if destructure_shared_values then (
               (* Rem.: the shared value can't contain loans nor borrows *)
-              cassert (ty_no_regions ty) meta "The shared value can't contain loans nor borrows";
+              cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
               let av : typed_avalue =
-                cassert (not (value_has_loans_or_borrows ctx sv.value)) meta "The shared value can't contain loans nor borrows";
+                sanity_check (not (value_has_loans_or_borrows ctx sv.value)) meta;
                 (* We introduce fresh ids for the symbolic values *)
                 let mk_value_with_fresh_sids (v : typed_value) : typed_value =
                   let visitor =
@@ -1752,7 +1752,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     | VSymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message";
+        sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta;
         ([], v)
   in
 
@@ -1808,7 +1808,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
     log#ldebug
       (lazy
         ("convert_value_to_abstractions: to_avalues:\n- value: "
-        ^ typed_value_to_string meta ctx v));
+        ^ typed_value_to_string ~meta:(Some meta) ctx v));
 
     let ty = v.ty in
     match v.value with
@@ -1852,13 +1852,13 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
         (avl, { v with value = VAdt adt })
     | VBorrow bc -> (
         let _, ref_ty, kind = ty_as_ref ty in
-        cassert (ty_no_regions ref_ty) meta "TODO: error message";
+        cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet";
         (* Sanity check *)
         sanity_check allow_borrows meta;
         (* Convert the borrow content *)
         match bc with
         | VSharedBorrow bid ->
-            cassert (ty_no_regions ref_ty) meta "TODO: error message";
+            cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet";
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let value = ABorrow (ASharedBorrow bid) in
             ([ { value; ty } ], v)
@@ -1887,7 +1887,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
             cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert (ty_no_regions ty) meta "TODO: error message";
+            cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RShared in
             let ignored = mk_aignored meta ty in
             (* Rem.: the shared value might contain loans *)
@@ -1905,7 +1905,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
         | VMutLoan bid ->
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert (ty_no_regions ty) meta "TODO: error message";
+            cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RMut in
             let ignored = mk_aignored meta ty in
             let av = ALoan (AMutLoan (bid, ignored)) in
@@ -1914,7 +1914,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
     | VSymbolic _ ->
         (* For now, we force all the symbolic values containing borrows to
            be eagerly expanded, and we don't support nested borrows *)
-        cassert (not (value_has_borrows ctx v.value)) meta "TODO: error message";
+        cassert (not (value_has_borrows ctx v.value)) meta "Nested borrows are not supported yet";
         (* Return nothing *)
         ([], v)
   in
@@ -1968,26 +1968,26 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : ab
   in
 
   let push_loans ids (lc : g_loan_content_with_ty) : unit =
-    cassert (BorrowId.Set.disjoint !loans ids) meta "TODO: error message";
+    sanity_check (BorrowId.Set.disjoint !loans ids) meta;
     loans := BorrowId.Set.union !loans ids;
     BorrowId.Set.iter
       (fun id ->
-        cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
+        sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta;
         loan_to_content := BorrowId.Map.add id lc !loan_to_content;
         borrows_loans := LoanId id :: !borrows_loans)
       ids
   in
   let push_loan id (lc : g_loan_content_with_ty) : unit =
-    cassert (not (BorrowId.Set.mem id !loans)) meta "TODO: error message";
+    sanity_check (not (BorrowId.Set.mem id !loans)) meta;
     loans := BorrowId.Set.add id !loans;
-    cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
+    sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta;
     loan_to_content := BorrowId.Map.add id lc !loan_to_content;
     borrows_loans := LoanId id :: !borrows_loans
   in
   let push_borrow id (bc : g_borrow_content_with_ty) : unit =
-    cassert (not (BorrowId.Set.mem id !borrows)) meta "TODO: error message";
+    sanity_check (not (BorrowId.Set.mem id !borrows)) meta;
     borrows := BorrowId.Set.add id !borrows;
-    cassert (not (BorrowId.Map.mem id !borrow_to_content)) meta "TODO: error message";
+    sanity_check (not (BorrowId.Map.mem id !borrow_to_content)) meta;
     borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
     borrows_loans := BorrowId id :: !borrows_loans
   in
@@ -2146,8 +2146,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
   (* Check that the abstractions are destructured *)
   if !Config.sanity_checks then (
     let destructure_shared_values = true in
-    cassert (abs_is_destructured meta destructure_shared_values ctx abs0) meta "Abstractions should be destructured";
-    cassert (abs_is_destructured meta destructure_shared_values ctx abs1) meta "Abstractions should be destructured");
+    sanity_check (abs_is_destructured meta destructure_shared_values ctx abs0) meta;
+    sanity_check (abs_is_destructured meta destructure_shared_values ctx abs1) meta);
 
   (* Compute the relevant information *)
   let {
@@ -2201,7 +2201,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
     log#ldebug
       (lazy
         ("merge_into_abstraction_aux: push_avalue: "
-        ^ typed_avalue_to_string meta ctx av));
+        ^ typed_avalue_to_string ~meta:(Some meta) ctx av));
     avalues := av :: !avalues
   in
   let push_opt_avalue av =
@@ -2215,7 +2215,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
   in
   let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t =
     let bids = BorrowId.Set.diff bids intersect in
-    cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
+    sanity_check (not (BorrowId.Set.is_empty bids)) meta;
     bids
   in
   let filter_bid (bid : BorrowId.id) : BorrowId.id option =
@@ -2278,7 +2278,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
         (* Check that the sets of ids are the same - if it is not the case, it
            means we actually need to merge more than 2 avalues: we ignore this
            case for now *)
-        cassert (BorrowId.Set.equal ids0 ids1) meta "Ids are not the same - Case ignored for now";
+        sanity_check (BorrowId.Set.equal ids0 ids1) meta;
         let ids = ids0 in
         if BorrowId.Set.is_empty ids then (
           (* If the set of ids is empty, we can eliminate this shared loan.
@@ -2290,10 +2290,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
              to preserve (in practice it works because we destructure the
              shared values in the abstractions, and forbid nested borrows).
           *)
-          cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
-          cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
-          cassert (is_aignored child0.value) meta "TODO: error message";
-          cassert (is_aignored child1.value) meta "TODO: error message";
+          sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+          sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+          sanity_check (is_aignored child0.value) meta;
+          sanity_check (is_aignored child1.value) meta;
           None)
         else (
           (* Register the loan ids *)
@@ -2365,7 +2365,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
                           craise meta "Unreachable"
                       | Abstract (ty, bc) -> { value = ABorrow bc; ty })
                   | Some bc0, Some bc1 ->
-                      cassert (merge_funs <> None) meta "TODO: error message";
+                      sanity_check (merge_funs <> None) meta;
                       merge_g_borrow_contents bc0 bc1
                   | None, None -> craise meta "Unreachable"
                 in
@@ -2405,10 +2405,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
                           match lc with
                           | ASharedLoan (bids, sv, child) ->
                               let bids = filter_bids bids in
-                              cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
-                              cassert (is_aignored child.value) meta "TODO: error message";
-                              cassert (
-                                not (value_has_loans_or_borrows ctx sv.value)) meta "TODO: error message";
+                              sanity_check (not (BorrowId.Set.is_empty bids)) meta;
+                              sanity_check (is_aignored child.value) meta;
+                              sanity_check (
+                                not (value_has_loans_or_borrows ctx sv.value)) meta;
                               let lc = ASharedLoan (bids, sv, child) in
                               set_loans_as_merged bids;
                               Some { value = ALoan lc; ty }
@@ -2421,7 +2421,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
                               (* The abstraction has been destructured, so those shouldn't appear *)
                               craise meta "Unreachable"))
                   | Some lc0, Some lc1 ->
-                      cassert (merge_funs <> None) meta "TODO: error message";
+                      sanity_check (merge_funs <> None) meta;
                       merge_g_loan_contents lc0 lc1
                   | None, None -> craise meta "Unreachable"
                 in
@@ -2476,7 +2476,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
   in
 
   (* Sanity check *)
-  if !Config.sanity_checks then sanity_check (abs_is_destructured meta true ctx abs) meta;
+  sanity_check (abs_is_destructured meta true ctx abs) meta;
   (* Return *)
   abs
 
-- 
cgit v1.2.3


From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 17:14:27 +0100
Subject: formatting

---
 compiler/InterpreterBorrows.ml | 317 +++++++++++++++++++++++++----------------
 1 file changed, 194 insertions(+), 123 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index c1cf8441..2ccf2d5d 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -30,8 +30,9 @@ let log = Logging.borrows_log
       loans. This is used to merge borrows with abstractions, to compute loop
       fixed points for instance.
 *)
-let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id option)
-    (allow_inner_loans : bool) (l : BorrowId.id) (ctx : eval_ctx) :
+let end_borrow_get_borrow (meta : Meta.meta)
+    (allowed_abs : AbstractionId.id option) (allow_inner_loans : bool)
+    (l : BorrowId.id) (ctx : eval_ctx) :
     ( eval_ctx * (AbstractionId.id option * g_borrow_content) option,
       priority_borrows_or_abs )
     result =
@@ -245,17 +246,23 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
     give the value back.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv : typed_value)
-    (ctx : eval_ctx) : eval_ctx =
+let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
+    (nv : typed_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
-  exec_assert (not (loans_in_value nv)) meta "Can not end a borrow because the value to give back contains bottom";
-  exec_assert (not (bottom_in_value ctx.ended_regions nv)) meta "Can not end a borrow because the value to give back contains bottom";
+  exec_assert
+    (not (loans_in_value nv))
+    meta "Can not end a borrow because the value to give back contains bottom";
+  exec_assert
+    (not (bottom_in_value ctx.ended_regions nv))
+    meta "Can not end a borrow because the value to give back contains bottom";
   (* Debug *)
   log#ldebug
     (lazy
       ("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: "
       ^ typed_value_to_string ~meta:(Some meta) ctx nv
-      ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
+      ^ "\n- context:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ "\n"));
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -382,8 +389,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv
               let given_back_meta = nv in
               (* Apply the projection *)
               let given_back =
-                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
-                  regions ancestors_regions nv borrowed_value_aty
+                apply_proj_borrows meta check_symbolic_no_ended ctx
+                  fresh_reborrow regions ancestors_regions nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
@@ -409,8 +416,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv
                * we don't register the fact that we inserted the value somewhere
                * (i.e., we don't call {!set_replaced}) *)
               let given_back =
-                apply_proj_borrows meta check_symbolic_no_ended ctx fresh_reborrow
-                  regions ancestors_regions nv borrowed_value_aty
+                apply_proj_borrows meta check_symbolic_no_ended ctx
+                  fresh_reborrow regions ancestors_regions nv borrowed_value_aty
               in
               (* Continue giving back in the child value *)
               let child = super#visit_typed_avalue opt_abs child in
@@ -440,9 +447,9 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv
   apply_registered_reborrows ctx
 
 (** Give back a *modified* symbolic value. *)
-let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions : RegionId.Set.t)
-    (proj_ty : rty) (sv : symbolic_value) (nsv : symbolic_value)
-    (ctx : eval_ctx) : eval_ctx =
+let give_back_symbolic_value (_config : config) (meta : Meta.meta)
+    (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value)
+    (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
   sanity_check (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta;
   (* Store the given-back value as a meta-value for synthesis purposes *)
@@ -485,8 +492,9 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions
     end abstraction when ending this abstraction. When doing this, we need
     to convert the {!avalue} to a {!type:value} by introducing the proper symbolic values.
  *)
-let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (bid : BorrowId.id)
-    (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx) : eval_ctx =
+let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
+    (bid : BorrowId.id) (nv : typed_avalue) (nsv : typed_value) (ctx : eval_ctx)
+    : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -588,7 +596,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) (
     we update.
     TODO: this was not the case before, so some sanity checks are not useful anymore.
  *)
-let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
+let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
+    (ctx : eval_ctx) : eval_ctx =
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
@@ -666,8 +675,8 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id) (ctx : eval_
     to an environment by inserting a new borrow id in the set of borrows tracked
     by a shared value, referenced by the [original_bid] argument.
  *)
-let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : BorrowId.id)
-    (ctx : eval_ctx) : eval_ctx =
+let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id)
+    (new_bid : BorrowId.id) (ctx : eval_ctx) : eval_ctx =
   (* Keep track of changes *)
   let r = ref false in
   let set_ref () =
@@ -720,7 +729,8 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B
     be expanded (because expanding this symbolic value would require expanding
     a reference whose region has already ended).
  *)
-let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) : symbolic_value =
+let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) :
+    symbolic_value =
   mk_fresh_symbolic_value meta av.ty
 
 (** Auxiliary function: see {!end_borrow_aux}.
@@ -739,8 +749,8 @@ let convert_avalue_to_given_back_value (meta : Meta.meta) (av : typed_avalue) :
     borrows. This kind of internal reshuffling. should be similar to ending
     abstractions (it is tantamount to ending *sub*-abstractions).
  *)
-let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_borrow_content)
-    (ctx : eval_ctx) : eval_ctx =
+let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id)
+    (bc : g_borrow_content) (ctx : eval_ctx) : eval_ctx =
   (* Debug *)
   log#ldebug
     (lazy
@@ -750,7 +760,9 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_bor
          | Abstract bc -> aborrow_content_to_string ~meta:(Some meta) ctx bc
        in
        "give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc
-       ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
+       ^ "\n- context:\n"
+       ^ eval_ctx_to_string ~meta:(Some meta) ctx
+       ^ "\n"));
   (* This is used for sanity checks *)
   let sanity_ek =
     { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -803,8 +815,8 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_bor
       | AEndedSharedBorrow ) ->
       craise meta "Unreachable"
 
-let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowId.id)
-    (ctx0 : eval_ctx) : cm_fun =
+let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
+    (l : BorrowId.id) (ctx0 : eval_ctx) : cm_fun =
   let check_disappeared (ctx : eval_ctx) : unit =
     let _ =
       match lookup_borrow_opt ek_all l ctx with
@@ -814,8 +826,9 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
             (lazy
               (fun_name ^ ": " ^ BorrowId.to_string l
              ^ ": borrow didn't disappear:\n- original context:\n"
-             ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n"
-             ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+              ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+              ^ "\n\n- new context:\n"
+              ^ eval_ctx_to_string ~meta:(Some meta) ctx));
           craise meta "Borrow not eliminated"
     in
     match lookup_loan_opt meta ek_all l ctx with
@@ -825,8 +838,9 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
           (lazy
             (fun_name ^ ": " ^ BorrowId.to_string l
            ^ ": loan didn't disappear:\n- original context:\n"
-           ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n"
-           ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+            ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+            ^ "\n\n- new context:\n"
+            ^ eval_ctx_to_string ~meta:(Some meta) ctx));
         craise meta "Loan not eliminated"
   in
   unit_to_cm_fun check_disappeared
@@ -852,8 +866,9 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
     perform anything smart and is trusted, and another function for the
     book-keeping.
  *)
-let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
-    (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun =
+let rec end_borrow_aux (config : config) (meta : Meta.meta)
+    (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option)
+    (l : BorrowId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
   let chain0 = chain in
@@ -863,7 +878,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a
   log#ldebug
     (lazy
       ("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n"
-     ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx));
 
   (* Utility function for the sanity checks: check that the borrow disappeared
    * from the context *)
@@ -942,8 +957,9 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a
       (* Compose *)
       cc cf ctx
 
-and end_borrows_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
-    (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun =
+and end_borrows_aux (config : config) (meta : Meta.meta)
+    (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option)
+    (lset : BorrowId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the borrow ids,
    * so that we actually end from the smallest id to the highest id - just
@@ -953,12 +969,13 @@ and end_borrows_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_
     (fun cf id -> end_borrow_aux config meta chain allowed_abs id cf)
     cf ids
 
-and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
-    (abs_id : AbstractionId.id) : cm_fun =
+and end_abstraction_aux (config : config) (meta : Meta.meta)
+    (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Check that we don't loop *)
   let chain =
-    add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id) chain
+    add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id)
+      chain
   in
   (* Remember the original context for printing purposes *)
   let ctx0 = ctx in
@@ -966,7 +983,8 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
     (lazy
       ("end_abstraction_aux: "
       ^ AbstractionId.to_string abs_id
-      ^ "\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0));
+      ^ "\n- original context:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx0));
 
   (* Lookup the abstraction - note that if we end a list of abstractions,
      ending one abstraction may lead to the current abstraction having
@@ -984,11 +1002,10 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
       (* Check that we can end the abstraction *)
       if abs.can_end then ()
       else
-        craise
-          meta
-             ("Can't end abstraction "
-             ^ AbstractionId.to_string abs.abs_id
-             ^ " as it is set as non-endable");
+        craise meta
+          ("Can't end abstraction "
+          ^ AbstractionId.to_string abs.abs_id
+          ^ " as it is set as non-endable");
 
       (* End the parent abstractions first *)
       let cc = end_abstractions_aux config meta chain abs.parents in
@@ -1010,7 +1027,8 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
               (lazy
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
-                ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
+                ^ "\n- context after loans ended:\n"
+                ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
       in
 
       (* End the abstraction itself by redistributing the borrows it contains *)
@@ -1030,7 +1048,9 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
       (* Remove all the references to the id of the current abstraction, and remove
        * the abstraction itself.
        * **Rk.**: this is where we synthesize the updated symbolic AST *)
-      let cc = comp cc (end_abstraction_remove_from_context config meta abs_id) in
+      let cc =
+        comp cc (end_abstraction_remove_from_context config meta abs_id)
+      in
 
       (* Debugging *)
       let cc =
@@ -1039,8 +1059,10 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
               (lazy
                 ("end_abstraction_aux: "
                 ^ AbstractionId.to_string abs_id
-                ^ "\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0
-                ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
+                ^ "\n- original context:\n"
+                ^ eval_ctx_to_string ~meta:(Some meta) ctx0
+                ^ "\n\n- new context:\n"
+                ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
       in
 
       (* Sanity check: ending an abstraction must preserve the invariants *)
@@ -1052,8 +1074,8 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
       (* Apply the continuation *)
       cc cf ctx
 
-and end_abstractions_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
-    (abs_ids : AbstractionId.Set.t) : cm_fun =
+and end_abstractions_aux (config : config) (meta : Meta.meta)
+    (chain : borrow_or_abs_ids) (abs_ids : AbstractionId.Set.t) : cm_fun =
  fun cf ->
   (* This is not necessary, but we prefer to reorder the abstraction ids,
    * so that we actually end from the smallest id to the highest id - just
@@ -1063,8 +1085,8 @@ and end_abstractions_aux (config : config) (meta : Meta.meta) (chain : borrow_or
     (fun cf id -> end_abstraction_aux config meta chain id cf)
     cf abs_ids
 
-and end_abstraction_loans (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
-    (abs_id : AbstractionId.id) : cm_fun =
+and end_abstraction_loans (config : config) (meta : Meta.meta)
+    (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   (* Lookup the abstraction *)
   let abs = ctx_lookup_abs ctx abs_id in
@@ -1091,14 +1113,16 @@ and end_abstraction_loans (config : config) (meta : Meta.meta) (chain : borrow_o
   | Some (SymbolicValue sv) ->
       (* There is a proj_loans over a symbolic value: end the proj_borrows
        * which intersect this proj_loans, then end the proj_loans itself *)
-      let cc = end_proj_loans_symbolic config meta chain abs_id abs.regions sv in
+      let cc =
+        end_proj_loans_symbolic config meta chain abs_id abs.regions sv
+      in
       (* Reexplore, looking for loans *)
       let cc = comp cc (end_abstraction_loans config meta chain abs_id) in
       (* Continue *)
       cc cf ctx
 
-and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
-    (abs_id : AbstractionId.id) : cm_fun =
+and end_abstraction_borrows (config : config) (meta : Meta.meta)
+    (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun =
  fun cf ctx ->
   log#ldebug
     (lazy
@@ -1297,9 +1321,9 @@ and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta)
         intersecting proj_borrows, either in the concrete context or in an
         abstraction
 *)
-and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids)
-    (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value)
-    : cm_fun =
+and end_proj_loans_symbolic (config : config) (meta : Meta.meta)
+    (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id)
+    (regions : RegionId.Set.t) (sv : symbolic_value) : cm_fun =
  fun cf ctx ->
   (* Small helpers for sanity checks *)
   let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in
@@ -1310,7 +1334,9 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow
   in
   (* Find the first proj_borrows which intersects the proj_loans *)
   let explore_shared = true in
-  match lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx with
+  match
+    lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx
+  with
   | None ->
       (* We couldn't find any in the context: it means that the symbolic value
        * is in the concrete environment (or that we dropped it, in which case
@@ -1366,7 +1392,9 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow
       let cf_end_internal : cm_fun =
        fun cf ctx ->
         (* All the proj_borrows are owned: simply erase them *)
-        let ctx = remove_intersecting_aproj_borrows_shared meta regions sv ctx in
+        let ctx =
+          remove_intersecting_aproj_borrows_shared meta regions sv ctx
+        in
         (* End the loan itself *)
         let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
         (* Sanity check *)
@@ -1402,9 +1430,11 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow
          * replace it with... Maybe we should introduce an ABottomProj? *)
         let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in
         (* Sanity check: no other occurrence of an intersecting projector of borrows *)
-        sanity_check (
-          Option.is_none
-            (lookup_intersecting_aproj_borrows_opt meta explore_shared regions sv ctx)) meta ;
+        sanity_check
+          (Option.is_none
+             (lookup_intersecting_aproj_borrows_opt meta explore_shared regions
+                sv ctx))
+          meta;
         (* End the projector of loans *)
         let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in
         (* Sanity check *)
@@ -1423,9 +1453,10 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow
         (* Continue *)
         cc cf ctx
 
-let end_borrow config (meta : Meta.meta ) : BorrowId.id -> cm_fun = end_borrow_aux config meta [] None
+let end_borrow config (meta : Meta.meta) : BorrowId.id -> cm_fun =
+  end_borrow_aux config meta [] None
 
-let end_borrows config (meta : Meta.meta ) : BorrowId.Set.t -> cm_fun =
+let end_borrows config (meta : Meta.meta) : BorrowId.Set.t -> cm_fun =
   end_borrows_aux config meta [] None
 
 let end_abstraction config meta = end_abstraction_aux config meta []
@@ -1466,7 +1497,9 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
   log#ldebug
     (lazy
       ("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l
-     ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
+     ^ "\n- context:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx
+      ^ "\n"));
   (* Lookup the shared loan - note that we can't promote a shared loan
    * in a shared value, but we can do it in a mutably borrowed value.
    * This is important because we can do: [let y = &two-phase ( *x );]
@@ -1479,15 +1512,21 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
       craise meta "Expected a shared loan, found a mut loan"
   | _, Concrete (VSharedLoan (bids, sv)) ->
       (* Check that there is only one borrow id (l) and update the loan *)
-      cassert (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1) meta "There should only be one borrow id";
+      cassert
+        (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1)
+        meta "There should only be one borrow id";
       (* We need to check that there aren't any loans in the value:
          we should have gotten rid of those already, but it is better
          to do a sanity check. *)
       sanity_check (not (loans_in_value sv)) meta;
       (* Check there isn't {!Bottom} (this is actually an invariant *)
-      cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a bottom";
+      cassert
+        (not (bottom_in_value ctx.ended_regions sv))
+        meta "There shouldn't be a bottom";
       (* Check there aren't reserved borrows *)
-      cassert (not (reserved_in_value sv)) meta "There shouldn't be reserved borrows";
+      cassert
+        (not (reserved_in_value sv))
+        meta "There shouldn't be reserved borrows";
       (* Update the loan content *)
       let ctx = update_loan meta ek l (VMutLoan l) ctx in
       (* Continue *)
@@ -1495,18 +1534,17 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      craise
-        meta
-           "Can't promote a shared loan to a mutable loan if the loan is \
-            inside an abstraction"
+      craise meta
+        "Can't promote a shared loan to a mutable loan if the loan is inside \
+         an abstraction"
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
     This function updates a shared borrow to a mutable borrow (and that is
     all: it doesn't touch the corresponding loan).
  *)
-let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) (cf : m_fun)
-    (borrowed_value : typed_value) : m_fun =
+let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
+    (cf : m_fun) (borrowed_value : typed_value) : m_fun =
  fun ctx ->
   (* Lookup the reserved borrow - note that we don't go inside borrows/loans:
      there can't be reserved borrows inside other borrows/loans
@@ -1523,17 +1561,16 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
         update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx
     | Abstract _ ->
         (* This can't happen for sure *)
-        craise
-          meta
-             "Can't promote a shared borrow to a mutable borrow if the borrow \
-              is inside an abstraction"
+        craise meta
+          "Can't promote a shared borrow to a mutable borrow if the borrow is \
+           inside an abstraction"
   in
   (* Continue *)
   cf ctx
 
 (** Promote a reserved mut borrow to a mut borrow. *)
-let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : BorrowId.id) : cm_fun
-    =
+let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
+    (l : BorrowId.id) : cm_fun =
  fun cf ctx ->
   (* Lookup the value *)
   let ek =
@@ -1588,10 +1625,9 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : Bo
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      craise
-        meta
-           "Can't activate a reserved mutable borrow referencing a loan inside\n\
-           \         an abstraction"
+      craise meta
+        "Can't activate a reserved mutable borrow referencing a loan inside\n\
+        \         an abstraction"
 
 let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs =
@@ -1621,7 +1657,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
         match lc with
         | ASharedLoan (bids, sv, child_av) ->
             (* We don't support nested borrows for now *)
-            cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
+            cassert
+              (not (value_has_borrows ctx sv.value))
+              meta "Nested borrows are not supported yet";
             (* Destructure the shared value *)
             let avl, sv =
               if destructure_shared_values then list_values sv else ([], sv)
@@ -1648,7 +1686,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             push { value; ty }
         | AIgnoredMutLoan (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+            cassert
+              (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
+              meta "Nested borrows are not supported yet";
             sanity_check (opt_bid = None) meta;
             (* Simply explore the child *)
             list_avalues false push_fail child_av
@@ -1659,7 +1699,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             { child = child_av; given_back = _; given_back_meta = _ }
         | AIgnoredSharedLoan child_av ->
             (* We don't support nested borrows for now *)
-            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+            cassert
+              (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
+              meta "Nested borrows are not supported yet";
             (* Simply explore the child *)
             list_avalues false push_fail child_av)
     | ABorrow bc -> (
@@ -1679,14 +1721,18 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             push av
         | AIgnoredMutBorrow (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+            cassert
+              (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
+              meta "Nested borrows are not supported yet";
             sanity_check (opt_bid = None) meta;
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AEndedIgnoredMutBorrow
             { child = child_av; given_back = _; given_back_meta = _ } ->
             (* We don't support nested borrows for now *)
-            cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
+            cassert
+              (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
+              meta "Nested borrows are not supported yet";
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AProjSharedBorrow asb ->
@@ -1725,9 +1771,12 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             let avl, sv = list_values sv in
             if destructure_shared_values then (
               (* Rem.: the shared value can't contain loans nor borrows *)
-              cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
+              cassert (ty_no_regions ty) meta
+                "Nested borrows are not supported yet";
               let av : typed_avalue =
-                sanity_check (not (value_has_loans_or_borrows ctx sv.value)) meta;
+                sanity_check
+                  (not (value_has_loans_or_borrows ctx sv.value))
+                  meta;
                 (* We introduce fresh ids for the symbolic values *)
                 let mk_value_with_fresh_sids (v : typed_value) : typed_value =
                   let visitor =
@@ -1742,7 +1791,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
                 in
                 let sv = mk_value_with_fresh_sids sv in
                 (* Create the new avalue *)
-                let value = ALoan (ASharedLoan (bids, sv, mk_aignored meta ty)) in
+                let value =
+                  ALoan (ASharedLoan (bids, sv, mk_aignored meta ty))
+                in
                 { value; ty }
               in
               let avl = List.append [ av ] avl in
@@ -1762,16 +1813,16 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
   (* Update *)
   { abs0 with avalues; kind = abs_kind; can_end }
 
-let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool) (ctx : eval_ctx)
-    (abs : abs) : bool =
+let abs_is_destructured (meta : Meta.meta) (destructure_shared_values : bool)
+    (ctx : eval_ctx) (abs : abs) : bool =
   let abs' =
     destructure_abs meta abs.kind abs.can_end destructure_shared_values ctx abs
   in
   abs = abs'
 
-let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
-    (destructure_shared_values : bool) (ctx : eval_ctx) (v : typed_value) :
-    abs list =
+let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
+    (can_end : bool) (destructure_shared_values : bool) (ctx : eval_ctx)
+    (v : typed_value) : abs list =
   (* Convert the value to a list of avalues *)
   let absl = ref [] in
   let push_abs (r_id : RegionId.id) (avalues : typed_avalue list) : unit =
@@ -1852,20 +1903,24 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
         (avl, { v with value = VAdt adt })
     | VBorrow bc -> (
         let _, ref_ty, kind = ty_as_ref ty in
-        cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet";
+        cassert (ty_no_regions ref_ty) meta
+          "Nested borrows are not supported yet";
         (* Sanity check *)
         sanity_check allow_borrows meta;
         (* Convert the borrow content *)
         match bc with
         | VSharedBorrow bid ->
-            cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet";
+            cassert (ty_no_regions ref_ty) meta
+              "Nested borrows are not supported yet";
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let value = ABorrow (ASharedBorrow bid) in
             ([ { value; ty } ], v)
         | VMutBorrow (bid, bv) ->
             let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
-            cassert (not (value_has_borrows ctx bv.value)) meta "Nested borrows are not supported yet";
+            cassert
+              (not (value_has_borrows ctx bv.value))
+              meta "Nested borrows are not supported yet";
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let ignored = mk_aignored meta ref_ty in
@@ -1884,10 +1939,13 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
         | VSharedLoan (bids, sv) ->
             let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
-            cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
+            cassert
+              (not (value_has_borrows ctx sv.value))
+              meta "Nested borrows are not supported yet";
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
+            cassert (ty_no_regions ty) meta
+              "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RShared in
             let ignored = mk_aignored meta ty in
             (* Rem.: the shared value might contain loans *)
@@ -1905,7 +1963,8 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
         | VMutLoan bid ->
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
+            cassert (ty_no_regions ty) meta
+              "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RMut in
             let ignored = mk_aignored meta ty in
             let av = ALoan (AMutLoan (bid, ignored)) in
@@ -1914,7 +1973,9 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
     | VSymbolic _ ->
         (* For now, we force all the symbolic values containing borrows to
            be eagerly expanded, and we don't support nested borrows *)
-        cassert (not (value_has_borrows ctx v.value)) meta "Nested borrows are not supported yet";
+        cassert
+          (not (value_has_borrows ctx v.value))
+          meta "Nested borrows are not supported yet";
         (* Return nothing *)
         ([], v)
   in
@@ -1955,8 +2016,8 @@ type merge_abstraction_info = {
     - all the borrows are destructured (for instance, shared loans can't
       contain shared loans).
  *)
-let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : abs) :
-    merge_abstraction_info =
+let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
+    (abs : abs) : merge_abstraction_info =
   let loans : loan_id_set ref = ref BorrowId.Set.empty in
   let borrows : borrow_id_set ref = ref BorrowId.Set.empty in
   let borrows_loans : borrow_or_loan_id list ref = ref [] in
@@ -2068,7 +2129,7 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : ab
 
       method! visit_symbolic_value _ sv =
         (* Sanity check: no borrows *)
-        sanity_check (not (symbolic_value_has_borrows ctx sv)) meta 
+        sanity_check (not (symbolic_value_has_borrows ctx sv)) meta
     end
   in
 
@@ -2135,19 +2196,25 @@ type merge_duplicates_funcs = {
 
     Merge two abstractions into one, without updating the context.
  *)
-let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
-    (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx) (abs0 : abs)
-    (abs1 : abs) : abs =
+let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
+    (can_end : bool) (merge_funs : merge_duplicates_funcs option)
+    (ctx : eval_ctx) (abs0 : abs) (abs1 : abs) : abs =
   log#ldebug
     (lazy
-      ("merge_into_abstraction_aux:\n- abs0:\n" ^ abs_to_string meta ctx abs0
-     ^ "\n\n- abs1:\n" ^ abs_to_string meta ctx abs1));
+      ("merge_into_abstraction_aux:\n- abs0:\n"
+      ^ abs_to_string meta ctx abs0
+      ^ "\n\n- abs1:\n"
+      ^ abs_to_string meta ctx abs1));
 
   (* Check that the abstractions are destructured *)
   if !Config.sanity_checks then (
     let destructure_shared_values = true in
-    sanity_check (abs_is_destructured meta destructure_shared_values ctx abs0) meta;
-    sanity_check (abs_is_destructured meta destructure_shared_values ctx abs1) meta);
+    sanity_check
+      (abs_is_destructured meta destructure_shared_values ctx abs0)
+      meta;
+    sanity_check
+      (abs_is_destructured meta destructure_shared_values ctx abs1)
+      meta);
 
   (* Compute the relevant information *)
   let {
@@ -2172,9 +2239,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
-  if merge_funs = None then (
-    sanity_check (BorrowId.Set.disjoint borrows0 borrows1) meta;
-    sanity_check (BorrowId.Set.disjoint loans0 loans1)) meta;
+  if merge_funs = None then
+    (sanity_check (BorrowId.Set.disjoint borrows0 borrows1) meta;
+     sanity_check (BorrowId.Set.disjoint loans0 loans1))
+      meta;
 
   (* Merge.
      There are several cases:
@@ -2405,10 +2473,13 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
                           match lc with
                           | ASharedLoan (bids, sv, child) ->
                               let bids = filter_bids bids in
-                              sanity_check (not (BorrowId.Set.is_empty bids)) meta;
+                              sanity_check
+                                (not (BorrowId.Set.is_empty bids))
+                                meta;
                               sanity_check (is_aignored child.value) meta;
-                              sanity_check (
-                                not (value_has_loans_or_borrows ctx sv.value)) meta;
+                              sanity_check
+                                (not (value_has_loans_or_borrows ctx sv.value))
+                                meta;
                               let lc = ASharedLoan (bids, sv, child) in
                               set_loans_as_merged bids;
                               Some { value = ALoan lc; ty }
@@ -2487,9 +2558,9 @@ let ctx_merge_regions (ctx : eval_ctx) (rid : RegionId.id)
   let env = Substitute.env_subst_rids rsubst ctx.env in
   { ctx with env }
 
-let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
-    (merge_funs : merge_duplicates_funcs option) (ctx : eval_ctx)
-    (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) :
+let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind)
+    (can_end : bool) (merge_funs : merge_duplicates_funcs option)
+    (ctx : eval_ctx) (abs_id0 : AbstractionId.id) (abs_id1 : AbstractionId.id) :
     eval_ctx * AbstractionId.id =
   (* Lookup the abstractions *)
   let abs0 = ctx_lookup_abs ctx abs_id0 in
-- 
cgit v1.2.3


From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

---
 compiler/InterpreterBorrows.ml | 258 ++++++++++++++++++++---------------------
 1 file changed, 129 insertions(+), 129 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 2ccf2d5d..cc34020a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -43,7 +43,7 @@ let end_borrow_get_borrow (meta : Meta.meta)
   in
   let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content)
       =
-    sanity_check (Option.is_none !replaced_bc) meta;
+    sanity_check __FILE__ __LINE__ (Option.is_none !replaced_bc) meta;
     replaced_bc := Some (abs_id, bc)
   in
   (* Raise an exception if:
@@ -182,7 +182,7 @@ let end_borrow_get_borrow (meta : Meta.meta)
                * Also note that, as we are moving the borrowed value inside the
                * abstraction (and not really giving the value back to the context)
                * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *)
-              craise meta "Unimplemented"
+              craise __FILE__ __LINE__ meta "Unimplemented"
               (* ABottom *))
             else
               (* Update the outer borrows before diving into the child avalue *)
@@ -225,8 +225,8 @@ let end_borrow_get_borrow (meta : Meta.meta)
       method! visit_abs outer abs =
         (* Update the outer abs *)
         let outer_abs, outer_borrows = outer in
-        sanity_check (Option.is_none outer_abs) meta;
-        sanity_check (Option.is_none outer_borrows) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none outer_abs) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none outer_borrows) meta;
         let outer = (Some abs.abs_id, None) in
         super#visit_abs outer abs
     end
@@ -249,10 +249,10 @@ let end_borrow_get_borrow (meta : Meta.meta)
 let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
     (nv : typed_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity check *)
-  exec_assert
+  exec_assert __FILE__ __LINE__
     (not (loans_in_value nv))
     meta "Can not end a borrow because the value to give back contains bottom";
-  exec_assert
+  exec_assert __FILE__ __LINE__
     (not (bottom_in_value ctx.ended_regions nv))
     meta "Can not end a borrow because the value to give back contains bottom";
   (* Debug *)
@@ -266,7 +266,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    sanity_check (not !replaced) meta;
+    sanity_check __FILE__ __LINE__ (not !replaced) meta;
     replaced := true
   in
   (* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
@@ -308,7 +308,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
                   ("give_back_value: improper type:\n- expected: "
                  ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                craise meta "Value given back doesn't have the proper type");
+                craise __FILE__ __LINE__ meta "Value given back doesn't have the proper type");
               (* Replace *)
               set_replaced ();
               nv.value)
@@ -353,7 +353,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
                   ABorrow
                     (AEndedIgnoredMutBorrow
                        { given_back; child; given_back_meta })
-              | _ -> craise meta "Unreachable"
+              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
             else
               (* Continue exploring *)
               ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child)
@@ -368,7 +368,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
         (* Preparing a bit *)
         let regions, ancestors_regions =
           match opt_abs with
-          | None -> craise meta "Unreachable"
+          | None -> craise __FILE__ __LINE__ meta "Unreachable"
           | Some abs -> (abs.regions, abs.ancestors_regions)
         in
         (* Rk.: there is a small issue with the types of the aloan values.
@@ -434,7 +434,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
         (* We remember in which abstraction we are before diving -
          * this is necessary for projecting values: we need to know
          * over which regions to project *)
-        sanity_check (Option.is_none opt_abs) meta;
+        sanity_check __FILE__ __LINE__ (Option.is_none opt_abs) meta;
         super#visit_EAbs (Some abs) abs
     end
   in
@@ -442,7 +442,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert !replaced meta "Only one loan should have been given back";
+  cassert __FILE__ __LINE__ !replaced meta "Only one loan should have been given back";
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
@@ -451,7 +451,7 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta)
     (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value)
     (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
-  sanity_check (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta;
+  sanity_check __FILE__ __LINE__ (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta;
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -473,7 +473,7 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta)
          type [T]! We thus *mustn't* introduce a projector here.
       *)
       (* AProjBorrows (nsv, sv.sv_ty) *)
-      internal_error meta
+      internal_error __FILE__ __LINE__ meta
     in
     AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
@@ -498,7 +498,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    cassert (not !replaced) meta "Only one loan should have been updated";
+    cassert __FILE__ __LINE__ (not !replaced) meta "Only one loan should have been updated";
     replaced := true
   in
   let obj =
@@ -541,7 +541,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                   ("give_back_avalue_to_same_abstraction: improper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                craise meta "Value given back doesn't have the proper type");
+                craise __FILE__ __LINE__ meta "Value given back doesn't have the proper type");
               (* This is the loan we are looking for: apply the projection to
                * the value we give back and replaced this mutable loan with
                * an ended loan *)
@@ -567,7 +567,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                * we don't register the fact that we inserted the value somewhere
                * (i.e., we don't call {!set_replaced}) *)
               (* Sanity check *)
-              sanity_check (nv.ty = ty) meta;
+              sanity_check __FILE__ __LINE__ (nv.ty = ty) meta;
               ALoan
                 (AEndedIgnoredMutLoan
                    { given_back = nv; child; given_back_meta = nsv }))
@@ -583,7 +583,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert !replaced meta "Only one loan should be given back";
+  cassert __FILE__ __LINE__ !replaced meta "Only one loan should be given back";
   (* Return *)
   ctx
 
@@ -601,7 +601,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    cassert (not !replaced) meta "Only one loan should be updated";
+    cassert __FILE__ __LINE__ (not !replaced) meta "Only one loan should be updated";
     replaced := true
   in
   let obj =
@@ -666,7 +666,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert !replaced meta "Exactly one loan should be given back";
+  cassert __FILE__ __LINE__ !replaced meta "Exactly one loan should be given back";
   (* Return *)
   ctx
 
@@ -680,7 +680,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id)
   (* Keep track of changes *)
   let r = ref false in
   let set_ref () =
-    sanity_check (not !r) meta;
+    sanity_check __FILE__ __LINE__ (not !r) meta;
     r := true
   in
 
@@ -710,7 +710,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id)
 
   let env = obj#visit_env () ctx.env in
   (* Check that we reborrowed once *)
-  sanity_check !r meta;
+  sanity_check __FILE__ __LINE__ !r meta;
   { ctx with env }
 
 (** Convert an {!type:avalue} to a {!type:value}.
@@ -770,24 +770,24 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id)
   match bc with
   | Concrete (VMutBorrow (l', tv)) ->
       (* Sanity check *)
-      sanity_check (l' = l) meta;
-      sanity_check (not (loans_in_value tv)) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) meta;
+      sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) meta;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Update the context *)
       give_back_value config meta l tv ctx
   | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
       (* Sanity check *)
-      sanity_check (l' = l) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) meta;
       (* Check that the borrow is somewhere - purely a sanity check *)
-      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract (AMutBorrow (l', av)) ->
       (* Sanity check *)
-      sanity_check (l' = l) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) meta;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Convert the avalue to a (fresh symbolic) value.
 
          Rem.: we shouldn't do this here. We should do this in a function
@@ -800,20 +800,20 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id)
         ctx
   | Abstract (ASharedBorrow l') ->
       (* Sanity check *)
-      sanity_check (l' = l) meta;
+      sanity_check __FILE__ __LINE__ (l' = l) meta;
       (* Check that the borrow is somewhere - purely a sanity check *)
-      sanity_check (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract (AProjSharedBorrow asb) ->
       (* Sanity check *)
-      sanity_check (borrow_in_asb l asb) meta;
+      sanity_check __FILE__ __LINE__ (borrow_in_asb l asb) meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract
       ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
       | AEndedSharedBorrow ) ->
-      craise meta "Unreachable"
+      craise __FILE__ __LINE__ meta "Unreachable"
 
 let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
     (l : BorrowId.id) (ctx0 : eval_ctx) : cm_fun =
@@ -829,7 +829,7 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
               ^ eval_ctx_to_string ~meta:(Some meta) ctx0
               ^ "\n\n- new context:\n"
               ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-          craise meta "Borrow not eliminated"
+          craise __FILE__ __LINE__ meta "Borrow not eliminated"
     in
     match lookup_loan_opt meta ek_all l ctx with
     | None -> () (* Ok *)
@@ -841,7 +841,7 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
             ^ eval_ctx_to_string ~meta:(Some meta) ctx0
             ^ "\n\n- new context:\n"
             ^ eval_ctx_to_string ~meta:(Some meta) ctx));
-        craise meta "Loan not eliminated"
+        craise __FILE__ __LINE__ meta "Loan not eliminated"
   in
   unit_to_cm_fun check_disappeared
 
@@ -937,7 +937,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
       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 *)
-      sanity_check (config.mode = SymbolicMode) meta;
+      sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta;
       (* Do a sanity check and continue *)
       cf_check cf ctx
   (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update
@@ -946,7 +946,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
       (* Sanity check: the borrowed value shouldn't contain loans *)
       (match bc with
       | Concrete (VMutBorrow (_, bv)) ->
-          sanity_check (Option.is_none (get_first_loan_in_value bv)) meta
+          sanity_check __FILE__ __LINE__ (Option.is_none (get_first_loan_in_value bv)) meta
       | _ -> ());
       (* Give back the value *)
       let ctx = give_back config meta l bc ctx in
@@ -1002,7 +1002,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta)
       (* Check that we can end the abstraction *)
       if abs.can_end then ()
       else
-        craise meta
+        craise __FILE__ __LINE__ meta
           ("Can't end abstraction "
           ^ AbstractionId.to_string abs.abs_id
           ^ " as it is set as non-endable");
@@ -1172,7 +1172,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
 
       method! visit_aproj env sproj =
         (match sproj with
-        | AProjLoans _ -> craise meta "Unexpected"
+        | AProjLoans _ -> craise __FILE__ __LINE__ meta "Unexpected"
         | AProjBorrows (sv, proj_ty) -> raise (FoundAProjBorrows (sv, proj_ty))
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj env sproj
@@ -1181,7 +1181,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
       method! visit_borrow_content _ bc =
         match bc with
         | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc)
-        | VReservedMutBorrow _ -> craise meta "Unreachable"
+        | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable"
     end
   in
   (* Lookup the abstraction *)
@@ -1241,7 +1241,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
             ctx
         | AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
         | AEndedSharedBorrow ->
-            craise meta "Unexpected"
+            craise __FILE__ __LINE__ meta "Unexpected"
       in
       (* Reexplore *)
       end_abstraction_borrows config meta chain abs_id cf ctx
@@ -1276,7 +1276,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
             match
               end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
             with
-            | Error _ -> craise meta "Unreachable"
+            | Error _ -> craise __FILE__ __LINE__ meta "Unreachable"
             | Ok (ctx, _) ->
                 (* Give back *)
                 give_back_shared config meta bid ctx)
@@ -1286,12 +1286,12 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta)
             match
               end_borrow_get_borrow meta (Some abs_id) allow_inner_loans bid ctx
             with
-            | Error _ -> craise meta "Unreachable"
+            | Error _ -> craise __FILE__ __LINE__ meta "Unreachable"
             | Ok (ctx, _) ->
                 (* Give the value back - note that the mut borrow was below a
                  * shared borrow: the value is thus unchanged *)
                 give_back_value config meta bid v ctx)
-        | VReservedMutBorrow _ -> craise meta "Unreachable"
+        | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable"
       in
       (* Reexplore *)
       end_abstraction_borrows config meta chain abs_id cf ctx
@@ -1430,7 +1430,7 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta)
          * replace it with... Maybe we should introduce an ABottomProj? *)
         let ctx = update_aproj_borrows meta abs_id sv AIgnoredProjBorrows ctx in
         (* Sanity check: no other occurrence of an intersecting projector of borrows *)
-        sanity_check
+        sanity_check __FILE__ __LINE__
           (Option.is_none
              (lookup_intersecting_aproj_borrows_opt meta explore_shared regions
                 sv ctx))
@@ -1509,22 +1509,22 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
   in
   match lookup_loan meta ek l ctx with
   | _, Concrete (VMutLoan _) ->
-      craise meta "Expected a shared loan, found a mut loan"
+      craise __FILE__ __LINE__ meta "Expected a shared loan, found a mut loan"
   | _, Concrete (VSharedLoan (bids, sv)) ->
       (* Check that there is only one borrow id (l) and update the loan *)
-      cassert
+      cassert __FILE__ __LINE__
         (BorrowId.Set.mem l bids && BorrowId.Set.cardinal bids = 1)
         meta "There should only be one borrow id";
       (* We need to check that there aren't any loans in the value:
          we should have gotten rid of those already, but it is better
          to do a sanity check. *)
-      sanity_check (not (loans_in_value sv)) meta;
+      sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta;
       (* Check there isn't {!Bottom} (this is actually an invariant *)
-      cassert
+      cassert __FILE__ __LINE__
         (not (bottom_in_value ctx.ended_regions sv))
         meta "There shouldn't be a bottom";
       (* Check there aren't reserved borrows *)
-      cassert
+      cassert __FILE__ __LINE__
         (not (reserved_in_value sv))
         meta "There shouldn't be reserved borrows";
       (* Update the loan content *)
@@ -1534,7 +1534,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      craise meta
+      craise __FILE__ __LINE__ meta
         "Can't promote a shared loan to a mutable loan if the loan is inside \
          an abstraction"
 
@@ -1555,13 +1555,13 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
   let ctx =
     match lookup_borrow meta ek l ctx with
     | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) ->
-        craise meta "Expected a reserved mutable borrow"
+        craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow"
     | Concrete (VReservedMutBorrow _) ->
         (* Update it *)
         update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx
     | Abstract _ ->
         (* This can't happen for sure *)
-        craise meta
+        craise __FILE__ __LINE__ meta
           "Can't promote a shared borrow to a mutable borrow if the borrow is \
            inside an abstraction"
   in
@@ -1577,7 +1577,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
   in
   match lookup_loan meta ek l ctx with
-  | _, Concrete (VMutLoan _) -> craise meta "Unreachable"
+  | _, Concrete (VMutLoan _) -> craise __FILE__ __LINE__ meta "Unreachable"
   | _, Concrete (VSharedLoan (bids, sv)) -> (
       (* If there are loans inside the value, end them. Note that there can't be
          reserved borrows inside the value.
@@ -1601,9 +1601,9 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
             (lazy
               ("activate_reserved_mut_borrow: resulting value:\n"
               ^ typed_value_to_string ~meta:(Some meta) ctx sv));
-          sanity_check (not (loans_in_value sv)) meta;
-          sanity_check (not (bottom_in_value ctx.ended_regions sv)) meta;
-          sanity_check (not (reserved_in_value sv)) meta;
+          sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta;
+          sanity_check __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions sv)) meta;
+          sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) meta;
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
           let bids = BorrowId.Set.remove l bids in
@@ -1625,7 +1625,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
   | _, Abstract _ ->
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
-      craise meta
+      craise __FILE__ __LINE__ meta
         "Can't activate a reserved mutable borrow referencing a loan inside\n\
         \         an abstraction"
 
@@ -1642,7 +1642,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
      ignore the children altogether. Instead, we explore them and make sure
      we don't register values while doing so.
   *)
-  let push_fail _ = craise meta "Unreachable" in
+  let push_fail _ = craise __FILE__ __LINE__ meta "Unreachable" in
   (* Function to explore an avalue and destructure it *)
   let rec list_avalues (allow_borrows : bool) (push : typed_avalue -> unit)
       (av : typed_avalue) : unit =
@@ -1657,7 +1657,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
         match lc with
         | ASharedLoan (bids, sv, child_av) ->
             (* We don't support nested borrows for now *)
-            cassert
+            cassert __FILE__ __LINE__
               (not (value_has_borrows ctx sv.value))
               meta "Nested borrows are not supported yet";
             (* Destructure the shared value *)
@@ -1686,10 +1686,10 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             push { value; ty }
         | AIgnoredMutLoan (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            cassert
+            cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
               meta "Nested borrows are not supported yet";
-            sanity_check (opt_bid = None) meta;
+            sanity_check __FILE__ __LINE__ (opt_bid = None) meta;
             (* Simply explore the child *)
             list_avalues false push_fail child_av
         | AEndedMutLoan
@@ -1699,14 +1699,14 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             { child = child_av; given_back = _; given_back_meta = _ }
         | AIgnoredSharedLoan child_av ->
             (* We don't support nested borrows for now *)
-            cassert
+            cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
               meta "Nested borrows are not supported yet";
             (* Simply explore the child *)
             list_avalues false push_fail child_av)
     | ABorrow bc -> (
         (* Sanity check - rem.: may be redundant with [push_fail] *)
-        sanity_check allow_borrows meta;
+        sanity_check __FILE__ __LINE__ allow_borrows meta;
         (* Explore the borrow content *)
         match bc with
         | AMutBorrow (bid, child_av) ->
@@ -1721,23 +1721,23 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             push av
         | AIgnoredMutBorrow (opt_bid, child_av) ->
             (* We don't support nested borrows for now *)
-            cassert
+            cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
               meta "Nested borrows are not supported yet";
-            sanity_check (opt_bid = None) meta;
+            sanity_check __FILE__ __LINE__ (opt_bid = None) meta;
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AEndedIgnoredMutBorrow
             { child = child_av; given_back = _; given_back_meta = _ } ->
             (* We don't support nested borrows for now *)
-            cassert
+            cassert __FILE__ __LINE__
               (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty))
               meta "Nested borrows are not supported yet";
             (* Just explore the child *)
             list_avalues false push_fail child_av
         | AProjSharedBorrow asb ->
             (* We don't support nested borrows *)
-            cassert (asb = []) meta "Nested borrows are not supported yet";
+            cassert __FILE__ __LINE__ (asb = []) meta "Nested borrows are not supported yet";
             (* Nothing specific to do *)
             ()
         | AEndedMutBorrow _ | AEndedSharedBorrow ->
@@ -1745,11 +1745,11 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
                be in the context anymore (if we end *one* borrow in an abstraction,
                we have to end them all and remove the abstraction from the context)
             *)
-            craise meta "Unreachable")
+            craise __FILE__ __LINE__ meta "Unreachable")
     | ASymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta
+        sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta
   and list_values (v : typed_value) : typed_avalue list * typed_value =
     let ty = v.ty in
     match v.value with
@@ -1761,20 +1761,20 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
         let avl = List.concat avll in
         let adt = { adt with field_values } in
         (avl, { v with value = VAdt adt })
-    | VBottom -> craise meta "Unreachable"
+    | VBottom -> craise __FILE__ __LINE__ meta "Unreachable"
     | VBorrow _ ->
         (* We don't support nested borrows for now *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
     | VLoan lc -> (
         match lc with
         | VSharedLoan (bids, sv) ->
             let avl, sv = list_values sv in
             if destructure_shared_values then (
               (* Rem.: the shared value can't contain loans nor borrows *)
-              cassert (ty_no_regions ty) meta
+              cassert __FILE__ __LINE__ (ty_no_regions ty) meta
                 "Nested borrows are not supported yet";
               let av : typed_avalue =
-                sanity_check
+                sanity_check __FILE__ __LINE__
                   (not (value_has_loans_or_borrows ctx sv.value))
                   meta;
                 (* We introduce fresh ids for the symbolic values *)
@@ -1799,11 +1799,11 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
               let avl = List.append [ av ] avl in
               (avl, sv))
             else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) })
-        | VMutLoan _ -> craise meta "Unreachable")
+        | VMutLoan _ -> craise __FILE__ __LINE__ meta "Unreachable")
     | VSymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta;
+        sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta;
         ([], v)
   in
 
@@ -1903,14 +1903,14 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
         (avl, { v with value = VAdt adt })
     | VBorrow bc -> (
         let _, ref_ty, kind = ty_as_ref ty in
-        cassert (ty_no_regions ref_ty) meta
+        cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta
           "Nested borrows are not supported yet";
         (* Sanity check *)
-        sanity_check allow_borrows meta;
+        sanity_check __FILE__ __LINE__ allow_borrows meta;
         (* Convert the borrow content *)
         match bc with
         | VSharedBorrow bid ->
-            cassert (ty_no_regions ref_ty) meta
+            cassert __FILE__ __LINE__ (ty_no_regions ref_ty) meta
               "Nested borrows are not supported yet";
             let ty = TRef (RFVar r_id, ref_ty, kind) in
             let value = ABorrow (ASharedBorrow bid) in
@@ -1918,7 +1918,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
         | VMutBorrow (bid, bv) ->
             let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
-            cassert
+            cassert __FILE__ __LINE__
               (not (value_has_borrows ctx bv.value))
               meta "Nested borrows are not supported yet";
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
@@ -1933,18 +1933,18 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
             (av :: avl, value)
         | VReservedMutBorrow _ ->
             (* This borrow should have been activated *)
-            craise meta "Unexpected")
+            craise __FILE__ __LINE__ meta "Unexpected")
     | VLoan lc -> (
         match lc with
         | VSharedLoan (bids, sv) ->
             let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
-            cassert
+            cassert __FILE__ __LINE__
               (not (value_has_borrows ctx sv.value))
               meta "Nested borrows are not supported yet";
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert (ty_no_regions ty) meta
+            cassert __FILE__ __LINE__ (ty_no_regions ty) meta
               "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RShared in
             let ignored = mk_aignored meta ty in
@@ -1963,7 +1963,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
         | VMutLoan bid ->
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
-            cassert (ty_no_regions ty) meta
+            cassert __FILE__ __LINE__ (ty_no_regions ty) meta
               "Nested borrows are not supported yet";
             let ty = mk_ref_ty (RFVar r_id) ty RMut in
             let ignored = mk_aignored meta ty in
@@ -1973,7 +1973,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind)
     | VSymbolic _ ->
         (* For now, we force all the symbolic values containing borrows to
            be eagerly expanded, and we don't support nested borrows *)
-        cassert
+        cassert __FILE__ __LINE__
           (not (value_has_borrows ctx v.value))
           meta "Nested borrows are not supported yet";
         (* Return nothing *)
@@ -2029,26 +2029,26 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
   in
 
   let push_loans ids (lc : g_loan_content_with_ty) : unit =
-    sanity_check (BorrowId.Set.disjoint !loans ids) meta;
+    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint !loans ids) meta;
     loans := BorrowId.Set.union !loans ids;
     BorrowId.Set.iter
       (fun id ->
-        sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta;
+        sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) meta;
         loan_to_content := BorrowId.Map.add id lc !loan_to_content;
         borrows_loans := LoanId id :: !borrows_loans)
       ids
   in
   let push_loan id (lc : g_loan_content_with_ty) : unit =
-    sanity_check (not (BorrowId.Set.mem id !loans)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) meta;
     loans := BorrowId.Set.add id !loans;
-    sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) meta;
     loan_to_content := BorrowId.Map.add id lc !loan_to_content;
     borrows_loans := LoanId id :: !borrows_loans
   in
   let push_borrow id (bc : g_borrow_content_with_ty) : unit =
-    sanity_check (not (BorrowId.Set.mem id !borrows)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) meta;
     borrows := BorrowId.Set.add id !borrows;
-    sanity_check (not (BorrowId.Map.mem id !borrow_to_content)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !borrow_to_content)) meta;
     borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
     borrows_loans := BorrowId id :: !borrows_loans
   in
@@ -2071,23 +2071,23 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
         let ty =
           match Option.get env with
           | Concrete ty -> ty
-          | Abstract _ -> craise meta "Unreachable"
+          | Abstract _ -> craise __FILE__ __LINE__ meta "Unreachable"
         in
         (match lc with
         | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
-        | VMutLoan _ -> craise meta "Unreachable");
+        | VMutLoan _ -> craise __FILE__ __LINE__ meta "Unreachable");
         (* Continue *)
         super#visit_loan_content env lc
 
       method! visit_borrow_content _ _ =
         (* Can happen if we explore shared values which contain borrows -
            i.e., if we have nested borrows (we forbid this for now) *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
 
       method! visit_aloan_content env lc =
         let ty =
           match Option.get env with
-          | Concrete _ -> craise meta "Unreachable"
+          | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable"
           | Abstract ty -> ty
         in
         (* Register the loans *)
@@ -2097,14 +2097,14 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
         | AEndedMutLoan _ | AEndedSharedLoan _ | AIgnoredMutLoan _
         | AEndedIgnoredMutLoan _ | AIgnoredSharedLoan _ ->
             (* The abstraction has been destructured, so those shouldn't appear *)
-            craise meta "Unreachable");
+            craise __FILE__ __LINE__ meta "Unreachable");
         (* Continue *)
         super#visit_aloan_content env lc
 
       method! visit_aborrow_content env bc =
         let ty =
           match Option.get env with
-          | Concrete _ -> craise meta "Unreachable"
+          | Concrete _ -> craise __FILE__ __LINE__ meta "Unreachable"
           | Abstract ty -> ty
         in
         (* Explore the borrow content *)
@@ -2118,18 +2118,18 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
               | AsbProjReborrows _ ->
                   (* Can only happen if the symbolic value (potentially) contains
                      borrows - i.e., we have nested borrows *)
-                  craise meta "Unreachable"
+                  craise __FILE__ __LINE__ meta "Unreachable"
             in
             List.iter register asb
         | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedMutBorrow _
         | AEndedSharedBorrow ->
             (* The abstraction has been destructured, so those shouldn't appear *)
-            craise meta "Unreachable");
+            craise __FILE__ __LINE__ meta "Unreachable");
         super#visit_aborrow_content env bc
 
       method! visit_symbolic_value _ sv =
         (* Sanity check: no borrows *)
-        sanity_check (not (symbolic_value_has_borrows ctx sv)) meta
+        sanity_check __FILE__ __LINE__ (not (symbolic_value_has_borrows ctx sv)) meta
     end
   in
 
@@ -2209,10 +2209,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   (* Check that the abstractions are destructured *)
   if !Config.sanity_checks then (
     let destructure_shared_values = true in
-    sanity_check
+    sanity_check __FILE__ __LINE__
       (abs_is_destructured meta destructure_shared_values ctx abs0)
       meta;
-    sanity_check
+    sanity_check __FILE__ __LINE__
       (abs_is_destructured meta destructure_shared_values ctx abs1)
       meta);
 
@@ -2240,8 +2240,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
   if merge_funs = None then
-    (sanity_check (BorrowId.Set.disjoint borrows0 borrows1) meta;
-     sanity_check (BorrowId.Set.disjoint loans0 loans1))
+    (sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint borrows0 borrows1) meta;
+     sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1))
       meta;
 
   (* Merge.
@@ -2283,7 +2283,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   in
   let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t =
     let bids = BorrowId.Set.diff bids intersect in
-    sanity_check (not (BorrowId.Set.is_empty bids)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.is_empty bids)) meta;
     bids
   in
   let filter_bid (bid : BorrowId.id) : BorrowId.id option =
@@ -2311,11 +2311,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
         (Option.get merge_funs).merge_ashared_borrows id ty0 ty1
     | AProjSharedBorrow _, AProjSharedBorrow _ ->
         (* Unreachable because requires nested borrows *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
   in
 
   let merge_g_borrow_contents (bc0 : g_borrow_content_with_ty)
@@ -2323,12 +2323,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     match (bc0, bc1) with
     | Concrete _, Concrete _ ->
         (* This can happen only in case of nested borrows *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
     | Abstract (ty0, bc0), Abstract (ty1, bc1) ->
         merge_aborrow_contents ty0 bc0 ty1 bc1
     | Concrete _, Abstract _ | Abstract _, Concrete _ ->
         (* TODO: is it really unreachable? *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
   in
 
   let merge_aloan_contents (ty0 : rty) (lc0 : aloan_content) (ty1 : rty)
@@ -2346,7 +2346,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
         (* Check that the sets of ids are the same - if it is not the case, it
            means we actually need to merge more than 2 avalues: we ignore this
            case for now *)
-        sanity_check (BorrowId.Set.equal ids0 ids1) meta;
+        sanity_check __FILE__ __LINE__ (BorrowId.Set.equal ids0 ids1) meta;
         let ids = ids0 in
         if BorrowId.Set.is_empty ids then (
           (* If the set of ids is empty, we can eliminate this shared loan.
@@ -2358,10 +2358,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
              to preserve (in practice it works because we destructure the
              shared values in the abstractions, and forbid nested borrows).
           *)
-          sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
-          sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
-          sanity_check (is_aignored child0.value) meta;
-          sanity_check (is_aignored child1.value) meta;
+          sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+          sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+          sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta;
+          sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta;
           None)
         else (
           (* Register the loan ids *)
@@ -2373,7 +2373,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     | _ ->
         (* Unreachable because those cases are ignored (ended/ignored borrows)
            or inconsistent *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
   in
 
   (* Note that because we may filter ids from a set of id, this function has
@@ -2384,12 +2384,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
     match (lc0, lc1) with
     | Concrete _, Concrete _ ->
         (* This can not happen: the values should have been destructured *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
     | Abstract (ty0, lc0), Abstract (ty1, lc1) ->
         merge_aloan_contents ty0 lc0 ty1 lc1
     | Concrete _, Abstract _ | Abstract _, Concrete _ ->
         (* TODO: is it really unreachable? *)
-        craise meta "Unreachable"
+        craise __FILE__ __LINE__ meta "Unreachable"
   in
 
   (* Note that we first explore the borrows/loans of [abs1], because we
@@ -2430,12 +2430,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
                              a concrete borrow can only happen inside a shared
                              loan
                           *)
-                          craise meta "Unreachable"
+                          craise __FILE__ __LINE__ meta "Unreachable"
                       | Abstract (ty, bc) -> { value = ABorrow bc; ty })
                   | Some bc0, Some bc1 ->
-                      sanity_check (merge_funs <> None) meta;
+                      sanity_check __FILE__ __LINE__ (merge_funs <> None) meta;
                       merge_g_borrow_contents bc0 bc1
-                  | None, None -> craise meta "Unreachable"
+                  | None, None -> craise __FILE__ __LINE__ meta "Unreachable"
                 in
                 push_avalue av)
       | LoanId bid ->
@@ -2468,16 +2468,16 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
                       | Concrete _ ->
                           (* This shouldn't happen because the avalues should
                              have been destructured. *)
-                          craise meta "Unreachable"
+                          craise __FILE__ __LINE__ meta "Unreachable"
                       | Abstract (ty, lc) -> (
                           match lc with
                           | ASharedLoan (bids, sv, child) ->
                               let bids = filter_bids bids in
-                              sanity_check
+                              sanity_check __FILE__ __LINE__
                                 (not (BorrowId.Set.is_empty bids))
                                 meta;
-                              sanity_check (is_aignored child.value) meta;
-                              sanity_check
+                              sanity_check __FILE__ __LINE__ (is_aignored child.value) meta;
+                              sanity_check __FILE__ __LINE__
                                 (not (value_has_loans_or_borrows ctx sv.value))
                                 meta;
                               let lc = ASharedLoan (bids, sv, child) in
@@ -2490,11 +2490,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
                           | AIgnoredMutLoan _ | AEndedIgnoredMutLoan _
                           | AIgnoredSharedLoan _ ->
                               (* The abstraction has been destructured, so those shouldn't appear *)
-                              craise meta "Unreachable"))
+                              craise __FILE__ __LINE__ meta "Unreachable"))
                   | Some lc0, Some lc1 ->
-                      sanity_check (merge_funs <> None) meta;
+                      sanity_check __FILE__ __LINE__ (merge_funs <> None) meta;
                       merge_g_loan_contents lc0 lc1
-                  | None, None -> craise meta "Unreachable"
+                  | None, None -> craise __FILE__ __LINE__ meta "Unreachable"
                 in
                 push_opt_avalue av))
     borrows_loans;
@@ -2512,7 +2512,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
       match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
-      | _ -> craise meta "Unexpected"
+      | _ -> craise __FILE__ __LINE__ meta "Unexpected"
     in
     let aborrows, aloans = List.partition is_borrow avalues in
     List.append aborrows aloans
@@ -2547,7 +2547,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   in
 
   (* Sanity check *)
-  sanity_check (abs_is_destructured meta true ctx abs) meta;
+  sanity_check __FILE__ __LINE__ (abs_is_destructured meta true ctx abs) meta;
   (* Return *)
   abs
 
-- 
cgit v1.2.3


From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 14:07:36 +0100
Subject: formatting and changed save_error condition for failing from b to not
 b

---
 compiler/InterpreterBorrows.ml | 88 ++++++++++++++++++++++++++++++------------
 1 file changed, 64 insertions(+), 24 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index cc34020a..b32261e6 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -308,7 +308,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
                   ("give_back_value: improper type:\n- expected: "
                  ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                craise __FILE__ __LINE__ meta "Value given back doesn't have the proper type");
+                craise __FILE__ __LINE__ meta
+                  "Value given back doesn't have the proper type");
               (* Replace *)
               set_replaced ();
               nv.value)
@@ -442,7 +443,8 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta "Only one loan should have been given back";
+  cassert __FILE__ __LINE__ !replaced meta
+    "Only one loan should have been given back";
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
@@ -451,7 +453,9 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta)
     (proj_regions : RegionId.Set.t) (proj_ty : rty) (sv : symbolic_value)
     (nsv : symbolic_value) (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
-  sanity_check __FILE__ __LINE__ (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty) meta;
+  sanity_check __FILE__ __LINE__
+    (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty)
+    meta;
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -498,7 +502,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    cassert __FILE__ __LINE__ (not !replaced) meta "Only one loan should have been updated";
+    cassert __FILE__ __LINE__ (not !replaced) meta
+      "Only one loan should have been updated";
     replaced := true
   in
   let obj =
@@ -541,7 +546,8 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
                   ("give_back_avalue_to_same_abstraction: improper type:\n\
                     - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
                  ^ ty_to_string ctx nv.ty);
-                craise __FILE__ __LINE__ meta "Value given back doesn't have the proper type");
+                craise __FILE__ __LINE__ meta
+                  "Value given back doesn't have the proper type");
               (* This is the loan we are looking for: apply the projection to
                * the value we give back and replaced this mutable loan with
                * an ended loan *)
@@ -601,7 +607,8 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   (* We use a reference to check that we updated exactly one loan *)
   let replaced : bool ref = ref false in
   let set_replaced () =
-    cassert __FILE__ __LINE__ (not !replaced) meta "Only one loan should be updated";
+    cassert __FILE__ __LINE__ (not !replaced) meta
+      "Only one loan should be updated";
     replaced := true
   in
   let obj =
@@ -666,7 +673,8 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta "Exactly one loan should be given back";
+  cassert __FILE__ __LINE__ !replaced meta
+    "Exactly one loan should be given back";
   (* Return *)
   ctx
 
@@ -773,21 +781,27 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id)
       sanity_check __FILE__ __LINE__ (l' = l) meta;
       sanity_check __FILE__ __LINE__ (not (loans_in_value tv)) meta;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__
+        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
+        meta;
       (* Update the context *)
       give_back_value config meta l tv ctx
   | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
       (* Sanity check *)
       sanity_check __FILE__ __LINE__ (l' = l) meta;
       (* Check that the borrow is somewhere - purely a sanity check *)
-      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__
+        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
+        meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract (AMutBorrow (l', av)) ->
       (* Sanity check *)
       sanity_check __FILE__ __LINE__ (l' = l) meta;
       (* Check that the corresponding loan is somewhere - purely a sanity check *)
-      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__
+        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
+        meta;
       (* Convert the avalue to a (fresh symbolic) value.
 
          Rem.: we shouldn't do this here. We should do this in a function
@@ -802,7 +816,9 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id)
       (* Sanity check *)
       sanity_check __FILE__ __LINE__ (l' = l) meta;
       (* Check that the borrow is somewhere - purely a sanity check *)
-      sanity_check __FILE__ __LINE__ (Option.is_some (lookup_loan_opt meta sanity_ek l ctx)) meta;
+      sanity_check __FILE__ __LINE__
+        (Option.is_some (lookup_loan_opt meta sanity_ek l ctx))
+        meta;
       (* Update the context *)
       give_back_shared config meta l ctx
   | Abstract (AProjSharedBorrow asb) ->
@@ -946,7 +962,9 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta)
       (* Sanity check: the borrowed value shouldn't contain loans *)
       (match bc with
       | Concrete (VMutBorrow (_, bv)) ->
-          sanity_check __FILE__ __LINE__ (Option.is_none (get_first_loan_in_value bv)) meta
+          sanity_check __FILE__ __LINE__
+            (Option.is_none (get_first_loan_in_value bv))
+            meta
       | _ -> ());
       (* Give back the value *)
       let ctx = give_back config meta l bc ctx in
@@ -1602,7 +1620,9 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
               ("activate_reserved_mut_borrow: resulting value:\n"
               ^ typed_value_to_string ~meta:(Some meta) ctx sv));
           sanity_check __FILE__ __LINE__ (not (loans_in_value sv)) meta;
-          sanity_check __FILE__ __LINE__ (not (bottom_in_value ctx.ended_regions sv)) meta;
+          sanity_check __FILE__ __LINE__
+            (not (bottom_in_value ctx.ended_regions sv))
+            meta;
           sanity_check __FILE__ __LINE__ (not (reserved_in_value sv)) meta;
           (* End the borrows which borrow from the value, at the exception of
              the borrow we want to promote *)
@@ -1737,7 +1757,8 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
             list_avalues false push_fail child_av
         | AProjSharedBorrow asb ->
             (* We don't support nested borrows *)
-            cassert __FILE__ __LINE__ (asb = []) meta "Nested borrows are not supported yet";
+            cassert __FILE__ __LINE__ (asb = []) meta
+              "Nested borrows are not supported yet";
             (* Nothing specific to do *)
             ()
         | AEndedMutBorrow _ | AEndedSharedBorrow ->
@@ -1749,7 +1770,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     | ASymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta
+        sanity_check __FILE__ __LINE__
+          (not (ty_has_borrows ctx.type_ctx.type_infos ty))
+          meta
   and list_values (v : typed_value) : typed_avalue list * typed_value =
     let ty = v.ty in
     match v.value with
@@ -1803,7 +1826,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     | VSymbolic _ ->
         (* For now, we fore all symbolic values containing borrows to be eagerly
            expanded *)
-        sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta;
+        sanity_check __FILE__ __LINE__
+          (not (ty_has_borrows ctx.type_ctx.type_infos ty))
+          meta;
         ([], v)
   in
 
@@ -2033,7 +2058,9 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
     loans := BorrowId.Set.union !loans ids;
     BorrowId.Set.iter
       (fun id ->
-        sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) meta;
+        sanity_check __FILE__ __LINE__
+          (not (BorrowId.Map.mem id !loan_to_content))
+          meta;
         loan_to_content := BorrowId.Map.add id lc !loan_to_content;
         borrows_loans := LoanId id :: !borrows_loans)
       ids
@@ -2041,14 +2068,18 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
   let push_loan id (lc : g_loan_content_with_ty) : unit =
     sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !loans)) meta;
     loans := BorrowId.Set.add id !loans;
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !loan_to_content)) meta;
+    sanity_check __FILE__ __LINE__
+      (not (BorrowId.Map.mem id !loan_to_content))
+      meta;
     loan_to_content := BorrowId.Map.add id lc !loan_to_content;
     borrows_loans := LoanId id :: !borrows_loans
   in
   let push_borrow id (bc : g_borrow_content_with_ty) : unit =
     sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem id !borrows)) meta;
     borrows := BorrowId.Set.add id !borrows;
-    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem id !borrow_to_content)) meta;
+    sanity_check __FILE__ __LINE__
+      (not (BorrowId.Map.mem id !borrow_to_content))
+      meta;
     borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
     borrows_loans := BorrowId id :: !borrows_loans
   in
@@ -2129,7 +2160,9 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx)
 
       method! visit_symbolic_value _ sv =
         (* Sanity check: no borrows *)
-        sanity_check __FILE__ __LINE__ (not (symbolic_value_has_borrows ctx sv)) meta
+        sanity_check __FILE__ __LINE__
+          (not (symbolic_value_has_borrows ctx sv))
+          meta
     end
   in
 
@@ -2240,7 +2273,9 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
   if merge_funs = None then
-    (sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint borrows0 borrows1) meta;
+    (sanity_check __FILE__ __LINE__
+       (BorrowId.Set.disjoint borrows0 borrows1)
+       meta;
      sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1))
       meta;
 
@@ -2358,8 +2393,12 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
              to preserve (in practice it works because we destructure the
              shared values in the abstractions, and forbid nested borrows).
           *)
-          sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta;
-          sanity_check __FILE__ __LINE__ (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+          sanity_check __FILE__ __LINE__
+            (not (value_has_loans_or_borrows ctx sv0.value))
+            meta;
+          sanity_check __FILE__ __LINE__
+            (not (value_has_loans_or_borrows ctx sv0.value))
+            meta;
           sanity_check __FILE__ __LINE__ (is_aignored child0.value) meta;
           sanity_check __FILE__ __LINE__ (is_aignored child1.value) meta;
           None)
@@ -2476,7 +2515,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
                               sanity_check __FILE__ __LINE__
                                 (not (BorrowId.Set.is_empty bids))
                                 meta;
-                              sanity_check __FILE__ __LINE__ (is_aignored child.value) meta;
+                              sanity_check __FILE__ __LINE__
+                                (is_aignored child.value) meta;
                               sanity_check __FILE__ __LINE__
                                 (not (value_has_loans_or_borrows ctx sv.value))
                                 meta;
-- 
cgit v1.2.3


From 1a86cac476c1f5c0d64d5a12db267d3ac651561b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 29 Mar 2024 17:49:46 +0100
Subject: Cleanup and fix a mistake

---
 compiler/InterpreterBorrows.ml | 29 +++++++++++++----------------
 1 file changed, 13 insertions(+), 16 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index b32261e6..e593ae75 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -443,8 +443,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta
-    "Only one loan should have been given back";
+  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
@@ -503,7 +502,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   let replaced : bool ref = ref false in
   let set_replaced () =
     cassert __FILE__ __LINE__ (not !replaced) meta
-      "Only one loan should have been updated";
+      "Exacly one loan should be updated";
     replaced := true
   in
   let obj =
@@ -589,7 +588,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta "Only one loan should be given back";
+  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
   (* Return *)
   ctx
 
@@ -608,7 +607,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   let replaced : bool ref = ref false in
   let set_replaced () =
     cassert __FILE__ __LINE__ (not !replaced) meta
-      "Only one loan should be updated";
+      "Exactly one loan should be updated";
     replaced := true
   in
   let obj =
@@ -673,8 +672,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta
-    "Exactly one loan should be given back";
+  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
   (* Return *)
   ctx
 
@@ -1553,8 +1551,8 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
       craise __FILE__ __LINE__ meta
-        "Can't promote a shared loan to a mutable loan if the loan is inside \
-         an abstraction"
+        "Can't promote a shared loan to a mutable loan if the loan is inside a \
+         region abstraction"
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
@@ -1581,7 +1579,7 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
         (* This can't happen for sure *)
         craise __FILE__ __LINE__ meta
           "Can't promote a shared borrow to a mutable borrow if the borrow is \
-           inside an abstraction"
+           inside a region abstraction"
   in
   (* Continue *)
   cf ctx
@@ -1647,7 +1645,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
       craise __FILE__ __LINE__ meta
         "Can't activate a reserved mutable borrow referencing a loan inside\n\
-        \         an abstraction"
+        \         a region abstraction"
 
 let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs =
@@ -2272,12 +2270,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
-  if merge_funs = None then
-    (sanity_check __FILE__ __LINE__
-       (BorrowId.Set.disjoint borrows0 borrows1)
-       meta;
-     sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1))
+  if merge_funs = None then (
+    sanity_check __FILE__ __LINE__
+      (BorrowId.Set.disjoint borrows0 borrows1)
       meta;
+    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) meta);
 
   (* Merge.
      There are several cases:
-- 
cgit v1.2.3