1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(* *********************************************************************)
(* *)
(* 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
(* 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);
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
(* Printing of error messages *)
let print_error oc msg =
let print_one_error = function
| Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
| Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
| Errors.POS i -> fprintf oc "%ld" (Camlcoq.P.to_int32 i)
in
List.iter print_one_error msg;
output_char oc '\n'
(* Command-line parsing *)
let explode_comma_option s =
match Str.split (Str.regexp ",") s with
| [] -> assert false
| _ :: tl -> tl
(* Record actions to be performed after parsing the command line *)
let actions : ((string -> string) * string) list ref = ref []
let push_action fn arg =
actions := (fn, arg) :: !actions
let push_linker_arg arg =
push_action (fun s -> s) arg
let perform_actions () =
let rec perform = function
| [] -> []
| (fn, arg) :: rem -> let res = fn arg in res :: perform rem
in perform (List.rev !actions)
|