1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */
#ifndef KRML_TYPES_H
#define KRML_TYPES_H
#include <inttypes.h>
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
/* Types which are either abstract, meaning that have to be implemented in C, or
* which are models, meaning that they are swapped out at compile-time for
* hand-written C types (in which case they're marked as noextract). */
typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_;
typedef int64_t FStar_Int64_t, FStar_Int64_t_;
typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_;
typedef int32_t FStar_Int32_t, FStar_Int32_t_;
typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_;
typedef int16_t FStar_Int16_t, FStar_Int16_t_;
typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_;
typedef int8_t FStar_Int8_t, FStar_Int8_t_;
/* Only useful when building Kremlib, because it's in the dependency graph of
* FStar.Int.Cast. */
typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
typedef int64_t FStar_Int63_t, FStar_Int63_t_;
typedef double FStar_Float_float;
typedef uint32_t FStar_Char_char;
typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;
typedef void *FStar_Dyn_dyn;
typedef const char *C_String_t, *C_String_t_, *C_Compat_String_t, *C_Compat_String_t_;
typedef int exit_code;
typedef FILE *channel;
typedef unsigned long long TestLib_cycles;
typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan;
/* Now Prims.string is no longer illegal with the new model in LowStar.Printf;
* it's operations that produce Prims_string which are illegal. Bring the
* definition into scope by default. */
typedef const char *Prims_string;
#if (defined(_MSC_VER) && defined(_M_X64) && !defined(__clang__))
#define IS_MSVC64 1
#endif
/* This code makes a number of assumptions and should be refined. In particular,
* it assumes that: any non-MSVC amd64 compiler supports int128. Maybe it would
* be easier to just test for defined(__SIZEOF_INT128__) only? */
#if (defined(__x86_64__) || \
defined(__x86_64) || \
defined(__aarch64__) || \
(defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) || \
defined(__s390x__) || \
(defined(_MSC_VER) && !defined(_M_X64) && defined(__clang__)) || \
(defined(__mips__) && defined(__LP64__)) || \
(defined(__riscv) && __riscv_xlen == 64) || \
defined(__SIZEOF_INT128__))
#define HAS_INT128 1
#endif
/* The uint128 type is a special case since we offer several implementations of
* it, depending on the compiler and whether the user wants the verified
* implementation or not. */
#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64)
#include <emmintrin.h>
typedef __m128i FStar_UInt128_uint128;
#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128)
typedef unsigned __int128 FStar_UInt128_uint128;
#else
typedef struct FStar_UInt128_uint128_s {
uint64_t low;
uint64_t high;
} FStar_UInt128_uint128;
#endif
/* The former is defined once, here (otherwise, conflicts for test-c89. The
* latter is for internal use. */
typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t;
#include "kremlin/lowstar_endianness.h"
#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64)
#include "fstar_uint128_msvc.h"
#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128)
#include "fstar_uint128_gcc64.h"
#else
#include "FStar_UInt128_Verified.h"
#include "fstar_uint128_struct_endianness.h"
#endif
#endif
|
