From 0b463547ddc409c885859a8bdb577746d87260a2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 May 2024 08:04:30 +0200 Subject: Print the name patterns of the definitions which fail to extract --- compiler/Translate.ml | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 72a98c3d..0f6aa7c1 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -206,9 +206,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef) with CFailure (meta, _) -> let name = name_to_string trans_ctx fdef.name in + let name_pattern = name_to_pattern_string trans_ctx fdef.name in save_error __FILE__ __LINE__ meta ("Could not translate the function '" ^ name - ^ "' because of previous error"); + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None (* TODO: factor out the return type *) @@ -245,9 +246,11 @@ let translate_crate_to_pure (crate : crate) : trans_ctx fdef ) with CFailure (meta, _) -> let name = name_to_string trans_ctx fdef.name in + let name_pattern = name_to_pattern_string trans_ctx fdef.name in save_error __FILE__ __LINE__ meta ("Could not translate the function signature of '" ^ name - ^ "' because of previous error"); + ^ " because of previous error\nName pattern: '" ^ name_pattern + ^ "'"); None) (FunDeclId.Map.values crate.fun_decls)) in @@ -262,13 +265,15 @@ let translate_crate_to_pure (crate : crate) : (* Translate the trait declarations *) let trait_decls = List.filter_map - (fun a -> - try Some (SymbolicToPure.translate_trait_decl trans_ctx a) + (fun d -> + try Some (SymbolicToPure.translate_trait_decl trans_ctx d) with CFailure (meta, _) -> - let name = name_to_string trans_ctx a.name in + let name = name_to_string trans_ctx d.name in + let name_pattern = name_to_pattern_string trans_ctx d.name in save_error __FILE__ __LINE__ meta ("Could not translate the trait declaration '" ^ name - ^ "' because of previous error"); + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" + ); None) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in @@ -276,13 +281,15 @@ let translate_crate_to_pure (crate : crate) : (* Translate the trait implementations *) let trait_impls = List.filter_map - (fun a -> - try Some (SymbolicToPure.translate_trait_impl trans_ctx a) + (fun d -> + try Some (SymbolicToPure.translate_trait_impl trans_ctx d) with CFailure (meta, _) -> - let name = name_to_string trans_ctx a.name in + let name = name_to_string trans_ctx d.name in + let name_pattern = name_to_pattern_string trans_ctx d.name in save_error __FILE__ __LINE__ meta ("Could not translate the trait instance '" ^ name - ^ "' because of previous error"); + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" + ); None) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in @@ -513,9 +520,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) try Some (SymbolicToPure.translate_global ctx.trans_ctx global) with CFailure (meta, _) -> let name = name_to_string ctx.trans_ctx global.name in + let name_pattern = name_to_pattern_string ctx.trans_ctx global.name in save_error __FILE__ __LINE__ meta ("Could not translate the global declaration '" ^ name - ^ "' because of previous error"); + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None in Extract.extract_global_decl ctx fmt global body config.interface -- cgit v1.2.3 From f37e029fd7ec7dce9410f4baaaad9d09f934de57 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 May 2024 08:06:44 +0200 Subject: Fix a crash which happens when type definitions are ignored --- compiler/Translate.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0f6aa7c1..60ae99f9 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -417,9 +417,12 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) else ExtractBase.MutRecInner in - (* Retrieve the declarations *) + (* Retrieve the declarations - note that some of them might have been ignored in + case of errors *) let defs = - List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids + List.filter_map + (fun id -> Pure.TypeDeclId.Map.find_opt id ctx.trans_types) + ids in (* Check if the definition are builtin - if yes they must be ignored. -- cgit v1.2.3 From b294639a5cbd2a51fc5bb5e55e0c386ee568ca8c Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 24 May 2024 13:28:12 +0200 Subject: Rename meta into span --- compiler/Translate.ml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 60ae99f9..02d495c0 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -127,7 +127,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) let ctx = { - meta = fdef.item_meta.meta; + span = fdef.item_meta.span; decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; @@ -179,7 +179,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } - | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable" in (* Add the backward inputs *) @@ -204,10 +204,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx) try Some (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx fdef.name in let name_pattern = name_to_pattern_string trans_ctx fdef.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the function '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None @@ -244,10 +244,10 @@ let translate_crate_to_pure (crate : crate) : ( fdef.def_id, SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef ) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx fdef.name in let name_pattern = name_to_pattern_string trans_ctx fdef.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the function signature of '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); @@ -267,10 +267,10 @@ let translate_crate_to_pure (crate : crate) : List.filter_map (fun d -> try Some (SymbolicToPure.translate_trait_decl trans_ctx d) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx d.name in let name_pattern = name_to_pattern_string trans_ctx d.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the trait declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -283,10 +283,10 @@ let translate_crate_to_pure (crate : crate) : List.filter_map (fun d -> try Some (SymbolicToPure.translate_trait_impl trans_ctx d) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx d.name in let name_pattern = name_to_pattern_string trans_ctx d.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the trait instance '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -496,7 +496,7 @@ 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 - sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.meta; + sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.span; let body = trans.f in let is_opaque = Option.is_none body.Pure.body in @@ -521,10 +521,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) *) let global = try Some (SymbolicToPure.translate_global ctx.trans_ctx global) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string ctx.trans_ctx global.name in let name_pattern = name_to_pattern_string ctx.trans_ctx global.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the global declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None @@ -810,7 +810,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) export_functions_group pure_funs | GlobalGroup id -> export_global id | TraitDeclGroup (RecGroup _ids) -> - craise_opt_meta __FILE__ __LINE__ None + craise_opt_span __FILE__ __LINE__ None "Mutually recursive trait declarations are not supported" | TraitDeclGroup (NonRecGroup id) -> (* TODO: update to extract groups *) -- cgit v1.2.3