Machine.ml 8.1 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
47
48
49
50
51
52
53
54
55
  sizeof_size_t: int;
  sizeof_ptrdiff_t: int;
  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;
56
  alignof_fun: int option;
57
  bigendian: bool;
58
  bitfields_msb_first: bool;
59
60
61
  supports_unaligned_accesses: bool;
  struct_passing_style: struct_passing_style;
  struct_return_style : struct_return_style;
62
63
64
}

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

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

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

166
167
(* Canned configurations for some ABIs *)

168
let x86_32 =
169
170
171
  { ilp32ll64 with name = "x86_32";
                   char_signed = true;
                   alignof_longlong = 4; alignof_double = 4;
172
                   alignof_longdouble = 4;
173
174
175
                   supports_unaligned_accesses = true;
                   struct_passing_style = SP_split_args;
                   struct_return_style = SR_ref}
176
177

let x86_32_macosx =
178
179
180
181
  {x86_32 with struct_passing_style = SP_split_args;
               struct_return_style = SR_int1248 }

let x86_32_bsd =
182
  x86_32_macosx
183

184
let x86_64 =
185
186
187
  { i32lpll64 with name = "x86_64"; char_signed = true;
                   struct_passing_style = SP_ref_callee; (* wrong *)
                   struct_return_style = SR_ref } (* to check *)
188

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

205
206
207
let ppc_32_diab_bigendian =
  { ppc_32_bigendian with sizeof_wchar = 2; wchar_signed = false }

208
209
let ppc_32_linux_bigendian = {ppc_32_bigendian with struct_return_style = SR_ref;}

210
let arm_littleendian =
211
212
  { ilp32ll64 with name = "arm"; struct_passing_style = SP_split_args;
                   struct_return_style = SR_int1to4;}
213

214
215
216
217
let arm_bigendian =
  { arm_littleendian with bigendian = true;
                          bitfields_msb_first = true }

218
let rv32 =
219
220
221
  { ilp32ll64 with name = "rv32";
                   struct_passing_style = SP_ref_callee; (* Wrong *)
                   struct_return_style = SR_ref } (* to check *)
222
let rv64 =
223
224
225
  { i32lpll64 with name = "rv64";
                   struct_passing_style = SP_ref_callee; (* Wrong *)
                   struct_return_style = SR_ref } (* to check *)
226

227
let mppa_k1c =
228
229
  { ilp32ll64 with sizeof_ptr = 8;
                   name = "k1c";
230
231
232
                   char_signed = true;
                   supports_unaligned_accesses = true }

233
(* Add GCC extensions re: sizeof and alignof *)
234
235
236
237
238

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

239
240
241
(* Normalize configuration for use with the CompCert reference interpreter *)

let compcert_interpreter c =
242
  { c with supports_unaligned_accesses = false }
243

244
(* Undefined configuration *)
245

246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
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;
  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;
275
276
277
  supports_unaligned_accesses = false;
  struct_passing_style = SP_ref_callee;
  struct_return_style = SR_ref;
278
279
280
281
282
}

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

let config = ref undef