source: Deliverables/D2.2/8051/cparser/GCC.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 12.0 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* GCC built-ins *)
17
18open C
19open Cutil
20
21(* Code adapted from CIL *)
22
23let voidType = TVoid []
24let charType = TInt(IChar, [])
25let intType = TInt(IInt, [])
26let uintType = TInt(IUInt, [])
27let longType = TInt(ILong, [])
28let ulongType = TInt(IULong, [])
29let ulongLongType = TInt(IULongLong, [])
30let floatType = TFloat(FFloat, [])
31let doubleType = TFloat(FDouble, [])
32let longDoubleType = TFloat (FLongDouble, [])
33let voidPtrType = TPtr(TVoid [], [])
34let voidConstPtrType = TPtr(TVoid [AConst], [])
35let charPtrType = TPtr(TInt(IChar, []), [])
36let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
37let intPtrType = TPtr(TInt(IInt, []), [])
38let sizeType = TInt(size_t_ikind, [])
39
40let builtins = {
41  Builtins.typedefs = [
42  "__builtin_va_list", voidPtrType
43];
44  Builtins.functions = [
45  "__builtin___fprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType ], true) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
46  "__builtin___memcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
47  "__builtin___memmove_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
48  "__builtin___mempcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
49  "__builtin___memset_chk",  (voidPtrType, [ voidPtrType; intType; sizeType; sizeType ], false);
50  "__builtin___printf_chk",  (intType, [ intType; charConstPtrType ], true);
51  "__builtin___snprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType ], true);
52  "__builtin___sprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType ], true);
53  "__builtin___stpcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
54  "__builtin___strcat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
55  "__builtin___strcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
56  "__builtin___strncat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
57  "__builtin___strncpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
58  "__builtin___vfprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType; voidPtrType ], false) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
59  "__builtin___vprintf_chk",  (intType, [ intType; charConstPtrType; voidPtrType ], false);
60  "__builtin___vsnprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType; voidPtrType ], false);
61  "__builtin___vsprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType; voidPtrType ], false);
62
63  "__builtin_acos",  (doubleType, [ doubleType ], false);
64  "__builtin_acosf",  (floatType, [ floatType ], false);
65  "__builtin_acosl",  (longDoubleType, [ longDoubleType ], false);
66
67  "__builtin_alloca",  (voidPtrType, [ uintType ], false);
68 
69  "__builtin_asin",  (doubleType, [ doubleType ], false);
70  "__builtin_asinf",  (floatType, [ floatType ], false);
71  "__builtin_asinl",  (longDoubleType, [ longDoubleType ], false);
72
73  "__builtin_atan",  (doubleType, [ doubleType ], false);
74  "__builtin_atanf",  (floatType, [ floatType ], false);
75  "__builtin_atanl",  (longDoubleType, [ longDoubleType ], false);
76
77  "__builtin_atan2",  (doubleType, [ doubleType; doubleType ], false);
78  "__builtin_atan2f",  (floatType, [ floatType; floatType ], false);
79  "__builtin_atan2l",  (longDoubleType, [ longDoubleType; 
80                                                longDoubleType ], false);
81
82  "__builtin_ceil",  (doubleType, [ doubleType ], false);
83  "__builtin_ceilf",  (floatType, [ floatType ], false);
84  "__builtin_ceill",  (longDoubleType, [ longDoubleType ], false);
85
86  "__builtin_cos",  (doubleType, [ doubleType ], false);
87  "__builtin_cosf",  (floatType, [ floatType ], false);
88  "__builtin_cosl",  (longDoubleType, [ longDoubleType ], false);
89
90  "__builtin_cosh",  (doubleType, [ doubleType ], false);
91  "__builtin_coshf",  (floatType, [ floatType ], false);
92  "__builtin_coshl",  (longDoubleType, [ longDoubleType ], false);
93
94  "__builtin_clz",  (intType, [ uintType ], false);
95  "__builtin_clzl",  (intType, [ ulongType ], false);
96  "__builtin_clzll",  (intType, [ ulongLongType ], false);
97  "__builtin_constant_p",  (intType, [ intType ], false);
98  "__builtin_ctz",  (intType, [ uintType ], false);
99  "__builtin_ctzl",  (intType, [ ulongType ], false);
100  "__builtin_ctzll",  (intType, [ ulongLongType ], false);
101
102  "__builtin_exp",  (doubleType, [ doubleType ], false);
103  "__builtin_expf",  (floatType, [ floatType ], false);
104  "__builtin_expl",  (longDoubleType, [ longDoubleType ], false);
105
106  "__builtin_expect",  (longType, [ longType; longType ], false);
107
108  "__builtin_fabs",  (doubleType, [ doubleType ], false);
109  "__builtin_fabsf",  (floatType, [ floatType ], false);
110  "__builtin_fabsl",  (longDoubleType, [ longDoubleType ], false);
111
112  "__builtin_ffs",  (intType, [ uintType ], false);
113  "__builtin_ffsl",  (intType, [ ulongType ], false);
114  "__builtin_ffsll",  (intType, [ ulongLongType ], false);
115  "__builtin_frame_address",  (voidPtrType, [ uintType ], false);
116
117  "__builtin_floor",  (doubleType, [ doubleType ], false);
118  "__builtin_floorf",  (floatType, [ floatType ], false);
119  "__builtin_floorl",  (longDoubleType, [ longDoubleType ], false);
120
121  "__builtin_huge_val",  (doubleType, [], false);
122  "__builtin_huge_valf",  (floatType, [], false);
123  "__builtin_huge_vall",  (longDoubleType, [], false);
124  "__builtin_inf",  (doubleType, [], false);
125  "__builtin_inff",  (floatType, [], false);
126  "__builtin_infl",  (longDoubleType, [], false);
127  "__builtin_memcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; uintType ], false);
128  "__builtin_mempcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
129
130  "__builtin_fmod",  (doubleType, [ doubleType ], false);
131  "__builtin_fmodf",  (floatType, [ floatType ], false);
132  "__builtin_fmodl",  (longDoubleType, [ longDoubleType ], false);
133
134  "__builtin_frexp",  (doubleType, [ doubleType; intPtrType ], false);
135  "__builtin_frexpf",  (floatType, [ floatType; intPtrType  ], false);
136  "__builtin_frexpl",  (longDoubleType, [ longDoubleType; 
137                                                intPtrType  ], false);
138
139  "__builtin_ldexp",  (doubleType, [ doubleType; intType ], false);
140  "__builtin_ldexpf",  (floatType, [ floatType; intType  ], false);
141  "__builtin_ldexpl",  (longDoubleType, [ longDoubleType; 
142                                                intType  ], false);
143
144  "__builtin_log",  (doubleType, [ doubleType ], false);
145  "__builtin_logf",  (floatType, [ floatType ], false);
146  "__builtin_logl",  (longDoubleType, [ longDoubleType ], false);
147
148  "__builtin_log10",  (doubleType, [ doubleType ], false);
149  "__builtin_log10f",  (floatType, [ floatType ], false);
150  "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
151
152  "__builtin_modff",  (floatType, [ floatType; 
153                                          TPtr(floatType,[]) ], false);
154  "__builtin_modfl",  (longDoubleType, [ longDoubleType; 
155                                               TPtr(longDoubleType, []) ], 
156                             false);
157
158  "__builtin_nan",  (doubleType, [ charConstPtrType ], false);
159  "__builtin_nanf",  (floatType, [ charConstPtrType ], false);
160  "__builtin_nanl",  (longDoubleType, [ charConstPtrType ], false);
161  "__builtin_nans",  (doubleType, [ charConstPtrType ], false);
162  "__builtin_nansf",  (floatType, [ charConstPtrType ], false);
163  "__builtin_nansl",  (longDoubleType, [ charConstPtrType ], false);
164  "__builtin_next_arg",  (voidPtrType, [], false);
165  "__builtin_object_size",  (sizeType, [ voidPtrType; intType ], false);
166
167  "__builtin_parity",  (intType, [ uintType ], false);
168  "__builtin_parityl",  (intType, [ ulongType ], false);
169  "__builtin_parityll",  (intType, [ ulongLongType ], false);
170
171  "__builtin_popcount",  (intType, [ uintType ], false);
172  "__builtin_popcountl",  (intType, [ ulongType ], false);
173  "__builtin_popcountll",  (intType, [ ulongLongType ], false);
174
175  "__builtin_powi",  (doubleType, [ doubleType; intType ], false);
176  "__builtin_powif",  (floatType, [ floatType; intType ], false);
177  "__builtin_powil",  (longDoubleType, [ longDoubleType; intType ], false);
178  "__builtin_prefetch",  (voidType, [ voidConstPtrType ], true);
179  "__builtin_return",  (voidType, [ voidConstPtrType ], false);
180  "__builtin_return_address",  (voidPtrType, [ uintType ], false);
181
182  "__builtin_sin",  (doubleType, [ doubleType ], false);
183  "__builtin_sinf",  (floatType, [ floatType ], false);
184  "__builtin_sinl",  (longDoubleType, [ longDoubleType ], false);
185
186  "__builtin_sinh",  (doubleType, [ doubleType ], false);
187  "__builtin_sinhf",  (floatType, [ floatType ], false);
188  "__builtin_sinhl",  (longDoubleType, [ longDoubleType ], false);
189
190  "__builtin_sqrt",  (doubleType, [ doubleType ], false);
191  "__builtin_sqrtf",  (floatType, [ floatType ], false);
192  "__builtin_sqrtl",  (longDoubleType, [ longDoubleType ], false);
193
194  "__builtin_stpcpy",  (charPtrType, [ charPtrType; charConstPtrType ], false);
195  "__builtin_strchr",  (charPtrType, [ charPtrType; charType ], false);
196  "__builtin_strcmp",  (intType, [ charConstPtrType; charConstPtrType ], false);
197  "__builtin_strcpy",  (charPtrType, [ charPtrType; charConstPtrType ], false);
198  "__builtin_strcspn",  (uintType, [ charConstPtrType; charConstPtrType ], false);
199  "__builtin_strncat",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
200  "__builtin_strncmp",  (intType, [ charConstPtrType; charConstPtrType; sizeType ], false);
201  "__builtin_strncpy",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
202  "__builtin_strspn",  (intType, [ charConstPtrType; charConstPtrType ], false);
203  "__builtin_strpbrk",  (charPtrType, [ charConstPtrType; charConstPtrType ], false);
204  (* When we parse builtin_types_compatible_p, we change its interface *)
205  "__builtin_types_compatible_p", 
206                              (intType, [ uintType; (* Sizeof the type *)
207                                          uintType  (* Sizeof the type *) ],
208                               false);
209  "__builtin_tan",  (doubleType, [ doubleType ], false);
210  "__builtin_tanf",  (floatType, [ floatType ], false);
211  "__builtin_tanl",  (longDoubleType, [ longDoubleType ], false);
212
213  "__builtin_tanh",  (doubleType, [ doubleType ], false);
214  "__builtin_tanhf",  (floatType, [ floatType ], false);
215  "__builtin_tanhl",  (longDoubleType, [ longDoubleType ], false);
216
217  "__builtin_va_end",  (voidType, [ voidPtrType ], false);
218  "__builtin_varargs_start", 
219    (voidType, [ voidPtrType ], false);
220  (* When we elaborate builtin_stdarg_start/builtin_va_start,
221     second argument is passed by address *)
222  "__builtin_va_start",  (voidType, [ voidPtrType; voidPtrType ], false);
223  "__builtin_stdarg_start",  (voidType, [ voidPtrType ], false);
224  (* When we parse builtin_va_arg, type argument becomes sizeof type *)
225  "__builtin_va_arg",  (voidType, [ voidPtrType; sizeType ], false);
226  "__builtin_va_copy",  (voidType, [ voidPtrType;
227                                           voidPtrType ],
228                              false)
229]
230}
Note: See TracBrowser for help on using the repository browser.