WIP Beginning working on better errors: began replacing raise (Failure) and assert by craise and cassert. Does not compile yet, still need to propagate the meta variable where it's relevant

1 files changed, 42 insertions, 40 deletions

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 9af3c71b..04aadafe 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -3,6 +3,7 @@ open Types
 open Values
 open LlbcAst
 open Contexts
+open Errors
 module SA = SymbolicAst
 module Micro = PureMicroPasses
 open TranslateCore
@@ -40,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 (meta : Meta.meta) (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 =
@@ -175,7 +176,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
           SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx
         in
         { ctx with forward_inputs }
-    | _ -> raise (Failure "Unreachable")
+    | _ -> craise meta "Unreachable"
   in
 
   (* Add the backward inputs *)
@@ -194,7 +195,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast)
 
 (* TODO: factor out the return type *)
-let translate_crate_to_pure (crate : crate) :
+let translate_crate_to_pure (meta : Meta.meta) (crate : crate) :
     trans_ctx
     * Pure.type_decl list
     * pure_fun_translation list
@@ -207,7 +208,7 @@ let translate_crate_to_pure (crate : crate) :
   let trans_ctx = compute_contexts crate in
 
   (* Translate all the type definitions *)
-  let type_decls = SymbolicToPure.translate_type_decls trans_ctx in
+  let type_decls = SymbolicToPure.translate_type_decls meta trans_ctx in
 
   (* Compute the type definition map *)
   let type_decls_map =
@@ -221,7 +222,7 @@ let translate_crate_to_pure (crate : crate) :
       (List.map
          (fun (fdef : LlbcAst.fun_decl) ->
            ( fdef.def_id,
-             SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx
+             SymbolicToPure.translate_fun_sig_from_decl_to_decomposed meta trans_ctx
                fdef ))
          (FunDeclId.Map.values crate.fun_decls))
   in
@@ -229,21 +230,21 @@ let translate_crate_to_pure (crate : crate) :
   (* Translate all the *transparent* functions *)
   let pure_translations =
     List.map
-      (translate_function_to_pure trans_ctx type_decls_map fun_dsigs)
+      (translate_function_to_pure meta 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)
+      (SymbolicToPure.translate_trait_decl meta trans_ctx)
       (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)
+      (SymbolicToPure.translate_trait_impl meta trans_ctx)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
 
@@ -351,9 +352,9 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     [is_rec]: [true] if the types are recursive. Necessarily [true] if there is
     > 1 type to extract.
  *)
-let export_types_group (fmt : Format.formatter) (config : gen_config)
+let export_types_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit =
-  assert (ids <> []);
+  cassert (ids <> []) meta "TODO: Error message";
   let export_type = export_type fmt config ctx in
   let ids_set = Pure.TypeDeclId.Set.of_list ids in
   let export_type_decl kind id = export_type ids_set kind id true false in
@@ -395,11 +396,11 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
 
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
-    assert (List.for_all (fun b -> b) builtin)
+    cassert (List.for_all (fun b -> b) builtin) meta "TODO: Error message"
   else if List.exists dont_extract defs then
     (* Check if we have to ignore declarations *)
     (* Sanity check *)
-    assert (List.for_all dont_extract defs)
+    cassert (List.for_all dont_extract defs) meta "TODO: Error message"
   else (
     (* Extract the type declarations.
 
@@ -441,13 +442,14 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
 
     TODO: check correct behavior with opaque globals.
  *)
-let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
+let export_global (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : GlobalDeclId.id) : unit =
   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
-  assert (trans.loops = []);
-  let body = trans.f in
+  assert (trans.fwd.loops = []);
+  assert (trans.backs = []);
+  let body = trans.fwd.f in
 
   let is_opaque = Option.is_none body.Pure.body in
   (* Check if we extract the global *)
@@ -491,7 +493,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     Rem.: this function doesn't check [config.extract_fun_decls]: it should have
     been checked by the caller.
  *)
-let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
+let export_functions_group_scc (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (is_rec : bool) (decls : Pure.fun_decl list) : unit =
   (* Utility to check a function has a decrease clause *)
   let has_decreases_clause (def : Pure.fun_decl) : bool =
@@ -502,7 +504,7 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
   (* Extract the function declarations *)
   (* Check if the functions are mutually recursive *)
   let is_mut_rec = List.length decls > 1 in
-  assert ((not is_mut_rec) || is_rec);
+  cassert ((not is_mut_rec) || is_rec) meta "TODO: Error message";
   let decls_length = List.length decls in
   (* We open and close the declaration group with [{start, end}_fun_decl_group].
 
@@ -566,7 +568,7 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
     In case of (non-mutually) recursive functions, we use a simple procedure to
     check if the forward and backward functions are mutually recursive.
  *)
-let export_functions_group (fmt : Format.formatter) (config : gen_config)
+let export_functions_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit =
   (* Check if the definition are builtin - if yes they must be ignored.
      Note that if one definition in the group is builtin, then all the
@@ -582,7 +584,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
 
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
-    assert (List.for_all (fun b -> b) builtin)
+    cassert (List.for_all (fun b -> b) builtin) meta "TODO: Error message"
   else
     (* Utility to check a function has a decrease clause *)
     let has_decreases_clause (def : Pure.fun_decl) : bool =
@@ -614,11 +616,11 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
               | FStar ->
                   Extract.extract_template_fstar_decreases_clause ctx fmt decl
               | Coq ->
-                  raise
-                    (Failure "Coq doesn't have decreases/termination clauses")
+                  craise
+                    meta "Coq doesn't have decreases/termination clauses"
               | HOL4 ->
-                  raise
-                    (Failure "HOL4 doesn't have decreases/termination clauses")
+                  craise
+                    meta "HOL4 doesn't have decreases/termination clauses"
           in
           extract_decrease f.f;
           List.iter extract_decrease f.loops)
@@ -637,7 +639,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
 
        (* Extract the subgroups *)
        let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
-         export_functions_group_scc fmt config ctx is_rec decls
+         export_functions_group_scc meta fmt config ctx is_rec decls
        in
        List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
 
@@ -692,16 +694,16 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     split the definitions between different files (or not), we can control
     what is precisely extracted.
  *)
-let extract_definitions (fmt : Format.formatter) (config : gen_config)
+let extract_definitions (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) : unit =
   (* Export the definition groups to the file, in the proper order.
      - [extract_decl]: extract the type declaration (if not filtered)
      - [extract_extra_info]: extra the extra type information (e.g.,
        the [Arguments] information in Coq).
   *)
-  let export_functions_group = export_functions_group fmt config ctx in
-  let export_global = export_global fmt config ctx in
-  let export_types_group = export_types_group fmt config ctx in
+  let export_functions_group = export_functions_group meta fmt config ctx in
+  let export_global = export_global meta fmt config ctx in
+  let export_types_group = export_types_group meta fmt config ctx in
   let export_trait_decl_group id =
     export_trait_decl fmt config ctx id true false
   in
@@ -783,7 +785,7 @@ type extract_file_info = {
   custom_includes : string list;
 }
 
-let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
+let extract_file (meta : Meta.meta) (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
     : unit =
   (* Open the file and create the formatter *)
   let out = open_out fi.filename in
@@ -883,7 +885,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   Format.pp_open_vbox fmt 0;
 
   (* Extract the definitions *)
-  extract_definitions fmt config ctx;
+  extract_definitions meta fmt config ctx;
 
   (* Close the box and end the formatting *)
   Format.pp_close_box fmt ();
@@ -903,11 +905,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   close_out out
 
 (** Translate a crate and write the synthesized code to an output file. *)
-let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
+let translate_crate (meta : Meta.meta) (filename : string) (dest_dir : string) (crate : crate) :
     unit =
   (* Translate the module to the pure AST *)
   let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls =
-    translate_crate_to_pure crate
+    translate_crate_to_pure meta crate
   in
 
   (* Initialize the names map by registering the keywords used in the
@@ -1036,7 +1038,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     match Filename.chop_suffix_opt ~suffix:".llbc" filename with
     | None ->
         (* Note that we already checked the suffix upon opening the file *)
-        raise (Failure "Unreachable")
+        craise meta "Unreachable"
     | Some filename ->
         (* Retrieve the file basename *)
         let basename = Filename.basename filename in
@@ -1078,7 +1080,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     let ( ^^ ) = Filename.concat in
     if !Config.split_files then mkdir_if (dest_dir ^^ crate_name);
     if needs_clauses_module then (
-      assert !Config.split_files;
+      cassert !Config.split_files meta "TODO: Error message";
       mkdir_if (dest_dir ^^ crate_name ^^ "Clauses")));
 
   (* Copy the "Primitives" file, if necessary *)
@@ -1228,7 +1230,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
              custom_includes = [];
            }
          in
-         extract_file opaque_config ctx file_info;
+         extract_file meta opaque_config ctx file_info;
          (* Return the additional dependencies *)
          [ opaque_imported_module ])
        else []
@@ -1269,7 +1271,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          custom_includes = opaque_types_module;
        }
      in
-     extract_file types_config ctx file_info;
+     extract_file meta types_config ctx file_info;
 
      (* Extract the template clauses *)
      (if needs_clauses_module && !Config.extract_template_decreases_clauses then
@@ -1298,7 +1300,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             custom_includes = [];
           }
         in
-        extract_file template_clauses_config ctx file_info);
+        extract_file meta template_clauses_config ctx file_info);
 
      (* Extract the opaque fun declarations, if needed *)
      let opaque_funs_module =
@@ -1354,7 +1356,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
              custom_includes = [ types_module ];
            }
          in
-         extract_file opaque_config ctx file_info;
+         extract_file meta opaque_config ctx file_info;
          (* Return the additional dependencies *)
          [ opaque_imported_module ])
        else []
@@ -1395,7 +1397,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
            [ types_module ] @ opaque_funs_module @ clauses_module;
        }
      in
-     extract_file fun_config ctx file_info)
+     extract_file meta fun_config ctx file_info)
    else
      let gen_config =
        {
@@ -1428,7 +1430,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          custom_includes = [];
        }
      in
-     extract_file gen_config ctx file_info);
+     extract_file meta gen_config ctx file_info);
 
   (* Generate the build file *)
   match !Config.backend with