diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | Makefile.extr | 3 | ||||
| -rwxr-xr-x | configure | 6 | ||||
| -rw-r--r-- | cparser/Cerrors.ml | 6 | ||||
| -rw-r--r-- | cparser/Cerrors.mli | 1 | ||||
| -rw-r--r-- | cparser/Elab.ml | 7 | ||||
| -rw-r--r-- | cparser/Parse.ml | 1 | ||||
| -rw-r--r-- | driver/Commandline.ml | 8 | ||||
| -rw-r--r-- | driver/Configuration.ml | 12 | ||||
| -rw-r--r-- | driver/Configuration.mli | 8 | ||||
| -rw-r--r-- | driver/Driver.ml | 1 | ||||
| -rw-r--r-- | driver/Driveraux.ml | 34 | ||||
| -rw-r--r-- | driver/Driveraux.mli | 2 | ||||
| -rw-r--r-- | driver/Interp.ml | 6 | ||||
| -rw-r--r-- | lib/Responsefile.mli | 31 | ||||
| -rw-r--r-- | lib/Responsefile.mll | 120 |
17 files changed, 235 insertions, 15 deletions
@@ -52,6 +52,7 @@ cparser/tests/generated/*.err backend/CMparser.automaton lib/Readconfig.ml lib/Tokenize.ml +lib/Responsefile.ml driver/Version.ml # Documentation doc/coq2html @@ -208,7 +208,8 @@ compcert.ini: Makefile.config echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \ echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ echo "struct_passing_style=$(STRUCT_PASSING)"; \ - echo "struct_return_style=$(STRUCT_RETURN)";) \ + echo "struct_return_style=$(STRUCT_RETURN)"; \ + echo "response_file_style=$(RESPONSEFILE)";) \ > compcert.ini driver/Version.ml: VERSION diff --git a/Makefile.extr b/Makefile.extr index 51dbd767..8fdc9ffe 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -63,7 +63,8 @@ MODORDER=tools/modorder .depend.extr PARSERS=backend/CMparser.mly cparser/pre_parser.mly LEXERS=backend/CMlexer.mll cparser/Lexer.mll \ - lib/Tokenize.mll lib/Readconfig.mll + lib/Tokenize.mll lib/Readconfig.mll \ + lib/Responsefile.mll LIBS=str.cmxa unix.cmxa $(MENHIR_LIBS) LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS))) @@ -20,6 +20,7 @@ target='' has_runtime_lib=true has_standard_headers=true clightgen=false +responsefile="gnu" usage='Usage: ./configure [options] target @@ -218,6 +219,7 @@ if test "$arch" = "powerpc"; then libmath="-lm" struct_passing="ref-caller" system="diab" + responsefile="diab" ;; *) abi="eabi" @@ -470,6 +472,7 @@ MODEL=$model STRUCT_PASSING=$struct_passing STRUCT_RETURN=$struct_return SYSTEM=$system +RESPONSEFILE=$responsefile EOF else cat >> Makefile.config <<'EOF' @@ -563,6 +566,9 @@ ASM_SUPPORTS_CFI=false # Turn on/off compilation of clightgen CLIGHTGEN=false +# Whether the other tools support responsefiles in gnu syntax +RESPONSEFILE="none" + EOF fi diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 5c077f37..a4d1a3f8 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -30,7 +30,7 @@ exception Abort 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 @@ -67,4 +67,6 @@ let check_errors () = (if !num_warnings = 1 then "" else "s"); !num_errors > 0 || (!warn_error && !num_warnings > 0) - +let raise_on_errors () = + if !num_errors > 0 || (!warn_error && !num_warnings > 0) then + raise Abort diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index 3e315fad..313573c3 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -22,3 +22,4 @@ val error : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val warning : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val info : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val check_errors : unit -> bool +val raise_on_errors : unit -> unit diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 76f8efdb..8cd7ed64 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -433,6 +433,7 @@ let elab_attribute env = function begin match elab_attr_arg loc env a with | AInt n when is_power_of_two n -> [AAlignas (Int64.to_int n)] | _ -> warning loc "bad _Alignas value, ignored"; [] + | exception Wrong_attr_arg -> warning loc "bad _Alignas value, ignored"; [] end | ALIGNAS_ATTR (_, loc) -> warning loc "_Alignas takes exactly one parameter, ignored"; [] @@ -812,7 +813,11 @@ and elab_struct_or_union_info kind loc env members attrs = check_incomplete m; (* Warn for empty structs or unions *) if m = [] then - warning loc "empty %s" (if kind = Struct then "struct" else "union"); + if kind = Struct then begin + warning loc "empty struct" + end else begin + fatal_error loc "empty union" + end; (composite_info_def env' kind attrs m, env') and elab_struct_or_union only kind loc tag optmembers attrs env = diff --git a/cparser/Parse.ml b/cparser/Parse.ml index c125e653..3f60ebb4 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -74,6 +74,7 @@ let preprocessed_file transfs name sourcefile = | 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 -> diff --git a/driver/Commandline.ml b/driver/Commandline.ml index 0a2c8fca..d125736a 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -16,6 +16,7 @@ (* Parsing of command-line flags and arguments *) open Printf +open Responsefile type pattern = | Exact of string @@ -99,4 +100,9 @@ let parse_array spec argv first last = in parse first let parse_cmdline spec = - parse_array spec Sys.argv 1 (Array.length Sys.argv - 1) + try + let argv = expandargv Sys.argv in + parse_array spec argv 1 (Array.length argv - 1) + with Responsefile.Error s -> + eprintf "%s" s; + exit 2 diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 765b075a..87e29e0f 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -176,3 +176,15 @@ let struct_return_style = | "int1-8" -> SR_int1to8 | "ref" -> SR_ref | v -> bad_config "struct_return_style" [v] + +type response_file_style = + | Gnu (* responsefiles in gnu compatible syntax *) + | Diab (* responsefiles in diab compatible syntax *) + | Unsupported (* responsefiles are not supported *) + +let response_file_style = + match get_config_string "response_file_style" with + | "unsupported" -> Unsupported + | "gnu" -> Gnu + | "diab" -> Diab + | v -> bad_config "response_file_style" [v] diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 4b9c64a9..197e8ad2 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -66,3 +66,11 @@ val struct_passing_style: struct_passing_style val struct_return_style: struct_return_style (** Calling conventions to use for returning structs and unions as first-class values *) + +type response_file_style = + | Gnu (* responsefiles in gnu compatible syntax *) + | Diab (* responsefiles in diab compatible syntax *) + | Unsupported (* responsefiles are not supported *) + +val response_file_style: response_file_style + (** Style of supported responsefiles *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 9c07dba1..0bfc7167 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -341,6 +341,7 @@ General options:\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ \ -version Print the version string and exit\n\ +\ @<file> Read command line options from <file>\n\ Interpreter mode:\n\ \ -interp Execute given .c files using the reference interpreter\n\ \ -quiet Suppress diagnostic messages for the interpreter\n\ diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 3fe22fac..33cd9215 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -14,13 +14,20 @@ open Printf open Clflags +(* Is this a gnu based tool chain *) +let gnu_system = Configuration.system <> "diab" + +(* Safe removal of files *) +let safe_remove file = + try Sys.remove file with Sys_error _ -> () + (* Invocation of external tools *) let rec waitpid_no_intr pid = try Unix.waitpid [] pid with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid -let command ?stdout args = +let command stdout args = if !option_v then begin eprintf "+ %s" (String.concat " " args); begin match stdout with @@ -51,12 +58,29 @@ let command ?stdout args = argv.(0) fn (Unix.error_message err) param; -1 +let command ?stdout args = + let resp = Sys.win32 && Configuration.response_file_style <> Configuration.Unsupported in + if resp && List.fold_left (fun len arg -> len + String.length arg + 1) 0 args > 7000 then + let quote,prefix = match Configuration.response_file_style with + | Configuration.Unsupported -> assert false + | Configuration.Gnu -> Responsefile.gnu_quote,"@" + | Configuration.Diab -> Responsefile.diab_quote,"-@" in + let file,oc = Filename.open_temp_file "compcert" "" in + let cmd,args = match args with + | cmd::args -> cmd,args + | [] -> assert false (* Should never happen *) in + List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args; + close_out oc; + let arg = prefix^file in + let ret = command stdout [cmd;arg] in + safe_remove file; + ret + else + 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 -let safe_remove file = - try Sys.remove file with Sys_error _ -> () - (* Determine names for output files. We use -o option if specified and if this is the final destination file (not a dump file). @@ -94,8 +118,6 @@ let print_error oc msg = List.iter print_one_error msg; output_char oc '\n' -let gnu_system = Configuration.system <> "diab" - (* Command-line parsing *) let explode_comma_option s = match Str.split (Str.regexp ",") s with diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 60efcc80..e6bac6e3 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -12,7 +12,7 @@ (* *********************************************************************) -val command: ?stdout:string -> string list -> int +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. *) diff --git a/driver/Interp.ml b/driver/Interp.ml index 5c2158ae..f42bed32 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -387,10 +387,12 @@ let do_external_function id sg ge w args m = match camlstring_of_coqstring id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> - print_string (do_printf m fmt args'); + let fmt' = do_printf m fmt args' in + let len = coqint_of_camlint (Int32.of_int (String.length fmt')) in + print_string fmt'; flush stdout; convert_external_args ge args sg.sig_args >>= fun eargs -> - Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) + Some(((w, [Event_syscall(id, eargs, EVint len)]), Vint len), m) | _ -> None diff --git a/lib/Responsefile.mli b/lib/Responsefile.mli new file mode 100644 index 00000000..ada5a15d --- /dev/null +++ b/lib/Responsefile.mli @@ -0,0 +1,31 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + + +val expandargv: string array -> string array + (** Expand responsefile arguments contained in the array and return the full + set of arguments. *) + +exception Error of string + (** Raised by [expandargv] in case of an error *) + +val gnu_quote : string -> string + (** [gnu_quote arg] returns [arg] quoted compatible with the gnu tool chain + quoting conventions. *) + +val diab_quote : string -> string + (** [diab_quote arg] returns [arg] quoted compatible with the diab tool chain + quoting conventions. *) diff --git a/lib/Responsefile.mll b/lib/Responsefile.mll new file mode 100644 index 00000000..35a2dbdb --- /dev/null +++ b/lib/Responsefile.mll @@ -0,0 +1,120 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + + +{ +(* To accumulate the characters in a word or quoted string *) +let buf = Buffer.create 32 + +(* Add the current contents of buf to the list of words seen so far, + taking care not to add empty strings unless warranted (e.g. quoted) *) +let stash inword words = + if inword then begin + let w = Buffer.contents buf in + Buffer.clear buf; + w :: words + end else + words + +} + +let whitespace = [' ' '\t' '\012' '\r' '\n'] + +let backslashes_even = "\\\\"* (* an even number of backslashes *) +let backslashes_odd = "\\\\"* '\\' (* an odd number of backslashes *) + +(* GNU-style quoting *) +(* "Options in file are separated by whitespace. A whitespace + character may be included in an option by surrounding the entire + option in either single or double quotes. Any character (including + a backslash) may be included by prefixing the character to be + included with a backslash. The file may itself contain additional + @file options; any such options will be processed recursively." *) + +rule gnu_unquoted inword words = parse + | eof { List.rev (stash inword words) } + | whitespace+ { gnu_unquoted false (stash inword words) lexbuf } + | '\'' { gnu_single_quote lexbuf; gnu_unquoted true words lexbuf } + | '\"' { gnu_double_quote lexbuf; gnu_unquoted true words lexbuf } + | "" { gnu_one_char lexbuf; gnu_unquoted true words lexbuf } + +and gnu_one_char = parse + | '\\' (_ as c) { Buffer.add_char buf c } + | _ as c { Buffer.add_char buf c } + +and gnu_single_quote = parse + | eof { () (* tolerance *) } + | '\'' { () } + | "" { gnu_one_char lexbuf; gnu_single_quote lexbuf } + +and gnu_double_quote = parse + | eof { () (* tolerance *) } + | '\"' { () } + | "" { gnu_one_char lexbuf; gnu_double_quote lexbuf } + +{ + +let re_responsefile = Str.regexp "@\\(.*\\)$" + +exception Error of string + +let expandargv argv = + let rec expand_arg seen arg k = + if not (Str.string_match re_responsefile arg 0) then + arg :: k + else begin + let filename = Str.matched_group 1 arg in + if List.mem filename seen then + raise (Error ("cycle in response files: " ^ filename)); + let ic = open_in filename in + let words = gnu_unquoted false [] (Lexing.from_channel ic) in + close_in ic; + expand_args (filename :: seen) words k + end + and expand_args seen args k = + match args with + | [] -> k + | a1 :: al -> expand_args seen al (expand_arg seen a1 k) + in + let args = Array.to_list argv in + Array.of_list (List.rev (expand_args [] args [])) + +(* This function reimplements quoting of writeargv from libiberty *) +let gnu_quote arg = + let len = String.length arg in + let buf = Buffer.create len in + String.iter (fun c -> begin match c with + | ' ' | '\t' | '\r' | '\n' | '\\' | '\'' | '"' -> + Buffer.add_char buf '\\' + | _ -> () end; + Buffer.add_char buf c) arg; + Buffer.contents buf + +let re_quote = Str.regexp ".*[ \t\n\r\"]" + +let diab_quote arg = + let buf = Buffer.create ((String.length arg) + 8) in + let doublequote = Str.string_match re_quote arg 0 in + if doublequote then begin + Buffer.add_char buf '"'; + String.iter (fun c -> + if c = '"' then Buffer.add_char buf '\\'; + Buffer.add_char buf c) arg; + if doublequote then Buffer.add_char buf '"'; + Buffer.contents buf + end else + arg +} |