target.h (12986B)
1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. 2 Licensed under the Apache 2.0 and MIT Licenses. */ 3 4 #ifndef KRML_HEADER_TARGET_H 5 #define KRML_HEADER_TARGET_H 6 7 #include <assert.h> 8 #include <inttypes.h> 9 #include <limits.h> 10 #include <stdbool.h> 11 #include <stddef.h> 12 #include <stdio.h> 13 #include <stdlib.h> 14 15 typedef float float32_t; 16 typedef double float64_t; 17 18 /* Since KaRaMeL emits the inline keyword unconditionally, we follow the 19 * guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this 20 * __inline__ to ensure the code compiles with -std=c90 and earlier. */ 21 #ifdef __GNUC__ 22 #define inline __inline__ 23 #endif 24 25 /* There is no support for aligned_alloc() in macOS before Catalina, so 26 * let's make a macro to use _mm_malloc() and _mm_free() functions 27 * from mm_malloc.h. */ 28 #if defined(__APPLE__) && defined(__MACH__) 29 #include <AvailabilityMacros.h> 30 #if defined(MAC_OS_X_VERSION_MIN_REQUIRED) && \ 31 (MAC_OS_X_VERSION_MIN_REQUIRED < 101500) 32 #include <mm_malloc.h> 33 #define LEGACY_MACOS 34 #else 35 #undef LEGACY_MACOS 36 #endif 37 #endif 38 39 /******************************************************************************/ 40 /* Macros that KaRaMeL will generate. */ 41 /******************************************************************************/ 42 43 /* For "bare" targets that do not have a C stdlib, the user might want to use 44 * [-add-early-include '"mydefinitions.h"'] and override these. */ 45 #ifndef KRML_HOST_PRINTF 46 #define KRML_HOST_PRINTF printf 47 #endif 48 49 #if ( \ 50 (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \ 51 (!(defined KRML_HOST_EPRINTF))) 52 #define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__) 53 #elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER) 54 #define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__) 55 #endif 56 57 #ifndef KRML_HOST_EXIT 58 #define KRML_HOST_EXIT exit 59 #endif 60 61 #ifndef KRML_HOST_MALLOC 62 #define KRML_HOST_MALLOC malloc 63 #endif 64 65 #ifndef KRML_HOST_CALLOC 66 #define KRML_HOST_CALLOC calloc 67 #endif 68 69 #ifndef KRML_HOST_FREE 70 #define KRML_HOST_FREE free 71 #endif 72 73 #ifndef KRML_HOST_IGNORE 74 #define KRML_HOST_IGNORE(x) (void)(x) 75 #endif 76 77 #ifndef KRML_MAYBE_UNUSED_VAR 78 #define KRML_MAYBE_UNUSED_VAR(x) KRML_HOST_IGNORE(x) 79 #endif 80 81 #ifndef KRML_MAYBE_UNUSED 82 #if defined(__GNUC__) || defined(__clang__) 83 #define KRML_MAYBE_UNUSED __attribute__((unused)) 84 #else 85 #define KRML_MAYBE_UNUSED 86 #endif 87 #endif 88 89 #ifndef KRML_ATTRIBUTE_TARGET 90 #if defined(__GNUC__) || defined(__clang__) 91 #define KRML_ATTRIBUTE_TARGET(x) __attribute__((target(x))) 92 #else 93 #define KRML_ATTRIBUTE_TARGET(x) 94 #endif 95 #endif 96 97 #ifndef KRML_NOINLINE 98 #if defined(__GNUC__) || defined(__clang__) 99 #define KRML_NOINLINE __attribute__((noinline, unused)) 100 #elif defined(_MSC_VER) 101 #define KRML_NOINLINE __declspec(noinline) 102 #elif defined(__SUNPRO_C) 103 #define KRML_NOINLINE __attribute__((noinline)) 104 #else 105 #define KRML_NOINLINE 106 #warning "The KRML_NOINLINE macro is not defined for this toolchain!" 107 #warning "The compiler may defeat side-channel resistance with optimizations." 108 #warning "Please locate target.h and try to fill it out with a suitable definition for this compiler." 109 #endif 110 #endif 111 112 #ifndef KRML_MUSTINLINE 113 #if defined(_MSC_VER) 114 #define KRML_MUSTINLINE inline __forceinline 115 #elif defined(__GNUC__) 116 #define KRML_MUSTINLINE inline __attribute__((always_inline)) 117 #elif defined(__SUNPRO_C) 118 #define KRML_MUSTINLINE inline __attribute__((always_inline)) 119 #else 120 #define KRML_MUSTINLINE inline 121 #warning "The KRML_MUSTINLINE macro defaults to plain inline for this toolchain!" 122 #warning "Please locate target.h and try to fill it out with a suitable definition for this compiler." 123 #endif 124 #endif 125 126 #ifndef KRML_PRE_ALIGN 127 #ifdef _MSC_VER 128 #define KRML_PRE_ALIGN(X) __declspec(align(X)) 129 #else 130 #define KRML_PRE_ALIGN(X) 131 #endif 132 #endif 133 134 #ifndef KRML_POST_ALIGN 135 #ifdef _MSC_VER 136 #define KRML_POST_ALIGN(X) 137 #else 138 #define KRML_POST_ALIGN(X) __attribute__((aligned(X))) 139 #endif 140 #endif 141 142 /* MinGW-W64 does not support C11 aligned_alloc, but it supports 143 * MSVC's _aligned_malloc. 144 */ 145 #ifndef KRML_ALIGNED_MALLOC 146 #ifdef __MINGW32__ 147 #include <_mingw.h> 148 #endif 149 #if ( \ 150 defined(_MSC_VER) || \ 151 (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR))) 152 #define KRML_ALIGNED_MALLOC(X, Y) _aligned_malloc(Y, X) 153 #elif defined(LEGACY_MACOS) 154 #define KRML_ALIGNED_MALLOC(X, Y) _mm_malloc(Y, X) 155 #else 156 #define KRML_ALIGNED_MALLOC(X, Y) aligned_alloc(X, Y) 157 #endif 158 #endif 159 160 /* Since aligned allocations with MinGW-W64 are done with 161 * _aligned_malloc (see above), such pointers must be freed with 162 * _aligned_free. 163 */ 164 #ifndef KRML_ALIGNED_FREE 165 #ifdef __MINGW32__ 166 #include <_mingw.h> 167 #endif 168 #if ( \ 169 defined(_MSC_VER) || \ 170 (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR))) 171 #define KRML_ALIGNED_FREE(X) _aligned_free(X) 172 #elif defined(LEGACY_MACOS) 173 #define KRML_ALIGNED_FREE(X) _mm_free(X) 174 #else 175 #define KRML_ALIGNED_FREE(X) free(X) 176 #endif 177 #endif 178 179 #ifndef KRML_HOST_TIME 180 181 #include <time.h> 182 183 /* Prims_nat not yet in scope */ 184 inline static int32_t 185 krml_time(void) 186 { 187 return (int32_t)time(NULL); 188 } 189 190 #define KRML_HOST_TIME krml_time 191 #endif 192 193 /* In statement position, exiting is easy. */ 194 #define KRML_EXIT \ 195 do { \ 196 KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \ 197 KRML_HOST_EXIT(254); \ 198 } while (0) 199 200 /* In expression position, use the comma-operator and a malloc to return an 201 * expression of the right size. KaRaMeL passes t as the parameter to the macro. 202 */ 203 #define KRML_EABORT(t, msg) \ 204 (KRML_HOST_PRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \ 205 KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t)))) 206 207 /* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of 208 * *elements*. Do an ugly, run-time check (some of which KaRaMeL can eliminate). 209 */ 210 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4)) 211 #define _KRML_CHECK_SIZE_PRAGMA \ 212 _Pragma("GCC diagnostic ignored \"-Wtype-limits\"") 213 #else 214 #define _KRML_CHECK_SIZE_PRAGMA 215 #endif 216 217 #define KRML_CHECK_SIZE(size_elt, sz) \ 218 do { \ 219 _KRML_CHECK_SIZE_PRAGMA \ 220 if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \ 221 KRML_HOST_PRINTF( \ 222 "Maximum allocatable size exceeded, aborting before overflow at " \ 223 "%s:%d\n", \ 224 __FILE__, __LINE__); \ 225 KRML_HOST_EXIT(253); \ 226 } \ 227 } while (0) 228 229 #if defined(_MSC_VER) && _MSC_VER < 1900 230 #define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) \ 231 _snprintf_s(buf, sz, _TRUNCATE, fmt, arg) 232 #else 233 #define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg) 234 #endif 235 236 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4)) 237 #define KRML_DEPRECATED(x) __attribute__((deprecated(x))) 238 #elif defined(__GNUC__) 239 /* deprecated attribute is not defined in GCC < 4.5. */ 240 #define KRML_DEPRECATED(x) 241 #elif defined(__SUNPRO_C) 242 #define KRML_DEPRECATED(x) __attribute__((deprecated(x))) 243 #elif defined(_MSC_VER) 244 #define KRML_DEPRECATED(x) __declspec(deprecated(x)) 245 #endif 246 247 /* Macros for prettier unrolling of loops */ 248 #define KRML_LOOP1(i, n, x) \ 249 { \ 250 x \ 251 i += n; \ 252 (void)i; \ 253 } 254 255 #define KRML_LOOP2(i, n, x) \ 256 KRML_LOOP1(i, n, x) \ 257 KRML_LOOP1(i, n, x) 258 259 #define KRML_LOOP3(i, n, x) \ 260 KRML_LOOP2(i, n, x) \ 261 KRML_LOOP1(i, n, x) 262 263 #define KRML_LOOP4(i, n, x) \ 264 KRML_LOOP2(i, n, x) \ 265 KRML_LOOP2(i, n, x) 266 267 #define KRML_LOOP5(i, n, x) \ 268 KRML_LOOP4(i, n, x) \ 269 KRML_LOOP1(i, n, x) 270 271 #define KRML_LOOP6(i, n, x) \ 272 KRML_LOOP4(i, n, x) \ 273 KRML_LOOP2(i, n, x) 274 275 #define KRML_LOOP7(i, n, x) \ 276 KRML_LOOP4(i, n, x) \ 277 KRML_LOOP3(i, n, x) 278 279 #define KRML_LOOP8(i, n, x) \ 280 KRML_LOOP4(i, n, x) \ 281 KRML_LOOP4(i, n, x) 282 283 #define KRML_LOOP9(i, n, x) \ 284 KRML_LOOP8(i, n, x) \ 285 KRML_LOOP1(i, n, x) 286 287 #define KRML_LOOP10(i, n, x) \ 288 KRML_LOOP8(i, n, x) \ 289 KRML_LOOP2(i, n, x) 290 291 #define KRML_LOOP11(i, n, x) \ 292 KRML_LOOP8(i, n, x) \ 293 KRML_LOOP3(i, n, x) 294 295 #define KRML_LOOP12(i, n, x) \ 296 KRML_LOOP8(i, n, x) \ 297 KRML_LOOP4(i, n, x) 298 299 #define KRML_LOOP13(i, n, x) \ 300 KRML_LOOP8(i, n, x) \ 301 KRML_LOOP5(i, n, x) 302 303 #define KRML_LOOP14(i, n, x) \ 304 KRML_LOOP8(i, n, x) \ 305 KRML_LOOP6(i, n, x) 306 307 #define KRML_LOOP15(i, n, x) \ 308 KRML_LOOP8(i, n, x) \ 309 KRML_LOOP7(i, n, x) 310 311 #define KRML_LOOP16(i, n, x) \ 312 KRML_LOOP8(i, n, x) \ 313 KRML_LOOP8(i, n, x) 314 315 #define KRML_UNROLL_FOR(i, z, n, k, x) \ 316 do { \ 317 uint32_t i = z; \ 318 KRML_LOOP##n(i, k, x) \ 319 } while (0) 320 321 #define KRML_ACTUAL_FOR(i, z, n, k, x) \ 322 do { \ 323 for (uint32_t i = z; i < n; i += k) { \ 324 x \ 325 } \ 326 } while (0) 327 328 #ifndef KRML_UNROLL_MAX 329 #define KRML_UNROLL_MAX 16 330 #endif 331 332 /* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */ 333 #if 0 <= KRML_UNROLL_MAX 334 #define KRML_MAYBE_FOR0(i, z, n, k, x) 335 #else 336 #define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 337 #endif 338 339 #if 1 <= KRML_UNROLL_MAX 340 #define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x) 341 #else 342 #define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 343 #endif 344 345 #if 2 <= KRML_UNROLL_MAX 346 #define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x) 347 #else 348 #define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 349 #endif 350 351 #if 3 <= KRML_UNROLL_MAX 352 #define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x) 353 #else 354 #define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 355 #endif 356 357 #if 4 <= KRML_UNROLL_MAX 358 #define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x) 359 #else 360 #define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 361 #endif 362 363 #if 5 <= KRML_UNROLL_MAX 364 #define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x) 365 #else 366 #define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 367 #endif 368 369 #if 6 <= KRML_UNROLL_MAX 370 #define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x) 371 #else 372 #define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 373 #endif 374 375 #if 7 <= KRML_UNROLL_MAX 376 #define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x) 377 #else 378 #define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 379 #endif 380 381 #if 8 <= KRML_UNROLL_MAX 382 #define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x) 383 #else 384 #define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 385 #endif 386 387 #if 9 <= KRML_UNROLL_MAX 388 #define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x) 389 #else 390 #define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 391 #endif 392 393 #if 10 <= KRML_UNROLL_MAX 394 #define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x) 395 #else 396 #define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 397 #endif 398 399 #if 11 <= KRML_UNROLL_MAX 400 #define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x) 401 #else 402 #define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 403 #endif 404 405 #if 12 <= KRML_UNROLL_MAX 406 #define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x) 407 #else 408 #define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 409 #endif 410 411 #if 13 <= KRML_UNROLL_MAX 412 #define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x) 413 #else 414 #define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 415 #endif 416 417 #if 14 <= KRML_UNROLL_MAX 418 #define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x) 419 #else 420 #define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 421 #endif 422 423 #if 15 <= KRML_UNROLL_MAX 424 #define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x) 425 #else 426 #define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 427 #endif 428 429 #if 16 <= KRML_UNROLL_MAX 430 #define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x) 431 #else 432 #define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 433 #endif 434 #endif /* KRML_HEADER_TARGET_H */