From 2e271d91c58a2d4db4adbb4c47d34bcbe1a6992e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 23 Nov 2018 22:05:24 +0000 Subject: Introduce intermediate bitvector representation in C Bitvectors that aren't fixed size, but can still be shown to fit within 64-bits, now have a specialised representation. Still need to introduce more optimized functions, as right now we mostly have to convert them into large bitvectors to pass them into most functions. Nevertheless, this doubles the performance of the TLBLookup function in ARMv8. --- lib/rts.c | 20 ++--- lib/rts.h | 24 +++--- lib/sail.c | 255 +++++++++++++++++++++++++++++++++++++++++++------------------ lib/sail.h | 190 ++++++++++++++++++++++++--------------------- 4 files changed, 305 insertions(+), 184 deletions(-) (limited to 'lib') 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 #include +#include + #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 #include #include - -#ifndef USE_INT128 #include -#endif #include @@ -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); -- cgit v1.2.3