mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

include paths

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-04 17:18:13 -07:00
parent 95797c84b0
commit ab11d8fff2
13 changed files with 28 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

68
src/math/bigfix/fstar_uint128_struct_endianness.h Normal file
View file

@ -0,0 +1,68 @@
/* 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