Added sanity_check and sanity_check_opt_meta helpers and changed sani…

…ty checks related cassert to these helpers to have a proper error message

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_ty = TTraitType (c.trait_ref, c.generics, c.type_name) in
     let trait_ty_ref = get_ref trait_ty in
     let ty_ref = get_ref c.ty in

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)
+      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

compiler/Extract.ml

@@ -300,7 +300,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
 
@@ -506,7 +506,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

compiler/ExtractBase.ml

@@ -2036,7 +2036,7 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (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
   let { keep_fwd; fwd = _; backs } = trans_group in

compiler/ExtractTypes.ml

@@ -888,7 +888,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 ();
@@ -1328,7 +1328,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
@@ -1488,7 +1488,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”");

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;

compiler/Interpreter.ml

@@ -612,8 +612,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

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
@@ -1383,9 +1383,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 *)
@@ -1464,7 +1464,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 *)
@@ -1545,9 +1545,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
@@ -1645,7 +1645,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) ->
@@ -1835,7 +1835,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 ->
@@ -2049,7 +2049,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
 
@@ -2154,8 +2154,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:
@@ -2457,7 +2457,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
 

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
 

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