Added sanity_check and sanity_check_opt_meta helpers and changed sanity checks related cassert to these helpers to have a proper error message

23 files changed, 113 insertions, 108 deletions

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 0ed46e8c..70739b3c 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -51,7 +51,7 @@ let compute_norm_trait_types_from_preds (meta : Meta.meta option)
     (* Sanity check: the type constraint can't make use of regions - Remark
        that it would be enough to only visit the field [ty] of the trait type
        constraint, but for safety we visit all the fields *)
-    cassert_opt_meta (trait_type_constraint_no_regions c) meta "TODO: error message";
+    sanity_check_opt_meta (trait_type_constraint_no_regions c) meta;
     let { trait_ref; type_name; ty } : trait_type_constraint = c in
     let trait_ty = TTraitType (trait_ref, type_name) in
     let trait_ty_ref = get_ref trait_ty in
diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 8fb65bc1..4c51720f 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -39,4 +39,10 @@ let cassert_opt_meta (b : bool) (meta : Meta.meta option) (msg : string) =
   | None -> 
     if b then 
       let () = save_error (None) msg in  
-      raise (CFailure msg)
\ No newline at end of file
+      raise (CFailure msg)
+
+let sanity_check b meta = cassert b meta "Internal error, please file an issue"
+let sanity_check_opt_meta b meta = cassert_opt_meta b meta "Internal error, please file an issue"
+
+let exec_raise = craise
+let exec_assert = cassert
\ No newline at end of file
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 564ffafb..82656273 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -277,7 +277,7 @@ let lets_require_wrap_in_do (meta : Meta.meta) (lets : (bool * typed_pattern * t
   | HOL4 ->
       (* HOL4 is similar to HOL4, but we add a sanity check *)
       let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in
-      if wrap_in_do then cassert (List.for_all (fun (m, _, _) -> m) lets) meta "TODO: error message";
+      if wrap_in_do then sanity_check (List.for_all (fun (m, _, _) -> m) lets) meta;
       wrap_in_do
   | FStar | Coq -> false
 
@@ -478,7 +478,7 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.for
           F.pp_print_string fmt fun_name);
 
       (* Sanity check: HOL4 doesn't support const generics *)
-      cassert (generics.const_generics = [] || !backend <> HOL4) meta "TODO: error message";
+      sanity_check (generics.const_generics = [] || !backend <> HOL4) meta;
       (* Print the generics.
 
          We might need to filter some of the type arguments, if the type
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index c2e3e35f..1c21e99c 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1904,7 +1904,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
 let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
   (* Sanity check: the function should not be a global body - those are handled
    * separately *)
-  cassert (not def.is_global_decl_body) def.meta "The function should not be a global body - those are handled separately";
+  sanity_check (not def.is_global_decl_body) def.meta;
   (* Lookup the LLBC def to compute the region group information *)
   let def_id = def.def_id in
   (* Add the function name *)
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index b26704ce..02aaec65 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -878,7 +878,7 @@ let extract_type_decl_variant (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F
     List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
   in
   (* Sanity check: HOL4 doesn't support const generics *)
-  cassert (cg_params = [] || !backend <> HOL4) meta "TODO: Error message";
+  sanity_check (cg_params = [] || !backend <> HOL4) meta;
   (* Print the final type *)
   if !backend <> HOL4 then (
     F.pp_print_space fmt ();
@@ -1324,7 +1324,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
     (extract_body : bool) : unit =
   (* Sanity check *)
-  cassert (extract_body || !backend <> HOL4) def.meta "TODO: error message";
+  sanity_check (extract_body || !backend <> HOL4) def.meta;
   let is_tuple_struct =
     TypesUtils.type_decl_from_decl_id_is_tuple_struct
       ctx.trans_ctx.type_ctx.type_infos def.def_id
@@ -1489,7 +1489,7 @@ let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
   (* Retrieve the definition name *)
   let def_name = ctx_get_local_type def.meta def.def_id ctx in
   (* Sanity check *)
-  cassert (def.generics = empty_generic_params) def.meta "TODO: error message";
+  sanity_check (def.generics = empty_generic_params) def.meta;
   (* Generate the declaration *)
   F.pp_print_space fmt ();
   F.pp_print_string fmt ("Type " ^ def_name ^ " = “: unit”");
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 14185a3d..f3840a8c 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -145,7 +145,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
         end
       in
       (* Sanity check: global bodies don't contain stateful calls *)
-      cassert ((not f.is_global_decl_body) || not !stateful) f.meta "Global bodies should not contain stateful calls";
+      sanity_check ((not f.is_global_decl_body) || not !stateful) f.meta;
       let builtin_info = get_builtin_info f in
       let has_builtin_info = builtin_info <> None in
       group_has_builtin_info := !group_has_builtin_info || has_builtin_info;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 2ac772ae..0bbde79c 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -628,8 +628,8 @@ module Test = struct
             fdef.name));
 
     (* Sanity check - *)
-    cassert (fdef.signature.generics = empty_generic_params) fdef.meta "TODO: Error message";
-    cassert (body.arg_count = 0) fdef.meta "TODO: Error message";
+    sanity_check (fdef.signature.generics = empty_generic_params) fdef.meta;
+    sanity_check (body.arg_count = 0) fdef.meta;
 
     (* Create the evaluation context *)
     let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in
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
 
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index a9a98b5c..d61e0bd1 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -100,7 +100,7 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) (combine : bool -> bool
     =
   let compare = compare_rtys meta default combine compare_regions in
   (* Sanity check - TODO: don't do this at every recursive call *)
-  cassert (ty_is_rty ty1 && ty_is_rty ty2) meta "ty1 or ty2 are not rty TODO: Error message";
+  sanity_check (ty_is_rty ty1 && ty_is_rty ty2) meta;
   (* Normalize the associated types *)
   match (ty1, ty2) with
   | TLiteral lit1, TLiteral lit2 ->
@@ -144,7 +144,7 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) (combine : bool -> bool
       combine params_b tys_b
   | TRef (r1, ty1, kind1), TRef (r2, ty2, kind2) ->
       (* Sanity check *)
-      cassert (kind1 = kind2) meta "kind1 and kind2 are not equal TODO: Error message";
+      sanity_check (kind1 = kind2) meta;
       (* Explanation for the case where we check if projections intersect:
        * the projections intersect if the borrows intersect or their contents
        * intersect. *)
@@ -795,7 +795,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) (can_update_shared : bo
   (* Small helpers for sanity checks *)
   let shared = ref None in
   let add_shared () =
-    match !shared with None -> shared := Some true | Some b -> cassert b meta "TODO :  error message "
+    match !shared with None -> shared := Some true | Some b -> sanity_check b meta
   in
   let set_non_shared () =
     match !shared with
@@ -821,7 +821,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta) (can_update_shared : bo
 
       method! visit_abstract_shared_borrows abs asb =
         (* Sanity check *)
-        (match !shared with Some b -> cassert b meta "TODO :  error message " | _ -> ());
+        (match !shared with Some b -> sanity_check  b meta | _ -> ());
         (* Explore *)
         if can_update_shared then
           let abs = Option.get abs in
@@ -1063,7 +1063,7 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb
   (* Apply *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Sanity check *)
-  cassert !found meta "TODO :  error message ";
+  sanity_check !found meta;
   (* Return *)
   ctx
 
@@ -1112,7 +1112,7 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : sy
   (* Apply *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Sanity check *)
-  cassert !found meta "TODO :  error message ";
+  sanity_check !found meta;
   (* Return *)
   ctx
 
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 2f886714..086c0786 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -557,7 +557,7 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv
             ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
         (* Sanity check: the symbolic value has disappeared *)
-        cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "TODO: error message")
+        sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
   in
   (* Continue *)
   cc cf ctx
@@ -594,7 +594,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_valu
     (tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
     (cf_after_join : st_m_fun) : m_fun =
   (* Sanity check *)
-  cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "TODO: error message";
+  sanity_check (sv.sv_ty = TLiteral (TInteger int_type)) meta;
   (* For all the branches of the switch, we expand the symbolic value
    * to the value given by the branch and execute the branch statement.
    * For the otherwise branch, we leave the symbolic value as it is
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 6c4f8af5..3922a3ab 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -137,7 +137,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
       | TAdt (TAssumed TBox, _) ->
           craise meta "Can't copy an assumed value other than Option"
       | TAdt (TAdtId _, _) as ty ->
-          cassert (allow_adt_copy || ty_is_primitively_copyable ty) meta "TODO: error message"
+        sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta
       | TAdt (TTuple, _) -> () (* Ok *)
       | TAdt
           ( TAssumed (TSlice | TArray),
@@ -147,7 +147,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
               const_generics = [];
               trait_refs = [];
             } ) ->
-          cassert (ty_is_primitively_copyable ty) meta "TODO: error message"
+            sanity_check (ty_is_primitively_copyable ty) meta
       | _ -> craise meta "Unreachable");
       let ctx, fields =
         List.fold_left_map
@@ -330,11 +330,11 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
       let copy cf v : m_fun =
        fun ctx ->
         (* Sanity checks *)
-        cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message";
-        cassert (
+        sanity_check (not (bottom_in_value ctx.ended_regions v)) meta;
+        sanity_check (
           Option.is_none
             (find_first_primitively_copyable_sv_with_borrows
-               ctx.type_ctx.type_infos v)) meta "TODO: error message";
+               ctx.type_ctx.type_infos v)) meta;
         (* Actually perform the copy *)
         let allow_adt_copy = false in
         let ctx, v = copy_value meta allow_adt_copy config ctx v in
@@ -737,9 +737,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
         | TAdtId def_id ->
             (* Sanity checks *)
             let type_decl = ctx_lookup_type_decl ctx def_id in
-            cassert (
+            sanity_check (
               List.length type_decl.generics.regions
-              = List.length generics.regions) meta "TODO: error message";
+              = List.length generics.regions) meta;
             let expected_field_types =
               AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id
                 opt_variant_id generics
@@ -758,10 +758,10 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
         | TAssumed _ -> craise meta "Unreachable")
     | AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
-        cassert (List.for_all (fun (v : typed_value) -> v.ty = ety) values) meta "All the values do not have the proper type";
+        sanity_check (List.for_all (fun (v : typed_value) -> v.ty = ety) values) meta;
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
-        cassert (len = Z.of_int (List.length values)) meta "The number of values is not consistent with the length";
+        sanity_check (len = Z.of_int (List.length values)) meta;
         let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
         let ty = TAdt (TAssumed TArray, generics) in
         (* In order to generate a better AST, we introduce a symbolic
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index ef2c5698..44b9a44e 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -267,9 +267,9 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
     borrow_substs := (lid, nlid) :: !borrow_substs;
 
     (* Rem.: the below sanity checks are not really necessary *)
-    cassert (AbstractionId.Set.is_empty abs.parents) meta "abs.parents is not empty TODO: Error message";
-    cassert (abs.original_parents = []) meta "original_parents is not empty TODO: Error message";
-    cassert (RegionId.Set.is_empty abs.ancestors_regions) meta "ancestors_regions is not empty TODO: Error message";
+    sanity_check (AbstractionId.Set.is_empty abs.parents) meta;
+    sanity_check (abs.original_parents = []) meta;
+    sanity_check (RegionId.Set.is_empty abs.ancestors_regions) meta;
 
     (* Introduce the new abstraction for the shared values *)
     cassert (ty_no_regions sv.ty) meta "TODO :  error message ";
@@ -323,7 +323,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
   let collect_shared_values_in_abs (abs : abs) : unit =
     let collect_shared_value lids (sv : typed_value) =
       (* Sanity check: we don't support nested borrows for now *)
-      cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows not supported yet";
+      sanity_check (not (value_has_borrows ctx sv.value)) meta;
 
       (* Filter the loan ids whose corresponding borrows appear in abstractions
          (see the documentation of the function) *)
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index c4709b7e..74d31975 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -307,8 +307,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
   *)
   let merge_amut_borrows id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
-    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
+    sanity_check (is_aignored child0.value) meta;
+    sanity_check (is_aignored child1.value) meta;
 
     (* We need to pick a type for the avalue. The types on the left and on the
        right may use different regions: it doesn't really matter (here, we pick
@@ -326,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
     let _ =
       let _, ty0, _ = ty_as_ref ty0 in
       let _, ty1, _ = ty_as_ref ty1 in
-      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta "TODO: error message";
-      cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta "TODO: error message"
+      sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty0)) meta;
+      sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty1)) meta
     in
 
     (* Same remarks as for [merge_amut_borrows] *)
@@ -338,8 +338,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
 
   let merge_amut_loans id ty0 child0 _ty1 child1 =
     (* Sanity checks *)
-    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
-    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
+    sanity_check (is_aignored child0.value) meta;
+    sanity_check (is_aignored child1.value) meta;
     (* Same remarks as for [merge_amut_borrows] *)
     let ty = ty0 in
     let child = child0 in
@@ -349,8 +349,8 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
   let merge_ashared_loans ids ty0 (sv0 : typed_value) child0 _ty1
       (sv1 : typed_value) child1 =
     (* Sanity checks *)
-    cassert (is_aignored child0.value) meta "Children are not [AIgnored]";
-    cassert (is_aignored child1.value) meta "Children are not [AIgnored]";
+    sanity_check (is_aignored child0.value) meta;
+    sanity_check (is_aignored child1.value) meta;
     (* Same remarks as for [merge_amut_borrows].
 
        This time we need to also merge the shared values. We rely on the
@@ -425,9 +425,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
           (* Variables are necessarily in the prefix *)
           craise meta "Unreachable"
       | EBinding (BDummy did, _) ->
-          cassert (not (DummyVarId.Set.mem did fixed_ids.dids)) meta "TODO: error message"
+          sanity_check (not (DummyVarId.Set.mem did fixed_ids.dids)) meta
       | EAbs abs ->
-          cassert (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta "TODO: error message"
+          sanity_check (not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)) meta
       | EFrame ->
           (* This should have been eliminated *)
           craise meta "Unreachable"
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 2e700c50..435174a7 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -43,8 +43,8 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
          match Id0.Map.find_opt id0 !map with
          | None -> ()
          | Some set ->
-             cassert (
-               (not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta "TODO: error message");
+            sanity_check (
+               (not check_not_already_registered) || not (Id1.Set.mem id1 set)) meta);
       (* Update the mapping *)
       map :=
         Id0.Map.update id0
@@ -53,10 +53,10 @@ let compute_abs_borrows_loans_maps (meta : Meta.meta) (no_duplicates : bool)
             | None -> Some (Id1.Set.singleton id1)
             | Some ids ->
                 (* Sanity check *)
-                cassert (not check_singleton_sets) meta "TODO: error message";
-                cassert (
+                sanity_check (not check_singleton_sets) meta;
+                sanity_check (
                   (not check_not_already_registered)
-                  || not (Id1.Set.mem id1 ids)) meta "TODO: error message";
+                  || not (Id1.Set.mem id1 ids)) meta;
                 (* Update *)
                 Some (Id1.Set.add id1 ids))
           !map
@@ -691,7 +691,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     let id1 = sv1.sv_id in
     if id0 = id1 then (
       (* Sanity check *)
-      cassert (sv0 = sv1) meta "TODO: error message";
+      sanity_check (sv0 = sv1) meta;
       (* Return *)
       sv0)
     else (
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 6ec12d6f..3733c06d 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -603,7 +603,7 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place)
         (* Reinsert *)
         let ctx = write_place meta access p v ctx in
         (* Sanity check *)
-        cassert (not (outer_loans_in_value v)) meta "TODO: Error message";
+        sanity_check (not (outer_loans_in_value v)) meta;
         (* Continue *)
         cf ctx)
   in
@@ -627,7 +627,7 @@ let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_
    fun ctx ->
     let v = read_place meta access p ctx in
     (* Sanity checks *)
-    cassert (not (outer_loans_in_value v)) meta "TODO: Error message";
+    sanity_check (not (outer_loans_in_value v)) meta;
     (* Continue *)
     cf v ctx
   in
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 7eaa7659..5f83b938 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -18,7 +18,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
   (* Sanity check - TODO: move those elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Subst.erase_regions ty in
-  cassert (ty_is_rty ty && ety = v.ty) meta "TODO: error message";
+  sanity_check (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then []
   else
@@ -95,7 +95,7 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
-  cassert (ty_is_rty ty && ety = v.ty) meta "TODO: error message";
+  sanity_check (ty_is_rty ty && ety = v.ty) meta;
   (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then { value = AIgnored; ty }
   else
@@ -261,7 +261,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
     (original_sv_ty : rty) : typed_avalue =
   (* Sanity check: if we have a proj_loans over a symbolic value, it should
    * contain regions which we will project *)
-  cassert (ty_has_regions_in_set regions original_sv_ty) meta "TODO: error message";
+  sanity_check (ty_has_regions_in_set regions original_sv_ty) meta;
   (* Match *)
   let (value, ty) : avalue * ty =
     match (see, original_sv_ty) with
@@ -276,7 +276,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
         (AAdt { variant_id; field_values }, original_sv_ty)
     | SeMutRef (bid, spc), TRef (r, ref_ty, RMut) ->
         (* Sanity check *)
-        cassert (spc.sv_ty = ref_ty) meta "TODO: error message";
+        sanity_check (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
@@ -294,7 +294,7 @@ let apply_proj_loans_on_symbolic_expansion (meta : Meta.meta) (regions : RegionI
           (ALoan (AIgnoredMutLoan (opt_bid, child_av)), ref_ty)
     | SeSharedRef (bids, spc), TRef (r, ref_ty, RShared) ->
         (* Sanity check *)
-        cassert (spc.sv_ty = ref_ty) meta "TODO: error message";
+        sanity_check (spc.sv_ty = ref_ty) meta;
         (* Apply the projector to the borrowed value *)
         let child_av = mk_aproj_loans_value_from_symbolic_value regions spc in
         (* Check if the region is in the set of projected regions (note that
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 0d0fd0a5..5e8f7c55 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -354,7 +354,7 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool)
         match ret_value with
         | None -> ()
         | Some ret_value ->
-            cassert (not (bottom_in_value ctx.ended_regions ret_value)) meta "TODO: Error message" )
+          sanity_check (not (bottom_in_value ctx.ended_regions ret_value)) meta)
   in
 
   (* Drop the outer *loans* we find in the local variables *)
@@ -504,8 +504,7 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) (fi
       let generics = func.generics in
       (* Sanity check: we don't fully handle the const generic vars environment
          in concrete mode yet *)
-      cassert (generics.const_generics = []) meta "The const generic vars environment
-    in concrete mode is not fully handled yet";
+         sanity_check (generics.const_generics = []) meta;
       (* There are two cases (and this is extremely annoying):
          - the function is not box_free
          - the function is box_free
@@ -1111,7 +1110,7 @@ and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : st_cm_f
               (* Evaluate the branch *)
               let cf_eval_branch cf =
                 (* Sanity check *)
-                cassert (sv.int_ty = int_ty) meta "TODO: Error message";
+                sanity_check (sv.int_ty = int_ty) meta;
                 (* Find the branch *)
                 match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with
                 | None -> eval_statement config otherwise cf
@@ -1236,7 +1235,7 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta)
       let generics = func.generics in
       (* Sanity check: we don't fully handle the const generic vars environment
          in concrete mode yet *)
-      cassert (generics.const_generics = []) meta "The const generic vars environment in concrete mode is not fully handled yet";
+         sanity_check (generics.const_generics = []) meta;
       fun cf ctx ->
         (* Retrieve the (correctly instantiated) body *)
         let def = ctx_lookup_fun_decl ctx fid in
@@ -1323,7 +1322,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
     eval_transparent_function_call_symbolic_inst meta call ctx
   in
   (* Sanity check *)
-  cassert (List.length call.args = List.length def.signature.inputs) def.meta "TODO: Error message";
+  sanity_check (List.length call.args = List.length def.signature.inputs) def.meta;
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config def.meta func def.signature
     regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
@@ -1495,10 +1494,10 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) (fi
   let dest = call.dest in
   (* Sanity check: make sure the type parameters don't contain regions -
    * this is a current limitation of our synthesis *)
-  cassert (
+   sanity_check (
     List.for_all
       (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty))
-      generics.types) meta "The parameters should not contain regions TODO: error message";
+      generics.types) meta;
 
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index b5402bb0..be8400f7 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -79,7 +79,7 @@ let mk_place_from_var_id (var_id : VarId.id) : place =
 (** Create a fresh symbolic value *)
 let mk_fresh_symbolic_value (meta : Meta.meta)  (ty : ty) : symbolic_value =
   (* Sanity check *)
-  cassert (ty_is_rty ty) meta "TODO: error message";
+  sanity_check (ty_is_rty ty) meta;
   let sv_id = fresh_symbolic_value_id () in
   let svalue = { sv_id; sv_ty = ty } in
   svalue
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index a8077ab7..50f008b8 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -105,8 +105,8 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
     let reprs = !ids_reprs in
     let infos = !borrows_infos in
     (* Sanity checks *)
-    cassert (not (BorrowId.Map.mem bid reprs)) meta "TODO: Error message";
-    cassert (not (BorrowId.Map.mem bid infos)) meta "TODO: Error message";
+    sanity_check (not (BorrowId.Map.mem bid reprs)) meta;
+    sanity_check (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 *)
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 2fb33036..d7423441 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1240,10 +1240,10 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     if List.for_all (fun (_, y) -> y = x) end_args then (
                       (* We can substitute *)
                       (* Sanity check: all types correct *)
-                      cassert (
+                      sanity_check (
                         List.for_all
                           (fun (generics1, _) -> generics1 = generics)
-                          args) def.meta "All types are not correct";
+                          args) def.meta;
                       { e with e = Var x })
                     else super#visit_texpression env e
                   else super#visit_texpression env e
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 05373ce8..0f9c2dfe 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -426,14 +426,14 @@ let iter_switch_body_branches (f : texpression -> unit) (sb : switch_body) :
 let mk_switch (meta : Meta.meta) (scrut : texpression) (sb : switch_body) : texpression =
   (* Sanity check: the scrutinee has the proper type *)
   (match sb with
-  | If (_, _) -> cassert (scrut.ty = TLiteral TBool) meta "The scrutinee does not have the proper type"
+  | If (_, _) -> sanity_check (scrut.ty = TLiteral TBool) meta
   | Match branches ->
       List.iter
-        (fun (b : match_branch) -> cassert (b.pat.ty = scrut.ty) meta "The scrutinee does not have the proper type")
+        (fun (b : match_branch) -> sanity_check (b.pat.ty = scrut.ty) meta)
         branches);
   (* Sanity check: all the branches have the same type *)
   let ty = get_switch_body_ty sb in
-  iter_switch_body_branches (fun e -> cassert (e.ty = ty) meta "All branches should have the same type") sb;
+  iter_switch_body_branches (fun e -> sanity_check (e.ty = ty) meta) sb;
   (* Put together *)
   let e = Switch (scrut, sb) in
   { e; ty }
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index 0672a25f..f4e2ff35 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -107,8 +107,8 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty
 
   let add_edge ~(short : region) ~(long : region) =
     (* Sanity checks *)
-    cassert_opt_meta (short <> RErased) meta "TODO: Error message";
-    cassert_opt_meta (long <> RErased) meta "TODO: Error message";
+    sanity_check_opt_meta (short <> RErased) meta;
+    sanity_check_opt_meta (long <> RErased) meta;
     (* Ignore the locally bound regions (at the level of arrow types for instance *)
     match (short, long) with
     | RBVar _, _ | _, RBVar _ -> ()
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index b62966bd..46058a9a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2019,7 +2019,7 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
     | Some _ ->
         (* Backward function *)
         (* Sanity check *)
-        cassert (opt_v = None) ctx.fun_decl.meta "TODO: Error message";
+        sanity_check (opt_v = None) ctx.fun_decl.meta;
         (* Group the variables in which we stored the values we need to give back.
            See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
         let backward_outputs = Option.get ctx.backward_outputs in
@@ -2429,7 +2429,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
   (* TODO: normalize the types *)
   if !Config.type_check_pure_code then
     List.iter
-      (fun (var, v) -> cassert ((var : var).ty = (v : texpression).ty) ctx.fun_decl.meta "TODO: error message")
+      (fun (var, v) -> sanity_check ((var : var).ty = (v : texpression).ty) ctx.fun_decl.meta)
       variables_values;
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
@@ -2584,7 +2584,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
           ^ pure_ty_to_string ctx given_back.ty
           ^ "\n- sig input ty: "
           ^ pure_ty_to_string ctx input.ty));
-      cassert (given_back.ty = input.ty) ctx.fun_decl.meta "TODO: error message")
+      sanity_check (given_back.ty = input.ty) ctx.fun_decl.meta)
     given_back_inputs;
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
@@ -2799,7 +2799,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
           let branch = List.hd branches in
           let ty = branch.branch.ty in
           (* Sanity check *)
-          cassert (List.for_all (fun br -> br.branch.ty = ty) branches) ctx.fun_decl.meta "There should be at least one branch";
+          sanity_check (List.for_all (fun br -> br.branch.ty = ty) branches) ctx.fun_decl.meta;
           (* Return *)
           { e; ty })
   | ExpandBool (true_e, false_e) ->
@@ -3377,11 +3377,11 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   in
 
   (* Sanity check: all the non-fresh symbolic values are in the context *)
-  cassert (
+  sanity_check (
     List.for_all
       (fun (sv : V.symbolic_value) ->
         V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var)
-      loop.input_svalues) ctx.fun_decl.meta "All the non-fresh symbolic values should be in the context";
+      loop.input_svalues) ctx.fun_decl.meta;
 
   (* Translate the loop inputs *)
   let inputs =
@@ -3736,10 +3736,10 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
                 (List.map (pure_ty_to_string ctx) signature.inputs)));
         (* TODO: we need to normalize the types *)
         if !Config.type_check_pure_code then
-          cassert (
+          sanity_check (
             List.for_all
               (fun (var, ty) -> (var : var).ty = ty)
-              (List.combine inputs signature.inputs)) def.meta "TODO: error message";
+              (List.combine inputs signature.inputs)) def.meta;
         Some { inputs; inputs_lvs; body }
   in