Refactor the handling of errors and warnings (#44)

* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/

* Replaced eprintf error.  Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.

* Raise on error before calling external tools.

* Added diagnostics to clightgen.

* Fix error handling of AsmToJson.

* Cleanup error handling of Elab and C2C.

*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.

1 files changed, 0 insertions, 430 deletions

diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml
deleted file mode 100644
index 34fc4fcf..00000000
--- a/cparser/Cerrors.ml
+++ /dev/null
@@ -1,430 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Management of errors and warnings *)
-
-open Format
-open Commandline
-
-(* Should errors be treated as fatal *)
-let error_fatal = ref false
-
-(* Maximum number of errors, 0 means unlimited *)
-let max_error = ref 0
-
-(* Whether [-Woption] should be printed *)
-let diagnostics_show_option = ref true
-
-(* Test if color diagnostics are available by testing if stderr is a tty
-   and if the environment varibale TERM is set
-*)
-let color_diagnostics =
-  let term = try Sys.getenv "TERM" with Not_found -> "" in
-  let activate = try
-      (Unix.isatty Unix.stderr && term <> "dumb" && term <>"")
-    with _ -> false in
-  ref activate
-
-let num_errors = ref 0
-let num_warnings = ref 0
-
-
-let error_limit_reached  () =
-  let max_err = !max_error in
-  max_err <> 0 && !num_errors >= max_err - 1
-
-let reset () = num_errors := 0; num_warnings := 0
-
-exception Abort
-
-(* [fatal_error_raw] is identical to [fatal_error], except it uses [Printf]
-   to print its message, as opposed to [Format], and does not automatically
-   introduce indentation and a final dot into the message. This is useful
-   for multi-line messages. *)
-
-let fatal_error_raw fmt =
-  incr num_errors;
-  Printf.kfprintf
-    (fun _ -> raise Abort)
-    stderr
-    (fmt ^^ "Fatal error; compilation aborted.\n%!")
-
-type msg_class =
-  | WarningMsg
-  | ErrorMsg
-  | FatalErrorMsg
-  | SuppressedMsg
-
-type warning_type =
-  | Unnamed
-  | Unknown_attribute
-  | Zero_length_array
-  | Celeven_extension
-  | Gnu_empty_struct
-  | Missing_declarations
-  | Constant_conversion
-  | Int_conversion
-  | Varargs
-  | Implicit_function_declaration
-  | Pointer_type_mismatch
-  | Compare_distinct_pointer_types
-  | Implicit_int
-  | Main_return_type
-  | Invalid_noreturn
-  | Return_type
-  | Literal_range
-  | Unknown_pragmas
-  | CompCert_conformance
-  | Inline_asm_sdump
-  | Unused_variable
-  | Unused_parameter
-
-(* List of active warnings *)
-let active_warnings: warning_type list ref = ref [
-  Unnamed;
-  Unknown_attribute;
-  Celeven_extension;
-  Gnu_empty_struct;
-  Missing_declarations;
-  Constant_conversion;
-  Int_conversion;
-  Varargs;
-  Implicit_function_declaration;
-  Pointer_type_mismatch;
-  Compare_distinct_pointer_types;
-  Implicit_int;
-  Main_return_type;
-  Invalid_noreturn;
-  Return_type;
-  Literal_range;
-  Inline_asm_sdump;
-]
-
-(* List of errors treated as warning *)
-let error_warnings: warning_type list ref = ref []
-
-(* Conversion from warning type to string *)
-let string_of_warning = function
-  | Unnamed -> ""
-  | Unknown_attribute -> "unknown-attributes"
-  | Zero_length_array -> "zero-length-array"
-  | Celeven_extension -> "c11-extensions"
-  | Gnu_empty_struct -> "gnu-empty-struct"
-  | Missing_declarations -> "missing-declarations"
-  | Constant_conversion -> "constant-conversion"
-  | Int_conversion -> "int-conversion"
-  | Varargs -> "varargs"
-  | Implicit_function_declaration -> "implicit-function-declaration"
-  | Pointer_type_mismatch -> "pointer-type-mismatch"
-  | Compare_distinct_pointer_types -> "compare-distinct-pointer-types"
-  | Implicit_int -> "implicit-int"
-  | Main_return_type -> "main-return-type"
-  | Invalid_noreturn -> "invalid-noreturn"
-  | Return_type -> "return-type"
-  | Literal_range -> "literal-range"
-  | Unknown_pragmas -> "unknown-pragmas"
-  | CompCert_conformance -> "compcert-conformance"
-  | Inline_asm_sdump -> "inline-asm-sdump"
-  | Unused_variable -> "unused-variable"
-  | Unused_parameter -> "unused-parameter"
-
-(* Activate the given warning *)
-let activate_warning w () =
-  if not (List.mem w !active_warnings) then
-    active_warnings:=w::!active_warnings
-
-(* Deactivate the given warning*)
-let deactivate_warning w  () =
-  active_warnings:=List.filter ((<>) w) !active_warnings;
-  error_warnings:= List.filter ((<>) w) !error_warnings
-
-(* Activate error for warning *)
-let warning_as_error w ()=
-  activate_warning w ();
-  if not (List.mem w !error_warnings) then
-    error_warnings := w::!error_warnings
-
-(* Deactivate error for warning *)
-let warning_not_as_error w () =
-  error_warnings:= List.filter ((<>) w) !error_warnings
-
-(* Activate all warnings *)
-let wall () =
-  active_warnings:=[
-    Unnamed;
-    Unknown_attribute;
-    Zero_length_array;
-    Celeven_extension;
-    Gnu_empty_struct;
-    Missing_declarations;
-    Constant_conversion;
-    Int_conversion;
-    Varargs;
-    Implicit_function_declaration;
-    Pointer_type_mismatch;
-    Compare_distinct_pointer_types;
-    Implicit_int;
-    Main_return_type;
-    Invalid_noreturn;
-    Return_type;
-    Literal_range;
-    Unknown_pragmas;
-    CompCert_conformance;
-    Inline_asm_sdump;
-    Unused_variable;
-    Unused_parameter
-  ]
-
-let wnothing () =
-  active_warnings :=[]
-
-(* Make all warnings an error *)
-let werror () =
-  error_warnings:=[
-    Unnamed;
-    Unknown_attribute;
-    Zero_length_array;
-    Celeven_extension;
-    Gnu_empty_struct;
-    Missing_declarations;
-    Constant_conversion;
-    Int_conversion;
-    Varargs;
-    Implicit_function_declaration;
-    Pointer_type_mismatch;
-    Compare_distinct_pointer_types;
-    Implicit_int;
-    Main_return_type;
-    Invalid_noreturn;
-    Return_type;
-    Literal_range;
-    Unknown_pragmas;
-    CompCert_conformance;
-    Inline_asm_sdump;
-    Unused_variable;
-  ]
-
-(* Generate the warning key for the message *)
-let key_of_warning w =
-  match w with
-  | Unnamed -> None
-  | _ -> if !diagnostics_show_option then
-      Some ("-W"^(string_of_warning w))
-    else
-      None
-
-(* Add -Werror to the printed keys *)
-let key_add_werror w =
-  if !diagnostics_show_option then
-    match w with
-    | None -> Some ("-Werror")
-    | Some s -> Some ("-Werror,"^s)
-  else
-    None
-
-(* Lookup how to print the warning *)
-let classify_warning w =
-  let key = key_of_warning w in
-  if List.mem w !active_warnings then
-    if List.mem w !error_warnings then
-      let key = key_add_werror key in
-      if !error_fatal then
-        FatalErrorMsg,key
-      else
-        ErrorMsg,key
-    else
-      WarningMsg,key
-  else
-    SuppressedMsg,None
-
-(* Print color codes if color_diagnostics are enabled *)
-let cprintf fmt c =
-  if !color_diagnostics then
-    fprintf fmt c
-  else
-    ifprintf fmt c
-
-(* Reset color codes *)
-let rsc fmt =
-  cprintf fmt "\x1b[0m"
-
-(* BOLD *)
-let bc fmt =
-  cprintf fmt "\x1b[1m"
-
-(* RED *)
-let rc fmt =
-  cprintf fmt "\x1b[31;1m"
-
-(* MAGENTA *)
-let mc fmt  =
-  cprintf fmt "\x1b[35;1m"
-
-(* Print key (if available) and flush the formatter *)
-let pp_key key fmt =
-  let key = match key with
-  | None -> ""
-  | Some s -> " ["^s^"]" in
-  fprintf fmt "%s%t@." key rsc
-
-(* Different loc output formats *)
-type loc_format =
-  | Default
-  | MSVC
-  | Vi
-
-let diagnostics_format : loc_format ref = ref Default
-
-(* Parse the option string *)
-let parse_loc_format s =
-  let s = String.sub s 21 ((String.length s) - 21) in
-  let loc_fmt = match s with
-  | "ccomp" -> Default
-  | "msvc" -> MSVC
-  | "vi" -> Vi
-  | s -> Printf.eprintf "Invalid value '%s' in '-fdiagnostics-format=%s'\n" s s; exit 2 in
-  diagnostics_format := loc_fmt
-
-(* Print the location or ccomp for the case of unknown loc *)
-let pp_loc fmt (filename,lineno) =
-  if filename <> "" && lineno <> -10 && filename <> "cabs loc unknown" then
-    match !diagnostics_format with
-    | Default -> fprintf fmt "%t%s:%d:%t " bc filename lineno rsc
-    | MSVC -> fprintf fmt "%t%s(%d):%t " bc filename lineno rsc
-    | Vi -> fprintf fmt "%t%s +%d:%t " bc filename lineno rsc
-  else
-    fprintf fmt "%tccomp:%t " bc rsc
-
-let error key loc fmt =
-  incr num_errors;
-  kfprintf (pp_key key)
-    err_formatter ("%a%terror:%t %t" ^^ fmt) pp_loc loc rc rsc bc
-
-let fatal_error key loc fmt =
-  incr num_errors;
-  kfprintf
-    (fun fmt -> pp_key key fmt;raise Abort)
-    err_formatter ("%a%terror:%t %t" ^^ fmt) pp_loc loc rc rsc bc
-
-let warning loc ty fmt =
-  let kind,key = classify_warning ty in
-  match kind with
-  | ErrorMsg ->
-      error key loc fmt
-  | FatalErrorMsg ->
-      fatal_error key loc fmt
-  | WarningMsg ->
-      incr num_warnings;
-      kfprintf (pp_key key)
-        err_formatter ("%a%twarning:%t %t" ^^ fmt) pp_loc loc mc rsc bc
-  | SuppressedMsg -> ifprintf err_formatter fmt
-
-let error loc fmt =
-  if !error_fatal || error_limit_reached ()then
-    fatal_error None loc fmt
-  else
-    error None loc fmt
-
-let fatal_error loc fmt =
-  fatal_error None loc fmt
-
-let check_errors () =
-  if !num_errors > 0 then
-    eprintf "@[<hov 0>%d error%s detected.@]@."
-            !num_errors
-            (if !num_errors = 1 then "" else "s");
-  !num_errors > 0
-
-let error_option w =
-  let key = string_of_warning w in
-  [Exact ("-W"^key), Unit (activate_warning w);
-   Exact ("-Wno-"^key), Unit (deactivate_warning w);
-   Exact ("-Werror="^key), Unit (warning_as_error w);
-   Exact ("-Wno-error="^key), Unit ( warning_not_as_error w)]
-
-let warning_options =
-  error_option Unnamed @
-  error_option Unknown_attribute @
-  error_option Zero_length_array @
-  error_option Celeven_extension @
-  error_option Gnu_empty_struct @
-  error_option Missing_declarations @
-  error_option Constant_conversion @
-  error_option Int_conversion @
-  error_option Varargs @
-  error_option Implicit_function_declaration @
-  error_option Pointer_type_mismatch @
-  error_option Compare_distinct_pointer_types @
-  error_option Implicit_int @
-  error_option Main_return_type @
-  error_option Invalid_noreturn @
-  error_option Return_type @
-  error_option Literal_range @
-  error_option Unknown_pragmas @
-  error_option CompCert_conformance @
-  error_option Inline_asm_sdump @
-  error_option Unused_variable @
-  error_option Unused_parameter @
-  [Exact ("-Wfatal-errors"), Set error_fatal;
-   Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
-   Exact ("-fno-diagnostics-color"), Unset color_diagnostics;
-   Exact ("-Werror"), Unit werror;
-   Exact ("-Wall"), Unit wall;
-   Exact ("-w"), Unit wnothing;
-   longopt_int ("-fmax-errors") ((:=) max_error);
-   Exact("-fno-diagnostics-show-option"),Unset diagnostics_show_option;
-   Exact("-fdiagnostics-show-option"),Set diagnostics_show_option;
-   _Regexp("-fdiagnostics-format=\\(ccomp\\|msvc\\|vi\\)"),Self parse_loc_format;
-  ]
-
-let warning_help = {|Diagnostic options:
-  -Wall              Enable all warnings
-  -W<warning>        Enable the specific <warning>
-  -Wno-<warning>     Disable the specific <warning>
-  -Werror            Make all warnings into errors
-  -Werror=<warning>  Turn <warning> into an error
-  -Wno-error=<warning> Turn <warning> into a warning even if -Werror is
-                       specified
-  -Wfatal-errors     Turn all errors into fatal errors aborting the compilation
-  -fdiagnostics-color Turn on colored diagnostics
-  -fno-diagnostics-color Turn of colored diagnostics
-  -fmax-errors=<n>   Maximum number of errors to report
-  -fdiagnostics-show-option Print the option name with mappable diagnostics
-  -fno-diagnostics-show-option Turn of printing of options with mappable
-                               diagnostics
-|}
-
-let raise_on_errors () =
-  if !num_errors > 0 then
-    raise Abort
-
-let crash exn =
-  if Version.buildnr <> "" && Version.tag <> "" then begin
-    let backtrace = Printexc.get_backtrace () in
-    eprintf "%tThis is CompCert, %s, Build:%s, Tag:%s%t\n"
-      bc Version.version Version.buildnr Version.tag rsc;
-    eprintf "Backtrace (please include this in your support request):\n%s"
-      backtrace;
-    eprintf "%tUncaught exception: %s.\n\
-\    Please report this problem to our support.\n\
-\    Error occurred in Build: %s, Tag: %s.\n%t"
-      rc (Printexc.to_string exn) Version.buildnr Version.tag rsc;
-    exit 2
-  end else begin
-    let backtrace = Printexc.get_backtrace ()
-    and exc = Printexc.to_string exn in
-    eprintf "Fatal error: uncaught exception %s\n%s" exc backtrace;
-    exit 2
-  end