diff options
| author | Escherichia | 2024-03-28 13:56:31 +0100 |
|---|---|---|
| committer | Escherichia | 2024-03-28 15:45:45 +0100 |
| commit | 5ad671a0960692af1c00609fa6864c6f44ca299c (patch) | |
| tree | 2c210b418d8b417ace12a95c1707095c47861c1b | |
| parent | 0f0082c81db8852dff23cd4691af19c434c8be78 (diff) | |
Should answer all comments, there are still some TODO: error message left
Diffstat (limited to '')
37 files changed, 882 insertions, 877 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 70739b3c..a4b0e921 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -239,7 +239,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = match trait_ref.trait_id with | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ } -> - cassert_opt_meta (ref_generics = empty_generic_args) ctx.meta "Higher order types are not supported yet TODO: error message"; + cassert_opt_meta (ref_generics = empty_generic_args) ctx.meta "Higher order trait types are not supported yet"; log#ldebug (lazy ("norm_ctx_normalize_ty: trait type: trait ref: " @@ -279,7 +279,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = ^ trait_ref_to_string ctx trait_ref ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* We can't project *) - cassert_opt_meta (trait_instance_id_is_local_clause trait_ref.trait_id) ctx.meta "TODO: error message"; + sanity_check_opt_meta (trait_instance_id_is_local_clause trait_ref.trait_id) ctx.meta ; TTraitType (trait_ref, type_name) in let tr : trait_type_ref = { trait_ref; type_name } in @@ -347,7 +347,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) match impl with | None -> (* This is actually a local clause *) - cassert_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta "TODO: error message"; + sanity_check_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta ; (ParentClause (inst_id, decl_id, clause_id), None) | Some impl -> (* We figure out the parent clause by doing the following: @@ -378,7 +378,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) match impl with | None -> (* This is actually a local clause *) - cassert_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta "Trait instance id is not a local clause"; + sanity_check_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta ; (ItemClause (inst_id, decl_id, item_name, clause_id), None) | Some impl -> (* We figure out the item clause by doing the following: @@ -511,7 +511,7 @@ let ctx_normalize_trait_type_constraint (meta : Meta.meta) (ctx : eval_ctx) norm_ctx_normalize_trait_type_constraint (mk_norm_ctx meta ctx) ttc (** Same as [type_decl_get_instantiated_variants_fields_types] but normalizes the types *) -let type_decl_get_inst_norm_variants_fields_rtypes (ctx : eval_ctx) +let type_decl_get_inst_norm_variants_fields_rtypes (meta : Meta.meta) (ctx : eval_ctx) (def : type_decl) (generics : generic_args) : (VariantId.id option * ty list) list = let res = @@ -519,16 +519,16 @@ let type_decl_get_inst_norm_variants_fields_rtypes (ctx : eval_ctx) in List.map (fun (variant_id, types) -> - (variant_id, List.map (ctx_normalize_ty def.meta ctx) types)) + (variant_id, List.map (ctx_normalize_ty meta ctx) types)) res (** Same as [type_decl_get_instantiated_field_types] but normalizes the types *) -let type_decl_get_inst_norm_field_rtypes (ctx : eval_ctx) (def : type_decl) +let type_decl_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx) (def : type_decl) (opt_variant_id : VariantId.id option) (generics : generic_args) : ty list = let types = Subst.type_decl_get_instantiated_field_types def opt_variant_id generics in - List.map (ctx_normalize_ty def.meta ctx) types + List.map (ctx_normalize_ty meta ctx) types (** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *) let ctx_adt_value_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx) (adt : adt_value) @@ -540,12 +540,12 @@ let ctx_adt_value_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx) (** Same as [ctx_adt_value_get_instantiated_field_types] but normalizes the types and erases the regions. *) -let type_decl_get_inst_norm_field_etypes (ctx : eval_ctx) (def : type_decl) +let type_decl_get_inst_norm_field_etypes (meta : Meta.meta) (ctx : eval_ctx) (def : type_decl) (opt_variant_id : VariantId.id option) (generics : generic_args) : ty list = let types = Subst.type_decl_get_instantiated_field_types def opt_variant_id generics in - let types = List.map (ctx_normalize_ty def.meta ctx) types in + let types = List.map (ctx_normalize_ty meta ctx) types in List.map Subst.erase_regions types (** Same as [ctx_adt_get_instantiated_field_types] but normalizes the types and diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 558aaa4e..51392edf 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -371,7 +371,7 @@ let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (n is important). *) let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx = - cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "Pushed variables and their values do not have the same type TODO: Error message"; + cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "The pushed variables and their values do not have the same type"; let bv = var_to_binder var in { ctx with env = EBinding (BVar bv, v) :: ctx.env } @@ -395,7 +395,7 @@ let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value List.for_all (fun (var, (value : typed_value)) -> TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty) - vars) meta "Pushed variables and their values do not have the same type TODO: Error message"; + vars) meta "The pushed variables and their values do not have the same type TODO: Error message"; let vars = List.map (fun (var, value) -> EBinding (BVar (var_to_binder var), value)) diff --git a/compiler/Errors.ml b/compiler/Errors.ml index 4c51720f..aff62022 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -11,38 +11,48 @@ let format_error_message (meta : Meta.meta) msg = exception CFailure of string - let error_list : (Meta.meta option * string) list ref = ref [] -let save_error (meta : Meta.meta option) (msg : string) = error_list := (meta, msg)::(!error_list) - -let craise (meta : Meta.meta) (msg : string) = - if !Config.fail_hard then - raise (Failure (format_error_message meta msg)) - else - let () = save_error (Some meta) msg in - raise (CFailure msg) +let push_error (meta : Meta.meta option) (msg : string) = error_list := (meta, msg)::(!error_list) -let cassert (b : bool) (meta : Meta.meta) (msg : string) = - if b then - craise meta msg +let save_error ?(b : bool = true) (meta : Meta.meta option) (msg : string) = + push_error meta msg; + match meta with + | Some m -> + if !Config.fail_hard && b then + raise (Failure (format_error_message m msg)) + | None -> + if !Config.fail_hard && b then + raise (Failure msg) let craise_opt_meta (meta : Meta.meta option) (msg : string) = match meta with - | Some m -> craise m msg + | Some m -> + if !Config.fail_hard then + raise (Failure (format_error_message m msg)) + else + let () = push_error (Some m) msg in + raise (CFailure msg) | None -> - let () = save_error (None) msg in + if !Config.fail_hard then + raise (Failure msg) + else + let () = push_error None msg in raise (CFailure msg) +let craise (meta : Meta.meta) (msg : string) = + craise_opt_meta (Some meta) msg + let cassert_opt_meta (b : bool) (meta : Meta.meta option) (msg : string) = - match meta with - | Some m -> cassert b m msg - | None -> - if b then - let () = save_error (None) msg in - raise (CFailure msg) + if b then + craise_opt_meta meta msg + +let cassert (b : bool) (meta : Meta.meta) (msg : string) = + cassert_opt_meta b (Some meta) 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 internal_error meta = craise meta "Internal error, please report 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 82656273..0e86e187 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -128,8 +128,8 @@ let extract_adt_g_value (meta : Meta.meta) | TAdt (TTuple, generics) -> (* Tuple *) (* For now, we only support fully applied tuple constructors *) - cassert (List.length generics.types = List.length field_values) meta "Only applied tuple constructors are currently supported"; - cassert (generics.const_generics = [] && generics.trait_refs = []) meta "Only applied tuple constructors are currently supported"; + cassert (List.length generics.types = List.length field_values) meta "Only fully applied tuple constructors are currently supported"; + cassert (generics.const_generics = [] && generics.trait_refs = []) meta "Only fully applied tuple constructors are currently supported"; extract_as_tuple () | TAdt (adt_id, _) -> (* "Regular" ADT *) @@ -188,7 +188,6 @@ let extract_adt_g_value (meta : Meta.meta) (* Extract globals in the same way as variables *) let extract_global (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (id : A.GlobalDeclId.id) (generics : generic_args) : unit = - (* let trait_decl = GlobalDeclId.Map.find id ctx.trait_decl_id in there might be a way to extract the meta ? *) let use_brackets = inside && generics <> empty_generic_args in F.pp_open_hvbox fmt ctx.indent_incr; if use_brackets then F.pp_print_string fmt "("; @@ -449,7 +448,7 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.for if not method_id.is_provided then ( (* Required method *) - cassert (lp_id = None) trait_decl.meta "TODO: Error message"; + sanity_check (lp_id = None) trait_decl.meta ; extract_trait_ref trait_decl.meta ctx fmt TypeDeclId.Set.empty true trait_ref; let fun_name = ctx_get_trait_method meta trait_ref.trait_decl_ref.trait_decl_id @@ -498,9 +497,10 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.for | Error (types, err) -> extract_generic_args meta ctx fmt TypeDeclId.Set.empty { generics with types }; - if !Config.fail_hard then craise meta err - else - F.pp_print_string fmt + (* if !Config.fail_hard then craise meta err + else *) + save_error (Some meta) err; + F.pp_print_string fmt "(\"ERROR: ill-formed builtin: invalid number of filtering \ arguments\")"); (* Print the arguments *) @@ -645,7 +645,7 @@ and extract_Lambda (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (* Open parentheses *) if inside then F.pp_print_string fmt "("; (* Print the lambda - note that there should always be at least one variable *) - cassert (xl <> []) meta "TODO: error message"; + sanity_check (xl <> []) meta ; F.pp_print_string fmt "fun"; let with_type = !backend = Coq in let ctx = @@ -944,7 +944,7 @@ and extract_StructUpdate (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.form (inside : bool) (e_ty : ty) (supd : struct_update) : unit = (* We can't update a subset of the fields in Coq (i.e., we can do [{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *) - cassert (!backend <> Coq || supd.init = None) meta "TODO: error message"; + sanity_check (!backend <> Coq || supd.init = None) meta ; (* In the case of HOL4, records with no fields are not supported and are thus extracted to unit. We need to check that by looking up the definition *) let extract_as_unit = @@ -1188,7 +1188,7 @@ let assert_backend_supports_decreases_clauses (meta : Meta.meta) = | FStar | Lean -> () | _ -> craise - meta "decreases clauses only supported for the Lean & F* backends" + meta "Decreases clauses are only supported for the Lean and F* backends" (** Extract a decreases clause function template body. @@ -1208,7 +1208,7 @@ let assert_backend_supports_decreases_clauses (meta : Meta.meta) = *) let extract_template_fstar_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = - cassert (!backend = FStar) def.meta "TODO: error message"; + cassert (!backend = FStar) def.meta "The generation of template decrease clauses is only supported for the F* backend"; (* Retrieve the function name *) let def_name = ctx_get_termination_measure def.meta def.def_id def.loop_id ctx in @@ -1273,7 +1273,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) *) let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = - cassert (!backend = Lean) def.meta "TODO: error message"; + cassert (!backend = Lean) def.meta "The generation of template termination and decreasing clauses is only supported for the Lean backend" ; (* * Extract a template for the termination measure *) @@ -1396,7 +1396,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit = - cassert (not def.is_global_decl_body) def.meta "TODO: error message"; + sanity_check (not def.is_global_decl_body) def.meta ; (* Retrieve the function name *) let def_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx in (* Add a break before *) @@ -1643,7 +1643,7 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = (* Retrieve the definition name *) let def_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx in - cassert (def.signature.generics.const_generics = []) def.meta "TODO: error message"; + cassert (def.signature.generics.const_generics = []) def.meta "Constant generics are not supported yet when generating code for HOL4"; (* Add the type/const gen parameters - note that we need those bindings only for the generation of the type (they are not top-level) *) let ctx, _, _, _ = @@ -1689,7 +1689,7 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit = - cassert (not def.is_global_decl_body) def.meta "TODO: error message"; + sanity_check (not def.is_global_decl_body) def.meta ; (* We treat HOL4 opaque functions in a specific manner *) if !backend = HOL4 && Option.is_none def.body then extract_fun_decl_hol4_opaque ctx fmt def @@ -2252,7 +2252,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) - we only generate trait clauses for the clauses we find in the pure generics *) let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params decl.meta f.llbc_name f.signature.llbc_generics generics ctx (* TODO: confirm it's the right meta*) + ctx_add_generic_params decl.meta f.llbc_name f.signature.llbc_generics generics ctx in let backend_uses_forall = match !backend with Coq | Lean -> true | FStar | HOL4 -> false @@ -2263,7 +2263,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) let use_forall_use_sep = false in extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty ~use_forall ~use_forall_use_sep ~use_arrows generics type_params cg_params - trait_clauses; (* TODO: confirm it's the right meta*) + trait_clauses; if use_forall then F.pp_print_string fmt ","; (* Extract the inputs and output *) F.pp_print_space fmt (); @@ -2558,8 +2558,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) in extract_trait_impl_item ctx fmt fun_name ty -(** Extract a trait implementation - * TODO: check if impl.meta everywhere is the right meta +(** Extract a trait implementation *) let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (impl : trait_impl) : unit = diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 1c21e99c..022643f5 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -262,9 +262,8 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id) \"" ^ name ^ "\":" ^ id1 ^ id2 ^ "\nYou may want to rename some of your definitions, or report an issue." in - log#serror err; (* If we fail hard on errors, raise an exception *) - craise_opt_meta None err + save_error None err let names_map_get_id_from_name (name : string) (nm : names_map) : id option = StringMap.find_opt name nm.name_to_id @@ -296,9 +295,8 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string) "Error when registering the name for id: " ^ id_to_string id ^ ":\nThe chosen name is already in the names set: " ^ name in - log#serror err; (* If we fail hard on errors, raise an exception *) - craise_opt_meta None err); + save_error None err); (* Insert *) names_map_add_unchecked id name nm @@ -425,7 +423,7 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string) (** The [id_to_string] function to print nice debugging messages if there are collisions *) -let names_maps_get ?(meta = None) (id_to_string : id -> string) (id : id) (nm : names_maps) : +let names_maps_get (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (nm : names_maps) : string = (* We do not use the same name map if we allow/disallow collisions *) let map_to_string (m : string IdMap.t) : string = @@ -445,9 +443,8 @@ let names_maps_get ?(meta = None) (id_to_string : id -> string) (id : id) (nm : "Could not find: " ^ id_to_string id ^ "\nNames map:\n" ^ map_to_string m in - log#serror err; - if !Config.fail_hard then craise_opt_meta meta err - else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)") + save_error meta err; + "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)") else let m = nm.names_map.id_to_name in match IdMap.find_opt id m with @@ -457,9 +454,8 @@ let names_maps_get ?(meta = None) (id_to_string : id -> string) (id : id) (nm : "Could not find: " ^ id_to_string id ^ "\nNames map:\n" ^ map_to_string m in - log#serror err; - if !Config.fail_hard then craise_opt_meta meta err - else "(ERROR: \"" ^ id_to_string id ^ "\")" + save_error meta err; + "(ERROR: \"" ^ id_to_string id ^ "\")" type names_map_init = { keywords : string list; @@ -591,17 +587,17 @@ let llbc_fun_id_to_string (ctx : extraction_ctx) = let fun_id_to_string (ctx : extraction_ctx) = PrintPure.regular_fun_id_to_string (extraction_ctx_to_fmt_env ctx) -let adt_variant_to_string ?(meta = None) (ctx : extraction_ctx) = +let adt_variant_to_string (meta : Meta.meta option) (ctx : extraction_ctx) = PrintPure.adt_variant_to_string ~meta:meta (extraction_ctx_to_fmt_env ctx) -let adt_field_to_string ?(meta = None) (ctx : extraction_ctx) = +let adt_field_to_string (meta : Meta.meta option) (ctx : extraction_ctx) = PrintPure.adt_field_to_string ~meta:meta (extraction_ctx_to_fmt_env ctx) (** Debugging function, used when communicating name collisions to the user, and also to print ids for internal debugging (in case of lookup miss for instance). *) -let id_to_string ?(meta = None) (id : id) (ctx : extraction_ctx) : string = +let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string = let trait_decl_id_to_string (id : A.TraitDeclId.id) : string = let trait_name = trait_decl_id_to_string ctx id in "trait_decl: " ^ trait_name ^ " (id: " ^ A.TraitDeclId.to_string id ^ ")" @@ -629,11 +625,11 @@ let id_to_string ?(meta = None) (id : id) (ctx : extraction_ctx) : string = | StructId id -> "struct constructor of: " ^ type_id_to_string ctx id | VariantId (id, variant_id) -> let type_name = type_id_to_string ctx id in - let variant_name = adt_variant_to_string ~meta:meta ctx id (Some variant_id) in + let variant_name = adt_variant_to_string meta ctx id (Some variant_id) in "type name: " ^ type_name ^ ", variant name: " ^ variant_name | FieldId (id, field_id) -> let type_name = type_id_to_string ctx id in - let field_name = adt_field_to_string ~meta:meta ctx id field_id in + let field_name = adt_field_to_string meta ctx id field_id in "type name: " ^ type_name ^ ", field name: " ^ field_name | UnknownId -> "keyword" | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id @@ -660,50 +656,50 @@ let id_to_string ?(meta = None) (id : id) (ctx : extraction_ctx) : string = | TraitSelfClauseId -> "trait_self_clause" let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = - let id_to_string (id : id) : string = id_to_string ~meta:(Some meta) id ctx in + let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in let names_maps = names_maps_add id_to_string id name ctx.names_maps in { ctx with names_maps } -let ctx_get ?(meta = None) (id : id) (ctx : extraction_ctx) : string = - let id_to_string (id : id) : string = id_to_string ~meta:meta id ctx in - names_maps_get ~meta:meta id_to_string id ctx.names_maps (* TODO check if we can remove the meta arg, same for following functions*) +let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string = + let id_to_string (id : id) : string = id_to_string meta id ctx in + names_maps_get meta id_to_string id ctx.names_maps let ctx_get_global (meta : Meta.meta) (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (GlobalId id) ctx + ctx_get (Some meta) (GlobalId id) ctx let ctx_get_function (meta : Meta.meta) (id : fun_id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (FunId id) ctx + ctx_get (Some meta) (FunId id) ctx let ctx_get_local_function (meta : Meta.meta) (id : A.FunDeclId.id) (lp : LoopId.id option) (ctx : extraction_ctx) : string = ctx_get_function meta (FromLlbc (FunId (FRegular id), lp)) ctx -let ctx_get_type ?(meta=None) (id : type_id) (ctx : extraction_ctx) : string = - cassert_opt_meta (id <> TTuple) meta "TODO: error message"; - ctx_get ~meta:meta (TypeId id) ctx +let ctx_get_type (meta : Meta.meta option) (id : type_id) (ctx : extraction_ctx) : string = + sanity_check_opt_meta (id <> TTuple) meta; + ctx_get meta (TypeId id) ctx let ctx_get_local_type (meta : Meta.meta) (id : TypeDeclId.id) (ctx : extraction_ctx) : string = - ctx_get_type ~meta:(Some meta) (TAdtId id) ctx + ctx_get_type (Some meta) (TAdtId id) ctx -let ctx_get_assumed_type ?(meta = None) (id : assumed_ty) (ctx : extraction_ctx) : string = - ctx_get_type ~meta:meta (TAssumed id) ctx +let ctx_get_assumed_type (meta : Meta.meta option) (id : assumed_ty) (ctx : extraction_ctx) : string = + ctx_get_type meta (TAssumed id) ctx let ctx_get_trait_constructor (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TraitDeclConstructorId id) ctx + ctx_get (Some meta) (TraitDeclConstructorId id) ctx let ctx_get_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) TraitSelfClauseId ctx + ctx_get (Some meta) TraitSelfClauseId ctx let ctx_get_trait_decl (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TraitDeclId id) ctx + ctx_get (Some meta) (TraitDeclId id) ctx let ctx_get_trait_impl (meta : Meta.meta) (id : trait_impl_id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TraitImplId id) ctx + ctx_get (Some meta) (TraitImplId id) ctx let ctx_get_trait_item (meta : Meta.meta) (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TraitItemId (id, item_name)) ctx + ctx_get (Some meta) (TraitItemId (id, item_name)) ctx let ctx_get_trait_const (meta : Meta.meta) (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = @@ -715,48 +711,48 @@ let ctx_get_trait_type (meta : Meta.meta) (id : trait_decl_id) (item_name : stri let ctx_get_trait_method (meta : Meta.meta) (id : trait_decl_id) (item_name : string) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TraitMethodId (id, item_name)) ctx + ctx_get (Some meta) (TraitMethodId (id, item_name)) ctx let ctx_get_trait_parent_clause (meta : Meta.meta) (id : trait_decl_id) (clause : trait_clause_id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TraitParentClauseId (id, clause)) ctx + ctx_get (Some meta) (TraitParentClauseId (id, clause)) ctx let ctx_get_trait_item_clause (meta : Meta.meta) (id : trait_decl_id) (item : string) (clause : trait_clause_id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TraitItemClauseId (id, item, clause)) ctx + ctx_get (Some meta) (TraitItemClauseId (id, item, clause)) ctx let ctx_get_var (meta : Meta.meta) (id : VarId.id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (VarId id) ctx + ctx_get (Some meta) (VarId id) ctx let ctx_get_type_var (meta : Meta.meta) (id : TypeVarId.id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TypeVarId id) ctx + ctx_get (Some meta) (TypeVarId id) ctx let ctx_get_const_generic_var (meta : Meta.meta) (id : ConstGenericVarId.id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (ConstGenericVarId id) ctx + ctx_get (Some meta) (ConstGenericVarId id) ctx let ctx_get_local_trait_clause (meta : Meta.meta) (id : TraitClauseId.id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (LocalTraitClauseId id) ctx + ctx_get (Some meta) (LocalTraitClauseId id) ctx let ctx_get_field (meta : Meta.meta) (type_id : type_id) (field_id : FieldId.id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (FieldId (type_id, field_id)) ctx + ctx_get (Some meta) (FieldId (type_id, field_id)) ctx let ctx_get_struct (meta : Meta.meta) (def_id : type_id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (StructId def_id) ctx + ctx_get (Some meta) (StructId def_id) ctx let ctx_get_variant (meta : Meta.meta) (def_id : type_id) (variant_id : VariantId.id) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (VariantId (def_id, variant_id)) ctx + ctx_get (Some meta) (VariantId (def_id, variant_id)) ctx let ctx_get_decreases_proof (meta : Meta.meta) (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (DecreasesProofId (FRegular def_id, loop_id)) ctx + ctx_get (Some meta) (DecreasesProofId (FRegular def_id, loop_id)) ctx let ctx_get_termination_measure (meta : Meta.meta) (def_id : A.FunDeclId.id) (loop_id : LoopId.id option) (ctx : extraction_ctx) : string = - ctx_get ~meta:(Some meta) (TerminationMeasureId (FRegular def_id, loop_id)) ctx + ctx_get (Some meta) (TerminationMeasureId (FRegular def_id, loop_id)) ctx (** Small helper to compute the name of a unary operation *) let unop_name (unop : unop) : string = @@ -1633,7 +1629,7 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) (basename let cl = to_snake_case name in let cl = String.split_on_char '_' cl in let cl = List.filter (fun s -> String.length s > 0) cl in - cassert (List.length cl > 0) meta "TODO: error message"; + sanity_check (List.length cl > 0) meta; let cl = List.map (fun s -> s.[0]) cl in StringUtils.string_of_chars cl in diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index 9df5b03e..c4e145a0 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -32,7 +32,7 @@ end For impl blocks, we simply use the name of the type (without its arguments) if all the arguments are variables. *) -let pattern_to_extract_name ?(meta = None) (name : pattern) : string list = +let pattern_to_extract_name (meta : Meta.meta option) (name : pattern) : string list = let c = { tgt = TkName } in let all_vars = let check (g : generic_arg) : bool = @@ -92,9 +92,9 @@ let pattern_to_extract_name ?(meta = None) (name : pattern) : string list = let name = visitor#visit_pattern () name in List.map (pattern_elem_to_string c) name -let pattern_to_type_extract_name = pattern_to_extract_name -let pattern_to_fun_extract_name = pattern_to_extract_name -let pattern_to_trait_impl_extract_name = pattern_to_extract_name +let pattern_to_type_extract_name = pattern_to_extract_name None +let pattern_to_fun_extract_name = pattern_to_extract_name None +let pattern_to_trait_impl_extract_name = pattern_to_extract_name None (* TODO: this is provisional. We just want to make sure that the extraction names we derive from the patterns (for the builtin definitions) are @@ -103,7 +103,7 @@ let name_to_simple_name (ctx : ctx) (n : Types.name) : string list = let c : to_pat_config = { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs } in - pattern_to_extract_name (name_to_pattern ctx c n) + pattern_to_extract_name None (name_to_pattern ctx c n) (** If the [prefix] is Some, we attempt to remove the common prefix between [prefix] and [name] from [name] *) @@ -125,4 +125,4 @@ let name_with_generics_to_simple_name (ctx : ctx) let _, _, name = pattern_common_prefix { equiv = true } prefix name in name in - pattern_to_extract_name name + pattern_to_extract_name None name diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 02aaec65..a8143876 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -287,7 +287,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ("val [" ^ String.concat ", " names ^ "] = DefineDiv ‘") else ( - assert (List.length names = 1) (* TODO: Error message, meta todo*); + sanity_check_opt_meta (List.length names = 1) None; let name = List.hd names in F.pp_print_string fmt ("val " ^ name ^ " = Define ‘")); F.pp_print_cut fmt () @@ -470,7 +470,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) if print_paren then F.pp_print_string fmt "("; (* TODO: for now, only the opaque *functions* are extracted in the opaque module. The opaque *types* are assumed. *) - F.pp_print_string fmt (ctx_get_type ~meta:(Some meta) type_id ctx); + F.pp_print_string fmt (ctx_get_type (Some meta) type_id ctx); (* We might need to filter the type arguments, if the type is builtin (for instance, we filter the global allocator type argument for `Vec`). *) @@ -496,7 +496,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) | HOL4 -> let { types; const_generics; trait_refs } = generics in (* Const generics are not supported in HOL4 *) - cassert (const_generics = []) meta "Const generics are not supported in HOL4"; + cassert (const_generics = []) meta "Constant generics are not supported yet when generating code for HOL4"; let print_tys = match type_id with | TAdtId id -> not (TypeDeclId.Set.mem id no_params_tys) @@ -513,7 +513,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (extract_rec true) types; if print_paren then F.pp_print_string fmt ")"; F.pp_print_space fmt ()); - F.pp_print_string fmt (ctx_get_type ~meta:(Some meta) type_id ctx); + F.pp_print_string fmt (ctx_get_type (Some meta) type_id ctx); if trait_refs <> [] then ( F.pp_print_space fmt (); Collections.List.iter_link (F.pp_print_space fmt) @@ -554,7 +554,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt type_name | _ -> (* HOL4 doesn't have 1st class types *) - cassert (!backend <> HOL4) meta "TODO: Error message"; + cassert (!backend <> HOL4) meta "Trait types are not supported yet when generating code for HOL4"; extract_trait_ref meta ctx fmt no_params_tys false trait_ref; F.pp_print_string fmt ("." ^ add_brackets type_name)) @@ -606,7 +606,7 @@ and extract_generic_args (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.form (extract_ty meta ctx fmt no_params_tys true) types); if const_generics <> [] then ( - cassert (!backend <> HOL4) meta "TODO: Error message"; + cassert (!backend <> HOL4) meta "Constant generics are not supported yet when generating code for HOL4"; F.pp_print_space fmt (); Collections.List.iter_link (F.pp_print_space fmt) (extract_const_generic meta ctx fmt true) @@ -661,9 +661,8 @@ and extract_trait_instance_id (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F | Self -> (* This has a specific treatment depending on the item we're extracting (associated type, etc.). We should have caught this elsewhere. *) - if !Config.fail_hard then - craise meta "Unexpected occurrence of `Self`" - else F.pp_print_string fmt "ERROR(\"Unexpected Self\")" + save_error (Some meta) "Unexpected occurrence of `Self`"; + F.pp_print_string fmt "ERROR(\"Unexpected Self\")" | TraitImpl id -> let name = ctx_get_trait_impl meta id ctx in F.pp_print_string fmt name @@ -1076,7 +1075,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) else ( (* We extract for Coq or Lean, and we have a recursive record, or a record in a group of mutually recursive types: we extract it as an inductive type *) - cassert (is_rec && (!backend = Coq || !backend = Lean)) def.meta "TODO: error message"; + cassert (is_rec && (!backend = Coq || !backend = Lean)) def.meta "Constant generics are not supported yet when generating code for HOL4"; (* Small trick: in Lean we use namespaces, meaning we don't need to prefix the constructor name with the name of the type at definition site, i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq @@ -1177,7 +1176,7 @@ let extract_generic_params (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo (trait_clauses : string list) : unit = let all_params = List.concat [ type_params; cg_params; trait_clauses ] in (* HOL4 doesn't support const generics *) - cassert (cg_params = [] || !backend <> HOL4) meta "HOL4 doesn't support const generics"; + cassert (cg_params = [] || !backend <> HOL4) meta "Constant generics are not supported yet when generating code for HOL4"; let left_bracket (implicit : bool) = if implicit && !backend <> FStar then F.pp_print_string fmt "{" else F.pp_print_string fmt "(" @@ -1395,7 +1394,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) | None -> F.pp_print_string fmt def_name); (* HOL4 doesn't support const generics, and type definitions in HOL4 don't support trait clauses *) - cassert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4) def.meta "HOL4 doesn't support const generics, and type definitions in HOL4 don't support trait clauses"; + cassert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4) def.meta "Constant generics and type definitions with trait clauses are not supported yet when generating code for HOL4"; (* Print the generic parameters *) extract_generic_params def.meta ctx_body fmt type_decl_group ~use_forall def.generics type_params cg_params trait_clauses; @@ -1464,9 +1463,9 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) (* Retrieve the definition name *) let def_name = ctx_get_local_type def.meta def.def_id ctx in (* Generic parameters are unsupported *) - cassert (def.generics.const_generics = []) def.meta "Generic parameters are unsupported"; + cassert (def.generics.const_generics = []) def.meta "Constant generics are not supported yet when generating code for HOL4"; (* Trait clauses on type definitions are unsupported *) - cassert (def.generics.trait_clauses = []) def.meta "Trait clauses on type definitions are unsupported"; + cassert (def.generics.trait_clauses = []) def.meta "Types with trait clauses are not supported yet when generating code for HOL4"; (* Types *) (* Count the number of parameters *) let num_params = List.length def.generics.types in @@ -1565,7 +1564,7 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = - cassert (!backend = Coq) decl.meta "TODO: error message"; + sanity_check (!backend = Coq) decl.meta; (* Generating the [Arguments] instructions is useful only if there are parameters *) let num_params = List.length decl.generics.types @@ -1611,7 +1610,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = - cassert (!backend = Coq) decl.meta "TODO: error message"; + sanity_check (!backend = Coq) decl.meta; match decl.kind with | Opaque | Enum _ -> () | Struct fields -> @@ -1782,7 +1781,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) * one line *) F.pp_open_hvbox fmt 0; (* Retrieve the name *) - let state_name = ctx_get_assumed_type TState ctx in + let state_name = ctx_get_assumed_type None TState ctx in (* The syntax for Lean and Coq is almost identical. *) let print_axiom () = let axiom = diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f3840a8c..9ca35e79 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -167,8 +167,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* We need to know if the declaration group contains a global - note that * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in - cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration"; (*TODO recheck how to get meta*) - cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration"; + cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "This global definition is in a group of mutually recursive definitions"; + cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "This builtin function belongs to a group of mutually recursive definitions"; (* We ignore on purpose functions that cannot fail and consider they *can* * fail: the result of the analysis is not used yet to adjust the translation * so that the functions which syntactically can't fail don't use an error monad. diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 0bbde79c..034304c7 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -211,7 +211,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : in (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) let call_id = fresh_fun_call_id () in - cassert (call_id = FunCallId.zero) fdef.meta "The abstractions should be empty (i.e., with no avalues) abstractions"; + sanity_check (call_id = FunCallId.zero) fdef.meta; let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : eval_ctx * typed_avalue list = (* Project over the values - we use *loan* projectors, as explained above *) @@ -272,7 +272,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) ^ "\n- inside_loop: " ^ Print.bool_to_string inside_loop ^ "\n- ctx:\n" - ^ Print.Contexts.eval_ctx_to_string fdef.meta ctx)); + ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.meta) ctx)); (* We need to instantiate the function signature - to retrieve * the return type. Note that it is important to re-generate * an instantiation of the signature, so that we use fresh @@ -330,7 +330,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let region_can_end rid = RegionGroupId.Set.mem rid parent_and_current_rgs in - cassert (region_can_end back_id) fdef.meta "The region should be able to end"; + sanity_check (region_can_end back_id) fdef.meta; let ctx = create_push_abstractions_from_abs_region_groups (fun rg_id -> SynthRet rg_id) @@ -417,9 +417,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) | Loop (loop_id', rg_id', LoopSynthInput) -> (* We only allow to end the loop synth input abs for the region group [rg_id] *) - cassert ( + sanity_check ( if Option.is_some loop_id then loop_id = Some loop_id' - else true) fdef.meta "Only the loop synth input abs for the region group [rg_id] are allowed to end"; + else true) fdef.meta; (* Loop abstractions *) let rg_id' = Option.get rg_id' in if rg_id' = back_id && inside_loop then @@ -427,7 +427,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) else abs | Loop (loop_id', _, LoopCall) -> (* We can end all the loop call abstractions *) - cassert (loop_id = Some loop_id') fdef.meta "TODO: error message"; + sanity_check (loop_id = Some loop_id') fdef.meta; { abs with can_end = true } | SynthInput rg_id' -> if rg_id' = back_id && end_fun_synth_input then @@ -603,7 +603,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Evaluate the function *) let symbolic = - eval_function_body config fdef.meta (Option.get fdef.body).body cf_finish ctx + eval_function_body config (Option.get fdef.body).body cf_finish ctx in (* Return *) @@ -655,7 +655,7 @@ module Test = struct in (* Evaluate the function *) - let _ = eval_function_body config body.meta body.body cf_check ctx in + let _ = eval_function_body config body.body cf_check ctx in () (** Small helper: return true if the function is a *transparent* unit function diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index ab2639ad..c1cf8441 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -42,7 +42,7 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt in let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content) = - cassert (Option.is_none !replaced_bc) meta "TODO: error message"; + sanity_check (Option.is_none !replaced_bc) meta; replaced_bc := Some (abs_id, bc) in (* Raise an exception if: @@ -224,8 +224,8 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt method! visit_abs outer abs = (* Update the outer abs *) let outer_abs, outer_borrows = outer in - cassert (Option.is_none outer_abs) meta "TODO: error message"; - cassert (Option.is_none outer_borrows) meta "TODO: error message"; + sanity_check (Option.is_none outer_abs) meta; + sanity_check (Option.is_none outer_borrows) meta; let outer = (Some abs.abs_id, None) in super#visit_abs outer abs end @@ -248,18 +248,18 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv : typed_value) (ctx : eval_ctx) : eval_ctx = (* Sanity check *) - sanity_check (not (loans_in_value nv)) meta; - sanity_check (not (bottom_in_value ctx.ended_regions nv)) meta; + exec_assert (not (loans_in_value nv)) meta "Can not end a borrow because the value to give back contains bottom"; + exec_assert (not (bottom_in_value ctx.ended_regions nv)) meta "Can not end a borrow because the value to give back contains bottom"; (* Debug *) log#ldebug (lazy ("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: " - ^ typed_value_to_string meta ctx nv - ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n")); + ^ typed_value_to_string ~meta:(Some meta) ctx nv + ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* We use a reference to check that we updated exactly one loan *) let replaced : bool ref = ref false in let set_replaced () = - cassert (not !replaced) meta "Exactly one loan should have been updated"; + sanity_check (not !replaced) meta; replaced := true in (* Whenever giving back symbolic values, they shouldn't contain already ended regions *) @@ -427,7 +427,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv (* We remember in which abstraction we are before diving - * this is necessary for projecting values: we need to know * over which regions to project *) - cassert (Option.is_none opt_abs) meta "TODO: error message"; + sanity_check (Option.is_none opt_abs) meta; super#visit_EAbs (Some abs) abs end in @@ -466,7 +466,7 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions type [T]! We thus *mustn't* introduce a projector here. *) (* AProjBorrows (nsv, sv.sv_ty) *) - craise meta "TODO: error message" + internal_error meta in AProjLoans (sv, (mv, child_proj) :: local_given_back) in @@ -671,7 +671,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B (* Keep track of changes *) let r = ref false in let set_ref () = - cassert (not !r) meta "TODO: error message"; + sanity_check (not !r) meta; r := true in @@ -701,7 +701,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B let env = obj#visit_env () ctx.env in (* Check that we reborrowed once *) - cassert !r meta "Not reborrowed once"; + sanity_check !r meta; { ctx with env } (** Convert an {!type:avalue} to a {!type:value}. @@ -746,11 +746,11 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_bor (lazy (let bc = match bc with - | Concrete bc -> borrow_content_to_string meta ctx bc - | Abstract bc -> aborrow_content_to_string meta ctx bc + | Concrete bc -> borrow_content_to_string ~meta:(Some meta) ctx bc + | Abstract bc -> aborrow_content_to_string ~meta:(Some meta) ctx bc in "give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc - ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n")); + ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* This is used for sanity checks *) let sanity_ek = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } @@ -814,8 +814,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": borrow didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); craise meta "Borrow not eliminated" in match lookup_loan_opt meta ek_all l ctx with @@ -825,8 +825,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": loan didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); craise meta "Loan not eliminated" in unit_to_cm_fun check_disappeared @@ -863,7 +863,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a log#ldebug (lazy ("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Utility function for the sanity checks: check that the borrow disappeared * from the context *) @@ -922,7 +922,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a log#ldebug (lazy "End borrow: borrow not found"); (* It is possible that we can't find a borrow in symbolic mode (ending * an abstraction may end several borrows at once *) - cassert (config.mode = SymbolicMode) meta "Borrow should be in symbolic mode"; + sanity_check (config.mode = SymbolicMode) meta; (* Do a sanity check and continue *) cf_check cf ctx (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update @@ -966,7 +966,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_ (lazy ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id - ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0)); + ^ "\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0)); (* Lookup the abstraction - note that if we end a list of abstractions, ending one abstraction may lead to the current abstraction having @@ -999,7 +999,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_ ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id ^ "\n- context after parent abstractions ended:\n" - ^ eval_ctx_to_string meta ctx))) + ^ eval_ctx_to_string ~meta:(Some meta) ctx))) in (* End the loans inside the abstraction *) @@ -1010,7 +1010,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_ (lazy ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id - ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string meta ctx))) + ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx))) in (* End the abstraction itself by redistributing the borrows it contains *) @@ -1039,8 +1039,8 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_ (lazy ("end_abstraction_aux: " ^ AbstractionId.to_string abs_id - ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx))) + ^ "\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx))) in (* Sanity check: ending an abstraction must preserve the invariants *) @@ -1173,7 +1173,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow log#ldebug (lazy ("end_abstraction_borrows: found aborrow content: " - ^ aborrow_content_to_string meta ctx bc)); + ^ aborrow_content_to_string ~meta:(Some meta) ctx bc)); let ctx = match bc with | AMutBorrow (bid, av) -> @@ -1243,7 +1243,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow log#ldebug (lazy ("end_abstraction_borrows: found borrow content: " - ^ borrow_content_to_string meta ctx bc)); + ^ borrow_content_to_string ~meta:(Some meta) ctx bc)); let ctx = match bc with | VSharedBorrow bid -> ( @@ -1466,7 +1466,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) log#ldebug (lazy ("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l - ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n")); + ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* Lookup the shared loan - note that we can't promote a shared loan * in a shared value, but we can do it in a mutably borrowed value. * This is important because we can do: [let y = &two-phase ( *x );] @@ -1485,9 +1485,9 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) to do a sanity check. *) sanity_check (not (loans_in_value sv)) meta; (* Check there isn't {!Bottom} (this is actually an invariant *) - cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a !Bottom"; + cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a bottom"; (* Check there aren't reserved borrows *) - cassert (not (reserved_in_value sv)) meta "There shouldn't have reserved borrows"; + cassert (not (reserved_in_value sv)) meta "There shouldn't be reserved borrows"; (* Update the loan content *) let ctx = update_loan meta ek l (VMutLoan l) ctx in (* Continue *) @@ -1563,7 +1563,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : Bo log#ldebug (lazy ("activate_reserved_mut_borrow: resulting value:\n" - ^ typed_value_to_string meta ctx sv)); + ^ typed_value_to_string ~meta:(Some meta) ctx sv)); sanity_check (not (loans_in_value sv)) meta; sanity_check (not (bottom_in_value ctx.ended_regions sv)) meta; sanity_check (not (reserved_in_value sv)) meta; @@ -1649,7 +1649,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) | AIgnoredMutLoan (opt_bid, child_av) -> (* We don't support nested borrows for now *) cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet"; - cassert (opt_bid = None) meta "TODO: error message"; + sanity_check (opt_bid = None) meta; (* Simply explore the child *) list_avalues false push_fail child_av | AEndedMutLoan @@ -1680,7 +1680,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) | AIgnoredMutBorrow (opt_bid, child_av) -> (* We don't support nested borrows for now *) cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet"; - cassert (opt_bid = None) meta "TODO: error message"; + sanity_check (opt_bid = None) meta; (* Just explore the child *) list_avalues false push_fail child_av | AEndedIgnoredMutBorrow @@ -1703,7 +1703,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) | ASymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message" + sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta and list_values (v : typed_value) : typed_avalue list * typed_value = let ty = v.ty in match v.value with @@ -1725,9 +1725,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) let avl, sv = list_values sv in if destructure_shared_values then ( (* Rem.: the shared value can't contain loans nor borrows *) - cassert (ty_no_regions ty) meta "The shared value can't contain loans nor borrows"; + cassert (ty_no_regions ty) meta "Nested borrows are not supported yet"; let av : typed_avalue = - cassert (not (value_has_loans_or_borrows ctx sv.value)) meta "The shared value can't contain loans nor borrows"; + sanity_check (not (value_has_loans_or_borrows ctx sv.value)) meta; (* We introduce fresh ids for the symbolic values *) let mk_value_with_fresh_sids (v : typed_value) : typed_value = let visitor = @@ -1752,7 +1752,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool) | VSymbolic _ -> (* For now, we fore all symbolic values containing borrows to be eagerly expanded *) - cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message"; + sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta; ([], v) in @@ -1808,7 +1808,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_ log#ldebug (lazy ("convert_value_to_abstractions: to_avalues:\n- value: " - ^ typed_value_to_string meta ctx v)); + ^ typed_value_to_string ~meta:(Some meta) ctx v)); let ty = v.ty in match v.value with @@ -1852,13 +1852,13 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_ (avl, { v with value = VAdt adt }) | VBorrow bc -> ( let _, ref_ty, kind = ty_as_ref ty in - cassert (ty_no_regions ref_ty) meta "TODO: error message"; + cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet"; (* Sanity check *) sanity_check allow_borrows meta; (* Convert the borrow content *) match bc with | VSharedBorrow bid -> - cassert (ty_no_regions ref_ty) meta "TODO: error message"; + cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet"; let ty = TRef (RFVar r_id, ref_ty, kind) in let value = ABorrow (ASharedBorrow bid) in ([ { value; ty } ], v) @@ -1887,7 +1887,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_ cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet"; (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) - cassert (ty_no_regions ty) meta "TODO: error message"; + cassert (ty_no_regions ty) meta "Nested borrows are not supported yet"; let ty = mk_ref_ty (RFVar r_id) ty RShared in let ignored = mk_aignored meta ty in (* Rem.: the shared value might contain loans *) @@ -1905,7 +1905,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_ | VMutLoan bid -> (* Push the avalue - note that we use [AIgnore] for the inner avalue *) (* For avalues, a loan has the borrow type *) - cassert (ty_no_regions ty) meta "TODO: error message"; + cassert (ty_no_regions ty) meta "Nested borrows are not supported yet"; let ty = mk_ref_ty (RFVar r_id) ty RMut in let ignored = mk_aignored meta ty in let av = ALoan (AMutLoan (bid, ignored)) in @@ -1914,7 +1914,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_ | VSymbolic _ -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - cassert (not (value_has_borrows ctx v.value)) meta "TODO: error message"; + cassert (not (value_has_borrows ctx v.value)) meta "Nested borrows are not supported yet"; (* Return nothing *) ([], v) in @@ -1968,26 +1968,26 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : ab in let push_loans ids (lc : g_loan_content_with_ty) : unit = - cassert (BorrowId.Set.disjoint !loans ids) meta "TODO: error message"; + sanity_check (BorrowId.Set.disjoint !loans ids) meta; loans := BorrowId.Set.union !loans ids; BorrowId.Set.iter (fun id -> - cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message"; + sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans) ids in let push_loan id (lc : g_loan_content_with_ty) : unit = - cassert (not (BorrowId.Set.mem id !loans)) meta "TODO: error message"; + sanity_check (not (BorrowId.Set.mem id !loans)) meta; loans := BorrowId.Set.add id !loans; - cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message"; + sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta; loan_to_content := BorrowId.Map.add id lc !loan_to_content; borrows_loans := LoanId id :: !borrows_loans in let push_borrow id (bc : g_borrow_content_with_ty) : unit = - cassert (not (BorrowId.Set.mem id !borrows)) meta "TODO: error message"; + sanity_check (not (BorrowId.Set.mem id !borrows)) meta; borrows := BorrowId.Set.add id !borrows; - cassert (not (BorrowId.Map.mem id !borrow_to_content)) meta "TODO: error message"; + sanity_check (not (BorrowId.Map.mem id !borrow_to_content)) meta; borrow_to_content := BorrowId.Map.add id bc !borrow_to_content; borrows_loans := BorrowId id :: !borrows_loans in @@ -2146,8 +2146,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end (* Check that the abstractions are destructured *) if !Config.sanity_checks then ( let destructure_shared_values = true in - cassert (abs_is_destructured meta destructure_shared_values ctx abs0) meta "Abstractions should be destructured"; - cassert (abs_is_destructured meta destructure_shared_values ctx abs1) meta "Abstractions should be destructured"); + sanity_check (abs_is_destructured meta destructure_shared_values ctx abs0) meta; + sanity_check (abs_is_destructured meta destructure_shared_values ctx abs1) meta); (* Compute the relevant information *) let { @@ -2201,7 +2201,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end log#ldebug (lazy ("merge_into_abstraction_aux: push_avalue: " - ^ typed_avalue_to_string meta ctx av)); + ^ typed_avalue_to_string ~meta:(Some meta) ctx av)); avalues := av :: !avalues in let push_opt_avalue av = @@ -2215,7 +2215,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end in let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t = let bids = BorrowId.Set.diff bids intersect in - cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message"; + sanity_check (not (BorrowId.Set.is_empty bids)) meta; bids in let filter_bid (bid : BorrowId.id) : BorrowId.id option = @@ -2278,7 +2278,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end (* Check that the sets of ids are the same - if it is not the case, it means we actually need to merge more than 2 avalues: we ignore this case for now *) - cassert (BorrowId.Set.equal ids0 ids1) meta "Ids are not the same - Case ignored for now"; + sanity_check (BorrowId.Set.equal ids0 ids1) meta; let ids = ids0 in if BorrowId.Set.is_empty ids then ( (* If the set of ids is empty, we can eliminate this shared loan. @@ -2290,10 +2290,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end to preserve (in practice it works because we destructure the shared values in the abstractions, and forbid nested borrows). *) - cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message"; - cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message"; - cassert (is_aignored child0.value) meta "TODO: error message"; - cassert (is_aignored child1.value) meta "TODO: error message"; + sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta; + sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta; + sanity_check (is_aignored child0.value) meta; + sanity_check (is_aignored child1.value) meta; None) else ( (* Register the loan ids *) @@ -2365,7 +2365,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end craise meta "Unreachable" | Abstract (ty, bc) -> { value = ABorrow bc; ty }) | Some bc0, Some bc1 -> - cassert (merge_funs <> None) meta "TODO: error message"; + sanity_check (merge_funs <> None) meta; merge_g_borrow_contents bc0 bc1 | None, None -> craise meta "Unreachable" in @@ -2405,10 +2405,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end match lc with | ASharedLoan (bids, sv, child) -> let bids = filter_bids bids in - cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message"; - cassert (is_aignored child.value) meta "TODO: error message"; - cassert ( - not (value_has_loans_or_borrows ctx sv.value)) meta "TODO: error message"; + sanity_check (not (BorrowId.Set.is_empty bids)) meta; + sanity_check (is_aignored child.value) meta; + sanity_check ( + not (value_has_loans_or_borrows ctx sv.value)) meta; let lc = ASharedLoan (bids, sv, child) in set_loans_as_merged bids; Some { value = ALoan lc; ty } @@ -2421,7 +2421,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end (* The abstraction has been destructured, so those shouldn't appear *) craise meta "Unreachable")) | Some lc0, Some lc1 -> - cassert (merge_funs <> None) meta "TODO: error message"; + sanity_check (merge_funs <> None) meta; merge_g_loan_contents lc0 lc1 | None, None -> craise meta "Unreachable" in @@ -2476,7 +2476,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end in (* Sanity check *) - if !Config.sanity_checks then sanity_check (abs_is_destructured meta true ctx abs) meta; + sanity_check (abs_is_destructured meta true ctx abs) meta; (* Return *) abs diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index d61e0bd1..1948c5a6 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -104,13 +104,13 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) (combine : bool -> bool (* Normalize the associated types *) match (ty1, ty2) with | TLiteral lit1, TLiteral lit2 -> - cassert (lit1 = lit2) meta "Tlitrals are not equal TODO: Error message"; + sanity_check (lit1 = lit2) meta; default | TAdt (id1, generics1), TAdt (id2, generics2) -> - cassert (id1 = id2) meta "ids are not equal TODO: Error message"; + sanity_check (id1 = id2) meta; (* There are no regions in the const generics, so we ignore them, but we still check they are the same, for sanity *) - cassert (generics1.const_generics = generics2.const_generics) meta "const generics are not the same"; + sanity_check (generics1.const_generics = generics2.const_generics) meta; (* We also ignore the trait refs *) @@ -152,12 +152,12 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) (combine : bool -> bool let tys_b = compare ty1 ty2 in combine regions_b tys_b | TVar id1, TVar id2 -> - cassert (id1 = id2) meta "Ids are not the same TODO: Error message"; + sanity_check (id1 = id2) meta; default | TTraitType _, TTraitType _ -> (* The types should have been normalized. If after normalization we get trait types, we can consider them as variables *) - cassert (ty1 = ty2) meta "The types are not normalized"; + sanity_check (ty1 = ty2) meta; default | _ -> log#lerror @@ -269,7 +269,7 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) super#visit_aloan_content env lc method! visit_EBinding env bv v = - cassert (Option.is_none !abs_or_var) meta "TODO : error message "; + sanity_check (Option.is_none !abs_or_var) meta; abs_or_var := Some (match bv with @@ -279,7 +279,7 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) abs_or_var := None method! visit_EAbs env abs = - cassert (Option.is_none !abs_or_var) meta "TODO : error message "; + sanity_check (Option.is_none !abs_or_var) meta; if ek.enter_abs then ( abs_or_var := Some (AbsId abs.abs_id); super#visit_EAbs env abs; @@ -320,7 +320,7 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (nl * returning we check that we updated at least once. *) let r = ref false in let update () : loan_content = - cassert (not !r) meta "TODO : error message "; + sanity_check (not !r) meta; r := true; nlc in @@ -367,7 +367,7 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (nl let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) - cassert !r meta "No loan was updated"; + sanity_check !r meta; ctx (** Update a abstraction loan content. @@ -383,7 +383,7 @@ let update_aloan (meta : Meta.meta ) (ek : exploration_kind) (l : BorrowId.id) ( * returning we check that we updated at least once. *) let r = ref false in let update () : aloan_content = - cassert (not !r) meta "TODO : error message "; + sanity_check (not !r) meta; r := true; nlc in @@ -416,7 +416,7 @@ let update_aloan (meta : Meta.meta ) (ek : exploration_kind) (l : BorrowId.id) ( let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one loan *) - cassert !r meta "No loan was uodated"; + sanity_check !r meta; ctx (** Lookup a borrow content from a borrow id. *) @@ -501,7 +501,7 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) * returning we check that we updated at least once. *) let r = ref false in let update () : borrow_content = - cassert (not !r) meta "TODO : error message "; + sanity_check (not !r) meta; r := true; nbc in @@ -542,7 +542,7 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) let ctx = obj#visit_eval_ctx () ctx in (* Check that we updated at least one borrow *) - cassert !r meta "No borrow was updated"; + sanity_check !r meta; ctx (** Update an abstraction borrow content. @@ -558,7 +558,7 @@ let update_aborrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) * returning we check that we updated at least once. *) let r = ref false in let update () : avalue = - cassert (not !r) meta "TODO: error message"; + sanity_check (not !r) meta; r := true; nv in @@ -881,7 +881,7 @@ let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta) (regions : R update_non_shared regions sv ctx in (* Check that we updated at least once *) - cassert !updated meta "Not updated at least once"; + sanity_check !updated meta; (* Return *) ctx @@ -936,7 +936,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta) (proj_regions : RegionId. (subst : abs -> (msymbolic_value * aproj) list -> aproj) (ctx : eval_ctx) : eval_ctx = (* *) - cassert (ty_is_rty proj_ty) meta "proj_ty is not rty TODO: Error message"; + sanity_check (ty_is_rty proj_ty) meta; (* Small helpers for sanity checks *) let updated = ref false in let update abs local_given_back : aproj = @@ -958,7 +958,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta) (proj_regions : RegionId. | AProjLoans (sv', given_back) -> let abs = Option.get abs in if same_symbolic_id sv sv' then ( - cassert (sv.sv_ty = sv'.sv_ty) meta "TODO : error message "; + sanity_check (sv.sv_ty = sv'.sv_ty) meta; if projections_intersect meta proj_ty proj_regions sv'.sv_ty abs.regions then update abs given_back @@ -969,7 +969,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta) (proj_regions : RegionId. (* Apply *) let ctx = obj#visit_eval_ctx None ctx in (* Check that we updated the context at least once *) - cassert !updated meta "Context was not updated at least once"; + sanity_check !updated meta; (* Return *) ctx @@ -989,7 +989,7 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb let found = ref None in let set_found x = (* There is at most one projector which corresponds to the description *) - cassert (Option.is_none !found) meta "More than one projecto corresponds to the description"; + sanity_check (Option.is_none !found) meta; found := Some x in (* The visitor *) @@ -1007,9 +1007,9 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb super#visit_aproj abs sproj | AProjLoans (sv', given_back) -> let abs = Option.get abs in - cassert (abs.abs_id = abs_id) meta "TODO : error message "; + sanity_check (abs.abs_id = abs_id) meta; if sv'.sv_id = sv.sv_id then ( - cassert (sv' = sv) meta "TODO : error message "; + sanity_check (sv' = sv) meta; set_found given_back) else ()); super#visit_aproj abs sproj @@ -1034,7 +1034,7 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb let found = ref false in let update () = (* We update at most once *) - cassert (not !found) meta "Updated more than once"; + sanity_check (not !found) meta; found := true; nproj in @@ -1053,9 +1053,9 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb super#visit_aproj abs sproj | AProjLoans (sv', _) -> let abs = Option.get abs in - cassert (abs.abs_id = abs_id) meta "TODO : error message "; + sanity_check (abs.abs_id = abs_id) meta; if sv'.sv_id = sv.sv_id then ( - cassert (sv' = sv) meta "TODO : error message "; + sanity_check (sv' = sv) meta; update ()) else super#visit_aproj (Some abs) sproj end @@ -1083,7 +1083,7 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : sy let found = ref false in let update () = (* We update at most once *) - cassert (not !found) meta "Updated more than once"; + sanity_check (not !found) meta; found := true; nproj in @@ -1102,9 +1102,9 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : sy super#visit_aproj abs sproj | AProjBorrows (sv', _proj_ty) -> let abs = Option.get abs in - cassert (abs.abs_id = abs_id) meta "TODO : error message "; + sanity_check (abs.abs_id = abs_id) meta; if sv'.sv_id = sv.sv_id then ( - cassert (sv' = sv) meta "TODO : error message "; + sanity_check (sv' = sv) meta; update ()) else super#visit_aproj (Some abs) sproj end diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 086c0786..a2550e88 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -66,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me (** When visiting an abstraction, we remember the regions it owns to be able to properly reduce projectors when expanding symbolic values *) method! visit_abs current_abs abs = - cassert (Option.is_none current_abs) meta "TODO: error message"; + sanity_check (Option.is_none current_abs) meta; let current_abs = Some abs in super#visit_abs current_abs abs @@ -78,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me method! visit_aproj current_abs aproj = (match aproj with | AProjLoans (sv, _) | AProjBorrows (sv, _) -> - cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message" + sanity_check (not (same_symbolic_id sv original_sv)) meta | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj current_abs aproj @@ -98,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me (* Check if this is the symbolic value we are looking for *) if same_symbolic_id sv original_sv then ( (* There mustn't be any given back values *) - cassert (given_back = []) meta "TODO: error message"; + sanity_check (given_back = []) meta; (* Apply the projector *) let projected_value = apply_proj_loans_on_symbolic_expansion meta proj_regions @@ -168,7 +168,7 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_s (* Count *) let replaced = ref false in let replace () = - if at_most_once then cassert (not !replaced) meta "TODO: error message"; + if at_most_once then sanity_check (not !replaced) meta; replaced := true; nv in @@ -215,10 +215,10 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e (* Lookup the definition and check if it is an enumeration with several * variants *) let def = ctx_lookup_type_decl ctx def_id in - cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: error message"; + sanity_check (List.length generics.regions = List.length def.generics.regions) meta; (* Retrieve, for every variant, the list of its instantiated field types *) let variants_fields_types = - AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def + AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes meta ctx def generics in (* Check if there is strictly more than one variant *) @@ -325,7 +325,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) else super#visit_VSymbolic env sv method! visit_EAbs proj_regions abs = - cassert (Option.is_none proj_regions) meta "TODO: error message"; + sanity_check (Option.is_none proj_regions) meta; let proj_regions = Some abs.regions in super#visit_EAbs proj_regions abs @@ -350,7 +350,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) method! visit_aproj proj_regions aproj = (match aproj with | AProjLoans (sv, _) | AProjBorrows (sv, _) -> - cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message" + sanity_check (not (same_symbolic_id sv original_sv)) meta | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()); super#visit_aproj proj_regions aproj @@ -376,7 +376,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) let ctx = obj#visit_eval_ctx None ctx in (* Finally, replace the projectors on loans *) let bids = !borrows in - cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message"; + sanity_check (not (BorrowId.Set.is_empty bids)) meta; let see = SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = @@ -394,9 +394,9 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun = fun cf ctx -> - cassert (region <> RErased) meta "TODO: error message"; + sanity_check (region <> RErased) meta; (* Check that we are allowed to expand the reference *) - cassert (not (region_in_set region ctx.ended_regions)) meta "TODO: error message"; + sanity_check (not (region_in_set region ctx.ended_regions)) meta; (* Match on the reference kind *) match rkind with | RMut -> @@ -446,7 +446,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met (see_cf_l : (symbolic_expansion option * st_cm_fun) list) (cf_after_join : st_m_fun) : m_fun = fun ctx -> - cassert (see_cf_l <> []) meta "TODO: error message"; + sanity_check (see_cf_l <> []) meta; (* Apply the symbolic expansion in the context and call the continuation *) let resl = List.map @@ -464,8 +464,8 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met (lazy ("apply_branching_symbolic_expansions_non_borrow: " ^ symbolic_value_to_string ctx0 sv - ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n")); + ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* Continuation *) cf_br cf_after_join ctx) see_cf_l @@ -476,7 +476,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met match resl with | Some _ :: _ -> Some (List.map Option.get resl) | None :: _ -> - List.iter (fun res -> cassert (res = None) meta "TODO: error message") resl; + List.iter (fun res -> sanity_check (res = None) meta) resl; None | _ -> craise meta "Unreachable" in @@ -492,7 +492,7 @@ let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_val let original_sv = sv in let original_sv_place = sv_place in let rty = original_sv.sv_ty in - cassert (rty = TLiteral TBool) meta "TODO: error message"; + sanity_check (rty = TLiteral TBool) meta; (* Expand the symbolic value to true or false and continue execution *) let see_true = SeLiteral (VBool true) in let see_false = SeLiteral (VBool false) in @@ -554,8 +554,8 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv (lazy ("expand_symbolic_value_no_branching: " ^ symbolic_value_to_string ctx0 sv - ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n")); + ^ "\n\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* Sanity check: the symbolic value has disappeared *) sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta) in diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 3922a3ab..7045d886 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -101,8 +101,8 @@ let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal) | TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty } | TInteger int_ty, VScalar v -> (* Check the type and the ranges *) - cassert (int_ty = v.int_ty) meta "Wrong type TODO: error message"; - cassert (check_scalar_value_in_range v) meta "Wrong range TODO: error message"; + sanity_check (int_ty = v.int_ty) meta; + sanity_check (check_scalar_value_in_range v) meta; { value = VLiteral (VScalar v); ty = TLiteral ty } (* Remaining cases (invalid) *) | _, _ -> craise meta "Improperly typed constant value" @@ -123,8 +123,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) log#ldebug (lazy ("copy_value: " - ^ typed_value_to_string meta ctx v - ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx)); + ^ typed_value_to_string ~meta:(Some meta) ctx v + ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Remark: at some point we rewrote this function to use iterators, but then * we reverted the changes: the result was less clear actually. In particular, * the fact that we have exhaustive matches below makes very obvious the cases @@ -135,7 +135,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) (* Sanity check *) (match v.ty with | TAdt (TAssumed TBox, _) -> - craise meta "Can't copy an assumed value other than Option" + exec_raise meta "Can't copy an assumed value other than Option" | TAdt (TAdtId _, _) as ty -> sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta | TAdt (TTuple, _) -> () (* Ok *) @@ -147,15 +147,15 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) const_generics = []; trait_refs = []; } ) -> - sanity_check (ty_is_primitively_copyable ty) meta - | _ -> craise meta "Unreachable"); + exec_assert (ty_is_primitively_copyable ty) meta "The type is not primitively copyable" + | _ -> exec_raise meta "Unreachable"); let ctx, fields = List.fold_left_map (copy_value meta allow_adt_copy config) ctx av.field_values in (ctx, { v with value = VAdt { av with field_values = fields } }) - | VBottom -> craise meta "Can't copy ⊥" + | VBottom -> exec_raise meta "Can't copy ⊥" | VBorrow bc -> ( (* We can only copy shared borrows *) match bc with @@ -165,13 +165,13 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) let bid' = fresh_borrow_id () in let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in (ctx, { v with value = VBorrow (VSharedBorrow bid') }) - | VMutBorrow (_, _) -> craise meta "Can't copy a mutable borrow" + | VMutBorrow (_, _) -> exec_raise meta "Can't copy a mutable borrow" | VReservedMutBorrow _ -> - craise meta "Can't copy a reserved mut borrow") + exec_raise meta "Can't copy a reserved mut borrow") | VLoan lc -> ( (* We can only copy shared loans *) match lc with - | VMutLoan _ -> craise meta "Can't copy a mutable loan" + | VMutLoan _ -> exec_raise meta "Can't copy a mutable loan" | VSharedLoan (_, sv) -> (* We don't copy the shared loan: only the shared value inside *) copy_value meta allow_adt_copy config ctx sv) @@ -256,7 +256,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan log#ldebug (lazy ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op - ^ "\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n")); + ^ "\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* Evaluate *) match op with | Constant cv -> ( @@ -305,14 +305,14 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan let e = cf cv ctx in (* If we are synthesizing a symbolic AST, it means that we are in symbolic mode: the value of the const generic is necessarily symbolic. *) - cassert (e = None || is_symbolic cv.value) meta "The value of the const generic should be symbolic"; + sanity_check (e = None || is_symbolic cv.value) meta; (* We have to wrap the generated expression *) match e with | None -> None | Some e -> (* If we are synthesizing a symbolic AST, it means that we are in symbolic mode: the value of the const generic is necessarily symbolic. *) - cassert (is_symbolic cv.value) meta "The value of the const generic should be symbolic"; + sanity_check (is_symbolic cv.value) meta; (* *) Some (SymbolicAst.IntroSymbolic @@ -321,7 +321,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan value_as_symbolic meta cv.value, SymbolicAst.VaCgValue vid, e ))) - | CFnPtr _ -> craise meta "TODO") + | CFnPtr _ -> craise meta "TODO: error message") | Copy p -> (* Access the value *) let access = Read in @@ -330,7 +330,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan let copy cf v : m_fun = fun ctx -> (* Sanity checks *) - sanity_check (not (bottom_in_value ctx.ended_regions v)) meta; + exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "Can not copy a value containing bottom"; sanity_check ( Option.is_none (find_first_primitively_copyable_sv_with_borrows @@ -351,7 +351,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan let move cf v : m_fun = fun ctx -> (* Check that there are no bottoms in the value we are about to move *) - cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move"; + exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move"; let bottom : typed_value = { value = VBottom; ty = v.ty } in let ctx = write_place meta access p bottom ctx in cf v ctx @@ -366,7 +366,7 @@ let eval_operand (config : config) (meta : Meta.meta) (op : operand) (cf : typed log#ldebug (lazy ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n" - ^ eval_ctx_to_string meta ctx ^ "\n")); + ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* We reorganize the context, then evaluate the operand *) comp (prepare_eval_operand_reorganize config meta op) @@ -421,7 +421,7 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (o | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)), VLiteral (VScalar sv) ) -> ( (* Cast between integers *) - cassert (src_ty = sv.int_ty) meta "TODO: error message"; + sanity_check (src_ty = sv.int_ty) meta; let i = sv.value in match mk_scalar tgt_ty i with | Error _ -> cf (Error EPanic) @@ -443,12 +443,12 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (o let b = if Z.of_int 0 = sv.value then false else if Z.of_int 1 = sv.value then true - else craise meta "Conversion from int to bool: out of range" + else exec_raise meta "Conversion from int to bool: out of range" in let value = VLiteral (VBool b) in let ty = TLiteral TBool in cf (Ok { ty; value }) - | _ -> craise meta "Invalid input for unop" + | _ -> exec_raise meta "Invalid input for unop" in comp eval_op apply cf @@ -466,7 +466,7 @@ let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) (o | Not, (TLiteral TBool as lty) -> lty | Neg, (TLiteral (TInteger _) as lty) -> lty | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty - | _ -> craise meta "Invalid input for unop" + | _ -> exec_raise meta "Invalid input for unop" in let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in (* Call the continuation *) @@ -494,9 +494,9 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ * The remaining binops only operate on scalars. *) if binop = Eq || binop = Ne then ( (* Equality operations *) - cassert (v1.ty = v2.ty) meta "TODO: error message"; + exec_assert (v1.ty = v2.ty) meta "TODO: error message"; (* Equality/inequality check is primitive only for a subset of types *) - cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message"; + exec_assert (ty_is_primitively_copyable v1.ty) meta "Type is not primitively copyable"; let b = v1 = v2 in Ok { value = VLiteral (VBool b); ty = TLiteral TBool }) else @@ -511,7 +511,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ match binop with | Lt | Le | Ge | Gt -> (* The two operands must have the same type and the result is a boolean *) - cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is a boolean"; + sanity_check (sv1.int_ty = sv2.int_ty) meta; let b = match binop with | Lt -> Z.lt sv1.value sv2.value @@ -527,7 +527,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ : typed_value) | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> ( (* The two operands must have the same type and the result is an integer *) - cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is an integer"; + sanity_check (sv1.int_ty = sv2.int_ty) meta; let res = match binop with | Div -> @@ -583,9 +583,9 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) let res_sv_ty = if binop = Eq || binop = Ne then ( (* Equality operations *) - cassert (v1.ty = v2.ty) meta "TODO: error message"; + sanity_check (v1.ty = v2.ty) meta; (* Equality/inequality check is primitive only for a subset of types *) - cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message"; + exec_assert (ty_is_primitively_copyable v1.ty) meta "The type is not primitively copyable"; TLiteral TBool) else (* Other operations: input types are integers *) @@ -593,10 +593,10 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> ( match binop with | Lt | Le | Ge | Gt -> - cassert (int_ty1 = int_ty2) meta "TODO: error message"; + sanity_check (int_ty1 = int_ty2) meta; TLiteral TBool | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> - cassert (int_ty1 = int_ty2) meta "TODO: error message"; + sanity_check (int_ty1 = int_ty2) meta; TLiteral (TInteger int_ty1) | Shl | Shr -> (* The number of bits can be of a different integer type @@ -632,7 +632,7 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) (bkind : bo In practice this restricted the behaviour too much, so for now we forbid them. *) - cassert (bkind <> BShallow) meta "Shallow borrow are currently forbidden"; + sanity_check (bkind <> BShallow) meta; (* Access the value *) let access = @@ -744,9 +744,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind : AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id opt_variant_id generics in - cassert ( + sanity_check ( expected_field_types - = List.map (fun (v : typed_value) -> v.ty) values) meta "TODO: error message"; + = List.map (fun (v : typed_value) -> v.ty) values) meta; (* Construct the value *) let av : adt_value = { variant_id = opt_variant_id; field_values = values } @@ -815,7 +815,7 @@ let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun = in let cf_continue cf v : m_fun = fun ctx -> - cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message"; + cassert (not (bottom_in_value ctx.ended_regions v)) meta "Fake read: the value contains bottom"; cf ctx in comp cf_prepare cf_continue cf ctx diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 4d4b709e..d2f1b5fb 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -68,7 +68,7 @@ let eval_loop_symbolic (config : config) (meta : meta) fun cf ctx -> (* Debug *) log#ldebug - (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n")); + (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n")); (* Generate a fresh loop id *) let loop_id = fresh_loop_id () in @@ -81,8 +81,8 @@ let eval_loop_symbolic (config : config) (meta : meta) (* Debug *) log#ldebug (lazy - ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string meta ctx - ^ "\n\nFixed point:\n" ^ eval_ctx_to_string meta fp_ctx)); + ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n\nFixed point:\n" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx)); (* Compute the loop input parameters *) let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values meta ctx fp_ctx in @@ -122,8 +122,8 @@ let eval_loop_symbolic (config : config) (meta : meta) (lazy ("eval_loop_symbolic: about to match the fixed-point context with the \ original context:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx - ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string meta ctx)); + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); let end_expr : SymbolicAst.expression option = match_ctx_with_target config meta loop_id true fp_bl_corresp fp_input_svalues fixed_ids fp_ctx cf ctx @@ -155,8 +155,8 @@ let eval_loop_symbolic (config : config) (meta : meta) (lazy ("eval_loop_symbolic: about to match the fixed-point context \ with the context at a continue:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx - ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string meta ctx)); + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); let cc = match_ctx_with_target config meta loop_id false fp_bl_corresp fp_input_svalues fixed_ids fp_ctx @@ -173,9 +173,9 @@ let eval_loop_symbolic (config : config) (meta : meta) log#ldebug (lazy ("eval_loop_symbolic: result:" ^ "\n- src context:\n" - ^ eval_ctx_to_string_no_filter meta ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx ^ "\n- fixed point:\n" - ^ eval_ctx_to_string_no_filter meta fp_ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx ^ "\n- fixed_sids: " ^ SymbolicValueId.Set.show fixed_ids.sids ^ "\n- fresh_sids: " @@ -209,7 +209,7 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ABorrow (AMutBorrow (bid, child_av)) -> - cassert (is_aignored child_av.value) meta "TODO: error message"; + sanity_check (is_aignored child_av.value) meta; Some (bid, child_av.ty) | ABorrow (ASharedBorrow _) -> None | _ -> craise meta "Unreachable") @@ -222,7 +222,7 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ALoan (AMutLoan (bid, child_av)) -> - cassert (is_aignored child_av.value) meta "TODO: error message"; + sanity_check (is_aignored child_av.value) meta; Some bid | ALoan (ASharedLoan _) -> None | _ -> craise meta "Unreachable") @@ -241,7 +241,7 @@ let eval_loop_symbolic (config : config) (meta : meta) ty) loan_ids in - cassert (BorrowId.Map.is_empty !borrows) meta "TODO: error message"; + sanity_check (BorrowId.Map.is_empty !borrows) meta; given_back_tys in diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index 6ef4a13b..2de5aed0 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -53,16 +53,17 @@ type abs_borrows_loans_maps = { regions. *) module type PrimMatcher = sig - val match_etys : Meta.meta -> eval_ctx -> eval_ctx -> ety -> ety -> ety - val match_rtys : Meta.meta -> eval_ctx -> eval_ctx -> rty -> rty -> rty + val meta : Meta.meta + val match_etys : eval_ctx -> eval_ctx -> ety -> ety -> ety + val match_rtys : eval_ctx -> eval_ctx -> rty -> rty -> rty (** The input primitive values are not equal *) val match_distinct_literals : - Meta.meta -> eval_ctx -> eval_ctx -> ety -> literal -> literal -> typed_value + eval_ctx -> eval_ctx -> ety -> literal -> literal -> typed_value (** The input ADTs don't have the same variant *) val match_distinct_adts : - Meta.meta -> eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value + eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value (** The meta-value is the result of a match. @@ -75,7 +76,6 @@ module type PrimMatcher = sig calling the match function. *) val match_shared_borrows : - Meta.meta -> eval_ctx -> eval_ctx -> (typed_value -> typed_value -> typed_value) -> @@ -93,7 +93,6 @@ module type PrimMatcher = sig - [bv]: the result of matching [bv0] with [bv1] *) val match_mut_borrows : - Meta.meta -> eval_ctx -> eval_ctx -> ety -> @@ -111,7 +110,6 @@ module type PrimMatcher = sig [v]: the result of matching the shared values coming from the two loans *) val match_shared_loans : - Meta.meta -> eval_ctx -> eval_ctx -> ety -> @@ -125,7 +123,7 @@ module type PrimMatcher = sig (** There are no constraints on the input symbolic values *) val match_symbolic_values : - Meta.meta -> eval_ctx -> eval_ctx -> symbolic_value -> symbolic_value -> symbolic_value + eval_ctx -> eval_ctx -> symbolic_value -> symbolic_value -> symbolic_value (** Match a symbolic value with a value which is not symbolic. @@ -135,7 +133,7 @@ module type PrimMatcher = sig end loans in one of the two environments). *) val match_symbolic_with_other : - Meta.meta -> eval_ctx -> eval_ctx -> bool -> symbolic_value -> typed_value -> typed_value + eval_ctx -> eval_ctx -> bool -> symbolic_value -> typed_value -> typed_value (** Match a bottom value with a value which is not bottom. @@ -145,11 +143,10 @@ module type PrimMatcher = sig end loans in one of the two environments). *) val match_bottom_with_other : - Meta.meta -> eval_ctx -> eval_ctx -> bool -> typed_value -> typed_value + eval_ctx -> eval_ctx -> bool -> typed_value -> typed_value (** The input ADTs don't have the same variant *) val match_distinct_aadts : - Meta.meta -> eval_ctx -> eval_ctx -> rty -> @@ -167,7 +164,6 @@ module type PrimMatcher = sig [ty]: result of matching ty0 and ty1 *) val match_ashared_borrows : - Meta.meta -> eval_ctx -> eval_ctx -> rty -> @@ -188,7 +184,6 @@ module type PrimMatcher = sig [av]: result of matching av0 and av1 *) val match_amut_borrows : - Meta.meta -> eval_ctx -> eval_ctx -> rty -> @@ -215,7 +210,6 @@ module type PrimMatcher = sig [av]: result of matching av0 and av1 *) val match_ashared_loans : - Meta.meta -> eval_ctx -> eval_ctx -> rty -> @@ -242,7 +236,6 @@ module type PrimMatcher = sig [av]: result of matching av0 and av1 *) val match_amut_loans : - Meta.meta -> eval_ctx -> eval_ctx -> rty -> @@ -259,7 +252,7 @@ module type PrimMatcher = sig is typically used to raise the proper exception). *) val match_avalues : - Meta.meta -> eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue + eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue end module type Matcher = sig @@ -267,15 +260,16 @@ module type Matcher = sig Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}. *) + val meta : Meta.meta val match_typed_values : - Meta.meta -> eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value + eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value (** Match two avalues. Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}. *) val match_typed_avalues : - Meta.meta -> eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue + eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue end (** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and @@ -304,6 +298,7 @@ module type MatchCheckEquivState = sig val aid_map : AbstractionId.InjSubst.t ref val lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value val lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value + val meta : Meta.meta end module type CheckEquivMatcher = sig @@ -353,6 +348,7 @@ module type MatchJoinState = sig (** The abstractions introduced when performing the matches *) val nabs : abs list ref + val meta : Meta.meta end (** Split an environment between the fixed abstractions, values, etc. and diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 44b9a44e..f6ce9b32 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -272,7 +272,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f 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 "; + cassert (ty_no_regions sv.ty) meta "Nested borrows are not supported yet"; let rty = sv.ty in (* Create the shared loan child *) @@ -461,9 +461,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id (lazy ("compute_loop_entry_fixed_point: after prepare_ashared_loans:" ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter meta ctx0 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0 ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx ^ "\n\n")); let cf_exit_loop_body (res : statement_eval_res) : m_fun = @@ -597,9 +597,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id log#ldebug (lazy ("compute_fixed_point:" ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter meta ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta ctx1 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1 ^ "\n\n")); (* Check if we reached a fixed point: if not, iterate *) @@ -612,7 +612,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id (lazy ("compute_fixed_point: fixed point computed before matching with input \ region groups:" ^ "\n\n- fp:\n" - ^ eval_ctx_to_string_no_filter meta fp + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp ^ "\n\n")); (* Make sure we have exactly one loop abstraction per function region (merge @@ -634,10 +634,10 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id method! visit_abs _ abs = match abs.kind with | Loop (loop_id', _, kind) -> - cassert (loop_id' = loop_id) meta "TODO : error message "; - cassert (kind = LoopSynthInput) meta "TODO : error message "; + sanity_check (loop_id' = loop_id) meta; + sanity_check (kind = LoopSynthInput) meta; (* The abstractions introduced so far should be endable *) - cassert (abs.can_end = true) meta "The abstractions introduced so far can not end"; + sanity_check (abs.can_end = true) meta; add_aid abs.abs_id; abs | _ -> abs @@ -694,9 +694,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id in (* By default, the [SynthInput] abs can't end *) let ctx = ctx_set_abs_can_end meta ctx abs_id true in - cassert ( + sanity_check ( let abs = ctx_lookup_abs ctx abs_id in - abs.kind = SynthInput rg_id) meta "TODO : error message "; + abs.kind = SynthInput rg_id) meta; (* End this abstraction *) let ctx = InterpreterBorrows.end_abstraction_no_synth config meta abs_id ctx @@ -725,7 +725,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id (* We also check that all the regions need to end - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating... *) - cassert (AbstractionId.Set.equal !aids_union !fp_aids) meta "Not all regions need to end TODO: Error message"; + sanity_check (AbstractionId.Set.equal !aids_union !fp_aids) meta; (* Merge the abstractions which need to be merged, and compute the map from region id to abstraction id *) @@ -815,8 +815,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id method! visit_abs _ abs = match abs.kind with | Loop (loop_id', _, kind) -> - cassert (loop_id' = loop_id) meta "TODO : error message "; - cassert (kind = LoopSynthInput) meta "TODO : error message "; + sanity_check (loop_id' = loop_id) meta; + sanity_check (kind = LoopSynthInput) meta; let kind : abs_kind = if remove_rg_id then Loop (loop_id, None, LoopSynthInput) else abs.kind @@ -838,7 +838,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id (lazy ("compute_fixed_point: fixed point after matching with the function \ region groups:\n" - ^ eval_ctx_to_string_no_filter meta fp_test)); + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_test)); compute_fixed_point fp_test 1 1 in @@ -855,8 +855,8 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se log#ldebug (lazy ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n" - ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string meta src_ctx - ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n")); + ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) src_ctx + ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx ^ "\n\n")); let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in let filt_src_ctx = { src_ctx with env = filt_src_env } in @@ -867,9 +867,9 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se (lazy ("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx:\n" - ^ eval_ctx_to_string meta filt_src_ctx + ^ eval_ctx_to_string ~meta:(Some meta) filt_src_ctx ^ "\n\n- filt_tgt_ctx:\n" - ^ eval_ctx_to_string meta filt_tgt_ctx + ^ eval_ctx_to_string ~meta:(Some meta) filt_tgt_ctx ^ "\n\n")); (* Match the source context and the filtered target context *) @@ -941,7 +941,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se ids.loan_ids in (* Check that the loan and borrows are related *) - cassert (BorrowId.Set.equal ids.borrow_ids loan_ids) meta "The loan and borrows are not related") + sanity_check (BorrowId.Set.equal ids.borrow_ids loan_ids) meta) new_absl; (* For every target abstraction (going back to the [list_nth_mut] example, @@ -1089,9 +1089,9 @@ let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) (fp_ctx : log#ldebug (lazy ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n" - ^ eval_ctx_to_string_no_filter meta ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx ^ "\n- fixed point:\n" - ^ eval_ctx_to_string_no_filter meta fp_ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx ^ "\n- fresh_sids: " ^ SymbolicValueId.Set.show fresh_sids ^ "\n- input_svalues: " diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 74d31975..8153ef08 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -136,7 +136,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id) log#ldebug (lazy ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids - ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string meta ctx0 ^ "\n\n")); + ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n")); let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in let can_end = true in @@ -171,13 +171,13 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id) log#ldebug (lazy ("collapse_ctx: after converting values to abstractions:\n" - ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n" + ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n" )); log#ldebug (lazy ("collapse_ctx: after decomposing the shared values in the abstractions:\n" - ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n" + ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n" )); (* Explore all the *new* abstractions, and compute various maps *) @@ -252,7 +252,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id) ^ AbstractionId.to_string abs_id1 ^ " into " ^ AbstractionId.to_string abs_id0 - ^ ":\n\n" ^ eval_ctx_to_string meta !ctx)); + ^ ":\n\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx)); (* Update the environment - pay attention to the order: we we merge [abs_id1] *into* [abs_id0] *) @@ -272,7 +272,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id) log#ldebug (lazy ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids - ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string meta !ctx ^ "\n\n")); + ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx ^ "\n\n")); (* Reorder the loans and borrows in the fresh abstractions *) let ctx = reorder_loans_borrows_in_fresh_abs meta old_ids.aids !ctx in @@ -281,7 +281,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id) (lazy ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids ^ "\n\n- after collapse and reorder borrows/loans:\n" - ^ eval_ctx_to_string meta ctx ^ "\n\n")); + ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n")); (* Return the new context *) ctx @@ -290,6 +290,7 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id : merge_duplicates_funcs = (* Rem.: the merge functions raise exceptions (that we catch). *) let module S : MatchJoinState = struct + let meta = meta let loop_id = loop_id let nabs = ref [] end in @@ -356,11 +357,11 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id This time we need to also merge the shared values. We rely on the join matcher [JM] to do so. *) - cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message"; - cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta "TODO: error message"; + sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta; + sanity_check (not (value_has_loans_or_borrows ctx sv1.value)) meta; let ty = ty0 in let child = child0 in - let sv = M.match_typed_values meta ctx ctx sv0 sv1 in + let sv = M.match_typed_values ctx ctx sv0 sv1 in let value = ALoan (ASharedLoan (ids, sv, child)) in { value; ty } in @@ -397,9 +398,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c (lazy ("join_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter meta ctx0 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0 ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta ctx1 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1 ^ "\n\n")); let env0 = List.rev ctx0.env in @@ -413,9 +414,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c (lazy ("join_suffixes:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter meta { ctx0 with env = List.rev env0 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx0 with env = List.rev env0 } ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 } ^ "\n\n")); (* Sanity check: there are no values/abstractions which should be in the prefix *) @@ -441,6 +442,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c in let module S : MatchJoinState = struct + let meta = meta let loop_id = loop_id let nabs = nabs end in @@ -468,7 +470,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c (* Still in the prefix: match the values *) cassert (b0 = b1) meta "Bindings are not the same. We are not in the prefix anymore"; let b = b0 in - let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in + let v = M.match_typed_values ctx0 ctx1 v0 v1 in let var = EBinding (BDummy b, v) in (* Continue *) var :: join_prefixes env0' env1') @@ -492,7 +494,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c ids must be the same"; (* Match the values *) let b = b0 in - let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in + let v = M.match_typed_values ctx0 ctx1 v0 v1 in let var = EBinding (BVar b, v) in (* Continue *) var :: join_prefixes env0' env1' @@ -669,21 +671,21 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Destructure the abstractions introduced in the new context *) let ctx = destructure_new_abs meta loop_id fixed_ids.aids ctx in log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Collapse the context we want to add to the join *) let ctx = collapse_ctx meta loop_id None fixed_ids ctx in log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Refresh the fresh abstractions *) let ctx = refresh_abs fixed_ids.aids ctx in @@ -693,7 +695,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after join:\n" - ^ eval_ctx_to_string meta ctx1)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx1)); (* Collapse again - the join might have introduce abstractions we want to merge with the others (note that those abstractions may actually @@ -702,7 +704,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo log#ldebug (lazy ("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n" - ^ eval_ctx_to_string meta !joined_ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) !joined_ctx)); (* Sanity check *) if !Config.sanity_checks then Invariants.check_invariants meta !joined_ctx; diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 435174a7..c02d3117 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -149,9 +149,9 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) let match_rec = match_types meta match_distinct_types match_regions in match (ty0, ty1) with | TAdt (id0, generics0), TAdt (id1, generics1) -> - cassert (id0 = id1) meta "TODO: error message"; - cassert (generics0.const_generics = generics1.const_generics) meta "TODO: error message"; - cassert (generics0.trait_refs = generics1.trait_refs) meta "TODO: error message"; + sanity_check (id0 = id1) meta; + sanity_check (generics0.const_generics = generics1.const_generics) meta; + sanity_check (generics0.trait_refs = generics1.trait_refs) meta; let id = id0 in let const_generics = generics1.const_generics in let trait_refs = generics1.trait_refs in @@ -168,27 +168,28 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty) let generics = { regions; types; const_generics; trait_refs } in TAdt (id, generics) | TVar vid0, TVar vid1 -> - cassert (vid0 = vid1) meta "TODO: error message"; + sanity_check (vid0 = vid1) meta; let vid = vid0 in TVar vid | TLiteral lty0, TLiteral lty1 -> - cassert (lty0 = lty1) meta "TODO: error message"; + sanity_check (lty0 = lty1) meta; ty0 | TNever, TNever -> ty0 | TRef (r0, ty0, k0), TRef (r1, ty1, k1) -> let r = match_regions r0 r1 in let ty = match_rec ty0 ty1 in - cassert (k0 = k1) meta "TODO: error message"; + sanity_check (k0 = k1) meta; let k = k0 in TRef (r, ty, k) | _ -> match_distinct_types ty0 ty1 module MakeMatcher (M : PrimMatcher) : Matcher = struct - let rec match_typed_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let meta = M.meta + let rec match_typed_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (v0 : typed_value) (v1 : typed_value) : typed_value = - let match_rec = match_typed_values meta ctx0 ctx1 in - let ty = M.match_etys meta ctx0 ctx1 v0.ty v1.ty in - (* Using ValuesUtils.value_has_borrows on purpose here: we want + let match_rec = match_typed_values ctx0 ctx1 in + let ty = M.match_etys ctx0 ctx1 v0.ty v1.ty in + (* Using ValuesUtils.value_ has_borrows on purpose here: we want to make explicit the fact that, though we have to pick one of the two contexts (ctx0 here) to call value_has_borrows, it doesn't matter here. *) @@ -197,7 +198,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct in match (v0.value, v1.value) with | VLiteral lv0, VLiteral lv1 -> - if lv0 = lv1 then v1 else M.match_distinct_literals meta ctx0 ctx1 ty lv0 lv1 + if lv0 = lv1 then v1 else M.match_distinct_literals ctx0 ctx1 ty lv0 lv1 | VAdt av0, VAdt av1 -> if av0.variant_id = av1.variant_id then let fields = List.combine av0.field_values av1.field_values in @@ -210,17 +211,17 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct { value; ty = v1.ty } else ( (* For now, we don't merge ADTs which contain borrows *) - cassert (not (value_has_borrows v0.value)) meta "ADTs which contain borrows are not merged yet"; - cassert (not (value_has_borrows v1.value)) meta "ADTs which contain borrows are not merged yet"; + sanity_check (not (value_has_borrows v0.value)) M.meta; + sanity_check (not (value_has_borrows v1.value)) M.meta; (* Merge *) - M.match_distinct_adts meta ctx0 ctx1 ty av0 av1) + M.match_distinct_adts ctx0 ctx1 ty av0 av1) | VBottom, VBottom -> v0 | VBorrow bc0, VBorrow bc1 -> let bc = match (bc0, bc1) with | VSharedBorrow bid0, VSharedBorrow bid1 -> let bid = - M.match_shared_borrows meta ctx0 ctx1 match_rec ty bid0 bid1 + M.match_shared_borrows ctx0 ctx1 match_rec ty bid0 bid1 in VSharedBorrow bid | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) -> @@ -229,9 +230,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct cassert ( not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos - bv.value)) meta "TODO: error message"; + bv.value)) M.meta "TODO: error message"; let bid, bv = - M.match_mut_borrows meta ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv + M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv in VMutBorrow (bid, bv) | VReservedMutBorrow _, _ @@ -242,7 +243,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct trying to match a reserved borrow, which shouldn't happen because reserved borrow should be eliminated very quickly - they are introduced just before function calls which activate them *) - craise meta "Unexpected" + craise M.meta "Unexpected" in { value = VBorrow bc; ty } | VLoan lc0, VLoan lc1 -> @@ -252,23 +253,23 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match (lc0, lc1) with | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) -> let sv = match_rec sv0 sv1 in - cassert (not (value_has_borrows sv.value)) meta "TODO: error message"; - let ids, sv = M.match_shared_loans meta ctx0 ctx1 ty ids0 ids1 sv in + cassert (not (value_has_borrows sv.value)) M.meta "TODO: error message"; + let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in VSharedLoan (ids, sv) | VMutLoan id0, VMutLoan id1 -> let id = M.match_mut_loans ctx0 ctx1 ty id0 id1 in VMutLoan id | VSharedLoan _, VMutLoan _ | VMutLoan _, VSharedLoan _ -> - craise meta "Unreachable" + craise M.meta "Unreachable" in { value = VLoan lc; ty = v1.ty } | VSymbolic sv0, VSymbolic sv1 -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - cassert (not (value_has_borrows v0.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; - cassert (not (value_has_borrows v1.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; + cassert (not (value_has_borrows v0.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; + cassert (not (value_has_borrows v1.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded"; (* Match *) - let sv = M.match_symbolic_values meta ctx0 ctx1 sv0 sv1 in + let sv = M.match_symbolic_values ctx0 ctx1 sv0 sv1 in { v1 with value = VSymbolic sv } | VLoan lc, _ -> ( match lc with @@ -278,27 +279,27 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct match lc with | VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids)) | VMutLoan id -> raise (ValueMatchFailure (LoanInRight id))) - | VSymbolic sv, _ -> M.match_symbolic_with_other meta ctx0 ctx1 true sv v1 - | _, VSymbolic sv -> M.match_symbolic_with_other meta ctx0 ctx1 false sv v0 - | VBottom, _ -> M.match_bottom_with_other meta ctx0 ctx1 true v1 - | _, VBottom -> M.match_bottom_with_other meta ctx0 ctx1 false v0 + | VSymbolic sv, _ -> M.match_symbolic_with_other ctx0 ctx1 true sv v1 + | _, VSymbolic sv -> M.match_symbolic_with_other ctx0 ctx1 false sv v0 + | VBottom, _ -> M.match_bottom_with_other ctx0 ctx1 true v1 + | _, VBottom -> M.match_bottom_with_other ctx0 ctx1 false v0 | _ -> log#ldebug (lazy ("Unexpected match case:\n- value0: " - ^ typed_value_to_string meta ctx0 v0 + ^ typed_value_to_string ~meta:(Some M.meta) ctx0 v0 ^ "\n- value1: " - ^ typed_value_to_string meta ctx1 v1)); - craise meta "Unexpected match case" + ^ typed_value_to_string ~meta:(Some M.meta) ctx1 v1)); + craise M.meta "Unexpected match case" - and match_typed_avalues (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + and match_typed_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) (v0 : typed_avalue) (v1 : typed_avalue) : typed_avalue = log#ldebug (lazy ("match_typed_avalues:\n- value0: " - ^ typed_avalue_to_string meta ctx0 v0 + ^ typed_avalue_to_string ~meta:(Some M.meta) ctx0 v0 ^ "\n- value1: " - ^ typed_avalue_to_string meta ctx1 v1)); + ^ typed_avalue_to_string ~meta:(Some M.meta) ctx1 v1)); (* Using ValuesUtils.value_has_borrows on purpose here: we want to make explicit the fact that, though we have to pick @@ -308,9 +309,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos in - let match_rec = match_typed_values meta ctx0 ctx1 in - let match_arec = match_typed_avalues meta ctx0 ctx1 in - let ty = M.match_rtys meta ctx0 ctx1 v0.ty v1.ty in + let match_rec = match_typed_values ctx0 ctx1 in + let match_arec = match_typed_avalues ctx0 ctx1 in + let ty = M.match_rtys ctx0 ctx1 v0.ty v1.ty in match (v0.value, v1.value) with | AAdt av0, AAdt av1 -> if av0.variant_id = av1.variant_id then @@ -323,15 +324,15 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct in { value; ty } else (* Merge *) - M.match_distinct_aadts meta ctx0 ctx1 v0.ty av0 v1.ty av1 ty - | ABottom, ABottom -> mk_abottom meta ty - | AIgnored, AIgnored -> mk_aignored meta ty + M.match_distinct_aadts ctx0 ctx1 v0.ty av0 v1.ty av1 ty + | ABottom, ABottom -> mk_abottom M.meta ty + | AIgnored, AIgnored -> mk_aignored M.meta ty | ABorrow bc0, ABorrow bc1 -> ( log#ldebug (lazy "match_typed_avalues: borrows"); match (bc0, bc1) with | ASharedBorrow bid0, ASharedBorrow bid1 -> log#ldebug (lazy "match_typed_avalues: shared borrows"); - M.match_ashared_borrows meta ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty + M.match_ashared_borrows ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty | AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) -> log#ldebug (lazy "match_typed_avalues: mut borrows"); log#ldebug @@ -340,10 +341,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut borrows: matched children values"); - M.match_amut_borrows meta ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av + M.match_amut_borrows ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av | AIgnoredMutBorrow _, AIgnoredMutBorrow _ -> (* The abstractions are destructured: we shouldn't get there *) - craise meta "Unexpected" + craise M.meta "Unexpected" | AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> ( match (asb0, asb1) with | [], [] -> @@ -352,7 +353,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct v0 | _ -> (* We should get there only if there are nested borrows *) - craise meta "Unexpected") + craise M.meta "Unexpected") | _ -> (* TODO: getting there is not necessarily inconsistent (it may just be because the environments don't match) so we may want @@ -363,7 +364,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct we are *currently* ending it, in which case we need to completely end it before continuing. *) - craise meta "Unexpected") + craise M.meta "Unexpected") | ALoan lc0, ALoan lc1 -> ( log#ldebug (lazy "match_typed_avalues: loans"); (* TODO: maybe we should enforce that the ids are always exactly the same - @@ -373,8 +374,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct log#ldebug (lazy "match_typed_avalues: shared loans"); let sv = match_rec sv0 sv1 in let av = match_arec av0 av1 in - cassert (not (value_has_borrows sv.value)) meta "TODO: error message"; - M.match_ashared_loans meta ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 + sanity_check (not (value_has_borrows sv.value)) M.meta; + M.match_ashared_loans ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1 av1 ty sv av | AMutLoan (id0, av0), AMutLoan (id1, av1) -> log#ldebug (lazy "match_typed_avalues: mut loans"); @@ -383,48 +384,49 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let av = match_arec av0 av1 in log#ldebug (lazy "match_typed_avalues: mut loans: matched children values"); - M.match_amut_loans meta ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av + M.match_amut_loans ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av | AIgnoredMutLoan _, AIgnoredMutLoan _ | AIgnoredSharedLoan _, AIgnoredSharedLoan _ -> (* Those should have been filtered when destructuring the abstractions - they are necessary only when there are nested borrows *) - craise meta "Unreachable" - | _ -> craise meta "Unreachable") + craise M.meta "Unreachable" + | _ -> craise M.meta "Unreachable") | ASymbolic _, ASymbolic _ -> (* For now, we force all the symbolic values containing borrows to be eagerly expanded, and we don't support nested borrows *) - craise meta "Unreachable" - | _ -> M.match_avalues meta ctx0 ctx1 v0 v1 + craise M.meta "Unreachable" + | _ -> M.match_avalues ctx0 ctx1 v0 v1 end module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (** Small utility *) + let meta = S.meta let push_abs (abs : abs) : unit = S.nabs := abs :: !S.nabs let push_absl (absl : abs list) : unit = List.iter push_abs absl - let match_etys (meta : Meta.meta) _ _ ty0 ty1 = - cassert (ty0 = ty1) meta "TODO: error message"; + let match_etys _ _ ty0 ty1 = + sanity_check (ty0 = ty1) meta; ty0 - let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = + let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows"; + sanity_check (ty0 = ty1) meta; ty0 - let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (_ : literal) : typed_value = mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_distinct_adts (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) + let match_distinct_adts (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety) (adt0 : adt_value) (adt1 : adt_value) : typed_value = (* Check that the ADTs don't contain borrows - this is redundant with checks performed by the caller, but we prefer to be safe with regards to future updates *) let check_no_borrows ctx (v : typed_value) = - cassert (not (value_has_borrows ctx v.value)) meta "ADTs should not contain borrows" + sanity_check (not (value_has_borrows ctx v.value)) meta in List.iter (check_no_borrows ctx0) adt0.field_values; List.iter (check_no_borrows ctx1) adt1.field_values; @@ -452,7 +454,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* No borrows, no loans, no bottoms: we can introduce a symbolic value *) mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_shared_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec + let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec (ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id = (* Lookup the shared values and match them - we do this mostly to make sure we end loans which might appear on one side @@ -508,7 +510,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) bid2 - let match_mut_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_mut_borrows (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety) (bid0 : borrow_id) (bv0 : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value = if bid0 = bid1 then ( @@ -560,10 +562,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct will update [v], while the backward loop function will return nothing. *) cassert ( - not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "TODO: error message"; + not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "Nested borrows are not supported yet"; if bv0 = bv1 then ( - cassert (bv0 = bv) meta "TODO: error message"; + sanity_check (bv0 = bv) meta; (bid0, bv)) else let rid = fresh_region_id () in @@ -571,7 +573,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct let kind = RMut in let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta "TODO: error message"; + sanity_check (ty_no_regions bv_ty) meta; let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in let borrow_av = @@ -624,7 +626,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Generate the avalues for the abstraction *) let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue = let bv_ty = bv.ty in - cassert (ty_no_regions bv_ty) meta "TODO: error message"; + cassert (ty_no_regions bv_ty) meta "Nested borrows are not supported yet"; let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in { value; ty = borrow_ty } in @@ -654,7 +656,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return the new borrow *) (bid2, sv) - let match_shared_loans (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = (* Check if the ids are the same - Rem.: we forbid the sets of loans @@ -671,7 +673,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct raise (ValueMatchFailure (LoansInRight extra_ids_right)); (* This should always be true if we get here *) - cassert (ids0 = ids1) meta "This should always be true if we get here "; + sanity_check (ids0 = ids1) meta; let ids = ids0 in (* Return *) @@ -685,7 +687,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct both borrows *) raise (ValueMatchFailure (LoanInLeft id0)) - let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -697,11 +699,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct else ( (* The caller should have checked that the symbolic values don't contain borrows *) - cassert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta "The caller should have checked that the symbolic values don't contain borrows"; + sanity_check (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta; (* We simply introduce a fresh symbolic value *) mk_fresh_symbolic_value meta sv0.sv_ty) - let match_symbolic_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = (* Check that: - there are no borrows in the symbolic value @@ -729,7 +731,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* Return a fresh symbolic value *) mk_fresh_symbolic_typed_value meta sv.sv_ty - let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* If there are outer loans in the non-bottom value, raise an exception. Otherwise, convert it to an abstraction and return [Bottom]. @@ -770,15 +772,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" + let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ = + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_avalues (meta: Meta.meta) _ _ _ _ = craise meta "Unreachable" + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_avalues _ _ _ _ = craise meta "Unreachable" end (* Very annoying: functors only take modules as inputs... *) @@ -788,6 +790,7 @@ module type MatchMoveState = sig (** The moved values *) val nvalues : typed_value list ref + val meta : Meta.meta end (* We use this matcher to move values in environment. @@ -808,40 +811,41 @@ end *) module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (** Small utility *) + let meta = S.meta let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues - let match_etys (meta : Meta.meta) _ _ ty0 ty1 = - cassert (ty0 = ty1) meta "TODO: error message"; + let match_etys _ _ ty0 ty1 = + sanity_check (ty0 = ty1) meta; ty0 - let match_rtys (meta : Meta.meta) _ _ ty0 ty1 = + let match_rtys _ _ ty0 ty1 = (* The types must be equal - in effect, this forbids to match symbolic values containing borrows *) - cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows"; + sanity_check (ty0 = ty1) meta; ty0 - let match_distinct_literals (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (l : literal) : typed_value = { value = VLiteral l; ty } - let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : adt_value) (adt1 : adt_value) : typed_value = (* Note that if there was a bottom inside the ADT on the left, the value on the left should have been simplified to bottom. *) { ty; value = VAdt adt1 } - let match_shared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety) + let match_shared_borrows (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety) (_ : borrow_id) (bid1 : borrow_id) : borrow_id = (* There can't be bottoms in shared values *) bid1 - let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id) + let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id) (_ : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (_ : typed_value) : borrow_id * typed_value = (* There can't be bottoms in borrowed values *) (bid1, bv1) - let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = (* There can't be bottoms in shared loans *) @@ -851,15 +855,15 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (id1 : loan_id) : loan_id = id1 - let match_symbolic_values (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value) + let match_symbolic_values (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value) (sv1 : symbolic_value) : symbolic_value = sv1 - let match_symbolic_with_other (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = if left then v else mk_typed_value_from_symbolic_value sv - let match_bottom_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (v : typed_value) : typed_value = let with_borrows = false in if left then ( @@ -891,22 +895,21 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (* As explained in comments: we don't use the join matcher to join avalues, only concrete values *) - let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable" + let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_ashared_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ = + let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_amut_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" - let match_avalues (meta : Meta.meta) _ _ _ _ = craise meta "Unreachable" + let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable" + let match_avalues _ _ _ _ = craise meta "Unreachable" end module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher = struct module MkGetSetM (Id : Identifiers.Id) = struct module Inj = Id.InjSubst - let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) = (* Check if k0 is already registered as a key *) match Inj.find_opt k0 !m with @@ -945,7 +948,7 @@ struct Id.Set.of_list (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) end - + let meta = S.meta module GetSetRid = MkGetSetM (RegionId) let match_rid = GetSetRid.match_e "match_rid: " S.rid_map @@ -989,10 +992,10 @@ struct let match_aids = GetSetAid.match_es "match_aids: " S.aid_map (** *) - let match_etys (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = + let match_etys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = if ty0 <> ty1 then raise (Distinct "match_etys") else ty0 - let match_rtys (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = + let match_rtys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 = let match_distinct_types _ _ = raise (Distinct "match_rtys") in let match_regions r0 r1 = match (r0, r1) with @@ -1004,15 +1007,15 @@ struct in match_types meta match_distinct_types match_regions ty0 ty1 - let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety) + let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety) (_ : literal) (_ : literal) : typed_value = mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty - let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) + let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) (_adt0 : adt_value) (_adt1 : adt_value) : typed_value = raise (Distinct "match_distinct_adts") - let match_shared_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) (match_typed_values : typed_value -> typed_value -> typed_value) (_ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id = log#ldebug @@ -1033,22 +1036,22 @@ struct (lazy ("MakeCheckEquivMatcher: match_shared_borrows: looked up values:" ^ "sv0: " - ^ typed_value_to_string meta ctx0 v0 + ^ typed_value_to_string ~meta:(Some meta) ctx0 v0 ^ ", sv1: " - ^ typed_value_to_string meta ctx1 v1)); + ^ typed_value_to_string ~meta:(Some meta) ctx1 v1)); let _ = match_typed_values v0 v1 in () in bid - let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) + let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ty : ety) (bid0 : borrow_id) (_bv0 : typed_value) (bid1 : borrow_id) (_bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value = let bid = match_borrow_id bid0 bid1 in (bid, bv) - let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) + let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) : loan_id_set * typed_value = let ids = match_loan_ids ids0 ids1 in @@ -1058,7 +1061,7 @@ struct (bid1 : loan_id) : loan_id = match_loan_id bid0 bid1 - let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -1077,12 +1080,12 @@ struct let sv_id = GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1 in - let sv_ty = match_rtys meta ctx0 ctx1 sv0.sv_ty sv1.sv_ty in + let sv_ty = match_rtys ctx0 ctx1 sv0.sv_ty sv1.sv_ty in let sv = { sv_id; sv_ty } in sv else ( (* Check: fixed values are fixed *) - cassert (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta "Fixed values should be fixed"; + sanity_check (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta; (* Update the symbolic value mapping *) let sv1 = mk_typed_value_from_symbolic_value sv1 in @@ -1095,21 +1098,21 @@ struct we want *) sv0) - let match_symbolic_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool) + let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( - cassert left meta "TODO: error message"; + sanity_check left meta; let id = sv.sv_id in (* Check: fixed values are fixed *) - cassert (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta "Fixed values should be fixed"; + sanity_check (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta; (* Update the binding for the target symbolic value *) S.sid_to_value_map := SymbolicValueId.Map.add_strict id v !S.sid_to_value_map; (* Return - the returned value is not used, so we can return whatever we want *) v) - let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) + let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = (* It can happen that some variables get initialized in some branches and not in some others, which causes problems when matching. *) @@ -1126,47 +1129,47 @@ struct ^ Print.bool_to_string left ^ "\n- value to match with bottom:\n" ^ show_typed_value v)) - let match_distinct_aadts _ _ _ _ _ _ _ _ = + let match_distinct_aadts _ _ _ _ _ _ _ = raise (Distinct "match_distinct_adts") - let match_ashared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty + let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty = let bid = match_borrow_id bid0 bid1 in let value = ABorrow (ASharedBorrow bid) in { value; ty } - let match_amut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1 + let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1 _av1 ty av = let bid = match_borrow_id bid0 bid1 in let value = ABorrow (AMutBorrow (bid, av)) in { value; ty } - let match_ashared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1 + let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1 ids1 _v1 _av1 ty v av = let bids = match_loan_ids ids0 ids1 in let value = ALoan (ASharedLoan (bids, v, av)) in { value; ty } - let match_amut_loans (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 + let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1 id1 _av1 ty av = log#ldebug (lazy ("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: " ^ BorrowId.to_string id0 ^ "\n- id1: " ^ BorrowId.to_string id1 ^ "\n- ty: " ^ ty_to_string ctx0 ty ^ "\n- av: " - ^ typed_avalue_to_string meta ctx1 av)); + ^ typed_avalue_to_string ~meta:(Some meta) ctx1 av)); let id = match_loan_id id0 id1 in let value = ALoan (AMutLoan (id, av)) in { value; ty } - let match_avalues (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = + let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 = log#ldebug (lazy ("avalues don't match:\n- v0: " - ^ typed_avalue_to_string meta ctx0 v0 + ^ typed_avalue_to_string ~meta:(Some meta) ctx0 v0 ^ "\n- v1: " - ^ typed_avalue_to_string meta ctx1 v1)); + ^ typed_avalue_to_string ~meta:(Some meta) ctx1 v1)); raise (Distinct "match_avalues") end @@ -1178,9 +1181,9 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) (lazy ("match_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter meta ctx0 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0 ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta ctx1 + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1 ^ "\n\n")); (* Initialize the maps and instantiate the matcher *) @@ -1222,6 +1225,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) in let module S : MatchCheckEquivState = struct + let meta = meta let check_equiv = check_equiv let rid_map = rid_map let blid_map = blid_map @@ -1288,7 +1292,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) log#ldebug (lazy "match_abstractions: matching values"); let _ = List.map - (fun (v0, v1) -> M.match_typed_avalues meta ctx0 ctx1 v0 v1) + (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1) (List.combine avalues0 avalues1) in log#ldebug (lazy "match_abstractions: values matched OK"); @@ -1309,9 +1313,9 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) ^ "\n- aid_map: " ^ AbstractionId.InjSubst.show_t !aid_map ^ "\n\n- ctx0:\n" - ^ eval_ctx_to_string_no_filter meta { ctx0 with env = List.rev env0 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx0 with env = List.rev env0 } ^ "\n\n- ctx1:\n" - ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 } + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 } ^ "\n\n")); match (env0, env1) with @@ -1320,19 +1324,19 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) be the same and their values equal (and the borrows/loans/symbolic *) if DummyVarId.Set.mem b0 fixed_ids.dids then ( (* Fixed values: the values must be equal *) - cassert (b0 = b1) meta "The fixed values should be equal"; - cassert (v0 = v1) meta "The fixed values should be equal"; + sanity_check (b0 = b1) meta; + sanity_check (v0 = v1) meta; (* The ids present in the left value must be fixed *) let ids, _ = compute_typed_value_ids v0 in - cassert ((not S.check_equiv) || ids_are_fixed ids)) meta "TODO: error message"; + sanity_check ((not S.check_equiv) || ids_are_fixed ids)) meta; (* We still match the values - allows to compute mappings (which are the identity actually) *) - let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in + let _ = M.match_typed_values ctx0 ctx1 v0 v1 in match_envs env0' env1' | EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' -> - cassert (b0 = b1) meta "TODO: error message"; + sanity_check (b0 = b1) meta; (* Match the values *) - let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in + let _ = M.match_typed_values ctx0 ctx1 v0 v1 in (* Continue *) match_envs env0' env1' | EAbs abs0 :: env0', EAbs abs1 :: env1' -> @@ -1341,10 +1345,10 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets) if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then ( log#ldebug (lazy "match_ctxs: match_envs: matching abs: fixed abs"); (* Still in the prefix: the abstractions must be the same *) - cassert (abs0 = abs1) meta "The abstractions should be the same"; + sanity_check (abs0 = abs1) meta; (* Their ids must be fixed *) let ids, _ = compute_abs_ids abs0 in - cassert ((not S.check_equiv) || ids_are_fixed ids) meta "The ids should be fixed"; + sanity_check ((not S.check_equiv) || ids_are_fixed ids) meta; (* Continue *) match_envs env0' env1') else ( @@ -1408,7 +1412,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (lazy ("prepare_match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " - ^ eval_ctx_to_string meta src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string meta tgt_ctx + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx )); (* End the loans which lead to mismatches when joining *) let rec cf_reorganize_join_tgt : cm_fun = @@ -1437,6 +1441,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id let nabs = ref [] in let module S : MatchJoinState = struct + let meta = meta let loop_id = loop_id let nabs = nabs end in @@ -1448,12 +1453,12 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) -> - cassert (b0 = b1) meta "TODO: error message"; - let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in () | EBinding (BVar b0, v0), EBinding (BVar b1, v1) -> - cassert (b0 = b1) meta "TODO: error message"; - let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in () | _ -> craise meta "Unexpected") (List.combine filt_src_env filt_tgt_env) @@ -1475,6 +1480,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id environment *) let nvalues = ref [] in let module S : MatchMoveState = struct + let meta = meta let loop_id = loop_id let nvalues = nvalues end in @@ -1485,12 +1491,12 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (fun (var0, var1) -> match (var0, var1) with | EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) -> - cassert (b0 = b1) meta "TODO: error message"; - let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in (var1, v) | EBinding (BVar b0, v0), EBinding ((BVar b1 as var1), v1) -> - cassert (b0 = b1) meta "TODO: error message"; - let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in + sanity_check (b0 = b1) meta; + let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in (var1, v) | _ -> craise meta "Unexpected") (List.combine filt_src_env filt_tgt_env) @@ -1520,8 +1526,8 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id (lazy ("cf_reorganize_join_tgt: done with borrows/loans and moves:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " - ^ eval_ctx_to_string meta src_ctx ^ "\n- tgt_ctx: " - ^ eval_ctx_to_string meta tgt_ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n- tgt_ctx: " + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); cf tgt_ctx with ValueMatchFailure e -> @@ -1590,7 +1596,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) let filt_src_env, new_absl, new_dummyl = ctx_split_fixed_new meta fixed_ids src_ctx in - cassert (new_dummyl = []) meta "TODO: error message"; + sanity_check (new_dummyl = []) meta; let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in let filt_src_ctx = { src_ctx with env = filt_src_env } in @@ -1622,13 +1628,13 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) log#ldebug (lazy ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: " - ^ eval_ctx_to_string meta src_ctx ^ "\n\n- tgt_ctx: " - ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n- filt_tgt_ctx: " - ^ eval_ctx_to_string_no_filter meta filt_tgt_ctx + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n\n- tgt_ctx: " + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx ^ "\n\n- filt_tgt_ctx: " + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_tgt_ctx ^ "\n\n- filt_src_ctx: " - ^ eval_ctx_to_string_no_filter meta filt_src_ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_src_ctx ^ "\n\n- new_absl:\n" - ^ eval_ctx_to_string meta + ^ eval_ctx_to_string ~meta:(Some meta) { src_ctx with env = List.map (fun abs -> EAbs abs) new_absl } ^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n" ^ show_borrow_loan_corresp fp_bl_maps @@ -1726,7 +1732,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) abstractions and in the *variable bindings* once we allow symbolic values containing borrows to not be eagerly expanded. *) - cassert Config.greedy_expand_symbolics_with_borrows meta "TODO: error message"; + sanity_check Config.greedy_expand_symbolics_with_borrows meta; (* Update the borrows and loans in the abstractions of the target context. @@ -1795,8 +1801,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) (* No mapping: this means that the borrow was mapped when we matched values (it doesn't come from a fresh abstraction) and because of this, it should actually be mapped to itself *) - cassert ( - BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta "The borrow should mapped to itself: no mapping means that the borrow was mapped when we matched values (it doesn't come from a fresh abstraction) "; + sanity_check ( + BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta; id | Some id -> id @@ -1808,8 +1814,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) method! visit_abs env abs = match abs.kind with | Loop (loop_id', rg_id, kind) -> - cassert (loop_id' = loop_id) meta "TODO: error message"; - cassert (kind = LoopSynthInput) meta "TODO: error message"; + sanity_check (loop_id' = loop_id) meta; + sanity_check (kind = LoopSynthInput) meta; let can_end = false in let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in let abs = { abs with kind; can_end } in @@ -1827,7 +1833,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) log#ldebug (lazy ("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n\ - - result ctx:\n" ^ eval_ctx_to_string meta tgt_ctx)); + - result ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); (* Sanity check *) if !Config.sanity_checks then diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 3733c06d..93ce0515 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -100,8 +100,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx : (* Check consistency *) (match (proj_kind, type_id) with | ProjAdt (def_id, opt_variant_id), TAdtId def_id' -> - cassert (def_id = def_id') meta "TODO: Error message"; - cassert (opt_variant_id = adt.variant_id) meta "TODO: Error message" + sanity_check (def_id = def_id') meta; + sanity_check (opt_variant_id = adt.variant_id) meta | _ -> craise meta "Unreachable"); (* Actually project *) let fv = FieldId.nth adt.field_values field_id in @@ -117,7 +117,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx : Ok (ctx, { res with updated })) (* Tuples *) | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> ( - cassert (arity = List.length adt.field_values) meta "TODO: Error message"; + sanity_check (arity = List.length adt.field_values) meta; let fv = FieldId.nth adt.field_values field_id in (* Project *) match access_projection meta access ctx update p' fv with @@ -349,16 +349,16 @@ let write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : type let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option) (generics : generic_args) : typed_value = - cassert (TypesUtils.generic_args_only_erased_regions generics) meta "TODO: Error message"; + sanity_check (TypesUtils.generic_args_only_erased_regions generics) meta; (* Lookup the definition and check if it is an enumeration - it should be an enumeration if and only if the projection element is a field projection with *some* variant id. Retrieve the list of fields at the same time. *) let def = ctx_lookup_type_decl ctx def_id in - cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message"; + sanity_check (List.length generics.regions = List.length def.generics.regions) meta; (* Compute the field types *) let field_types = - AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id + AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def opt_variant_id generics in (* Initialize the expanded value *) @@ -425,14 +425,14 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind (* "Regular" ADTs *) | ( Field (ProjAdt (def_id, opt_variant_id), _), TAdt (TAdtId def_id', generics) ) -> - cassert (def_id = def_id') meta "TODO: Error message"; + sanity_check (def_id = def_id') meta; compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id generics (* Tuples *) | ( Field (ProjTuple arity, _), TAdt (TTuple, { regions = []; types; const_generics = []; trait_refs = [] }) ) -> - cassert (arity = List.length types) meta "TODO: Error message"; + sanity_check (arity = List.length types) meta; (* Generate the field values *) compute_expanded_bottom_tuple_value meta types | _ -> @@ -616,7 +616,7 @@ let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_ log#ldebug (lazy ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p - ^ "\n- Initial context:\n" ^ eval_ctx_to_string meta ctx)); + ^ "\n- Initial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Access the place *) let access = Write in let cc = update_ctx_along_write_place config meta access p in diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 5f83b938..809303ae 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -84,7 +84,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx) | VLoan _, _ -> craise meta "Unreachable" | VSymbolic s, _ -> (* Check that the projection doesn't contain ended regions *) - cassert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta "TODO: error message"; + sanity_check (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta; [ AsbProjReborrows (s, ty) ] | _ -> craise meta "Unreachable" @@ -212,13 +212,13 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) ( ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: " ^ RegionId.Set.to_string None rset2 ^ "\n")); - cassert (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta "TODO: error message"; + sanity_check (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta; ASymbolic (AProjBorrows (s, ty)) | _ -> log#lerror (lazy ("apply_proj_borrows: unexpected inputs:\n- input value: " - ^ typed_value_to_string meta ctx v + ^ typed_value_to_string ~meta:(Some meta) ctx v ^ "\n- proj rty: " ^ ty_to_string ctx ty)); craise meta "Unreachable" in @@ -464,7 +464,7 @@ let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id) (* Visit *) let ctx = obj#visit_eval_ctx () ctx in (* Check that there are no reborrows remaining *) - cassert (!reborrows = []) meta "TODO: error message"; + sanity_check (!reborrows = []) meta; (* Return *) ctx @@ -483,7 +483,7 @@ let prepare_reborrows (config : config) (meta : Meta.meta) (allow_reborrows : bo let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx = match config.mode with | ConcreteMode -> - cassert (!reborrows = []) meta "TODO: error message"; + sanity_check (!reborrows = []) meta; ctx | SymbolicMode -> (* Apply the reborrows *) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 5e8f7c55..a872f24a 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -24,7 +24,7 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Note that we use [Write], not [Move]: we allow to drop values *below* borrows *) let access = Write in (* First make sure we can access the place, by ending loans or expanding @@ -45,7 +45,7 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); cf ctx in (* Compose and apply *) @@ -99,9 +99,9 @@ let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) (p : log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string meta ctx rv + ^ typed_value_to_string ~meta:(Some meta) ctx rv ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) let rvalue_vid = fresh_dummy_var_id () in let cc = push_dummy_var rvalue_vid rv in @@ -119,16 +119,16 @@ let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) (p : let ctx = ctx_push_dummy_var ctx dest_vid mv in (* Write to the destination *) (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) - cassert (not (bottom_in_value ctx.ended_regions rv)) meta "TODO: Error message"; + exec_assert (not (bottom_in_value ctx.ended_regions rv)) meta "The value to move contains bottom"; (* Update the destination *) let ctx = write_place meta Write p rv ctx in (* Debug *) log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string meta ctx rv + ^ typed_value_to_string ~meta:(Some meta) ctx rv ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string meta ctx)); + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Continue *) cf ctx in @@ -149,7 +149,7 @@ let eval_assertion_concrete (config : config) (meta : Meta.meta) (assertion : as if b = assertion.expected then cf Unit ctx else cf Panic ctx | _ -> craise - meta ("Expected a boolean, got: " ^ typed_value_to_string meta ctx v) + meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) comp eval_op eval_assert cf ctx @@ -167,7 +167,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) (* Evaluate the assertion *) let eval_assert cf (v : typed_value) : m_fun = fun ctx -> - cassert (v.ty = TLiteral TBool) meta "TODO: Error message"; + sanity_check (v.ty = TLiteral TBool) meta; (* We make a choice here: we could completely decouple the concrete and * symbolic executions here but choose not to. In the case where we * know the concrete value of the boolean we test, we use this value @@ -178,8 +178,8 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) (* Delegate to the concrete evaluation function *) eval_assertion_concrete config meta assertion cf ctx | VSymbolic sv -> - cassert (config.mode = SymbolicMode) meta "TODO: Error message"; - cassert (sv.sv_ty = TLiteral TBool) meta "TODO: Error message"; + sanity_check(config.mode = SymbolicMode) meta; + sanity_check (sv.sv_ty = TLiteral TBool) meta; (* We continue the execution as if the test had succeeded, and thus * perform the symbolic expansion: sv ~~> true. * We will of course synthesize an assertion in the generated code @@ -194,7 +194,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) S.synthesize_assertion ctx v expr | _ -> craise - meta ("Expected a boolean, got: " ^ typed_value_to_string meta ctx v) + meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) comp eval_op eval_assert cf ctx @@ -218,7 +218,7 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) (variant_i ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p ^ "\n- variant id: " ^ VariantId.to_string variant_id - ^ "\n- initial context:\n" ^ eval_ctx_to_string meta ctx)); + ^ "\n- initial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Access the value *) let access = Write in let cc = update_ctx_along_read_place config meta access p in @@ -259,7 +259,7 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) (variant_i in assign_to_place config meta bottom_v p (cf Unit) ctx | _, VSymbolic _ -> - cassert (config.mode = SymbolicMode) meta "The Config mode should be SymbolicMode"; + sanity_check (config.mode = SymbolicMode) meta; (* This is a bit annoying: in theory we should expand the symbolic value * then set the discriminant, because in the case the discriminant is * exactly the one we set, the fields are left untouched, and in the @@ -287,13 +287,13 @@ let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) *) let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) (fid : assumed_fun_id) (generics : generic_args) : ety = - cassert (generics.trait_refs = []) meta "TODO: Error message"; + sanity_check (generics.trait_refs = []) meta; (* [Box::free] has a special treatment *) match fid with | BoxFree -> - cassert (generics.regions = []) meta "TODO: Error message"; - cassert (List.length generics.types = 1) meta "TODO: Error message"; - cassert (generics.const_generics = []) meta "TODO: Error message"; + sanity_check (generics.regions = []) meta; + sanity_check (List.length generics.types = 1) meta; + sanity_check (generics.const_generics = []) meta; mk_unit_ty | _ -> (* Retrieve the function's signature *) @@ -324,7 +324,7 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = fun ctx -> (* Debug *) - log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string meta ctx)); + log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* List the local variables, but the return variable *) let ret_vid = VarId.zero in @@ -377,7 +377,7 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) log#ldebug (lazy ("pop_frame: after dropping outer loans in local variables:\n" - ^ eval_ctx_to_string meta ctx))) + ^ eval_ctx_to_string ~meta:(Some meta) ctx))) in (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all @@ -479,7 +479,7 @@ let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args) (* Required type checking *) let input_box = InterpreterPaths.read_place meta Write input_box_place ctx in (let input_ty = ty_get_box input_box.ty in - cassert (input_ty = boxed_ty)) meta "TODO: Error message"; + sanity_check (input_ty = boxed_ty)) meta; (* Drop the value *) let cc = drop_value config meta input_box_place in @@ -930,7 +930,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = (lazy ("\n**About to evaluate statement**: [\n" ^ statement_to_string_with_tab ctx st - ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string st.meta ctx ^ "\n\n")); + ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ~meta:(Some st.meta) ctx ^ "\n\n")); (* Take a snapshot of the current context for the purpose of generating pretty names *) let cc = S.cf_save_snapshot in @@ -963,7 +963,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = log#ldebug (lazy ("about to assign to place: " ^ place_to_string ctx p - ^ "\n- Context:\n" ^ eval_ctx_to_string st.meta ctx)); + ^ "\n- Context:\n" ^ eval_ctx_to_string ~meta:(Some st.meta) ctx)); match res with | Error EPanic -> cf Panic ctx | Ok rv -> ( @@ -1037,7 +1037,7 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) | SymbolicMode -> (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) - cassert (ty_no_regions global.ty) meta "TODO: Error message"; + cassert (ty_no_regions global.ty) global.meta "Const globals should not contain regions"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in @@ -1049,7 +1049,7 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self global.ty in - let sval = mk_fresh_symbolic_value ty in + let sval = mk_fresh_symbolic_value global.meta ty in let cc = assign_to_place config global.meta (mk_typed_value_from_symbolic_value sval) dest in @@ -1250,7 +1250,7 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) | Some body -> body in (* TODO: we need to normalize the types if we want to correctly support traits *) - cassert (generics.trait_refs = []) body.meta "Traits are not supported yet TODO: error message"; + cassert (generics.trait_refs = []) body.meta "Traits are not supported yet in concrete mode"; (* There shouldn't be any reference to Self *) let tr_self = UnknownTrait __FUNCTION__ in let subst = @@ -1259,7 +1259,7 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) let locals, body_st = Subst.fun_body_substitute_in_body subst body in (* Evaluate the input operands *) - cassert (List.length args = body.arg_count) body.meta "TODO: Error message"; + sanity_check(List.length args = body.arg_count) body.meta; let cc = eval_operands config body.meta args in (* Push a frame delimiter - we use {!comp_transmit} to transmit the result @@ -1295,7 +1295,7 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) let cc = comp cc (push_uninitialized_vars meta locals) in (* Execute the function body *) - let cc = comp cc (eval_function_body config meta body_st) in + let cc = comp cc (eval_function_body config body_st) in (* Pop the stack frame and move the return value to its destination *) let cf_finish cf res = @@ -1387,11 +1387,11 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (meta : Meta.met * be fed to functions (i.e., symbolic values output from function return * values and which contain borrows of borrows can't be used as function * inputs *) - cassert ( + sanity_check ( List.for_all (fun arg -> not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) - args) meta "The input argument should not contain symbolic values that can't be fed to functions TODO: error message"; + args) meta; (* Initialize the abstractions and push them in the context. * First, we define the function which, given an initialized, empty @@ -1538,7 +1538,7 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) (fi regions_hierarchy inst_sig generics None args dest cf ctx (** Evaluate a statement seen as a function body *) -and eval_function_body (config : config) (meta : Meta.meta) (body : statement) : st_cm_fun = +and eval_function_body (config : config) (body : statement) : st_cm_fun = fun cf ctx -> log#ldebug (lazy "eval_function_body:"); let cc = eval_statement config body in @@ -1550,7 +1550,7 @@ and eval_function_body (config : config) (meta : Meta.meta) (body : statement) : * checking the invariants *) let cc = greedy_expand_symbolic_values config body.meta in (* Sanity check *) - let cc = comp_check_ctx cc (Invariants.check_invariants meta) in (* Check if right meta *) + let cc = comp_check_ctx cc (Invariants.check_invariants body.meta) in (* Check if right meta *) (* Continue *) cc (cf res) in diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index 519d2c8e..13743cb1 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -48,4 +48,4 @@ val create_push_abstractions_from_abs_region_groups : val eval_statement : config -> statement -> st_cm_fun (** Evaluate a statement seen as a function body *) -val eval_function_body : config -> Meta.meta -> statement -> st_cm_fun +val eval_function_body : config -> statement -> st_cm_fun diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index be8400f7..a24cd543 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -20,7 +20,7 @@ let log = Logging.interpreter_log let get_cf_ctx_no_synth (meta : Meta.meta) (f : cm_fun) (ctx : eval_ctx) : eval_ctx = let nctx = ref None in let cf ctx = - cassert (!nctx = None) meta "TODO: error message"; + sanity_check (!nctx = None) meta; nctx := Some ctx; None in @@ -62,9 +62,9 @@ let statement_to_string ctx = Print.EvalCtx.statement_to_string ctx "" " " let statement_to_string_with_tab ctx = Print.EvalCtx.statement_to_string ctx " " " " -let env_elem_to_string meta ctx = Print.EvalCtx.env_elem_to_string meta ctx "" " " -let env_to_string meta ctx env = eval_ctx_to_string meta { ctx with env } -let abs_to_string meta ctx = Print.EvalCtx.abs_to_string meta ctx "" " " +let env_elem_to_string meta ctx = Print.EvalCtx.env_elem_to_string ~meta:(Some meta) ctx "" " " +let env_to_string meta ctx env = eval_ctx_to_string ~meta:(Some meta) { ctx with env } +let abs_to_string meta ctx = Print.EvalCtx.abs_to_string ~meta:(Some meta) ctx "" " " let same_symbolic_id (sv0 : symbolic_value) (sv1 : symbolic_value) : bool = sv0.sv_id = sv1.sv_id @@ -85,12 +85,12 @@ let mk_fresh_symbolic_value (meta : Meta.meta) (ty : ty) : symbolic_value = svalue let mk_fresh_symbolic_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : symbolic_value = - cassert (ty_no_regions ty) meta "TODO: error message"; + sanity_check (ty_no_regions ty) meta; mk_fresh_symbolic_value meta ty (** Create a fresh symbolic value *) let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value = - cassert (ty_is_rty rty) meta "TODO: error message"; + sanity_check (ty_is_rty rty) meta; let ty = Substitute.erase_regions rty in (* Generate the fresh a symbolic value *) let value = mk_fresh_symbolic_value meta rty in @@ -98,7 +98,7 @@ let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value = { value; ty } let mk_fresh_symbolic_typed_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : typed_value = - cassert (ty_no_regions ty) meta "TODO: error message"; + sanity_check (ty_no_regions ty) meta; mk_fresh_symbolic_typed_value meta ty (** Create a typed value from a symbolic value. *) @@ -127,7 +127,7 @@ let mk_aproj_loans_value_from_symbolic_value (regions : RegionId.Set.t) (** Create a borrows projector from a symbolic value *) let mk_aproj_borrows_from_symbolic_value (meta : Meta.meta) (proj_regions : RegionId.Set.t) (svalue : symbolic_value) (proj_ty : ty) : aproj = - cassert (ty_is_rty proj_ty) meta "TODO: error message"; + sanity_check (ty_is_rty proj_ty) meta; if ty_has_regions_in_set proj_regions proj_ty then AProjBorrows (svalue, proj_ty) else AIgnoredProjBorrows @@ -153,7 +153,7 @@ let remove_borrow_from_asb (meta : Meta.meta) (bid : BorrowId.id) (asb : abstrac false)) asb in - cassert (!removed = 1) meta "TODO: error message"; + sanity_check (!removed = 1) meta; asb (** We sometimes need to return a value whose type may vary depending on @@ -499,8 +499,8 @@ let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (generics : generic_ (* Generate the type substitution Note that for now we don't support instantiating the type parameters with types containing regions. *) - cassert (List.for_all TypesUtils.ty_no_regions generics.types) meta "TODO: error message"; - cassert (TypesUtils.trait_instance_id_no_regions tr_self) meta "TODO: error message"; + sanity_check (List.for_all TypesUtils.ty_no_regions generics.types) meta; + sanity_check (TypesUtils.trait_instance_id_no_regions tr_self) meta; let tsubst = Substitute.make_type_subst_from_vars sg.generics.types generics.types in diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 50f008b8..9b389ba5 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -55,7 +55,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (* Link all the id representants to a borrow information *) let borrows_infos : borrow_info BorrowId.Map.t ref = ref BorrowId.Map.empty in let context_to_string () : string = - eval_ctx_to_string meta ctx ^ "- representants:\n" + eval_ctx_to_string ~meta:(Some meta) ctx ^ "- representants:\n" ^ ids_reprs_to_string " " !ids_reprs ^ "\n- info:\n" ^ borrows_infos_to_string " " !borrows_infos @@ -77,12 +77,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : let infos = !borrows_infos in (* Use the first borrow id as representant *) let repr_bid = BorrowId.Set.min_elt bids in - cassert (not (BorrowId.Map.mem repr_bid infos)) meta "TODO: Error message"; + sanity_check (not (BorrowId.Map.mem repr_bid infos)) meta; (* Insert the mappings to the representant *) let reprs = BorrowId.Set.fold (fun bid reprs -> - cassert (not (BorrowId.Map.mem bid reprs)) meta "TODO: Error message"; + sanity_check (not (BorrowId.Map.mem bid reprs)) meta; BorrowId.Map.add bid repr_bid reprs) bids reprs in @@ -212,10 +212,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : | RShared, (BShared | BReserved) | RMut, BMut -> () | _ -> craise meta "Invariant not satisfied"); (* A reserved borrow can't point to a value inside an abstraction *) - cassert (kind <> BReserved || not info.loan_in_abs) meta "A reserved borrow can't point to a value inside an abstraction"; + sanity_check (kind <> BReserved || not info.loan_in_abs) meta; (* Insert the borrow id *) let borrow_ids = info.borrow_ids in - cassert (not (BorrowId.Set.mem bid borrow_ids)) meta "TODO: Error message"; + sanity_check (not (BorrowId.Set.mem bid borrow_ids)) meta; let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in (* Update the info in the map *) update_info bid info @@ -270,7 +270,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : List.iter (fun (rkind, bid) -> let info = find_info bid in - cassert (info.loan_kind = rkind) meta "Not all the ignored loans are present at the proper place") + sanity_check (info.loan_kind = rkind) meta) !ignored_loans; (* Then, check the borrow infos *) @@ -278,11 +278,11 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : (fun _ info -> (* Note that we can't directly compare the sets - I guess they are * different depending on the order in which we add the elements... *) - cassert ( + sanity_check ( BorrowId.Set.elements info.loan_ids - = BorrowId.Set.elements info.borrow_ids) meta "TODO: Error message"; + = BorrowId.Set.elements info.borrow_ids) meta; match info.loan_kind with - | RMut -> cassert (BorrowId.Set.cardinal info.loan_ids = 1) meta "TODO: Error message" + | RMut -> sanity_check (BorrowId.Set.cardinal info.loan_ids = 1) meta | RShared -> ()) !borrows_infos @@ -297,7 +297,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_VBottom info = (* No ⊥ inside borrowed values *) - cassert (Config.allow_bottom_below_borrow || not info.outer_borrow) meta "There should be no ⊥ inside borrowed values" + sanity_check (Config.allow_bottom_below_borrow || not info.outer_borrow) meta method! visit_ABottom _info = (* ⊥ inside an abstraction is not the same as in a regular value *) @@ -310,7 +310,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | VSharedLoan (_, _) -> set_outer_shared info | VMutLoan _ -> (* No mutable loan inside a shared loan *) - cassert (not info.outer_shared) meta "There should be no mutable loan inside a shared loan"; + sanity_check (not info.outer_shared) meta; set_outer_mut info in (* Continue exploring *) @@ -322,7 +322,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match bc with | VSharedBorrow _ -> set_outer_shared info | VReservedMutBorrow _ -> - cassert (not info.outer_borrow) meta "TODO: Error message"; + sanity_check (not info.outer_borrow) meta; set_outer_shared info | VMutBorrow (_, _) -> set_outer_mut info in @@ -369,7 +369,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) : unit = match (cv, ty) with - | VScalar sv, TInteger int_ty -> cassert (sv.int_ty = int_ty) meta "TODO: Error message" + | VScalar sv, TInteger int_ty -> sanity_check (sv.int_ty = int_ty) meta | VBool _, TBool | VChar _, TChar -> () | _ -> craise meta "Erroneous typing" @@ -393,17 +393,17 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = method! visit_EBinding info binder v = (* We also check that the regions are erased *) - cassert (ty_is_ety v.ty) meta "The regions should be erased"; + sanity_check (ty_is_ety v.ty) meta; super#visit_EBinding info binder v method! visit_symbolic_value inside_abs v = (* Check that the types have regions *) - cassert (ty_is_rty v.sv_ty) meta "The types should have regions"; + sanity_check (ty_is_rty v.sv_ty) meta; super#visit_symbolic_value inside_abs v method! visit_typed_value info tv = (* Check that the types have erased regions *) - cassert (ty_is_ety tv.ty) meta "The types should have erased regions"; + sanity_check (ty_is_ety tv.ty) meta; (* Check the current pair (value, type) *) (match (tv.value, tv.ty) with | VLiteral cv, TLiteral ty -> check_literal_type meta cv ty @@ -413,40 +413,40 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - cassert ( - List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message"; - cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message"; + sanity_check ( + List.length generics.regions = List.length def.generics.regions) meta; + sanity_check (List.length generics.types = List.length def.generics.types) meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent" + sanity_check (VariantId.to_int variant_id < List.length variants) meta | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = - AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def + AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def av.variant_id generics in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The field types are not correct") + (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Tuple case *) | VAdt av, TAdt (TTuple, generics) -> - cassert (generics.regions = []) meta "TODO: Error message"; - cassert (generics.const_generics = []) meta "TODO: Error message"; - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (generics.regions = []) meta; + sanity_check (generics.const_generics = []) meta; + sanity_check (av.variant_id = None) meta; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The fields does not have the proper values or there are not as many fields as field types at the same time TODO: error message") + (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Assumed type case *) | VAdt av, TAdt (TAssumed aty_id, generics) -> ( - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (av.variant_id = None) meta; match ( aty_id, av.field_values, @@ -456,20 +456,20 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ inner_value ], [], [ inner_ty ], [] -> - cassert (inner_value.ty = inner_ty) meta "TODO: Error message" + sanity_check (inner_value.ty = inner_ty) meta | TArray, inner_values, _, [ inner_ty ], [ cg ] -> (* *) - cassert ( + sanity_check ( List.for_all (fun (v : typed_value) -> v.ty = inner_ty) - inner_values) meta "TODO: Error message"; + inner_values) meta; (* The length is necessarily concrete *) let len = (ValuesUtils.literal_as_scalar (TypesUtils.const_generic_as_literal cg)) .value in - cassert (Z.of_int (List.length inner_values) = len) meta "TODO: Error message" + sanity_check (Z.of_int (List.length inner_values) = len) meta | (TSlice | TStr), _, _, _, _ -> craise meta "Unexpected" | _ -> craise meta "Erroneous type") | VBottom, _ -> (* Nothing to check *) () @@ -481,27 +481,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - cassert (sv.ty = ref_ty) meta "TODO: Error message" + sanity_check (sv.ty = ref_ty) meta | _ -> craise meta "Inconsistent context") | VMutBorrow (_, bv), RMut -> - cassert ( + sanity_check ( (* Check that the borrowed value has the proper type *) - bv.ty = ref_ty) meta "TODO: Error message" + bv.ty = ref_ty) meta | _ -> craise meta "Erroneous typing") | VLoan lc, ty -> ( match lc with - | VSharedLoan (_, sv) -> cassert (sv.ty = ty) meta "TODO: Error message" + | VSharedLoan (_, sv) -> sanity_check (sv.ty = ty) meta | VMutLoan bid -> ( (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with - | Concrete (VMutBorrow (_, bv)) -> cassert (bv.ty = ty) meta "The borrowed value does not have the proper type" + | Concrete (VMutBorrow (_, bv)) -> sanity_check (bv.ty = ty) meta | Abstract (AMutBorrow (_, sv)) -> - cassert (Substitute.erase_regions sv.ty = ty) meta "The borrowed value does not have the proper type" + sanity_check (Substitute.erase_regions sv.ty = ty) meta | _ -> craise meta "Inconsistent context")) | VSymbolic sv, ty -> let ty' = Substitute.erase_regions sv.sv_ty in - cassert (ty' = ty) meta "TODO: Error message" + sanity_check (ty' = ty) meta | _ -> craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) super#visit_typed_value info tv @@ -516,7 +516,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * *) method! visit_typed_avalue info atv = (* Check that the types have regions *) - cassert (ty_is_rty atv.ty) meta "The types should have regions"; + sanity_check (ty_is_rty atv.ty) meta; (* Check the current pair (value, type) *) (match (atv.value, atv.ty) with (* ADT case *) @@ -525,43 +525,43 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = * parameters, etc. *) let def = ctx_lookup_type_decl ctx def_id in (* Check the number of parameters *) - cassert ( - List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message"; - cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message"; - cassert ( + sanity_check ( + List.length generics.regions = List.length def.generics.regions) meta; + sanity_check (List.length generics.types = List.length def.generics.types) meta; + sanity_check ( List.length generics.const_generics - = List.length def.generics.const_generics) meta "TODO: Error message"; + = List.length def.generics.const_generics) meta; (* Check that the variant id is consistent *) (match (av.variant_id, def.kind) with | Some variant_id, Enum variants -> - cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent" + sanity_check (VariantId.to_int variant_id < List.length variants) meta | None, Struct _ -> () | _ -> craise meta "Erroneous typing"); (* Check that the field types are correct *) let field_types = - AssociatedTypes.type_decl_get_inst_norm_field_rtypes ctx def + AssociatedTypes.type_decl_get_inst_norm_field_rtypes meta ctx def av.variant_id generics in let fields_with_types = List.combine av.field_values field_types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "TODO: Error message") + (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Tuple case *) | AAdt av, TAdt (TTuple, generics) -> - cassert (generics.regions = []) meta "TODO: Error message"; - cassert (generics.const_generics = []) meta "TODO: Error message"; - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (generics.regions = []) meta; + sanity_check (generics.const_generics = []) meta; + sanity_check (av.variant_id = None) meta; (* Check that the fields have the proper values - and check that there * are as many fields as field types at the same time *) let fields_with_types = List.combine av.field_values generics.types in List.iter - (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "The fields do not have the proper values or there are not as many fields as field types at the same time TODO: Error message") + (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta) fields_with_types (* Assumed type case *) | AAdt av, TAdt (TAssumed aty_id, generics) -> ( - cassert (av.variant_id = None) meta "TODO: Error message"; + sanity_check (av.variant_id = None) meta; match ( aty_id, av.field_values, @@ -571,27 +571,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = with (* Box *) | TBox, [ boxed_value ], [], [ boxed_ty ], [] -> - cassert (boxed_value.ty = boxed_ty) meta "TODO: Error message" + sanity_check (boxed_value.ty = boxed_ty) meta | _ -> craise meta "Erroneous type") | ABottom, _ -> (* Nothing to check *) () | ABorrow bc, TRef (_, ref_ty, rkind) -> ( match (bc, rkind) with | AMutBorrow (_, av), RMut -> (* Check that the child value has the proper type *) - cassert (av.ty = ref_ty) meta "TODO: Error message" + sanity_check (av.ty = ref_ty) meta | ASharedBorrow bid, RShared -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan meta ek_all bid ctx in match glc with | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) -> - cassert (sv.ty = Substitute.erase_regions ref_ty) meta "TODO: Error message" + sanity_check (sv.ty = Substitute.erase_regions ref_ty) meta | _ -> craise meta "Inconsistent context") - | AIgnoredMutBorrow (_opt_bid, av), RMut -> cassert (av.ty = ref_ty) meta "TODO: Error message" + | AIgnoredMutBorrow (_opt_bid, av), RMut -> sanity_check (av.ty = ref_ty) meta | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ }, RMut ) -> - cassert (given_back.ty = ref_ty) meta "TODO: Error message"; - cassert (child.ty = ref_ty) meta "TODO: Error message" + sanity_check (given_back.ty = ref_ty) meta; + sanity_check (child.ty = ref_ty) meta | AProjSharedBorrow _, RShared -> () | _ -> craise meta "Inconsistent context") | ALoan lc, aty -> ( @@ -599,54 +599,54 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av) -> ( let borrowed_aty = aloan_get_expected_child_type aty in - cassert (child_av.ty = borrowed_aty) meta "TODO: Error message"; + sanity_check (child_av.ty = borrowed_aty) meta; (* Lookup the borrowed value to check it has the proper type *) let glc = lookup_borrow meta ek_all bid ctx in match glc with | Concrete (VMutBorrow (_, bv)) -> - cassert (bv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message" + sanity_check (bv.ty = Substitute.erase_regions borrowed_aty) meta | Abstract (AMutBorrow (_, sv)) -> - cassert ( + sanity_check ( Substitute.erase_regions sv.ty - = Substitute.erase_regions borrowed_aty) meta "TODO: Error message" + = Substitute.erase_regions borrowed_aty) meta | _ -> craise meta "Inconsistent context") | AIgnoredMutLoan (None, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - cassert (child_av.ty = borrowed_aty) meta "TODO: Error message" + sanity_check (child_av.ty = borrowed_aty) meta | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) -> let borrowed_aty = aloan_get_expected_child_type aty in - cassert (sv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message"; + sanity_check (sv.ty = Substitute.erase_regions borrowed_aty) meta; (* TODO: the type of aloans doesn't make sense, see above *) - cassert (child_av.ty = borrowed_aty) meta "TODO: Error message" + sanity_check (child_av.ty = borrowed_aty) meta | AEndedMutLoan { given_back; child; given_back_meta = _ } | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } -> let borrowed_aty = aloan_get_expected_child_type aty in - cassert (given_back.ty = borrowed_aty) meta "TODO: Error message"; - cassert (child.ty = borrowed_aty) meta "TODO: Error message" + sanity_check (given_back.ty = borrowed_aty) meta; + sanity_check (child.ty = borrowed_aty) meta | AIgnoredSharedLoan child_av -> - cassert (child_av.ty = aloan_get_expected_child_type aty) meta "TODO: Error message") + sanity_check (child_av.ty = aloan_get_expected_child_type aty) meta) | ASymbolic aproj, ty -> ( let ty1 = Substitute.erase_regions ty in match aproj with | AProjLoans (sv, _) -> let ty2 = Substitute.erase_regions sv.sv_ty in - cassert (ty1 = ty2) meta "TODO: Error message"; + sanity_check (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - cassert (ty_has_regions_in_set abs.regions sv.sv_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message" + sanity_check (ty_has_regions_in_set abs.regions sv.sv_ty) meta | AProjBorrows (sv, proj_ty) -> let ty2 = Substitute.erase_regions sv.sv_ty in - cassert (ty1 = ty2) meta "TODO: Error message"; + sanity_check (ty1 = ty2) meta; (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to [_] *) let abs = Option.get info in - cassert (ty_has_regions_in_set abs.regions proj_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message" + sanity_check (ty_has_regions_in_set abs.regions proj_ty) meta | AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with - | AProjBorrows (_sv, ty') -> cassert (ty' = ty) meta "TODO: Error message" + | AProjBorrows (_sv, ty') -> sanity_check (ty' = ty) meta | AEndedProjBorrows _ | AIgnoredProjBorrows -> () | _ -> craise meta "Unexpected") given_back_ls @@ -657,7 +657,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = (lazy ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv ^ "\n- value: " - ^ typed_avalue_to_string meta ctx atv + ^ typed_avalue_to_string ~meta:(Some meta) ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); craise meta "Erroneous typing"); (* Continue exploring to inspect the subterms *) @@ -766,15 +766,15 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = *) (* A symbolic value can't be both in the regular environment and inside * projectors of borrows in abstractions *) - cassert (info.env_count = 0 || info.aproj_borrows = []) meta "A symbolic value can't be both in the regular environment and inside projectors of borrows in abstractions"; + sanity_check (info.env_count = 0 || info.aproj_borrows = []) meta; (* A symbolic value containing borrows can't be duplicated (i.e., copied): * it must be expanded first *) if ty_has_borrows ctx.type_ctx.type_infos info.ty then - cassert (info.env_count <= 1) meta "A symbolic value containing borrows can't be duplicated (i.e., copied): it must be expanded first"; + sanity_check (info.env_count <= 1) meta; (* A duplicated symbolic value is necessarily primitively copyable *) - cassert (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta "A duplicated symbolic value should necessarily be primitively copyable"; + sanity_check (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta; - cassert (info.aproj_borrows = [] || info.aproj_loans <> []) meta "TODO: Error message"; + sanity_check (info.aproj_borrows = [] || info.aproj_loans <> []) meta; (* At the same time: * - check that the loans don't intersect * - compute the set of regions for which we project loans @@ -786,7 +786,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = let regions = RegionId.Set.fold (fun rid regions -> - cassert (not (RegionId.Set.mem rid regions)) meta "The loan projectors should contain the region projectors"; + sanity_check (not (RegionId.Set.mem rid regions)) meta; RegionId.Set.add rid regions) regions linfo.regions in @@ -796,8 +796,8 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = (* Check that the union of the loan projectors contains the borrow projections. *) List.iter (fun binfo -> - cassert ( - projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta "The union of the loan projectors should contain the borrow projections") + sanity_check ( + projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta) info.aproj_borrows; () in @@ -806,7 +806,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit = let check_invariants (meta : Meta.meta) (ctx : eval_ctx) : unit = if !Config.sanity_checks then ( - log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string meta ctx)); + log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); check_loans_borrows_relation_invariant meta ctx; check_borrowed_values_invariant meta ctx; check_typing_invariant meta ctx; diff --git a/compiler/Main.ml b/compiler/Main.ml index f860bec8..f8765247 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -113,7 +113,7 @@ let () = Arg.Clear lean_gen_lakefile, " Generate a default lakefile.lean (Lean only)" ); ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC"); - ("-abort-on-error", Arg.Set fail_hard, " Fail hard (fail on first error) in case of error"); + ("-abort-on-error", Arg.Set fail_hard, "Abort on the first encountered error"); ( "-tuple-nested-proj", Arg.Set use_nested_tuple_projectors, " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \ diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 3ea9c777..c10dbf5d 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -215,11 +215,11 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl = inherit [_] map_statement as super method! visit_Loop entered_loop loop = - cassert (not entered_loop) st.meta "TODO: error message"; + cassert (not entered_loop) st.meta "Nested loops are not supported yet"; super#visit_Loop true loop method! visit_Break _ i = - cassert (i = 0) st.meta "TODO: error message"; + cassert (i = 0) st.meta "Breaks to outer loops are not supported yet"; nst.content end in @@ -234,7 +234,7 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl = method! visit_Sequence env st1 st2 = match st1.content with | Loop _ -> - cassert (statement_has_no_loop_break_continue st2) st2.meta "TODO: error message"; + sanity_check (statement_has_no_loop_break_continue st2) st2.meta; (replace_breaks_with st1 st2).content | _ -> super#visit_Sequence env st1 st2 end @@ -393,7 +393,6 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl = let body = filter_visitor#visit_statement () body in (* Check that the filtered variables completely disappeared from the body *) - (* let statement = crate in *) let check_visitor = object inherit [_] iter_statement as super diff --git a/compiler/Print.ml b/compiler/Print.ml index 85e7eaf6..47ae9b79 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -43,12 +43,12 @@ module Values = struct * typed_avalue_to_string. At some point we had done it, because [typed_value] * and [typed_avalue] were instances of the same general type [g_typed_value], * but then we removed this general type because it proved to be a bad idea. *) - let rec typed_value_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_value) : string = + let rec typed_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (v : typed_value) : string = match v.value with | VLiteral cv -> literal_to_string cv | VAdt av -> ( let field_values = - List.map (typed_value_to_string meta env) av.field_values + List.map (typed_value_to_string~meta:meta env) av.field_values in match v.ty with | TAdt (TTuple, _) -> @@ -83,28 +83,28 @@ module Values = struct | TArray, _ -> (* Happens when we aggregate values *) "@Array[" ^ String.concat ", " field_values ^ "]" - | _ -> craise meta ("Inconsistent value: " ^ show_typed_value v) + | _ -> craise_opt_meta meta ("Inconsistent value: " ^ show_typed_value v) ) - | _ -> craise meta "Inconsistent typed value") + | _ -> craise_opt_meta meta "Inconsistent typed value") | VBottom -> "⊥ : " ^ ty_to_string env v.ty - | VBorrow bc -> borrow_content_to_string meta env bc - | VLoan lc -> loan_content_to_string meta env lc + | VBorrow bc -> borrow_content_to_string ~meta:meta env bc + | VLoan lc -> loan_content_to_string ~meta:meta env lc | VSymbolic s -> symbolic_value_to_string env s - and borrow_content_to_string (meta : Meta.meta) (env : fmt_env) (bc : borrow_content) : string = + and borrow_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (bc : borrow_content) : string = match bc with | VSharedBorrow bid -> "shared_borrow@" ^ BorrowId.to_string bid | VMutBorrow (bid, tv) -> "mut_borrow@" ^ BorrowId.to_string bid ^ " (" - ^ typed_value_to_string meta env tv + ^ typed_value_to_string ~meta:meta env tv ^ ")" | VReservedMutBorrow bid -> "reserved_borrow@" ^ BorrowId.to_string bid - and loan_content_to_string (meta : Meta.meta) (env : fmt_env) (lc : loan_content) : string = + and loan_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (lc : loan_content) : string = match lc with | VSharedLoan (loans, v) -> let loans = BorrowId.Set.to_string None loans in - "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string meta env v ^ ")" + "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string ~meta:meta env v ^ ")" | VMutLoan bid -> "ml@" ^ BorrowId.to_string bid let abstract_shared_borrow_to_string (env : fmt_env) @@ -142,11 +142,11 @@ module Values = struct | AEndedProjBorrows _mv -> "_" | AIgnoredProjBorrows -> "_" - let rec typed_avalue_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_avalue) : string = + let rec typed_avalue_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (v : typed_avalue) : string = match v.value with | AAdt av -> ( let field_values = - List.map (typed_avalue_to_string meta env) av.field_values + List.map (typed_avalue_to_string ~meta:meta env) av.field_values in match v.ty with | TAdt (TTuple, _) -> @@ -178,75 +178,75 @@ module Values = struct (* Assumed type *) match (aty, field_values) with | TBox, [ bv ] -> "@Box(" ^ bv ^ ")" - | _ -> craise meta "Inconsistent value") - | _ -> craise meta "Inconsistent typed value") + | _ -> craise_opt_meta meta "Inconsistent value") + | _ -> craise_opt_meta meta "Inconsistent typed value") | ABottom -> "⊥ : " ^ ty_to_string env v.ty - | ABorrow bc -> aborrow_content_to_string meta env bc - | ALoan lc -> aloan_content_to_string meta env lc + | ABorrow bc -> aborrow_content_to_string ~meta:meta env bc + | ALoan lc -> aloan_content_to_string ~meta:meta env lc | ASymbolic s -> aproj_to_string env s | AIgnored -> "_" - and aloan_content_to_string (meta : Meta.meta) (env : fmt_env) (lc : aloan_content) : string = + and aloan_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (lc : aloan_content) : string = match lc with | AMutLoan (bid, av) -> "@mut_loan(" ^ BorrowId.to_string bid ^ ", " - ^ typed_avalue_to_string meta env av + ^ typed_avalue_to_string ~meta:meta env av ^ ")" | ASharedLoan (loans, v, av) -> let loans = BorrowId.Set.to_string None loans in "@shared_loan(" ^ loans ^ ", " - ^ typed_value_to_string meta env v + ^ typed_value_to_string ~meta:meta env v ^ ", " - ^ typed_avalue_to_string meta env av + ^ typed_avalue_to_string ~meta:meta env av ^ ")" | AEndedMutLoan ml -> "@ended_mut_loan{" - ^ typed_avalue_to_string meta env ml.child + ^ typed_avalue_to_string ~meta:meta env ml.child ^ "; " - ^ typed_avalue_to_string meta env ml.given_back + ^ typed_avalue_to_string ~meta:meta env ml.given_back ^ " }" | AEndedSharedLoan (v, av) -> "@ended_shared_loan(" - ^ typed_value_to_string meta env v + ^ typed_value_to_string ~meta:meta env v ^ ", " - ^ typed_avalue_to_string meta env av + ^ typed_avalue_to_string ~meta:meta env av ^ ")" | AIgnoredMutLoan (opt_bid, av) -> "@ignored_mut_loan(" ^ option_to_string BorrowId.to_string opt_bid ^ ", " - ^ typed_avalue_to_string meta env av + ^ typed_avalue_to_string ~meta:meta env av ^ ")" | AEndedIgnoredMutLoan ml -> "@ended_ignored_mut_loan{ " - ^ typed_avalue_to_string meta env ml.child + ^ typed_avalue_to_string ~meta:meta env ml.child ^ "; " - ^ typed_avalue_to_string meta env ml.given_back + ^ typed_avalue_to_string ~meta:meta env ml.given_back ^ "}" | AIgnoredSharedLoan sl -> - "@ignored_shared_loan(" ^ typed_avalue_to_string meta env sl ^ ")" + "@ignored_shared_loan(" ^ typed_avalue_to_string ~meta:meta env sl ^ ")" - and aborrow_content_to_string (meta : Meta.meta) (env : fmt_env) (bc : aborrow_content) : string + and aborrow_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (bc : aborrow_content) : string = match bc with | AMutBorrow (bid, av) -> "mb@" ^ BorrowId.to_string bid ^ " (" - ^ typed_avalue_to_string meta env av + ^ typed_avalue_to_string ~meta:meta env av ^ ")" | ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid | AIgnoredMutBorrow (opt_bid, av) -> "@ignored_mut_borrow(" ^ option_to_string BorrowId.to_string opt_bid ^ ", " - ^ typed_avalue_to_string meta env av + ^ typed_avalue_to_string ~meta:meta env av ^ ")" | AEndedMutBorrow (_mv, child) -> - "@ended_mut_borrow(" ^ typed_avalue_to_string meta env child ^ ")" + "@ended_mut_borrow(" ^ typed_avalue_to_string ~meta:meta env child ^ ")" | AEndedIgnoredMutBorrow { child; given_back; given_back_meta = _ } -> "@ended_ignored_mut_borrow{ " - ^ typed_avalue_to_string meta env child + ^ typed_avalue_to_string ~meta:meta env child ^ "; " - ^ typed_avalue_to_string meta env given_back + ^ typed_avalue_to_string ~meta:meta env given_back ^ ")" | AEndedSharedBorrow -> "@ended_shared_borrow" | AProjSharedBorrow sb -> @@ -276,11 +276,11 @@ module Values = struct ^ ")" | Identity -> "Identity" - let abs_to_string (meta : Meta.meta) (env : fmt_env) (verbose : bool) (indent : string) + let abs_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (verbose : bool) (indent : string) (indent_incr : string) (abs : abs) : string = let indent2 = indent ^ indent_incr in let avs = - List.map (fun av -> indent2 ^ typed_avalue_to_string meta env av) abs.avalues + List.map (fun av -> indent2 ^ typed_avalue_to_string ~meta:meta env av) abs.avalues in let avs = String.concat ",\n" avs in let kind = @@ -323,7 +323,7 @@ module Contexts = struct | BVar b -> var_binder_to_string env b | BDummy bid -> dummy_var_id_to_string bid - let env_elem_to_string (meta : Meta.meta) (env : fmt_env) (verbose : bool) + let env_elem_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (verbose : bool) (with_var_types : bool) (indent : string) (indent_incr : string) (ev : env_elem) : string = match ev with @@ -332,17 +332,17 @@ module Contexts = struct let ty = if with_var_types then " : " ^ ty_to_string env tv.ty else "" in - indent ^ bv ^ ty ^ " -> " ^ typed_value_to_string meta env tv ^ " ;" - | EAbs abs -> abs_to_string meta env verbose indent indent_incr abs - | EFrame -> craise meta "Can't print a Frame element" + indent ^ bv ^ ty ^ " -> " ^ typed_value_to_string ~meta:meta env tv ^ " ;" + | EAbs abs -> abs_to_string ~meta:meta env verbose indent indent_incr abs + | EFrame -> craise_opt_meta meta "Can't print a Frame element" - let opt_env_elem_to_string (meta : Meta.meta) (env : fmt_env) (verbose : bool) + let opt_env_elem_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (verbose : bool) (with_var_types : bool) (indent : string) (indent_incr : string) (ev : env_elem option) : string = match ev with | None -> indent ^ "..." | Some ev -> - env_elem_to_string meta env verbose with_var_types indent indent_incr ev + env_elem_to_string ~meta:meta env verbose with_var_types indent indent_incr ev (** Filters "dummy" bindings from an environment, to gain space and clarity/ See [env_to_string]. *) @@ -379,7 +379,7 @@ module Contexts = struct "..." to gain space and clarity. [with_var_types]: if true, print the type of the variables *) - let env_to_string (meta : Meta.meta) (filter : bool) (fmt_env : fmt_env) (verbose : bool) + let env_to_string ?(meta : Meta.meta option = None) (filter : bool) (fmt_env : fmt_env) (verbose : bool) (with_var_types : bool) (env : env) : string = let env = if filter then filter_env env else List.map (fun ev -> Some ev) env @@ -388,7 +388,7 @@ module Contexts = struct ^ String.concat "\n" (List.map (fun ev -> - opt_env_elem_to_string meta fmt_env verbose with_var_types " " " " ev) + opt_env_elem_to_string ~meta:meta fmt_env verbose with_var_types " " " " ev) env) ^ "\n}" @@ -468,7 +468,7 @@ module Contexts = struct let frames = split_aux [] [] env in frames - let eval_ctx_to_string_gen (meta : Meta.meta) (verbose : bool) (filter : bool) + let eval_ctx_to_string_gen ?(meta : Meta.meta option = None) (verbose : bool) (filter : bool) (with_var_types : bool) (ctx : eval_ctx) : string = let fmt_env = eval_ctx_to_fmt_env ctx in let ended_regions = RegionId.Set.to_string None ctx.ended_regions in @@ -486,24 +486,24 @@ module Contexts = struct | EBinding (BDummy _, _) -> num_dummies := !num_abs + 1 | EBinding (BVar _, _) -> num_bindings := !num_bindings + 1 | EAbs _ -> num_abs := !num_abs + 1 - | _ -> craise meta "Unreachable") + | _ -> craise_opt_meta meta "Unreachable") f; "\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: " ^ string_of_int !num_bindings ^ "\n- dummy bindings: " ^ string_of_int !num_dummies ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n" - ^ env_to_string meta filter fmt_env verbose with_var_types f + ^ env_to_string ~meta:meta filter fmt_env verbose with_var_types f ^ "\n") frames in "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames - let eval_ctx_to_string (meta : Meta.meta) (ctx : eval_ctx) : string = - eval_ctx_to_string_gen meta false true true ctx + let eval_ctx_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) : string = + eval_ctx_to_string_gen ~meta:meta false true true ctx - let eval_ctx_to_string_no_filter (meta : Meta.meta) (ctx : eval_ctx) : string = - eval_ctx_to_string_gen meta false false true ctx + let eval_ctx_to_string_no_filter ?(meta : Meta.meta option = None) (ctx : eval_ctx) : string = + eval_ctx_to_string_gen ~meta:meta false false true ctx end (** Pretty-printing for LLBC ASTs (functions based on an evaluation context) *) @@ -541,22 +541,22 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in trait_instance_id_to_string env x - let borrow_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (bc : borrow_content) : string = + let borrow_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (bc : borrow_content) : string = let env = eval_ctx_to_fmt_env ctx in - borrow_content_to_string meta env bc + borrow_content_to_string ~meta:meta env bc - let loan_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (lc : loan_content) : string = + let loan_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (lc : loan_content) : string = let env = eval_ctx_to_fmt_env ctx in - loan_content_to_string meta env lc + loan_content_to_string ~meta:meta env lc - let aborrow_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (bc : aborrow_content) : string + let aborrow_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (bc : aborrow_content) : string = let env = eval_ctx_to_fmt_env ctx in - aborrow_content_to_string meta env bc + aborrow_content_to_string ~meta:meta env bc - let aloan_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (lc : aloan_content) : string = + let aloan_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (lc : aloan_content) : string = let env = eval_ctx_to_fmt_env ctx in - aloan_content_to_string meta env lc + aloan_content_to_string ~meta:meta env lc let aproj_to_string (ctx : eval_ctx) (p : aproj) : string = let env = eval_ctx_to_fmt_env ctx in @@ -566,13 +566,13 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in symbolic_value_to_string env sv - let typed_value_to_string (meta : Meta.meta) (ctx : eval_ctx) (v : typed_value) : string = + let typed_value_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (v : typed_value) : string = let env = eval_ctx_to_fmt_env ctx in - typed_value_to_string meta env v + typed_value_to_string ~meta:meta env v - let typed_avalue_to_string (meta : Meta.meta) (ctx : eval_ctx) (v : typed_avalue) : string = + let typed_avalue_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (v : typed_avalue) : string = let env = eval_ctx_to_fmt_env ctx in - typed_avalue_to_string meta env v + typed_avalue_to_string ~meta:meta env v let place_to_string (ctx : eval_ctx) (op : place) : string = let env = eval_ctx_to_fmt_env ctx in @@ -613,13 +613,13 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in trait_impl_to_string env " " " " timpl - let env_elem_to_string (meta : Meta.meta) (ctx : eval_ctx) (indent : string) + let env_elem_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (indent : string) (indent_incr : string) (ev : env_elem) : string = let env = eval_ctx_to_fmt_env ctx in - env_elem_to_string meta env false true indent indent_incr ev + env_elem_to_string ~meta:meta env false true indent indent_incr ev - let abs_to_string (meta : Meta.meta) (ctx : eval_ctx) (indent : string) (indent_incr : string) + let abs_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (indent : string) (indent_incr : string) (abs : abs) : string = let env = eval_ctx_to_fmt_env ctx in - abs_to_string meta env false indent indent_incr abs + abs_to_string ~meta:meta env false indent indent_incr abs end diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 3008e1bd..6ef87194 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -351,7 +351,7 @@ let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id) (** TODO: we don't need a general function anymore (it is now only used for patterns) *) -let adt_g_value_to_string (meta : Meta.meta) (env : fmt_env) (value_to_string : 'v -> string) +let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (value_to_string : 'v -> string) (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) : string = let field_values = List.map value_to_string field_values in @@ -386,50 +386,50 @@ let adt_g_value_to_string (meta : Meta.meta) (env : fmt_env) (value_to_string : match aty with | TState | TRawPtr _ -> (* This type is opaque: we can't get there *) - craise meta "Unreachable" + craise_opt_meta meta "Unreachable" | TResult -> let variant_id = Option.get variant_id in if variant_id = result_return_id then match field_values with | [ v ] -> "@Result::Return " ^ v - | _ -> craise meta "Result::Return takes exactly one value" + | _ -> craise_opt_meta meta "Result::Return takes exactly one value" else if variant_id = result_fail_id then match field_values with | [ v ] -> "@Result::Fail " ^ v - | _ -> craise meta "Result::Fail takes exactly one value" + | _ -> craise_opt_meta meta "Result::Fail takes exactly one value" else - craise meta "Unreachable: improper variant id for result type" + craise_opt_meta meta "Unreachable: improper variant id for result type" | TError -> - cassert (field_values = []) meta "TODO: error message"; + cassert_opt_meta (field_values = []) meta "TODO: error message"; let variant_id = Option.get variant_id in if variant_id = error_failure_id then "@Error::Failure" else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel" - else craise meta "Unreachable: improper variant id for error type" + else craise_opt_meta meta "Unreachable: improper variant id for error type" | TFuel -> let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then ( - cassert (field_values = []) meta "TODO: error message"; + cassert_opt_meta (field_values = []) meta "TODO: error message"; "@Fuel::Zero") else if variant_id = fuel_succ_id then match field_values with | [ v ] -> "@Fuel::Succ " ^ v - | _ -> craise meta "@Fuel::Succ takes exactly one value" - else craise meta "Unreachable: improper variant id for fuel type" + | _ -> craise_opt_meta meta "@Fuel::Succ takes exactly one value" + else craise_opt_meta meta "Unreachable: improper variant id for fuel type" | TArray | TSlice | TStr -> - cassert (variant_id = None) meta "TODO: error message"; + cassert_opt_meta (variant_id = None) meta "TODO: error message"; let field_values = List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values in let id = assumed_ty_to_string aty in id ^ " [" ^ String.concat "; " field_values ^ "]") | _ -> - craise + craise_opt_meta meta ("Inconsistently typed value: expected ADT type but found:" ^ "\n- ty: " ^ ty_to_string env false ty ^ "\n- variant_id: " ^ Print.option_to_string VariantId.to_string variant_id) -let rec typed_pattern_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_pattern) : string = +let rec typed_pattern_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (v : typed_pattern) : string = match v.value with | PatConstant cv -> literal_to_string cv | PatVar (v, None) -> var_to_string env v @@ -440,8 +440,8 @@ let rec typed_pattern_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_pa ^ ")" | PatDummy -> "_" | PatAdt av -> - adt_g_value_to_string meta env - (typed_pattern_to_string meta env) + adt_g_value_to_string ~meta:meta env + (typed_pattern_to_string ~meta:meta env) av.variant_id av.field_values v.ty let fun_sig_to_string (env : fmt_env) (sg : fun_sig) : string = @@ -522,7 +522,7 @@ let fun_or_op_id_to_string (env : fmt_env) (fun_id : fun_or_op_id) : string = binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">" (** [inside]: controls the introduction of parentheses *) -let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : bool) (indent : string) +let rec texpression_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) (inside : bool) (indent : string) (indent_incr : string) (e : texpression) : string = match e.e with | Var var_id -> var_id_to_string env var_id @@ -532,22 +532,22 @@ let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : b (* Recursively destruct the app, to have a pair (app, arguments list) *) let app, args = destruct_apps e in (* Convert to string *) - app_to_string metadata env inside indent indent_incr app args + app_to_string ~meta:metadata env inside indent indent_incr app args | Lambda _ -> let xl, e = destruct_lambdas e in - let e = lambda_to_string metadata env indent indent_incr xl e in + let e = lambda_to_string ~meta:metadata env indent indent_incr xl e in if inside then "(" ^ e ^ ")" else e | Qualif _ -> (* Qualifier without arguments *) - app_to_string metadata env inside indent indent_incr e [] + app_to_string ~meta:metadata env inside indent indent_incr e [] | Let (monadic, lv, re, e) -> - let e = let_to_string metadata env indent indent_incr monadic lv re e in + let e = let_to_string ~meta:metadata env indent indent_incr monadic lv re e in if inside then "(" ^ e ^ ")" else e | Switch (scrutinee, body) -> - let e = switch_to_string metadata env indent indent_incr scrutinee body in + let e = switch_to_string ~meta:metadata env indent indent_incr scrutinee body in if inside then "(" ^ e ^ ")" else e | Loop loop -> - let e = loop_to_string metadata env indent indent_incr loop in + let e = loop_to_string ~meta:metadata env indent indent_incr loop in if inside then "(" ^ e ^ ")" else e | StructUpdate supd -> ( let s = @@ -566,7 +566,7 @@ let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : b (fun (fid, fe) -> let field = FieldId.nth field_names fid in let fe = - texpression_to_string metadata env false indent2 indent_incr fe + texpression_to_string ~metadata:metadata env false indent2 indent_incr fe in "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";") supd.updates @@ -577,21 +577,21 @@ let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : b let fields = List.map (fun (_, fe) -> - texpression_to_string metadata env false indent2 indent_incr fe) + texpression_to_string ~metadata:metadata env false indent2 indent_incr fe) supd.updates in "[ " ^ String.concat ", " fields ^ " ]" - | _ -> craise metadata "Unexpected") + | _ -> craise_opt_meta metadata "Unexpected") | Meta (meta, e) -> ( - let meta_s = emeta_to_string metadata env meta in - let e = texpression_to_string metadata env inside indent indent_incr e in + let meta_s = emeta_to_string ~metadata:metadata env meta in + let e = texpression_to_string ~metadata:metadata env inside indent indent_incr e in match meta with | Assignment _ | SymbolicAssignments _ | SymbolicPlaces _ | Tag _ -> let e = meta_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") -and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : string) +and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bool) (indent : string) (indent_incr : string) (app : texpression) (args : texpression list) : string = (* There are two possibilities: either the [app] is an instantiated, @@ -611,13 +611,13 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s (global_decl_id_to_string env global_id, generics) | AdtCons adt_cons_id -> let variant_s = - adt_variant_to_string ~meta:(Some meta) env adt_cons_id.adt_id + adt_variant_to_string ~meta:meta env adt_cons_id.adt_id adt_cons_id.variant_id in (ConstStrings.constructor_prefix ^ variant_s, []) | Proj { adt_id; field_id } -> - let adt_s = adt_variant_to_string ~meta:(Some meta) env adt_id None in - let field_s = adt_field_to_string ~meta:(Some meta) env adt_id field_id in + let adt_s = adt_variant_to_string ~meta:meta env adt_id None in + let field_s = adt_field_to_string ~meta:meta env adt_id field_id in (* Adopting an F*-like syntax *) (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, []) | TraitConst (trait_ref, const_name) -> @@ -627,7 +627,7 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s | _ -> (* "Regular" expression case *) let inside = args <> [] || (args = [] && inside) in - (texpression_to_string meta env inside indent indent_incr app, []) + (texpression_to_string ~metadata:meta env inside indent indent_incr app, []) in (* Convert the arguments. * The arguments are expressions, so indentation might get weird... (though @@ -635,7 +635,7 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s let arg_to_string = let inside = true in let indent1 = indent ^ indent_incr in - texpression_to_string meta env inside indent1 indent_incr + texpression_to_string ~metadata:meta env inside indent1 indent_incr in let args = List.map arg_to_string args in let all_args = List.append generics args in @@ -646,31 +646,31 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s (* Add parentheses *) if all_args <> [] && inside then "(" ^ e ^ ")" else e -and lambda_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string) +and lambda_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string) (xl : typed_pattern list) (e : texpression) : string = - let xl = List.map (typed_pattern_to_string meta env) xl in - let e = texpression_to_string meta env false indent indent_incr e in + let xl = List.map (typed_pattern_to_string ~meta:meta env) xl in + let e = texpression_to_string ~metadata:meta env false indent indent_incr e in "λ " ^ String.concat " " xl ^ ". " ^ e -and let_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string) +and let_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string) (monadic : bool) (lv : typed_pattern) (re : texpression) (e : texpression) : string = let indent1 = indent ^ indent_incr in let inside = false in - let re = texpression_to_string meta env inside indent1 indent_incr re in - let e = texpression_to_string meta env inside indent indent_incr e in - let lv = typed_pattern_to_string meta env lv in + let re = texpression_to_string ~metadata:meta env inside indent1 indent_incr re in + let e = texpression_to_string ~metadata:meta env inside indent indent_incr e in + let lv = typed_pattern_to_string ~meta:meta env lv in if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e -and switch_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string) +and switch_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string) (scrutinee : texpression) (body : switch_body) : string = let indent1 = indent ^ indent_incr in (* Printing can mess up on the scrutinee, because it is an expression - but * in most situations it will be a value or a function call, so it should be * ok*) - let scrut = texpression_to_string meta env true indent1 indent_incr scrutinee in - let e_to_string = texpression_to_string meta env false indent1 indent_incr in + let scrut = texpression_to_string ~metadata:meta env true indent1 indent_incr scrutinee in + let e_to_string = texpression_to_string ~metadata:meta env false indent1 indent_incr in match body with | If (e_true, e_false) -> let e_true = e_to_string e_true in @@ -679,13 +679,13 @@ and switch_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (inden ^ indent ^ "else\n" ^ indent1 ^ e_false | Match branches -> let branch_to_string (b : match_branch) : string = - let pat = typed_pattern_to_string meta env b.pat in + let pat = typed_pattern_to_string ~meta:meta env b.pat in indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ e_to_string b.branch in let branches = List.map branch_to_string branches in "match " ^ scrut ^ " with\n" ^ String.concat "\n" branches -and loop_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string) +and loop_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string) (loop : loop) : string = let indent1 = indent ^ indent_incr in let indent2 = indent1 ^ indent_incr in @@ -696,17 +696,17 @@ and loop_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_ in let output_ty = "output_ty: " ^ ty_to_string env false loop.output_ty in let fun_end = - texpression_to_string meta env false indent2 indent_incr loop.fun_end + texpression_to_string ~metadata:meta env false indent2 indent_incr loop.fun_end in let loop_body = - texpression_to_string meta env false indent2 indent_incr loop.loop_body + texpression_to_string ~metadata:meta env false indent2 indent_incr loop.loop_body in "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ output_ty ^ "\n" ^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1 ^ "}\n" ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n" ^ indent ^ "}" -and emeta_to_string (metadata : Meta.meta) (env : fmt_env) (meta : emeta) : string = +and emeta_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) (meta : emeta) : string = let meta = match meta with | Assignment (lp, rv, rp) -> @@ -716,14 +716,14 @@ and emeta_to_string (metadata : Meta.meta) (env : fmt_env) (meta : emeta) : stri | Some rp -> " [@src=" ^ mplace_to_string env rp ^ "]" in "@assign(" ^ mplace_to_string env lp ^ " := " - ^ texpression_to_string metadata env false "" "" rv + ^ texpression_to_string ~metadata:metadata env false "" "" rv ^ rp ^ ")" | SymbolicAssignments info -> let infos = List.map (fun (var_id, rv) -> VarId.to_string var_id ^ " == " - ^ texpression_to_string metadata env false "" "" rv) + ^ texpression_to_string ~metadata:metadata env false "" "" rv) info in let infos = String.concat ", " infos in @@ -756,5 +756,5 @@ let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string = if inputs = [] then indent else " fun " ^ String.concat " " inputs ^ " ->\n" ^ indent in - let body = texpression_to_string def.meta env inside indent indent body.body in + let body = texpression_to_string ~metadata:(Some def.meta) env inside indent indent body.body in "let " ^ name ^ " :\n " ^ signature ^ " =\n" ^ inputs ^ body diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index d7423441..1df7176d 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -222,7 +222,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* Register a variable for constraints propagation - used when an variable is * introduced (left-hand side of a left binding) *) let register_var (ctx : pn_ctx) (v : var) : pn_ctx = - cassert (not (VarId.Map.mem v.id ctx.pure_vars)) def.meta "TODO: error message"; + sanity_check (not (VarId.Map.mem v.id ctx.pure_vars)) def.meta; match v.basename with | None -> ctx | Some name -> @@ -1204,7 +1204,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = let num_fields = List.length fields in (* In order to simplify, there must be as many arguments as * there are fields *) - cassert (num_fields > 0) def.meta "The number of fields is not > 0"; + sanity_check (num_fields > 0) def.meta; if num_fields = List.length args then (* We now need to check that all the arguments are of the form: * [x.field] for some variable [x], and where the projection @@ -1572,7 +1572,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl = let arg, args = Collections.List.pop args in mk_apps def.meta arg args | BoxFree -> - cassert (args = []) def.meta "TODO: error message"; + sanity_check (args = []) def.meta; mk_unit_rvalue | SliceIndexShared | SliceIndexMut | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut @@ -1767,7 +1767,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl = (* TODO: this information should be computed in SymbolicToPure and * store in an enum ("monadic" should be an enum, not a bool). *) let re_ty = Option.get (opt_destruct_result def.meta re.ty) in - cassert (lv.ty = re_ty) def.meta "TODO: error message"; + sanity_check (lv.ty = re_ty) def.meta; let err_vid = fresh_id () in let err_var : var = { @@ -1981,7 +1981,6 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) : (List.concat (List.map (fun { f; loops } -> [ f :: loops ]) transl)) in let subgroups = ReorderDecls.group_reorder_fun_decls all_decls in -(* TODO meta or not meta ? *) log#ldebug (lazy ("filter_loop_inputs: all_decls:\n\n" @@ -2021,7 +2020,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) : ^ String.concat ", " (List.map (var_to_string ctx) inputs_prefix) ^ "\n")); let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in - cassert (Option.is_some decl.loop_id) decl.meta "TODO: error message"; + sanity_check (Option.is_some decl.loop_id) decl.meta; let fun_id = (E.FRegular decl.def_id, decl.loop_id) in @@ -2173,7 +2172,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) : in let fwd_info = { fwd_info; effect_info; ignore_output } in - cassert (fun_sig_info_is_wf fwd_info) decl.meta "TODO: error message"; + sanity_check (fun_sig_info_is_wf fwd_info) decl.meta; let signature = { generics; diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index 6bc11a7c..d2fa57ae 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -15,9 +15,9 @@ let get_adt_field_types (meta : Meta.meta) (type_decls : type_decl TypeDeclId.Ma match type_id with | TTuple -> (* Tuple *) - cassert (generics.const_generics = []) meta "TODO: error message"; - cassert (generics.trait_refs = []) meta "TODO: error message"; - cassert (variant_id = None) meta "TODO: error message"; + sanity_check (generics.const_generics = []) meta; + sanity_check (generics.trait_refs = []) meta; + sanity_check (variant_id = None) meta; generics.types | TAdtId def_id -> (* "Regular" ADT *) @@ -37,10 +37,10 @@ let get_adt_field_types (meta : Meta.meta) (type_decls : type_decl TypeDeclId.Ma else craise meta "Unreachable: improper variant id for result type" | TError -> - cassert (generics = empty_generic_args) meta "TODO: error message"; + sanity_check (generics = empty_generic_args) meta; let variant_id = Option.get variant_id in - cassert ( - variant_id = error_failure_id || variant_id = error_out_of_fuel_id) meta "TODO: error message"; + sanity_check ( + variant_id = error_failure_id || variant_id = error_out_of_fuel_id) meta; [] | TFuel -> let variant_id = Option.get variant_id in @@ -64,7 +64,7 @@ type tc_ctx = { let check_literal (meta : Meta.meta) (v : literal) (ty : literal_type) : unit = match (ty, v) with - | TInteger int_ty, VScalar sv -> cassert (int_ty = sv.int_ty) meta "TODO: error message" + | TInteger int_ty, VScalar sv -> sanity_check (int_ty = sv.int_ty) meta | TBool, VBool _ | TChar, VChar _ -> () | _ -> craise meta "Inconsistent type" @@ -76,7 +76,7 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx) (v : typed_pattern ctx | PatDummy -> ctx | PatVar (var, _) -> - cassert (var.ty = v.ty) meta "TODO: error message"; + sanity_check (var.ty = v.ty) meta; let env = VarId.Map.add var.id var.ty ctx.env in { ctx with env } | PatAdt av -> @@ -110,21 +110,21 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : * we use a locally nameless representation *) match VarId.Map.find_opt var_id ctx.env with | None -> () - | Some ty -> cassert (ty = e.ty) meta "TODO: error message") + | Some ty -> sanity_check (ty = e.ty) meta) | CVar cg_id -> let ty = T.ConstGenericVarId.Map.find cg_id ctx.const_generics in - cassert (ty = e.ty) meta "TODO: error message" + sanity_check (ty = e.ty) meta | Const cv -> check_literal meta cv (ty_as_literal meta e.ty) | App (app, arg) -> let input_ty, output_ty = destruct_arrow meta app.ty in - cassert (input_ty = arg.ty) meta "TODO: error message"; - cassert (output_ty = e.ty) meta "TODO: error message"; + sanity_check (input_ty = arg.ty) meta; + sanity_check (output_ty = e.ty) meta; check_texpression meta ctx app; check_texpression meta ctx arg | Lambda (pat, body) -> let pat_ty, body_ty = destruct_arrow meta e.ty in - cassert (pat.ty = pat_ty) meta "TODO: error message"; - cassert (body.ty = body_ty) meta "TODO: error message"; + sanity_check (pat.ty = pat_ty) meta; + sanity_check (body.ty = body_ty) meta; (* Check the pattern and register the introduced variables at the same time *) let ctx = check_typed_pattern meta ctx pat in check_texpression meta ctx body @@ -139,8 +139,8 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : let adt_ty, field_ty = destruct_arrow meta e.ty in let adt_id, adt_generics = ty_as_adt meta adt_ty in (* Check the ADT type *) - cassert (adt_id = proj_adt_id) meta "TODO: error message"; - cassert (adt_generics = qualif.generics) meta "TODO: error message"; + sanity_check (adt_id = proj_adt_id) meta; + sanity_check (adt_generics = qualif.generics) meta; (* Retrieve and check the expected field type *) let variant_id = None in let expected_field_tys = @@ -148,23 +148,23 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : qualif.generics in let expected_field_ty = FieldId.nth expected_field_tys field_id in - cassert (expected_field_ty = field_ty) meta "TODO: error message" + sanity_check (expected_field_ty = field_ty) meta | AdtCons id -> ( let expected_field_tys = get_adt_field_types meta ctx.type_decls id.adt_id id.variant_id qualif.generics in let field_tys, adt_ty = destruct_arrows e.ty in - cassert (expected_field_tys = field_tys) meta "TODO: error message"; + sanity_check (expected_field_tys = field_tys) meta; match adt_ty with | TAdt (type_id, generics) -> - cassert (type_id = id.adt_id) meta "TODO: error message"; - cassert (generics = qualif.generics) meta "TODO: error message" + sanity_check (type_id = id.adt_id) meta; + sanity_check (generics = qualif.generics) meta | _ -> craise meta "Unreachable")) | Let (monadic, pat, re, e_next) -> let expected_pat_ty = if monadic then destruct_result meta re.ty else re.ty in - cassert (pat.ty = expected_pat_ty) meta "TODO: error message"; - cassert (e.ty = e_next.ty) meta "TODO: error message"; + sanity_check (pat.ty = expected_pat_ty) meta; + sanity_check (e.ty = e_next.ty) meta; (* Check the right-expression *) check_texpression meta ctx re; (* Check the pattern and register the introduced variables at the same time *) @@ -175,20 +175,20 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : check_texpression meta ctx scrut; match switch_body with | If (e_then, e_else) -> - cassert (scrut.ty = TLiteral TBool) meta "TODO: error message"; - cassert (e_then.ty = e.ty) meta "TODO: error message"; - cassert (e_else.ty = e.ty) meta "TODO: error message"; + sanity_check (scrut.ty = TLiteral TBool) meta; + sanity_check (e_then.ty = e.ty) meta; + sanity_check (e_else.ty = e.ty) meta; check_texpression meta ctx e_then; check_texpression meta ctx e_else | Match branches -> let check_branch (br : match_branch) : unit = - cassert (br.pat.ty = scrut.ty) meta "TODO: error message"; + sanity_check (br.pat.ty = scrut.ty) meta; let ctx = check_typed_pattern meta ctx br.pat in check_texpression meta ctx br.branch in List.iter check_branch branches) | Loop loop -> - cassert (loop.fun_end.ty = e.ty) meta "TODO: error message"; + sanity_check (loop.fun_end.ty = e.ty) meta; check_texpression meta ctx loop.fun_end; check_texpression meta ctx loop.loop_body | StructUpdate supd -> ( @@ -196,11 +196,11 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : (if Option.is_some supd.init then match VarId.Map.find_opt (Option.get supd.init) ctx.env with | None -> () - | Some ty -> cassert (ty = e.ty) meta "TODO: error message"); + | Some ty -> sanity_check (ty = e.ty) meta); (* Check the fields *) (* Retrieve and check the expected field type *) let adt_id, adt_generics = ty_as_adt meta e.ty in - cassert (adt_id = supd.struct_id) meta "TODO: error message"; + sanity_check (adt_id = supd.struct_id) meta; (* The id can only be: a custom type decl or an array *) match adt_id with | TAdtId _ -> @@ -211,7 +211,7 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : List.iter (fun ((fid, fe) : _ * texpression) -> let expected_field_ty = FieldId.nth expected_field_tys fid in - cassert (expected_field_ty = fe.ty) meta "TODO: error message"; + sanity_check (expected_field_ty = fe.ty) meta; check_texpression meta ctx fe) supd.updates | TAssumed TArray -> @@ -220,10 +220,10 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : in List.iter (fun ((_, fe) : _ * texpression) -> - cassert (expected_field_ty = fe.ty) meta "TODO: error message"; + sanity_check (expected_field_ty = fe.ty) meta; check_texpression meta ctx fe) supd.updates | _ -> craise meta "Unexpected") | Meta (_, e_next) -> - cassert (e_next.ty = e.ty) meta "TODO: error message"; + sanity_check (e_next.ty = e.ty) meta; check_texpression meta ctx e_next diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 0f9c2dfe..cce70382 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -78,7 +78,7 @@ let fun_sig_info_is_wf (info : fun_sig_info) : bool = let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty = match ty with | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty) - | _ -> craise meta "Unreachable" + | _ -> craise meta "Not an arrow type" let compute_literal_type (cv : literal) : literal_type = match cv with @@ -237,7 +237,7 @@ let is_var (e : texpression) : bool = match e.e with Var _ -> true | _ -> false let as_var (meta : Meta.meta) (e : texpression) : VarId.id = - match e.e with Var v -> v | _ -> craise meta "Unreachable" + match e.e with Var v -> v | _ -> craise meta "Not a var" let is_cvar (e : texpression) : bool = match e.e with CVar _ -> true | _ -> false @@ -251,7 +251,7 @@ let is_const (e : texpression) : bool = let ty_as_adt (meta : Meta.meta) (ty : ty) : type_id * generic_args = match ty with | TAdt (id, generics) -> (id, generics) - | _ -> craise meta "Unreachable" + | _ -> craise meta "Not an ADT" (** Remove the external occurrences of {!Meta} *) let rec unmeta (e : texpression) : texpression = @@ -294,7 +294,7 @@ let destruct_lets_no_interleave (meta : Meta.meta) (e : texpression) : let m = match e.e with | Let (monadic, _, _, _) -> monadic - | _ -> craise meta "Unreachable" + | _ -> craise meta "Not a let-binding" in (* Destruct the rest *) let rec destruct_lets (e : texpression) : @@ -323,12 +323,11 @@ let destruct_apps (e : texpression) : texpression * texpression list = (** Make an [App (app, arg)] expression *) let mk_app (meta : Meta.meta) (app : texpression) (arg : texpression) : texpression = let raise_or_return msg = - if !Config.fail_hard then craise meta msg - else - let e = App (app, arg) in - (* Dummy type - TODO: introduce an error type *) - let ty = app.ty in - { e; ty } + save_error (Some meta) msg; + let e = App (app, arg) in + (* Dummy type - TODO: introduce an error type *) + let ty = app.ty in + { e; ty } in match app.ty with | TArrow (ty0, ty1) -> @@ -371,8 +370,8 @@ let opt_destruct_function_call (e : texpression) : let opt_destruct_result (meta : Meta.meta) (ty : ty) : ty option = match ty with | TAdt (TAssumed TResult, generics) -> - cassert (generics.const_generics = []) meta "TODO: Error message"; - cassert (generics.trait_refs = []) meta "TODO: Error message"; + sanity_check (generics.const_generics = []) meta; + sanity_check (generics.trait_refs = []) meta; Some (Collections.List.to_cons_nil generics.types) | _ -> None @@ -381,8 +380,8 @@ let destruct_result (meta : Meta.meta) (ty : ty) : ty = Option.get (opt_destruct let opt_destruct_tuple (meta : Meta.meta) (ty : ty) : ty list option = match ty with | TAdt (TTuple, generics) -> - cassert (generics.const_generics = []) meta "TODO: Error message"; - cassert (generics.trait_refs = []) meta "TODO: Error message"; + sanity_check (generics.const_generics = []) meta; + sanity_check (generics.trait_refs = []) meta; Some generics.types | _ -> None diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index f4e2ff35..a4d66854 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -44,7 +44,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty (fun_decls : fun_decl FunDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) - (trait_impls : trait_impl TraitImplId.Map.t) (* ?meta *) (fun_name : string) + (trait_impls : trait_impl TraitImplId.Map.t) (fun_name : string) (sg : fun_sig) : region_var_groups = log#ldebug (lazy (__FUNCTION__ ^ ": " ^ fun_name)); (* Initialize a normalization context (we may need to normalize some @@ -174,13 +174,13 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) - cassert_opt_meta ( - AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta "The trait should reference a clause, and not an implementation (otherwise it should have been normalized)"; + sanity_check_opt_meta ( + AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta; (* We have nothing to do *) () | TArrow (regions, inputs, output) -> (* TODO: *) - cassert_opt_meta (regions = []) meta "Regions should be empty"; + cassert_opt_meta (regions = []) meta "We don't support arrow types with locally quantified regions"; (* We can ignore the outer regions *) List.iter (explore_ty []) (output :: inputs) and explore_generics (outer : region list) (generics : generic_args) = @@ -223,7 +223,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty (SccId.Map.bindings sccs.sccs) in (* The SCC should only contain the 'static *) - cassert_opt_meta (static_scc = [ RStatic ]) meta "The SCC should only contain the 'static"; + sanity_check_opt_meta (static_scc = [ RStatic ]) meta; (* Remove the group as well as references to this group from the other SCCs *) let { sccs; scc_deps } = sccs in diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index a35fdbf3..14cda863 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -80,9 +80,9 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) (ctx : eval_ct | TAssumed aty -> ( match aty with | TBox -> - cassert (generics.regions = []) meta "Regions should be empty TODO: error message"; - cassert (List.length generics.types = 1) meta "Too many types TODO: error message"; - cassert (generics.const_generics = []) meta "const_generics should be empty TODO: error message"; + sanity_check (generics.regions = []) meta; + sanity_check (List.length generics.types = 1) meta; + sanity_check (generics.const_generics = []) meta; generics.types | TArray | TSlice | TStr -> (* Those types don't have fields *) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 46058a9a..e60d6870 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -325,7 +325,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string = let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string = let env = bs_ctx_to_fmt_env ctx in - Print.Values.typed_value_to_string ctx.fun_decl.meta env v + Print.Values.typed_value_to_string ~meta:(Some ctx.fun_decl.meta) env v let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string = let env = bs_ctx_to_pure_fmt_env ctx in @@ -349,7 +349,7 @@ let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = let texpression_to_string (ctx : bs_ctx) (e : texpression) : string = let env = bs_ctx_to_pure_fmt_env ctx in - PrintPure.texpression_to_string ctx.fun_decl.meta env false "" " " e + PrintPure.texpression_to_string ~metadata:(Some ctx.fun_decl.meta) env false "" " " e let fun_id_to_string (ctx : bs_ctx) (id : A.fun_id) : string = let env = bs_ctx_to_fmt_env ctx in @@ -363,9 +363,9 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.fun_decl_to_string env def -let typed_pattern_to_string (meta : Meta.meta) (ctx : bs_ctx) (p : Pure.typed_pattern) : string = +let typed_pattern_to_string ?(meta : Meta.meta option = None) (ctx : bs_ctx) (p : Pure.typed_pattern) : string = let env = bs_ctx_to_pure_fmt_env ctx in - PrintPure.typed_pattern_to_string meta env p + PrintPure.typed_pattern_to_string ~meta:meta env p let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) : fun_effect_info = @@ -384,7 +384,7 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let verbose = false in let indent = "" in let indent_incr = " " in - Print.Values.abs_to_string ctx.fun_decl.meta env verbose indent indent_incr abs + Print.Values.abs_to_string ~meta:(Some ctx.fun_decl.meta) env verbose indent indent_incr abs let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = @@ -478,7 +478,7 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty = | TTraitType (trait_ref, type_name) -> let trait_ref = translate_strait_ref meta trait_ref in TTraitType (trait_ref, type_name) - | TArrow _ -> craise meta "TODO" + | TArrow _ -> craise meta "TODO: error message" and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) : generic_args = translate_generic_args meta (translate_sty meta) generics @@ -555,7 +555,7 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : let name = Print.Types.name_to_string env def.name in let { T.regions; types; const_generics; trait_clauses } = def.generics in (* Can't translate types with regions for now *) - cassert (regions = []) def.meta "Translating types with regions is not supported yet"; + cassert (regions = []) def.meta "ADTs containing borrows are not supported yet"; let trait_clauses = List.map (translate_trait_clause def.meta) trait_clauses in let generics = { types; const_generics; trait_clauses } in let kind = translate_type_decl_kind def.meta def.T.kind in @@ -620,7 +620,7 @@ let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) (ty : T.ty not (List.exists (TypesUtils.ty_has_borrows type_infos) - generics.types)) meta "General parametricity is not supported yet"; + generics.types)) meta "ADTs containing borrows are not supported yet"; match t_generics.types with | [ bty ] -> bty | _ -> @@ -640,7 +640,7 @@ let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) (ty : T.ty | TTraitType (trait_ref, type_name) -> let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in TTraitType (trait_ref, type_name) - | TArrow _ -> craise meta "TODO" + | TArrow _ -> craise meta "TODO: error message" and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos) (generics : T.generic_args) : generic_args = @@ -701,7 +701,7 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos) else None | TAssumed TBox -> ( (* Don't accept ADTs (which are not tuples) with borrows for now *) - cassert (not (TypesUtils.ty_has_borrows type_infos ty)) meta "ADTs with borrows are not supported yet"; + cassert (not (TypesUtils.ty_has_borrows type_infos ty)) meta "ADTs containing borrows are not supported yet"; (* Eliminate the box *) match generics.types with | [ bty ] -> translate bty @@ -744,7 +744,7 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos) let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in Some (TTraitType (trait_ref, type_name)) else None - | TArrow _ -> craise meta "TODO" + | TArrow _ -> craise meta "TODO: error message" (** Simply calls [translate_back_ty] *) let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) @@ -794,7 +794,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) (back_funs : texpression option RegionGroupId.Map.t option) (ctx : bs_ctx) : bs_ctx = let calls = ctx.calls in - cassert (not (V.FunCallId.Map.mem call_id calls)) ctx.fun_decl.meta "TODO: error message"; + sanity_check (not (V.FunCallId.Map.mem call_id calls)) ctx.fun_decl.meta; let info = { forward; forward_inputs = args; back_funs } in let calls = V.FunCallId.Map.add call_id info calls in { ctx with calls } @@ -816,7 +816,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id) let calls = V.FunCallId.Map.add call_id info ctx.calls in (* Insert the abstraction in the abstractions map *) let abstractions = ctx.abstractions in - cassert (not (V.AbstractionId.Map.mem abs.abs_id abstractions)) ctx.fun_decl.meta "This abstraction should not be in the abstractions map"; + sanity_check (not (V.AbstractionId.Map.mem abs.abs_id abstractions)) ctx.fun_decl.meta; let abstractions = V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions in @@ -896,7 +896,7 @@ let compute_raw_fun_effect_info (meta : Meta.meta) (fun_infos : fun_info A.FunD is_rec = info.is_rec || Option.is_some lid; } | FunId (FAssumed aid) -> - cassert (lid = None) meta "TODO: error message"; + sanity_check (lid = None) meta; { can_fail = Assumed.assumed_fun_can_fail aid; stateful_group = false; @@ -926,7 +926,7 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref) (* This is necessarily for the current function *) match fun_id with | FunId (FRegular fid) -> ( - cassert (fid = ctx.fun_decl.def_id) ctx.fun_decl.meta "TODO: error message"; + sanity_check (fid = ctx.fun_decl.def_id) ctx.fun_decl.meta; (* Lookup the loop *) let lid = V.LoopId.Map.find lid ctx.loop_ids_map in let loop_info = LoopId.Map.find lid ctx.loops in @@ -1188,7 +1188,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta) else false in let info = { fwd_info; effect_info = fwd_effect_info; ignore_output } in - cassert (fun_sig_info_is_wf info) meta "TODO: error message"; + sanity_check (fun_sig_info_is_wf info) meta; info in @@ -1541,7 +1541,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (* Eliminate the tuple wrapper if it is a tuple with exactly one field *) match v.ty with | TAdt (TTuple, _) -> - cassert (variant_id = None) ctx.fun_decl.meta "TODO: error message"; + sanity_check (variant_id = None) ctx.fun_decl.meta; mk_simpl_tuple_texpression ctx.fun_decl.meta field_values | _ -> (* Retrieve the type and the translated generics from the translated @@ -1619,7 +1619,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) -> - cassert (field_values = []) ctx.fun_decl.meta "Only tuples can currently contain borrows"; + cassert (field_values = []) ctx.fun_decl.meta "ADTs containing borrows are not supported yet"; None | TTuple -> (* Return *) @@ -1687,7 +1687,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option = (* The symbolic value was left unchanged *) Some (symbolic_value_to_texpression ctx msv) | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) -> - cassert (child_aproj = AIgnoredProjBorrows) ctx.fun_decl.meta "TODO: error message"; + sanity_check (child_aproj = AIgnoredProjBorrows) ctx.fun_decl.meta; (* The symbolic value was updated *) Some (symbolic_value_to_texpression ctx mnv) | V.AEndedProjLoans (_, _) -> @@ -1762,12 +1762,12 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) let adt_id, _ = TypesUtils.ty_as_adt av.ty in match adt_id with | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) -> - cassert (field_values = []) ctx.fun_decl.meta "Only tuples can currently contain borrows"; + cassert (field_values = []) ctx.fun_decl.meta "ADTs with borrows are not supported yet"; (ctx, None) | TTuple -> (* Return *) let variant_id = adt_v.variant_id in - cassert (variant_id = None) ctx.fun_decl.meta "TODO: error message"; + sanity_check (variant_id = None) ctx.fun_decl.meta; if field_values = [] then (ctx, None) else (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern] @@ -2042,9 +2042,9 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option) and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) (ctx : bs_ctx) : texpression = - cassert (is_continue = ctx.inside_loop) ctx.fun_decl.meta "TODO: error message"; + sanity_check (is_continue = ctx.inside_loop) ctx.fun_decl.meta; let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in - cassert (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta "TODO: error message"; + sanity_check (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta; (* Lookup the loop information *) let loop_id = Option.get ctx.loop_id in @@ -2313,7 +2313,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : (match binop with (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *) | E.Shl | E.Shr -> () - | _ -> cassert (int_ty0 = int_ty1) ctx.fun_decl.meta "TODO: error message"); + | _ -> sanity_check (int_ty0 = int_ty1) ctx.fun_decl.meta); let effect_info = { can_fail = ExpressionsUtils.binop_can_fail binop; @@ -2368,7 +2368,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) ^ T.RegionGroupId.to_string rg_id ^ "\n- loop_id: " ^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id - ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ctx.fun_decl.meta ectx ^ "\n- abs:\n" + ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ~meta:(Some ctx.fun_decl.meta) ectx ^ "\n- abs:\n" ^ abs_to_string ctx abs ^ "\n")); (* When we end an input abstraction, this input abstraction gets back @@ -2382,7 +2382,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) for a parent backward function. *) let bid = Option.get ctx.bid in - cassert (rg_id = bid) ctx.fun_decl.meta "TODO: error message"; + sanity_check (rg_id = bid) ctx.fun_decl.meta; (* First, introduce the given back variables. @@ -2523,8 +2523,8 @@ and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) (* We can do this simply by checking that it consumes and gives back nothing *) let inputs = abs_to_consumed ctx ectx abs in let ctx, outputs = abs_to_given_back None abs ctx in - cassert (inputs = []) ctx.fun_decl.meta "TODO: error message"; - cassert (outputs = []) ctx.fun_decl.meta "TODO: error message"; + sanity_check (inputs = []) ctx.fun_decl.meta; + sanity_check (outputs = []) ctx.fun_decl.meta; (* Translate the next expression *) translate_expression e ctx @@ -2566,7 +2566,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) (* Retrieve the values consumed upon ending the loans inside this * abstraction: as there are no nested borrows, there should be none. *) let consumed = abs_to_consumed ctx ectx abs in - cassert (consumed = []) ctx.fun_decl.meta "Nested borrows are not supported yet TODO: error message"; + cassert (consumed = []) ctx.fun_decl.meta "Nested borrows are not supported yet"; (* Retrieve the values given back upon ending this abstraction - note that * we don't provide meta-place information, because those assignments will * be inlined anyway... *) @@ -2601,7 +2601,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) texpression = let vloop_id = loop_id in let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in - cassert (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta "TODO: error message"; + sanity_check (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta; let rg_id = Option.get rg_id in (* There are two cases depending on the [abs_kind] (whether this is a synth input or a regular loop call) *) @@ -2819,7 +2819,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) ^ pure_ty_to_string ctx true_e.ty ^ "\n\nfalse_e.ty: " ^ pure_ty_to_string ctx false_e.ty)); - if !Config.fail_hard then cassert (ty = false_e.ty) ctx.fun_decl.meta "TODO: error message"; (* TODO: remove if ? *) + save_error ~b:(ty = false_e.ty) (Some ctx.fun_decl.meta) "Internal error, please file an issue"; { e; ty } | ExpandInt (int_ty, branches, otherwise) -> let translate_branch ((v, branch_e) : V.scalar_value * S.expression) : @@ -2844,8 +2844,8 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) Match all_branches ) in let ty = otherwise.branch.ty in - cassert ( - List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches) ctx.fun_decl.meta "TODO: error message"; + sanity_check ( + List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches) ctx.fun_decl.meta; { e; ty } (* Translate and [ExpandAdt] when there is no branching (i.e., one branch). @@ -3480,7 +3480,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* Add the loop information in the context *) let ctx = - cassert (not (LoopId.Map.mem loop_id ctx.loops)) ctx.fun_decl.meta "The loop information should not already be in the context TODO: error message"; + sanity_check (not (LoopId.Map.mem loop_id ctx.loops)) ctx.fun_decl.meta; (* Note that we will retrieve the input values later in the [ForwardEnd] (and will introduce the outputs at that moment, together with the actual diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 787bfb4f..bdd27d0f 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -47,7 +47,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac let get_scalar (see : symbolic_expansion option) : scalar_value = match see with | Some (SeLiteral (VScalar cv)) -> - cassert (cv.int_ty = int_ty) meta "For all the regular branches, the symbolic value should have been expanded to a constant TODO: Error message"; + sanity_check (cv.int_ty = int_ty) meta; cv | _ -> craise meta "Unreachable" in @@ -57,7 +57,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac (* For the otherwise branch, the symbolic value should have been left * unchanged *) let otherwise_see, otherwise = otherwise in - cassert (otherwise_see = None) meta "For the otherwise branch, the symbolic value should have been left unchanged"; + sanity_check (otherwise_see = None) meta; (* Return *) ExpandInt (int_ty, branches, otherwise) | TAdt (_, _) -> diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 11b179db..f97d7ab1 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -354,7 +354,7 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) *) let export_types_group (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit = - assert (ids <> []) (* meta "TODO: Error message" *); + assert (ids <> []); let export_type = export_type fmt config ctx in let ids_set = Pure.TypeDeclId.Set.of_list ids in let export_type_decl kind id = export_type ids_set kind id true false in @@ -396,11 +396,11 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) if List.exists (fun b -> b) builtin then (* Sanity check *) - assert (List.for_all (fun b -> b) builtin) (* meta "TODO: Error message" *) + assert (List.for_all (fun b -> b) builtin) else if List.exists dont_extract defs then (* Check if we have to ignore declarations *) (* Sanity check *) - assert (List.for_all dont_extract defs) (* meta "TODO: Error message" *) + assert (List.for_all dont_extract defs) else ( (* Extract the type declarations. @@ -447,8 +447,8 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = GlobalDeclId.Map.find id global_decls in let trans = FunDeclId.Map.find global.body ctx.trans_funs in - cassert (trans.fwd.loops = []) global.meta "TODO: Error message"; - cassert (trans.backs = []) global.meta "TODO: Error message"; + sanity_check (trans.fwd.loops = []) global.meta; + sanity_check (trans.backs = []) global.meta; let body = trans.fwd.f in let is_opaque = Option.is_none body.Pure.body in @@ -915,7 +915,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Initialize the names map by registering the keywords used in the language, as well as some primitive names ("u32", etc.). We insert the names of the local declarations later. *) - let names_maps = Extract.initialize_names_maps () in (*TODO*) + let names_maps = Extract.initialize_names_maps () in (* We need to compute which functions are recursive, in order to know * whether we should generate a decrease clause or not. *) @@ -1038,7 +1038,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : match Filename.chop_suffix_opt ~suffix:".llbc" filename with | None -> (* Note that we already checked the suffix upon opening the file *) - raise (Failure "Unreachable") (* TODO check *) + raise (Failure "Unreachable") | Some filename -> (* Retrieve the file basename *) let basename = Filename.basename filename in diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml index 51c9e8cc..9c4b8b45 100644 --- a/compiler/ValuesUtils.ml +++ b/compiler/ValuesUtils.ml @@ -12,23 +12,23 @@ let mk_unit_value : typed_value = { value = VAdt { variant_id = None; field_values = [] }; ty = mk_unit_ty } let mk_typed_value (meta : Meta.meta) (ty : ty) (value : value) : typed_value = - cassert (ty_is_ety ty) meta "TODO: error message"; + sanity_check (ty_is_ety ty) meta; { value; ty } let mk_typed_avalue (meta : Meta.meta) (ty : ty) (value : avalue) : typed_avalue = - cassert (ty_is_rty ty) meta "TODO: error message"; + sanity_check (ty_is_rty ty) meta; { value; ty } let mk_bottom (meta : Meta.meta) (ty : ty) : typed_value = - cassert (ty_is_ety ty) meta "TODO: error message"; + sanity_check (ty_is_ety ty) meta; { value = VBottom; ty } let mk_abottom (meta : Meta.meta) (ty : ty) : typed_avalue = - cassert (ty_is_rty ty) meta "TODO: error message"; + sanity_check (ty_is_rty ty) meta; { value = ABottom; ty } let mk_aignored (meta : Meta.meta) (ty : ty) : typed_avalue = - cassert (ty_is_rty ty) meta "TODO: error message"; + sanity_check (ty_is_rty ty) meta; { value = AIgnored; ty } let value_as_symbolic (meta : Meta.meta) (v : value) : symbolic_value = |