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 <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 /* 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 #ifndef KRML_MAYBE_UNUSED_VAR 61 # define KRML_MAYBE_UNUSED_VAR(x) KRML_HOST_IGNORE(x) 62 #endif 63 64 #ifndef KRML_MAYBE_UNUSED 65 # if defined(__GNUC__) 66 # define KRML_MAYBE_UNUSED __attribute__((unused)) 67 # else 68 # define KRML_MAYBE_UNUSED 69 # endif 70 #endif 71 72 #ifndef KRML_NOINLINE 73 # if defined(_MSC_VER) 74 # define KRML_NOINLINE __declspec(noinline) 75 # elif defined (__GNUC__) 76 # define KRML_NOINLINE __attribute__((noinline,unused)) 77 # else 78 # define KRML_NOINLINE 79 # warning "The KRML_NOINLINE macro is not defined for this toolchain!" 80 # warning "The compiler may defeat side-channel resistance with optimizations." 81 # warning "Please locate target.h and try to fill it out with a suitable definition for this compiler." 82 # endif 83 #endif 84 85 /* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of 86 * *elements*. Do an ugly, run-time check (some of which KaRaMeL can eliminate). 87 */ 88 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4)) 89 # define _KRML_CHECK_SIZE_PRAGMA \ 90 _Pragma("GCC diagnostic ignored \"-Wtype-limits\"") 91 #else 92 # define _KRML_CHECK_SIZE_PRAGMA 93 #endif 94 95 #define KRML_CHECK_SIZE(size_elt, sz) \ 96 do { \ 97 _KRML_CHECK_SIZE_PRAGMA \ 98 if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \ 99 KRML_HOST_PRINTF( \ 100 "Maximum allocatable size exceeded, aborting before overflow at " \ 101 "%s:%d\n", \ 102 __FILE__, __LINE__); \ 103 KRML_HOST_EXIT(253); \ 104 } \ 105 } while (0) 106 107 /* Macros for prettier unrolling of loops */ 108 #define KRML_LOOP1(i, n, x) { \ 109 x \ 110 i += n; \ 111 (void) i; \ 112 } 113 114 #define KRML_LOOP2(i, n, x) \ 115 KRML_LOOP1(i, n, x) \ 116 KRML_LOOP1(i, n, x) 117 118 #define KRML_LOOP3(i, n, x) \ 119 KRML_LOOP2(i, n, x) \ 120 KRML_LOOP1(i, n, x) 121 122 #define KRML_LOOP4(i, n, x) \ 123 KRML_LOOP2(i, n, x) \ 124 KRML_LOOP2(i, n, x) 125 126 #define KRML_LOOP5(i, n, x) \ 127 KRML_LOOP4(i, n, x) \ 128 KRML_LOOP1(i, n, x) 129 130 #define KRML_LOOP6(i, n, x) \ 131 KRML_LOOP4(i, n, x) \ 132 KRML_LOOP2(i, n, x) 133 134 #define KRML_LOOP7(i, n, x) \ 135 KRML_LOOP4(i, n, x) \ 136 KRML_LOOP3(i, n, x) 137 138 #define KRML_LOOP8(i, n, x) \ 139 KRML_LOOP4(i, n, x) \ 140 KRML_LOOP4(i, n, x) 141 142 #define KRML_LOOP9(i, n, x) \ 143 KRML_LOOP8(i, n, x) \ 144 KRML_LOOP1(i, n, x) 145 146 #define KRML_LOOP10(i, n, x) \ 147 KRML_LOOP8(i, n, x) \ 148 KRML_LOOP2(i, n, x) 149 150 #define KRML_LOOP11(i, n, x) \ 151 KRML_LOOP8(i, n, x) \ 152 KRML_LOOP3(i, n, x) 153 154 #define KRML_LOOP12(i, n, x) \ 155 KRML_LOOP8(i, n, x) \ 156 KRML_LOOP4(i, n, x) 157 158 #define KRML_LOOP13(i, n, x) \ 159 KRML_LOOP8(i, n, x) \ 160 KRML_LOOP5(i, n, x) 161 162 #define KRML_LOOP14(i, n, x) \ 163 KRML_LOOP8(i, n, x) \ 164 KRML_LOOP6(i, n, x) 165 166 #define KRML_LOOP15(i, n, x) \ 167 KRML_LOOP8(i, n, x) \ 168 KRML_LOOP7(i, n, x) 169 170 #define KRML_LOOP16(i, n, x) \ 171 KRML_LOOP8(i, n, x) \ 172 KRML_LOOP8(i, n, x) 173 174 #define KRML_UNROLL_FOR(i, z, n, k, x) \ 175 do { \ 176 uint32_t i = z; \ 177 KRML_LOOP##n(i, k, x) \ 178 } while (0) 179 180 #define KRML_ACTUAL_FOR(i, z, n, k, x) \ 181 do { \ 182 for (uint32_t i = z; i < n; i += k) { \ 183 x \ 184 } \ 185 } while (0) 186 187 #ifndef KRML_UNROLL_MAX 188 # define KRML_UNROLL_MAX 16 189 #endif 190 191 /* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */ 192 #if 0 <= KRML_UNROLL_MAX 193 # define KRML_MAYBE_FOR0(i, z, n, k, x) 194 #else 195 # define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 196 #endif 197 198 #if 1 <= KRML_UNROLL_MAX 199 # define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x) 200 #else 201 # define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 202 #endif 203 204 #if 2 <= KRML_UNROLL_MAX 205 # define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x) 206 #else 207 # define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 208 #endif 209 210 #if 3 <= KRML_UNROLL_MAX 211 # define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x) 212 #else 213 # define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 214 #endif 215 216 #if 4 <= KRML_UNROLL_MAX 217 # define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x) 218 #else 219 # define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 220 #endif 221 222 #if 5 <= KRML_UNROLL_MAX 223 # define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x) 224 #else 225 # define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 226 #endif 227 228 #if 6 <= KRML_UNROLL_MAX 229 # define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x) 230 #else 231 # define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 232 #endif 233 234 #if 7 <= KRML_UNROLL_MAX 235 # define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x) 236 #else 237 # define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 238 #endif 239 240 #if 8 <= KRML_UNROLL_MAX 241 # define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x) 242 #else 243 # define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 244 #endif 245 246 #if 9 <= KRML_UNROLL_MAX 247 # define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x) 248 #else 249 # define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 250 #endif 251 252 #if 10 <= KRML_UNROLL_MAX 253 # define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x) 254 #else 255 # define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 256 #endif 257 258 #if 11 <= KRML_UNROLL_MAX 259 # define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x) 260 #else 261 # define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 262 #endif 263 264 #if 12 <= KRML_UNROLL_MAX 265 # define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x) 266 #else 267 # define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 268 #endif 269 270 #if 13 <= KRML_UNROLL_MAX 271 # define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x) 272 #else 273 # define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 274 #endif 275 276 #if 14 <= KRML_UNROLL_MAX 277 # define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x) 278 #else 279 # define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 280 #endif 281 282 #if 15 <= KRML_UNROLL_MAX 283 # define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x) 284 #else 285 # define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 286 #endif 287 288 #if 16 <= KRML_UNROLL_MAX 289 # define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x) 290 #else 291 # define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) 292 #endif 293 #endif 294