diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/nostd/arch/x86/sail_spinlock.S | 68 | ||||
| -rw-r--r-- | lib/nostd/sail.c | 119 | ||||
| -rw-r--r-- | lib/nostd/sail.h | 12 | ||||
| -rw-r--r-- | lib/nostd/sail_alloc.h | 2 | ||||
| -rw-r--r-- | lib/nostd/sail_arena.c | 16 | ||||
| -rw-r--r-- | lib/nostd/sail_spinlock.h | 10 | ||||
| -rw-r--r-- | lib/nostd/stubs/sail_failure.c | 8 | ||||
| -rw-r--r-- | lib/nostd/test/test.c | 38 | ||||
| -rw-r--r-- | lib/string.sail | 4 |
9 files changed, 247 insertions, 30 deletions
diff --git a/lib/nostd/arch/x86/sail_spinlock.S b/lib/nostd/arch/x86/sail_spinlock.S new file mode 100644 index 00000000..517a969d --- /dev/null +++ b/lib/nostd/arch/x86/sail_spinlock.S @@ -0,0 +1,68 @@ + +/* + * 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 00394e27..fc42f620 100644 --- a/lib/nostd/sail.c +++ b/lib/nostd/sail.c @@ -1,21 +1,110 @@ - -#ifndef SAIL_INT64 -#define SAIL_INT64 -#endif - -#ifndef SAIL_BITS64 -#define SAIL_BITS64 -#endif - #include <sail_alloc.h> #include <sail_failure.h> #include <sail.h> /* ********************************************************************** */ -/* Sail integers */ +/* Sail strings */ /* ********************************************************************** */ -#if defined(SAIL_INT64) || defined(SAIL_INT128) +/* + * Implementation is /incredibly/ inefficient... but we don't use + * strings that much anyway. A better implementation would not use + * char* due to immutability requirements, but that would make + * inter-operating with the C world harder. + */ + +void CREATE(sail_string)(sail_string *str) +{ + char *istr = (char *) sail_malloc(1 * sizeof(char)); + istr[0] = '\0'; + *str = istr; +} + +void RECREATE(sail_string)(sail_string *str) +{ + sail_free(*str); + char *istr = (char *) sail_malloc(1 * sizeof(char)); + istr[0] = '\0'; + *str = istr; +} + +size_t sail_strlen(const sail_string str) +{ + size_t i = 0; + while (true) { + if (str[i] == '\0') { + return i; + } + i++; + } +} + +char *sail_strcpy(char *dest, const char *src) +{ + size_t i; + for (i = 0; src[i] != '\0'; i++) { + dest[i] = src[i]; + } + dest[i] = '\0'; + return dest; +} + +int sail_strcmp(const char *str1, const char *str2) +{ + size_t i = 0; + while (true) { + if (str1[i] == str2[i]) { + i++; + } else { + return str1[i] - str2[i]; + } + } +} + +char *sail_strcat(char *dest, const char *src) +{ + size_t i = 0; + while (dest[i] != '\0') { + i++; + } + return sail_strcpy(dest + i, src); +} + +void COPY(sail_string)(sail_string *str1, const sail_string str2) +{ + size_t len = sail_strlen(str2); + *str1 = sail_realloc(*str1, len + 1); + *str1 = sail_strcpy(*str1, str2); +} + +void KILL(sail_string)(sail_string *str) +{ + sail_free(*str); +} + +bool eq_string(const sail_string str1, const sail_string str2) +{ + return sail_strcmp(str1, str2) == 0; +} + +bool EQUAL(sail_string)(const sail_string str1, const sail_string str2) +{ + return sail_strcmp(str1, str2) == 0; +} + +void undefined_string(sail_string *str, const unit u) {} + +void concat_str(sail_string *stro, const sail_string str1, const sail_string str2) +{ + *stro = sail_realloc(*stro, sail_strlen(str1) + sail_strlen(str2) + 1); + (*stro)[0] = '\0'; + sail_strcat(*stro, str1); + sail_strcat(*stro, str2); +} + +/* ********************************************************************** */ +/* Sail integers */ +/* ********************************************************************** */ sail_int CREATE_OF(sail_int, mach_int)(const mach_int op) { @@ -24,7 +113,7 @@ sail_int CREATE_OF(sail_int, mach_int)(const mach_int op) mach_int CREATE_OF(mach_int, sail_int)(const sail_int op) { - if (MACH_INT_MIN < op && op < MACH_INT_MAX) { + if (MACH_INT_MIN <= op && op <= MACH_INT_MAX) { return (mach_int) op; } else { sail_failure("Lost precision when converting from sail integer to machine integer"); @@ -34,7 +123,7 @@ mach_int CREATE_OF(mach_int, sail_int)(const sail_int op) mach_int CONVERT_OF(mach_int, sail_int)(const sail_int op) { - if (MACH_INT_MIN < op && op < MACH_INT_MAX) { + if (MACH_INT_MIN <= op && op <= MACH_INT_MAX) { return (mach_int) op; } else { sail_failure("Lost precision when converting from sail integer to machine integer"); @@ -246,10 +335,6 @@ sail_int pow2(const sail_int exp) return pow_int(2, exp); } -#else - -#endif - /* ********************************************************************** */ /* Sail bitvectors */ /* ********************************************************************** */ diff --git a/lib/nostd/sail.h b/lib/nostd/sail.h index f41f9bf6..fbc7b235 100644 --- a/lib/nostd/sail.h +++ b/lib/nostd/sail.h @@ -119,15 +119,15 @@ static inline bool EQUAL(mach_int)(const mach_int a, const mach_int b) * but MUCH faster. the SAIL_INT_FUNCTION macro allows defining * function prototypes that work for either case. */ -#if defined(SAIL_INT64) || defined(SAIL_INT64) +#if defined(SAIL_INT64) || defined(SAIL_INT128) #ifdef SAIL_INT64 typedef int64_t sail_int; #define SAIL_INT_MAX INT64_MAX #define SAIL_INT_MIN INT64_MIN #else typedef __int128 sail_int; -#define SAIL_INT_MAX INT128_MAX -#define SAIL_INT_MIN INT128_MIN +#define SAIL_INT_MAX (((__int128) 0x7FFFFFFFFFFFFFFF << 64) | (__int128) 0xFFFFFFFFFFFFFFFF) +#define SAIL_INT_MIN (~SAIL_INT_MAX) #endif #define SAIL_INT_FUNCTION(fname, ...) sail_int fname(__VA_ARGS__) #else @@ -136,7 +136,7 @@ typedef mpz_t sail_int; #endif SAIL_INT_FUNCTION(CREATE_OF(sail_int, mach_int), const mach_int); -SAIL_INT_FUNCTION(CREATE_OF(sail_int, sail_string, const sail_string); +SAIL_INT_FUNCTION(CREATE_OF(sail_int, sail_string), const sail_string); mach_int CREATE_OF(mach_int, sail_int)(const sail_int); SAIL_INT_FUNCTION(CONVERT_OF(sail_int, mach_int), const mach_int); @@ -192,7 +192,7 @@ SAIL_INT_FUNCTION(min_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(neg_int, const sail_int); SAIL_INT_FUNCTION(abs_int, const sail_int); SAIL_INT_FUNCTION(pow_int, const sail_int, const sail_int); -SAIL_INT_FUNCTION(pow2, sail_int, const sail_int); +SAIL_INT_FUNCTION(pow2, const sail_int); /* ********************************************************************** */ /* Sail bitvectors */ @@ -229,7 +229,7 @@ typedef struct { mpz_t *bits; } lbits; #define SAIL_BITS_FUNCTION(fname, ...) void fname(lbits*, __VA_ARGS__) -SAIL_BUILTIN_TYPE(lbits); +SAIL_BUILTIN_TYPE(lbits) #endif SAIL_BITS_FUNCTION(CREATE_OF(lbits, fbits), const fbits, const uint64_t, const bool); diff --git a/lib/nostd/sail_alloc.h b/lib/nostd/sail_alloc.h index 4a28e121..8dd2e7d5 100644 --- a/lib/nostd/sail_alloc.h +++ b/lib/nostd/sail_alloc.h @@ -5,6 +5,8 @@ void *sail_malloc(size_t size); +void *sail_realloc(void *ptr, size_t new_size); + void sail_free(void *ptr); #endif diff --git a/lib/nostd/sail_arena.c b/lib/nostd/sail_arena.c index 720b3a6d..f0ed5f90 100644 --- a/lib/nostd/sail_arena.c +++ b/lib/nostd/sail_arena.c @@ -1,26 +1,33 @@ #include <stdint.h> #include <sail_alloc.h> +#include <sail_spinlock.h> #include <sail_arena.h> static unsigned char *sail_arena_buffer; static size_t sail_arena_length; static size_t sail_arena_offset; +static volatile int 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; } void sail_arena_reset(void) { + sail_spin_lock(&sail_arena_lock); sail_arena_offset = 0; + sail_spin_unlock(&sail_arena_lock); } void *sail_malloc_align(size_t size, uintptr_t align) { + sail_spin_lock(&sail_arena_lock); + uintptr_t offset = (uintptr_t)sail_arena_buffer + (uintptr_t)sail_arena_offset; uintptr_t modulo = offset & (align - 1); @@ -33,9 +40,11 @@ void *sail_malloc_align(size_t size, uintptr_t align) void *ptr = &sail_arena_buffer[offset]; sail_arena_offset = offset + size; + sail_spin_unlock(&sail_arena_lock); return ptr; } + sail_spin_unlock(&sail_arena_lock); return NULL; } @@ -45,7 +54,12 @@ void *sail_malloc_align(size_t size, uintptr_t align) void *sail_malloc(size_t size) { - return sail_malloc_align(size, SAIL_ARENA_ALIGNMENT); + return sail_malloc_align(size, SAIL_ARENA_ALIGNMENT); +} + +void *sail_realloc(void *ptr, size_t new_size) +{ + return sail_malloc_align(new_size, SAIL_ARENA_ALIGNMENT); } void sail_free(void *ptr) {} diff --git a/lib/nostd/sail_spinlock.h b/lib/nostd/sail_spinlock.h new file mode 100644 index 00000000..5e776b46 --- /dev/null +++ b/lib/nostd/sail_spinlock.h @@ -0,0 +1,10 @@ +#ifndef __SAIL_SPINLOCK__ +#define __SAIL_SPINLOCK__ + +int sail_spin_unlock(volatile int *lock); + +int sail_spin_lock(volatile int *lock); + +int sail_spin_trylock(volatile int *lock); + +#endif diff --git a/lib/nostd/stubs/sail_failure.c b/lib/nostd/stubs/sail_failure.c index 029c42fb..06d3f53d 100644 --- a/lib/nostd/stubs/sail_failure.c +++ b/lib/nostd/stubs/sail_failure.c @@ -5,12 +5,16 @@ void sail_match_failure(char *message) { - fprintf(stderr, "Match failure: %s", message); + fprintf(stderr, "Match failure: %s\n", message); +#ifndef SAIL_NO_FAILURE exit(EXIT_FAILURE); +#endif } void sail_failure(char *message) { - fprintf(stderr, "Failure: %s", message); + fprintf(stderr, "Failure: %s\n", message); +#ifndef SAIL_NO_FAILURE exit(EXIT_FAILURE); +#endif } diff --git a/lib/nostd/test/test.c b/lib/nostd/test/test.c new file mode 100644 index 00000000..13eb0169 --- /dev/null +++ b/lib/nostd/test/test.c @@ -0,0 +1,38 @@ +#include <stdint.h> +#include <assert.h> +#include <gmp.h> + +#include <sail.h> + +int main(void) +{ +#ifdef SAIL_INT128 + /* Check that our 128-bit integer MIN/MAX macros do sensible things */ + assert(SAIL_INT_MAX > SAIL_INT_MIN); + assert(SAIL_INT_MAX > 0); + assert(SAIL_INT_MIN < 0); + assert(SAIL_INT_MIN - SAIL_INT_MIN == 0); + assert(SAIL_INT_MAX - SAIL_INT_MAX == 0); + assert((uint64_t) (SAIL_INT_MAX >> 64) == 0x7FFFFFFFFFFFFFFF); + assert((uint64_t) (SAIL_INT_MAX >> 127) == 0); + assert((uint64_t) (SAIL_INT_MAX >> 126) == 1); + assert((unsigned __int128) SAIL_INT_MAX + 1 == (unsigned __int128) SAIL_INT_MIN); + assert((__int128) ((unsigned __int128) SAIL_INT_MAX + 1) == SAIL_INT_MIN); + assert((__int128) ((unsigned __int128) SAIL_INT_MAX + 1) < 0); + assert((uint64_t) SAIL_INT_MAX == 0xFFFFFFFFFFFFFFFF); + + /* Expect precision failures */ + assert(CREATE_OF(mach_int, sail_int)(SAIL_INT_MAX) == -1); + assert(CREATE_OF(mach_int, sail_int)(SAIL_INT_MIN) == -1); + + /* Expect warnings for overflow/underflow */ + assert(add_int(SAIL_INT_MAX, SAIL_INT_MAX) == -1); //overflow + assert(add_int(SAIL_INT_MAX, 1) == -1); //overflow + assert(add_int(SAIL_INT_MAX, 0) == SAIL_INT_MAX); + assert(add_int(SAIL_INT_MIN, SAIL_INT_MIN) == -1); //underflow + assert(add_int(SAIL_INT_MIN, -1) == -1); //underflow + assert(add_int(SAIL_INT_MIN, 0) == SAIL_INT_MIN); +#endif + + return 0; +} diff --git a/lib/string.sail b/lib/string.sail index d5fe297e..9e6044b9 100644 --- a/lib/string.sail +++ b/lib/string.sail @@ -7,8 +7,6 @@ val eq_string = {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string overload operator == = {eq_string} -infixl 9 ^-^ - val concat_str = {coq: "String.append", lem: "stringAppend", _: "concat_str"} : (string, string) -> string val "dec_str" : int -> string @@ -25,8 +23,6 @@ val concat_str_dec : (string, int) -> string function concat_str_dec(str, x) = concat_str(str, dec_str(x)) -overload operator ^-^ = {concat_str, concat_str_bits, concat_str_dec} - val print_endline = "print_endline" : string -> unit val prerr_endline = "prerr_endline" : string -> unit |