From fbaeaaec35da748db98a3cf9e405024024561426 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 19 Apr 2016 17:14:50 +0200 Subject: Moved some system functions into own module. The process handling is now in its own file, like the output name generation etc. Bug 18768 --- driver/Driver.ml | 69 +------------------------------------------- driver/Sysaux.ml | 85 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ driver/Sysaux.mli | 34 ++++++++++++++++++++++ 3 files changed, 120 insertions(+), 68 deletions(-) create mode 100644 driver/Sysaux.ml create mode 100644 driver/Sysaux.mli 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 *) -- cgit