Moved some system functions into own module.

The process handling is now in its own file, like the output name
generation etc.
Bug 18768

3 files changed, 120 insertions, 68 deletions

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 567ff018..0cacae13 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -15,6 +15,7 @@ open Commandline
 open Camlcoq
 open Clflags
 open Timing
+open Sysaux
 
 (* Location of the compatibility library *)
 
@@ -28,49 +29,6 @@ let dump_options = ref false
 (* Optional sdump suffix *)
 let sdump_suffix = ref ".json"
 
-(* 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 argv = Array.of_list args in
-  assert (Array.length argv > 0);
-  try
-    let fd_out =
-      match stdout with
-      | None -> Unix.stdout
-      | Some f ->
-          Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
-    let pid =
-      Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
-    let (_, status) =
-      waitpid_no_intr pid in
-    if stdout <> None then Unix.close fd_out;
-    match status with
-    | Unix.WEXITED rc -> rc
-    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
-  with Unix.Unix_error(err, fn, param) ->
-    eprintf "Error executing '%s': %s: %s %s\n"
-            argv.(0) fn (Unix.error_message err) param;
-    -1
-
-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 _ -> ()
-
 (* Printing of error messages *)
 
 let print_error oc msg =
@@ -82,24 +40,6 @@ let print_error oc msg =
     List.iter print_one_error msg;
     output_char oc '\n'
 
-(* Determine names for output files.  We use -o option if specified
-   and if this is the final destination file (not a dump file).
-   Otherwise, we generate a file in the current directory. *)
-
-let output_filename ?(final = false) source_file source_suffix output_suffix =
-  match !option_o with
-  | Some file when final -> file
-  | _ ->
-    Filename.basename (Filename.chop_suffix source_file source_suffix)
-    ^ output_suffix
-
-(* A variant of [output_filename] where the default output name is fixed *)
-
-let output_filename_default default_file =
-  match !option_o with
-  | Some file -> file
-  | None -> default_file
-
 (* From C to preprocessed C *)
 
 let preprocess ifile ofile =
@@ -280,13 +220,6 @@ let linker exe_name files =
     exit 2
   end
 
-(* All input files should exist *)
-
-let ensure_inputfile_exists name =
-  if not (Sys.file_exists name) then begin
-    eprintf "error: no such file or directory: '%s'\n" name;
-    exit 2
-  end
 
 (* Processing of a .c file *)
 
diff --git a/driver/Sysaux.ml b/driver/Sysaux.ml
new file mode 100644
index 00000000..c9bdd8bf
--- /dev/null
+++ b/driver/Sysaux.ml
@@ -0,0 +1,85 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Printf
+open Clflags
+
+(* 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 argv = Array.of_list args in
+  assert (Array.length argv > 0);
+  try
+    let fd_out =
+      match stdout with
+      | None -> Unix.stdout
+      | Some f ->
+          Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
+    let pid =
+      Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
+    let (_, status) =
+      waitpid_no_intr pid in
+    if stdout <> None then Unix.close fd_out;
+    match status with
+    | Unix.WEXITED rc -> rc
+    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
+  with Unix.Unix_error(err, fn, param) ->
+    eprintf "Error executing '%s': %s: %s %s\n"
+            argv.(0) fn (Unix.error_message err) param;
+    -1
+
+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).
+   Otherwise, we generate a file in the current directory. *)
+
+let output_filename ?(final = false) source_file source_suffix output_suffix =
+  match !option_o with
+  | Some file when final -> file
+  | _ ->
+    Filename.basename (Filename.chop_suffix source_file source_suffix)
+    ^ output_suffix
+
+(* A variant of [output_filename] where the default output name is fixed *)
+
+let output_filename_default default_file =
+  match !option_o with
+  | Some file -> file
+  | None -> default_file
+
+(* All input files should exist *)
+
+let ensure_inputfile_exists name =
+  if not (Sys.file_exists name) then begin
+    eprintf "error: no such file or directory: '%s'\n" name;
+    exit 2
+  end
diff --git a/driver/Sysaux.mli b/driver/Sysaux.mli
new file mode 100644
index 00000000..c639e780
--- /dev/null
+++ b/driver/Sysaux.mli
@@ -0,0 +1,34 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+
+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. *)
+
+val command_error: string -> int -> unit
+   (** Generate an error message for the given command and exit code *)
+
+val safe_remove: string -> unit
+   (** Remove the given file if it exists *)
+
+val output_filename: ?final:bool -> string -> string -> string -> string
+   (** Determine names for output files.  We use -o option if specified
+       and if this is the final destination file (not a dump file).
+       Otherwise, we generate a file in the current directory. *)
+
+val output_filename_default: string -> string
+   (** Return either the file specified by -o or the given file name *)
+
+val ensure_inputfile_exists: string -> unit
+   (** Test whether the given input file exists *)