From f02f00a01b598567f70e138c144d9581973802e6 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Feb 2018 16:38:54 +0100 Subject: 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. --- arm/AsmToJSON.ml | 2 +- cfrontend/C2C.ml | 35 ++-- cfrontend/CPragmas.ml | 2 +- cparser/Bitfields.ml | 2 +- cparser/Cerrors.ml | 430 --------------------------------------------- cparser/Cerrors.mli | 80 --------- cparser/Checks.ml | 2 +- cparser/Cutil.ml | 2 +- cparser/Diagnostics.ml | 437 ++++++++++++++++++++++++++++++++++++++++++++++ cparser/Diagnostics.mli | 86 +++++++++ cparser/Elab.ml | 4 +- cparser/ExtendedAsm.ml | 4 +- cparser/Lexer.mll | 10 +- cparser/PackedStructs.ml | 2 +- cparser/Parse.ml | 15 +- cparser/Parse.mli | 2 +- cparser/Rename.ml | 2 +- cparser/Unblock.ml | 3 +- driver/Assembler.ml | 4 +- driver/Commandline.ml | 25 +-- driver/Commandline.mli | 11 +- driver/Driver.ml | 46 +++-- driver/Driveraux.ml | 25 ++- driver/Driveraux.mli | 4 +- driver/Frontend.ml | 15 +- driver/Linker.ml | 4 +- exportclight/Clightgen.ml | 33 ++-- powerpc/AsmToJSON.ml | 2 +- 28 files changed, 649 insertions(+), 640 deletions(-) delete mode 100644 cparser/Cerrors.ml delete mode 100644 cparser/Cerrors.mli create mode 100644 cparser/Diagnostics.ml create mode 100644 cparser/Diagnostics.mli diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index fadcdf58..49cca929 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -154,7 +154,7 @@ let pp_instructions pp ic = begin match ef with | EF_inline_asm _ -> instruction pp "Pinlineasm" [Id]; - Cerrors.warning ("", -10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" + Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump") | EF_annot (kind,txt, targs) -> let annot_string = PrintAsmaux.annot_text TargetPrinter.preg_annot "r1" (camlstring_of_coqstring txt) args in let len = String.length annot_string in diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 743ffd3b..6a2c6a4e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -120,13 +120,16 @@ let currentLocation = ref Cutil.no_loc let updateLoc l = currentLocation := l let error fmt = - Cerrors.error !currentLocation fmt + Diagnostics.error !currentLocation fmt + +let fatal_error fmt = + Diagnostics.fatal_error !currentLocation fmt let unsupported msg = - Cerrors.error !currentLocation "unsupported feature: %s" msg + Diagnostics.error !currentLocation "unsupported feature: %s" msg let warning t msg = - Cerrors.warning !currentLocation t msg + Diagnostics.warning !currentLocation t msg let string_of_errmsg msg = let string_of_err = function @@ -657,11 +660,11 @@ let checkFloatOverflow f typ = match f with | Fappli_IEEE.B754_finite _ -> () | Fappli_IEEE.B754_zero _ -> - warning Cerrors.Literal_range "magnitude of floating-point constant too small for type '%s'" typ + warning Diagnostics.Literal_range "magnitude of floating-point constant too small for type '%s'" typ | Fappli_IEEE.B754_infinity _ -> - warning Cerrors.Literal_range "magnitude of floating-point constant too large for type '%s'" typ + warning Diagnostics.Literal_range "magnitude of floating-point constant too large for type '%s'" typ | Fappli_IEEE.B754_nan _ -> - warning Cerrors.Literal_range "floating-point converts converts to 'NaN'" + warning Diagnostics.Literal_range "floating-point converts converts to 'NaN'" let convertFloat f kind = let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in @@ -783,7 +786,7 @@ let rec convertExpr env e = let e2' = convertExpr env e2 in if Cutil.is_composite_type env e1.etyp && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then - warning Cerrors.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored"; + warning Diagnostics.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored"; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| @@ -1080,7 +1083,7 @@ let rec convertStmt env s = | _ -> Cutil.is_debug_stmt s in if init.sdesc <> C.Sskip && not (init_debug init) then begin - warning Cerrors.Unnamed "ignored code at beginning of 'switch'"; + warning Diagnostics.Unnamed "ignored code at beginning of 'switch'"; contains_case init end; let te = convertExpr env e in @@ -1276,7 +1279,7 @@ let rec convertGlobdecls env res gl = begin match Cutil.unroll env ty with | TFun(tres, targs, va, a) -> if targs = None then - warning Cerrors.Unnamed "'%s' is declared without a function prototype" id.name; + warning Diagnostics.Unnamed "'%s' is declared without a function prototype" id.name; convertGlobdecls env (convertFundecl env d :: res) gl' | _ -> convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl' @@ -1290,7 +1293,7 @@ let rec convertGlobdecls env res gl = convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then - warning Cerrors.Unknown_pragmas "unknown pragma ignored"; + warning Diagnostics.Unknown_pragmas "unknown pragma ignored"; convertGlobdecls env res gl' (** Convert struct and union declarations. @@ -1388,7 +1391,7 @@ let public_globals gl = (** Convert a [C.program] into a [Csyntax.program] *) let convertProgram p = - Cerrors.reset(); + Diagnostics.reset(); stringNum := 0; Hashtbl.clear decl_atom; Hashtbl.clear stringTable; @@ -1399,9 +1402,8 @@ let convertProgram p = let typs = convertCompositedefs env [] p in match build_composite_env typs with | Errors.Error msg -> - error "incorrect struct or union definition: %s" - (string_of_errmsg msg); - None + fatal_error "incorrect struct or union definition: %s" + (string_of_errmsg msg) | Errors.OK ce -> comp_env := ce; let gl1 = convertGlobdecls env [] p in @@ -1413,6 +1415,7 @@ let convertProgram p = prog_main = intern_string "main"; prog_types = typs; prog_comp_env = ce } in - if Cerrors.check_errors () then None else Some p' + Diagnostics.check_errors (); + p' with Env.Error msg -> - error "%s" (Env.error_message msg); None + fatal_error "%s" (Env.error_message msg) diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index d61af920..44660718 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -72,7 +72,7 @@ let process_pragma name = | "section" :: _ -> C2C.error "ill-formed `section' pragma"; true | "use_section" :: classname :: identlist -> - if identlist = [] then C2C.warning Cerrors.Unnamed "empty `use_section' pragma"; + if identlist = [] then C2C.warning Diagnostics.Unnamed "empty `use_section' pragma"; List.iter (process_use_section_pragma classname) identlist; true | "use_section" :: _ -> diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 35da5d4e..e0dccbd2 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -66,7 +66,7 @@ let is_signed_enum_bitfield env sid fld eid n = else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members then true else begin - Cerrors.warning Cutil.no_loc Cerrors.Unnamed + Diagnostics.warning Diagnostics.no_loc Diagnostics.Unnamed "not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.C.name fld sid.C.name n; false 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 "@[%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 Enable the specific - -Wno- Disable the specific - -Werror Make all warnings into errors - -Werror= Turn into an error - -Wno-error= Turn 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= 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 diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli deleted file mode 100644 index c351443c..00000000 --- a/cparser/Cerrors.mli +++ /dev/null @@ -1,80 +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. *) -(* *) -(* *********************************************************************) - -(* Printing of warnings and error messages *) - -val reset : unit -> unit - (** Reset the error counters. *) - -exception Abort - (** Exception raised upon fatal errors *) - -val check_errors : unit -> bool - (** Check whether errors occured *) - -type warning_type = - | Unnamed (** warnings which cannot be turned off *) - | Unknown_attribute (** usage of unsupported/unknown attributes *) - | Zero_length_array (** gnu extension for zero lenght arrays *) - | Celeven_extension (** C11 features *) - | Gnu_empty_struct (** gnu extension for empty struct *) - | Missing_declarations (** declation which do not declare anything *) - | Constant_conversion (** dangerous constant conversions *) - | Int_conversion (** pointer <-> int conversions *) - | Varargs (** promotable vararg argument *) - | Implicit_function_declaration (** deprecated implicit function declaration *) - | Pointer_type_mismatch (** pointer type mismatch in ?: operator *) - | Compare_distinct_pointer_types (** comparison between different pointer types *) - | Implicit_int (** implict int parameter or return type *) - | Main_return_type (** wrong return type for main *) - | Invalid_noreturn (** noreturn function containing return *) - | Return_type (** void return in non-void function *) - | Literal_range (** literal ranges *) - | Unknown_pragmas (** unknown/unsupported pragma *) - | CompCert_conformance (** features that are not part of the CompCert C core language *) - | Inline_asm_sdump (** inline assembler used in combination of sdump *) - | Unused_variable (** unused local variables *) - | Unused_parameter (** unused function parameter *) - -val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -(** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to - the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] - and warning key for [w] *) - -val error : (string * int) -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -(** [error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to - the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] - and warning key for [w]. *) - -val fatal_error : (string * int) -> ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a -(** [fatal_error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to - the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] - and warning key for [w]. Additionally raises the excpetion [Abort] after printing the error message *) - -val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a -(** [fatal_error_raw] is identical to fatal_error, except it uses [Printf] and does not automatically - introduce indentation *) - -val warning_help : string -(** Help string for all warning options *) - -val warning_options : (Commandline.pattern * Commandline.action) list -(** List of all options for diagnostics *) - -val raise_on_errors : unit -> unit -(** Raise [Abort] if an error was encountered *) - -val crash: exn -> unit -(** Report the backtrace of the last exception and exit *) diff --git a/cparser/Checks.ml b/cparser/Checks.ml index 073d1057..ee36e226 100644 --- a/cparser/Checks.ml +++ b/cparser/Checks.ml @@ -14,7 +14,7 @@ (* *********************************************************************) open C -open Cerrors +open Diagnostics open Cutil open Env diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 9bc11141..71c253f8 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -15,7 +15,7 @@ (* Operations on C types and abstract syntax *) -open Cerrors +open Diagnostics open C open Env open Machine diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml new file mode 100644 index 00000000..d9b96393 --- /dev/null +++ b/cparser/Diagnostics.ml @@ -0,0 +1,437 @@ +(* *********************************************************************) +(* *) +(* 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) = + let lineno = if lineno = -10 then "" else + match !diagnostics_format with + | Default -> sprintf ":%d" lineno + | MSVC -> sprintf "(%d)" lineno + | Vi -> sprintf " +%d" lineno in + if filename <> "" && filename <> "cabs loc unknown" then + fprintf fmt "%t%s%s:%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 begin + eprintf "@[%d error%s detected.@]@." + !num_errors + (if !num_errors = 1 then "" else "s"); + raise Abort + end + +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 Enable the specific + -Wno- Disable the specific + -Werror Make all warnings into errors + -Werror= Turn into an error + -Wno-error= Turn 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= 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 + +let no_loc = ("", -1) + +let file_loc file = (file,-10) diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli new file mode 100644 index 00000000..54395136 --- /dev/null +++ b/cparser/Diagnostics.mli @@ -0,0 +1,86 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Printing of warnings and error messages *) + +val reset : unit -> unit + (** Reset the error counters. *) + +exception Abort + (** Exception raised upon fatal errors *) + +val check_errors : unit -> unit + (** Check whether errors occured and raise abort if an error occured *) + +type warning_type = + | Unnamed (** warnings which cannot be turned off *) + | Unknown_attribute (** usage of unsupported/unknown attributes *) + | Zero_length_array (** gnu extension for zero lenght arrays *) + | Celeven_extension (** C11 features *) + | Gnu_empty_struct (** gnu extension for empty struct *) + | Missing_declarations (** declation which do not declare anything *) + | Constant_conversion (** dangerous constant conversions *) + | Int_conversion (** pointer <-> int conversions *) + | Varargs (** promotable vararg argument *) + | Implicit_function_declaration (** deprecated implicit function declaration *) + | Pointer_type_mismatch (** pointer type mismatch in ?: operator *) + | Compare_distinct_pointer_types (** comparison between different pointer types *) + | Implicit_int (** implict int parameter or return type *) + | Main_return_type (** wrong return type for main *) + | Invalid_noreturn (** noreturn function containing return *) + | Return_type (** void return in non-void function *) + | Literal_range (** literal ranges *) + | Unknown_pragmas (** unknown/unsupported pragma *) + | CompCert_conformance (** features that are not part of the CompCert C core language *) + | Inline_asm_sdump (** inline assembler used in combination of sdump *) + | Unused_variable (** unused local variables *) + | Unused_parameter (** unused function parameter *) + +val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +(** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w] *) + +val error : (string * int) -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +(** [error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w]. *) + +val fatal_error : (string * int) -> ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a +(** [fatal_error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w]. Additionally raises the excpetion [Abort] after printing the error message *) + +val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a +(** [fatal_error_raw] is identical to fatal_error, except it uses [Printf] and does not automatically + introduce indentation *) + +val warning_help : string +(** Help string for all warning options *) + +val warning_options : (Commandline.pattern * Commandline.action) list +(** List of all options for diagnostics *) + +val raise_on_errors : unit -> unit +(** Raise [Abort] if an error was encountered *) + +val crash: exn -> unit +(** Report the backtrace of the last exception and exit *) + +val no_loc : string * int +(** Location used for unknown locations *) + +val file_loc : string -> string * int +(** [file_loc f] generates a location for file [f] *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 86e71865..4de43fe0 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -20,8 +20,8 @@ open Machine open Cabs open C -open Cerrors -open Cutil +open Diagnostics +open !Cutil (** * Utility functions *) diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 30d1a0cc..6cd95aec 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -33,7 +33,7 @@ open Printf open Machine open C open Cutil -open Cerrors +open Diagnostics (* Renaming of labeled and numbered operands *) @@ -176,7 +176,7 @@ let rename_placeholders loc template subst = try StringMap.find p subst with Not_found -> - error loc"'%s' in asm text does not designate any operand" p; + error loc "'%s' in asm text does not designate any operand" p; "%" in Str.global_substitute re_asm_placeholder diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index ec344f7a..cf8788c5 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -126,16 +126,16 @@ let currentLoc = (* Error reporting *) let fatal_error lb fmt = - Cerrors.fatal_error + Diagnostics.fatal_error (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let error lb fmt = - Cerrors.error + Diagnostics.error (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let warning lb fmt = - Cerrors.warning - (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Cerrors.Unnamed ("warning: " ^^ fmt) + Diagnostics.warning + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Diagnostics.Unnamed ("warning: " ^^ fmt) (* Simple character escapes *) @@ -483,7 +483,7 @@ and singleline_comment = parse and supplier = I.lexer_lexbuf_to_supplier lexer lexbuf and succeed () = () and fail checkpoint = - Cerrors.fatal_error_raw "%s" (ErrorReports.report text !buffer checkpoint) + Diagnostics.fatal_error_raw "%s" (ErrorReports.report text !buffer checkpoint) in I.loop_handle succeed fail supplier checkpoint diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index b74a29d4..e1287eb8 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -23,7 +23,7 @@ open Machine open C open Cutil open Env -open Cerrors +open Diagnostics open Transform (* The set of struct fields that are byte-swapped. diff --git a/cparser/Parse.ml b/cparser/Parse.ml index ecd13332..8665e158 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -46,7 +46,7 @@ let read_file sourcefile = text let preprocessed_file transfs name sourcefile = - Cerrors.reset(); + Diagnostics.reset(); (* Reading the whole file at once may seem costly, but seems to be the simplest / most robust way of accessing the text underlying a range of positions. This is used when printing an error message. @@ -55,7 +55,6 @@ let preprocessed_file transfs name sourcefile = on my machine. *) let text = read_file sourcefile in let p = - try let t = parse_transformations transfs in let rec inf = Datatypes.S inf in let ast : Cabs.definition list = @@ -70,13 +69,11 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies between grammars. *) - Cerrors.fatal_error Cutil.no_loc "Internal error while parsing" + Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing" | Parser.Parser.Inter.Timeout_pr -> assert false | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in let p1 = Timing.time "Elaboration" Elab.elab_file ast in - Cerrors.raise_on_errors (); - Timing.time2 "Emulations" transform_program t p1 name - with - | Cerrors.Abort -> - [] in - if Cerrors.check_errors() then None else Some p + Diagnostics.check_errors (); + Timing.time2 "Emulations" transform_program t p1 name in + Diagnostics.check_errors(); + p diff --git a/cparser/Parse.mli b/cparser/Parse.mli index 58c3cfb9..433e2e73 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -15,7 +15,7 @@ (* Entry point for the library: parse, elaborate, and transform *) -val preprocessed_file: string -> string -> string -> C.program option +val preprocessed_file: string -> string -> string -> C.program (* first arg: desired transformations second arg: source file name before preprocessing diff --git a/cparser/Rename.ml b/cparser/Rename.ml index f402ea39..cdb5751e 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -83,7 +83,7 @@ let ident env id = try IdentMap.find id env.re_id with Not_found -> - Cerrors.fatal_error no_loc "internal error: rename: %s__%d unbound" + Diagnostics.fatal_error Diagnostics.no_loc "internal error: rename: %s__%d unbound" id.name id.stamp let rec typ env = function diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 91e2ce20..5df2e2cf 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -20,7 +20,6 @@ open C open Cutil -open Cerrors (* Convert an initializer to a list of assignment expressions. *) @@ -32,7 +31,7 @@ let rec local_initializer env path init k = let (ty_elt, sz) = match unroll env path.etyp with | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) - | _ -> fatal_error no_loc "Wrong type for array initializer" in + | _ -> Diagnostics.fatal_error Diagnostics.no_loc "Wrong type for array initializer" in let rec array_init pos il = if pos >= sz then k else begin let (i1, il') = 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=] 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- to turn off -f) -sdump Save info for post-linking validation in .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 diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 2878cb17..9cb0674e 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -19,6 +19,7 @@ open Clflags open CommonOptions open Driveraux open Frontend +open Diagnostics let tool_name = "Clight generator" @@ -29,6 +30,7 @@ let option_normalize = ref false (* From CompCert C AST to Clight *) let compile_c_ast sourcename csyntax ofile = + let loc = file_loc sourcename in let clight = match SimplExpr.transl_program csyntax with | Errors.OK p -> @@ -38,12 +40,10 @@ let compile_c_ast sourcename csyntax ofile = then Clightnorm.norm_program p' else p' | Errors.Error msg -> - print_error stderr msg; - exit 2 + fatal_error loc "%a" print_error msg end | Errors.Error msg -> - print_error stderr msg; - exit 2 in + fatal_error loc "%a" print_error msg in (* Dump Clight in C syntax if requested *) if !option_dclight then begin let ofile = Filename.chop_suffix sourcename ".c" ^ ".light.c" in @@ -104,7 +104,8 @@ language_support_help ^ -dclight Save generated Clight in .light.c |} ^ general_help ^ - Cerrors.warning_help + warning_help + let print_usage_and_exit () = printf "%s" usage_string; exit 0 @@ -145,11 +146,11 @@ let cmdline_actions = Exact "-dclight", Set option_dclight;] @ general_options (* Diagnostic options *) - @ Cerrors.warning_options + @ warning_options @ language_support_options @ (* 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 -> incr num_input_files; push_action process_c_file s); @@ -160,6 +161,7 @@ let cmdline_actions = ] let _ = + try Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288; (* 512k *) Gc.major_heap_increment = 4194304 (* 4M *) @@ -167,12 +169,13 @@ let _ = Printexc.record_backtrace true; Frontend.init (); parse_cmdline cmdline_actions; - if !option_o <> None && !num_input_files >= 2 then begin - eprintf "Ambiguous '-o' option (multiple source files)\n"; - exit 2 - end; - if !num_input_files = 0 then begin - eprintf "clightgen: error: no input file\n"; - exit 2 - end; + if !option_o <> None && !num_input_files >= 2 then + fatal_error no_loc "Ambiguous '-o' option (multiple source files)"; + if !num_input_files = 0 then + fatal_error no_loc "no input file"; perform_actions () + with + | Sys_error msg + | CmdError msg -> error no_loc "%s" msg; exit 2 + | Abort -> exit 2 + | e -> crash e diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 5baed5dc..7c4c8f8a 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -340,7 +340,7 @@ let pp_instructions pp ic = begin match ef with | EF_inline_asm _ -> instruction pp "Pinlineasm" [Id]; - Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" + Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump") | EF_annot (kind,txt,targs) -> let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in let len = String.length annot_string in -- cgit