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.

8 files changed, 64 insertions, 70 deletions

diff --git a/driver/Assembler.ml b/driver/Assembler.ml
index ba9351ca..1694dfa8 100644
--- a/driver/Assembler.ml
+++ b/driver/Assembler.ml
@@ -18,6 +18,7 @@ open Driveraux
 (* From asm to object file *)
 
 let assemble ifile ofile =
+  Diagnostics.raise_on_errors ();
   let cmd = List.concat [
     Configuration.asm;
     ["-o"; ofile];
@@ -27,8 +28,7 @@ let assemble ifile ofile =
   let exc = command cmd in
   if exc <> 0 then begin
     safe_remove ofile;
-    command_error "assembler" exc;
-    exit 2
+    command_error "assembler" exc
   end
 
 let assembler_actions =
diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index 035c33e0..f139212d 100644
--- a/driver/Commandline.ml
+++ b/driver/Commandline.ml
@@ -35,6 +35,8 @@ type action =
   | Ignore
   | Unit of (unit -> unit)
 
+exception CmdError of string
+
 let match_pattern text = function
   | Exact s ->
       text = s
@@ -72,7 +74,8 @@ let parse_array spec argv first last =
         with Not_found -> find_action s inexact_cases in
       match optact with
       | None ->
-          eprintf "Unknown argument `%s'\n" s; exit 2
+        let msg = sprintf "Unknown argument `%s'" s in
+        raise (CmdError msg)
       | Some(Set r) ->
           r := true; parse (i+1)
       | Some(Unset r) ->
@@ -83,7 +86,8 @@ let parse_array spec argv first last =
           if i + 1 <= last then begin
             fn argv.(i+1); parse (i+2)
           end else begin
-            eprintf "Option `%s' expects an argument\n" s; exit 2
+            let msg = sprintf "Option `%s' expects an argument" s in
+            raise (CmdError msg)
           end
       | Some(Integer fn) ->
           if i + 1 <= last then begin
@@ -91,18 +95,20 @@ let parse_array spec argv first last =
               try
                 int_of_string argv.(i+1)
               with Failure _ ->
-                eprintf "Argument to option `%s' must be an integer\n" s;
-                exit 2
+                let msg = sprintf "Argument to option `%s' must be an integer" s in
+                raise (CmdError msg)
             in
             fn n; parse (i+2)
           end else begin
-            eprintf "Option `%s' expects an argument\n" s; exit 2
+            let msg = sprintf  "Option `%s' expects an argument" s in
+            raise (CmdError msg)
           end
       | Some (Ignore) ->
           if i + 1 <= last then begin
             parse (i+2)
           end else begin
-            eprintf "Option `%s' expects an argument\n" s; exit 2
+            let msg = sprintf "Option `%s' expects an argument" s in
+            raise (CmdError msg)
           end
       | Some (Unit f) -> f (); parse (i+1)
     end
@@ -115,8 +121,7 @@ let parse_cmdline spec =
     argv := expandargv Sys.argv;
     parse_array spec !argv 1 (Array.length !argv - 1)
   with Responsefile.Error s ->
-    eprintf "%s" s;
-    exit 2
+    raise (CmdError s)
 
 let long_int_action key s =
   let ls = String.length s
@@ -126,8 +131,8 @@ let long_int_action key s =
   try
     int_of_string s
   with Failure _ ->
-    eprintf "Argument to option `%s' must be an integer\n" key;
-    exit 2
+    let msg =  sprintf "Argument to option `%s' must be an integer" key in
+    raise (CmdError msg)
 
 let longopt_int key f =
   let act s =
diff --git a/driver/Commandline.mli b/driver/Commandline.mli
index 32f5daf3..e1b917f2 100644
--- a/driver/Commandline.mli
+++ b/driver/Commandline.mli
@@ -35,12 +35,17 @@ type action =
   | Integer of (int -> unit)    (** read next arg as an int, call function *)
   | Ignore                      (** ignore the next arg *)
   | Unit of (unit -> unit)      (** call the function with unit as argument *)
-
-val parse_cmdline: (pattern * action) list -> unit
-
 (* Note on precedence: [Exact] patterns are tried first, then the other
    patterns are tried in the order in which they appear in the list. *)
 
+exception CmdError of string
+(** Raise by [parse_cmdline] when an error occured *)
+
+val parse_cmdline: (pattern * action) list -> unit
+(** [parse_cmdline actions] parses the commandline and performs all [actions].
+    Raises [CmdError] if an error occurred.
+*)
+
 val longopt_int: string -> (int -> unit) -> pattern * action
 (** [longopt_int key fn] generates a pattern and an action for
     options of the form [key=<n>] and calls [fn] with the integer argument
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 063e49d2..9c9f2d79 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -19,6 +19,7 @@ open Driveraux
 open Frontend
 open Assembler
 open Linker
+open Diagnostics
 
 (* Name used for version string etc. *)
 let tool_name = "C verified compiler"
@@ -61,8 +62,8 @@ let compile_c_file sourcename ifile ofile =
     | Errors.OK asm ->
         asm
     | Errors.Error msg ->
-        eprintf "%s: %a" sourcename print_error msg;
-        exit 2 in
+      let loc = file_loc sourcename in
+        fatal_error loc "%a"  print_error msg in
   (* Dump Asm in binary and JSON format *)
   AsmToJSON.print_if asm sourcename;
   (* Print Asm in text form *)
@@ -143,10 +144,8 @@ let process_h_file sourcename =
     ensure_inputfile_exists sourcename;
     preprocess sourcename (output_filename_default "-");
     ""
-  end else begin
-    eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename;
-    exit 2
-  end
+  end else
+    fatal_error no_loc "input file %s ignored (not in -E mode)\n" sourcename
 
 let target_help =
   if Configuration.arch = "arm" && Configuration.model <> "armv6" then
@@ -223,7 +222,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -sdump         Save info for post-linking validation in <file>.json
 |} ^
   general_help ^
-  Cerrors.warning_help ^
+  warning_help ^
   {|Interpreter mode:
   -interp        Execute given .c files using the reference interpreter
   -quiet         Suppress diagnostic messages for the interpreter
@@ -237,10 +236,9 @@ let print_usage_and_exit () =
 
 let enforce_buildnr nr =
   let build = int_of_string Version.buildnr in
-  if nr != build then begin
-    eprintf "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\
-Please use matching builds of QSK and CompCert.\n" build nr; exit 2
-  end
+  if nr != build then
+    fatal_error no_loc "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\
+Please use matching builds of QSK and CompCert." build nr
 
 let dump_mnemonics destfile =
   let oc = open_out_bin destfile in
@@ -349,7 +347,7 @@ let cmdline_actions =
 (* General options *)
    general_options @
 (* Diagnostic options *)
-  Cerrors.warning_options @
+  warning_options @
 (* Interpreter mode *)
  [ Exact "-interp", Set option_interp;
   Exact "-quiet", Unit (fun () -> Interp.trace := 0);
@@ -371,7 +369,7 @@ let cmdline_actions =
   @ [
 (* Catch options that are not handled *)
   Prefix "-", Self (fun s ->
-      eprintf "Unknown option `%s'\n" s; exit 2);
+      fatal_error no_loc "Unknown option `%s'" s);
 (* File arguments *)
   Suffix ".c", Self (fun s ->
       push_action process_c_file s; incr num_source_files; incr num_input_files);
@@ -405,21 +403,17 @@ let _ =
     Frontend.init ();
     parse_cmdline cmdline_actions;
     DebugInit.init (); (* Initialize the debug functions *)
-    if nolink () && !option_o <> None && !num_source_files >= 2 then begin
-      eprintf "Ambiguous '-o' option (multiple source files)\n";
-      exit 2
-    end;
+    if nolink () && !option_o <> None && !num_source_files >= 2 then
+      fatal_error no_loc "Ambiguous '-o' option (multiple source files)";
     if !num_input_files = 0 then
-      begin
-        eprintf "ccomp: error: no input file\n";
-        exit 2
-      end;
+      fatal_error no_loc "no input file";
     let linker_args = time "Total compilation time" perform_actions () in
     if not (nolink ()) && linker_args <> [] then begin
       linker (output_filename_default "a.out") linker_args
     end;
-   if  Cerrors.check_errors () then exit 2
-  with Sys_error msg ->
-    eprintf "I/O error: %s.\n" msg; exit 2
-     | e ->
-       Cerrors.crash e
+    check_errors ()
+  with
+  | Sys_error msg
+  | CmdError msg -> error no_loc "%s" msg; exit 2
+  | Abort -> exit 2
+  | e -> crash e
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 6d8d0adc..ccc3d00d 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -13,6 +13,7 @@
 
 open Printf
 open Clflags
+open Diagnostics
 
 (* Safe removal of files *)
 let safe_remove file =
@@ -46,9 +47,9 @@ let command stdout args =
     match status with
     | Unix.WEXITED rc -> rc
     | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
+        error no_loc "Command '%s' killed on a signal." argv.(0); -1
   with Unix.Unix_error(err, fn, param) ->
-    eprintf "Error executing '%s': %s: %s %s\n"
+    error no_loc "executing '%s': %s: %s %s"
             argv.(0) fn (Unix.error_message err) param;
     -1
 
@@ -81,7 +82,7 @@ let command ?stdout args =
     command stdout args
 
 let command_error n exc =
-  eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc
+  fatal_error no_loc "%s command failed with exit code %d (use -v to see invocation)\n" n exc
 
 
 (* Determine names for output files.  We use -o option if specified
@@ -105,20 +106,18 @@ let output_filename_default default_file =
 (* All input files should exist *)
 
 let ensure_inputfile_exists name =
-  if not (Sys.file_exists name) then begin
-    eprintf "error: no such file or directory: '%s'\n" name;
-    exit 2
-  end
+  if not (Sys.file_exists name) then
+    fatal_error no_loc "no such file or directory: '%s'" name
+
 (* Printing of error messages *)
 
-let print_error oc msg =
+let print_error pp msg =
   let print_one_error = function
-  | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
-  | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
-  | Errors.POS i -> fprintf oc "%ld" (Camlcoq.P.to_int32 i)
+  | Errors.MSG s -> Format.pp_print_string pp (Camlcoq.camlstring_of_coqstring s)
+  | Errors.CTX i -> Format.pp_print_string pp (Camlcoq.extern_atom i)
+  | Errors.POS i -> Format.fprintf pp "%ld" (Camlcoq.P.to_int32 i)
   in
-    List.iter print_one_error msg;
-    output_char oc '\n'
+  List.iter print_one_error msg
 
 (* Command-line parsing *)
 let explode_comma_option s =
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli
index 51333b2a..6f0eaddb 100644
--- a/driver/Driveraux.mli
+++ b/driver/Driveraux.mli
@@ -16,7 +16,7 @@ val command: ?stdout:string -> string list -> int
     (** Execute the command with the given arguments and an optional file for
         the stdout. Returns the exit code. *)
 
-val command_error: string -> int -> unit
+val command_error: string -> int -> 'a
    (** Generate an error message for the given command and exit code *)
 
 val safe_remove: string -> unit
@@ -38,7 +38,7 @@ val output_filename_default: string -> string
 val ensure_inputfile_exists: string -> unit
    (** Test whether the given input file exists *)
 
-val print_error:out_channel -> Errors.errcode list -> unit
+val print_error:Format.formatter -> Errors.errcode list -> unit
    (** Printing of error messages *)
 
 val explode_comma_option: string -> string list
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 2b9d5860..2bc4f844 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -14,7 +14,6 @@
 open Clflags
 open Commandline
 open Driveraux
-open Printf
 
 (* Common frontend functions between clightgen and ccomp *)
 
@@ -22,6 +21,7 @@ open Printf
 (* From C to preprocessed C *)
 
 let preprocess ifile ofile =
+  Diagnostics.raise_on_errors ();
   let output =
     if ofile = "-" then None else Some ofile in
   let cmd = List.concat [
@@ -37,8 +37,6 @@ let preprocess ifile ofile =
   if exc <> 0 then begin
     if ofile <> "-" then safe_remove ofile;
     command_error "preprocessor" exc;
-    eprintf "Error during preprocessing.\n";
-    exit 2
   end
 
 (* From preprocessed C to Csyntax *)
@@ -54,18 +52,11 @@ let parse_c_file sourcename ifile =
   ^ (if !option_fpacked_structs then "p" else "")
   in
   (* Parsing and production of a simplified C AST *)
-  let ast =
-    match Parse.preprocessed_file simplifs sourcename ifile with
-    | None -> exit 2
-    | Some p -> p in
+  let ast = Parse.preprocessed_file simplifs sourcename ifile in
   (* Save C AST if requested *)
   Cprint.print_if ast;
   (* Conversion to Csyntax *)
-  let csyntax =
-    match Timing.time "CompCert C generation" C2C.convertProgram ast with
-    | None -> exit 2
-    | Some p -> p in
-  flush stderr;
+  let csyntax = Timing.time "CompCert C generation" C2C.convertProgram ast in
   (* Save CompCert C AST if requested *)
   PrintCsyntax.print_if csyntax;
   csyntax
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 37a5cde0..6e6ad6b4 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -19,6 +19,7 @@ open Driveraux
 (* Linking *)
 
 let linker exe_name files =
+  Diagnostics.raise_on_errors ();
   let cmd = List.concat [
     Configuration.linker;
     ["-o"; exe_name];
@@ -29,8 +30,7 @@ let linker exe_name files =
   ] in
   let exc = command cmd in
   if exc <> 0 then begin
-    command_error "linker" exc;
-    exit 2
+    command_error "linker" exc
   end