From ea2d6b70ed06c60dba9ba81cf53883c85fb92068 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 8 Jul 2016 10:15:31 +0200 Subject: Added responsefile support for commandline. Commandline can now be passed in a file specifed with @file on the Commandline. The quoting convention is similar to the one used by gcc, etc. Options are separated by whitespaces and options with whitespaecs need to be quoted. Bug 18303 --- driver/Commandline.ml | 8 +++++++- driver/Driver.ml | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Commandline.ml b/driver/Commandline.ml index 0a2c8fca..1981776e 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 = expand_responsefiles Sys.argv in + parse_array spec argv 1 (Array.length argv - 1) + with Arg.Bad s -> + eprintf "%s" s; + exit 2 diff --git a/driver/Driver.ml b/driver/Driver.ml index 7311215d..6d8cf9ac 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -334,6 +334,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\ +\ @ Read command line options from \n\ Interpreter mode:\n\ \ -interp Execute given .c files using the reference interpreter\n\ \ -quiet Suppress diagnostic messages for the interpreter\n\ -- cgit From efa462bd1655c6b2c8f064e214762650092257e8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 12 Jul 2016 13:18:42 +0200 Subject: Added heuristic for passing arg via responsefiles. Since gnu make and other tools under windows seem to have a limit of around 8000 bytes per command line the arguments should be passed via responsefiles instead. Bug 18308 --- driver/Assembler.ml | 9 +++++++-- driver/Driveraux.ml | 23 +++++++++++++++++++++-- driver/Driveraux.mli | 8 +++++++- driver/Frontend.ml | 9 +++++++-- driver/Linker.ml | 13 +++++++++---- 5 files changed, 51 insertions(+), 11 deletions(-) (limited to 'driver') diff --git a/driver/Assembler.ml b/driver/Assembler.ml index 52fb17d8..d6cb65ea 100644 --- a/driver/Assembler.ml +++ b/driver/Assembler.ml @@ -18,12 +18,17 @@ open Driveraux (* From asm to object file *) let assemble ifile ofile = - let cmd = List.concat [ - Configuration.asm; + let cmd,opts = match Configuration.asm with + | name::opts -> name,opts + | [] -> assert false (* Should be catched in Configuration *) in + let opts = List.concat [ + opts; ["-o"; ofile]; List.rev !assembler_options; [ifile] ] in + let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["@"^a]) in + let cmd = cmd::opts in let exc = command cmd in if exc <> 0 then begin safe_remove ofile; diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 3fe22fac..8ebf261d 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -14,12 +14,33 @@ open Printf open Clflags +(* Is this a gnu based tool chain *) +let gnu_system = Configuration.system <> "diab" + (* 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 responsefile args resp_arg = + try + if Sys.win32 && (String.length (String.concat "" args) > 7000) then + let file,oc = Filename.open_temp_file "compcert" "" in + let whitespace = Str.regexp "[ \t\r\n]" in + let quote arg = + if Str.string_match whitespace arg 0 then + Filename.quote arg (* We need to quote arguments containing whitespaces *) + else + arg in + List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args; + close_out oc; + resp_arg file + else + args + with Sys_error _ -> + args + let command ?stdout args = if !option_v then begin eprintf "+ %s" (String.concat " " args); @@ -94,8 +115,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..54df4336 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -12,7 +12,13 @@ (* *********************************************************************) -val command: ?stdout:string -> string list -> int +val responsefile: string list -> (string -> string list) -> string list + (** [responsefiles args resp_arg] Test whether [args] should be passed + via responsefile and writes them into a file. [resp_arg] generates + the new argument constructed from the responsefile. If no + responsefile is written the arguments are returned unchanged. *) + +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/Frontend.ml b/driver/Frontend.ml index 043d4e5a..41b09b58 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -24,8 +24,11 @@ open Printf let preprocess ifile ofile = let output = if ofile = "-" then None else Some ofile in - let cmd = List.concat [ - Configuration.prepro; + let cmd,opts = match Configuration.prepro with + | name::opts -> name,opts + | [] -> assert false (* Should be catched in Configuration *) in + let opts = List.concat [ + opts; ["-D__COMPCERT__"]; (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] @@ -33,6 +36,8 @@ let preprocess ifile ofile = List.rev !prepro_options; [ifile] ] in + let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["@"^a]) in + let cmd = cmd::opts in let exc = command ?stdout:output cmd in if exc <> 0 then begin if ofile <> "-" then safe_remove ofile; diff --git a/driver/Linker.ml b/driver/Linker.ml index 2f767023..14c9bcb3 100644 --- a/driver/Linker.ml +++ b/driver/Linker.ml @@ -19,14 +19,19 @@ open Driveraux (* Linking *) let linker exe_name files = - let cmd = List.concat [ - Configuration.linker; + let cmd,opts = match Configuration.linker with + | name::opts -> name,opts + | [] -> assert false (* Should be catched in Configuration *) in + let opts = List.concat [ + opts; ["-o"; exe_name]; files; (if Configuration.has_runtime_lib - then ["-L" ^ !stdlib_path; "-lcompcert"] - else []) + then ["-L" ^ !stdlib_path; "-lcompcert"] + else []) ] in + let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["-@"^a]) in + let cmd = cmd::opts in let exc = command cmd in if exc <> 0 then begin command_error "linker" exc; -- cgit From 2129fe8f2e19c4dd91955e5300e76d924e0a3e6d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 19 Jul 2016 09:44:26 +0200 Subject: Merged responfile function into command. Command now decides whether to use a responsefile or call the external command directly. Bug 18004 --- driver/Assembler.ml | 9 ++------- driver/Driveraux.ml | 49 +++++++++++++++++++++++++++---------------------- driver/Driveraux.mli | 6 ------ driver/Frontend.ml | 9 ++------- driver/Linker.ml | 9 ++------- 5 files changed, 33 insertions(+), 49 deletions(-) (limited to 'driver') diff --git a/driver/Assembler.ml b/driver/Assembler.ml index d6cb65ea..52fb17d8 100644 --- a/driver/Assembler.ml +++ b/driver/Assembler.ml @@ -18,17 +18,12 @@ open Driveraux (* From asm to object file *) let assemble ifile ofile = - let cmd,opts = match Configuration.asm with - | name::opts -> name,opts - | [] -> assert false (* Should be catched in Configuration *) in - let opts = List.concat [ - opts; + let cmd = List.concat [ + Configuration.asm; ["-o"; ofile]; List.rev !assembler_options; [ifile] ] in - let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["@"^a]) in - let cmd = cmd::opts in let exc = command cmd in if exc <> 0 then begin safe_remove ofile; diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 8ebf261d..2c03c65c 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -17,31 +17,17 @@ open Clflags (* Is this a gnu based tool chain *) let gnu_system = Configuration.system <> "diab" +(* Sage removale 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 responsefile args resp_arg = - try - if Sys.win32 && (String.length (String.concat "" args) > 7000) then - let file,oc = Filename.open_temp_file "compcert" "" in - let whitespace = Str.regexp "[ \t\r\n]" in - let quote arg = - if Str.string_match whitespace arg 0 then - Filename.quote arg (* We need to quote arguments containing whitespaces *) - else - arg in - List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args; - close_out oc; - resp_arg file - else - args - with Sys_error _ -> - args - -let command ?stdout args = +let command stdout args = if !option_v then begin eprintf "+ %s" (String.concat " " args); begin match stdout with @@ -72,12 +58,31 @@ 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 + +let command ?stdout args = + if Sys.win32 && 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; + close_out oc; + let arg = if gnu_system then "@"^file else "-@"^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). diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 54df4336..e6bac6e3 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -12,12 +12,6 @@ (* *********************************************************************) -val responsefile: string list -> (string -> string list) -> string list - (** [responsefiles args resp_arg] Test whether [args] should be passed - via responsefile and writes them into a file. [resp_arg] generates - the new argument constructed from the responsefile. If no - responsefile is written the arguments are returned unchanged. *) - 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/Frontend.ml b/driver/Frontend.ml index 41b09b58..043d4e5a 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -24,11 +24,8 @@ open Printf let preprocess ifile ofile = let output = if ofile = "-" then None else Some ofile in - let cmd,opts = match Configuration.prepro with - | name::opts -> name,opts - | [] -> assert false (* Should be catched in Configuration *) in - let opts = List.concat [ - opts; + let cmd = List.concat [ + Configuration.prepro; ["-D__COMPCERT__"]; (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] @@ -36,8 +33,6 @@ let preprocess ifile ofile = List.rev !prepro_options; [ifile] ] in - let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["@"^a]) in - let cmd = cmd::opts in let exc = command ?stdout:output cmd in if exc <> 0 then begin if ofile <> "-" then safe_remove ofile; diff --git a/driver/Linker.ml b/driver/Linker.ml index 14c9bcb3..305c5603 100644 --- a/driver/Linker.ml +++ b/driver/Linker.ml @@ -19,19 +19,14 @@ open Driveraux (* Linking *) let linker exe_name files = - let cmd,opts = match Configuration.linker with - | name::opts -> name,opts - | [] -> assert false (* Should be catched in Configuration *) in - let opts = List.concat [ - opts; + let cmd = List.concat [ + Configuration.linker; ["-o"; exe_name]; files; (if Configuration.has_runtime_lib then ["-L" ^ !stdlib_path; "-lcompcert"] else []) ] in - let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["-@"^a]) in - let cmd = cmd::opts in let exc = command cmd in if exc <> 0 then begin command_error "linker" exc; -- cgit From f22c32dcda0e8b546e85e8ad95d0ad655e365d38 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 20 Jul 2016 13:20:19 +0200 Subject: Added simplified reader and printer for gnu @files The functions expandargv and writeargv resemble the functions from the libiberity that are used by the gnu tools. Additionaly a new configuration is added in order to determine which kind of response files are supported for calls to other tools. Bug 18308 --- driver/Commandline.ml | 2 +- driver/Configuration.ml | 10 ++++++++++ driver/Configuration.mli | 7 +++++++ driver/Driveraux.ml | 21 +++++++++++++-------- 4 files changed, 31 insertions(+), 9 deletions(-) (limited to 'driver') 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 -- cgit From 0a38e7727f3c38742704907e0c4dc60da6b99743 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 21 Jul 2016 14:39:00 +0200 Subject: Added support for quoting for diab backend. The diab data compiler has different quoting conventions compared to the gnu tools. Bug 18308. --- driver/Configuration.ml | 2 ++ driver/Configuration.mli | 1 + driver/Driveraux.ml | 18 +++++++++++++++++- 3 files changed, 20 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index be581e14..0a2b3eec 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -174,10 +174,12 @@ let struct_return_style = 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 1092bf6d..7087c3c2 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -66,6 +66,7 @@ val struct_return_style: struct_return_style 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 diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 6bd48344..1ee39e8e 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -69,14 +69,30 @@ let gnu_quote arg = Buffer.add_char buf c) arg; Buffer.contents buf +let re_whitespace = Str.regexp ".*[ \t\n\r]" + +let diab_quote arg = + let buf = Buffer.create ((String.length arg) + 8) in + let doublequote = Str.string_match re_whitespace arg 0 in + if doublequote then 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 + 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 = match Configuration.response_file_style with + | Configuration.Unsupported -> assert false + | Configuration.Gnu -> gnu_quote + | Configuration.Diab -> 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 " (gnu_quote a)) args; + List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args; close_out oc; let arg = if gnu_system then "@"^file else "-@"^file in let ret = command stdout [cmd;arg] in -- cgit From 951c37603e2a807b116f91d7390bd6e641d8092b Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 21 Jul 2016 14:45:44 +0200 Subject: Corrected diab quoting. Bug 18308 --- driver/Driveraux.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'driver') diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 1ee39e8e..a773b37c 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -69,17 +69,20 @@ let gnu_quote arg = Buffer.add_char buf c) arg; Buffer.contents buf -let re_whitespace = Str.regexp ".*[ \t\n\r]" +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_whitespace arg 0 in - if doublequote then 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 + 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 let command ?stdout args = let resp = Sys.win32 && Configuration.response_file_style <> Configuration.Unsupported in -- cgit From eb2844b87fa0e176bd65466d7ab7d16666344406 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 10 Aug 2016 13:31:25 +0200 Subject: Added missing begin end around quoting. Bug 18308. --- driver/Driveraux.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index a773b37c..de1326ce 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -62,10 +62,10 @@ let command stdout args = let gnu_quote arg = let len = String.length arg in let buf = Buffer.create len in - String.iter (fun c -> match c with + 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 -- cgit From 5309f16159e4decd81330622dcdd6eb4b25819a1 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 16 Aug 2016 10:35:17 +0200 Subject: Moved quoting functions in Responsefile Also corrected some typos and corrected exception handling for expandargv. Bug 18308 --- driver/Commandline.ml | 2 +- driver/Driveraux.ml | 36 +++++------------------------------- driver/Linker.ml | 4 ++-- 3 files changed, 8 insertions(+), 34 deletions(-) (limited to 'driver') diff --git a/driver/Commandline.ml b/driver/Commandline.ml index 7e683680..d125736a 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -103,6 +103,6 @@ let parse_cmdline spec = try let argv = expandargv Sys.argv in parse_array spec argv 1 (Array.length argv - 1) - with Arg.Bad s -> + with Responsefile.Error s -> eprintf "%s" s; exit 2 diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index de1326ce..33cd9215 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -17,7 +17,7 @@ open Clflags (* Is this a gnu based tool chain *) let gnu_system = Configuration.system <> "diab" -(* Sage removale of files *) +(* Safe removal of files *) let safe_remove file = try Sys.remove file with Sys_error _ -> () @@ -58,46 +58,20 @@ let command stdout args = argv.(0) fn (Unix.error_message err) param; -1 -(* 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 - 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 = match Configuration.response_file_style with + let quote,prefix = match Configuration.response_file_style with | Configuration.Unsupported -> assert false - | Configuration.Gnu -> gnu_quote - | Configuration.Diab -> diab_quote in + | 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 = if gnu_system then "@"^file else "-@"^file in + let arg = prefix^file in let ret = command stdout [cmd;arg] in safe_remove file; ret diff --git a/driver/Linker.ml b/driver/Linker.ml index 305c5603..2f767023 100644 --- a/driver/Linker.ml +++ b/driver/Linker.ml @@ -24,8 +24,8 @@ let linker exe_name files = ["-o"; exe_name]; files; (if Configuration.has_runtime_lib - then ["-L" ^ !stdlib_path; "-lcompcert"] - else []) + then ["-L" ^ !stdlib_path; "-lcompcert"] + else []) ] in let exc = command cmd in if exc <> 0 then begin -- cgit From b08fd2ea809b87af8551ff6bc50e544209798d24 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 17 Aug 2016 08:35:21 +0200 Subject: Fixed issue with emulation of printf The emulated printf in the interpreter did always return 0 instead of the numbers of bytes printed. Bug 19564 --- driver/Interp.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'driver') 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 -- cgit