Have generic vectors working in C backend

10 files changed, 233 insertions, 8 deletions

diff --git a/aarch64/no_vector.isail b/aarch64/no_vector.isail
index 15e29e26..aa0855d5 100644
--- a/aarch64/no_vector.isail
+++ b/aarch64/no_vector.isail
@@ -1,4 +1,8 @@
 :unload
 :load prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail
 initialize_registers()
-:run
\ No newline at end of file
+:run
+:elf ../bench.elf
+main()
+:run
+:q
\ No newline at end of file
diff --git a/lib/flow.sail b/lib/flow.sail
index 8c902803..1a0e0f2f 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -34,6 +34,8 @@ val lt_int = "lt" : (int, int) -> bool
 val gt_int = "lt" : (int, int) -> bool
 
 overload operator == = {eq_atom, eq_range, eq_int}
+overload operator | = {or_bool}
+overload operator & = {and_bool}
 
 $ifdef TEST
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index e24f5111..8a55ed61 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -13,6 +13,18 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 /* Used for creating long bitvector literals in the C backend. */
 val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
+val vector_access = {
+  ocaml: "access",
+  lem: "access_list_dec",
+  c: "vector_access"
+} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
+
+val vector_update = {
+  ocaml: "update",
+  lem: "update_list_dec",
+  c: "vector_update"
+} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
+
 val add_bits = {
   ocaml: "add_vec",
   c: "add_bits"
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 77f1b39f..92da4c3d 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -927,6 +927,11 @@ let rec instr_ctyps (I_aux (instr, aux)) =
   | I_throw cval | I_jump (cval, _) | I_return cval -> [cval_ctyp cval]
   | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure -> []
 
+let rec c_ast_registers = function
+  | CDEF_reg_dec (id, ctyp) :: ast -> (id, ctyp) :: c_ast_registers ast
+  | _ :: ast -> c_ast_registers ast
+  | [] -> []
+
 let cdef_ctyps ctx = function
   | CDEF_reg_dec (_, ctyp) -> [ctyp]
   | CDEF_fundef (id, _, _, instrs) ->
@@ -1071,6 +1076,10 @@ let is_ct_list = function
   | CT_list _ -> true
   | _ -> false
 
+let is_ct_vector = function
+  | CT_vector _ -> true
+  | _ -> false
+
 let rec is_bitvector = function
   | [] -> true
   | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals
@@ -2073,8 +2082,9 @@ let sgen_ctyp = function
   | CT_enum (id, _) -> "enum " ^ sgen_id id
   | CT_variant (id, _) -> "struct " ^ sgen_id id
   | CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
-  | CT_vector _ -> "int" (* FIXME *)
+  | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
   | CT_string -> "sail_string"
+  | CT_real -> "real"
 
 let sgen_ctyp_name = function
   | CT_unit -> "unit"
@@ -2089,8 +2099,9 @@ let sgen_ctyp_name = function
   | CT_enum (id, _) -> sgen_id id
   | CT_variant (id, _) -> sgen_id id
   | CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
-  | CT_vector _ -> "int" (* FIXME *)
+  | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
   | CT_string -> "sail_string"
+  | CT_real -> "real"
 
 let sgen_cval_param (frag, ctyp) =
   match ctyp with
@@ -2151,6 +2162,18 @@ let rec codegen_instr ctx (I_aux (instr, _)) =
   | I_funcall (x, f, args, ctyp) ->
      let args = Util.string_of_list ", " sgen_cval args in
      let fname = if Env.is_extern f ctx.tc_env "c" then Env.get_extern f ctx.tc_env "c" else sgen_id f in
+     let fname =
+       match fname, ctyp with
+       | "vector_access", CT_bit -> "bitvector_access"
+       | "vector_access", _ -> Printf.sprintf "vector_access_%s" (sgen_ctyp_name ctyp)
+       | "vector_update", CT_uint64 _ -> "update_uint64_t"
+       | "vector_update", CT_bv _ -> "update_bv"
+       | "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp)
+       | "undefined_vector", CT_uint64 _ -> "undefined_uint64_t"
+       | "undefined_vector", CT_bv _ -> "undefined_bv_t"
+       | "undefined_vector", _ -> Printf.sprintf "undefined_vector_%s" (sgen_ctyp_name ctyp)
+       | fname, _ -> fname
+     in
      if is_stack_ctyp ctyp then
        string (Printf.sprintf "  %s = %s(%s);" (sgen_clexp_pure x) fname args)
      else
@@ -2445,6 +2468,93 @@ let codegen_list ctx ctyp =
       ^^ codegen_cons id ctyp ^^ twice hardline
     end
 
+let codegen_vector ctx (direction, ctyp) =
+  let id = mk_id (string_of_ctyp (CT_vector (direction, ctyp))) in
+  if IdSet.mem id !generated then
+    empty
+  else
+    let vector_typedef =
+      string (Printf.sprintf "struct %s {\n  size_t len;\n  %s *data;\n};\n" (sgen_id id) (sgen_ctyp ctyp))
+      ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id))
+    in
+    let vector_init =
+      string (Printf.sprintf "void init_%s(%s *rop) {\n  rop->len = 0;\n  rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
+    in
+    let vector_set =
+      string (Printf.sprintf "void set_%s(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+      ^^ string (Printf.sprintf "  clear_%s(rop);\n" (sgen_id id))
+      ^^ string "  rop->len = op.len;\n"
+      ^^ string (Printf.sprintf "  rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
+      ^^ string "  for (int i = 0; i < op.len; i++) {\n"
+      ^^ string (if is_stack_ctyp ctyp then
+                   "    (rop->data)[i] = op.data[i];\n"
+                 else
+                   Printf.sprintf "    init_%s((rop->data) + i);\n    set_%s((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+      ^^ string "  }\n"
+      ^^ string "}"
+    in
+    let vector_clear =
+      string (Printf.sprintf "void clear_%s(%s *rop) {\n" (sgen_id id) (sgen_id id))
+      ^^ (if is_stack_ctyp ctyp then empty
+         else
+           string "  for (int i = 0; i < (rop->len); i++) {\n"
+           ^^ string (Printf.sprintf "    clear_%s((rop->data) + i);\n" (sgen_ctyp_name ctyp))
+           ^^ string "  }\n")
+      ^^ string "  if (rop->data != NULL) free(rop->data);\n"
+      ^^ string "}"
+    in
+    let vector_update =
+      string (Printf.sprintf "void vector_update_%s(%s *rop, %s op, mpz_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+      ^^ string "  int m = mpz_get_ui(n);\n"
+      ^^ string "  if (rop->data == op.data) {\n"
+      ^^ string (if is_stack_ctyp ctyp then
+                   "    rop->data[m] = elem;\n"
+                 else
+                   Printf.sprintf "  set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+      ^^ string "  } else {\n"
+      ^^ string (Printf.sprintf "    set_%s(rop, op);\n" (sgen_id id))
+      ^^ string (if is_stack_ctyp ctyp then
+                   "    rop->data[m] = elem;\n"
+                 else
+                   Printf.sprintf "  set_%s((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+      ^^ string "  }\n"
+      ^^ string "}"
+    in
+    let vector_access =
+      if is_stack_ctyp ctyp then
+        string (Printf.sprintf "%s vector_access_%s(%s op, mpz_t n) {\n" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id))
+        ^^ string "  int m = mpz_get_ui(n);\n"
+        ^^ string "  return op.data[m];\n"
+        ^^ string "}"
+      else
+        string (Printf.sprintf "void vector_access_%s(%s *rop, %s op, mpz_t n) {\n" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id))
+        ^^ string "  int m = mpz_get_ui(n);\n"
+        ^^ string (Printf.sprintf "  set_%s(rop, op.data[m]);\n" (sgen_ctyp_name ctyp))
+        ^^ string "}"
+    in
+    let vector_undefined =
+      string (Printf.sprintf "void undefined_vector_%s(%s *rop, mpz_t len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+      ^^ string (Printf.sprintf "  rop->len = mpz_get_ui(len);\n")
+      ^^ string (Printf.sprintf "  rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
+      ^^ string "  for (int i = 0; i < (rop->len); i++) {\n"
+      ^^ string (if is_stack_ctyp ctyp then
+                   "    (rop->data)[i] = elem;\n"
+                 else
+                   Printf.sprintf "    init_%s((rop->data) + i);\n    set_%s((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+      ^^ string "  }\n"
+      ^^ string "}"
+    in
+    begin
+      generated := IdSet.add id !generated;
+      vector_typedef ^^ twice hardline
+      ^^ vector_init ^^ twice hardline
+      ^^ vector_clear ^^ twice hardline
+      ^^ vector_undefined ^^ twice hardline
+      ^^ vector_access ^^ twice hardline
+      ^^ vector_set ^^ twice hardline
+      ^^ vector_update ^^ twice hardline
+    end
+
 let codegen_def' ctx = function
   | CDEF_reg_dec (id, ctyp) ->
      string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline
@@ -2504,13 +2614,20 @@ let codegen_def ctx def =
     | CT_list ctyp -> ctyp
     | _ -> assert false
   in
+  let unvector = function
+    | CT_vector (direction, ctyp) -> (direction, ctyp)
+    | _ -> assert false
+  in
   let tups = List.filter is_ct_tup (cdef_ctyps ctx def) in
   let tups = List.map (fun ctyp -> codegen_tup ctx (untup ctyp)) tups in
   let lists = List.filter is_ct_list (cdef_ctyps ctx def) in
   let lists = List.map (fun ctyp -> codegen_list ctx (unlist ctyp)) lists in
+  let vectors = List.filter is_ct_vector (cdef_ctyps ctx def) in
+  let vectors = List.map (fun ctyp -> codegen_vector ctx (unvector ctyp)) vectors in
   prerr_endline (Pretty_print_sail.to_string (pp_cdef def));
   concat tups
   ^^ concat lists
+  ^^ concat vectors
   ^^ codegen_def' ctx def
 
 let compile_ast ctx (Defs defs) =
@@ -2542,14 +2659,29 @@ let compile_ast ctx (Defs defs) =
       List.map (fun n -> Printf.sprintf "  kill_letbind_%d();" n) ctx.letbinds
     in
 
+    let regs = c_ast_registers cdefs in
+
+    let register_init_clear (id, ctyp) =
+      if is_stack_ctyp ctyp then
+        [], []
+      else
+        [ Printf.sprintf "  init_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ],
+        [ Printf.sprintf "  clear_%s(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ]
+    in
+
     let postamble = separate hardline (List.map string
        ( [ "int main(void)";
-           "{" ]
+           "{";
+           "  setup_real();" ]
        @ fst exn_boilerplate
+       @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
+       @ (if regs = [] then [] else [ "  zinitializze_registers(UNIT);" ])
        @ letbind_initializers
        @ [ "  zmain(UNIT);" ]
        @ letbind_finalizers
+       @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs)
        @ snd exn_boilerplate
+       @ [ "  return 0;" ]
        @ [ "}" ] ))
     in
 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 1dac7a1c..7620ca50 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -265,7 +265,7 @@ let fixities =
         (mk_id "|", (InfixR, 2));
       ]
   in
-  ref Bindings.empty (*(fixities' : (prec * int) Bindings.t)*)
+  ref (fixities' : (prec * int) Bindings.t)
 
 let rec doc_exp (E_aux (e_aux, _) as exp) =
   match e_aux with
diff --git a/src/sail.ml b/src/sail.ml
index 35a7279b..95e060b2 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -88,7 +88,7 @@ let options = Arg.align ([
     Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
     " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml");
   ( "-c",
-    Arg.Tuple [Arg.Set opt_print_c; (* Arg.Set Initial_check.opt_undefined_gen *)],
+    Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
     " output a C translated version of the input");
   ( "-lem_ast",
     Arg.Set opt_print_lem_ast,
diff --git a/src/specialize.ml b/src/specialize.ml
index efa8783e..2ebc7307 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -80,6 +80,10 @@ let id_of_instantiation id instantiation =
   let str = Util.zencode_string (Util.string_of_list ", " string_of_binding (KBindings.bindings instantiation)) ^ "#" in
   prepend_id str id
 
+let string_of_instantiation instantiation =
+  let string_of_binding (kid, uvar) = string_of_kid kid ^ " => " ^ Type_check.string_of_uvar uvar in
+  Util.zencode_string (Util.string_of_list ", " string_of_binding (KBindings.bindings instantiation))
+
 (* Returns a list of all the instantiations of a function id in an
    ast. *)
 let rec instantiations_of id ast =
@@ -161,6 +165,7 @@ let specialize_id_valspec instantiations id ast =
        let typschm = mk_typschm typq typ in
 
        let spec_id = id_of_instantiation id instantiation in
+
        if IdSet.mem spec_id !spec_ids then [] else
          begin
            spec_ids := IdSet.add spec_id !spec_ids;
@@ -209,7 +214,7 @@ let specialize_id_overloads instantiations id (Defs defs) =
    valspecs are then re-specialized. This process is iterated until
    the whole spec is specialized. *)
 let remove_unused_valspecs ast =
-  let calls = ref (IdSet.singleton (mk_id "main")) in
+  let calls = ref (IdSet.of_list [mk_id "main"; mk_id "execute"; mk_id "decode"; mk_id "initialize_registers"]) in
   let vs_ids = Initial_check.val_spec_ids ast in
 
   let inspect_exp = function
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..8afb192d 100644
--- a/test/c/sail.h
+++ b/test/c/sail.h
@@ -30,6 +30,8 @@ bool not(const bool b) {
   return !b;
 }
 
+int undefined_bit(unit u) { return 0; }
+
 // ***** Sail strings *****
 void init_sail_string(sail_string *str) {
   char *istr = (char *) malloc(1 * sizeof(char));
@@ -64,7 +66,7 @@ unit print_int64(const sail_string str, const int64_t op) {
   return UNIT;
 }
 
-// ***** Multiple precision integers *****
+// ***** 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.
@@ -103,6 +105,10 @@ bool gt(const mpz_t op1, const mpz_t op2) {
   return mpz_cmp(op1, op2) > 0;
 }
 
+void undefined_int(mpz_t *rop, const unit u) {
+  mpz_set_ui(*rop, 0ul);
+}
+
 void add_int(mpz_t *rop, const mpz_t op1, const mpz_t op2)
 {
   mpz_add(*rop, op1, op2);
@@ -165,6 +171,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;
@@ -182,6 +192,19 @@ void add_bits(bv_t *rop, const bv_t op1, const bv_t op2) {
   mpz_clrbit(*rop->bits, op1.len);
 }
 
+uint64_t add_bits_32(const uint64_t op1, const uint64_t op2) {
+  return (op1 + op2) & 0x00000000FFFFFFFFul;
+}
+
+
+bool eq_bits(const bv_t op1, const bv_t op2) {
+  return mpz_cmp(*op1.bits, *op2.bits) == 0;
+}
+
+bool eq_bits_32(const uint64_t op1, const uint64_t op2) {
+  return (op1 == op2);
+}
+
 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);
@@ -193,4 +216,28 @@ unit print_bits(const sail_string str, const bv_t op) {
   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);
+}
+
+#endif
+
 #endif