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 4ac759d0bceef49d16197e3bb8c9767ece693c5e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 2 Aug 2016 10:59:27 +0200 Subject: Added -dall which enables all tracing. --- driver/Driver.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index a0ec07f1..68615727 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -333,6 +333,7 @@ Code generation options: (use -fno- to turn off -f)\n\ \ -dltl Save LTL after register allocation in .ltl\n\ \ -dmach Save generated Mach code in .mach\n\ \ -dasm Save generated assembly in .s\n\ +\ -dall Save all generated intermidate files in .\n\ \ -sdump Save info for post-linking validation in .json\n\ \ -doptions Save the compiler configurations in .opt.json\n\ General options:\n\ @@ -440,6 +441,17 @@ let cmdline_actions = Exact "-dalloctrace", Set option_dalloctrace; Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; + Exact "-dall", Self (fun _ -> + option_dprepro := true; + option_dparse := true; + option_dcmedium := true; + option_dclight := true; + option_dcminor := true; + option_drtl := true; + option_dalloctrace := true; + option_dmach := true; + option_dasm := true; + dump_options:=true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); Exact "-doptions", Set dump_options; -- cgit From 028aaefc44b8ed8bafd8b8896fedb53f6e68df3c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 5 Aug 2016 14:05:34 +0200 Subject: Implement support for big endian arm targets. Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418 --- driver/Configuration.ml | 5 +++++ driver/Configuration.mli | 3 +++ driver/Driver.ml | 4 +++- 3 files changed, 11 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index e1a02573..765b075a 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -121,6 +121,11 @@ let arch = | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" +let is_big_endian = + match get_config_string "endianness" with + | "big" -> true + | "little" -> false + | v -> bad_config "endianness" [v] let system = get_config_string "system" let has_runtime_lib = match get_config_string "has_runtime_lib" with diff --git a/driver/Configuration.mli b/driver/Configuration.mli index dde9d6fd..4b9c64a9 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -19,6 +19,9 @@ val model: string val abi: string (** ABI to use *) +val is_big_endian: bool + (** Endianness to use *) + val system: string (** Flavor of operating system that runs CompCert *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 68615727..9c07dba1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -524,7 +524,9 @@ let _ = | "powerpc" -> if Configuration.system = "linux" then Machine.ppc_32_bigendian else Machine.ppc_32_diab_bigendian - | "arm" -> Machine.arm_littleendian + | "arm" -> if Configuration.is_big_endian + then Machine.arm_bigendian + else Machine.arm_littleendian | "ia32" -> if Configuration.abi = "macosx" then Machine.x86_32_macosx else Machine.x86_32 -- 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 From 0200f6b77550e95c0ec309d1a44f5253fc790e4f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 22 Aug 2016 13:34:56 +0200 Subject: Print whole command line. When response files are used CompCert should still print all command line arguments since the response file is deleted after usage. Bug 19297. --- driver/Driveraux.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'driver') diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 33cd9215..d25301d2 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -28,14 +28,6 @@ let rec waitpid_no_intr pid = with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid let command stdout args = - if !option_v then begin - eprintf "+ %s" (String.concat " " args); - begin match stdout with - | None -> () - | Some f -> eprintf " > %s" f - end; - prerr_endline "" - end; let argv = Array.of_list args in assert (Array.length argv > 0); try @@ -59,6 +51,14 @@ let command stdout args = -1 let command ?stdout args = + if !option_v then begin + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" + end; 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 -- cgit