Support for large bitvector literals in C backend

9 files changed, 181 insertions, 7 deletions

diff --git a/language/bytecode.ott b/language/bytecode.ott
index 19c4d9cc..161be4b3 100644
--- a/language/bytecode.ott
+++ b/language/bytecode.ott
@@ -137,6 +137,8 @@ cdef :: 'CDEF_' ::=
     } {
       instr0 ; ... ; instri
     } :: :: let
+% The first list of instructions creates up the global letbinding, the
+% second kills it.
   | function id mid ( id0 , ... , idn ) {
       instr0 ; ... ; instrm
     } :: :: fundef
\ No newline at end of file
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
new file mode 100644
index 00000000..84493f73
--- /dev/null
+++ b/lib/vector_dec.sail
@@ -0,0 +1,25 @@
+$ifndef _VECTOR_DEC
+$define _VECTOR_DEC
+
+type bits ('n : Int) = vector('n, dec, bit)
+
+val "zeros" : forall 'n. atom('n) -> bits('n)
+
+val "print_bits" : forall 'n. (string, bits('n)) -> unit
+
+val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
+val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
+
+val add_bits = {
+  ocaml: "add_vec",
+  c: "add_bits"
+} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val add_bits_int = {
+  ocaml: "add_vec_int",
+  c: "add_bits_int"
+} : forall 'n. (bits('n), int) -> bits('n)
+
+$endif
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 8c33fd5c..934bfdff 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -945,7 +945,7 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
   | I_alloc (ctyp, id) ->
      pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
   | I_init (ctyp, id, cval) ->
-     pp_keyword "create" ^^ parens (pp_ctyp ctyp) ^^ string " = " ^^ pp_cval cval
+     pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
   | I_funcall (x, f, args, ctyp2) ->
      separate space [ pp_clexp x; string "=";
                       string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args);
@@ -1026,6 +1026,11 @@ let rec string_of_aval_bit = function
   | AV_lit (L_aux (L_zero, _), _) -> "0"
   | AV_lit (L_aux (L_one, _), _) -> "1"
 
+let rec chunkify n xs =
+  match Util.take n xs, Util.drop n xs with
+  | xs, [] -> [xs]
+  | xs, ys -> xs :: chunkify n ys
+
 let rec compile_aval ctx = function
   | AV_C_fragment (frag, typ) ->
      [], (frag, ctyp_of_typ ctx typ), []
@@ -1053,7 +1058,6 @@ let rec compile_aval ctx = function
   | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit "0", CT_bit), []
   | AV_lit (L_aux (L_one, _), _) -> [], (F_lit "1", CT_bit), []
 
-
   | AV_lit (L_aux (_, l) as lit, _) ->
      c_error ~loc:l ("Encountered unexpected literal " ^ string_of_lit lit)
 
@@ -1078,7 +1082,7 @@ let rec compile_aval ctx = function
 
   | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 ->
      begin
-       let bitstring = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit avals)) in
+       let bitstring = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit avals) ^ "ul") in
        let len = List.length avals in
        match destruct_vector ctx.tc_env typ with
        | Some (_, Ord_aux (Ord_inc, _), _) ->
@@ -1091,6 +1095,21 @@ let rec compile_aval ctx = function
           c_error "Encountered vector literal without vector type"
      end
 
+  | AV_vector (avals, typ) when is_bitvector avals ->
+     let len = List.length avals in
+     let bitstring avals = F_lit ("0b" ^ String.concat "" (List.map string_of_aval_bit avals) ^ "ul") in
+     let first_chunk = bitstring (Util.take (len mod 64) avals) in
+     let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in
+     let gs = gensym () in
+     [idecl (CT_bv true) gs;
+      iinit (CT_bv true) gs (first_chunk, CT_uint64 (len mod 64, true))]
+     @ List.map (fun chunk -> ifuncall (CL_id gs)
+                                       (mk_id "append_64")
+                                       [(F_id gs, CT_bv true); (chunk, CT_uint64 (64, true))]
+                                       (CT_bv true)) chunks,
+     (F_id gs, CT_bv true),
+     [iclear (CT_bv true) gs]
+
   | AV_vector _ ->
      c_error "Have AV_vector"
 
@@ -1140,7 +1159,7 @@ let compile_funcall ctx id args typ =
       fun ret -> ifuncall ret id sargs ret_ctyp
     else if not (is_stack_ctyp ret_ctyp) && is_stack_ctyp final_ctyp then
       let gs = gensym () in
-      setup := idecl ret_ctyp gs :: ialloc ret_ctyp gs :: !setup;
+      setup := ialloc ret_ctyp gs :: idecl ret_ctyp gs :: !setup;
       setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup;
       cleanup := iclear ret_ctyp gs :: !cleanup;
       fun ret -> iconvert ret final_ctyp gs ret_ctyp
@@ -1901,6 +1920,15 @@ let sgen_ctyp_name = function
   | CT_variant (id, _) -> sgen_id id
   | CT_string -> "sail_string"
 
+let sgen_cval_param (frag, ctyp) =
+  match ctyp with
+  | CT_bv direction ->
+     string_of_fragment frag ^ ", " ^ string_of_bool direction
+  | CT_uint64 (len, direction) ->
+     string_of_fragment frag ^ ", " ^ string_of_int len ^ "ul , " ^ string_of_bool direction
+  | _ ->
+     string_of_fragment frag
+
 let sgen_cval = function (frag, _) -> string_of_fragment frag
 
 let sgen_clexp = function
@@ -1962,7 +1990,7 @@ let rec codegen_instr ctx (I_aux (instr, _)) =
                             (sgen_ctyp_name ctyp)
                             (sgen_ctyp_name (cval_ctyp cval))
                             (sgen_id id)
-                            (sgen_cval cval))
+                            (sgen_cval_param cval))
   | I_alloc (ctyp, id) ->
      string (Printf.sprintf "  init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
   | I_convert (x, ctyp1, y, ctyp2) ->
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index eb11a62d..b31ca9df 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -549,4 +549,6 @@ let shift_bits_left (x, y) =
   let rbits = x @ zeros in
   drop yi rbits
 
+let zeros n = replicate_bits ([B0], n)
+
 let speculate_conditional_success () = true
diff --git a/src/util.ml b/src/util.ml
index 94caf9fc..a627fd58 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -387,7 +387,12 @@ let is_none opt = not (is_some opt)
 let rec take n xs = match n, xs with
   | 0, _ -> []
   | n, [] -> []
-  | n, (x :: xs) -> x :: take (n - 1) xs 
+  | n, (x :: xs) -> x :: take (n - 1) xs
+
+let rec drop n xs = match n, xs with
+  | 0, xs -> xs
+  | n, [] -> []
+  | n, (x :: xs) -> drop (n - 1) xs
 
 let termcode n =
   if !opt_colors then
diff --git a/src/util.mli b/src/util.mli
index 8aa7f42d..b74442a2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -230,6 +230,7 @@ val is_some : 'a option -> bool
 val is_none : 'a option -> bool
 
 val take : int -> 'a list -> 'a list
+val drop : int -> 'a list -> 'a list
 
 val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
 
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