summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/nostd/arch/x86/sail_spinlock.S68
-rw-r--r--lib/nostd/sail.c119
-rw-r--r--lib/nostd/sail.h12
-rw-r--r--lib/nostd/sail_alloc.h2
-rw-r--r--lib/nostd/sail_arena.c16
-rw-r--r--lib/nostd/sail_spinlock.h10
-rw-r--r--lib/nostd/stubs/sail_failure.c8
-rw-r--r--lib/nostd/test/test.c38
-rw-r--r--lib/string.sail4
-rw-r--r--src/jib/c_backend.ml2
10 files changed, 248 insertions, 31 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
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 1b949a20..4f0770ff 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -195,7 +195,7 @@ let rec is_stack_ctyp ctyp = match ctyp with
| CT_fint n -> n <= 64
| CT_lint when !optimize_fixed_int -> true
| CT_lint -> false
- | CT_lbits _ when !optimize_fixed_int -> true
+ | CT_lbits _ when !optimize_fixed_bits -> true
| CT_lbits _ -> false
| CT_real | CT_string | CT_list _ | CT_vector _ -> false
| CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 08:27:46 +0000