1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
2 Licensed under the Apache 2.0 License. */
3
4 #ifndef __KREMLIN_TARGET_H
5 #define __KREMLIN_TARGET_H
6
7 #include <stdlib.h>
8 #include <stdio.h>
9 #include <stdbool.h>
10 #include <inttypes.h>
11 #include <limits.h>
12
13 #include "kremlin/internal/callconv.h"
14
15 /******************************************************************************/
16 /* Macros that KreMLin will generate. */
17 /******************************************************************************/
18
19 /* For "bare" targets that do not have a C stdlib, the user might want to use
20 * [-add-early-include '"mydefinitions.h"'] and override these. */
21 #ifndef KRML_HOST_PRINTF
22 # define KRML_HOST_PRINTF printf
23 #endif
24
25 #if ( \
26 (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
27 (!(defined KRML_HOST_EPRINTF)))
28 # define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
29 #endif
30
31 #ifndef KRML_HOST_EXIT
32 # define KRML_HOST_EXIT exit
33 #endif
34
35 #ifndef KRML_HOST_MALLOC
36 # define KRML_HOST_MALLOC malloc
37 #endif
38
39 #ifndef KRML_HOST_CALLOC
40 # define KRML_HOST_CALLOC calloc
41 #endif
42
43 #ifndef KRML_HOST_FREE
44 # define KRML_HOST_FREE free
45 #endif
46
47 #ifndef KRML_HOST_TIME
48
49 # include <time.h>
50
51 /* Prims_nat not yet in scope */
krml_time()52 inline static int32_t krml_time() {
53 return (int32_t)time(NULL);
54 }
55
56 # define KRML_HOST_TIME krml_time
57 #endif
58
59 /* In statement position, exiting is easy. */
60 #define KRML_EXIT \
61 do { \
62 KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \
63 KRML_HOST_EXIT(254); \
64 } while (0)
65
66 /* In expression position, use the comma-operator and a malloc to return an
67 * expression of the right size. KreMLin passes t as the parameter to the macro.
68 */
69 #define KRML_EABORT(t, msg) \
70 (KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \
71 KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t))))
72
73 /* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
74 * *elements*. Do an ugly, run-time check (some of which KreMLin can eliminate).
75 */
76
77 #ifdef __GNUC__
78 # define _KRML_CHECK_SIZE_PRAGMA \
79 _Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
80 #else
81 # define _KRML_CHECK_SIZE_PRAGMA
82 #endif
83
84 #define KRML_CHECK_SIZE(size_elt, sz) \
85 do { \
86 _KRML_CHECK_SIZE_PRAGMA \
87 if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \
88 KRML_HOST_PRINTF( \
89 "Maximum allocatable size exceeded, aborting before overflow at " \
90 "%s:%d\n", \
91 __FILE__, __LINE__); \
92 KRML_HOST_EXIT(253); \
93 } \
94 } while (0)
95
96 #if defined(_MSC_VER) && _MSC_VER < 1900
97 # define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
98 #else
99 # define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
100 #endif
101
102 #endif
103