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-- | driver/Commandline.ml | 2 | ||||
| -rw-r--r-- | driver/Configuration.ml | 10 | ||||
| -rw-r--r-- | driver/Configuration.mli | 7 | ||||
| -rw-r--r-- | driver/Driveraux.ml | 21 | ||||
| -rw-r--r-- | lib/Responsefile.ml | 133 | ||||
| -rw-r--r-- | lib/Responsefile.mli | 2 | ||||
| -rw-r--r-- | lib/Responsefile.mll | 97 |
11 files changed, 140 insertions, 145 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 @@ -207,7 +207,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 @@ -118,6 +119,7 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" + responsefile="unsupported" ;; *) system="linux" @@ -386,6 +388,7 @@ HAS_RUNTIME_LIB=$has_runtime_lib HAS_STANDARD_HEADERS=$has_standard_headers ASM_SUPPORTS_CFI=$asm_supports_cfi CLIGHTGEN=$clightgen +RESPONSEFILE=$responsefile EOF else cat >> Makefile.config <<'EOF' @@ -469,6 +472,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/driver/Commandline.ml b/driver/Commandline.ml index 1981776e..7e683680 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -101,7 +101,7 @@ let parse_array spec argv first last = let parse_cmdline spec = try - let argv = expand_responsefiles Sys.argv in + let argv = expandargv Sys.argv in parse_array spec argv 1 (Array.length argv - 1) with Arg.Bad s -> eprintf "%s" s; diff --git a/driver/Configuration.ml b/driver/Configuration.ml index e1a02573..be581e14 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -171,3 +171,13 @@ 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 *) + | Unsupported (* responsefiles are not supported *) + +let response_file_style = + match get_config_string "response_file_style" with + | "unsupported" -> Unsupported + | "gnu" -> Gnu + | v -> bad_config "response_file_style" [v] diff --git a/driver/Configuration.mli b/driver/Configuration.mli index dde9d6fd..1092bf6d 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -63,3 +63,10 @@ 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 *) + | Unsupported (* responsefiles are not supported *) + +val response_file_style: response_file_style + (** Style of supported responsefiles *) diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 2c03c65c..6bd48344 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -58,20 +58,25 @@ let command stdout args = argv.(0) fn (Unix.error_message err) param; -1 -let quote arg = - let whitespace = Str.regexp "[ \t\r\n]" in - if Str.string_match whitespace arg 0 then - Filename.quote arg (* We need to quote arguments containing whitespaces *) - else - arg +(* 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 -> match c with + | ' ' | '\t' | '\r' | '\n' | '\\' | '\'' | '"' -> + Buffer.add_char buf '\\' + | _ -> (); + Buffer.add_char buf c) arg; + Buffer.contents buf let command ?stdout args = - if Sys.win32 && List.fold_left (fun len arg -> len + String.length arg + 1) 0 args > 7000 then + 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 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; + List.iter (fun a -> Printf.fprintf oc "%s " (gnu_quote a)) args; close_out oc; let arg = if gnu_system then "@"^file else "-@"^file in let ret = command stdout [cmd;arg] in diff --git a/lib/Responsefile.ml b/lib/Responsefile.ml deleted file mode 100644 index c10fe302..00000000 --- a/lib/Responsefile.ml +++ /dev/null @@ -1,133 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - - -let rec singlequote ic buf = - match input_char ic with - | exception End_of_file -> () - | '\'' -> () - | c -> Buffer.add_char buf c; singlequote ic buf - -let doublequote ic buf = - let rec aux buf = - match input_char ic with - | exception End_of_file -> (* Backslash-newline is ignored. *) - () - | '\"' -> - () - | '\\' -> - begin match input_char ic with - | exception End_of_file -> (* tolerance *) - Buffer.add_char buf '\\' - | '\n' -> - aux buf - | ('\\' | '\"') as c -> - Buffer.add_char buf c; aux buf - | c -> - Buffer.add_char buf '\\'; Buffer.add_char buf c; aux buf - end - | c -> - Buffer.add_char buf c; aux buf in - aux buf - -let doublequote_win ic buf = - let rec aux_win buf n = - match input_char ic with - | exception End_of_file -> (* tolerance *) - add_backslashes n - | '\\' -> - aux_win buf (n+1) - | '\"' -> - if n land 1 = 1 then begin - add_backslashes (n/2); Buffer.add_char buf '\"'; - aux_win buf 0 - end else begin - add_backslashes n - end - | '\n' -> - if n >= 1 then add_backslashes (n-1) else Buffer.add_char buf '\n'; - aux_win buf 0 - | c -> - add_backslashes n; Buffer.add_char buf c; aux_win buf 0 - and add_backslashes n = - for _i = 1 to n do Buffer.add_char buf '\\' done in - aux_win buf 0 - -let doublequote = if Sys.win32 then doublequote_win else doublequote - -let is_add_file file = - String.length file > 1 && String.get file 0 = '@' - -let cut_add file = - String.sub file 1 (String.length file - 1) - -let readwords file = - let visited = ref [] in - let rec aux file = - if Sys.file_exists file then begin - if List.mem file !visited then - raise (Arg.Bad "Circular includes in response files"); - visited := file :: !visited; - let ic = open_in_bin file in - let buf = Buffer.create 32 in - let words = ref [] in - let stash inw = - if inw then begin - let word = Buffer.contents buf in - if is_add_file word then - words := (aux (cut_add word))@ !words - else - words := Buffer.contents buf :: !words; - Buffer.clear buf - end in - let rec unquoted inw = - match input_char ic with - | exception End_of_file -> - stash inw - | ' ' | '\t' | '\r' | '\n' -> - stash inw; unquoted false - | '\\' -> - begin match input_char ic with - | exception End_of_file -> (* tolerance; treat like \newline *) - unquoted inw - | '\n' -> - unquoted inw - | c -> - Buffer.add_char buf c; unquoted true - end - | '\'' -> - singlequote ic buf; unquoted true - | '\"' -> - doublequote ic buf; - unquoted true - | c -> - Buffer.add_char buf c; unquoted true in - unquoted false; - close_in ic; - !words - end else [file] in - List.rev (aux file) - -let expand_responsefiles args = - let acc = ref [] in - for i = (Array.length args - 1) downto 0 do - let file = args.(i) in - if is_add_file file then - acc := readwords (cut_add file) @ !acc - else - acc := file::!acc - done; - Array.of_list !acc diff --git a/lib/Responsefile.mli b/lib/Responsefile.mli index b55dac16..ec82c32e 100644 --- a/lib/Responsefile.mli +++ b/lib/Responsefile.mli @@ -15,6 +15,6 @@ (* *********************************************************************) -val expand_responsefiles: string array -> string array +val expandargv: string array -> string array (** Expand responsefile arguments contained in the array and return the full set of arguments. *) diff --git a/lib/Responsefile.mll b/lib/Responsefile.mll new file mode 100644 index 00000000..bb29fd75 --- /dev/null +++ b/lib/Responsefile.mll @@ -0,0 +1,97 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + + +(* Parsing response files with various quoting styles *) + +{ +(* 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 [])) + +} |