Merge branch 'master' into advanced-diagnostics

7 files changed, 93 insertions, 20 deletions

diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index c5c2b82c..ce5acf9d 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
@@ -103,4 +104,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 e1a02573..87e29e0f 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
@@ -171,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 dde9d6fd..197e8ad2 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 *)
 
@@ -63,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 78baed47..8b0cd7ac 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -333,13 +333,15 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\
 \  -dltl          Save LTL after register allocation in <file>.ltl\n\
 \  -dmach         Save generated Mach code in <file>.mach\n\
 \  -dasm          Save generated assembly in <file>.s\n\
+\  -dall          Save all generated intermidate files in <file>.<ext>\n\
 \  -sdump         Save info for post-linking validation in <file>.json\n\
 \  -doptions      Save the compiler configurations in <file>.opt.json\n\
 General options:\n\
 \  -stdlib <dir>  Set the path of the Compcert run-time library\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" ^
+\  -version       Print the version string and exit\n\
+\  @<file>        Read command line options from <file>\n" ^
   Cerrors.warning_help ^
 "Interpreter mode:\n\
 \  -interp        Execute given .c files using the reference interpreter\n\
@@ -442,6 +444,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;
@@ -515,7 +528,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
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 3fe22fac..d25301d2 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -14,21 +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 =
-  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 command stdout args =
   let argv = Array.of_list args in
   assert (Array.length argv > 0);
   try
@@ -51,12 +50,37 @@ let command ?stdout args =
             argv.(0) fn (Unix.error_message err) param;
     -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
+    | 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