| /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. |
| Licensed under the Apache 2.0 License. */ |
| |
| #ifndef FSTAR_UINT128_STRUCT_ENDIANNESS_H |
| #define FSTAR_UINT128_STRUCT_ENDIANNESS_H |
| |
| /* Hand-written implementation of endianness-related uint128 functions |
| * for the extracted uint128 implementation */ |
| |
| /* Access 64-bit fields within the int128. */ |
| #define HIGH64_OF(x) ((x)->high) |
| #define LOW64_OF(x) ((x)->low) |
| |
| /* A series of definitions written using pointers. */ |
| |
| inline static void |
| load128_le_(uint8_t *b, uint128_t *r) |
| { |
| LOW64_OF(r) = load64_le(b); |
| HIGH64_OF(r) = load64_le(b + 8); |
| } |
| |
| inline static void |
| store128_le_(uint8_t *b, uint128_t *n) |
| { |
| store64_le(b, LOW64_OF(n)); |
| store64_le(b + 8, HIGH64_OF(n)); |
| } |
| |
| inline static void |
| load128_be_(uint8_t *b, uint128_t *r) |
| { |
| HIGH64_OF(r) = load64_be(b); |
| LOW64_OF(r) = load64_be(b + 8); |
| } |
| |
| inline static void |
| store128_be_(uint8_t *b, uint128_t *n) |
| { |
| store64_be(b, HIGH64_OF(n)); |
| store64_be(b + 8, LOW64_OF(n)); |
| } |
| |
| #ifndef KRML_NOSTRUCT_PASSING |
| |
| inline static uint128_t |
| load128_le(uint8_t *b) |
| { |
| uint128_t r; |
| load128_le_(b, &r); |
| return r; |
| } |
| |
| inline static void |
| store128_le(uint8_t *b, uint128_t n) |
| { |
| store128_le_(b, &n); |
| } |
| |
| inline static uint128_t |
| load128_be(uint8_t *b) |
| { |
| uint128_t r; |
| load128_be_(b, &r); |
| return r; |
| } |
| |
| inline static void |
| store128_be(uint8_t *b, uint128_t n) |
| { |
| store128_be_(b, &n); |
| } |
| |
| #else /* !defined(KRML_STRUCT_PASSING) */ |
| |
| #define print128 print128_ |
| #define load128_le load128_le_ |
| #define store128_le store128_le_ |
| #define load128_be load128_be_ |
| #define store128_be store128_be_ |
| |
| #endif /* KRML_STRUCT_PASSING */ |
| |
| #endif |
