From 0b463547ddc409c885859a8bdb577746d87260a2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 May 2024 08:04:30 +0200 Subject: [PATCH 1/2] Print the name patterns of the definitions which fail to extract --- compiler/SymbolicToPure.ml | 9 +++++---- compiler/Translate.ml | 30 +++++++++++++++++++----------- 2 files changed, 24 insertions(+), 15 deletions(-) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 6c925bcd6..4aa24fcf1 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3923,14 +3923,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = List.filter_map - (fun a -> - try Some (translate_type_decl ctx a) + (fun d -> + try Some (translate_type_decl ctx d) with CFailure (meta, _) -> let env = PrintPure.decls_ctx_to_fmt_env ctx in - let name = PrintPure.name_to_string env a.name in + let name = PrintPure.name_to_string env d.name in + let name_pattern = TranslateCore.name_to_pattern_string ctx d.name in save_error __FILE__ __LINE__ meta ("Could not translate type decl '" ^ name - ^ "' because of previous error"); + ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 72a98c3db..0f6aa7c10 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 From f37e029fd7ec7dce9410f4baaaad9d09f934de57 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 May 2024 08:06:44 +0200 Subject: [PATCH 2/2] Fix a crash which happens when type definitions are ignored --- compiler/Translate.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0f6aa7c10..60ae99f9d 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.