diff options
| -rw-r--r-- | compiler/AssociatedTypes.ml | 2 | ||||
| -rw-r--r-- | compiler/Errors.ml | 8 | ||||
| -rw-r--r-- | compiler/Extract.ml | 4 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 2 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 6 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 2 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 54 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 18 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.ml | 20 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 10 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 15 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 4 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 4 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 6 | ||||
| -rw-r--r-- | compiler/RegionsHierarchy.ml | 4 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 16 |
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 |