Add configuration registers so __SetConfig ASL can be translated

Registers can now be marked as configuration registers, for example:

register configuration CFG_RVBAR = 0x1300000

They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:

Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ

For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.

Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.

15 files changed, 81 insertions, 55 deletions

diff --git a/src/anf.ml b/src/anf.ml
index 4c2405b3..d51d29a3 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -307,7 +307,7 @@ let rec map_functions f (AE_aux (aexp, env, l)) =
 
 let pp_lvar lvar doc =
   match lvar with
-  | Register typ ->
+  | Register (_, _, typ) ->
      string "[R/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
   | Local (Mutable, typ) ->
      string "[M/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
diff --git a/src/ast_util.ml b/src/ast_util.ml
index c57cd21f..28b27e93 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -54,7 +54,7 @@ module Big_int = Nat_big_num
 
 type mut = Immutable | Mutable
 
-type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound
+type lvar = Register of effect * effect * typ | Enum of typ | Local of mut * typ | Unbound
 
 let no_annot = (Parse_ast.Unknown, ())
 
@@ -562,6 +562,7 @@ let string_of_base_effect_aux = function
   | BE_unspec -> "unspec"
   | BE_nondet -> "nondet"
   | BE_escape -> "escape"
+  | BE_config -> "configuration"
   (*| BE_lset -> "lset"
   | BE_lret -> "lret"*)
 
diff --git a/src/ast_util.mli b/src/ast_util.mli
index d23d56da..57e1a7cc 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -58,7 +58,7 @@ type mut = Immutable | Mutable
 (** [lvar] is the type of variables - they can either be registers,
    local mutable or immutable variables, nullary union constructors
    (i.e. None in option), or unbound identifiers *)
-type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound
+type lvar = Register of effect * effect * typ | Enum of typ | Local of mut * typ | Unbound
 
 val no_annot : unit annot
 val gen_loc : Parse_ast.l -> Parse_ast.l
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 9f23412e..2e6e1e29 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -287,8 +287,9 @@ let pp_cdef = function
      pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space
      ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
      ^^ hardline
-  | CDEF_reg_dec (id, ctyp) ->
-     pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+  | CDEF_reg_dec (id, ctyp, instrs) ->
+     pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ space
+     ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
      ^^ hardline
   | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline
   | CDEF_let (n, bindings, instrs) ->
diff --git a/src/c_backend.ml b/src/c_backend.ml
index f630e91a..3b57c9ed 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -57,7 +57,7 @@ open PPrint
 open Value2
 
 open Anf
-   
+
 module Big_int = Nat_big_num
 
 let c_verbosity = ref 1
@@ -303,7 +303,7 @@ let rec c_aval ctx = function
        match lvar with
        | Local (_, typ) when is_stack_typ ctx typ ->
           AV_C_fragment (F_id id, typ)
-       | Register typ when is_stack_typ ctx typ ->
+       | Register (_, _, typ) when is_stack_typ ctx typ ->
           AV_C_fragment (F_id id, typ)
        | _ -> v
      end
@@ -484,12 +484,12 @@ let rec instr_ctyps (I_aux (instr, aux)) =
   | 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
+  | CDEF_reg_dec (id, ctyp, instrs) :: ast -> (id, ctyp, instrs) :: c_ast_registers ast
   | _ :: ast -> c_ast_registers ast
   | [] -> []
 
 let cdef_ctyps ctx = function
-  | CDEF_reg_dec (_, ctyp) -> [ctyp]
+  | CDEF_reg_dec (_, ctyp, instrs) -> ctyp :: List.concat (List.map instr_ctyps instrs)
   | CDEF_spec (_, ctyps, ctyp) -> ctyp :: ctyps
   | CDEF_fundef (id, _, _, instrs) ->
      let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
@@ -1482,8 +1482,12 @@ let letdef_count = ref 0
 (** Compile a Sail toplevel definition into an IR definition **)
 let rec compile_def ctx = function
   | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) ->
-     [CDEF_reg_dec (id, ctyp_of_typ ctx typ)], ctx
-  | DEF_reg_dec _ -> failwith "Unsupported register declaration" (* FIXME *)
+     [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx
+  | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
+     let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in
+     let setup, ctyp, call, cleanup = compile_aexp ctx aexp in
+     let instrs = setup @ [call (CL_id id)] @ cleanup in
+     [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx
 
   | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) ->
      c_debug (lazy "Compiling VS");
@@ -2485,7 +2489,7 @@ let codegen_alloc = function
   | _ -> assert false
 
 let codegen_def' ctx = function
-  | CDEF_reg_dec (id, ctyp) ->
+  | CDEF_reg_dec (id, ctyp, _) ->
      string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline
      ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))
 
@@ -2605,6 +2609,9 @@ let sgen_startup = function
      Printf.sprintf "  startup_%s();" (sgen_id id)
   | _ -> assert false
 
+let sgen_instr id ctx instr =
+  Pretty_print_sail.to_string (codegen_instr id ctx instr)
+
 let is_cdef_finish = function
   | CDEF_startup _ -> true
   | _ -> false
@@ -2729,11 +2736,12 @@ let compile_ast ctx (Defs defs) =
 
     let regs = c_ast_registers cdefs in
 
-    let register_init_clear (id, ctyp) =
+    let register_init_clear (id, ctyp, instrs) =
       if is_stack_ctyp ctyp then
-        [], []
+        List.map (sgen_instr (mk_id "reg") ctx) instrs, []
       else
-        [ Printf.sprintf "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ],
+        [ Printf.sprintf "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ]
+        @ List.map (sgen_instr (mk_id "reg") ctx) instrs,
         [ Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ]
     in
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index a774352d..af3d5fd5 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -319,7 +319,8 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
                                | Parse_ast.BE_undef  -> BE_undef
                                | Parse_ast.BE_unspec -> BE_unspec
                                | Parse_ast.BE_nondet -> BE_nondet
-                               | Parse_ast.BE_escape -> BE_escape),l))
+                               | Parse_ast.BE_escape -> BE_escape
+                               | Parse_ast.BE_config -> BE_config),l))
                              effects)
                | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None
     ), l)
@@ -857,7 +858,9 @@ let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
   DEC_aux(
     (match regdec with
       | Parse_ast.DEC_reg(typ,id) ->
-	DEC_reg(to_ast_typ k_env def_ord typ,to_ast_id id)
+        DEC_reg(to_ast_typ k_env def_ord typ,to_ast_id id)
+      | Parse_ast.DEC_config(id,typ,exp) ->
+        DEC_config(to_ast_id id,to_ast_typ k_env def_ord typ,to_ast_exp k_env def_ord exp)
       | Parse_ast.DEC_alias(id,e) ->
 	DEC_alias(to_ast_id id,to_ast_alias_spec k_env def_ord e)
       | Parse_ast.DEC_typ_alias(typ,id,e) ->
diff --git a/src/lexer.mll b/src/lexer.mll
index 621a1a44..16574ef1 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -179,6 +179,7 @@ let kw_table =
      ("unspec",                  (fun x -> Unspec));
      ("nondet",                  (fun x -> Nondet));
      ("escape",                  (fun x -> Escape));
+     ("configuration",           (fun _ -> Configuration));
    ]
 
 
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 6de40977..369a325c 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -322,7 +322,7 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
        | Local (Immutable, _) | Unbound -> zencode ctx id
        | Enum _ -> zencode_upper ctx id
        | Register _ when is_passed_by_name (typ_of exp) -> zencode ctx id
-       | Register typ ->
+       | Register (_, _, typ) ->
           if !opt_trace_ocaml then
             let var = gensym () in
             let str_typ = parens (ocaml_string_typ (Rewrites.simple_typ typ) var) in
@@ -339,7 +339,7 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp =
   | LEXP_cast (_, id) | LEXP_id id ->
      begin
        match Env.lookup_id id (env_of exp) with
-       | Register typ ->
+       | Register (_, _, typ) ->
           let var = gensym () in
           let traced_exp =
             if !opt_trace_ocaml then
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 2848edc0..26cb9df7 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -98,7 +98,7 @@ base_effect_aux =  (* effect *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
  | BE_escape
-
+ | BE_config
 
 type 
 kid_aux =  (* identifiers with kind, ticked to differntiate from program variables *)
@@ -496,6 +496,7 @@ kind_def_aux =  (* Definition body for elements of kind; many are shorthands for
 type 
 dec_spec_aux =  (* Register declarations *)
    DEC_reg of atyp * id
+ | DEC_config of id * atyp * exp
  | DEC_alias of id * exp
  | DEC_typ_alias of atyp * id * exp
 
diff --git a/src/parser.mly b/src/parser.mly
index 60ccc81f..0637d61a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -178,7 +178,7 @@ let rec desugar_rchain chain s e =
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %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 Mutual Var Ref
+%token Repeat Until While Do Mutual Var Ref Configuration
 
 %nonassoc Then
 %nonassoc Else
@@ -634,6 +634,8 @@ effect:
     { mk_effect BE_nondet $startpos $endpos }
   | Escape
     { mk_effect BE_escape $startpos $endpos }
+  | Configuration
+    { mk_effect BE_config $startpos $endpos }
 
 effect_list:
   | effect
@@ -1331,6 +1333,8 @@ val_spec_def:
 register_def:
   | Register id Colon typ
     { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
+  | Register Configuration id Colon typ Eq exp
+    { mk_reg_dec (DEC_config ($3, $5, $7)) $startpos $endpos }
 
 default_def:
   | Default base_kind Inc
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 4b9fa6a9..d59bd132 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -487,6 +487,7 @@ let doc_mapdef (MD_aux (MD_mapping (id, typa, mapcls), _)) =
 let doc_dec (DEC_aux (reg,_)) =
   match reg with
   | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ]
+  | DEC_config (id, typ, exp) -> separate space [string "register configuration"; doc_id id; colon; doc_typ typ; equals; doc_exp exp]
   | DEC_alias(id,alspec) -> string "ALIAS"
   | DEC_typ_alias(typ,id,alspec) -> string "ALIAS"
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 6212e0da..b67f9c49 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -396,13 +396,15 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls
   in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
 
 let rewrite_def rewriters d = match d with
+  | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) ->
+     DEF_reg_dec (DEC_aux (DEC_config (id, typ, rewriters.rewrite_exp rewriters exp), annot))
   | DEF_type _ | DEF_mapdef _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d
   | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
   | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
   | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
 
-let rewrite_defs_base rewriters (Defs defs) = 
+let rewrite_defs_base rewriters (Defs defs) =
   let rec rewrite ds = match ds with
     | [] -> []
     | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 7bb82719..04668989 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -445,6 +445,8 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd
 let fv_of_rd consider_var (DEC_aux (d,_)) = match d with
   | DEC_reg(t,id) ->
     init_env (string_of_id id), fv_of_typ consider_var mt mt t
+  | DEC_config(id,t,exp) ->
+    init_env (string_of_id id), fv_of_typ consider_var mt mt t
   | DEC_alias(id,alias) ->
     init_env (string_of_id id),mt
   | DEC_typ_alias(t,id,alias) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index fec146a0..0a29b6d6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -82,10 +82,9 @@ let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ Lazy.
 
 let lvar_typ = function
   | Local (_, typ) -> typ
-  | Register typ -> typ
+  | Register (_, _, typ) -> typ
   | Enum typ -> typ
-  | _ -> assert false
-                
+
 type type_error =
   (* First parameter is the error that caused us to start doing type
      coercions, the second is the errors encountered by all possible
@@ -384,8 +383,8 @@ module Env : sig
   val get_flow : id -> t -> typ -> typ
   val remove_flow : id -> t -> t
   val is_register : id -> t -> bool
-  val get_register : id -> t -> typ
-  val add_register : id -> typ -> t -> t
+  val get_register : id -> t -> effect * effect * typ
+  val add_register : id -> effect -> effect -> typ -> t -> t
   val is_mutable : id -> t -> bool
   val get_constraints : t -> n_constraint list
   val add_constraint : n_constraint -> t -> t
@@ -450,7 +449,7 @@ end = struct
       defined_val_specs : IdSet.t;
       locals : (mut * typ) Bindings.t;
       union_ids : (typquant * typ) Bindings.t;
-      registers : typ Bindings.t;
+      registers : (effect * effect * typ) Bindings.t;
       variants : (typquant * type_union list) Bindings.t;
       mappings : (typquant * typ * typ) Bindings.t;
       typ_vars : (Ast.l * base_kind_aux) KBindings.t;
@@ -1048,14 +1047,14 @@ end = struct
 
   let get_casts env = env.casts
 
-  let add_register id typ env =
+  let add_register id reff weff typ env =
     wf_typ env typ;
     if Bindings.mem id env.registers
     then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
     else
       begin
         typ_print (lazy ("Adding register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ));
-        { env with registers = Bindings.add id typ env.registers }
+        { env with registers = Bindings.add id (reff, weff, typ) env.registers }
       end
 
   let get_locals env = env.locals
@@ -1067,17 +1066,16 @@ end = struct
       Local (mut, if raw then typ else flow typ)
     with
     | Not_found ->
-       begin
-         try Register (Bindings.find id env.registers) with
-         | Not_found ->
-            begin
-              try
-                let (enum, _) = List.find (fun (enum, ctors) -> IdSet.mem id ctors) (Bindings.bindings env.enums) in
-                Enum (mk_typ (Typ_id enum))
-              with
-              | Not_found -> Unbound
-            end
-       end
+    try
+      let reff, weff, typ = Bindings.find id env.registers in
+      Register (reff, weff, typ)
+    with
+    | Not_found ->
+    try
+      let (enum, _) = List.find (fun (enum, ctors) -> IdSet.mem id ctors) (Bindings.bindings env.enums) in
+      Enum (mk_typ (Typ_id enum))
+    with
+    | Not_found -> Unbound
 
   let add_typ_var l kid k env =
     if KBindings.mem kid env.typ_vars
@@ -2926,7 +2924,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
        let infer_flexp = function
          | LEXP_id v ->
             begin match Env.lookup_id v env with
-            | Register typ -> typ, LEXP_id v, true
+            | Register (_, _, typ) -> typ, LEXP_id v, true
             | Local (Mutable, typ) -> typ, LEXP_id v, false
             | _ -> typ_error l "l-expression field is not a register or a local mutable type"
             end
@@ -2938,7 +2936,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
                 | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
                 | Local (Immutable, vtyp) -> true, vtyp, false
                 | Local (Mutable, vtyp) -> false, vtyp, false
-                | Register vtyp -> false, vtyp, true
+                | Register (_, _, vtyp) -> false, vtyp, true
               in
               let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
               let inferred_exp = match access with
@@ -2969,7 +2967,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
      annot_assign tlexp checked_exp, env'
   | LEXP_id v when has_typ v env ->
      begin match Env.lookup_id ~raw:true v env with
-     | Local (Mutable, vtyp) | Register vtyp ->
+     | Local (Mutable, vtyp) | Register (_, _, vtyp) ->
         let checked_exp = crule check_exp env exp vtyp in
         let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
         annot_assign tlexp checked_exp, env'
@@ -2993,10 +2991,10 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
           subtyp l env typ typ_annot;
           subtyp l env typ_annot vtyp;
           annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
-       | Register vtyp ->
+       | Register (_, weff, vtyp) ->
           subtyp l env typ typ_annot;
           subtyp l env typ_annot vtyp;
-          annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env
+          annot_lexp_effect (LEXP_cast (typ_annot, v)) typ weff, env
        | Unbound ->
           subtyp l env typ typ_annot;
           annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
@@ -3016,7 +3014,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
      | Local (Immutable, _) | Enum _ ->
         typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
      | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env
-     | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env
+     | Register (_, weff, vtyp) -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ weff, env
      | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
      end
   | LEXP_tup lexps ->
@@ -3048,7 +3046,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
      begin match Env.lookup_id v env with
      | Local (Mutable, typ) -> annot_lexp (LEXP_id v) typ
      (* Probably need to remove flows here *)
-     | Register typ -> annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg])
+     | Register (_, weff, typ) -> annot_lexp_effect (LEXP_id v) typ weff
      | Local (Immutable, _) | Enum _ ->
         typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
      | Unbound ->
@@ -3115,13 +3113,13 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
      end
   | LEXP_field (LEXP_aux (LEXP_id v, _), fid) ->
      (* FIXME: will only work for ASL *)
-     let rec_id =
+     let rec_id, weff =
        match Env.lookup_id v env with
-       | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id
+       | Register (_, weff, Typ_aux (Typ_id rec_id, _)) -> rec_id, weff
        | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
      in
      let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in
-     annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg])
+     annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ weff
   | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp)
 
 and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
@@ -3134,7 +3132,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      begin
        match Env.lookup_id v env with
        | Local (_, typ) | Enum typ -> annot_exp (E_id v) typ
-       | Register typ -> annot_exp_effect (E_id v) typ (mk_effect [BE_rreg])
+       | Register (reff, _, typ) -> annot_exp_effect (E_id v) typ reff
        | Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
      end
   | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
@@ -3306,7 +3304,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      let (_, typ) = Bindings.find id (Env.get_locals env) in
      annot_exp (E_ref id) (ref_typ typ)
   | E_ref id when Env.is_register id env ->
-     let typ = Env.get_register id env in
+     let _, _, typ = Env.get_register id env in
      annot_exp (E_ref id) (register_typ typ)
   | _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp)
 
@@ -4460,8 +4458,12 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_default default -> check_default env default
   | DEF_overload (id, ids) -> [DEF_overload (id, ids)], Env.add_overloads id ids env
   | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, _))) ->
-     let env = Env.add_register id typ env in
+     let env = Env.add_register id (mk_effect [BE_rreg]) (mk_effect [BE_wreg]) typ env in
      [DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, Some (env, typ, no_effect))))], env
+  | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), (l, _))) ->
+     let checked_exp = crule check_exp env (strip_exp exp) typ in
+     let env = Env.add_register id no_effect (mk_effect [BE_config]) typ env in
+     [DEF_reg_dec (DEC_aux (DEC_config (id, typ, checked_exp), (l, Some (env, typ, no_effect))))], env
   | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
   | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
   | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
diff --git a/src/type_check.mli b/src/type_check.mli
index 62fd846e..4f87e4e6 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -106,7 +106,7 @@ module Env : sig
 
   val update_val_spec : id -> typquant * typ -> t -> t
 
-  val get_register : id -> t -> typ
+  val get_register : id -> t -> effect * effect * typ
 
   (** Return all the identifiers in an enumeration. Throws a type
      error if the enumeration doesn't exist. *)