Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

1 files changed, 190 insertions, 124 deletions

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index b87cdff7..642d7a37 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -8,6 +8,7 @@ open Cps
 open TypesUtils
 open InterpreterUtils
 open InterpreterBorrowsCore
+open Errors
 
 (** The local logger *)
 let log = Logging.invariants_log
@@ -47,14 +48,16 @@ type borrow_kind = BMut | BShared | BReserved
     - loans and borrows are correctly related
     - a two-phase borrow can't point to a value inside an abstraction
  *)
-let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
+let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
+    unit =
   (* Link all the borrow ids to a representant - necessary because of shared
    * borrows/loans *)
   let ids_reprs : BorrowId.id BorrowId.Map.t ref = ref BorrowId.Map.empty in
   (* Link all the id representants to a borrow information *)
   let borrows_infos : borrow_info BorrowId.Map.t ref = ref BorrowId.Map.empty in
   let context_to_string () : string =
-    eval_ctx_to_string ctx ^ "- representants:\n"
+    eval_ctx_to_string ~meta:(Some meta) ctx
+    ^ "- representants:\n"
     ^ ids_reprs_to_string "  " !ids_reprs
     ^ "\n- info:\n"
     ^ borrows_infos_to_string "  " !borrows_infos
@@ -76,12 +79,12 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
     let infos = !borrows_infos in
     (* Use the first borrow id as representant *)
     let repr_bid = BorrowId.Set.min_elt bids in
-    assert (not (BorrowId.Map.mem repr_bid infos));
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem repr_bid infos)) meta;
     (* Insert the mappings to the representant *)
     let reprs =
       BorrowId.Set.fold
         (fun bid reprs ->
-          assert (not (BorrowId.Map.mem bid reprs));
+          sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) meta;
           BorrowId.Map.add bid repr_bid reprs)
         bids reprs
     in
@@ -104,8 +107,8 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
     let reprs = !ids_reprs in
     let infos = !borrows_infos in
     (* Sanity checks *)
-    assert (not (BorrowId.Map.mem bid reprs));
-    assert (not (BorrowId.Map.mem bid infos));
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid reprs)) meta;
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Map.mem bid infos)) meta;
     (* Add the mapping for the representant *)
     let reprs = BorrowId.Map.add bid bid reprs in
     (* Add the mapping for the loan info *)
@@ -183,7 +186,7 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
           ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
         in
         log#serror err;
-        raise (Failure err)
+        craise __FILE__ __LINE__ meta err
   in
 
   let update_info (bid : BorrowId.id) (info : borrow_info) : unit =
@@ -195,7 +198,7 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
         (fun x ->
           match x with
           | Some _ -> Some info
-          | None -> raise (Failure "Unreachable"))
+          | None -> craise __FILE__ __LINE__ meta "Unreachable")
         !borrows_infos
     in
     borrows_infos := infos
@@ -209,12 +212,14 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
     (* Check that the borrow kind is consistent *)
     (match (info.loan_kind, kind) with
     | RShared, (BShared | BReserved) | RMut, BMut -> ()
-    | _ -> raise (Failure "Invariant not satisfied"));
+    | _ -> craise __FILE__ __LINE__ meta "Invariant not satisfied");
     (* A reserved borrow can't point to a value inside an abstraction *)
-    assert (kind <> BReserved || not info.loan_in_abs);
+    sanity_check __FILE__ __LINE__
+      (kind <> BReserved || not info.loan_in_abs)
+      meta;
     (* Insert the borrow id *)
     let borrow_ids = info.borrow_ids in
-    assert (not (BorrowId.Set.mem bid borrow_ids));
+    sanity_check __FILE__ __LINE__ (not (BorrowId.Set.mem bid borrow_ids)) meta;
     let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in
     (* Update the info in the map *)
     update_info bid info
@@ -269,7 +274,7 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
   List.iter
     (fun (rkind, bid) ->
       let info = find_info bid in
-      assert (info.loan_kind = rkind))
+      sanity_check __FILE__ __LINE__ (info.loan_kind = rkind) meta)
     !ignored_loans;
 
   (* Then, check the borrow infos *)
@@ -277,11 +282,15 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
     (fun _ info ->
       (* Note that we can't directly compare the sets - I guess they are
        * different depending on the order in which we add the elements... *)
-      assert (
-        BorrowId.Set.elements info.loan_ids
-        = BorrowId.Set.elements info.borrow_ids);
+      sanity_check __FILE__ __LINE__
+        (BorrowId.Set.elements info.loan_ids
+        = BorrowId.Set.elements info.borrow_ids)
+        meta;
       match info.loan_kind with
-      | RMut -> assert (BorrowId.Set.cardinal info.loan_ids = 1)
+      | RMut ->
+          sanity_check __FILE__ __LINE__
+            (BorrowId.Set.cardinal info.loan_ids = 1)
+            meta
       | RShared -> ())
     !borrows_infos
 
@@ -289,14 +298,16 @@ let check_loans_borrows_relation_invariant (ctx : eval_ctx) : unit =
     - borrows/loans can't contain ⊥ or reserved mut borrows
     - shared loans can't contain mutable loans
  *)
-let check_borrowed_values_invariant (ctx : eval_ctx) : unit =
+let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
   let visitor =
     object
       inherit [_] iter_eval_ctx as super
 
       method! visit_VBottom info =
         (* No ⊥ inside borrowed values *)
-        assert (Config.allow_bottom_below_borrow || not info.outer_borrow)
+        sanity_check __FILE__ __LINE__
+          (Config.allow_bottom_below_borrow || not info.outer_borrow)
+          meta
 
       method! visit_ABottom _info =
         (* ⊥ inside an abstraction is not the same as in a regular value *)
@@ -309,7 +320,7 @@ let check_borrowed_values_invariant (ctx : eval_ctx) : unit =
           | VSharedLoan (_, _) -> set_outer_shared info
           | VMutLoan _ ->
               (* No mutable loan inside a shared loan *)
-              assert (not info.outer_shared);
+              sanity_check __FILE__ __LINE__ (not info.outer_shared) meta;
               set_outer_mut info
         in
         (* Continue exploring *)
@@ -321,7 +332,7 @@ let check_borrowed_values_invariant (ctx : eval_ctx) : unit =
           match bc with
           | VSharedBorrow _ -> set_outer_shared info
           | VReservedMutBorrow _ ->
-              assert (not info.outer_borrow);
+              sanity_check __FILE__ __LINE__ (not info.outer_borrow) meta;
               set_outer_shared info
           | VMutBorrow (_, _) -> set_outer_mut info
         in
@@ -366,13 +377,15 @@ let check_borrowed_values_invariant (ctx : eval_ctx) : unit =
   let info = { outer_borrow = false; outer_shared = false } in
   visitor#visit_eval_ctx info ctx
 
-let check_literal_type (cv : literal) (ty : literal_type) : unit =
+let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) :
+    unit =
   match (cv, ty) with
-  | VScalar sv, TInteger int_ty -> assert (sv.int_ty = int_ty)
+  | VScalar sv, TInteger int_ty ->
+      sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta
   | VBool _, TBool | VChar _, TChar -> ()
-  | _ -> raise (Failure "Erroneous typing")
+  | _ -> craise __FILE__ __LINE__ meta "Erroneous typing"
 
-let check_typing_invariant (ctx : eval_ctx) : unit =
+let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
   (* TODO: the type of aloans doens't make sense: they have a type
    * of the shape [& (mut) T] where they should have type [T]...
    * This messes a bit the type invariant checks when checking the
@@ -392,60 +405,67 @@ let check_typing_invariant (ctx : eval_ctx) : unit =
 
       method! visit_EBinding info binder v =
         (* We also check that the regions are erased *)
-        assert (ty_is_ety v.ty);
+        sanity_check __FILE__ __LINE__ (ty_is_ety v.ty) meta;
         super#visit_EBinding info binder v
 
       method! visit_symbolic_value inside_abs v =
         (* Check that the types have regions *)
-        assert (ty_is_rty v.sv_ty);
+        sanity_check __FILE__ __LINE__ (ty_is_rty v.sv_ty) meta;
         super#visit_symbolic_value inside_abs v
 
       method! visit_typed_value info tv =
         (* Check that the types have erased regions *)
-        assert (ty_is_ety tv.ty);
+        sanity_check __FILE__ __LINE__ (ty_is_ety tv.ty) meta;
         (* Check the current pair (value, type) *)
         (match (tv.value, tv.ty) with
-        | VLiteral cv, TLiteral ty -> check_literal_type cv ty
+        | VLiteral cv, TLiteral ty -> check_literal_type meta cv ty
         (* ADT case *)
         | VAdt av, TAdt (TAdtId def_id, generics) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
             let def = ctx_lookup_type_decl ctx def_id in
             (* Check the number of parameters *)
-            assert (
-              List.length generics.regions = List.length def.generics.regions);
-            assert (List.length generics.types = List.length def.generics.types);
+            sanity_check __FILE__ __LINE__
+              (List.length generics.regions = List.length def.generics.regions)
+              meta;
+            sanity_check __FILE__ __LINE__
+              (List.length generics.types = List.length def.generics.types)
+              meta;
             (* Check that the variant id is consistent *)
             (match (av.variant_id, def.kind) with
             | Some variant_id, Enum variants ->
-                assert (VariantId.to_int variant_id < List.length variants)
+                sanity_check __FILE__ __LINE__
+                  (VariantId.to_int variant_id < List.length variants)
+                  meta
             | None, Struct _ -> ()
-            | _ -> raise (Failure "Erroneous typing"));
+            | _ -> craise __FILE__ __LINE__ meta "Erroneous typing");
             (* Check that the field types are correct *)
             let field_types =
-              AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def
+              AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def
                 av.variant_id generics
             in
             let fields_with_types = List.combine av.field_values field_types in
             List.iter
-              (fun ((v, ty) : typed_value * ty) -> assert (v.ty = ty))
+              (fun ((v, ty) : typed_value * ty) ->
+                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
               fields_with_types
         (* Tuple case *)
         | VAdt av, TAdt (TTuple, generics) ->
-            assert (generics.regions = []);
-            assert (generics.const_generics = []);
-            assert (av.variant_id = None);
+            sanity_check __FILE__ __LINE__ (generics.regions = []) meta;
+            sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
             let fields_with_types =
               List.combine av.field_values generics.types
             in
             List.iter
-              (fun ((v, ty) : typed_value * ty) -> assert (v.ty = ty))
+              (fun ((v, ty) : typed_value * ty) ->
+                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
               fields_with_types
         (* Assumed type case *)
         | VAdt av, TAdt (TAssumed aty_id, generics) -> (
-            assert (av.variant_id = None);
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
             match
               ( aty_id,
                 av.field_values,
@@ -455,53 +475,62 @@ let check_typing_invariant (ctx : eval_ctx) : unit =
             with
             (* Box *)
             | TBox, [ inner_value ], [], [ inner_ty ], [] ->
-                assert (inner_value.ty = inner_ty)
+                sanity_check __FILE__ __LINE__ (inner_value.ty = inner_ty) meta
             | TArray, inner_values, _, [ inner_ty ], [ cg ] ->
                 (* *)
-                assert (
-                  List.for_all
-                    (fun (v : typed_value) -> v.ty = inner_ty)
-                    inner_values);
+                sanity_check __FILE__ __LINE__
+                  (List.for_all
+                     (fun (v : typed_value) -> v.ty = inner_ty)
+                     inner_values)
+                  meta;
                 (* The length is necessarily concrete *)
                 let len =
                   (ValuesUtils.literal_as_scalar
                      (TypesUtils.const_generic_as_literal cg))
                     .value
                 in
-                assert (Z.of_int (List.length inner_values) = len)
-            | (TSlice | TStr), _, _, _, _ -> raise (Failure "Unexpected")
-            | _ -> raise (Failure "Erroneous type"))
+                sanity_check __FILE__ __LINE__
+                  (Z.of_int (List.length inner_values) = len)
+                  meta
+            | (TSlice | TStr), _, _, _, _ ->
+                craise __FILE__ __LINE__ meta "Unexpected"
+            | _ -> craise __FILE__ __LINE__ meta "Erroneous type")
         | VBottom, _ -> (* Nothing to check *) ()
         | VBorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | VSharedBorrow bid, RShared | VReservedMutBorrow bid, RMut -> (
                 (* Lookup the borrowed value to check it has the proper type *)
-                let _, glc = lookup_loan ek_all bid ctx in
+                let _, glc = lookup_loan meta ek_all bid ctx in
                 match glc with
                 | Concrete (VSharedLoan (_, sv))
                 | Abstract (ASharedLoan (_, sv, _)) ->
-                    assert (sv.ty = ref_ty)
-                | _ -> raise (Failure "Inconsistent context"))
+                    sanity_check __FILE__ __LINE__ (sv.ty = ref_ty) meta
+                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
             | VMutBorrow (_, bv), RMut ->
-                assert (
-                  (* Check that the borrowed value has the proper type *)
-                  bv.ty = ref_ty)
-            | _ -> raise (Failure "Erroneous typing"))
+                sanity_check __FILE__ __LINE__
+                  ((* Check that the borrowed value has the proper type *)
+                   bv.ty = ref_ty)
+                  meta
+            | _ -> craise __FILE__ __LINE__ meta "Erroneous typing")
         | VLoan lc, ty -> (
             match lc with
-            | VSharedLoan (_, sv) -> assert (sv.ty = ty)
+            | VSharedLoan (_, sv) ->
+                sanity_check __FILE__ __LINE__ (sv.ty = ty) meta
             | VMutLoan bid -> (
                 (* Lookup the borrowed value to check it has the proper type *)
-                let glc = lookup_borrow ek_all bid ctx in
+                let glc = lookup_borrow meta ek_all bid ctx in
                 match glc with
-                | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = ty)
+                | Concrete (VMutBorrow (_, bv)) ->
+                    sanity_check __FILE__ __LINE__ (bv.ty = ty) meta
                 | Abstract (AMutBorrow (_, sv)) ->
-                    assert (Substitute.erase_regions sv.ty = ty)
-                | _ -> raise (Failure "Inconsistent context")))
+                    sanity_check __FILE__ __LINE__
+                      (Substitute.erase_regions sv.ty = ty)
+                      meta
+                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context"))
         | VSymbolic sv, ty ->
             let ty' = Substitute.erase_regions sv.sv_ty in
-            assert (ty' = ty)
-        | _ -> raise (Failure "Erroneous typing"));
+            sanity_check __FILE__ __LINE__ (ty' = ty) meta
+        | _ -> craise __FILE__ __LINE__ meta "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_value info tv
 
@@ -515,7 +544,7 @@ let check_typing_invariant (ctx : eval_ctx) : unit =
        * *)
       method! visit_typed_avalue info atv =
         (* Check that the types have regions *)
-        assert (ty_is_rty atv.ty);
+        sanity_check __FILE__ __LINE__ (ty_is_rty atv.ty) meta;
         (* Check the current pair (value, type) *)
         (match (atv.value, atv.ty) with
         (* ADT case *)
@@ -524,43 +553,51 @@ let check_typing_invariant (ctx : eval_ctx) : unit =
              * parameters, etc. *)
             let def = ctx_lookup_type_decl ctx def_id in
             (* Check the number of parameters *)
-            assert (
-              List.length generics.regions = List.length def.generics.regions);
-            assert (List.length generics.types = List.length def.generics.types);
-            assert (
-              List.length generics.const_generics
-              = List.length def.generics.const_generics);
+            sanity_check __FILE__ __LINE__
+              (List.length generics.regions = List.length def.generics.regions)
+              meta;
+            sanity_check __FILE__ __LINE__
+              (List.length generics.types = List.length def.generics.types)
+              meta;
+            sanity_check __FILE__ __LINE__
+              (List.length generics.const_generics
+              = List.length def.generics.const_generics)
+              meta;
             (* Check that the variant id is consistent *)
             (match (av.variant_id, def.kind) with
             | Some variant_id, Enum variants ->
-                assert (VariantId.to_int variant_id < List.length variants)
+                sanity_check __FILE__ __LINE__
+                  (VariantId.to_int variant_id < List.length variants)
+                  meta
             | None, Struct _ -> ()
-            | _ -> raise (Failure "Erroneous typing"));
+            | _ -> craise __FILE__ __LINE__ meta "Erroneous typing");
             (* Check that the field types are correct *)
             let field_types =
-              AssociatedTypes.type_decl_get_inst_norm_field_rtypes ctx def
+              AssociatedTypes.type_decl_get_inst_norm_field_rtypes meta ctx def
                 av.variant_id generics
             in
             let fields_with_types = List.combine av.field_values field_types in
             List.iter
-              (fun ((v, ty) : typed_avalue * ty) -> assert (v.ty = ty))
+              (fun ((v, ty) : typed_avalue * ty) ->
+                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
               fields_with_types
         (* Tuple case *)
         | AAdt av, TAdt (TTuple, generics) ->
-            assert (generics.regions = []);
-            assert (generics.const_generics = []);
-            assert (av.variant_id = None);
+            sanity_check __FILE__ __LINE__ (generics.regions = []) meta;
+            sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
             (* Check that the fields have the proper values - and check that there
              * are as many fields as field types at the same time *)
             let fields_with_types =
               List.combine av.field_values generics.types
             in
             List.iter
-              (fun ((v, ty) : typed_avalue * ty) -> assert (v.ty = ty))
+              (fun ((v, ty) : typed_avalue * ty) ->
+                sanity_check __FILE__ __LINE__ (v.ty = ty) meta)
               fields_with_types
         (* Assumed type case *)
         | AAdt av, TAdt (TAssumed aty_id, generics) -> (
-            assert (av.variant_id = None);
+            sanity_check __FILE__ __LINE__ (av.variant_id = None) meta;
             match
               ( aty_id,
                 av.field_values,
@@ -570,84 +607,101 @@ let check_typing_invariant (ctx : eval_ctx) : unit =
             with
             (* Box *)
             | TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
-                assert (boxed_value.ty = boxed_ty)
-            | _ -> raise (Failure "Erroneous type"))
+                sanity_check __FILE__ __LINE__ (boxed_value.ty = boxed_ty) meta
+            | _ -> craise __FILE__ __LINE__ meta "Erroneous type")
         | ABottom, _ -> (* Nothing to check *) ()
         | ABorrow bc, TRef (_, ref_ty, rkind) -> (
             match (bc, rkind) with
             | AMutBorrow (_, av), RMut ->
                 (* Check that the child value has the proper type *)
-                assert (av.ty = ref_ty)
+                sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta
             | ASharedBorrow bid, RShared -> (
                 (* Lookup the borrowed value to check it has the proper type *)
-                let _, glc = lookup_loan ek_all bid ctx in
+                let _, glc = lookup_loan meta ek_all bid ctx in
                 match glc with
                 | Concrete (VSharedLoan (_, sv))
                 | Abstract (ASharedLoan (_, sv, _)) ->
-                    assert (sv.ty = Substitute.erase_regions ref_ty)
-                | _ -> raise (Failure "Inconsistent context"))
-            | AIgnoredMutBorrow (_opt_bid, av), RMut -> assert (av.ty = ref_ty)
+                    sanity_check __FILE__ __LINE__
+                      (sv.ty = Substitute.erase_regions ref_ty)
+                      meta
+                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
+            | AIgnoredMutBorrow (_opt_bid, av), RMut ->
+                sanity_check __FILE__ __LINE__ (av.ty = ref_ty) meta
             | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ },
                 RMut ) ->
-                assert (given_back.ty = ref_ty);
-                assert (child.ty = ref_ty)
+                sanity_check __FILE__ __LINE__ (given_back.ty = ref_ty) meta;
+                sanity_check __FILE__ __LINE__ (child.ty = ref_ty) meta
             | AProjSharedBorrow _, RShared -> ()
-            | _ -> raise (Failure "Inconsistent context"))
+            | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
         | ALoan lc, aty -> (
             match lc with
             | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
               -> (
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (child_av.ty = borrowed_aty);
+                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta;
                 (* Lookup the borrowed value to check it has the proper type *)
-                let glc = lookup_borrow ek_all bid ctx in
+                let glc = lookup_borrow meta ek_all bid ctx in
                 match glc with
                 | Concrete (VMutBorrow (_, bv)) ->
-                    assert (bv.ty = Substitute.erase_regions borrowed_aty)
+                    sanity_check __FILE__ __LINE__
+                      (bv.ty = Substitute.erase_regions borrowed_aty)
+                      meta
                 | Abstract (AMutBorrow (_, sv)) ->
-                    assert (
-                      Substitute.erase_regions sv.ty
+                    sanity_check __FILE__ __LINE__
+                      (Substitute.erase_regions sv.ty
                       = Substitute.erase_regions borrowed_aty)
-                | _ -> raise (Failure "Inconsistent context"))
+                      meta
+                | _ -> craise __FILE__ __LINE__ meta "Inconsistent context")
             | AIgnoredMutLoan (None, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (child_av.ty = borrowed_aty)
+                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta
             | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (sv.ty = Substitute.erase_regions borrowed_aty);
+                sanity_check __FILE__ __LINE__
+                  (sv.ty = Substitute.erase_regions borrowed_aty)
+                  meta;
                 (* TODO: the type of aloans doesn't make sense, see above *)
-                assert (child_av.ty = borrowed_aty)
+                sanity_check __FILE__ __LINE__ (child_av.ty = borrowed_aty) meta
             | AEndedMutLoan { given_back; child; given_back_meta = _ }
             | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } ->
                 let borrowed_aty = aloan_get_expected_child_type aty in
-                assert (given_back.ty = borrowed_aty);
-                assert (child.ty = borrowed_aty)
+                sanity_check __FILE__ __LINE__
+                  (given_back.ty = borrowed_aty)
+                  meta;
+                sanity_check __FILE__ __LINE__ (child.ty = borrowed_aty) meta
             | AIgnoredSharedLoan child_av ->
-                assert (child_av.ty = aloan_get_expected_child_type aty))
+                sanity_check __FILE__ __LINE__
+                  (child_av.ty = aloan_get_expected_child_type aty)
+                  meta)
         | ASymbolic aproj, ty -> (
             let ty1 = Substitute.erase_regions ty in
             match aproj with
             | AProjLoans (sv, _) ->
                 let ty2 = Substitute.erase_regions sv.sv_ty in
-                assert (ty1 = ty2);
+                sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
-                assert (ty_has_regions_in_set abs.regions sv.sv_ty)
+                sanity_check __FILE__ __LINE__
+                  (ty_has_regions_in_set abs.regions sv.sv_ty)
+                  meta
             | AProjBorrows (sv, proj_ty) ->
                 let ty2 = Substitute.erase_regions sv.sv_ty in
-                assert (ty1 = ty2);
+                sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
                 (* Also check that the symbolic values contain regions of interest -
                  * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
-                assert (ty_has_regions_in_set abs.regions proj_ty)
+                sanity_check __FILE__ __LINE__
+                  (ty_has_regions_in_set abs.regions proj_ty)
+                  meta
             | AEndedProjLoans (_msv, given_back_ls) ->
                 List.iter
                   (fun (_, proj) ->
                     match proj with
-                    | AProjBorrows (_sv, ty') -> assert (ty' = ty)
+                    | AProjBorrows (_sv, ty') ->
+                        sanity_check __FILE__ __LINE__ (ty' = ty) meta
                     | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()
-                    | _ -> raise (Failure "Unexpected"))
+                    | _ -> craise __FILE__ __LINE__ meta "Unexpected")
                   given_back_ls
             | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
         | AIgnored, _ -> ()
@@ -656,9 +710,9 @@ let check_typing_invariant (ctx : eval_ctx) : unit =
               (lazy
                 ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
                ^ "\n- value: "
-                ^ typed_avalue_to_string ctx atv
+                ^ typed_avalue_to_string ~meta:(Some meta) ctx atv
                 ^ "\n- type: " ^ ty_to_string ctx atv.ty));
-            raise (Failure "Erroneous typing"));
+            craise __FILE__ __LINE__ meta "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
     end
@@ -697,7 +751,7 @@ type sv_info = {
     - the union of the aproj_loans contains the aproj_borrows applied on the
       same symbolic values
  *)
-let check_symbolic_values (ctx : eval_ctx) : unit =
+let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
   (* Small utility *)
   let module M = SymbolicValueId.Map in
   let infos : sv_info M.t ref = ref M.empty in
@@ -765,15 +819,21 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
      *)
     (* A symbolic value can't be both in the regular environment and inside
      * projectors of borrows in abstractions *)
-    assert (info.env_count = 0 || info.aproj_borrows = []);
+    sanity_check __FILE__ __LINE__
+      (info.env_count = 0 || info.aproj_borrows = [])
+      meta;
     (* A symbolic value containing borrows can't be duplicated (i.e., copied):
      * it must be expanded first *)
     if ty_has_borrows ctx.type_ctx.type_infos info.ty then
-      assert (info.env_count <= 1);
+      sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
     (* A duplicated symbolic value is necessarily primitively copyable *)
-    assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty);
+    sanity_check __FILE__ __LINE__
+      (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
+      meta;
 
-    assert (info.aproj_borrows = [] || info.aproj_loans <> []);
+    sanity_check __FILE__ __LINE__
+      (info.aproj_borrows = [] || info.aproj_loans <> [])
+      meta;
     (* At the same time:
      * - check that the loans don't intersect
      * - compute the set of regions for which we project loans
@@ -785,7 +845,9 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
           let regions =
             RegionId.Set.fold
               (fun rid regions ->
-                assert (not (RegionId.Set.mem rid regions));
+                sanity_check __FILE__ __LINE__
+                  (not (RegionId.Set.mem rid regions))
+                  meta;
                 RegionId.Set.add rid regions)
               regions linfo.regions
           in
@@ -795,25 +857,29 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
     (* Check that the union of the loan projectors contains the borrow projections. *)
     List.iter
       (fun binfo ->
-        assert (
-          projection_contains info.ty loan_regions binfo.proj_ty binfo.regions))
+        sanity_check __FILE__ __LINE__
+          (projection_contains meta info.ty loan_regions binfo.proj_ty
+             binfo.regions)
+          meta)
       info.aproj_borrows;
     ()
   in
 
   M.iter check_info !infos
 
-let check_invariants (ctx : eval_ctx) : unit =
+let check_invariants (meta : Meta.meta) (ctx : eval_ctx) : unit =
   if !Config.sanity_checks then (
-    log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx));
-    check_loans_borrows_relation_invariant ctx;
-    check_borrowed_values_invariant ctx;
-    check_typing_invariant ctx;
-    check_symbolic_values ctx)
+    log#ldebug
+      (lazy
+        ("Checking invariants:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+    check_loans_borrows_relation_invariant meta ctx;
+    check_borrowed_values_invariant meta ctx;
+    check_typing_invariant meta ctx;
+    check_symbolic_values meta ctx)
   else log#ldebug (lazy "Not checking invariants (check is not activated)")
 
 (** Same as {!check_invariants}, but written in CPS *)
-let cf_check_invariants : cm_fun =
+let cf_check_invariants (meta : Meta.meta) : cm_fun =
  fun cf ctx ->
-  check_invariants ctx;
+  check_invariants meta ctx;
   cf ctx