1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
2 Licensed under the Apache 2.0 License. */
3
4 #ifndef FSTAR_UINT128_STRUCT_ENDIANNESS_H
5 #define FSTAR_UINT128_STRUCT_ENDIANNESS_H
6
7 /* Hand-written implementation of endianness-related uint128 functions
8 * for the extracted uint128 implementation */
9
10 /* Access 64-bit fields within the int128. */
11 #define HIGH64_OF(x) ((x)->high)
12 #define LOW64_OF(x) ((x)->low)
13
14 /* A series of definitions written using pointers. */
15
load128_le_(uint8_t * b,uint128_t * r)16 inline static void load128_le_(uint8_t *b, uint128_t *r) {
17 LOW64_OF(r) = load64_le(b);
18 HIGH64_OF(r) = load64_le(b + 8);
19 }
20
store128_le_(uint8_t * b,uint128_t * n)21 inline static void store128_le_(uint8_t *b, uint128_t *n) {
22 store64_le(b, LOW64_OF(n));
23 store64_le(b + 8, HIGH64_OF(n));
24 }
25
load128_be_(uint8_t * b,uint128_t * r)26 inline static void load128_be_(uint8_t *b, uint128_t *r) {
27 HIGH64_OF(r) = load64_be(b);
28 LOW64_OF(r) = load64_be(b + 8);
29 }
30
store128_be_(uint8_t * b,uint128_t * n)31 inline static void store128_be_(uint8_t *b, uint128_t *n) {
32 store64_be(b, HIGH64_OF(n));
33 store64_be(b + 8, LOW64_OF(n));
34 }
35
36 #ifndef KRML_NOSTRUCT_PASSING
37
load128_le(uint8_t * b)38 inline static uint128_t load128_le(uint8_t *b) {
39 uint128_t r;
40 load128_le_(b, &r);
41 return r;
42 }
43
store128_le(uint8_t * b,uint128_t n)44 inline static void store128_le(uint8_t *b, uint128_t n) {
45 store128_le_(b, &n);
46 }
47
load128_be(uint8_t * b)48 inline static uint128_t load128_be(uint8_t *b) {
49 uint128_t r;
50 load128_be_(b, &r);
51 return r;
52 }
53
store128_be(uint8_t * b,uint128_t n)54 inline static void store128_be(uint8_t *b, uint128_t n) {
55 store128_be_(b, &n);
56 }
57
58 #else /* !defined(KRML_STRUCT_PASSING) */
59
60 # define print128 print128_
61 # define load128_le load128_le_
62 # define store128_le store128_le_
63 # define load128_be load128_be_
64 # define store128_be store128_be_
65
66 #endif /* KRML_STRUCT_PASSING */
67
68 #endif
69