Merge branch 'sail2' of github.com:rems-project/sail into sail2

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