Increase support for register "field" accesses; there is now a bug in how run_interp handles SubReg register forms.

3 files changed, 56 insertions, 19 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index ad22aa36..6bc4964d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -118,6 +118,18 @@ type outcome =
 (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value or a memory request *)
 val interp : defs tannot -> exp tannot -> outcome
 
+val to_register_fields : defs tannot -> list (id * list (id * index_range))
+let rec to_register_fields (Defs defs) = 
+  match defs with
+  | [ ] -> [ ]
+  | (DEF_aux def (l,tannot))::defs -> 
+    match def with 
+    | DEF_type (TD_aux (TD_register id n1 n2 indexes) l') ->
+      (id,List.map (fun (a,b) -> (b,a)) indexes)::(to_register_fields (Defs defs))
+    | _ -> to_register_fields (Defs defs)
+    end 
+  end
+
 val to_registers : defs tannot -> env
 let rec to_registers (Defs defs) = 
   match defs with
@@ -166,7 +178,7 @@ let rec to_data_constructors (Defs defs) =
     | _ -> to_data_constructors (Defs defs) end
    end
 
-val in_env : env -> id -> maybe value
+val in_env :forall 'a. (list (id * 'a)) -> id -> maybe 'a
 let rec in_env env id =
  match env with
  | [] -> Nothing
@@ -574,8 +586,8 @@ let rec find_case pexps value =
   end
 
 (*top_level is a tuple of 
-  (all definitions, letbound and enum values, register values, and Typedef union constructors) *)
-type top_level = Env of (defs tannot) * env * env * list (id * typ)
+  (all definitions, letbound and enum values, register values, Typedef union constructors, and sub register mappings) *)
+type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range))
 
 val interp_main : top_level -> env -> mem -> (exp tannot) -> (outcome * mem * env)
 val exp_list : top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> mem -> list value -> list (exp tannot) -> (outcome * mem * env)
@@ -607,7 +619,7 @@ let rec exp_list t_level build_e build_v l_env l_mem vals exps =
   end
 
 and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env defs lets regs ctors) = t_level in 
+  let (Env defs lets regs ctors subregs) = t_level in 
   let (typ,tag,ncs,effect) = match annot with 
     | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown),
 		  Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
@@ -770,7 +782,19 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
                                             | Nothing -> (Error l "Field not found in record",lm,le) end
                         | _ -> (Error l "Field access of vectors not implemented",lm,le)
                         end )
-                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot))))
+                      (fun a -> 
+			match (exp,a) with
+			  | (E_aux _ (l,Just(_,Tag_extern _,_,_)),
+			     (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_))) as regf) Nothing) s)) ->
+			    match in_env subregs id' with
+			      | Just(indexes) ->
+				match in_env indexes id with
+				  | Just ir -> 
+				    (Action (Read_reg (SubReg id regf ir) Nothing) s)
+				  | _ -> Error l "Internal error, unrecognized read, no id"
+		                end 
+                              | Nothing -> Error l "Internal error, unrecognized read, no reg" end
+                          | _ -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot))) end)
     | E_vector_access vec i ->
       (*Need to update to read one position of a register*)
       resolve_outcome (interp_main t_level l_env l_mem i)
@@ -1012,7 +1036,7 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
     end
 
 and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
-   let (Env defs lets regs ctors) = t_level in
+   let (Env defs lets regs ctors subregs) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown), Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1177,7 +1201,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
        | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem lm n value, l_env),Nothing)
        | (Just (V_boxref n t),false) -> 
 	 ((Value (in_mem lm n) Tag_empty,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
-       | (Just v, true) -> ((Error l "Field access requires record",lm,le),Nothing)
+       | (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing)
        | (Just v,false) -> ((Value v Tag_empty,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
        | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end
      | ((Action a s,lm,le), Just lexp_builder) ->  
@@ -1185,7 +1209,17 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
        | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
        | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
        | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
-       | _ -> ((Error l "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing)
+       | Write_reg ((Reg id' t') as regf) Nothing value -> 
+	 match in_env subregs id' with
+	   | Just(indexes) ->
+	     match in_env indexes id with
+	       | Just ir -> 
+		 ((Action (Write_reg (SubReg id regf ir) Nothing value) s,lm,le), 
+		  (if is_top_level then Nothing else Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))))
+	       | _ -> ((Error l "Internal error, unrecognized write",lm,le),Nothing)
+		 end 
+            | Nothing -> ((Error l "Internal error, unrecognized write",lm,le),Nothing) end
+       | _ -> ((Error l "Internal error, unrecognized write",lm,le),Nothing)
        end 
      | e -> e end)
      end	
@@ -1212,14 +1246,14 @@ end
 
 (*Beef up to pick up enums as well*)
 let rec to_global_letbinds (Defs defs) t_level =
-  let  (Env defs' lets regs ctors) = t_level in
+  let  (Env defs' lets regs ctors subregs) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, emem, []),t_level)
   | (DEF_aux def (l,_))::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind t_level [] emem lbind with
-      | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors)
+      | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs)
       | ((Action a s,lm,le),_) -> 
 	((Error l "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
       | (e,_) -> (e,t_level) end
@@ -1229,7 +1263,7 @@ let rec to_global_letbinds (Defs defs) t_level =
 
 
 let interp defs exp =
-  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) in 
+  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) in 
   let (o,t_level) = to_global_letbinds defs t_level in
   match o with
   | (Value _ _,_,_) -> 
@@ -1254,7 +1288,7 @@ let rec resume_main t_level stack value =
   end
 
 let resume defs stack value =
-  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) in 
+  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) in 
   let (o,t_level) = to_global_letbinds defs t_level in
   match o with
   | (Value _ _,_,_) -> 
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index 11209ab5..e52d5ff9 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -5,10 +5,13 @@
  }
 
 register (xer) XER
+register (bit[1]) query
 
 function bit main _ = {
   XER := 0b010101010101010101010101010101010101010101010101010101010101001;
   f := XER;
   (bit[7]) foo := XER[57..63];
+  query := XER.SO;
+(*  XER.SO := query;*)
   bitzero }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 58bbffee..fad01f87 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -378,27 +378,27 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
       | Some(Some((params,t),tag,cs,ef)) ->
 	let t,cs,ef = subst params t cs ef in
-	let t,cs,ef = match get_abbrev d_env t with
+	let ta,cs,ef = match get_abbrev d_env t with
 	  | Some(t,cs1,ef1) -> t,cs@cs1,union_effects ef ef1
 	  | None -> t,cs,ef in
-        (match t.t,expect_t.t with 
+        (match ta.t,expect_t.t with 
         | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
         | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
           let tannot = Some(([],t),Emp,cs,ef) in
           let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in
-          (e',t',t_env,cs@cs',ef)
+          (e',t,t_env,cs@cs',ef)
         | Tapp("register",[TA_typ(t')]),_ ->
 	  let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
-          let tannot = Some(([],t),External (Some "register"),cs,ef') in
+          let tannot = Some(([],ta),External (Some "register"),cs,ef') in
           let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t in
-          (e',t',t_env,cs@cs',ef)
+          (e',t,t_env,cs@cs',ef)
         | Tapp("reg",[TA_typ(t)]),_ ->
           let tannot = Some(([],t),Emp,cs,pure_e) in
           let t',cs',e' = type_coerce l d_env t (rebuild tannot) expect_t in
-          (e',t',t_env,cs@cs',pure_e)
+          (e',t,t_env,cs@cs',pure_e)
         | _ -> 
           let t',cs',e' = type_coerce l d_env t (rebuild (Some(([],t),tag,cs,pure_e))) expect_t in
-          (e',t',t_env,cs@cs',pure_e)
+          (e',t,t_env,cs@cs',pure_e)
         )
       | Some None | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound"))
     | E_lit (L_aux(lit,l')) ->