CoCalc -- target.h

GitHub Repository: allendowney/cpython
Path: blob/main/Modules/_hacl/include/krml/internal/target.h
¹² views
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
267

268
Product

Resources

Company
