blob: deca85f2fe75b964972de28783eee6090c375ddf (
plain)
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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
(* is distributed under the terms of the INRIA Non-Commercial *)
(* License Agreement. *)
(* *)
(* *********************************************************************)
open Printf
let search_argv key =
let len = Array.length Commandline.argv in
let res: string option ref = ref None in
for i = 1 to len - 2 do
if Commandline.argv.(i) = key then
res := Some Commandline.argv.(i + 1);
done;
!res
let absolute_path base file =
if Filename.is_relative file then
Filename.concat base file
else
file
(* Locate the .ini file, which is either in the same directory as
the executable or in the directory ../share *)
let ini_file_name =
match search_argv "-conf" with
| Some s -> absolute_path (Sys.getcwd ()) s
| None ->
try
Sys.getenv "COMPCERT_CONFIG"
with Not_found ->
let ini_name = match search_argv "-target" with
| Some s -> s^".ini"
| None -> "compcert.ini" in
let exe_dir = Filename.dirname Sys.executable_name in
let share_dir =
Filename.concat (Filename.concat exe_dir Filename.parent_dir_name)
"share" in
let share_compcert_dir =
Filename.concat share_dir "compcert" in
let search_path = [exe_dir;share_dir;share_compcert_dir] in
let files = List.map (fun s -> Filename.concat s ini_name) search_path in
try
List.find Sys.file_exists files
with Not_found ->
begin
eprintf "Cannot find compcert.ini configuration file.\n";
exit 2
end
let ini_dir = Filename.dirname ini_file_name
(* Read in the .ini file *)
let _ =
try
Readconfig.read_config_file ini_file_name
with
| Readconfig.Error(file, lineno, msg) ->
eprintf "Error reading configuration file %s.\n" ini_file_name;
eprintf "%s:%d:%s\n" file lineno msg;
exit 2
| Sys_error msg ->
eprintf "Error reading configuration file %s.\n" ini_file_name;
eprintf "%s\n" msg;
exit 2
let get_config key =
match Readconfig.key_val key with
| Some v -> v
| None -> eprintf "Configuration option `%s' is not set\n" key; exit 2
let bad_config key vl =
eprintf "Invalid value `%s' for configuration option `%s'\n"
(String.concat " " vl) key;
exit 2
let get_config_string key =
match get_config key with
| [v] -> v
| vl -> bad_config key vl
let get_config_list key =
match get_config key with
| [] -> bad_config key []
| vl -> vl
let tool_absolute_path tools =
match tools with
| [] -> []
| tool::args -> let tool =
if Filename.is_implicit tool && Filename.dirname tool = Filename.current_dir_name then
tool
else
absolute_path ini_dir tool in
tool::args
let opt_config_list key =
match Readconfig.key_val key with
| Some v -> v
| None -> []
let prepro =
tool_absolute_path (get_config_list "prepro")@(opt_config_list "prepro_options")
let asm =
tool_absolute_path (get_config_list "asm")@(opt_config_list "asm_options")
let linker =
tool_absolute_path (get_config_list "linker")@(opt_config_list "linker_options")
let get_bool_config key =
match get_config_string key with
| "true" -> true
| "false" -> false
| v -> bad_config key [v]
let arch =
match get_config_string "arch" with
| "powerpc"|"arm"|"x86"|"riscV"|"kvx"|"aarch64" as a -> a
| v -> bad_config "arch" [v]
let model = get_config_string "model"
let os = get_config_string "os"
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 = get_bool_config "has_runtime_lib"
let has_standard_headers = get_bool_config "has_standard_headers"
let stdlib_path =
if has_runtime_lib then
let path = get_config_string "stdlib_path" in
absolute_path ini_dir path
else
""
let asm_supports_cfi = get_bool_config "asm_supports_cfi"
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]
let gnu_toolchain = system <> "diab"
let elf_target = system <> "macos" && system <> "cygwin"
|
