Support for large bitvector literals in C backend

3 files changed, 112 insertions, 1 deletions

diff --git a/test/c/bitvector.expect b/test/c/bitvector.expect
new file mode 100644
index 00000000..9e11e149
--- /dev/null
+++ b/test/c/bitvector.expect
@@ -0,0 +1,10 @@
+x = 16'0xBEEF
+y = 200'0x0
+z = 16'0xCAFE
+zero_extend(z) = 32'0xCAFE
+q = 72'0xABFEEDDEADBEEFCAFE
+k = 8'0xFF
+k + k = 8'0xFE
+0xFF + 1 = 8'0x0
+0xFF + 2 = 8'0x1
+0xFF + 3 = 8'0x2
diff --git a/test/c/bitvector.sail b/test/c/bitvector.sail
new file mode 100644
index 00000000..5311caff
--- /dev/null
+++ b/test/c/bitvector.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+val test : (vector(16, dec, bit), vector(200, dec, bit)) -> bool
+
+function test (x, y)  = {
+  print_bits("x = ", x);
+  print_bits("y = ", y);
+  true
+}
+
+val main : unit -> unit
+
+function main () = {
+  if test(0xBEEF, zeros(200)) then () else ();
+  let z = 0xCAFE;
+  print_bits("z = ", z);
+  print_bits("zero_extend(z) = ", zero_extend(z, 32));
+  let q = 0xAB_FEED_DEAD_BEEF_CAFE;
+  print_bits("q = ", q);
+  let k = 0xFF;
+  print_bits("k = ", k);
+  print_bits("k + k = ", add_bits(k, k));
+  print_bits("0xFF + 1 = ", add_bits_int(0xFF, 1));
+  print_bits("0xFF + 2 = ", add_bits_int(0xFF, 2));
+  print_bits("0xFF + 3 = ", add_bits_int(0xFF, 3));
+  ()
+}
diff --git a/test/c/sail.h b/test/c/sail.h
index e86dd542..033d791e 100644
--- a/test/c/sail.h
+++ b/test/c/sail.h
@@ -14,7 +14,7 @@ typedef int unit;
 
 typedef struct {
   mp_bitcnt_t len;
-  mpz_t bits;
+  mpz_t *bits;
 } bv_t;
 
 typedef char *sail_string;
@@ -121,4 +121,76 @@ void abs_int(mpz_t *rop, const mpz_t op) {
   mpz_abs(*rop, op);
 }
 
+// ***** Sail bitvectors *****
+
+void init_bv_t(bv_t *rop) {
+  rop->bits = malloc(sizeof(mpz_t));
+  rop->len = 0;
+  mpz_init(*rop->bits);
+}
+
+void init_bv_t_of_uint64_t(bv_t *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);
+}
+
+void set_bv_t(bv_t *rop, const bv_t op) {
+  rop->len = op.len;
+  mpz_set(*rop->bits, *op.bits);
+}
+
+void append_64(bv_t *rop, 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);
+}
+
+uint64_t convert_uint64_t_of_bv_t(const bv_t op) {
+  return mpz_get_ui(*op.bits);
+}
+
+void zeros(bv_t *rop, const mpz_t op) {
+  rop->len = mpz_get_ui(op);
+  mpz_set_ui(*rop->bits, 0ul);
+}
+
+void zero_extend(bv_t *rop, const bv_t op, const mpz_t len) {
+  rop->len = mpz_get_ui(len);
+  mpz_set(*rop->bits, *op.bits);
+}
+
+void clear_bv_t(bv_t *rop) {
+  mpz_clear(*rop->bits);
+  free(rop->bits);
+}
+
+void mask(bv_t *rop) {
+  if (mpz_sizeinbase(*rop->bits, 2) > rop->len) {
+    mpz_t m;
+    mpz_init(m);
+    mpz_ui_pow_ui(m, 2ul, rop->len);
+    mpz_sub_ui(m, m, 1ul);
+    mpz_and(*rop->bits, *rop->bits, m);
+    mpz_clear(m);
+  }
+}
+
+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);
+  mpz_clrbit(*rop->bits, op1.len);
+}
+
+void add_bits_int(bv_t *rop, const bv_t op1, const mpz_t op2) {
+  rop->len = op1.len;
+  mpz_add(*rop->bits, *op1.bits, op2);
+  mask(rop);
+}
+
+unit print_bits(const sail_string str, const bv_t op) {
+  fputs(str, stdout);
+  gmp_printf("%d'0x%ZX\n", op.len, op.bits);
+}
+
 #endif