error catching should now be able to tell when code couldn't be generated

3 files changed, 144 insertions, 101 deletions

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.