More work on bare-metal Sail

1 files changed, 134 insertions, 235 deletions

diff --git a/lib/nostd/sail.h b/lib/nostd/sail.h
index 52318a61..f41f9bf6 100644
--- a/lib/nostd/sail.h
+++ b/lib/nostd/sail.h
@@ -1,15 +1,13 @@
-#ifndef __SAIL_LIB
-#define __SAIL_LIB
+#ifndef __SAIL_LIB__
+#define __SAIL_LIB__
 
+/*
+ * Only use libraries here that work with -ffreestanding and -nostdlib
+ */
 #include <stddef.h>
 #include <stdint.h>
 #include <stdbool.h>
 
-void *sail_malloc(size_t);
-void sail_free(void *);
-
-void sail_match_failure(char *message);
-
 /*
  * The Sail compiler expects functions to follow a specific naming
  * convention for allocation, deallocation, and (deep)-copying. These
@@ -25,42 +23,69 @@ void sail_match_failure(char *message);
 #define UNDEFINED(type) undefined_ ## type
 #define EQUAL(type) eq_ ## type
 
+/*
+ * This is only needed for types that are not just simple C types that
+ * live on the stack, and need some kind of setup and teardown
+ * routines, as Sail won't use these otherwise.
+ */
 #define SAIL_BUILTIN_TYPE(type)\
   void create_ ## type(type *);\
   void recreate_ ## type(type *);\
   void copy_ ## type(type *, const type);\
   void kill_ ## type(type *);
 
-/* ***** Sail unit type ***** */
+/* ********************************************************************** */
+/* Sail unit type                                                         */
+/* ********************************************************************** */
 
 typedef int unit;
 
 #define UNIT 0
 
-unit UNDEFINED(unit)(const unit);
-bool EQUAL(unit)(const unit, const unit);
+static inline unit UNDEFINED(unit)(const unit u)
+{
+     return UNIT;
+}
 
-unit skip(const unit);
-unit sail_exit(const unit);
+static inline bool EQUAL(unit)(const unit u1, const unit u2)
+{
+     return true;
+}
 
-/* ***** Sail booleans ***** */
+/* ********************************************************************** */
+/* Sail booleans                                                          */
+/* ********************************************************************** */
 
 /*
  * and_bool and or_bool are special-cased by the compiler to ensure
- * short-circuiting evaluation.
+ * proper short-circuiting evaluation.
  */
-bool not(const bool);
-bool EQUAL(bool)(const bool, const bool);
-bool UNDEFINED(bool)(const unit);
 
-/* ***** Sail strings ***** */
+static inline bool not(const bool b)
+{
+     return !b;
+}
+
+static inline bool EQUAL(bool)(const bool a, const bool b)
+{
+     return a == b;
+}
+
+static inline bool UNDEFINED(bool)(const unit u)
+{
+     return false;
+}
+
+/* ********************************************************************** */
+/* Sail strings                                                           */
+/* ********************************************************************** */
 
 /*
  * Sail strings are just C strings.
  */
 typedef char *sail_string;
 
-SAIL_BUILTIN_TYPE(sail_string);
+SAIL_BUILTIN_TYPE(sail_string)
 
 void undefined_string(sail_string *str, const unit u);
 
@@ -72,29 +97,51 @@ bool string_startswith(sail_string s, sail_string prefix);
 
 unit sail_assert(bool, sail_string);
 
-/* ***** Sail integers ***** */
+/* ********************************************************************** */
+/* Sail integers                                                          */
+/* ********************************************************************** */
+
+/* First, we define a type for machine-precision integers, int64_t */
 
 typedef int64_t mach_int;
+#define MACH_INT_MAX INT64_MAX
+#define MACH_INT_MIN INT64_MIN
 
-bool EQUAL(mach_int)(const mach_int, const mach_int);
+static inline bool EQUAL(mach_int)(const mach_int a, const mach_int b)
+{
+     return a == b;
+}
 
+/*
+ * For arbitrary precision types, we define a type sail_int. Currently
+ * sail_int can either be using GMP arbitrary-precision integers
+ * (default) or using __int128 or int64_t which is potentially unsound
+ * but MUCH faster. the SAIL_INT_FUNCTION macro allows defining
+ * function prototypes that work for either case.
+ */
+#if defined(SAIL_INT64) || defined(SAIL_INT64)
+#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
+#endif
+#define SAIL_INT_FUNCTION(fname, ...) sail_int fname(__VA_ARGS__)
+#else
+typedef mpz_t sail_int;
+#define SAIL_INT_FUNCTION(fname, ...) void fname(sail_int*, __VA_ARGS__)
+#endif
 
-uint64_t sail_int_get_ui(const sail_int);
-
-void dec_str(sail_string *str, const sail_int n);
-void hex_str(sail_string *str, const sail_int n);
-
-#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__)
-
-// SAIL_BUILTIN_TYPE(sail_int);
-
-sail_int CREATE_OF(sail_int, mach_int)(const mach_int);
+SAIL_INT_FUNCTION(CREATE_OF(sail_int, mach_int), const mach_int);
+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);
+SAIL_INT_FUNCTION(CONVERT_OF(sail_int, sail_string), const sail_string);
 mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
-sail_int CONVERT_OF(sail_int, mach_int)(const mach_int);
-sail_int CONVERT_OF(sail_int, sail_string)(const sail_string);
 
 /*
  * Comparison operators for integers
@@ -112,230 +159,82 @@ bool gteq(const sail_int, const sail_int);
  */
 mach_int shl_mach_int(const mach_int, const mach_int);
 mach_int shr_mach_int(const mach_int, const mach_int);
-SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(shl_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(shr_int, const sail_int, const sail_int);
 
 /*
  * undefined_int and undefined_range can't use the UNDEFINED(TYPE)
  * macro, because they're slightly magical. They take extra parameters
- * to ensure that no undefined int can violate any type-guaranteed
+ * to ensure that no undefined integer can violate any type-guaranteed
  * constraints.
  */
-SAIL_INT_FUNCTION(undefined_int, sail_int, const int);
-SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(undefined_int, const int);
+SAIL_INT_FUNCTION(undefined_range, const sail_int, const sail_int);
 
 /*
  * Arithmetic operations in integers. We include functions for both
  * truncating towards zero, and rounding towards -infinity (floor) as
- * fdiv/fmod and tdiv/tmod respectively.
+ * fdiv/fmod and tdiv/tmod respectively. Plus euclidian division
+ * ediv/emod.
  */
-SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(sub_nat, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(ediv_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(emod_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int);
-//SAIL_INT_FUNCTION(fdiv_int, sail_int, const sail_int, const sail_int);
-//SAIL_INT_FUNCTION(fmod_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(max_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(min_int, sail_int, const sail_int, const sail_int);
-SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int);
-SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int);
-SAIL_INT_FUNCTION(pow_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(add_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(sub_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(sub_nat, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(mult_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(ediv_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(emod_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(tdiv_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(tmod_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(fdiv_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(fmod_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(max_int, const sail_int, const sail_int);
+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(make_the_value, sail_int, const sail_int);
-SAIL_INT_FUNCTION(size_itself_int, sail_int, const sail_int);
+/* ********************************************************************** */
+/* Sail bitvectors                                                        */
+/* ********************************************************************** */
 
-/* ***** Sail bitvectors ***** */
+/*
+ * Sail bitvectors are divided into three types:
+ * - (f)ixed, statically known bitvectors fbits
+ * - (s)mall bitvectors of an unknown width, but guaranteed to be less than 64-bits, sbits
+ * - Arbitrarily (l)arge bitvectors of an unknown width, lbits
+ *
+ * These types form a total order where each can be losslessly
+ * converted upwards into the other.
+ */
 
 typedef uint64_t fbits;
 
-bool eq_bit(const fbits a, const fbits b);
-
-bool EQUAL(fbits)(const fbits, const fbits);
+/*
+ * For backwards compatability with older Sail C libraries
+ */
+typedef uint64_t mach_bits;
 
 typedef struct {
-  uint64_t len;
-  uint64_t bits;
+     uint64_t len;
+     uint64_t bits;
 } sbits;
 
-// For backwards compatability
-typedef uint64_t mach_bits;
+#ifdef SAIL_BITS64
 typedef sbits lbits;
+#define SAIL_BITS_FUNCTION(fname, ...) lbits fname(__VA_ARGS__)
+#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
 
-lbits append_64(const lbits, const uint64_t);
-
-lbits add_bits_int(const lbits, const sail_int);
-lbits sub_bits_int(const lbits, const sail_int);
-
-lbits UNDEFINED(lbits)(bool);
-
-lbits vector_subrange_lbits(const lbits, const sail_int, const sail_int);
-
-lbits vector_update_subrange_lbits(const lbits, const sail_int, const sail_int, const lbits);
-
-lbits slice(const lbits, const sail_int, const sail_int);
-
-lbits set_slice(const sail_int, const sail_int, const lbits, const sail_int, const lbits);
-
-lbits get_slice_int(const sail_int, const sail_int, const sail_int);
-
-lbits zeros(const sail_int);
-lbits zero_extend(const lbits, const sail_int);
-
-bool eq_bits(const lbits, const lbits);
-bool neq_bits(const lbits, const lbits);
-lbits not_bits(const lbits);
-lbits xor_bits(const lbits, const lbits);
-lbits or_bits(const lbits, const lbits);
-lbits and_bits(const lbits, const lbits);
-lbits add_bits(const lbits, const lbits);
-lbits sub_bits(const lbits, const lbits);
-
-lbits append(const lbits, const lbits);
-
-lbits replicate_bits(const lbits, const sail_int);
-
-sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction);
-fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction);
-sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction);
-
-/* Bitvector conversions */
-
-lbits CONVERT_OF(lbits, fbits)(const fbits, const uint64_t, const bool);
-lbits CONVERT_OF(lbits, sbits)(const sbits, const bool);
-
-fbits CONVERT_OF(fbits, lbits)(const lbits, const bool);
-fbits CONVERT_OF(fbits, sbits)(const sbits, const bool);
-
-sbits CONVERT_OF(sbits, fbits)(const fbits, const uint64_t, const bool);
-sbits CONVERT_OF(sbits, lbits)(const lbits, const bool);
-
-fbits UNDEFINED(fbits)(const unit);
-
-sbits undefined_sbits(void);
-
-/*
- * Wrapper around >> operator to avoid UB when shift amount is greater
- * than or equal to 64.
- */
-fbits safe_rshift(const fbits, const fbits);
-
-fbits fast_zero_extend(const sbits op, const uint64_t n);
-fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m);
-fbits fast_sign_extend2(const sbits op, const uint64_t m);
-
-sail_int length_lbits(const lbits op);
-
-bool eq_bits(const lbits op1, const lbits op2);
-bool EQUAL(lbits)(const lbits op1, const lbits op2);
-bool neq_bits(const lbits op1, const lbits op2);
-
-fbits bitvector_access(const lbits op, const sail_int n_mpz);
-
-sail_int sail_unsigned(const lbits op);
-sail_int sail_signed(const lbits op);
-
-mach_int fast_signed(const fbits, const uint64_t);
-mach_int fast_unsigned(const fbits);
-
-sbits append_sf(const sbits, const fbits, const uint64_t);
-sbits append_fs(const fbits, const uint64_t, const sbits);
-sbits append_ss(const sbits, const sbits);
-
-fbits fast_replicate_bits(const fbits shift, const fbits v, const mach_int times);
-
-sail_int set_slice_int(const sail_int, const sail_int, const sail_int, const lbits);
-
-fbits fast_update_subrange(const fbits op,
-			   const mach_int n,
-			   const mach_int m,
-			   const fbits slice);
-
-sbits sslice(const fbits op, const mach_int start, const mach_int len);
-
-bool eq_sbits(const sbits op1, const sbits op2);
-bool neq_sbits(const sbits op1, const sbits op2);
-sbits not_sbits(const sbits op);
-sbits xor_sbits(const sbits op1, const sbits op2);
-sbits or_sbits(const sbits op1, const sbits op2);
-sbits and_sbits(const sbits op1, const sbits op2);
-sbits add_sbits(const sbits op1, const sbits op2);
-sbits sub_sbits(const sbits op1, const sbits op2);
-
-/* ***** Sail reals ***** */
-
-typedef double real;
-
-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, sail_int, const real);
-SAIL_INT_FUNCTION(round_down, sail_int, const real);
-
-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);
-
-unit print_real(const sail_string, const real);
-unit prerr_real(const sail_string, const real);
-
-void random_real(real *rop, unit);
-
-/* ***** String utilities ***** */
-
-SAIL_INT_FUNCTION(string_length, sail_int, sail_string);
-void string_drop(sail_string *dst, sail_string s, sail_int len);
-void string_take(sail_string *dst, sail_string s, sail_int len);
-
-/* ***** Printing ***** */
-
-void string_of_int(sail_string *str, const sail_int i);
-void string_of_lbits(sail_string *str, const lbits op);
-void string_of_fbits(sail_string *str, const fbits op);
-void decimal_string_of_lbits(sail_string *str, const lbits op);
-void decimal_string_of_fbits(sail_string *str, const fbits op);
-
-unit print_bits(const sail_string str, const lbits op);
-unit prerr_bits(const sail_string str, const lbits op);
-
-unit print(const sail_string str);
-unit print_endline(const sail_string str);
-
-unit prerr(const sail_string str);
-unit prerr_endline(const sail_string str);
-
-unit print_int(const sail_string str, const sail_int op);
-unit prerr_int(const sail_string str, const sail_int op);
-
-unit sail_putchar(const sail_int op);
-
-/* ***** Misc ***** */
-
-sail_int get_time_ns(const unit);
+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, sbits), const fbits, const bool);
 
 #endif