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