diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/c/gvector.expect | 3 | ||||
| -rw-r--r-- | test/c/gvector.sail | 20 | ||||
| -rw-r--r-- | test/c/sail.h | 344 | ||||
| -rw-r--r-- | test/ocaml/bitfield/bitfield.sail | 9 | ||||
| -rw-r--r-- | test/ocaml/bitfield/expect | 2 |
5 files changed, 374 insertions, 4 deletions
diff --git a/test/c/gvector.expect b/test/c/gvector.expect new file mode 100644 index 00000000..ae7bf842 --- /dev/null +++ b/test/c/gvector.expect @@ -0,0 +1,3 @@ +T[1] = 5 +y[1] = 5 +R[0] = 32'0xDEADBEEF diff --git a/test/c/gvector.sail b/test/c/gvector.sail new file mode 100644 index 00000000..e7553644 --- /dev/null +++ b/test/c/gvector.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <vector_dec.sail> + +val "print_int" : (string, int) -> unit + +register R : vector(32, dec, vector(32, dec, bit)) + +register T : vector(32, dec, int) + +val main : unit -> unit effect {rreg, wreg} + +function main () = { + R[0] = 0xDEAD_BEEF; + T[1] = 5; + print_int("T[1] = ", T[1]); + let y = T; + print_int("y[1] = ", y[1]); + print_bits("R[0] = ", R[0]); +}
\ No newline at end of file diff --git a/test/c/sail.h b/test/c/sail.h index 033d791e..880f5a57 100644 --- a/test/c/sail.h +++ b/test/c/sail.h @@ -26,10 +26,50 @@ void sail_match_failure(void) { exit(1); } +unit sail_assert(bool b, sail_string msg) { + if (b) return UNIT; + fprintf(stderr, "Assertion failed: %s\n", msg); + exit(1); +} + +unit sail_exit(const unit u) { + fprintf(stderr, "Unexpected exit\n"); + exit(1); +} + +void elf_entry(mpz_t *rop, const unit u) { + mpz_set_ui(*rop, 0x8000ul); +} + +// Sail bits are mapped to ints where bitzero = 0 and bitone = 1 +bool eq_bit(const int a, const int b) { + return a == b; +} + +int undefined_bit(unit u) { return 0; } + +// ***** Sail booleans ***** + bool not(const bool b) { return !b; } +bool and_bool(const bool a, const bool b) { + return a && b; +} + +bool or_bool(const bool a, const bool b) { + return a || b; +} + +bool eq_bool(const bool a, const bool b) { + return a == b; +} + +bool undefined_bool(const unit u) { + return false; +} + // ***** Sail strings ***** void init_sail_string(sail_string *str) { char *istr = (char *) malloc(1 * sizeof(char)); @@ -47,11 +87,20 @@ void clear_sail_string(sail_string *str) { free(*str); } +bool eq_string(const sail_string str1, const sail_string str2) { + return strcmp(str1, str2) == 0; +} + unit print_endline(sail_string str) { printf("%s\n", str); return UNIT; } +unit prerr_endline(sail_string str) { + fprintf(stderr, "%s\n", str); + return UNIT; +} + unit print_int(const sail_string str, const mpz_t op) { fputs(str, stdout); mpz_out_str(stdout, 10, op); @@ -64,7 +113,12 @@ unit print_int64(const sail_string str, const int64_t op) { return UNIT; } -// ***** Multiple precision integers ***** +unit sail_putchar(const mpz_t op) { + char c = (char) mpz_get_ui(op); + putchar(c); +} + +// ***** Arbitrary precision integers ***** // We wrap around the GMP functions so they follow a consistent naming // scheme that is shared with the other builtin sail types. @@ -89,6 +143,10 @@ void init_mpz_t_of_sail_string(mpz_t *rop, sail_string str) { mpz_init_set_str(*rop, str, 10); } +int64_t convert_int64_t_of_mpz_t(const mpz_t op) { + return mpz_get_si(op); +} + // ***** Sail builtins for integers ***** bool eq_int(const mpz_t op1, const mpz_t op2) { @@ -103,6 +161,26 @@ bool gt(const mpz_t op1, const mpz_t op2) { return mpz_cmp(op1, op2) > 0; } +bool lteq(const mpz_t op1, const mpz_t op2) { + return mpz_cmp(op1, op2) <= 0; +} + +bool gteq(const mpz_t op1, const mpz_t op2) { + return mpz_cmp(op1, op2) >= 0; +} + +void shl_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { + mpz_mul_2exp(*rop, op1, mpz_get_ui(op2)); +} + +void undefined_int(mpz_t *rop, const unit u) { + mpz_set_ui(*rop, 0ul); +} + +void undefined_range(mpz_t *rop, const mpz_t l, const mpz_t u) { + mpz_set(*rop, l); +} + void add_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { mpz_add(*rop, op1, op2); @@ -113,6 +191,37 @@ void sub_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) mpz_sub(*rop, op1, op2); } +void mult_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) +{ + mpz_mul(*rop, op1, op2); +} + +void div_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) +{ + mpz_tdiv_q(*rop, op1, op2); +} + +void mod_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) +{ + mpz_tdiv_r(*rop, op1, op2); +} + +void max_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { + if (lt(op1, op2)) { + mpz_set(*rop, op2); + } else { + mpz_set(*rop, op1); + } +} + +void min_int(mpz_t *rop, const mpz_t op1, const mpz_t op2) { + if (gt(op1, op2)) { + mpz_set(*rop, op2); + } else { + mpz_set(*rop, op1); + } +} + void neg_int(mpz_t *rop, const mpz_t op) { mpz_neg(*rop, op); } @@ -121,8 +230,20 @@ void abs_int(mpz_t *rop, const mpz_t op) { mpz_abs(*rop, op); } +void pow2(mpz_t *rop, mpz_t exp) { + uint64_t exp_ui = mpz_get_ui(exp); + mpz_t base; + mpz_init_set_ui(base, 2ul); + mpz_pow_ui(*rop, base, exp_ui); + mpz_clear(base); +} + // ***** Sail bitvectors ***** +void length_bv_t(mpz_t *rop, const bv_t op) { + mpz_set_ui(*rop, op.len); +} + void init_bv_t(bv_t *rop) { rop->bits = malloc(sizeof(mpz_t)); rop->len = 0; @@ -140,12 +261,32 @@ void set_bv_t(bv_t *rop, const bv_t op) { mpz_set(*rop->bits, *op.bits); } -void append_64(bv_t *rop, bv_t op, const uint64_t chunk) { +void append_64(bv_t *rop, const bv_t op, const uint64_t chunk) { rop->len = rop->len + 64ul; mpz_mul_2exp(*rop->bits, *op.bits, 64ul); mpz_add_ui(*rop->bits, *rop->bits, chunk); } +void append(bv_t *rop, const bv_t op1, const bv_t op2) { + rop->len = op1.len + op2.len; + mpz_mul_2exp(*rop->bits, *op1.bits, op2.len); + mpz_add(*rop->bits, *rop->bits, *op2.bits); +} + +void replicate_bits(bv_t *rop, const bv_t op1, const mpz_t op2) { + uint64_t op2_ui = mpz_get_ui(op2); + rop->len = op1.len * op2_ui; + mpz_set(*rop->bits, *op1.bits); + for (int i = 1; i < op2_ui; i++) { + mpz_mul_2exp(*rop->bits, *rop->bits, op2_ui); + mpz_add(*rop->bits, *rop->bits, *op1.bits); + } +} + +void slice(bv_t *rop, const bv_t op, const mpz_t i, const mpz_t len) { + // TODO +} + uint64_t convert_uint64_t_of_bv_t(const bv_t op) { return mpz_get_ui(*op.bits); } @@ -165,6 +306,10 @@ void clear_bv_t(bv_t *rop) { free(rop->bits); } +void undefined_bv_t(bv_t *rop, mpz_t len, int bit) { + zeros(rop, len); +} + void mask(bv_t *rop) { if (mpz_sizeinbase(*rop->bits, 2) > rop->len) { mpz_t m; @@ -176,6 +321,49 @@ void mask(bv_t *rop) { } } +void and_bits(bv_t *rop, const bv_t op1, const bv_t op2) { + rop->len = op1.len; + mpz_and(*rop->bits, *op1.bits, *op2.bits); +} + +void or_bits(bv_t *rop, const bv_t op1, const bv_t op2) { + rop->len = op1.len; + mpz_ior(*rop->bits, *op1.bits, *op2.bits); +} + +void not_bits(bv_t *rop, const bv_t op) { + rop->len = op.len; + mpz_com(*rop->bits, *op.bits); +} + +void xor_bits(bv_t *rop, const bv_t op1, const bv_t op2) { + rop->len = op1.len; + mpz_xor(*rop->bits, *op1.bits, *op2.bits); +} + +bool eq_bits(const bv_t op1, const bv_t op2) { + return mpz_cmp(*op1.bits, *op2.bits) == 0; +} + +void sail_uint(mpz_t *rop, const bv_t op) { + mpz_set(*rop, *op.bits); +} + +void sint(mpz_t *rop, const bv_t op) { + if (mpz_tstbit(*op.bits, op.len - 1)) { + mpz_set(*rop, *op.bits); + mpz_clrbit(*rop, op.len - 1); + mpz_t x; + mpz_init(x); + mpz_setbit(x, op.len - 1); + mpz_neg(x, x); + mpz_add(*rop, *rop, *op.bits); + mpz_clear(x); + } else { + mpz_set(*rop, *op.bits); + } +} + void add_bits(bv_t *rop, const bv_t op1, const bv_t op2) { rop->len = op1.len; mpz_add(*rop->bits, *op1.bits, *op2.bits); @@ -188,9 +376,161 @@ void add_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) { mask(rop); } +void sub_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) { + rop->len = op1.len; + mpz_sub(*rop->bits, *op1.bits, op2); + mask(rop); +} + +void get_slice_int(bv_t *rop, const mpz_t n, const mpz_t m, const mpz_t o) { + // TODO +} + +void set_slice_int(mpz_t *rop, const mpz_t n, const mpz_t m, const mpz_t o, const bv_t op) { + // TODO +} + +void vector_update_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n, const mpz_t m, const bv_t slice) { + // TODO +} + +void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n, const mpz_t m) { + // TODO +} + +int bitvector_access(const bv_t op, const mpz_t n) { + return 0; // TODO +} + +void hex_slice (bv_t *rop, const sail_string hex, const mpz_t n, const mpz_t m) { + // TODO +} + +void set_slice (bv_t *rop, const mpz_t len, const mpz_t slen, const bv_t op, const mpz_t i, const bv_t slice) { + // TODO +} + unit print_bits(const sail_string str, const bv_t op) { fputs(str, stdout); gmp_printf("%d'0x%ZX\n", op.len, op.bits); } +// ***** Real number implementation ***** + +#define REAL_FLOAT + +#ifdef REAL_FLOAT + +typedef mpf_t real; + +#define FLOAT_PRECISION 255 + +void setup_real(void) { + mpf_set_default_prec(FLOAT_PRECISION); +} + +void init_real(real *rop) { + mpf_init(*rop); +} + +void clear_real(real *rop) { + mpf_clear(*rop); +} + +void set_real(real *rop, const real op) { + mpf_set(*rop, op); +} + +void undefined_real(real *rop, unit u) { + mpf_set_ui(*rop, 0ul); +} + +void neg_real(real *rop, const real op) { + mpf_neg(*rop, op); +} + +void mult_real(real *rop, const real op1, const real op2) { + mpf_mul(*rop, op1, op2); +} + +void sub_real(real *rop, const real op1, const real op2) { + mpf_sub(*rop, op1, op2); +} + +void add_real(real *rop, const real op1, const real op2) { + mpf_add(*rop, op1, op2); +} + +void div_real(real *rop, const real op1, const real op2) { + mpf_div(*rop, op1, op2); +} + +void sqrt_real(real *rop, const real op) { + mpf_sqrt(*rop, op); +} + +void abs_real(real *rop, const real op) { + mpf_abs(*rop, op); +} + +void round_up(mpz_t *rop, const real op) { + mpf_t x; + mpf_ceil(x, op); + mpz_set_ui(*rop, mpf_get_ui(x)); + mpf_clear(x); +} + +void round_down(mpz_t *rop, const real op) { + mpf_t x; + mpf_floor(x, op); + mpz_set_ui(*rop, mpf_get_ui(x)); + mpf_clear(x); +} + +void to_real(real *rop, const mpz_t op) { + mpf_set_z(*rop, op); +} + +bool eq_real(const real op1, const real op2) { + return mpf_cmp(op1, op2) == 0; +} + +bool lt_real(const real op1, const real op2) { + return mpf_cmp(op1, op2) < 0; +} + +bool gt_real(const real op1, const real op2) { + return mpf_cmp(op1, op2) > 0; +} + +bool lteq_real(const real op1, const real op2) { + return mpf_cmp(op1, op2) <= 0; +} + +bool gteq_real(const real op1, const real op2) { + return mpf_cmp(op1, op2) >= 0; +} + +void real_power(real *rop, const real base, const mpz_t exp) { + uint64_t exp_ui = mpz_get_ui(exp); + mpf_pow_ui(*rop, base, exp_ui); +} + +void init_real_of_sail_string(real *rop, const sail_string op) { + // FIXME + mpf_init(*rop); +} + #endif + +#endif + +// ***** Memory ***** + +unit write_ram(const mpz_t m, const mpz_t n, const bv_t x, const bv_t y, const bv_t data) { + return UNIT; +} + +void read_ram(bv_t *data, const mpz_t m, const mpz_t n, const bv_t x, const bv_t y) { + // TODO +} diff --git a/test/ocaml/bitfield/bitfield.sail b/test/ocaml/bitfield/bitfield.sail index 5a70d52e..2a53ab3c 100644 --- a/test/ocaml/bitfield/bitfield.sail +++ b/test/ocaml/bitfield/bitfield.sail @@ -12,7 +12,8 @@ bitfield cr : bits(8) = { register CR : cr bitfield dr : vector(4, inc, bit) = { - DR0 : 2 .. 3 + DR0 : 2 .. 3, + LT : 2 } register DR : dr @@ -28,5 +29,9 @@ function main () = { print_bits("CR.CR0: ", CR.CR0()); print_bits("CR: ", CR.bits()); CR->CR3() = 0b0; - print_bits("CR: ", CR.bits()) + print_bits("CR: ", CR.bits()); + CR = update_CR1(CR, 0b11); + print_bits("CR.CR1: ", CR.CR1()); + CR = update_CR1(CR, 0b01); + print_bits("CR.CR1: ", CR.CR1()); } diff --git a/test/ocaml/bitfield/expect b/test/ocaml/bitfield/expect index 63247dfd..e6e5a618 100644 --- a/test/ocaml/bitfield/expect +++ b/test/ocaml/bitfield/expect @@ -3,3 +3,5 @@ CR: 0x0F CR.CR0: 0x8 CR: 0x8F CR: 0x8E +CR.CR1: 0b11 +CR.CR1: 0b01 |