diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-02-08 16:38:54 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-02-08 16:38:54 +0100 |
commit | f02f00a01b598567f70e138c144d9581973802e6 (patch) | |
tree | db15b2ad60692f936435cdd784e7bb7f6a977a40 /driver | |
parent | 54fa98c3833091a75d0c1afe84b42afc35452fe3 (diff) | |
download | compcert-f02f00a01b598567f70e138c144d9581973802e6.tar.gz compcert-f02f00a01b598567f70e138c144d9581973802e6.zip |
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.
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Assembler.ml | 4 | ||||
-rw-r--r-- | driver/Commandline.ml | 25 | ||||
-rw-r--r-- | driver/Commandline.mli | 11 | ||||
-rw-r--r-- | driver/Driver.ml | 46 | ||||
-rw-r--r-- | driver/Driveraux.ml | 25 | ||||
-rw-r--r-- | driver/Driveraux.mli | 4 | ||||
-rw-r--r-- | driver/Frontend.ml | 15 | ||||
-rw-r--r-- | driver/Linker.ml | 4 |
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 |