Machine.ml 6.6 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* *********************************************************************)
(*                                                                     *)
(*              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 *)

type t = {
19
  name: string;
20
21
22
23
24
25
26
27
28
29
30
31
  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;
32
  wchar_signed: bool;
33
34
35
36
37
38
39
40
41
42
43
  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;
44
  alignof_fun: int option;
45
  bigendian: bool;
46
  bitfields_msb_first: bool;
47
48
49
  supports_unaligned_accesses: bool;
  struct_return_as_int: int;
  struct_passing_style: struct_passing_style
50
51
}

52
53
54
55
56
and struct_passing_style =
  | SP_ref_callee
  | SP_ref_caller
  | SP_split_args

57
let ilp32ll64 = {
58
  name = "ilp32ll64";
59
60
61
62
63
64
65
66
67
68
69
70
  char_signed = false;
  sizeof_ptr = 4;
  sizeof_short = 2;
  sizeof_int = 4;
  sizeof_long = 4;
  sizeof_longlong = 8;
  sizeof_float = 4;
  sizeof_double = 8;
  sizeof_longdouble = 16;
  sizeof_void = None;
  sizeof_fun = None;
  sizeof_wchar = 4;
71
  wchar_signed = true;
72
73
74
75
76
77
78
79
80
81
82
  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;
  alignof_longdouble = 16;
  alignof_void = None;
83
  alignof_fun = None;
84
  bigendian = false;
85
  bitfields_msb_first = false;
86
87
88
  supports_unaligned_accesses = false;
  struct_return_as_int = 0;
  struct_passing_style = SP_ref_callee
89
90
91
}

let i32lpll64 = {
92
  name = "i32lpll64";
93
94
95
96
97
98
99
100
101
102
103
104
  char_signed = false;
  sizeof_ptr = 8;
  sizeof_short = 2;
  sizeof_int = 4;
  sizeof_long = 8;
  sizeof_longlong = 8;
  sizeof_float = 4;
  sizeof_double = 8;
  sizeof_longdouble = 16;
  sizeof_void = None;
  sizeof_fun = None;
  sizeof_wchar = 4;
105
  wchar_signed = true;
106
107
108
109
110
111
112
113
114
115
116
  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;
  alignof_longdouble = 16;
  alignof_void = None;
117
  alignof_fun = None;
118
  bigendian = false;
119
  bitfields_msb_first = false;
120
121
122
  supports_unaligned_accesses = false;
  struct_return_as_int = 0;
  struct_passing_style = SP_ref_callee
123
124
125
}

let il32pll64 = {
126
  name = "il32pll64";
127
128
129
130
131
132
133
134
135
136
137
138
  char_signed = false;
  sizeof_ptr = 8;
  sizeof_short = 2;
  sizeof_int = 4;
  sizeof_long = 4;
  sizeof_longlong = 8;
  sizeof_float = 4;
  sizeof_double = 8;
  sizeof_longdouble = 16;
  sizeof_void = None;
  sizeof_fun = None;
  sizeof_wchar = 4;
139
  wchar_signed = true;
140
141
142
143
144
145
146
147
148
149
150
  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;
  alignof_longdouble = 16;
  alignof_void = None;
151
  alignof_fun = None;
152
  bigendian = false;
153
  bitfields_msb_first = false;
154
155
156
  supports_unaligned_accesses = false;
  struct_return_as_int = 0;
  struct_passing_style = SP_ref_callee
157
158
}

159
160
(* Canned configurations for some ABIs *)

161
let x86_32 =
162
163
164
  { ilp32ll64 with name = "x86_32";
                   char_signed = true;
                   alignof_longlong = 4; alignof_double = 4;
165
166
167
168
169
170
171
172
                   sizeof_longdouble = 12; alignof_longdouble = 4;
                   supports_unaligned_accesses = true;
                   struct_passing_style = SP_split_args }

let x86_32_macosx =
  { x86_32 with sizeof_longdouble = 16; alignof_longdouble = 16;
                struct_return_as_int = 8 }

173
let x86_64 =
174
  { i32lpll64 with name = "x86_64"; char_signed = true }
175

176
177
178
let win32 =
  { ilp32ll64 with name = "win32"; char_signed = true;
                   sizeof_wchar = 2; wchar_signed = false }
179
let win64 =
180
181
  { il32pll64 with name = "win64"; char_signed = true;
                   sizeof_wchar = 2; wchar_signed = false }
182
let ppc_32_bigendian =
183
184
185
  { ilp32ll64 with name = "powerpc";
                   bigendian = true;
                   bitfields_msb_first = true;
186
187
188
189
                   supports_unaligned_accesses = true;
                   struct_return_as_int = 8;
                   struct_passing_style = SP_ref_caller }

190
191
let arm_littleendian =
  { ilp32ll64 with name = "arm";
192
193
                   struct_return_as_int = 4;
                   struct_passing_style = SP_split_args }
194
195

(* Add GCC extensions re: sizeof and alignof *)
196
197
198
199
200

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

201
202
203
204
205
206
207
208
(* Normalize configuration for use with the CompCert reference interpreter *)

let compcert_interpreter c =
  { c with sizeof_longdouble = 8; alignof_longdouble = 8;
           supports_unaligned_accesses = false;
           struct_return_as_int = 0;
           struct_passing_style = SP_ref_callee }

209
(* Undefined configuration *)
210

211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
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;
240
241
242
  supports_unaligned_accesses = false;
  struct_return_as_int = 0;
  struct_passing_style = SP_ref_callee
243
244
245
246
247
}

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

let config = ref undef