cparser/GCC.ml

   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
  18 open C
  19 open Cutil
  20
  21 (* Code adapted from CIL *)
  22
  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, [])
  39
  40 let 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 }