From 9c1773530a7056c161e69471b36eaa3603f6ed26 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 17:58:32 +0200 Subject: Add field mk_return, mk_panic in SymbolicToPure.bs_ctx --- compiler/Translate.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 348183c5..22288fe2 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -158,6 +158,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx) inside_loop = false; loop_ids_map; loops = Pure.LoopId.Map.empty; + mk_return = None; + mk_panic = None; } in -- cgit v1.2.3 From fc51bfd88076a66000dbfe76e832d3fdd72aee76 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 5 Apr 2024 10:36:40 +0200 Subject: error catching should now be able to tell when code couldn't be generated --- compiler/Translate.ml | 57 +++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 46 insertions(+), 11 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 348183c5..28e5531d 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure (trans_ctx : trans_ctx) +let translate_function_to_pure_hook (trans_ctx : trans_ctx) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = @@ -195,6 +195,17 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | None -> SymbolicToPure.translate_fun_decl ctx None | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast) +let translate_function_to_pure (trans_ctx : trans_ctx) + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) + (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : + pure_fun_translation_no_loops option = + try + Some + (translate_function_to_pure_hook trans_ctx pure_type_decls fun_dsigs fdef) + with CFailure (meta, _) -> + let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + None + (* TODO: factor out the return type *) let translate_crate_to_pure (crate : crate) : trans_ctx @@ -220,32 +231,51 @@ let translate_crate_to_pure (crate : crate) : (* Compute the decomposed fun sigs for the whole crate *) let fun_dsigs = FunDeclId.Map.of_list - (List.map + (List.filter_map (fun (fdef : LlbcAst.fun_decl) -> - ( fdef.def_id, - SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx - fdef )) + try + Some + ( fdef.def_id, + SymbolicToPure.translate_fun_sig_from_decl_to_decomposed + trans_ctx fdef ) + with CFailure (meta, _) -> + let () = + save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + in + None) (FunDeclId.Map.values crate.fun_decls)) in (* Translate all the *transparent* functions *) let pure_translations = - List.map + List.filter_map (translate_function_to_pure trans_ctx type_decls_map fun_dsigs) (FunDeclId.Map.values crate.fun_decls) in (* Translate the trait declarations *) let trait_decls = - List.map - (SymbolicToPure.translate_trait_decl trans_ctx) + List.filter_map + (fun a -> + try Some (SymbolicToPure.translate_trait_decl trans_ctx a) + with CFailure (meta, _) -> + let () = + save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + in + None) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in (* Translate the trait implementations *) let trait_impls = - List.map - (SymbolicToPure.translate_trait_impl trans_ctx) + List.filter_map + (fun a -> + try Some (SymbolicToPure.translate_trait_impl trans_ctx a) + with CFailure (meta, _) -> + let () = + save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + in + None) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in @@ -471,7 +501,12 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) groups are always singletons, so the [extract_global_decl] function takes care of generating the delimiters. *) - let global = SymbolicToPure.translate_global ctx.trans_ctx global in + let global = + try Some (SymbolicToPure.translate_global ctx.trans_ctx global) + with CFailure (meta, _) -> + let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + None + in Extract.extract_global_decl ctx fmt global body config.interface (** Utility. -- cgit v1.2.3 From 760e8374533bd7e13059e18c223428baab4535ea Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 5 Apr 2024 12:29:33 +0200 Subject: resolved comments --- compiler/Translate.ml | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 28e5531d..c23b2a47 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure_hook (trans_ctx : trans_ctx) +let translate_function_to_pure_aux (trans_ctx : trans_ctx) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = @@ -201,9 +201,12 @@ let translate_function_to_pure (trans_ctx : trans_ctx) pure_fun_translation_no_loops option = try Some - (translate_function_to_pure_hook trans_ctx pure_type_decls fun_dsigs fdef) + (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef) with CFailure (meta, _) -> - let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + let () = + save_error __FILE__ __LINE__ meta + "Could not translate function because of previous error" + in None (* TODO: factor out the return type *) @@ -240,7 +243,8 @@ let translate_crate_to_pure (crate : crate) : trans_ctx fdef ) with CFailure (meta, _) -> let () = - save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + save_error __FILE__ __LINE__ meta + "Could not translate function because of previous error" in None) (FunDeclId.Map.values crate.fun_decls)) @@ -260,7 +264,8 @@ let translate_crate_to_pure (crate : crate) : try Some (SymbolicToPure.translate_trait_decl trans_ctx a) with CFailure (meta, _) -> let () = - save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + save_error __FILE__ __LINE__ meta + "Could not translate trait decl because of previous error" in None) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) @@ -273,7 +278,8 @@ let translate_crate_to_pure (crate : crate) : try Some (SymbolicToPure.translate_trait_impl trans_ctx a) with CFailure (meta, _) -> let () = - save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + save_error __FILE__ __LINE__ meta + "Could not translate trait impl because of previous error" in None) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) @@ -504,7 +510,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, _) -> - let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + let () = + save_error __FILE__ __LINE__ meta + "Could not translate global because of previous error" + in None in Extract.extract_global_decl ctx fmt global body config.interface -- cgit v1.2.3 From 3a470ec6661a494631a12594989126804aeb044d Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 5 Apr 2024 14:44:17 +0200 Subject: Resolved comments and added the name of the not translated element --- compiler/Translate.ml | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index c23b2a47..2fcf5b43 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -203,9 +203,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx) Some (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 () = save_error __FILE__ __LINE__ meta - "Could not translate function because of previous error" + ("Could not translate function '" ^ name ^ "' because of previous error") in None @@ -230,7 +231,6 @@ let translate_crate_to_pure (crate : crate) : Pure.TypeDeclId.Map.of_list (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls) in - (* Compute the decomposed fun sigs for the whole crate *) let fun_dsigs = FunDeclId.Map.of_list @@ -242,9 +242,11 @@ let translate_crate_to_pure (crate : crate) : SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef ) with CFailure (meta, _) -> + let name = name_to_string trans_ctx fdef.name in let () = save_error __FILE__ __LINE__ meta - "Could not translate function because of previous error" + ("Could not translate function signature '" ^ name + ^ "' because of previous error") in None) (FunDeclId.Map.values crate.fun_decls)) @@ -263,9 +265,11 @@ let translate_crate_to_pure (crate : crate) : (fun a -> try Some (SymbolicToPure.translate_trait_decl trans_ctx a) with CFailure (meta, _) -> + let name = name_to_string trans_ctx a.name in let () = save_error __FILE__ __LINE__ meta - "Could not translate trait decl because of previous error" + ("Could not translate trait decl '" ^ name + ^ "' because of previous error") in None) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) @@ -277,9 +281,11 @@ let translate_crate_to_pure (crate : crate) : (fun a -> try Some (SymbolicToPure.translate_trait_impl trans_ctx a) with CFailure (meta, _) -> + let name = name_to_string trans_ctx a.name in let () = save_error __FILE__ __LINE__ meta - "Could not translate trait impl because of previous error" + ("Could not translate trait impl '" ^ name + ^ "' because of previous error") in None) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) @@ -511,8 +517,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 () = + let name = name_to_string ctx.trans_ctx global.name in save_error __FILE__ __LINE__ meta - "Could not translate global because of previous error" + ("Could not translate global '" ^ name + ^ "' because of previous error") in None in -- cgit v1.2.3 From 581d5c0cb8e618382fa41e5a42175560283ff0a1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 7 Apr 2024 14:27:14 +0200 Subject: Cleanup a bit and improve the error messages --- compiler/Translate.ml | 69 ++++++++++++++++++++++++++------------------------- 1 file changed, 35 insertions(+), 34 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 2fcf5b43..870f8a22 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -204,10 +204,9 @@ 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 () = - save_error __FILE__ __LINE__ meta - ("Could not translate function '" ^ name ^ "' because of previous error") - in + save_error __FILE__ __LINE__ meta + ("Could not translate the function '" ^ name + ^ "' because of previous error"); None (* TODO: factor out the return type *) @@ -231,6 +230,7 @@ let translate_crate_to_pure (crate : crate) : Pure.TypeDeclId.Map.of_list (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls) in + (* Compute the decomposed fun sigs for the whole crate *) let fun_dsigs = FunDeclId.Map.of_list @@ -243,11 +243,9 @@ let translate_crate_to_pure (crate : crate) : trans_ctx fdef ) with CFailure (meta, _) -> let name = name_to_string trans_ctx fdef.name in - let () = - save_error __FILE__ __LINE__ meta - ("Could not translate function signature '" ^ name - ^ "' because of previous error") - in + save_error __FILE__ __LINE__ meta + ("Could not translate the function signature of '" ^ name + ^ "' because of previous error"); None) (FunDeclId.Map.values crate.fun_decls)) in @@ -266,11 +264,9 @@ let translate_crate_to_pure (crate : crate) : try Some (SymbolicToPure.translate_trait_decl trans_ctx a) with CFailure (meta, _) -> let name = name_to_string trans_ctx a.name in - let () = - save_error __FILE__ __LINE__ meta - ("Could not translate trait decl '" ^ name - ^ "' because of previous error") - in + save_error __FILE__ __LINE__ meta + ("Could not translate the trait declaration '" ^ name + ^ "' because of previous error"); None) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in @@ -282,11 +278,9 @@ let translate_crate_to_pure (crate : crate) : try Some (SymbolicToPure.translate_trait_impl trans_ctx a) with CFailure (meta, _) -> let name = name_to_string trans_ctx a.name in - let () = - save_error __FILE__ __LINE__ meta - ("Could not translate trait impl '" ^ name - ^ "' because of previous error") - in + save_error __FILE__ __LINE__ meta + ("Could not translate the trait instance '" ^ name + ^ "' because of previous error"); None) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in @@ -516,12 +510,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, _) -> - let () = - let name = name_to_string ctx.trans_ctx global.name in - save_error __FILE__ __LINE__ meta - ("Could not translate global '" ^ name - ^ "' because of previous error") - in + let name = name_to_string ctx.trans_ctx global.name in + save_error __FILE__ __LINE__ meta + ("Could not translate the global declaration '" ^ name + ^ "' because of previous error"); None in Extract.extract_global_decl ctx fmt global body config.interface @@ -778,22 +770,28 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) | TypeGroup (RecGroup ids) -> if config.extract_types then export_types_group true ids | FunGroup (NonRecGroup id) -> ( - (* Lookup *) - let pure_fun = FunDeclId.Map.find id ctx.trans_funs in + (* Lookup - the translated function may not be in the map if we had + to ignore it because of errors *) + let pure_fun = FunDeclId.Map.find_opt id ctx.trans_funs in (* Special case: we skip trait method *declarations* (we will extract their type directly in the records we generate for the trait declarations themselves, there is no point in having separate type definitions) *) - match pure_fun.f.Pure.kind with - | TraitItemDecl _ -> () - | _ -> - (* Translate *) - export_functions_group [ pure_fun ]) + match pure_fun with + | Some pure_fun -> ( + match pure_fun.f.Pure.kind with + | TraitItemDecl _ -> () + | _ -> + (* Translate *) + export_functions_group [ pure_fun ]) + | None -> ()) | FunGroup (RecGroup ids) -> (* General case of mutually recursive functions *) (* Lookup *) let pure_funs = - List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids + List.filter_map + (fun id -> FunDeclId.Map.find_opt id ctx.trans_funs) + ids in (* Translate *) export_functions_group pure_funs @@ -951,7 +949,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) | Coq -> Printf.fprintf out "End %s.\n" fi.module_name); (* Some logging *) - log#linfo (lazy ("Generated: " ^ fi.filename)); + if !Errors.error_list <> [] then + log#linfo + (lazy ("Generated the partial file (because of errors): " ^ fi.filename)) + else log#linfo (lazy ("Generated: " ^ fi.filename)); (* Flush and close the file *) close_out out -- cgit v1.2.3