diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/nostd/arch/x86/sail_spinlock.S | 68 | ||||
| -rw-r--r-- | lib/nostd/sail.c | 220 | ||||
| -rw-r--r-- | lib/nostd/sail.h | 159 | ||||
| -rw-r--r-- | lib/nostd/sail_arena.c | 4 | ||||
| -rw-r--r-- | lib/nostd/sail_failure.h | 7 | ||||
| -rw-r--r-- | lib/nostd/sail_spinlock.h | 44 | ||||
| -rw-r--r-- | lib/nostd/stubs/sail_failure.c | 12 |
7 files changed, 437 insertions, 77 deletions
diff --git a/lib/nostd/arch/x86/sail_spinlock.S b/lib/nostd/arch/x86/sail_spinlock.S deleted file mode 100644 index 517a969d..00000000 --- a/lib/nostd/arch/x86/sail_spinlock.S +++ /dev/null @@ -1,68 +0,0 @@ - -/* - * Enabling and disabling interrupts setting is clearly not going - * to be very useful for running on x86 in Linux userspace, but - * mostly here just to think about what we might need for ARM - */ -.macro enable_interrupts -#ifdef SAIL_DISABLE_INTERRUPTS - sti -#endif -.endm - -.macro disable_interrupts -#ifdef SAIL_DISABLE_INTERRUPTS - cli -#endif -.endm - -sail_spin_unlock: - movl $1, (%rdi) - xorl %eax, %eax - enable_interrupts - ret - - .globl sail_spin_unlock - -/* Attempt to aquire the lock. zero flag will be set on success, otherwise set */ -.macro acquire reg, mem - disable_interrupts - movl $0, \reg - xchgl \reg, \mem - cmpl $1, \reg -.endm - -sail_spin_lock: - /* If the value pointed to by %rdi is equal to 0 (locked), then spin */ - cmpl $0, (%rdi) - je .spin -.acquire: - acquire %eax, (%rdi) -#ifdef SAIL_DISABLE_INTERRUPTS - jnz .failed -#else - jnz .spin -#endif - xorl %eax, %eax - ret -.failed: - enable_interrupts -.spin: - pause - cmpl $0, (%rdi) - je .spin - jmp .acquire - - .globl sail_spin_lock - -sail_spin_trylock: - acquire %eax, (%rdi) - jnz .failed_try - xorl %eax, %eax - ret -.failed_try: - enable_interrupts - movl $1, %eax - ret - - .globl sail_spin_trylock diff --git a/lib/nostd/sail.c b/lib/nostd/sail.c index fc42f620..d25f5eae 100644 --- a/lib/nostd/sail.c +++ b/lib/nostd/sail.c @@ -2,6 +2,7 @@ #include <sail_failure.h> #include <sail.h> + /* ********************************************************************** */ /* Sail strings */ /* ********************************************************************** */ @@ -338,3 +339,222 @@ sail_int pow2(const sail_int exp) /* ********************************************************************** */ /* Sail bitvectors */ /* ********************************************************************** */ + +lbits CONVERT_OF(lbits, fbits)(const fbits op, const uint64_t len, const bool order) +{ + lbits rop; + rop.len = len; + rop.bits = op; + return rop; +} + +fbits CONVERT_OF(fbits, lbits)(const lbits op, const bool direction) +{ + return op.bits; +} + +sbits CONVERT_OF(sbits, lbits)(const lbits op, const bool order) +{ + return op; +} + +lbits CONVERT_OF(lbits, sbits)(const sbits op, const bool order) +{ + return op; +} + +lbits UNDEFINED(lbits)(const sail_int len) +{ + lbits rop; + rop.bits = 0; + rop.len = (uint64_t) len; + return rop; +} + +bool eq_bits(const lbits op1, const lbits op2) +{ + return op1.bits == op2.bits; +} + +bool EQUAL(lbits)(const lbits op1, const lbits op2) +{ + return op1.bits == op2.bits; +} + +bool neq_bits(const lbits op1, const lbits op2) +{ + return op1.bits != op2.bits; +} + +lbits not_bits(const lbits op) +{ + lbits rop; + rop.bits = (~op.bits) & sail_bzhi_u64(UINT64_MAX, op.len); + rop.len = op.len; + return rop; +} + +lbits and_bits(const lbits op1, const lbits op2) +{ + lbits rop; + rop.bits = op1.bits & op2.bits; + rop.len = op1.len; + return rop; +} + +lbits or_bits(const lbits op1, const lbits op2) +{ + lbits rop; + rop.bits = op1.bits | op2.bits; + rop.len = op1.len; + return rop; +} + +lbits xor_bits(const lbits op1, const lbits op2) +{ + lbits rop; + rop.bits = op1.bits ^ op2.bits; + rop.len = op1.len; + return rop; +} + +lbits add_bits(const lbits op1, const lbits op2) +{ + lbits rop; + rop.bits = (op1.bits + op2.bits) & sail_bzhi_u64(UINT64_MAX, op1.len); + rop.len = op1.len; + return rop; +} + +lbits sub_bits(const lbits op1, const lbits op2) +{ + lbits rop; + rop.bits = (op1.bits - op2.bits) & sail_bzhi_u64(UINT64_MAX, op1.len); + rop.len = op1.len; + return rop; +} + +lbits add_bits_int(const lbits op1, const sail_int op2) +{ + lbits rop; + rop.bits = (op1.bits + ((uint64_t) op2)) & sail_bzhi_u64(UINT64_MAX, op1.len); + rop.len = op1.len; + return rop; +} + + +lbits sub_bits_int(const lbits op1, const sail_int op2) +{ + lbits rop; + rop.bits = (op1.bits - ((uint64_t) op2)) & sail_bzhi_u64(UINT64_MAX, op1.len); + rop.len = op1.len; + return rop; +} + +sail_int sail_unsigned(const lbits op) +{ + return (sail_int) op.bits; +} + +sail_int sail_signed(const lbits op) +{ + return (sail_int) ((int64_t) op.bits); +} + +fbits bitvector_access(const lbits bv, const sail_int n) +{ + return 1 & (bv.bits >> ((uint64_t) n)); +} + +lbits slice(const lbits op, const sail_int start, const sail_int len) +{ + uint64_t l = len; + lbits rop; + rop.bits = sail_bzhi_u64(op.bits >> ((uint64_t) start), l); + rop.len = l; + return rop; +} + +lbits set_slice(const sail_int len, + const sail_int slen, + const lbits op, + const sail_int start, + const lbits slice) +{ + uint64_t s = start; + uint64_t mask = (1 << (uint64_t) slen) - 1; + lbits rop; + rop.len = op.len; + rop.bits = op.bits; + rop.bits &= ~(mask << s); + rop.bits |= slice.bits << s; + return rop; +} + +lbits append(const lbits op1, const lbits op2) +{ + lbits rop; + rop.bits = (op1.bits << op2.len) | op2.bits; + rop.len = op1.len + op2.len; + return rop; +} + +sail_int length_lbits(const lbits op) +{ + return (sail_int) op.len; +} + +lbits zeros(const sail_int len) +{ + lbits rop; + rop.bits = 0; + rop.len = (uint64_t) len; + return rop; +} + +lbits replicate_bits(const lbits op, const sail_int n) +{ + return op; +} + +lbits get_slice_int(const sail_int len, const sail_int n, const sail_int start) +{ + return zeros(len); +} + +sail_int set_slice_int(const sail_int len, const sail_int n, const sail_int start, const lbits slice) +{ + return n; +} + +lbits vector_subrange_lbits(const lbits op, const sail_int n, const sail_int m) +{ + return op; +} + +lbits vector_update_subrange_lbits(const lbits op, const sail_int n, const sail_int m, const lbits slice) +{ + return op; +} + +/* ********************************************************************** */ +/* Sail reals */ +/* ********************************************************************** */ + +void CREATE(real)(double *r) {} +void KILL(real)(double *r) {} + +void to_real(real *rop, const sail_int op) +{ + *rop = (double) op; +} + +void div_real(real *rop, const real op1, const real op2) +{ + *rop = op1 / op2; +} + +sail_int round_up(const real op) +{ + return (sail_int) op; +} diff --git a/lib/nostd/sail.h b/lib/nostd/sail.h index fbc7b235..d553e6b3 100644 --- a/lib/nostd/sail.h +++ b/lib/nostd/sail.h @@ -8,6 +8,19 @@ #include <stdint.h> #include <stdbool.h> +#ifdef SAIL_X86INTRIN +#include <x64intrin.h> +#endif + +static inline uint64_t sail_bzhi_u64(uint64_t op1, uint64_t op2) +{ +#ifdef SAIL_X64INTRIN + return _bzhi_u64(op1, op2); +#else + return (op1 << (64 - op2)) >> (64 - op2); +#endif +} + /* * The Sail compiler expects functions to follow a specific naming * convention for allocation, deallocation, and (deep)-copying. These @@ -95,8 +108,6 @@ bool EQUAL(sail_string)(const sail_string, const sail_string); void concat_str(sail_string *stro, const sail_string str1, const sail_string str2); bool string_startswith(sail_string s, sail_string prefix); -unit sail_assert(bool, sail_string); - /* ********************************************************************** */ /* Sail integers */ /* ********************************************************************** */ @@ -120,6 +131,7 @@ static inline bool EQUAL(mach_int)(const mach_int a, const mach_int b) * function prototypes that work for either case. */ #if defined(SAIL_INT64) || defined(SAIL_INT128) + #ifdef SAIL_INT64 typedef int64_t sail_int; #define SAIL_INT_MAX INT64_MAX @@ -130,9 +142,22 @@ typedef __int128 sail_int; #define SAIL_INT_MIN (~SAIL_INT_MAX) #endif #define SAIL_INT_FUNCTION(fname, ...) sail_int fname(__VA_ARGS__) + +static inline uint64_t sail_int_get_ui(const sail_int op) +{ + return (uint64_t) op; +} + #else + typedef mpz_t sail_int; #define SAIL_INT_FUNCTION(fname, ...) void fname(sail_int*, __VA_ARGS__) + +static inline uint64_t sail_int_get_ui(const sail_int op) +{ + return (uint64_t) mpz_get_ui(op); +} + #endif SAIL_INT_FUNCTION(CREATE_OF(sail_int, mach_int), const mach_int); @@ -210,6 +235,20 @@ SAIL_INT_FUNCTION(pow2, const sail_int); typedef uint64_t fbits; +static inline bool EQUAL(fbits)(const fbits op1, const fbits op2) +{ + return op1 == op2; +} + +static inline fbits safe_rshift(const fbits x, const fbits n) +{ + if (n >= 64) { + return 0; + } else { + return x >> n; + } +} + /* * For backwards compatability with older Sail C libraries */ @@ -220,21 +259,133 @@ typedef struct { uint64_t bits; } sbits; +static inline sbits CONVERT_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool order) +{ + sbits rop; + rop.len = len; + rop.bits = op; + return rop; +} + +static inline fbits CONVERT_OF(fbits, sbits)(const sbits op, const bool order) +{ + return op.bits; +} + +/* + * If the SAIL_BITS64 symbol is defined, we will use sbits as the + * lbits type. + */ + #ifdef SAIL_BITS64 + typedef sbits lbits; #define SAIL_BITS_FUNCTION(fname, ...) lbits fname(__VA_ARGS__) + +static inline lbits CREATE_OF(lbits, fbits)(const fbits op, const uint64_t len, const bool order) +{ + lbits rop; + rop.bits = op; + rop.len = len; + return rop; +} + +static inline lbits CREATE_OF(lbits, sbits)(const sbits op, const bool order) +{ + return op; +} + #else + typedef struct { mp_bitcnt_t len; mpz_t *bits; } lbits; #define SAIL_BITS_FUNCTION(fname, ...) void fname(lbits*, __VA_ARGS__) SAIL_BUILTIN_TYPE(lbits) -#endif SAIL_BITS_FUNCTION(CREATE_OF(lbits, fbits), const fbits, const uint64_t, const bool); -SAIL_BITS_FUNCTION(RECREATE_OF(lbits, fbits), const fbits, const uint64_t, const bool); SAIL_BITS_FUNCTION(CREATE_OF(lbits, sbits), const fbits, const bool); +SAIL_BITS_FUNCTION(RECREATE_OF(lbits, fbits), const fbits, const uint64_t, const bool); SAIL_BITS_FUNCTION(RECREATE_OF(lbits, sbits), const fbits, const bool); #endif + +SAIL_BITS_FUNCTION(CONVERT_OF(lbits, fbits), const fbits, const uint64_t, const bool); +fbits CONVERT_OF(fbits, lbits)(const lbits, const bool); +SAIL_BITS_FUNCTION(CONVERT_OF(lbits, sbits), const sbits, const bool); +sbits CONVERT_OF(sbits, lbits)(const lbits, const bool); + +SAIL_BITS_FUNCTION(UNDEFINED(lbits), const sail_int); + +bool eq_bits(const lbits, const lbits); +bool EQUAL(lbits)(const lbits, const lbits); +bool neq_bits(const lbits, const lbits); + +SAIL_BITS_FUNCTION(not_bits, const lbits); +SAIL_BITS_FUNCTION(and_bits, const lbits, const lbits); +SAIL_BITS_FUNCTION(or_bits, const lbits, const lbits); +SAIL_BITS_FUNCTION(xor_bits, const lbits, const lbits); + +SAIL_BITS_FUNCTION(add_bits, const lbits, const lbits); +SAIL_BITS_FUNCTION(sub_bits, const lbits, const lbits); +SAIL_BITS_FUNCTION(add_bits_int, const lbits, const sail_int); +SAIL_BITS_FUNCTION(sub_bits_int, const lbits, const sail_int); + +SAIL_INT_FUNCTION(sail_signed, const lbits op); +SAIL_INT_FUNCTION(sail_unsigned, const lbits op); + +fbits bitvector_access(const lbits bv, const sail_int n); +SAIL_BITS_FUNCTION(slice, const lbits, const sail_int, const sail_int); +SAIL_BITS_FUNCTION(set_slice, const sail_int len, const sail_int slen, const lbits op, const sail_int start, const lbits slice); +SAIL_BITS_FUNCTION(append, const lbits, const lbits); +SAIL_INT_FUNCTION(length_lbits, const lbits); +SAIL_BITS_FUNCTION(zeros, const sail_int); +SAIL_BITS_FUNCTION(replicate_bits, const lbits op, const sail_int n); +SAIL_BITS_FUNCTION(get_slice_int, const sail_int len, const sail_int n, const sail_int start); +SAIL_INT_FUNCTION(set_slice_int, const sail_int len, const sail_int n, const sail_int start, const lbits slice); +SAIL_BITS_FUNCTION(vector_subrange_lbits, const lbits op, const sail_int n, const sail_int m); +SAIL_BITS_FUNCTION(vector_update_subrange_lbits, const lbits op, const sail_int n, const sail_int m, const lbits slice); + +/* ********************************************************************** */ +/* Sail reals */ +/* ********************************************************************** */ + +#ifdef SAIL_FLOATING_REAL +typedef double real; +#else +typedef mpq_t real; +#endif + +SAIL_BUILTIN_TYPE(real); + +void CREATE_OF(real, sail_string)(real *rop, const sail_string op); +void CONVERT_OF(real, sail_string)(real *rop, const sail_string op); + +void UNDEFINED(real)(real *rop, unit u); + +void neg_real(real *rop, const real op); + +void mult_real(real *rop, const real op1, const real op2); +void sub_real(real *rop, const real op1, const real op2); +void add_real(real *rop, const real op1, const real op2); +void div_real(real *rop, const real op1, const real op2); + +void sqrt_real(real *rop, const real op); +void abs_real(real *rop, const real op); + +SAIL_INT_FUNCTION(round_up, const real op); +SAIL_INT_FUNCTION(round_down, const real op); + +void to_real(real *rop, const sail_int op); + +bool EQUAL(real)(const real op1, const real op2); + +bool lt_real(const real op1, const real op2); +bool gt_real(const real op1, const real op2); +bool lteq_real(const real op1, const real op2); +bool gteq_real(const real op1, const real op2); + +void real_power(real *rop, const real base, const sail_int exp); + +#endif diff --git a/lib/nostd/sail_arena.c b/lib/nostd/sail_arena.c index f0ed5f90..d2bc17ac 100644 --- a/lib/nostd/sail_arena.c +++ b/lib/nostd/sail_arena.c @@ -7,14 +7,14 @@ static unsigned char *sail_arena_buffer; static size_t sail_arena_length; static size_t sail_arena_offset; -static volatile int sail_arena_lock; +static struct sail_spinlock sail_arena_lock; void sail_arena_init(void *buffer, size_t length) { sail_arena_buffer = buffer; sail_arena_length = length; sail_arena_offset = 0; - sail_arena_lock = 1; + sail_spin_init(&sail_arena_lock); } void sail_arena_reset(void) diff --git a/lib/nostd/sail_failure.h b/lib/nostd/sail_failure.h index fd339097..61ada596 100644 --- a/lib/nostd/sail_failure.h +++ b/lib/nostd/sail_failure.h @@ -1,6 +1,8 @@ #ifndef __SAIL_FAILURE__ #define __SAIL_FAILURE__ +#include <stdbool.h> + /* * Called when some builtin hits an unexpected case, such as overflow * when using 64- or 128-bit integers. @@ -12,4 +14,9 @@ void sail_failure(char *message); */ void sail_match_failure(char *message); +/* + * Implements the Sail assert construct + */ +int sail_assert(bool result, char *message); + #endif diff --git a/lib/nostd/sail_spinlock.h b/lib/nostd/sail_spinlock.h index 5e776b46..d69672dd 100644 --- a/lib/nostd/sail_spinlock.h +++ b/lib/nostd/sail_spinlock.h @@ -1,10 +1,48 @@ +/* + * Copyright 2018 The Hafnium Authors. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * https://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + #ifndef __SAIL_SPINLOCK__ #define __SAIL_SPINLOCK__ -int sail_spin_unlock(volatile int *lock); +#include <stdatomic.h> + +struct sail_spinlock { + atomic_flag v; +}; + +#define SPINLOCK_INIT \ + { \ + .v = ATOMIC_FLAG_INIT \ + } + +static inline void sail_spin_init(struct sail_spinlock *l) +{ + *l = (struct sail_spinlock)SPINLOCK_INIT; +} -int sail_spin_lock(volatile int *lock); +static inline void sail_spin_lock(struct sail_spinlock *l) +{ + while (atomic_flag_test_and_set_explicit(&l->v, memory_order_acquire)) { + /* do nothing */ + } +} -int sail_spin_trylock(volatile int *lock); +static inline void sail_spin_unlock(struct sail_spinlock *l) +{ + atomic_flag_clear_explicit(&l->v, memory_order_release); +} #endif diff --git a/lib/nostd/stubs/sail_failure.c b/lib/nostd/stubs/sail_failure.c index 06d3f53d..e6120ded 100644 --- a/lib/nostd/stubs/sail_failure.c +++ b/lib/nostd/stubs/sail_failure.c @@ -18,3 +18,15 @@ void sail_failure(char *message) exit(EXIT_FAILURE); #endif } + +int sail_assert(bool result, char *message) +{ + if (~result) { + fprintf(stderr, "Assert failed: %s\n", message); +#ifndef SAIL_NO_FAILURE + exit(EXIT_FAILURE); +#endif + return 0; + } + return 0; +} |