More efficient bitfield implementation

5 files changed, 73 insertions, 44 deletions

diff --git a/aarch64/Makefile b/aarch64/Makefile
index 58281dc7..07bc67ae 100644
--- a/aarch64/Makefile
+++ b/aarch64/Makefile
@@ -8,7 +8,7 @@ aarch64.c: no_vector.sail
 	$(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c
 
 aarch64_c: aarch64.c
-	gcc -O2 $^ -o aarch64_c -lgmp -L $(SAIL_DIR)/lib
+	gcc -O2 $^ -o aarch64_c -lgmp -I $(SAIL_DIR)/lib
 
 aarch64: no_vector.sail
 	$(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
diff --git a/lib/sail.h b/lib/sail.h
index 99b57d8a..319db18d 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -740,6 +740,17 @@ void set_slice_int(mpz_t *rop,
   }
 }
 
+// This is a bit of a hack to let us optimize away the Align__1
+// function in aarch64.
+void arm_align(bv_t *rop, const bv_t x_bv, const mpz_t y_mpz) {
+  uint64_t x = mpz_get_ui(*x_bv.bits);
+  uint64_t y = mpz_get_ui(y_mpz);
+  uint64_t z = y * (x / y);
+  mp_bitcnt_t n = x_bv.len;
+  mpz_set_ui(*rop->bits, safe_rshift(UINT64_MAX, 64l - (n - 1)) & z);
+  rop->len = n;
+}
+
 void vector_update_subrange_bv_t(bv_t *rop,
 				 const bv_t op,
 				 const mpz_t n_mpz,
@@ -765,16 +776,20 @@ void vector_subrange_bv_t(bv_t *rop, const bv_t op, const mpz_t n_mpz, const mpz
   uint64_t n = mpz_get_ui(n_mpz);
   uint64_t m = mpz_get_ui(m_mpz);
 
-  mpz_set_ui(*rop->bits, 0ul);
   rop->len = n - (m - 1ul);
+  mpz_fdiv_q_2exp(*rop->bits, *op.bits, m);
+  normalise_bv_t(rop);
 
-  for (uint64_t i = 0; i < rop->len; i++) {
-    if (mpz_tstbit(*op.bits, i + m)) {
-      mpz_setbit(*rop->bits, i);
-    } else {
-      mpz_clrbit(*rop->bits, i);
-    }
-  }
+  /* mpz_set_ui(*rop->bits, 0ul); */
+  /* rop->len = n - (m - 1ul); */
+
+  /* for (uint64_t i = 0; i < rop->len; i++) { */
+  /*   if (mpz_tstbit(*op.bits, i + m)) { */
+  /*     mpz_setbit(*rop->bits, i); */
+  /*   } else { */
+  /*     mpz_clrbit(*rop->bits, i); */
+  /*   } */
+  /* } */
 }
 
 int bitvector_access(const bv_t op, const mpz_t n_mpz) {
diff --git a/mips/main.sail b/mips/main.sail
index 8b1e01d7..6f7d377e 100644
--- a/mips/main.sail
+++ b/mips/main.sail
@@ -16,7 +16,7 @@ function fetch_and_execute () = {
   /* the following skips are required on mips to fake the tag effects otherwise type checker complains  */
   skip_rmemt();
   skip_wmvt();
-  prerr_bits("PC: ", PC);
+  /* prerr_bits("PC: ", PC); */
   loop_again = true;
   try {
     let pc_pa = TranslatePC(PC);
@@ -62,9 +62,12 @@ function dump_mips_state () : unit -> unit = {
   }
 }
 
+val "load_raw" : (bits(64), string) -> unit
+
 val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}
 
 function main () = {
+  load_raw(0x0000000000100000, "/home/aa2019/mips_freebsd/kernel");
   init_registers(to_bits(64, elf_entry()));
   startTime = get_time_ns();
   while (fetch_and_execute()) do ();
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"