123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293 |
- /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
- Licensed under the Apache 2.0 License. */
- #ifndef __KRML_TARGET_H
- #define __KRML_TARGET_H
- #include <assert.h>
- #include <inttypes.h>
- #include <limits.h>
- #include <stdbool.h>
- #include <stddef.h>
- #include <stdio.h>
- #include <stdlib.h>
- /* Since KaRaMeL emits the inline keyword unconditionally, we follow the
- * guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this
- * __inline__ to ensure the code compiles with -std=c90 and earlier. */
- #ifdef __GNUC__
- # define inline __inline__
- #endif
- /******************************************************************************/
- /* Macros that KaRaMeL will generate. */
- /******************************************************************************/
- /* For "bare" targets that do not have a C stdlib, the user might want to use
- * [-add-early-include '"mydefinitions.h"'] and override these. */
- #ifndef KRML_HOST_PRINTF
- # define KRML_HOST_PRINTF printf
- #endif
- #if ( \
- (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
- (!(defined KRML_HOST_EPRINTF)))
- # define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
- #elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
- # define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
- #endif
- #ifndef KRML_HOST_EXIT
- # define KRML_HOST_EXIT exit
- #endif
- #ifndef KRML_HOST_MALLOC
- # define KRML_HOST_MALLOC malloc
- #endif
- #ifndef KRML_HOST_CALLOC
- # define KRML_HOST_CALLOC calloc
- #endif
- #ifndef KRML_HOST_FREE
- # define KRML_HOST_FREE free
- #endif
- #ifndef KRML_HOST_IGNORE
- # define KRML_HOST_IGNORE(x) (void)(x)
- #endif
- #ifndef KRML_MAYBE_UNUSED_VAR
- # define KRML_MAYBE_UNUSED_VAR(x) KRML_HOST_IGNORE(x)
- #endif
- #ifndef KRML_MAYBE_UNUSED
- # if defined(__GNUC__)
- # define KRML_MAYBE_UNUSED __attribute__((unused))
- # else
- # define KRML_MAYBE_UNUSED
- # endif
- #endif
- #ifndef KRML_NOINLINE
- # if defined(_MSC_VER)
- # define KRML_NOINLINE __declspec(noinline)
- # elif defined (__GNUC__)
- # define KRML_NOINLINE __attribute__((noinline,unused))
- # else
- # define KRML_NOINLINE
- # warning "The KRML_NOINLINE macro is not defined for this toolchain!"
- # warning "The compiler may defeat side-channel resistance with optimizations."
- # warning "Please locate target.h and try to fill it out with a suitable definition for this compiler."
- # endif
- #endif
- /* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
- * *elements*. Do an ugly, run-time check (some of which KaRaMeL can eliminate).
- */
- #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4))
- # define _KRML_CHECK_SIZE_PRAGMA \
- _Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
- #else
- # define _KRML_CHECK_SIZE_PRAGMA
- #endif
- #define KRML_CHECK_SIZE(size_elt, sz) \
- do { \
- _KRML_CHECK_SIZE_PRAGMA \
- if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \
- KRML_HOST_PRINTF( \
- "Maximum allocatable size exceeded, aborting before overflow at " \
- "%s:%d\n", \
- __FILE__, __LINE__); \
- KRML_HOST_EXIT(253); \
- } \
- } while (0)
- /* Macros for prettier unrolling of loops */
- #define KRML_LOOP1(i, n, x) { \
- x \
- i += n; \
- (void) i; \
- }
- #define KRML_LOOP2(i, n, x) \
- KRML_LOOP1(i, n, x) \
- KRML_LOOP1(i, n, x)
- #define KRML_LOOP3(i, n, x) \
- KRML_LOOP2(i, n, x) \
- KRML_LOOP1(i, n, x)
- #define KRML_LOOP4(i, n, x) \
- KRML_LOOP2(i, n, x) \
- KRML_LOOP2(i, n, x)
- #define KRML_LOOP5(i, n, x) \
- KRML_LOOP4(i, n, x) \
- KRML_LOOP1(i, n, x)
- #define KRML_LOOP6(i, n, x) \
- KRML_LOOP4(i, n, x) \
- KRML_LOOP2(i, n, x)
- #define KRML_LOOP7(i, n, x) \
- KRML_LOOP4(i, n, x) \
- KRML_LOOP3(i, n, x)
- #define KRML_LOOP8(i, n, x) \
- KRML_LOOP4(i, n, x) \
- KRML_LOOP4(i, n, x)
- #define KRML_LOOP9(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP1(i, n, x)
- #define KRML_LOOP10(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP2(i, n, x)
- #define KRML_LOOP11(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP3(i, n, x)
- #define KRML_LOOP12(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP4(i, n, x)
- #define KRML_LOOP13(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP5(i, n, x)
- #define KRML_LOOP14(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP6(i, n, x)
- #define KRML_LOOP15(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP7(i, n, x)
- #define KRML_LOOP16(i, n, x) \
- KRML_LOOP8(i, n, x) \
- KRML_LOOP8(i, n, x)
- #define KRML_UNROLL_FOR(i, z, n, k, x) \
- do { \
- uint32_t i = z; \
- KRML_LOOP##n(i, k, x) \
- } while (0)
- #define KRML_ACTUAL_FOR(i, z, n, k, x) \
- do { \
- for (uint32_t i = z; i < n; i += k) { \
- x \
- } \
- } while (0)
- #ifndef KRML_UNROLL_MAX
- # define KRML_UNROLL_MAX 16
- #endif
- /* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */
- #if 0 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR0(i, z, n, k, x)
- #else
- # define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 1 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x)
- #else
- # define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 2 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x)
- #else
- # define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 3 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x)
- #else
- # define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 4 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x)
- #else
- # define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 5 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x)
- #else
- # define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 6 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x)
- #else
- # define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 7 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x)
- #else
- # define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 8 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x)
- #else
- # define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 9 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x)
- #else
- # define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 10 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x)
- #else
- # define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 11 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x)
- #else
- # define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 12 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x)
- #else
- # define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 13 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x)
- #else
- # define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 14 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x)
- #else
- # define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 15 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x)
- #else
- # define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #if 16 <= KRML_UNROLL_MAX
- # define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x)
- #else
- # define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
- #endif
- #endif
|