summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/rts.c20
-rw-r--r--lib/rts.h24
-rw-r--r--lib/sail.c255
-rw-r--r--lib/sail.h190
4 files changed, 305 insertions, 184 deletions
diff --git a/lib/rts.c b/lib/rts.c
index 2f594ff8..bc0d4732 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -32,7 +32,7 @@ unit sail_exit(unit u)
static uint64_t g_verbosity = 0;
-mach_bits sail_get_verbosity(const unit u)
+fbits sail_get_verbosity(const unit u)
{
return g_verbosity;
}
@@ -214,9 +214,9 @@ void kill_mem()
bool write_ram(const mpz_t addr_size, // Either 32 or 64
const mpz_t data_size_mpz, // Number of bytes
- const sail_bits hex_ram, // Currently unused
- const sail_bits addr_bv,
- const sail_bits data)
+ const lbits hex_ram, // Currently unused
+ const lbits addr_bv,
+ const lbits data)
{
uint64_t addr = mpz_get_ui(*addr_bv.bits);
uint64_t data_size = mpz_get_ui(data_size_mpz);
@@ -238,11 +238,11 @@ bool write_ram(const mpz_t addr_size, // Either 32 or 64
return true;
}
-void read_ram(sail_bits *data,
+void read_ram(lbits *data,
const mpz_t addr_size,
const mpz_t data_size_mpz,
- const sail_bits hex_ram,
- const sail_bits addr_bv)
+ const lbits hex_ram,
+ const lbits addr_bv)
{
uint64_t addr = mpz_get_ui(*addr_bv.bits);
uint64_t data_size = mpz_get_ui(data_size_mpz);
@@ -261,7 +261,7 @@ void read_ram(sail_bits *data,
mpz_clear(byte);
}
-unit load_raw(mach_bits addr, const sail_string file)
+unit load_raw(fbits addr, const sail_string file)
{
FILE *fp = fopen(file, "r");
@@ -339,7 +339,7 @@ bool is_tracing(const unit u)
return g_trace_enabled;
}
-void trace_mach_bits(const mach_bits x) {
+void trace_fbits(const fbits x) {
if (g_trace_enabled) fprintf(stderr, "0x%" PRIx64, x);
}
@@ -355,7 +355,7 @@ void trace_sail_int(const sail_int op) {
if (g_trace_enabled) mpz_out_str(stderr, 10, op);
}
-void trace_sail_bits(const sail_bits op) {
+void trace_lbits(const lbits op) {
if (g_trace_enabled) fprint_bits("", op, "", stderr);
}
diff --git a/lib/rts.h b/lib/rts.h
index 98bbd078..f5e5e3b1 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -26,7 +26,7 @@ unit sail_exit(unit);
* The intention is that you can use individual bits to turn on/off different
* pieces of debugging output.
*/
-mach_bits sail_get_verbosity(const unit u);
+fbits sail_get_verbosity(const unit u);
/*
* Put processor to sleep until an external device calls wakeup_request().
@@ -55,20 +55,20 @@ uint64_t read_mem(uint64_t);
bool write_ram(const mpz_t addr_size, // Either 32 or 64
const mpz_t data_size_mpz, // Number of bytes
- const sail_bits hex_ram, // Currently unused
- const sail_bits addr_bv,
- const sail_bits data);
+ const lbits hex_ram, // Currently unused
+ const lbits addr_bv,
+ const lbits data);
-void read_ram(sail_bits *data,
+void read_ram(lbits *data,
const mpz_t addr_size,
const mpz_t data_size_mpz,
- const sail_bits hex_ram,
- const sail_bits addr_bv);
+ const lbits hex_ram,
+ const lbits addr_bv);
-unit write_tag_bool(const mach_bits, const bool);
-bool read_tag_bool(const mach_bits);
+unit write_tag_bool(const fbits, const bool);
+bool read_tag_bool(const fbits);
-unit load_raw(mach_bits addr, const sail_string file);
+unit load_raw(fbits addr, const sail_string file);
void load_image(char *);
@@ -106,8 +106,8 @@ void trace_sail_int(const sail_int);
void trace_bool(const bool);
void trace_unit(const unit);
void trace_sail_string(const sail_string);
-void trace_mach_bits(const mach_bits);
-void trace_sail_bits(const sail_bits);
+void trace_fbits(const fbits);
+void trace_lbits(const lbits);
void trace_unknown(void);
void trace_argsep(void);
diff --git a/lib/sail.c b/lib/sail.c
index 6ea41fcc..fbf230a6 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -7,6 +7,8 @@
#include<string.h>
#include<time.h>
+#include <x86intrin.h>
+
#include"sail.h"
/*
@@ -53,7 +55,7 @@ unit skip(const unit u)
/* ***** Sail bit type ***** */
-bool eq_bit(const mach_bits a, const mach_bits b)
+bool eq_bit(const fbits a, const fbits b)
{
return a == b;
}
@@ -415,74 +417,144 @@ void pow2(sail_int *rop, const sail_int exp)
/* ***** Sail bitvectors ***** */
-bool EQUAL(mach_bits)(const mach_bits op1, const mach_bits op2)
+bool EQUAL(fbits)(const fbits op1, const fbits op2)
{
return op1 == op2;
}
-void CREATE(sail_bits)(sail_bits *rop)
+void CREATE(lbits)(lbits *rop)
{
rop->bits = malloc(sizeof(mpz_t));
rop->len = 0;
mpz_init(*rop->bits);
}
-void RECREATE(sail_bits)(sail_bits *rop)
+void RECREATE(lbits)(lbits *rop)
{
rop->len = 0;
mpz_set_ui(*rop->bits, 0);
}
-void COPY(sail_bits)(sail_bits *rop, const sail_bits op)
+void COPY(lbits)(lbits *rop, const lbits op)
{
rop->len = op.len;
mpz_set(*rop->bits, *op.bits);
}
-void KILL(sail_bits)(sail_bits *rop)
+void KILL(lbits)(lbits *rop)
{
mpz_clear(*rop->bits);
free(rop->bits);
}
-void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+void CREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len, const bool direction)
{
rop->bits = malloc(sizeof(mpz_t));
rop->len = len;
mpz_init_set_ui(*rop->bits, op);
}
-mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits op)
+fbits CREATE_OF(fbits, lbits)(const lbits op, const bool direction)
{
return mpz_get_ui(*op.bits);
}
-void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
+sbits CREATE_OF(sbits, lbits)(const lbits op, const bool direction)
+{
+ sbits rop;
+ rop.bits = mpz_get_ui(*op.bits);
+ rop.len = op.len;
+ return rop;
+}
+
+sbits CREATE_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction)
+{
+ sbits rop;
+ rop.bits = op;
+ rop.len = len;
+ return rop;
+}
+
+void RECREATE_OF(lbits, fbits)(lbits *rop, const uint64_t op, const uint64_t len, const bool direction)
{
rop->len = len;
mpz_set_ui(*rop->bits, op);
}
-mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits op, const bool direction)
+void CREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction)
+{
+ rop->bits = malloc(sizeof(mpz_t));
+ rop->len = op.len;
+ mpz_init_set_ui(*rop->bits, op.bits);
+}
+
+void RECREATE_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction)
+{
+ rop->len = op.len;
+ mpz_set_ui(*rop->bits, op.bits);
+}
+
+// Bitvector conversions
+
+inline
+fbits CONVERT_OF(fbits, lbits)(const lbits op, const bool direction)
{
return mpz_get_ui(*op.bits);
}
-void CONVERT_OF(sail_bits, mach_bits)(sail_bits *rop, const mach_bits op, const uint64_t len, const bool direction)
+inline
+fbits CONVERT_OF(fbits, sbits)(const sbits op, const bool direction)
+{
+ return op.bits;
+}
+
+void CONVERT_OF(lbits, fbits)(lbits *rop, const fbits op, const uint64_t len, const bool direction)
{
rop->len = len;
// use safe_rshift to correctly handle the case when we have a 0-length vector.
mpz_set_ui(*rop->bits, op & safe_rshift(UINT64_MAX, 64 - len));
}
-void UNDEFINED(sail_bits)(sail_bits *rop, const sail_int len, const mach_bits bit)
+void CONVERT_OF(lbits, sbits)(lbits *rop, const sbits op, const bool direction)
+{
+ rop->len = op.len;
+ mpz_set_ui(*rop->bits, op.bits & safe_rshift(UINT64_MAX, 64 - op.len));
+}
+
+inline
+sbits CONVERT_OF(sbits, fbits)(const fbits op, const uint64_t len, const bool direction)
+{
+ sbits rop;
+ rop.len = len;
+ rop.bits = op;
+ return rop;
+}
+
+inline
+sbits CONVERT_OF(sbits, lbits)(const lbits op, const bool direction)
+{
+ sbits rop;
+ rop.len = op.len;
+ rop.bits = mpz_get_ui(*op.bits);
+ return rop;
+}
+
+void UNDEFINED(lbits)(lbits *rop, const sail_int len, const fbits bit)
{
zeros(rop, len);
}
-mach_bits UNDEFINED(mach_bits)(const unit u) { return 0; }
+fbits UNDEFINED(fbits)(const unit u) { return 0; }
-mach_bits safe_rshift(const mach_bits x, const mach_bits n)
+sbits undefined_sbits(void)
+{
+ sbits rop;
+ rop.bits = UINT64_C(0);
+ rop.len = UINT64_C(0);
+ return rop;
+}
+
+fbits safe_rshift(const fbits x, const fbits n)
{
if (n >= 64) {
return 0ul;
@@ -491,7 +563,7 @@ mach_bits safe_rshift(const mach_bits x, const mach_bits n)
}
}
-void normalize_sail_bits(sail_bits *rop) {
+void normalize_lbits(lbits *rop) {
/* TODO optimisation: keep a set of masks of various sizes handy */
mpz_set_ui(sail_lib_tmp1, 1);
mpz_mul_2exp(sail_lib_tmp1, sail_lib_tmp1, rop->len);
@@ -499,64 +571,64 @@ void normalize_sail_bits(sail_bits *rop) {
mpz_and(*rop->bits, *rop->bits, sail_lib_tmp1);
}
-void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk)
+void append_64(lbits *rop, const lbits op, const fbits chunk)
{
rop->len = rop->len + 64ul;
mpz_mul_2exp(*rop->bits, *op.bits, 64ul);
mpz_add_ui(*rop->bits, *rop->bits, chunk);
}
-void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void add_bits(lbits *rop, const lbits op1, const lbits op2)
{
rop->len = op1.len;
mpz_add(*rop->bits, *op1.bits, *op2.bits);
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void sub_bits(lbits *rop, const lbits op1, const lbits op2)
{
assert(op1.len == op2.len);
rop->len = op1.len;
mpz_sub(*rop->bits, *op1.bits, *op2.bits);
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+void add_bits_int(lbits *rop, const lbits op1, const mpz_t op2)
{
rop->len = op1.len;
mpz_add(*rop->bits, *op1.bits, op2);
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+void sub_bits_int(lbits *rop, const lbits op1, const mpz_t op2)
{
rop->len = op1.len;
mpz_sub(*rop->bits, *op1.bits, op2);
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void and_bits(lbits *rop, const lbits op1, const lbits op2)
{
assert(op1.len == op2.len);
rop->len = op1.len;
mpz_and(*rop->bits, *op1.bits, *op2.bits);
}
-void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void or_bits(lbits *rop, const lbits op1, const lbits op2)
{
assert(op1.len == op2.len);
rop->len = op1.len;
mpz_ior(*rop->bits, *op1.bits, *op2.bits);
}
-void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void xor_bits(lbits *rop, const lbits op1, const lbits op2)
{
assert(op1.len == op2.len);
rop->len = op1.len;
mpz_xor(*rop->bits, *op1.bits, *op2.bits);
}
-void not_bits(sail_bits *rop, const sail_bits op)
+void not_bits(lbits *rop, const lbits op)
{
rop->len = op.len;
mpz_set(*rop->bits, *op.bits);
@@ -565,7 +637,7 @@ void not_bits(sail_bits *rop, const sail_bits op)
}
}
-void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void mults_vec(lbits *rop, const lbits op1, const lbits op2)
{
mpz_t op1_int, op2_int;
mpz_init(op1_int);
@@ -574,33 +646,33 @@ void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
sail_signed(&op2_int, op2);
rop->len = op1.len * 2;
mpz_mul(*rop->bits, op1_int, op2_int);
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
mpz_clear(op1_int);
mpz_clear(op2_int);
}
-void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void mult_vec(lbits *rop, const lbits op1, const lbits op2)
{
rop->len = op1.len * 2;
mpz_mul(*rop->bits, *op1.bits, *op2.bits);
- normalize_sail_bits(rop); /* necessary? */
+ normalize_lbits(rop); /* necessary? */
}
-void zeros(sail_bits *rop, const sail_int op)
+void zeros(lbits *rop, const sail_int op)
{
rop->len = mpz_get_ui(op);
mpz_set_ui(*rop->bits, 0);
}
-void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len)
+void zero_extend(lbits *rop, const lbits op, const sail_int len)
{
assert(op.len <= mpz_get_ui(len));
rop->len = mpz_get_ui(len);
mpz_set(*rop->bits, *op.bits);
}
-void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len)
+void sign_extend(lbits *rop, const lbits op, const sail_int len)
{
assert(op.len <= mpz_get_ui(len));
rop->len = mpz_get_ui(len);
@@ -614,12 +686,12 @@ void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len)
}
}
-void length_sail_bits(sail_int *rop, const sail_bits op)
+void length_lbits(sail_int *rop, const lbits op)
{
mpz_set_ui(*rop, op.len);
}
-bool eq_bits(const sail_bits op1, const sail_bits op2)
+bool eq_bits(const lbits op1, const lbits op2)
{
assert(op1.len == op2.len);
for (mp_bitcnt_t i = 0; i < op1.len; i++) {
@@ -628,12 +700,12 @@ bool eq_bits(const sail_bits op1, const sail_bits op2)
return true;
}
-bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2)
+bool EQUAL(lbits)(const lbits op1, const lbits op2)
{
return eq_bits(op1, op2);
}
-bool neq_bits(const sail_bits op1, const sail_bits op2)
+bool neq_bits(const lbits op1, const lbits op2)
{
assert(op1.len == op2.len);
for (mp_bitcnt_t i = 0; i < op1.len; i++) {
@@ -642,8 +714,8 @@ bool neq_bits(const sail_bits op1, const sail_bits op2)
return false;
}
-void vector_subrange_sail_bits(sail_bits *rop,
- const sail_bits op,
+void vector_subrange_lbits(lbits *rop,
+ const lbits op,
const sail_int n_mpz,
const sail_int m_mpz)
{
@@ -652,30 +724,30 @@ void vector_subrange_sail_bits(sail_bits *rop,
rop->len = n - (m - 1ul);
mpz_fdiv_q_2exp(*rop->bits, *op.bits, m);
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len)
+void sail_truncate(lbits *rop, const lbits op, const sail_int len)
{
assert(op.len >= mpz_get_ui(len));
rop->len = mpz_get_ui(len);
mpz_set(*rop->bits, *op.bits);
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz)
+fbits bitvector_access(const lbits op, const sail_int n_mpz)
{
uint64_t n = mpz_get_ui(n_mpz);
- return (mach_bits) mpz_tstbit(*op.bits, n);
+ return (fbits) mpz_tstbit(*op.bits, n);
}
-void sail_unsigned(sail_int *rop, const sail_bits op)
+void sail_unsigned(sail_int *rop, const lbits op)
{
/* Normal form of bv_t is always positive so just return the bits. */
mpz_set(*rop, *op.bits);
}
-void sail_signed(sail_int *rop, const sail_bits op)
+void sail_signed(sail_int *rop, const lbits op)
{
if (op.len == 0) {
mpz_set_ui(*rop, 0);
@@ -694,19 +766,19 @@ void sail_signed(sail_int *rop, const sail_bits op)
}
inline
-mach_int fast_unsigned(const mach_bits op)
+mach_int fast_unsigned(const fbits op)
{
return (mach_int) op;
}
-void append(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void append(lbits *rop, const lbits op1, const lbits op2)
{
rop->len = op1.len + op2.len;
mpz_mul_2exp(*rop->bits, *op1.bits, op2.len);
mpz_ior(*rop->bits, *rop->bits, *op2.bits);
}
-void replicate_bits(sail_bits *rop, const sail_bits op1, const mpz_t op2)
+void replicate_bits(lbits *rop, const lbits op1, const mpz_t op2)
{
uint64_t op2_ui = mpz_get_ui(op2);
rop->len = op1.len * op2_ui;
@@ -742,7 +814,7 @@ uint64_t fast_replicate_bits(const uint64_t shift, const uint64_t v, const int64
// <-------^
// (8 bit) 4
//
-void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz)
+void get_slice_int(lbits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz)
{
uint64_t start = mpz_get_ui(start_mpz);
uint64_t len = mpz_get_ui(len_mpz);
@@ -761,7 +833,7 @@ void set_slice_int(sail_int *rop,
const sail_int len_mpz,
const sail_int n,
const sail_int start_mpz,
- const sail_bits slice)
+ const lbits slice)
{
uint64_t start = mpz_get_ui(start_mpz);
@@ -776,11 +848,11 @@ void set_slice_int(sail_int *rop,
}
}
-void vector_update_subrange_sail_bits(sail_bits *rop,
- const sail_bits op,
+void vector_update_subrange_lbits(lbits *rop,
+ const lbits op,
const sail_int n_mpz,
const sail_int m_mpz,
- const sail_bits slice)
+ const lbits slice)
{
uint64_t n = mpz_get_ui(n_mpz);
uint64_t m = mpz_get_ui(m_mpz);
@@ -797,7 +869,7 @@ void vector_update_subrange_sail_bits(sail_bits *rop,
}
}
-void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz)
+void slice(lbits *rop, const lbits op, const sail_int start_mpz, const sail_int len_mpz)
{
assert(mpz_get_ui(start_mpz) + mpz_get_ui(len_mpz) <= op.len);
uint64_t start = mpz_get_ui(start_mpz);
@@ -811,12 +883,25 @@ void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const s
}
}
-void set_slice(sail_bits *rop,
+inline
+sbits sslice(const fbits op, const mach_int start, const mach_int len)
+{
+ sbits rop;
+#ifdef INTRINSICS
+ rop.bits = _bzhi_u64(op >> start, len);
+#else
+ rop.bits = (op >> start) & safe_rshift(UINT64_MAX, 64 - len);
+#endif
+ rop.len = len;
+ return rop;
+}
+
+void set_slice(lbits *rop,
const sail_int len_mpz,
const sail_int slen_mpz,
- const sail_bits op,
+ const lbits op,
const sail_int start_mpz,
- const sail_bits slice)
+ const lbits slice)
{
uint64_t start = mpz_get_ui(start_mpz);
@@ -832,21 +917,21 @@ void set_slice(sail_bits *rop,
}
}
-void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void shift_bits_left(lbits *rop, const lbits op1, const lbits op2)
{
rop->len = op1.len;
mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void shift_bits_right(lbits *rop, const lbits op1, const lbits op2)
{
rop->len = op1.len;
mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(*op2.bits));
}
/* FIXME */
-void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2)
+void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2)
{
rop->len = op1.len;
mp_bitcnt_t shift_amt = mpz_get_ui(*op2.bits);
@@ -860,20 +945,20 @@ void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits
}
}
-void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2)
+void shiftl(lbits *rop, const lbits op1, const sail_int op2)
{
rop->len = op1.len;
mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2));
- normalize_sail_bits(rop);
+ normalize_lbits(rop);
}
-void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2)
+void shiftr(lbits *rop, const lbits op1, const sail_int op2)
{
rop->len = op1.len;
mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2));
}
-void reverse_endianness(sail_bits *rop, const sail_bits op)
+void reverse_endianness(lbits *rop, const lbits op)
{
rop->len = op.len;
if (rop->len == 64ul) {
@@ -907,6 +992,26 @@ void reverse_endianness(sail_bits *rop, const sail_bits op)
}
}
+inline
+bool eq_sbits(const sbits op1, const sbits op2)
+{
+ return op1.bits == op2.bits;
+}
+
+inline
+bool neq_sbits(const sbits op1, const sbits op2)
+{
+ return op1.bits != op2.bits;
+}
+
+sbits xor_sbits(const sbits op1, const sbits op2)
+{
+ sbits rop;
+ rop.bits = op1.bits ^ op2.bits;
+ rop.len = op1.len;
+ return rop;
+}
+
/* ***** Sail Reals ***** */
void CREATE(real)(real *rop)
@@ -1148,7 +1253,7 @@ void string_of_int(sail_string *str, const sail_int i)
}
/* asprinf is a GNU extension, but it should exist on BSD */
-void string_of_mach_bits(sail_string *str, const mach_bits op)
+void string_of_fbits(sail_string *str, const fbits op)
{
int bytes = asprintf(str, "0x%" PRIx64, op);
if (bytes == -1) {
@@ -1156,7 +1261,7 @@ void string_of_mach_bits(sail_string *str, const mach_bits op)
}
}
-void string_of_sail_bits(sail_string *str, const sail_bits op)
+void string_of_lbits(sail_string *str, const lbits op)
{
if ((op.len % 4) == 0) {
gmp_asprintf(str, "0x%*0Zx", op.len / 4, *op.bits);
@@ -1165,7 +1270,7 @@ void string_of_sail_bits(sail_string *str, const sail_bits op)
}
}
-void decimal_string_of_mach_bits(sail_string *str, const mach_bits op)
+void decimal_string_of_fbits(sail_string *str, const fbits op)
{
int bytes = asprintf(str, "%" PRId64, op);
if (bytes == -1) {
@@ -1173,13 +1278,13 @@ void decimal_string_of_mach_bits(sail_string *str, const mach_bits op)
}
}
-void decimal_string_of_sail_bits(sail_string *str, const sail_bits op)
+void decimal_string_of_lbits(sail_string *str, const lbits op)
{
gmp_asprintf(str, "%Z", *op.bits);
}
void fprint_bits(const sail_string pre,
- const sail_bits op,
+ const lbits op,
const sail_string post,
FILE *stream)
{
@@ -1214,13 +1319,13 @@ void fprint_bits(const sail_string pre,
fputs(post, stream);
}
-unit print_bits(const sail_string str, const sail_bits op)
+unit print_bits(const sail_string str, const lbits op)
{
fprint_bits(str, op, "\n", stdout);
return UNIT;
}
-unit prerr_bits(const sail_string str, const sail_bits op)
+unit prerr_bits(const sail_string str, const lbits op)
{
fprint_bits(str, op, "\n", stderr);
return UNIT;
diff --git a/lib/sail.h b/lib/sail.h
index 6b67b7e0..56df9740 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -4,10 +4,7 @@
#include<stdlib.h>
#include<stdio.h>
#include<stdbool.h>
-
-#ifndef USE_INT128
#include<gmp.h>
-#endif
#include<time.h>
@@ -85,14 +82,6 @@ typedef int64_t mach_int;
bool EQUAL(mach_int)(const mach_int, const mach_int);
-/*
- * Integers can be either stack-allocated as 128-bit integers if
- * __int128 is available, or use GMP arbitrary precision
- * integers. This affects the function signatures, so use a macro to
- * paper over the differences.
- */
-#ifndef USE_INT128
-
typedef mpz_t sail_int;
#define SAIL_INT_FUNCTION(fname, rtype, ...) void fname(rtype*, __VA_ARGS__)
@@ -110,13 +99,6 @@ void RECREATE_OF(sail_int, sail_string)(mpz_t *, const sail_string);
mach_int CONVERT_OF(mach_int, sail_int)(const sail_int);
void CONVERT_OF(sail_int, mach_int)(sail_int *, const mach_int);
-#else
-
-typedef __int128 sail_int;
-#define SAIL_INT_FUNCTION(fname, rtype, ...) rtype fname(__VA_ARGS__)
-
-#endif
-
/*
* Comparison operators for integers
*/
@@ -170,125 +152,159 @@ SAIL_INT_FUNCTION(pow2, sail_int, const sail_int);
/* ***** Sail bitvectors ***** */
-typedef uint64_t mach_bits;
+typedef uint64_t fbits;
-bool eq_bit(const mach_bits a, const mach_bits b);
+bool eq_bit(const fbits a, const fbits b);
-bool EQUAL(mach_bits)(const mach_bits, const mach_bits);
+bool EQUAL(fbits)(const fbits, const fbits);
+
+typedef struct {
+ uint64_t len;
+ uint64_t bits;
+} sbits;
typedef struct {
mp_bitcnt_t len;
mpz_t *bits;
-} sail_bits;
+} lbits;
-SAIL_BUILTIN_TYPE(sail_bits);
+// For backwards compatability
+typedef uint64_t mach_bits;
+typedef lbits sail_bits;
+
+SAIL_BUILTIN_TYPE(lbits);
+
+void CREATE_OF(lbits, fbits)(lbits *,
+ const fbits op,
+ const uint64_t len,
+ const bool direction);
+
+void RECREATE_OF(lbits, fbits)(lbits *,
+ const fbits op,
+ const uint64_t len,
+ const bool direction);
+
+void CREATE_OF(lbits, sbits)(lbits *,
+ const sbits op,
+ const bool direction);
-void CREATE_OF(sail_bits, mach_bits)(sail_bits *,
- const mach_bits op,
- const mach_bits len,
- const bool direction);
+void RECREATE_OF(lbits, sbits)(lbits *,
+ const sbits op,
+ const bool direction);
-void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
- const mach_bits op,
- const mach_bits len,
- const bool direction);
+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);
-mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits);
+/* Bitvector conversions */
-mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool);
+fbits CONVERT_OF(fbits, lbits)(const lbits, const bool);
+fbits CONVERT_OF(fbits, sbits)(const sbits, const bool);
-void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool);
+void CONVERT_OF(lbits, fbits)(lbits *, const fbits, const uint64_t, const bool);
+void CONVERT_OF(lbits, sbits)(lbits *, const sbits, const bool);
-void UNDEFINED(sail_bits)(sail_bits *, const sail_int len, const mach_bits bit);
-mach_bits UNDEFINED(mach_bits)(const unit);
+sbits CONVERT_OF(sbits, fbits)(const fbits, const uint64_t, const bool);
+sbits CONVERT_OF(sbits, lbits)(const lbits, const bool);
+
+void UNDEFINED(lbits)(lbits *, const sail_int len, const fbits bit);
+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.
*/
-mach_bits safe_rshift(const mach_bits, const mach_bits);
+fbits safe_rshift(const fbits, const fbits);
/*
* Used internally to construct large bitvector literals.
*/
-void append_64(sail_bits *rop, const sail_bits op, const mach_bits chunk);
+void append_64(lbits *rop, const lbits op, const fbits chunk);
-void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void add_bits(lbits *rop, const lbits op1, const lbits op2);
+void sub_bits(lbits *rop, const lbits op1, const lbits op2);
-void add_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
-void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2);
+void add_bits_int(lbits *rop, const lbits op1, const mpz_t op2);
+void sub_bits_int(lbits *rop, const lbits op1, const mpz_t op2);
-void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void not_bits(sail_bits *rop, const sail_bits op);
+void and_bits(lbits *rop, const lbits op1, const lbits op2);
+void or_bits(lbits *rop, const lbits op1, const lbits op2);
+void xor_bits(lbits *rop, const lbits op1, const lbits op2);
+void not_bits(lbits *rop, const lbits op);
-void mults_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void mult_vec(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void mults_vec(lbits *rop, const lbits op1, const lbits op2);
+void mult_vec(lbits *rop, const lbits op1, const lbits op2);
-void zeros(sail_bits *rop, const sail_int op);
+void zeros(lbits *rop, const sail_int op);
-void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len);
-void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len);
+void zero_extend(lbits *rop, const lbits op, const sail_int len);
+void sign_extend(lbits *rop, const lbits op, const sail_int len);
-void length_sail_bits(sail_int *rop, const sail_bits op);
+void length_lbits(sail_int *rop, const lbits op);
-bool eq_bits(const sail_bits op1, const sail_bits op2);
-bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2);
-bool neq_bits(const sail_bits op1, const sail_bits op2);
+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);
-void vector_subrange_sail_bits(sail_bits *rop,
- const sail_bits op,
+void vector_subrange_lbits(lbits *rop,
+ const lbits op,
const sail_int n_mpz,
const sail_int m_mpz);
-void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len);
+void sail_truncate(lbits *rop, const lbits op, const sail_int len);
-mach_bits bitvector_access(const sail_bits op, const sail_int n_mpz);
+fbits bitvector_access(const lbits op, const sail_int n_mpz);
-void sail_unsigned(sail_int *rop, const sail_bits op);
-void sail_signed(sail_int *rop, const sail_bits op);
+void sail_unsigned(sail_int *rop, const lbits op);
+void sail_signed(sail_int *rop, const lbits op);
-mach_int fast_unsigned(const mach_bits);
+mach_int fast_unsigned(const fbits);
-void append(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void append(lbits *rop, const lbits op1, const lbits op2);
-void replicate_bits(sail_bits *rop, const sail_bits op1, const sail_int op2);
-mach_bits fast_replicate_bits(const mach_bits shift, const mach_bits v, const mach_int times);
+void replicate_bits(lbits *rop, const lbits op1, const sail_int op2);
+fbits fast_replicate_bits(const fbits shift, const fbits v, const mach_int times);
-void get_slice_int(sail_bits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz);
+void get_slice_int(lbits *rop, const sail_int len_mpz, const sail_int n, const sail_int start_mpz);
void set_slice_int(sail_int *rop,
const sail_int len_mpz,
const sail_int n,
const sail_int start_mpz,
- const sail_bits slice);
+ const lbits slice);
-void vector_update_subrange_sail_bits(sail_bits *rop,
- const sail_bits op,
+void vector_update_subrange_lbits(lbits *rop,
+ const lbits op,
const sail_int n_mpz,
const sail_int m_mpz,
- const sail_bits slice);
+ const lbits slice);
-void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz);
+void slice(lbits *rop, const lbits op, const sail_int start_mpz, const sail_int len_mpz);
-void set_slice(sail_bits *rop,
+sbits sslice(const fbits op, const mach_int start, const mach_int len);
+
+void set_slice(lbits *rop,
const sail_int len_mpz,
const sail_int slen_mpz,
- const sail_bits op,
+ const lbits op,
const sail_int start_mpz,
- const sail_bits slice);
+ const lbits slice);
+
+void shift_bits_left(lbits *rop, const lbits op1, const lbits op2);
+void shift_bits_right(lbits *rop, const lbits op1, const lbits op2);
+void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2);
-void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2);
-void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2);
+void shiftl(lbits *rop, const lbits op1, const sail_int op2);
+void shiftr(lbits *rop, const lbits op1, const sail_int op2);
-void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2);
-void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2);
+void reverse_endianness(lbits*, lbits);
-void reverse_endianness(sail_bits*, sail_bits);
+bool eq_sbits(const sbits op1, const sbits op2);
+bool neq_sbits(const sbits op1, const sbits op2);
+sbits xor_sbits(const sbits op1, const sbits op2);
/* ***** Sail reals ***** */
@@ -338,21 +354,21 @@ 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_sail_bits(sail_string *str, const sail_bits op);
-void string_of_mach_bits(sail_string *str, const mach_bits op);
-void decimal_string_of_sail_bits(sail_string *str, const sail_bits op);
-void decimal_string_of_mach_bits(sail_string *str, const mach_bits op);
+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);
/*
* Utility function not callable from Sail!
*/
void fprint_bits(const sail_string pre,
- const sail_bits op,
+ const lbits op,
const sail_string post,
FILE *stream);
-unit print_bits(const sail_string str, const sail_bits op);
-unit prerr_bits(const sail_string str, const sail_bits 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);