More efficient bitfield implementation

2 files changed, 45 insertions, 34 deletions

diff --git a/src/bitfield.ml b/src/bitfield.ml
index 391a653d..161908cd 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -64,62 +64,68 @@ let rec combine = function
      Defs (defs @ defs')
 
 let newtype name size order =
-  let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in
-  ast_of_def_string order nt
-
-(* These functions define the getter and setter for all the bits in the field. *)
-let full_getter name size order =
-  let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in
-  let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in
-  combine [ast_of_def_string order fg_val; ast_of_def_string order fg_function]
-
-let full_setter name size order =
-  let fs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" name name (bitvec size order) in
-  let fs_function = String.concat "\n"
-    [ Printf.sprintf "function _set_%s (r_ref, v) = {" name;
-                     "  r = _reg_deref(r_ref);";
-      Printf.sprintf "  r = Mk_%s(v);" name;
-                     "  (*r_ref) = r";
-                     "}"
-    ]
+  let chunks_64 =
+    Util.list_init (size / 64) (fun i -> Printf.sprintf "%s_chunk_%i : vector(64, %s, bit)" name i (string_of_order order))
   in
-  combine [ast_of_def_string order fs_val; ast_of_def_string order fs_function]
-
-let full_overload name order =
-  ast_of_def_string order (Printf.sprintf "overload _mod_bits = {_get_%s, _set_%s}" name name)
+  let chunks =
+    if size mod 64 = 0 then chunks_64 else
+      let chunk_rem =
+        Printf.sprintf "%s_chunk_%i : vector(%i, %s, bit)" name (List.length chunks_64) (size mod 64) (string_of_order order)
+      in
+      chunk_rem :: List.rev chunks_64
+  in
+  let nt = Printf.sprintf "struct %s = {\n  %s }" name (Util.string_of_list ",\n  " (fun x -> x) chunks) in
+  ast_of_def_string order nt
 
-let full_accessor name size order =
-  combine [full_getter name size order; full_setter name size order; full_overload name order]
+let rec translate_indices hi lo =
+  if hi / 64 = lo / 64 then
+    [(hi / 64, hi mod 64, lo mod 64)]
+  else
+    (hi / 64, hi mod 64, 0) :: translate_indices (hi - (hi mod 64 + 1)) lo
 
 (* For every index range, create a getter and setter *)
 let index_range_getter name field order start stop =
+  let indices = translate_indices start stop in
   let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
   let irg_val = Printf.sprintf "val _get_%s_%s : %s -> %s" name field name (bitvec size order) in
-  let irg_function = Printf.sprintf "function _get_%s_%s Mk_%s(v) = v[%i .. %i]" name field name start stop in
+  let body (chunk, start, stop) =
+    Printf.sprintf "v.%s_chunk_%i[%i .. %i]" name chunk start stop
+  in
+  let irg_function = Printf.sprintf "function _get_%s_%s v = %s" name field (Util.string_of_list " @ " body indices) in
   combine [ast_of_def_string order irg_val; ast_of_def_string order irg_function]
 
 let index_range_setter name field order start stop =
+  let indices = translate_indices start stop in
   let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
   let irs_val = Printf.sprintf "val _set_%s_%s : (register(%s), %s) -> unit effect {wreg}" name field name (bitvec size order) in
   (* Read-modify-write using an internal _reg_deref function without rreg effect *)
+  let body (chunk, hi, lo) =
+    Printf.sprintf "r.%s_chunk_%i = [ r.%s_chunk_%i with %i .. %i = v[%i .. %i]]"
+                   name chunk name chunk hi lo ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop)
+  in
   let irs_function = String.concat "\n"
     [ Printf.sprintf "function _set_%s_%s (r_ref, v) = {" name field;
-      Printf.sprintf "  r = _get_%s(_reg_deref(r_ref));" name;
-      Printf.sprintf "  r[%i .. %i] = v;" start stop;
-      Printf.sprintf "  (*r_ref) = Mk_%s(r)" name;
+                     "  r = _reg_deref(r_ref);";
+      Printf.sprintf "  %s;" (Util.string_of_list ";\n  " body indices);
+                     "  (*r_ref) = r";
                      "}"
     ]
   in
   combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function]
 
 let index_range_update name field order start stop =
+  let indices = translate_indices start stop in
   let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
   let iru_val = Printf.sprintf "val _update_%s_%s : (%s, %s) -> %s" name field name (bitvec size order) name in
   (* Read-modify-write using an internal _reg_deref function without rreg effect *)
+  let body (chunk, hi, lo) =
+    Printf.sprintf "let v = { v with %s_chunk_%i = [ v.%s_chunk_%i with %i .. %i = x[%i .. %i]] }"
+                   name chunk name chunk hi lo ((hi + chunk * 64) - stop) ((lo + chunk * 64) - stop)
+  in
   let iru_function = String.concat "\n"
-    [ Printf.sprintf "function _update_%s_%s (Mk_%s(v), x) = {" name field name;
-      Printf.sprintf "  Mk_%s([v with %i .. %i = x]);" name start stop;
-                     "}"
+    [ Printf.sprintf "function _update_%s_%s (v, x) =" name field;
+      Printf.sprintf "  %s in" (Util.string_of_list " in\n  " body indices);
+                     "  v"
     ]
   in
   let iru_overload = Printf.sprintf "overload update_%s = {_update_%s_%s}" field name field in
@@ -142,4 +148,5 @@ let field_accessor name order (id, ir) = index_range_accessor name (string_of_id
 
 let macro id size order ranges =
   let name = string_of_id id in
-  combine ([newtype name size order; full_accessor name size order] @ List.map (field_accessor name order) ranges)
+  let ranges = (mk_id "bits", BF_aux (BF_range (Big_int.of_int (size - 1), Big_int.of_int 0), Parse_ast.Unknown)) :: ranges in
+  combine ([newtype name size order] @ List.map (field_accessor name order) ranges)
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 06e92f3a..e088b5e5 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -990,6 +990,9 @@ let analyze_primop' ctx env l id args typ =
   | "and_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] ->
      AE_val (AV_C_fragment (F_op (v1, "&", v2), typ))
 
+  | "not_bits", [AV_C_fragment (v, _)] ->
+     AE_val (AV_C_fragment (F_unary ("~", v), typ))
+
   | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] ->
      let len = F_op (f, "-", F_op (t, "-", v_one)) in
      AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ))
@@ -1700,7 +1703,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
         be different. *)
      let pointer_assign ctyp1 ctyp2 =
        match ctyp1 with
-       | CT_ref ctyp1 -> ctyp_equal ctyp1 ctyp2
+       | CT_ref ctyp1 when ctyp_equal ctyp1 ctyp2 -> true
+       | CT_ref ctyp1 -> c_error ~loc:l "Incompatible type in pointer assignment"
        | _ -> false
      in
      let assign_ctyp = ctyp_of_typ ctx assign_typ in
@@ -2546,7 +2550,7 @@ let sgen_clexp = function
 let sgen_clexp_pure = function
   | CL_id id -> sgen_id id
   | CL_field (id, field) -> sgen_id id ^ "." ^ Util.zencode_string field
-  | CL_addr id -> sgen_id id
+  | CL_addr id -> "*" ^ sgen_id id
   | CL_addr_field (id, field) -> sgen_id id ^ "->" ^ Util.zencode_string field
   | CL_have_exception -> "have_exception"
   | CL_current_exception -> "current_exception"