diff options
| -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 | ||||
| -rw-r--r-- | src/c_backend.ml | 87 | ||||
| -rwxr-xr-x | test/c/run_tests.py | 1 | ||||
| -rw-r--r-- | test/c/small_slice.expect | 2 | ||||
| -rw-r--r-- | test/c/small_slice.sail | 16 |
8 files changed, 375 insertions, 220 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); diff --git a/src/c_backend.ml b/src/c_backend.ml index 2bac9945..3d281337 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -168,7 +168,7 @@ let rec ctyp_of_typ ctx typ = let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in begin match nexp_simp n with | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction) - | n when ctx.optimize_z3 && prove ctx.local_env (nc_lteq n (nint 64)) -> CT_lbits direction (* TODO: CT_sbits direction *) + | n when ctx.optimize_z3 && prove ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction | _ -> CT_lbits direction end @@ -372,9 +372,10 @@ let rec analyze_functions ctx f (AE_aux (aexp, env, l)) = | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp) - | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> + | AE_let (mut, id, typ1, aexp1, (AE_aux (_, env2, _) as aexp2), typ2) -> let aexp1 = analyze_functions ctx f aexp1 in - let ctyp1 = ctyp_of_typ ctx typ1 in + (* Use aexp2's environment because it will contain constraints for id *) + let ctyp1 = ctyp_of_typ { ctx with local_env = env2 } typ1 in let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2) @@ -423,12 +424,15 @@ let analyze_primop' ctx id args typ = c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")")); match extern, args with - | "eq_bits", [AV_C_fragment (v1, typ1, _); AV_C_fragment (v2, typ2, _)] -> + | "eq_bits", [AV_C_fragment (v1, _, CT_fbits _); AV_C_fragment (v2, _, _)] -> AE_val (AV_C_fragment (F_op (v1, "==", v2), typ, CT_bool)) -(* - | "neq_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> - AE_val (AV_C_fragment (F_op (v1, "!=", v2), typ)) - *) + | "eq_bits", [AV_C_fragment (v1, _, CT_sbits _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_call ("eq_sbits", [v1; v2]), typ, CT_bool)) + + | "neq_bits", [AV_C_fragment (v1, _, CT_fbits _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, "!=", v2), typ, CT_bool)) + | "neq_bits", [AV_C_fragment (v1, _, CT_sbits _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_call ("neq_sbits", [v1; v2]), typ, CT_bool)) | "eq_int", [AV_C_fragment (v1, typ1, _); AV_C_fragment (v2, typ2, _)] -> AE_val (AV_C_fragment (F_op (v1, "==", v2), typ, CT_bool)) @@ -444,13 +448,15 @@ let analyze_primop' ctx id args typ = | "gteq", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> AE_val (AV_C_fragment (F_op (v1, ">=", v2), typ, CT_bool)) - | "xor_bits", [AV_C_fragment (v1, typ1, ctyp); AV_C_fragment (v2, typ2, _)] -> + | "xor_bits", [AV_C_fragment (v1, _, (CT_fbits _ as ctyp)); AV_C_fragment (v2, _, CT_fbits _)] -> AE_val (AV_C_fragment (F_op (v1, "^", v2), typ, ctyp)) + | "xor_bits", [AV_C_fragment (v1, _, (CT_sbits _ as ctyp)); AV_C_fragment (v2, _, CT_sbits _)] -> + AE_val (AV_C_fragment (F_call ("xor_sbits", [v1; v2]), typ, ctyp)) - | "or_bits", [AV_C_fragment (v1, typ1, ctyp); AV_C_fragment (v2, typ2, _)] -> + | "or_bits", [AV_C_fragment (v1, _, (CT_fbits _ as ctyp)); AV_C_fragment (v2, _, CT_fbits _)] -> AE_val (AV_C_fragment (F_op (v1, "|", v2), typ, ctyp)) - | "and_bits", [AV_C_fragment (v1, typ1, ctyp); AV_C_fragment (v2, typ2, _)] -> + | "and_bits", [AV_C_fragment (v1, _, (CT_fbits _ as ctyp)); AV_C_fragment (v2, _, CT_fbits _)] -> AE_val (AV_C_fragment (F_op (v1, "&", v2), typ, ctyp)) | "not_bits", [AV_C_fragment (v, _, ctyp)] -> @@ -461,25 +467,29 @@ let analyze_primop' ctx id args typ = | _ -> no_change end - | "vector_subrange", [AV_C_fragment (vec, _, _); AV_C_fragment (f, _, _); AV_C_fragment (t, _, _)] + | "vector_subrange", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (f, _, _); AV_C_fragment (t, _, _)] when is_fbits_typ ctx typ -> let len = F_op (f, "-", F_op (t, "-", v_one)) in AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ, ctyp_of_typ ctx typ)) - | "vector_access", [AV_C_fragment (vec, _, _); AV_C_fragment (n, _, _)] -> + | "vector_access", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (n, _, _)] -> AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ, CT_bit)) | "eq_bit", [AV_C_fragment (a, _, _); AV_C_fragment (b, _, _)] -> AE_val (AV_C_fragment (F_op (a, "==", b), typ, CT_bool)) - | "slice", [AV_C_fragment (vec, _, _); AV_C_fragment (start, _, _); AV_C_fragment (len, _, _)] + | "slice", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (start, _, _); AV_C_fragment (len, _, _)] when is_fbits_typ ctx typ -> AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", start)), typ, ctyp_of_typ ctx typ)) + | "slice", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (start, _, _); AV_C_fragment (len, _, _)] + when is_sbits_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("sslice", [vec; start; len]), typ, ctyp_of_typ ctx typ)) + | "undefined_bit", _ -> AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ, CT_bit)) @@ -1021,8 +1031,8 @@ let pointer_assign ctyp1 ctyp2 = let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctx = { ctx with local_env = env } in match aexp_aux with - | AE_let (mut, id, binding_typ, binding, body, body_typ) -> - let binding_ctyp = ctyp_of_typ ctx binding_typ in + | AE_let (mut, id, binding_typ, binding, (AE_aux (_, body_env, _) as body), body_typ) -> + let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in let setup, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id] @@ -1201,7 +1211,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = [] | AE_assign (id, assign_typ, aexp) -> - let assign_ctyp = ctyp_of_typ ctx assign_typ in + let assign_ctyp = + match Bindings.find_opt id ctx.locals with + | Some (_, ctyp) -> ctyp + | None -> ctyp_of_typ ctx assign_typ + in let setup, call, cleanup = compile_aexp ctx aexp in setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup @@ -2121,13 +2135,13 @@ let codegen_id id = string (sgen_id id) let rec sgen_ctyp = function | CT_unit -> "unit" - | CT_bit -> "mach_bits" + | CT_bit -> "fbits" | CT_bool -> "bool" - | CT_fbits _ -> "mach_bits" + | CT_fbits _ -> "fbits" | CT_sbits _ -> "sbits" | CT_int64 -> "mach_int" | CT_int -> "sail_int" - | CT_lbits _ -> "sail_bits" + | CT_lbits _ -> "lbits" | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> "struct " ^ sgen_id id | CT_enum (id, _) -> "enum " ^ sgen_id id @@ -2141,13 +2155,13 @@ let rec sgen_ctyp = function let rec sgen_ctyp_name = function | CT_unit -> "unit" - | CT_bit -> "mach_bits" + | CT_bit -> "fbits" | CT_bool -> "bool" - | CT_fbits _ -> "mach_bits" + | CT_fbits _ -> "fbits" | CT_sbits _ -> "sbits" | CT_int64 -> "mach_int" | CT_int -> "sail_int" - | CT_lbits _ -> "sail_bits" + | CT_lbits _ -> "lbits" | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> sgen_id id | CT_enum (id, _) -> sgen_id id @@ -2176,7 +2190,7 @@ let rec sgen_clexp = function | CL_id (id, _) -> "&" ^ sgen_id id | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ Util.zencode_string field ^ ")" | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")" - | CL_addr clexp -> "*(" ^ sgen_clexp clexp ^ ")" + | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))" | CL_have_exception -> "have_exception" | CL_current_exception _ -> "current_exception" @@ -2184,7 +2198,7 @@ let rec sgen_clexp_pure = function | CL_id (id, _) -> sgen_id id | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ Util.zencode_string field | CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n - | CL_addr clexp -> "*(" ^ sgen_clexp_pure clexp ^ ")" + | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))" | CL_have_exception -> "have_exception" | CL_current_exception _ -> "current_exception" @@ -2294,26 +2308,26 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = end | "vector_update_subrange", _ -> Printf.sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp) | "vector_subrange", _ -> Printf.sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp) - | "vector_update", CT_fbits _ -> "update_mach_bits" - | "vector_update", CT_lbits _ -> "update_sail_bits" + | "vector_update", CT_fbits _ -> "update_fbits" + | "vector_update", CT_lbits _ -> "update_lbits" | "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp) | "string_of_bits", _ -> begin match cval_ctyp (List.nth args 0) with - | CT_fbits _ -> "string_of_mach_bits" - | CT_lbits _ -> "string_of_sail_bits" + | CT_fbits _ -> "string_of_fbits" + | CT_lbits _ -> "string_of_lbits" | _ -> assert false end | "decimal_string_of_bits", _ -> begin match cval_ctyp (List.nth args 0) with - | CT_fbits _ -> "decimal_string_of_mach_bits" - | CT_lbits _ -> "decimal_string_of_sail_bits" + | CT_fbits _ -> "decimal_string_of_fbits" + | CT_lbits _ -> "decimal_string_of_lbits" | _ -> assert false end | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) - | "undefined_vector", CT_fbits _ -> "UNDEFINED(mach_bits)" - | "undefined_vector", CT_lbits _ -> "UNDEFINED(sail_bits)" - | "undefined_bit", _ -> "UNDEFINED(mach_bits)" + | "undefined_vector", CT_fbits _ -> "UNDEFINED(fbits)" + | "undefined_vector", CT_lbits _ -> "UNDEFINED(lbits)" + | "undefined_bit", _ -> "UNDEFINED(fbits)" | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) | fname, _ -> fname in @@ -2338,7 +2352,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = ksprintf string " %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval) else ksprintf string " %s %s = CREATE_OF(%s, %s)(%s);" - (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_cval cval) + (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_cval_param cval) | I_init (ctyp, id, cval) -> ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline ^^ ksprintf string " CREATE_OF(%s, %s)(&%s, %s);" @@ -2372,6 +2386,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | CT_bit -> "UINT64_C(0)", [] | CT_int64 -> "INT64_C(0xdeadc0de)", [] | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] + | CT_sbits _ -> "undefined_sbits()", [] | CT_bool -> "false", [] | CT_enum (_, ctor :: _) -> sgen_id ctor, [] | CT_tup ctyps when is_stack_ctyp ctyp -> @@ -3032,7 +3047,7 @@ let sgen_finish = function let instrument_tracing ctx = let module StringSet = Set.Make(String) in - let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in + let traceable = StringSet.of_list ["fbits"; "sail_string"; "lbits"; "sail_int"; "unit"; "bool"] in let rec instrument = function | (I_aux (I_funcall (clexp, _, id, args), _) as instr) :: instrs -> let trace_start = diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 6cd75981..268763ad 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -63,6 +63,7 @@ xml = '<testsuites>\n' xml += test_c('unoptimized C', '', '', True) xml += test_c('optimized C', '-O2', '-O', True) xml += test_c('constant folding', '', '-Oconstant_fold', True) +xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True) xml += test_c('address sanitised', '-O2 -fsanitize=undefined', '-O', False) xml += test_interpreter('interpreter') diff --git a/test/c/small_slice.expect b/test/c/small_slice.expect new file mode 100644 index 00000000..64d39581 --- /dev/null +++ b/test/c/small_slice.expect @@ -0,0 +1,2 @@ +v1 = 0x1234 +v2 = 0x34 diff --git a/test/c/small_slice.sail b/test/c/small_slice.sail new file mode 100644 index 00000000..80878a80 --- /dev/null +++ b/test/c/small_slice.sail @@ -0,0 +1,16 @@ +default Order dec + +$include <prelude.sail> + +function get_16((): unit) -> range(0, 16) = 16 +function get_8((): unit) -> range(0, 16) = 8 + +function main((): unit) -> unit = { + let x = get_16(); + let y = get_8(); + let addr = 0x1234_ABCD; + let v1 = slice(addr, 16, x); + let v2 = slice(addr, 16, y); + print_bits("v1 = ", v1); + print_bits("v2 = ", v2); +}
\ No newline at end of file |