/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. Licensed under the Apache 2.0 and MIT Licenses. */ #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 … #endif #if ( \ (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \ (!(defined KRML_HOST_EPRINTF))) #define KRML_HOST_EPRINTF(...) … #elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER) #define KRML_HOST_EPRINTF … #endif #ifndef KRML_HOST_EXIT #define KRML_HOST_EXIT … #endif #ifndef KRML_HOST_MALLOC #define KRML_HOST_MALLOC … #endif #ifndef KRML_HOST_CALLOC #define KRML_HOST_CALLOC … #endif #ifndef KRML_HOST_FREE #define KRML_HOST_FREE … #endif #ifndef KRML_HOST_IGNORE #define KRML_HOST_IGNORE(x) … #endif #ifndef KRML_MAYBE_UNUSED_VAR #define KRML_MAYBE_UNUSED_VAR(x) … #endif #ifndef KRML_MAYBE_UNUSED # if defined(__GNUC__) #define KRML_MAYBE_UNUSED … # else #define KRML_MAYBE_UNUSED # endif #endif #ifndef KRML_ATTRIBUTE_TARGET # if defined(__GNUC__) #define KRML_ATTRIBUTE_TARGET(x) … # else #define KRML_ATTRIBUTE_TARGET … # endif #endif #ifndef KRML_NOINLINE # if defined(_MSC_VER) #define KRML_NOINLINE … # elif defined (__GNUC__) #define KRML_NOINLINE … # elif defined (__SUNPRO_C) #define KRML_NOINLINE … # 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 #ifndef KRML_MUSTINLINE # if defined(_MSC_VER) #define KRML_MUSTINLINE … # elif defined (__GNUC__) #define KRML_MUSTINLINE … # elif defined (__SUNPRO_C) #define KRML_MUSTINLINE … # else #define KRML_MUSTINLINE … # warning "The KRML_MUSTINLINE macro defaults to plain inline for this toolchain!" # warning "Please locate target.h and try to fill it out with a suitable definition for this compiler." # endif #endif #ifndef KRML_PRE_ALIGN # ifdef _MSC_VER #define KRML_PRE_ALIGN … # else #define KRML_PRE_ALIGN(X) … # endif #endif #ifndef KRML_POST_ALIGN # ifdef _MSC_VER #define KRML_POST_ALIGN … # else #define KRML_POST_ALIGN(X) … # endif #endif /* MinGW-W64 does not support C11 aligned_alloc, but it supports * MSVC's _aligned_malloc. */ #ifndef KRML_ALIGNED_MALLOC # ifdef __MINGW32__ # include <_mingw.h> # endif # if ( \ defined(_MSC_VER) || \ (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR))) #define KRML_ALIGNED_MALLOC … # else #define KRML_ALIGNED_MALLOC(X, Y) … # endif #endif /* Since aligned allocations with MinGW-W64 are done with * _aligned_malloc (see above), such pointers must be freed with * _aligned_free. */ #ifndef KRML_ALIGNED_FREE # ifdef __MINGW32__ # include <_mingw.h> # endif # if ( \ defined(_MSC_VER) || \ (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR))) #define KRML_ALIGNED_FREE … # else #define KRML_ALIGNED_FREE(X) … # 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 … #else #define _KRML_CHECK_SIZE_PRAGMA #endif #define KRML_CHECK_SIZE(size_elt, sz) … /* Macros for prettier unrolling of loops */ #define KRML_LOOP1(i, n, x) … #define KRML_LOOP2(i, n, x) … #define KRML_LOOP3(i, n, x) … #define KRML_LOOP4(i, n, x) … #define KRML_LOOP5(i, n, x) … #define KRML_LOOP6(i, n, x) … #define KRML_LOOP7(i, n, x) … #define KRML_LOOP8(i, n, x) … #define KRML_LOOP9(i, n, x) … #define KRML_LOOP10(i, n, x) … #define KRML_LOOP11(i, n, x) … #define KRML_LOOP12(i, n, x) … #define KRML_LOOP13(i, n, x) … #define KRML_LOOP14(i, n, x) … #define KRML_LOOP15(i, n, x) … #define KRML_LOOP16(i, n, x) … #define KRML_UNROLL_FOR(i, z, n, k, x) … #define KRML_ACTUAL_FOR(i, z, n, k, x) … #ifndef KRML_UNROLL_MAX #define KRML_UNROLL_MAX … #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 … #endif #if 1 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR1(i, z, n, k, x) … #else #define KRML_MAYBE_FOR1 … #endif #if 2 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR2(i, z, n, k, x) … #else #define KRML_MAYBE_FOR2 … #endif #if 3 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR3(i, z, n, k, x) … #else #define KRML_MAYBE_FOR3 … #endif #if 4 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR4(i, z, n, k, x) … #else #define KRML_MAYBE_FOR4 … #endif #if 5 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR5(i, z, n, k, x) … #else #define KRML_MAYBE_FOR5 … #endif #if 6 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR6(i, z, n, k, x) … #else #define KRML_MAYBE_FOR6 … #endif #if 7 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR7(i, z, n, k, x) … #else #define KRML_MAYBE_FOR7 … #endif #if 8 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR8(i, z, n, k, x) … #else #define KRML_MAYBE_FOR8 … #endif #if 9 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR9(i, z, n, k, x) … #else #define KRML_MAYBE_FOR9 … #endif #if 10 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR10(i, z, n, k, x) … #else #define KRML_MAYBE_FOR10 … #endif #if 11 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR11(i, z, n, k, x) … #else #define KRML_MAYBE_FOR11 … #endif #if 12 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR12(i, z, n, k, x) … #else #define KRML_MAYBE_FOR12 … #endif #if 13 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR13(i, z, n, k, x) … #else #define KRML_MAYBE_FOR13 … #endif #if 14 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR14(i, z, n, k, x) … #else #define KRML_MAYBE_FOR14 … #endif #if 15 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR15(i, z, n, k, x) … #else #define KRML_MAYBE_FOR15 … #endif #if 16 <= KRML_UNROLL_MAX #define KRML_MAYBE_FOR16(i, z, n, k, x) … #else #define KRML_MAYBE_FOR16 … #endif #endif
Codebase Browser
cpython