target.h 10 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293
  1. /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
  2. Licensed under the Apache 2.0 License. */
  3. #ifndef __KRML_TARGET_H
  4. #define __KRML_TARGET_H
  5. #include <assert.h>
  6. #include <inttypes.h>
  7. #include <limits.h>
  8. #include <stdbool.h>
  9. #include <stddef.h>
  10. #include <stdio.h>
  11. #include <stdlib.h>
  12. /* Since KaRaMeL emits the inline keyword unconditionally, we follow the
  13. * guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this
  14. * __inline__ to ensure the code compiles with -std=c90 and earlier. */
  15. #ifdef __GNUC__
  16. # define inline __inline__
  17. #endif
  18. /******************************************************************************/
  19. /* Macros that KaRaMeL will generate. */
  20. /******************************************************************************/
  21. /* For "bare" targets that do not have a C stdlib, the user might want to use
  22. * [-add-early-include '"mydefinitions.h"'] and override these. */
  23. #ifndef KRML_HOST_PRINTF
  24. # define KRML_HOST_PRINTF printf
  25. #endif
  26. #if ( \
  27. (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
  28. (!(defined KRML_HOST_EPRINTF)))
  29. # define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
  30. #elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
  31. # define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
  32. #endif
  33. #ifndef KRML_HOST_EXIT
  34. # define KRML_HOST_EXIT exit
  35. #endif
  36. #ifndef KRML_HOST_MALLOC
  37. # define KRML_HOST_MALLOC malloc
  38. #endif
  39. #ifndef KRML_HOST_CALLOC
  40. # define KRML_HOST_CALLOC calloc
  41. #endif
  42. #ifndef KRML_HOST_FREE
  43. # define KRML_HOST_FREE free
  44. #endif
  45. #ifndef KRML_HOST_IGNORE
  46. # define KRML_HOST_IGNORE(x) (void)(x)
  47. #endif
  48. #ifndef KRML_MAYBE_UNUSED_VAR
  49. # define KRML_MAYBE_UNUSED_VAR(x) KRML_HOST_IGNORE(x)
  50. #endif
  51. #ifndef KRML_MAYBE_UNUSED
  52. # if defined(__GNUC__)
  53. # define KRML_MAYBE_UNUSED __attribute__((unused))
  54. # else
  55. # define KRML_MAYBE_UNUSED
  56. # endif
  57. #endif
  58. #ifndef KRML_NOINLINE
  59. # if defined(_MSC_VER)
  60. # define KRML_NOINLINE __declspec(noinline)
  61. # elif defined (__GNUC__)
  62. # define KRML_NOINLINE __attribute__((noinline,unused))
  63. # else
  64. # define KRML_NOINLINE
  65. # warning "The KRML_NOINLINE macro is not defined for this toolchain!"
  66. # warning "The compiler may defeat side-channel resistance with optimizations."
  67. # warning "Please locate target.h and try to fill it out with a suitable definition for this compiler."
  68. # endif
  69. #endif
  70. /* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
  71. * *elements*. Do an ugly, run-time check (some of which KaRaMeL can eliminate).
  72. */
  73. #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4))
  74. # define _KRML_CHECK_SIZE_PRAGMA \
  75. _Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
  76. #else
  77. # define _KRML_CHECK_SIZE_PRAGMA
  78. #endif
  79. #define KRML_CHECK_SIZE(size_elt, sz) \
  80. do { \
  81. _KRML_CHECK_SIZE_PRAGMA \
  82. if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \
  83. KRML_HOST_PRINTF( \
  84. "Maximum allocatable size exceeded, aborting before overflow at " \
  85. "%s:%d\n", \
  86. __FILE__, __LINE__); \
  87. KRML_HOST_EXIT(253); \
  88. } \
  89. } while (0)
  90. /* Macros for prettier unrolling of loops */
  91. #define KRML_LOOP1(i, n, x) { \
  92. x \
  93. i += n; \
  94. (void) i; \
  95. }
  96. #define KRML_LOOP2(i, n, x) \
  97. KRML_LOOP1(i, n, x) \
  98. KRML_LOOP1(i, n, x)
  99. #define KRML_LOOP3(i, n, x) \
  100. KRML_LOOP2(i, n, x) \
  101. KRML_LOOP1(i, n, x)
  102. #define KRML_LOOP4(i, n, x) \
  103. KRML_LOOP2(i, n, x) \
  104. KRML_LOOP2(i, n, x)
  105. #define KRML_LOOP5(i, n, x) \
  106. KRML_LOOP4(i, n, x) \
  107. KRML_LOOP1(i, n, x)
  108. #define KRML_LOOP6(i, n, x) \
  109. KRML_LOOP4(i, n, x) \
  110. KRML_LOOP2(i, n, x)
  111. #define KRML_LOOP7(i, n, x) \
  112. KRML_LOOP4(i, n, x) \
  113. KRML_LOOP3(i, n, x)
  114. #define KRML_LOOP8(i, n, x) \
  115. KRML_LOOP4(i, n, x) \
  116. KRML_LOOP4(i, n, x)
  117. #define KRML_LOOP9(i, n, x) \
  118. KRML_LOOP8(i, n, x) \
  119. KRML_LOOP1(i, n, x)
  120. #define KRML_LOOP10(i, n, x) \
  121. KRML_LOOP8(i, n, x) \
  122. KRML_LOOP2(i, n, x)
  123. #define KRML_LOOP11(i, n, x) \
  124. KRML_LOOP8(i, n, x) \
  125. KRML_LOOP3(i, n, x)
  126. #define KRML_LOOP12(i, n, x) \
  127. KRML_LOOP8(i, n, x) \
  128. KRML_LOOP4(i, n, x)
  129. #define KRML_LOOP13(i, n, x) \
  130. KRML_LOOP8(i, n, x) \
  131. KRML_LOOP5(i, n, x)
  132. #define KRML_LOOP14(i, n, x) \
  133. KRML_LOOP8(i, n, x) \
  134. KRML_LOOP6(i, n, x)
  135. #define KRML_LOOP15(i, n, x) \
  136. KRML_LOOP8(i, n, x) \
  137. KRML_LOOP7(i, n, x)
  138. #define KRML_LOOP16(i, n, x) \
  139. KRML_LOOP8(i, n, x) \
  140. KRML_LOOP8(i, n, x)
  141. #define KRML_UNROLL_FOR(i, z, n, k, x) \
  142. do { \
  143. uint32_t i = z; \
  144. KRML_LOOP##n(i, k, x) \
  145. } while (0)
  146. #define KRML_ACTUAL_FOR(i, z, n, k, x) \
  147. do { \
  148. for (uint32_t i = z; i < n; i += k) { \
  149. x \
  150. } \
  151. } while (0)
  152. #ifndef KRML_UNROLL_MAX
  153. # define KRML_UNROLL_MAX 16
  154. #endif
  155. /* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */
  156. #if 0 <= KRML_UNROLL_MAX
  157. # define KRML_MAYBE_FOR0(i, z, n, k, x)
  158. #else
  159. # define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  160. #endif
  161. #if 1 <= KRML_UNROLL_MAX
  162. # define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x)
  163. #else
  164. # define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  165. #endif
  166. #if 2 <= KRML_UNROLL_MAX
  167. # define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x)
  168. #else
  169. # define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  170. #endif
  171. #if 3 <= KRML_UNROLL_MAX
  172. # define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x)
  173. #else
  174. # define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  175. #endif
  176. #if 4 <= KRML_UNROLL_MAX
  177. # define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x)
  178. #else
  179. # define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  180. #endif
  181. #if 5 <= KRML_UNROLL_MAX
  182. # define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x)
  183. #else
  184. # define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  185. #endif
  186. #if 6 <= KRML_UNROLL_MAX
  187. # define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x)
  188. #else
  189. # define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  190. #endif
  191. #if 7 <= KRML_UNROLL_MAX
  192. # define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x)
  193. #else
  194. # define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  195. #endif
  196. #if 8 <= KRML_UNROLL_MAX
  197. # define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x)
  198. #else
  199. # define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  200. #endif
  201. #if 9 <= KRML_UNROLL_MAX
  202. # define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x)
  203. #else
  204. # define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  205. #endif
  206. #if 10 <= KRML_UNROLL_MAX
  207. # define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x)
  208. #else
  209. # define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  210. #endif
  211. #if 11 <= KRML_UNROLL_MAX
  212. # define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x)
  213. #else
  214. # define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  215. #endif
  216. #if 12 <= KRML_UNROLL_MAX
  217. # define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x)
  218. #else
  219. # define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  220. #endif
  221. #if 13 <= KRML_UNROLL_MAX
  222. # define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x)
  223. #else
  224. # define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  225. #endif
  226. #if 14 <= KRML_UNROLL_MAX
  227. # define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x)
  228. #else
  229. # define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  230. #endif
  231. #if 15 <= KRML_UNROLL_MAX
  232. # define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x)
  233. #else
  234. # define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  235. #endif
  236. #if 16 <= KRML_UNROLL_MAX
  237. # define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x)
  238. #else
  239. # define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
  240. #endif
  241. #endif