/* 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