| /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. |
| Licensed under the Apache 2.0 License. */ |
| |
| #ifndef __KREMLIN_TARGET_H |
| #define __KREMLIN_TARGET_H |
| |
| #include <stdlib.h> |
| #include <stdio.h> |
| #include <stdbool.h> |
| #include <inttypes.h> |
| #include <limits.h> |
| |
| #include "kremlin/internal/callconv.h" |
| |
| /******************************************************************************/ |
| /* Macros that KreMLin 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 printf |
| #endif |
| |
| #if ( \ |
| (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \ |
| (!(defined KRML_HOST_EPRINTF))) |
| # define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__) |
| #endif |
| |
| #ifndef KRML_HOST_EXIT |
| # define KRML_HOST_EXIT exit |
| #endif |
| |
| #ifndef KRML_HOST_MALLOC |
| # define KRML_HOST_MALLOC malloc |
| #endif |
| |
| #ifndef KRML_HOST_CALLOC |
| # define KRML_HOST_CALLOC calloc |
| #endif |
| |
| #ifndef KRML_HOST_FREE |
| # define KRML_HOST_FREE free |
| #endif |
| |
| #ifndef KRML_HOST_TIME |
| |
| # include <time.h> |
| |
| /* Prims_nat not yet in scope */ |
| inline static int32_t krml_time() { |
| return (int32_t)time(NULL); |
| } |
| |
| # define KRML_HOST_TIME krml_time |
| #endif |
| |
| /* In statement position, exiting is easy. */ |
| #define KRML_EXIT \ |
| do { \ |
| KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \ |
| KRML_HOST_EXIT(254); \ |
| } while (0) |
| |
| /* In expression position, use the comma-operator and a malloc to return an |
| * expression of the right size. KreMLin passes t as the parameter to the macro. |
| */ |
| #define KRML_EABORT(t, msg) \ |
| (KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \ |
| KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t)))) |
| |
| /* 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 KreMLin can eliminate). |
| */ |
| |
| #ifdef __GNUC__ |
| # define _KRML_CHECK_SIZE_PRAGMA \ |
| _Pragma("GCC diagnostic ignored \"-Wtype-limits\"") |
| #else |
| # define _KRML_CHECK_SIZE_PRAGMA |
| #endif |
| |
| #define KRML_CHECK_SIZE(size_elt, sz) \ |
| do { \ |
| _KRML_CHECK_SIZE_PRAGMA \ |
| if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \ |
| KRML_HOST_PRINTF( \ |
| "Maximum allocatable size exceeded, aborting before overflow at " \ |
| "%s:%d\n", \ |
| __FILE__, __LINE__); \ |
| KRML_HOST_EXIT(253); \ |
| } \ |
| } while (0) |
| |
| #if defined(_MSC_VER) && _MSC_VER < 1900 |
| # define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg) |
| #else |
| # define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg) |
| #endif |
| |
| #endif |