Machine.ml 8.5 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* Machine-dependent aspects *)

18
19
20
21
22
23
24
25
26
27
28
29
type struct_passing_style =
  | SP_ref_callee                       (* by reference, callee takes copy *)
  | SP_ref_caller                       (* by reference, caller takes copy *)
  | SP_split_args                       (* by value, as a sequence of ints *)

type struct_return_style =
  | SR_int1248      (* return by content if size is 1, 2, 4 or 8 bytes *)
  | SR_int1to4      (* return by content if size is <= 4 *)
  | SR_int1to8      (* return by content if size is <= 8 *)
  | SR_ref          (* always return by assignment to a reference
                       given as extra argument *)

30
type t = {
31
  name: string;
32
33
34
35
36
37
38
39
40
41
42
43
  char_signed: bool;
  sizeof_ptr: int;
  sizeof_short: int;
  sizeof_int: int;
  sizeof_long: int;
  sizeof_longlong: int;
  sizeof_float: int;
  sizeof_double: int;
  sizeof_longdouble: int;
  sizeof_void: int option;
  sizeof_fun: int option;
  sizeof_wchar: int;
44
  wchar_signed: bool;
45
46
  sizeof_size_t: int;
  sizeof_ptrdiff_t: int;
47
  sizeof_intreg: int;
48
49
50
51
52
53
54
55
56
  alignof_ptr: int;
  alignof_short: int;
  alignof_int: int;
  alignof_long: int;
  alignof_longlong: int;
  alignof_float: int;
  alignof_double: int;
  alignof_longdouble: int;
  alignof_void: int option;
57
  alignof_fun: int option;
58
  bigendian: bool;
59
  bitfields_msb_first: bool;
60
61
62
  supports_unaligned_accesses: bool;
  struct_passing_style: struct_passing_style;
  struct_return_style : struct_return_style;
63
64
65
}

let ilp32ll64 = {
66
  name = "ilp32ll64";
67
68
69
70
71
72
73
74
  char_signed = false;
  sizeof_ptr = 4;
  sizeof_short = 2;
  sizeof_int = 4;
  sizeof_long = 4;
  sizeof_longlong = 8;
  sizeof_float = 4;
  sizeof_double = 8;
75
  sizeof_longdouble = 8;
76
77
78
  sizeof_void = None;
  sizeof_fun = None;
  sizeof_wchar = 4;
79
  wchar_signed = true;
80
81
  sizeof_size_t = 4;
  sizeof_ptrdiff_t = 4;
82
  sizeof_intreg = 4;
83
84
85
86
87
88
89
  alignof_ptr = 4;
  alignof_short = 2;
  alignof_int = 4;
  alignof_long = 4;
  alignof_longlong = 8;
  alignof_float = 4;
  alignof_double = 8;
90
  alignof_longdouble = 8;
91
  alignof_void = None;
92
  alignof_fun = None;
93
  bigendian = false;
94
  bitfields_msb_first = false;
95
96
97
  supports_unaligned_accesses = false;
  struct_passing_style = SP_ref_callee;
  struct_return_style = SR_ref;
98
99
100
}

let i32lpll64 = {
101
  name = "i32lpll64";
102
103
104
105
106
107
108
109
  char_signed = false;
  sizeof_ptr = 8;
  sizeof_short = 2;
  sizeof_int = 4;
  sizeof_long = 8;
  sizeof_longlong = 8;
  sizeof_float = 4;
  sizeof_double = 8;
110
  sizeof_longdouble = 8;
111
112
113
  sizeof_void = None;
  sizeof_fun = None;
  sizeof_wchar = 4;
114
  wchar_signed = true;
115
116
  sizeof_size_t = 8;
  sizeof_ptrdiff_t = 8;
117
  sizeof_intreg = 8;
118
119
120
121
122
123
124
  alignof_ptr = 8;
  alignof_short = 2;
  alignof_int = 4;
  alignof_long = 8;
  alignof_longlong = 8;
  alignof_float = 4;
  alignof_double = 8;
125
  alignof_longdouble = 8;
126
  alignof_void = None;
127
  alignof_fun = None;
128
  bigendian = false;
129
  bitfields_msb_first = false;
130
131
132
  supports_unaligned_accesses = false;
  struct_passing_style = SP_ref_callee;
  struct_return_style = SR_ref;
133
134
135
}

let il32pll64 = {
136
  name = "il32pll64";
137
138
139
140
141
142
143
144
  char_signed = false;
  sizeof_ptr = 8;
  sizeof_short = 2;
  sizeof_int = 4;
  sizeof_long = 4;
  sizeof_longlong = 8;
  sizeof_float = 4;
  sizeof_double = 8;
145
  sizeof_longdouble = 8;
146
147
148
  sizeof_void = None;
  sizeof_fun = None;
  sizeof_wchar = 4;
149
  wchar_signed = true;
150
151
  sizeof_size_t = 8;
  sizeof_ptrdiff_t = 8;
152
  sizeof_intreg = 8;
153
154
155
156
157
158
159
  alignof_ptr = 8;
  alignof_short = 2;
  alignof_int = 4;
  alignof_long = 4;
  alignof_longlong = 8;
  alignof_float = 4;
  alignof_double = 8;
160
  alignof_longdouble = 8;
161
  alignof_void = None;
162
  alignof_fun = None;
163
  bigendian = false;
164
  bitfields_msb_first = false;
165
166
167
  supports_unaligned_accesses = false;
  struct_passing_style = SP_ref_callee;
  struct_return_style = SR_ref;
168
169
}

170
171
(* Canned configurations for some ABIs *)

172
let x86_32 =
173
174
175
  { ilp32ll64 with name = "x86_32";
                   char_signed = true;
                   alignof_longlong = 4; alignof_double = 4;
176
                   alignof_longdouble = 4;
177
178
179
                   supports_unaligned_accesses = true;
                   struct_passing_style = SP_split_args;
                   struct_return_style = SR_ref}
180
181

let x86_32_macosx =
182
183
184
185
  {x86_32 with struct_passing_style = SP_split_args;
               struct_return_style = SR_int1248 }

let x86_32_bsd =
186
  x86_32_macosx
187

188
let x86_64 =
189
190
191
  { i32lpll64 with name = "x86_64"; char_signed = true;
                   struct_passing_style = SP_ref_callee; (* wrong *)
                   struct_return_style = SR_ref } (* to check *)
192

193
194
let win32 =
  { ilp32ll64 with name = "win32"; char_signed = true;
195
196
197
                   sizeof_wchar = 2; wchar_signed = false;
                   struct_passing_style = SP_split_args;
                   struct_return_style = SR_ref }
198
let win64 =
199
200
  { il32pll64 with name = "win64"; char_signed = true;
                   sizeof_wchar = 2; wchar_signed = false }
201
let ppc_32_bigendian =
202
203
204
  { ilp32ll64 with name = "powerpc";
                   bigendian = true;
                   bitfields_msb_first = true;
205
206
207
                   supports_unaligned_accesses = true;
                   struct_passing_style = SP_ref_caller;
                   struct_return_style =  SR_int1to8; }
208

209
210
211
let ppc_32_r64_bigendian =
  { ppc_32_bigendian with sizeof_intreg = 8;}

212
213
214
let ppc_32_diab_bigendian =
  { ppc_32_bigendian with sizeof_wchar = 2; wchar_signed = false }

215
216
217
let ppc_32_r64_diab_bigendian =
  { ppc_32_diab_bigendian with sizeof_intreg = 8;}

218
219
let ppc_32_linux_bigendian = {ppc_32_bigendian with struct_return_style = SR_ref;}

220
221
222
let ppc_32_r64_linux_bigendian =
  { ppc_32_linux_bigendian with sizeof_intreg = 8;}

223
let arm_littleendian =
224
225
  { ilp32ll64 with name = "arm"; struct_passing_style = SP_split_args;
                   struct_return_style = SR_int1to4;}
226

227
228
229
230
let arm_bigendian =
  { arm_littleendian with bigendian = true;
                          bitfields_msb_first = true }

231
let rv32 =
232
233
234
  { ilp32ll64 with name = "rv32";
                   struct_passing_style = SP_ref_callee; (* Wrong *)
                   struct_return_style = SR_ref } (* to check *)
235
let rv64 =
236
237
238
  { i32lpll64 with name = "rv64";
                   struct_passing_style = SP_ref_callee; (* Wrong *)
                   struct_return_style = SR_ref } (* to check *)
239

Xavier Leroy's avatar
Xavier Leroy committed
240
241
242
243
244
let aarch64 =
  { i32lpll64 with name = "aarch64";
                   struct_passing_style = SP_ref_callee; (* Wrong *)
                   struct_return_style = SR_ref } (* Wrong *)

Xavier Leroy's avatar
Xavier Leroy committed
245
246
247
let aarch64_apple =
  { aarch64 with char_signed = true }

248
(* Add GCC extensions re: sizeof and alignof *)
249
250
251
252
253

let gcc_extensions c =
  { c with sizeof_void = Some 1; sizeof_fun = Some 1;
           alignof_void = Some 1; alignof_fun = Some 1 }

254
255
256
(* Normalize configuration for use with the CompCert reference interpreter *)

let compcert_interpreter c =
257
  { c with supports_unaligned_accesses = false }
258

259
(* Undefined configuration *)
260

261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
let undef = {
  name = "UNDEFINED";
  char_signed = false;
  sizeof_ptr = 0;
  sizeof_short = 0;
  sizeof_int = 0;
  sizeof_long = 0;
  sizeof_longlong = 0;
  sizeof_float = 0;
  sizeof_double = 0;
  sizeof_longdouble = 0;
  sizeof_void = None;
  sizeof_fun = None;
  sizeof_wchar = 0;
  wchar_signed = true;
  sizeof_size_t = 0;
  sizeof_ptrdiff_t = 0;
278
  sizeof_intreg = 0;
279
280
281
282
283
284
285
286
287
288
289
290
  alignof_ptr = 0;
  alignof_short = 0;
  alignof_int = 0;
  alignof_long = 0;
  alignof_longlong = 0;
  alignof_float = 0;
  alignof_double = 0;
  alignof_longdouble = 0;
  alignof_void = None;
  alignof_fun = None;
  bigendian = false;
  bitfields_msb_first = false;
291
292
293
  supports_unaligned_accesses = false;
  struct_passing_style = SP_ref_callee;
  struct_return_style = SR_ref;
294
295
296
297
298
}

(* The current configuration.  Must be initialized before use. *)

let config = ref undef