diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/rts.c | 20 | ||||
| -rw-r--r-- | lib/rts.h | 24 | ||||
| -rw-r--r-- | lib/sail.c | 255 | ||||
| -rw-r--r-- | lib/sail.h | 190 |
4 files changed, 305 insertions, 184 deletions
@@ -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); } @@ -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); @@ -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; @@ -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); |
