Added bitfield syntax to replicate register bits type

For example:

bitfield cr : vector(8, dec, bit) = {
  CR0 : 7 .. 4,
  LT : 7,
  CR1 : 3 .. 2,
  CR2 : 1,
  CR3 : 0,
}

The difference this creates a newtype wrapper around the vector type,
then generates getters and setters for all the fields once, rather
than having to handle this construct separately in every backend.

14 files changed, 196 insertions, 130 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 7e966bf2..e502f86f 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -726,6 +726,7 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
   | LEXP_vector_range (lexp, e1, e2) -> rewrap (E_vector_subrange (lexp_to_exp lexp, e1, e2))
   | LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id))
   | LEXP_memory (id, exps) -> rewrap (E_app (id, exps))
+  | LEXP_deref exp -> rewrap (E_app (mk_id "reg_deref", [exp]))
 
 let destruct_range (Typ_aux (typ_aux, _)) =
   match typ_aux with
diff --git a/src/bitfield.ml b/src/bitfield.ml
new file mode 100644
index 00000000..0a32654d
--- /dev/null
+++ b/src/bitfield.ml
@@ -0,0 +1,79 @@
+
+module Big_int = Nat_big_num
+
+open Initial_check
+open Ast
+open Ast_util
+
+let bitvec size order =
+  Printf.sprintf "vector(%i, %s, bit)" size (string_of_order order)
+
+let rec combine = function
+  | [] -> Defs []
+  | (Defs defs) :: ast ->
+     let (Defs defs') = combine ast in
+     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
+
+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";
+                     "}"
+    ]
+  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 full_accessor name size order =
+  combine [full_getter name size order; full_setter name size order; full_overload name order]
+
+let index_range_getter' name field order start stop =
+  let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+  let irg_val = Printf.sprintf "val _get_%s : %s -> %s" field name (bitvec size order) in
+  let irg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v[%i .. %i]" field name start stop 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 size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+  let irs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" field name (bitvec size order) in
+  let irs_function = String.concat "\n"
+    [ Printf.sprintf "function _set_%s (r_ref, v) = {" 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;
+                     "}"
+    ]
+  in
+  combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function]
+
+let index_range_overload field order =
+  ast_of_def_string order (Printf.sprintf "overload _mod_%s = {_get_%s, _set_%s}" field field field)
+
+let index_range_accessor name field order (BF_aux (bf_aux, l)) =
+  let getter n m = index_range_getter' name field order (Big_int.to_int n) (Big_int.to_int m) in
+  let setter n m = index_range_setter' name field order (Big_int.to_int n) (Big_int.to_int m) in
+  let overload = index_range_overload field order in
+  match bf_aux with
+  | BF_single n -> combine [getter n n; setter n n; overload]
+  | BF_range (n, m) -> combine [getter n m; setter n m; overload]
+  | BF_concat _ -> failwith "Unimplemented"
+
+let field_accessor name order (id, ir) = index_range_accessor name (string_of_id id) order ir
+
+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)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 0cea64a1..52ed1da1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -691,13 +691,12 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_de
     let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,())) in (* Add check that all enums have unique names *)
     let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
     td_enum, (names,k_env,def_ord)
-  | Parse_ast.TD_register(id,t1,t2,ranges) -> 
+  | Parse_ast.TD_bitfield(id,typ,ranges) ->
     let id = to_ast_id id in
     let key = id_to_string id in
-    let n1 = to_ast_nexp k_env t1 in
-    let n2 = to_ast_nexp k_env t2 in
-    let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in
-    TD_aux(TD_register(id,n1,n2,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
+    let typ = to_ast_typ k_env def_ord typ in
+    let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in
+    TD_aux(TD_bitfield(id,typ,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
 
 let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def) envs_out =
   match td with
@@ -1000,25 +999,34 @@ let undefined_typschm id typq =
     let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in
     mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef])))
 
+let have_undefined_builtins = ref false
+
 let generate_undefineds vs_ids (Defs defs) =
   let gen_vs id str =
     if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
   in
-  let undefined_builtins = List.concat
-    [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
-     gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
-     gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
-     gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
-     gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}";
-     gen_vs (mk_id "undefined_real") "unit -> real effect {undef}";
-     gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
-     gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
-     gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
-     (* FIXME: How to handle inc/dec order correctly? *)
-     gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type). (atom('n), 'a) -> vector('n, dec,'a) effect {undef}";
-     (* Only used with lem_mwords *)
-     gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
-     gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+  let undefined_builtins =
+    if !have_undefined_builtins then
+      []
+    else
+      begin
+        have_undefined_builtins := true;
+        List.concat
+          [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
+           gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
+           gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
+           gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
+           gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}";
+           gen_vs (mk_id "undefined_real") "unit -> real effect {undef}";
+           gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
+           gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
+           gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
+           (* FIXME: How to handle inc/dec order correctly? *)
+           gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type). (atom('n), 'a) -> vector('n, dec,'a) effect {undef}";
+           (* Only used with lem_mwords *)
+           gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+           gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+      end
   in
   let undefined_tu = function
     | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
@@ -1088,3 +1096,7 @@ let process_ast order defs =
       let ast = generate_undefineds vs_ids ast in
       generate_initialize_registers vs_ids ast
     end
+
+let ast_of_def_string order str =
+  let def = Parser2.def_eof Lexer2.token (Lexing.from_string str) in
+  process_ast order (Defs [def])
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 6059b0ac..9d1e0d30 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -54,6 +54,7 @@ open Ast_util
 val opt_undefined_gen : bool ref
 val opt_magic_hash : bool ref
 
+val ast_of_def_string : order -> string -> unit defs
 val process_ast : order -> Parse_ast.defs -> unit defs
 
 val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/lexer2.mll b/src/lexer2.mll
index e24de0d0..3a1f7066 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -155,6 +155,7 @@ let kw_table =
      ("while",                   (fun _ -> While));
      ("do",                      (fun _ -> Do));
      ("mutual",                  (fun _ -> Mutual));
+     ("bitfield",                (fun _ -> Bitfield));
 
      ("barr",                    (fun x -> Barr));
      ("depend",                  (fun x -> Depend));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index e84e8a60..362333f3 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -429,8 +429,7 @@ type_def_aux =  (* Type definition body *)
  | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
  | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
  | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
+ | TD_bitfield of id * atyp * (id * index_range) list (* register mutable bitfield type definition *)
 
 type 
 val_spec_aux =  (* Value type specification *)
diff --git a/src/parser.mly b/src/parser.mly
index 43dc0a74..d2a5933a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1247,8 +1247,6 @@ type_def:
     { tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
   | Typedef tid name_sect Eq Enumerate Lcurly enum_body Rcurly
     { tdloc (TD_enum($2,$3,$7,false)) }
-  | Typedef tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
-    { tdloc (TD_register($2, $7, $9, $12)) }
 
 default_typ:
   | Default atomic_kind tyvar
diff --git a/src/parser2.mly b/src/parser2.mly
index 521da6f8..7af70687 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -93,6 +93,7 @@ let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m
 let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m)
 let mk_nc nc n m = NC_aux (nc, loc n m)
 let mk_sd s n m = SD_aux (s, loc n m)
+let mk_ir r n m = BF_aux (r, loc n m)
 
 let mk_funcl f n m = FCL_aux (f, loc n m)
 let mk_fun fn n m = FD_aux (fn, loc n m)
@@ -154,7 +155,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Record Mutual Var Ref
 
@@ -185,8 +186,10 @@ let rec desugar_rchain chain s e =
 %start file
 %start typschm_eof
 %start exp_eof
+%start def_eof
 %type <Parse_ast.typschm> typschm_eof
 %type <Parse_ast.exp> exp_eof
+%type <Parse_ast.def> def_eof
 %type <Parse_ast.defs> file
 
 %%
@@ -1045,6 +1048,24 @@ funcls:
   | id funcl_patexp And funcls
     { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4 }
 
+index_range:
+  | Num
+    { mk_ir (BF_single $1) $startpos $endpos }
+  | Num DotDot Num
+    { mk_ir (BF_range ($1, $3)) $startpos $endpos }
+
+r_id_def:
+  | id Colon index_range
+    { $1, $3 }
+
+r_def_body:
+  | r_id_def
+    { [$1] }
+  | r_id_def Comma
+    { [$1] }
+  | r_id_def Comma r_def_body
+    { $1 :: $3 }
+
 type_def:
   | Typedef id typquant Eq typ
     { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
@@ -1066,6 +1087,8 @@ type_def:
     { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Union id typquant Eq Lcurly type_unions Rcurly
     { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+  | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly
+    { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos }
 
 enum_bar:
   | id
@@ -1197,6 +1220,10 @@ defs_list:
   | def defs_list
     { $1::$2 }
 
+def_eof:
+  | def Eof
+    { $1 }
+
 defs:
   | defs_list
     { (Defs $1) }
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 8f789c14..a79ae0eb 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1150,36 +1150,6 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
               fromInterpValuePP ^^ hardline ^^ hardline ^^
                 fromToInterpValuePP ^^ hardline
             else empty)
-  | TD_register(id,n1,n2,rs) ->
-    match n1, n2 with
-    | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
-       let dir_b = i1 < i2 in
-       let dir = (if dir_b then "true" else "false") in
-       let dir_suffix = (if dir_b then "_inc" else "_dec") in
-       let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
-       let size = if dir_b then Big_int.add (Big_int.sub i2 i1) (Big_int.of_int 1) else Big_int.add (Big_int.sub i1 i2) (Big_int.of_int 1) in
-       let vtyp = vector_typ (nconstant size) ord bit_typ in
-       let tannot = doc_tannot_lem sequential mwords false vtyp in
-       let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
-                                                       doc_range_lem r;]) in
-       let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
-       doc_op equals
-         (concat [string "type";space;doc_id_lem id])
-         (doc_typ_lem sequential mwords vtyp)
-       ^^ hardline ^^
-       doc_op equals
-         (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"])
-         (string "reg")
-       ^^ hardline ^^
-       doc_op equals
-         (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"])
-         (string "reg")
-       ^^ hardline ^^
-         doc_op equals
-           (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
-           (string "Register" ^^ space ^^
-              align (separate space [string "regname"; doc_int size; doc_int i1; string dir;
-                                     break 0 ^^ brackets (align doc_rids)]))
     | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
 
 let doc_rec_lem (Rec_aux(r,_)) = match r with
@@ -1354,7 +1324,8 @@ let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) =
   (* | VS_val_spec (_,_,Some _,_) -> empty *)
   | _ -> empty
 
-let find_regtypes defs =
+let find_regtypes defs = []
+                           (*
   List.fold_left
     (fun acc def ->
       match def with
@@ -1362,6 +1333,7 @@ let find_regtypes defs =
          (tname, (n1, n2, fields)) :: acc
       | _ -> acc
     ) [] defs
+                            *)
 
 let is_field_accessor regtypes fdef =
   let is_field_of regtyp field =
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 176fcd2e..d42cd2a5 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -526,11 +526,11 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
         let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
         fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
           kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
-      | TD_register(id,n1,n2,rs) ->
-        let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
+      | TD_bitfield(id,typ,rs) ->
+        let pp_rid ppf (id, r) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
         let pp_rids = (list_pp pp_rid pp_rid) in
-        fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
-          kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
+        fprintf ppf "@[<0>(%a %a %a [%a])@]"
+          kwd "TD_bitfield" pp_lem_id id pp_lem_typ typ pp_rids rs
   in
   fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot
 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 30eb71e0..38b9e134 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -432,16 +432,6 @@ let doc_typdef (TD_aux(td,_)) = match td with
       doc_op equals
         (concat [string "typedef"; space; doc_id id; doc_namescm nm])
         (string "enumerate" ^^ space ^^ braces enums_doc)
-  | TD_register(id,n1,n2,rs) ->
-      let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in
-      let doc_rids = group (separate_map (break 1) doc_rid rs) in
-      doc_op equals
-        (string "typedef" ^^ space ^^ doc_id id)
-        (separate space [
-          string "register bits";
-          brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2);
-          braces doc_rids;
-        ])
 
 let doc_kindef (KD_aux(kd,_)) = match kd with
   | KD_nabbrev(kind,id,nm,n) ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 9b97b88b..2ecaf91d 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1527,46 +1527,8 @@ let rewrite_register_ref_writes (Defs defs) =
     | None -> E_assign (lexp, exp) in
   let rewrite_exp _ = fold_exp { id_exp_alg with e_assign = e_assign } in
 
-  let generate_field_accessors l env id n1 n2 fields =
-    let i1, i2 = match n1, n2 with
-      | Nexp_aux(Nexp_constant i1, _),Nexp_aux(Nexp_constant i2, _) -> i1, i2
-      | _ -> raise (Reporting_basic.err_typ l
-         ("Non-constant indices in register type " ^ string_of_id id)) in
-    let dir_b = i1 < i2 in
-    let dir = (if dir_b then "true" else "false") in
-    let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
-    let size = if dir_b then Big_int.succ (Big_int.sub i2 i1) else Big_int.succ (Big_int.sub i1 i2) in
-    let rtyp = mk_id_typ id in
-    let vtyp = vector_typ (nconstant size) ord bit_typ in
-    let accessors (fr, fid) =
-      let i, j = match fr with
-        | BF_aux (BF_single i, _) -> (i, i)
-        | BF_aux (BF_range (i, j), _) -> (i, j)
-        | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in
-      let mk_num_exp i = mk_lit_exp (L_num i) in
-      let reg_pat, reg_env = bind_pat env (mk_pat (P_typ (rtyp, mk_pat (P_id (mk_id "reg"))))) rtyp in
-      let inferred_get = infer_exp reg_env (mk_exp (E_vector_subrange
-        (mk_exp (E_id (mk_id "reg")), mk_num_exp i, mk_num_exp j))) in
-      let ftyp = typ_of inferred_get in
-      let v_pat, v_env = bind_pat reg_env (mk_pat (P_typ (ftyp, mk_pat (P_id (mk_id "v"))))) ftyp in
-      let inferred_set = infer_exp v_env (mk_exp (E_vector_update_subrange
-        (mk_exp (E_id (mk_id "reg")), mk_num_exp i, mk_num_exp j, mk_exp (E_id (mk_id "v"))))) in
-      let set_args = P_aux (P_tup [reg_pat; v_pat], (l, Some (env, tuple_typ [rtyp; ftyp], no_effect))) in
-      let fsuffix = "_" ^ string_of_id id ^ "_" ^ string_of_id fid in
-      let rec_opt = Rec_aux (Rec_nonrec, l) in
-      let tannot ret_typ = Typ_annot_opt_aux (Typ_annot_opt_some (TypQ_aux (TypQ_tq [], l), ret_typ), l) in
-      let eff_opt = Effect_opt_aux (Effect_opt_pure, l) in
-      let mk_funcl id pat exp = FCL_aux (FCL_Funcl (mk_id id, Pat_aux (Pat_exp (pat, exp),(l,None))), (l, None)) in
-      let mk_fundef id pat exp ret_typ = DEF_fundef (FD_aux (FD_function (rec_opt, tannot ret_typ, eff_opt, [mk_funcl id pat exp]), (l, None))) in
-      [mk_fundef ("get" ^ fsuffix) reg_pat inferred_get ftyp;
-      mk_fundef ("set" ^ fsuffix) set_args inferred_set (typ_of inferred_set)] in
-    List.concat (List.map accessors fields) in
-
   let rewriters = { rewriters_base with rewrite_exp = rewrite_exp } in
   let rec rewrite ds = match ds with
-    | (DEF_type (TD_aux (TD_register (id, n1, n2, fields), (l, Some (env, _, _)))) as d) :: ds ->
-       let (Defs d), env = check env (Defs [d]) in
-       d @ (generate_field_accessors l env id n1 n2 fields) @ rewrite ds
     | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds)
     | [] -> [] in
   Defs (rewrite (write_reg_spec @ defs))
@@ -1883,7 +1845,7 @@ let rewrite_type_def_typs rw_typ rw_typquant rw_typschm (TD_aux (td, annot)) =
   | TD_variant (id, nso, typq, tus, flag) ->
      TD_aux (TD_variant (id, nso, rw_typquant typq, List.map (rewrite_type_union_typs rw_typ) tus, flag), annot)
   | TD_enum (id, nso, ids, flag) -> TD_aux (TD_enum (id, nso, ids, flag), annot)
-  | TD_register (id, n1, n2, ranges) -> TD_aux (TD_register (id, n1, n2, ranges), annot)
+  | TD_bitfield _ -> assert false (* Processed before re-writing *)
 
 (* FIXME: other reg_dec types *)
 let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) =
@@ -2146,8 +2108,8 @@ let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list
   match l with
   | [] -> k []
   | exp :: exps -> f exp (fun exp -> mapCont f exps (fun exps -> k (exp :: exps)))
-                
-let rewrite_defs_letbind_effects  =  
+
+let rewrite_defs_letbind_effects  =
 
   let rec value ((E_aux (exp_aux,_)) as exp) =
     not (effectful exp || updates_vars exp)
@@ -2169,7 +2131,7 @@ let rewrite_defs_letbind_effects  =
 
   and n_fexp (fexp : 'a fexp) (k : 'a fexp -> 'a exp) : 'a exp =
     let (FE_aux (FE_Fexp (id,exp),annot)) = fexp in
-    n_exp_name exp (fun exp -> 
+    n_exp_name exp (fun exp ->
     k (fix_eff_fexp (FE_aux (FE_Fexp (id,exp),annot))))
 
   and n_fexpL (fexps : 'a fexp list) (k : 'a fexp list -> 'a exp) : 'a exp =
@@ -2209,6 +2171,9 @@ let rewrite_defs_letbind_effects  =
     let (LEXP_aux (lexp_aux,annot)) = lexp in
     match lexp_aux with
     | LEXP_id _ -> k lexp
+    | LEXP_deref exp ->
+       n_exp exp (fun exp ->
+       k (fix_eff_lexp (LEXP_aux (LEXP_deref exp, annot))))
     | LEXP_memory (id,es) ->
        n_exp_nameL es (fun es -> 
        k (fix_eff_lexp (LEXP_aux (LEXP_memory (id,es),annot))))
@@ -2254,6 +2219,7 @@ let rewrite_defs_letbind_effects  =
     | E_block es -> failwith "E_block should have been removed till now"
     | E_nondet _ -> failwith "E_nondet not supported"
     | E_id id -> k exp
+    | E_ref id -> k exp
     | E_lit _ -> k exp
     | E_cast (typ,exp') ->
        n_exp_name exp' (fun exp' ->
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index b9affe12..3d3b13e3 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -432,8 +432,8 @@ let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
     typ_variants consider_var bindings tunions
   | TD_enum(id,_,ids,_) ->
     Nameset.of_list (List.map string_of_id (id::ids)),mt
-  | TD_register(id,n1,n2,_) ->
-    init_env (string_of_id id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2
+  | TD_bitfield(id,typ,_) ->
+    init_env (string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *)
 
 let fv_of_tannot_opt consider_var (Typ_annot_opt_aux (t,_)) =
   match t with
diff --git a/src/type_check.ml b/src/type_check.ml
index 0c1d55ce..3269de1d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3453,32 +3453,50 @@ let mk_synonym typq typ =
                                       ^ " in type synonym " ^ string_of_typ typ
                                       ^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
 
-let check_typedef env (TD_aux (tdef, (l, _))) =
+let check_kinddef env (KD_aux (kdef, (l, _))) =
+  let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
+  match kdef with
+  | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_nat, _)]),_) as kind), id, nmscm, nexp) ->
+     [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
+     Env.add_num_def id nexp env
+  | _ -> kd_err ()
+
+let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
+  fun env (TD_aux (tdef, (l, _))) ->
   let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Typedef") in
   match tdef with
-  | TD_abbrev(id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) ->
+  | TD_abbrev (id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ) env
-  | TD_record(id, nmscm, typq, fields, _) ->
+  | TD_record (id, nmscm, typq, fields, _) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env
-  | TD_variant(id, nmscm, typq, arms, _) ->
+  | TD_variant (id, nmscm, typq, arms, _) ->
      let env =
        env
        |> Env.add_variant id (typq, arms)
        |> (fun env -> List.fold_left (fun env tu -> check_type_union env id typq tu) env arms)
      in
      [DEF_type (TD_aux (tdef, (l, None)))], env
-  | TD_enum(id, nmscm, ids, _) ->
+  | TD_enum (id, nmscm, ids, _) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_enum id ids env
+  | TD_bitfield (id, typ, ranges) ->
+     let typ = Env.expand_synonyms env typ in
+     begin
+       match typ with
+       (* The type of a bitfield must be a constant-width bitvector *)
+       | Typ_aux (Typ_app (v, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant size, _)), _);
+                               Typ_arg_aux (Typ_arg_order order, _);
+                               Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id b, _)), _)]), _)
+            when string_of_id v = "vector" && string_of_id b = "bit" ->
+          let size = Big_int.to_int size in
+          let (Defs defs), env = check' env (Bitfield.macro id size order ranges) in
+          defs, env
+       | _ ->
+          typ_error l "Bad bitfield type"
+     end
+  | _ -> td_err ()
 
-let check_kinddef env (KD_aux (kdef, (l, _))) =
-  let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
-  match kdef with
-  | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_nat, _)]),_) as kind), id, nmscm, nexp) ->
-     [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
-     Env.add_num_def id nexp env
-  | _ -> kd_err ()
-
-let rec check_def env def =
+and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
+  fun env def ->
   let cd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Case") in
   match def with
   | DEF_kind kdef -> check_kinddef env kdef
@@ -3507,7 +3525,8 @@ let rec check_def env def =
      let defs, env = check_def env def
      in List.map (fun def -> DEF_comm (DC_comm_struct def)) defs, env
 
-let rec check' env (Defs defs) =
+and check' : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+  fun env (Defs defs) ->
   match defs with
   | [] -> (Defs []), env
   | def :: defs ->
@@ -3515,7 +3534,8 @@ let rec check' env (Defs defs) =
      let (Defs defs, env) = check' env (Defs defs) in
      (Defs (def @ defs)), env
 
-let check env defs =
+let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+  fun env defs ->
   try check' env defs with
   | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))