1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
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. *)
14 (* *********************************************************************)
21 (* Code adapted from CIL *)
23 let voidType = TVoid []
24 let charType = TInt(IChar, [])
25 let intType = TInt(IInt, [])
26 let uintType = TInt(IUInt, [])
27 let longType = TInt(ILong, [])
28 let ulongType = TInt(IULong, [])
29 let ulongLongType = TInt(IULongLong, [])
30 let floatType = TFloat(FFloat, [])
31 let doubleType = TFloat(FDouble, [])
32 let longDoubleType = TFloat (FLongDouble, [])
33 let voidPtrType = TPtr(TVoid [], [])
34 let voidConstPtrType = TPtr(TVoid [AConst], [])
35 let charPtrType = TPtr(TInt(IChar, []), [])
36 let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
37 let intPtrType = TPtr(TInt(IInt, []), [])
38 let sizeType = TInt(size_t_ikind, [])
42 "__builtin_va_list", voidPtrType
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);
63 "__builtin_acos", (doubleType, [ doubleType ], false);
64 "__builtin_acosf", (floatType, [ floatType ], false);
65 "__builtin_acosl", (longDoubleType, [ longDoubleType ], false);
67 "__builtin_alloca", (voidPtrType, [ uintType ], false);
69 "__builtin_asin", (doubleType, [ doubleType ], false);
70 "__builtin_asinf", (floatType, [ floatType ], false);
71 "__builtin_asinl", (longDoubleType, [ longDoubleType ], false);
73 "__builtin_atan", (doubleType, [ doubleType ], false);
74 "__builtin_atanf", (floatType, [ floatType ], false);
75 "__builtin_atanl", (longDoubleType, [ longDoubleType ], false);
77 "__builtin_atan2", (doubleType, [ doubleType; doubleType ], false);
78 "__builtin_atan2f", (floatType, [ floatType; floatType ], false);
79 "__builtin_atan2l", (longDoubleType, [ longDoubleType;
80 longDoubleType ], false);
82 "__builtin_ceil", (doubleType, [ doubleType ], false);
83 "__builtin_ceilf", (floatType, [ floatType ], false);
84 "__builtin_ceill", (longDoubleType, [ longDoubleType ], false);
86 "__builtin_cos", (doubleType, [ doubleType ], false);
87 "__builtin_cosf", (floatType, [ floatType ], false);
88 "__builtin_cosl", (longDoubleType, [ longDoubleType ], false);
90 "__builtin_cosh", (doubleType, [ doubleType ], false);
91 "__builtin_coshf", (floatType, [ floatType ], false);
92 "__builtin_coshl", (longDoubleType, [ longDoubleType ], false);
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);
102 "__builtin_exp", (doubleType, [ doubleType ], false);
103 "__builtin_expf", (floatType, [ floatType ], false);
104 "__builtin_expl", (longDoubleType, [ longDoubleType ], false);
106 "__builtin_expect", (longType, [ longType; longType ], false);
108 "__builtin_fabs", (doubleType, [ doubleType ], false);
109 "__builtin_fabsf", (floatType, [ floatType ], false);
110 "__builtin_fabsl", (longDoubleType, [ longDoubleType ], false);
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);
117 "__builtin_floor", (doubleType, [ doubleType ], false);
118 "__builtin_floorf", (floatType, [ floatType ], false);
119 "__builtin_floorl", (longDoubleType, [ longDoubleType ], false);
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);
130 "__builtin_fmod", (doubleType, [ doubleType ], false);
131 "__builtin_fmodf", (floatType, [ floatType ], false);
132 "__builtin_fmodl", (longDoubleType, [ longDoubleType ], false);
134 "__builtin_frexp", (doubleType, [ doubleType; intPtrType ], false);
135 "__builtin_frexpf", (floatType, [ floatType; intPtrType ], false);
136 "__builtin_frexpl", (longDoubleType, [ longDoubleType;
137 intPtrType ], false);
139 "__builtin_ldexp", (doubleType, [ doubleType; intType ], false);
140 "__builtin_ldexpf", (floatType, [ floatType; intType ], false);
141 "__builtin_ldexpl", (longDoubleType, [ longDoubleType;
144 "__builtin_log", (doubleType, [ doubleType ], false);
145 "__builtin_logf", (floatType, [ floatType ], false);
146 "__builtin_logl", (longDoubleType, [ longDoubleType ], false);
148 "__builtin_log10", (doubleType, [ doubleType ], false);
149 "__builtin_log10f", (floatType, [ floatType ], false);
150 "__builtin_log10l", (longDoubleType, [ longDoubleType ], false);
152 "__builtin_modff", (floatType, [ floatType;
153 TPtr(floatType,[]) ], false);
154 "__builtin_modfl", (longDoubleType, [ longDoubleType;
155 TPtr(longDoubleType, []) ],
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);
167 "__builtin_parity", (intType, [ uintType ], false);
168 "__builtin_parityl", (intType, [ ulongType ], false);
169 "__builtin_parityll", (intType, [ ulongLongType ], false);
171 "__builtin_popcount", (intType, [ uintType ], false);
172 "__builtin_popcountl", (intType, [ ulongType ], false);
173 "__builtin_popcountll", (intType, [ ulongLongType ], false);
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);
182 "__builtin_sin", (doubleType, [ doubleType ], false);
183 "__builtin_sinf", (floatType, [ floatType ], false);
184 "__builtin_sinl", (longDoubleType, [ longDoubleType ], false);
186 "__builtin_sinh", (doubleType, [ doubleType ], false);
187 "__builtin_sinhf", (floatType, [ floatType ], false);
188 "__builtin_sinhl", (longDoubleType, [ longDoubleType ], false);
190 "__builtin_sqrt", (doubleType, [ doubleType ], false);
191 "__builtin_sqrtf", (floatType, [ floatType ], false);
192 "__builtin_sqrtl", (longDoubleType, [ longDoubleType ], false);
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 *) ],
209 "__builtin_tan", (doubleType, [ doubleType ], false);
210 "__builtin_tanf", (floatType, [ floatType ], false);
211 "__builtin_tanl", (longDoubleType, [ longDoubleType ], false);
213 "__builtin_tanh", (doubleType, [ doubleType ], false);
214 "__builtin_tanhf", (floatType, [ floatType ], false);
215 "__builtin_tanhl", (longDoubleType, [ longDoubleType ], false);
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;