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/Extract.ml | 181 +++++++++++++++++++++++---------------------- compiler/SymbolicToPure.ml | 7 +- compiler/Translate.ml | 57 +++++++++++--- 3 files changed, 144 insertions(+), 101 deletions(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index af0bf98d..1fc8a97f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1880,99 +1880,102 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) and {!extract_fun_decl}. *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (global : global_decl) (body : fun_decl) (interface : bool) : unit = + (global : global_decl option) (body : fun_decl) (interface : bool) : unit = let meta = body.meta in sanity_check __FILE__ __LINE__ body.is_global_decl_body meta; sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta; - - (* Add a break then the name of the corresponding LLBC declaration *) - F.pp_print_break fmt 0 0; - let name = - if !Config.extract_external_name_patterns && not global.is_local then - Some global.llbc_name - else None - in - extract_comment_with_span ctx fmt - [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] - name global.meta.span; - F.pp_print_space fmt (); - - let decl_name = ctx_get_global meta global.def_id ctx in - let body_name = - ctx_get_function meta - (FromLlbc (Pure.FunId (FRegular global.body_id), None)) - ctx - in - let decl_ty, body_ty = - let ty = body.signature.output in - if body.signature.fwd_info.effect_info.can_fail then - (unwrap_result_ty meta ty, ty) - else (ty, mk_result_ty ty) - in - (* Add the type parameters *) - let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params meta global.llbc_name global.llbc_generics - global.generics ctx - in - match body.body with - | None -> - (* No body: only generate a [val x_c : u32] declaration *) - let kind = if interface then Declared else Assumed in - if !backend = HOL4 then - extract_global_decl_hol4_opaque meta ctx fmt decl_name global.generics - decl_ty - else - extract_global_decl_body_gen meta ctx fmt kind decl_name global.generics - type_params cg_params trait_clauses decl_ty None - | Some body -> - (* There is a body *) - (* Generate: [let x_body : result u32 = Return 3] *) - extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name - global.generics type_params cg_params trait_clauses body_ty - (Some (fun fmt -> extract_texpression meta ctx fmt false body.body)); + match global with + | Some global -> ( + (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; - (* Generate: [let x_c : u32 = eval_global x_body] *) - extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name - global.generics type_params cg_params trait_clauses decl_ty - (Some - (fun fmt -> - let all_params = - List.concat [ type_params; cg_params; trait_clauses ] - in - let extract_params () = - List.iter - (fun p -> - F.pp_print_space fmt (); - F.pp_print_string fmt p) - all_params - in - let use_brackets = all_params <> [] in - (* Extract the name *) - let before, after = - match !backend with - | FStar | Lean -> - ( (fun () -> - F.pp_print_string fmt "eval_global"; - F.pp_print_space fmt ()), - fun () -> () ) - | Coq -> - ((fun () -> ()), fun () -> F.pp_print_string fmt "%global") - | HOL4 -> - ( (fun () -> - F.pp_print_string fmt "get_return_value"; - F.pp_print_space fmt ()), - fun () -> () ) - in - before (); - if use_brackets then F.pp_print_string fmt "("; - F.pp_print_string fmt body_name; - (* Extract the generic params *) - extract_params (); - if use_brackets then F.pp_print_string fmt ")"; - (* *) - after ())); - (* Add a break to insert lines between declarations *) - F.pp_print_break fmt 0 0 + let name = + if !Config.extract_external_name_patterns && not global.is_local then + Some global.llbc_name + else None + in + extract_comment_with_span ctx fmt + [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] + name global.meta.span; + F.pp_print_space fmt (); + + let decl_name = ctx_get_global meta global.def_id ctx in + let body_name = + ctx_get_function meta + (FromLlbc (Pure.FunId (FRegular global.body_id), None)) + ctx + in + let decl_ty, body_ty = + let ty = body.signature.output in + if body.signature.fwd_info.effect_info.can_fail then + (unwrap_result_ty meta ty, ty) + else (ty, mk_result_ty ty) + in + (* Add the type parameters *) + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params meta global.llbc_name global.llbc_generics + global.generics ctx + in + match body.body with + | None -> + (* No body: only generate a [val x_c : u32] declaration *) + let kind = if interface then Declared else Assumed in + if !backend = HOL4 then + extract_global_decl_hol4_opaque meta ctx fmt decl_name + global.generics decl_ty + else + extract_global_decl_body_gen meta ctx fmt kind decl_name + global.generics type_params cg_params trait_clauses decl_ty None + | Some body -> + (* There is a body *) + (* Generate: [let x_body : result u32 = Return 3] *) + extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name + global.generics type_params cg_params trait_clauses body_ty + (Some (fun fmt -> extract_texpression meta ctx fmt false body.body)); + F.pp_print_break fmt 0 0; + (* Generate: [let x_c : u32 = eval_global x_body] *) + extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name + global.generics type_params cg_params trait_clauses decl_ty + (Some + (fun fmt -> + let all_params = + List.concat [ type_params; cg_params; trait_clauses ] + in + let extract_params () = + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + all_params + in + let use_brackets = all_params <> [] in + (* Extract the name *) + let before, after = + match !backend with + | FStar | Lean -> + ( (fun () -> + F.pp_print_string fmt "eval_global"; + F.pp_print_space fmt ()), + fun () -> () ) + | Coq -> + ( (fun () -> ()), + fun () -> F.pp_print_string fmt "%global" ) + | HOL4 -> + ( (fun () -> + F.pp_print_string fmt "get_return_value"; + F.pp_print_space fmt ()), + fun () -> () ) + in + before (); + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt body_name; + (* Extract the generic params *) + extract_params (); + if use_brackets then F.pp_print_string fmt ")"; + (* *) + after ())); + (* Add a break to insert lines between declarations *) + F.pp_print_break fmt 0 0) + | None -> () (** Similar to {!extract_trait_decl_register_names} *) let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index f036cc37..b4c55d80 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3861,7 +3861,12 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = def let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = - List.map (translate_type_decl ctx) + List.filter_map + (fun a -> + try Some (translate_type_decl ctx a) + with CFailure (meta, _) -> + let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) 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/Extract.ml | 184 +++++++++++++++++++++++---------------------- compiler/SymbolicToPure.ml | 5 +- compiler/Translate.ml | 23 ++++-- 3 files changed, 113 insertions(+), 99 deletions(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1fc8a97f..f7d08fdb 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1879,102 +1879,104 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl} and {!extract_fun_decl}. *) -let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (global : global_decl option) (body : fun_decl) (interface : bool) : unit = +let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) + (global : global_decl) (body : fun_decl) (interface : bool) : unit = let meta = body.meta in sanity_check __FILE__ __LINE__ body.is_global_decl_body meta; sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta; - match global with - | Some global -> ( - (* Add a break then the name of the corresponding LLBC declaration *) + (* Add a break then the name of the corresponding LLBC declaration *) + F.pp_print_break fmt 0 0; + let name = + if !Config.extract_external_name_patterns && not global.is_local then + Some global.llbc_name + else None + in + extract_comment_with_span ctx fmt + [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] + name global.meta.span; + F.pp_print_space fmt (); + + let decl_name = ctx_get_global meta global.def_id ctx in + let body_name = + ctx_get_function meta + (FromLlbc (Pure.FunId (FRegular global.body_id), None)) + ctx + in + let decl_ty, body_ty = + let ty = body.signature.output in + if body.signature.fwd_info.effect_info.can_fail then + (unwrap_result_ty meta ty, ty) + else (ty, mk_result_ty ty) + in + (* Add the type parameters *) + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params meta global.llbc_name global.llbc_generics + global.generics ctx + in + match body.body with + | None -> + (* No body: only generate a [val x_c : u32] declaration *) + let kind = if interface then Declared else Assumed in + if !backend = HOL4 then + extract_global_decl_hol4_opaque meta ctx fmt decl_name global.generics + decl_ty + else + extract_global_decl_body_gen meta ctx fmt kind decl_name global.generics + type_params cg_params trait_clauses decl_ty None + | Some body -> + (* There is a body *) + (* Generate: [let x_body : result u32 = Return 3] *) + extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name + global.generics type_params cg_params trait_clauses body_ty + (Some (fun fmt -> extract_texpression meta ctx fmt false body.body)); F.pp_print_break fmt 0 0; - let name = - if !Config.extract_external_name_patterns && not global.is_local then - Some global.llbc_name - else None - in - extract_comment_with_span ctx fmt - [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] - name global.meta.span; - F.pp_print_space fmt (); + (* Generate: [let x_c : u32 = eval_global x_body] *) + extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name + global.generics type_params cg_params trait_clauses decl_ty + (Some + (fun fmt -> + let all_params = + List.concat [ type_params; cg_params; trait_clauses ] + in + let extract_params () = + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + all_params + in + let use_brackets = all_params <> [] in + (* Extract the name *) + let before, after = + match !backend with + | FStar | Lean -> + ( (fun () -> + F.pp_print_string fmt "eval_global"; + F.pp_print_space fmt ()), + fun () -> () ) + | Coq -> + ((fun () -> ()), fun () -> F.pp_print_string fmt "%global") + | HOL4 -> + ( (fun () -> + F.pp_print_string fmt "get_return_value"; + F.pp_print_space fmt ()), + fun () -> () ) + in + before (); + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt body_name; + (* Extract the generic params *) + extract_params (); + if use_brackets then F.pp_print_string fmt ")"; + (* *) + after ())); + (* Add a break to insert lines between declarations *) + F.pp_print_break fmt 0 0 - let decl_name = ctx_get_global meta global.def_id ctx in - let body_name = - ctx_get_function meta - (FromLlbc (Pure.FunId (FRegular global.body_id), None)) - ctx - in - let decl_ty, body_ty = - let ty = body.signature.output in - if body.signature.fwd_info.effect_info.can_fail then - (unwrap_result_ty meta ty, ty) - else (ty, mk_result_ty ty) - in - (* Add the type parameters *) - let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params meta global.llbc_name global.llbc_generics - global.generics ctx - in - match body.body with - | None -> - (* No body: only generate a [val x_c : u32] declaration *) - let kind = if interface then Declared else Assumed in - if !backend = HOL4 then - extract_global_decl_hol4_opaque meta ctx fmt decl_name - global.generics decl_ty - else - extract_global_decl_body_gen meta ctx fmt kind decl_name - global.generics type_params cg_params trait_clauses decl_ty None - | Some body -> - (* There is a body *) - (* Generate: [let x_body : result u32 = Return 3] *) - extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name - global.generics type_params cg_params trait_clauses body_ty - (Some (fun fmt -> extract_texpression meta ctx fmt false body.body)); - F.pp_print_break fmt 0 0; - (* Generate: [let x_c : u32 = eval_global x_body] *) - extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name - global.generics type_params cg_params trait_clauses decl_ty - (Some - (fun fmt -> - let all_params = - List.concat [ type_params; cg_params; trait_clauses ] - in - let extract_params () = - List.iter - (fun p -> - F.pp_print_space fmt (); - F.pp_print_string fmt p) - all_params - in - let use_brackets = all_params <> [] in - (* Extract the name *) - let before, after = - match !backend with - | FStar | Lean -> - ( (fun () -> - F.pp_print_string fmt "eval_global"; - F.pp_print_space fmt ()), - fun () -> () ) - | Coq -> - ( (fun () -> ()), - fun () -> F.pp_print_string fmt "%global" ) - | HOL4 -> - ( (fun () -> - F.pp_print_string fmt "get_return_value"; - F.pp_print_space fmt ()), - fun () -> () ) - in - before (); - if use_brackets then F.pp_print_string fmt "("; - F.pp_print_string fmt body_name; - (* Extract the generic params *) - extract_params (); - if use_brackets then F.pp_print_string fmt ")"; - (* *) - after ())); - (* Add a break to insert lines between declarations *) - F.pp_print_break fmt 0 0) +let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) + (global : global_decl option) (body : fun_decl) (interface : bool) : unit = + match global with + | Some global -> extract_global_decl_aux ctx fmt global body interface | None -> () (** Similar to {!extract_trait_decl_register_names} *) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index b4c55d80..eac4adb9 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3865,7 +3865,10 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = (fun a -> try Some (translate_type_decl ctx a) 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 generate code, see previous error" + in None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) 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/SymbolicToPure.ml | 5 ++++- compiler/Translate.ml | 20 ++++++++++++++------ 2 files changed, 18 insertions(+), 7 deletions(-) (limited to 'compiler') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index eac4adb9..607da445 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3865,9 +3865,12 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = (fun a -> try Some (translate_type_decl ctx a) with CFailure (meta, _) -> + let env = PrintPure.decls_ctx_to_fmt_env ctx in + let name = PrintPure.name_to_string env a.name in let () = save_error __FILE__ __LINE__ meta - "Could not generate code, see previous error" + ("Could not translate type decl '" ^ name + ^ "' because of previous error") in None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) 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/Extract.ml | 3 +- compiler/InterpreterBorrows.ml | 26 ++++++-------- compiler/InterpreterBorrowsCore.ml | 4 +-- compiler/InterpreterPaths.ml | 21 ++++++------ compiler/InterpreterProjectors.ml | 4 +-- compiler/Invariants.ml | 5 ++- compiler/Main.ml | 4 ++- compiler/PrePasses.ml | 19 +++++++++-- compiler/Print.ml | 1 + compiler/PureTypeCheck.ml | 9 +++-- compiler/SymbolicToPure.ml | 8 ++--- compiler/Translate.ml | 69 +++++++++++++++++++------------------- 12 files changed, 91 insertions(+), 82 deletions(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index f7d08fdb..985fb470 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) ^ string_of_int (List.length types) ^ " type arguments" in - log#serror err; + save_error __FILE__ __LINE__ None err; Result.Error (types, err)) else let types = List.combine filter types in @@ -1884,6 +1884,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) let meta = body.meta in sanity_check __FILE__ __LINE__ body.is_global_decl_body meta; sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta; + (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; let name = diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index e593ae75..a158ed9a 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -303,13 +303,11 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) if bid' = bid then ( (* Sanity check *) let expected_ty = ty in - if nv.ty <> expected_ty then ( - log#serror - ("give_back_value: improper type:\n- expected: " - ^ ty_to_string ctx ty ^ "\n- received: " - ^ ty_to_string ctx nv.ty); + if nv.ty <> expected_ty then craise __FILE__ __LINE__ meta - "Value given back doesn't have the proper type"); + ("Value given back doesn't have the proper type:\n\ + - expected: " ^ ty_to_string ctx ty ^ "\n- received: " + ^ ty_to_string ctx nv.ty); (* Replace *) set_replaced (); nv.value) @@ -540,13 +538,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta) * see the comment at the level of the definition of * {!typed_avalue} *) let _, expected_ty, _ = ty_get_ref ty in - if nv.ty <> expected_ty then ( - log#serror - ("give_back_avalue_to_same_abstraction: improper type:\n\ + if nv.ty <> expected_ty then + craise __FILE__ __LINE__ meta + ("Value given back doesn't have the proper type:\n\ - expected: " ^ ty_to_string ctx ty ^ "\n- received: " ^ ty_to_string ctx nv.ty); - craise __FILE__ __LINE__ meta - "Value given back doesn't have the proper type"); (* This is the loan we are looking for: apply the projection to * the value we give back and replaced this mutable loan with * an ended loan *) @@ -836,26 +832,26 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) match lookup_borrow_opt ek_all l ctx with | None -> () (* Ok *) | Some _ -> - log#lerror + log#ltrace (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": borrow didn't disappear:\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)); - craise __FILE__ __LINE__ meta "Borrow not eliminated" + internal_error __FILE__ __LINE__ meta in match lookup_loan_opt meta ek_all l ctx with | None -> () (* Ok *) | Some _ -> - log#lerror + log#ltrace (lazy (fun_name ^ ": " ^ BorrowId.to_string l ^ ": loan didn't disappear:\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)); - craise __FILE__ __LINE__ meta "Loan not eliminated" + internal_error __FILE__ __LINE__ meta in unit_to_cm_fun check_disappeared diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index 6e65b11d..a01be046 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -162,11 +162,11 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) sanity_check __FILE__ __LINE__ (ty1 = ty2) meta; default | _ -> - log#lerror + log#ltrace (lazy ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1 ^ "\n- ty2: " ^ show_ty ty2)); - craise __FILE__ __LINE__ meta "Unreachable" + internal_error __FILE__ __LINE__ meta (** Check if two different projections intersect. This is necessary when giving a symbolic value to an abstraction: we need to check that diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index f2c0bcb1..ab3daa72 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -83,7 +83,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) let nv = update v in (* Type checking *) if nv.ty <> v.ty then ( - log#lerror + log#ltrace (lazy ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: " ^ show_ety v.ty)); @@ -252,8 +252,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) let pe = "- pe: " ^ show_projection_elem pe in let v = "- v:\n" ^ show_value v in let ty = "- ty:\n" ^ show_ety ty in - log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty); - craise __FILE__ __LINE__ meta "Inconsistent projection") + craise __FILE__ __LINE__ meta + ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty)) (** Generic function to access (read/write) the value at a given place. @@ -319,14 +319,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place) (* Note that we ignore the new environment: it should be the same as the original one. *) - if !Config.sanity_checks then - if ctx1 <> ctx then ( - let msg = - "Unexpected environment update:\nNew environment:\n" - ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env - in - log#serror msg; - craise __FILE__ __LINE__ meta "Unexpected environment update"); + (if !Config.sanity_checks then + if ctx1 <> ctx then + let msg = + "Unexpected environment update:\nNew environment:\n" + ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env + in + craise __FILE__ __LINE__ meta msg); Ok read_value let read_place (meta : Meta.meta) (access : access_kind) (p : place) diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 6e86e6a4..3993d845 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -217,12 +217,12 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) meta); ASymbolic (AProjBorrows (s, ty)) | _ -> - log#lerror + log#ltrace (lazy ("apply_proj_borrows: unexpected inputs:\n- input value: " ^ typed_value_to_string ~meta:(Some meta) ctx v ^ "\n- proj rty: " ^ ty_to_string ctx ty)); - craise __FILE__ __LINE__ meta "Unreachable" + internal_error __FILE__ __LINE__ meta in { value; ty } diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 642d7a37..2ccf3ad4 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) : "find_info: could not find the representant of borrow " ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string () in - log#serror err; craise __FILE__ __LINE__ meta err in @@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit = | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()) | AIgnored, _ -> () | _ -> - log#lerror + log#ltrace (lazy ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv ^ "\n- value: " ^ typed_avalue_to_string ~meta:(Some meta) ctx atv ^ "\n- type: " ^ ty_to_string ctx atv.ty)); - craise __FILE__ __LINE__ meta "Erroneous typing"); + internal_error __FILE__ __LINE__ meta); (* Continue exploring to inspect the subterms *) super#visit_typed_avalue info atv end diff --git a/compiler/Main.ml b/compiler/Main.ml index 416f3a07..6161f2f2 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -283,7 +283,9 @@ let () = if !Errors.error_list <> [] then ( List.iter (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg)) - !Errors.error_list; + (* Reverse the list of error messages so that we print them from the + earliest to the latest. *) + (List.rev !Errors.error_list); exit 1); (* Print total elapsed time *) diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 0b39f64a..a46ef79c 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -238,9 +238,9 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl = method! visit_Sequence env st1 st2 = match st1.content with | Loop _ -> - sanity_check __FILE__ __LINE__ + cassert __FILE__ __LINE__ (statement_has_no_loop_break_continue st2) - st2.meta; + st2.meta "Sequences of loops are not supported yet"; (replace_breaks_with st1 st2).content | _ -> super#visit_Sequence env st1 st2 end @@ -437,9 +437,22 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl = let apply_passes (crate : crate) : crate = let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in + (* Attempt to apply a pass: if it fails we replace the body by [None] *) + let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) = + try pass f + with CFailure (_, _) -> + (* The error was already registered, we don't need to register it twice. + However, we replace the body of the function, and save an error to + report to the user the fact that we will ignore the function body *) + let fmt = Print.Crate.crate_to_fmt_env crate in + let name = Print.name_to_string fmt f.name in + save_error __FILE__ __LINE__ (Some f.meta) + ("Ignoring the body of '" ^ name ^ "' because of previous error"); + { f with body = None } + in let fun_decls = List.fold_left - (fun fl pass -> FunDeclId.Map.map pass fl) + (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl) crate.fun_decls passes in let crate = { crate with fun_decls } in diff --git a/compiler/Print.ml b/compiler/Print.ml index dad1aea3..51286553 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -1,4 +1,5 @@ include Charon.PrintUtils +include Charon.PrintTypes include Charon.PrintLlbcAst open Charon.PrintTypes open Charon.PrintExpressions diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index 098e2564..27044c27 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -93,12 +93,11 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx) get_adt_field_types meta ctx.type_decls type_id av.variant_id generics in let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx = - if ty <> v.ty then ( + if ty <> v.ty then (* TODO: we need to normalize the types *) - log#serror - ("check_typed_pattern: not the same types:" ^ "\n- ty: " - ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); - craise __FILE__ __LINE__ meta "Inconsistent types"); + craise __FILE__ __LINE__ meta + ("Inconsistent types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: " + ^ show_ty v.ty); check_typed_pattern meta ctx v in (* Check the field types: check that the field patterns have the expected diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 607da445..93f9ef75 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3867,11 +3867,9 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = with CFailure (meta, _) -> let env = PrintPure.decls_ctx_to_fmt_env ctx in let name = PrintPure.name_to_string env a.name in - let () = - save_error __FILE__ __LINE__ meta - ("Could not translate type decl '" ^ name - ^ "' because of previous error") - in + save_error __FILE__ __LINE__ meta + ("Could not translate type decl '" ^ name + ^ "' because of previous error"); None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) 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 From a9a2f81e365eeef4fd157fb56cd5107f95c91163 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 7 Apr 2024 14:47:36 +0200 Subject: Improve the error messages further --- compiler/Interpreter.ml | 12 ++++++++++++ compiler/InterpreterStatements.ml | 13 ++++++++++++- compiler/TypesUtils.ml | 20 ++++++++++++++++++++ 3 files changed, 44 insertions(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index d0a54750..769e3144 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -191,6 +191,18 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : * do it, and because it gives a bit of sanity. * *) let sg = fdef.signature in + (* Sanity check: no nested borrows, borrows in ADTs, etc. *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) + (sg.output :: sg.inputs)) + fdef.meta "Nested borrows are not supported yet"; + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) + (sg.output :: sg.inputs)) + fdef.meta "ADTs containing borrows are not supported yet"; + (* Create the context *) let regions_hierarchy = FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 1cf1c5ef..de89f316 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1365,10 +1365,21 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = eval_transparent_function_call_symbolic_inst meta call ctx in - (* Sanity check *) + (* Sanity check: same number of inputs *) sanity_check __FILE__ __LINE__ (List.length call.args = List.length def.signature.inputs) def.meta; + (* Sanity check: no nested borrows, borrows in ADTs, etc. *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) + (inst_sg.output :: inst_sg.inputs)) + meta "Nested borrows are not supported yet"; + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) + (inst_sg.output :: inst_sg.inputs)) + meta "ADTs containing borrows are not supported yet"; (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config def.meta func def.signature regions_hierarchy inst_sg generics trait_method_generics call.args call.dest diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index f5dd7df4..b2c60cc6 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -12,6 +12,26 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = let info = TypesAnalysis.analyze_ty infos ty in info.TypesAnalysis.contains_borrow +let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool + = + let visitor = + object + inherit [_] iter_ty as super + + method! visit_ty env ty = + match ty with + | TAdt (type_id, _) when type_id <> TTuple -> + let info = TypesAnalysis.analyze_ty infos ty in + if info.TypesAnalysis.contains_borrow then raise Found + else super#visit_ty env ty + | _ -> super#visit_ty env ty + end + in + try + visitor#visit_ty () ty; + false + with Found -> true + (** Retuns true if the type contains nested borrows. Note that we can't simply explore the type and look for regions: sometimes -- cgit v1.2.3