Correctly type checking and interpreting accesses of register "fields". Register-reading action isn't reading the subreg correctly still (seems to be making up a value though).

Corrects but to vectors.sail and power.sail use of plus.
(A new bug in power.sail is exposed using a binary operator with one value)

5 files changed, 44 insertions, 21 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 6bc4964d..20fc1fb6 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -595,13 +595,7 @@ val interp_lbind : top_level -> env -> mem -> (letbind tannot) -> ((outcome * me
 
 let resolve_outcome to_match value_thunk action_thunk =
   match to_match with
-    | (Value v tag,lm,le) -> 
-      match (tag,v) with 
-	| (Tag_extern _, V_register regform) ->
-	  (Action (Read_reg regform Nothing) 
-	          (Frame (id_of_string "0")
-		         (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) le lm Top), lm,le)
-	| _ -> value_thunk v lm le end
+    | (Value v tag,lm,le) -> value_thunk v lm le
     | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
     | (Error l s,lm,le) -> (Error l s,lm,le)
   end
@@ -630,7 +624,13 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
       else (Value (V_lit lit) Tag_empty, l_mem,l_env)
     | E_cast typ exp -> 
       resolve_outcome (interp_main t_level l_env l_mem exp)
-	              (fun v lm le -> (Value v tag,lm,le))
+	              (fun v lm le -> 
+                        match (tag,v) with 
+	                | (Tag_extern _, V_register regform) ->
+	                  (Action (Read_reg regform Nothing) 
+	                     (Frame (id_of_string "0")
+		                (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) le lm Top), lm,le)
+                        | _ -> (Value v tag,lm,le) end)
 	              (fun a -> a )
  (* TODO introduce coercions to change offset of vectors *)
     | E_id id -> 
@@ -794,6 +794,16 @@ and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
 				  | _ -> Error l "Internal error, unrecognized read, no id"
 		                end 
                               | Nothing -> Error l "Internal error, unrecognized read, no reg" end
+                         | (E_aux _ (l,Just(_,Tag_extern _,_,_)),
+                            (Action (Read_reg ((Reg _ (Just((T_abbrev (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*)
@@ -1209,17 +1219,27 @@ 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)))
-       | Write_reg ((Reg id' t') as regf) Nothing value -> 
+       | Write_reg ((Reg _ (Just(T_id id',_,_,_))) 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, no field",lm,le),Nothing)
+		 end 
+            | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
+       | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_))) 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)
+	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
 		 end 
-            | Nothing -> ((Error l "Internal error, unrecognized write",lm,le),Nothing) end
-       | _ -> ((Error l "Internal error, unrecognized write",lm,le),Nothing)
+            | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
+       | _ -> ((Error l "Internal error, unrecognized write, no matching action",lm,le),Nothing)
        end 
      | e -> e end)
      end	
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index 5faf8d55..b355f75a 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -12,6 +12,6 @@ function bit main _ = {
   f := XER;
   (bit[7]) foo := XER[57..63];
   query := XER.SO;
-  (*XER.SO := query;*)
+  XER.SO := 0b0;
   bitzero }
 
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index e13644b4..c7fd6d77 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -19,7 +19,7 @@ function bit main _ = {
   slice_check := v3[1..10];
   slice_check := v3[5..10];
 
-  gpr_small[1] := v3;
+  gpr_small[1] := v3; (*Writes to slice_check*)
   slice_check_copy := gpr_small[1];
  
   i := [bitzero, bitzero, bitone, bitzero];
diff --git a/src/type_check.ml b/src/type_check.ml
index 983340a1..1aa2ea1a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1032,10 +1032,13 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t))) 
     | LEXP_field(vec,id)-> 
       let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in
-      (match item_t.t with
+      let vec_t = match vec' with
+        | LEXP_aux(_,(l',Some((parms,t),_,_,_))) -> t
+        | _ -> item_t in
+      (match vec_t.t with
 	| Tid i | Tabbrev({t=Tid i},_) ->
 	  (match lookup_record_typ i d_env.rec_env with
-	    | None -> typ_error l ("Expected a register for this update, instead found an expression with type " ^ i)
+	    | None -> typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i)
 	    | Some(((i,rec_kind,fields) as r)) ->
 	      let fi = id_to_string id in
 	      (match lookup_field_type fi r with
@@ -1043,7 +1046,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 		  typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
 		| Some((params,et),_,cs,_) ->
 		  let et,cs,ef = subst params et cs ef in
-		  (LEXP_aux(LEXP_field(vec',id),(l,(Some(([],item_t),tag,csi@cs,ef)))),et,env,tag,csi@cs,ef)))
+		  (LEXP_aux(LEXP_field(vec',id),(l,(Some(([],vec_t),tag,csi@cs,ef)))),et,env,tag,csi@cs,ef)))
 	| _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t)))
 
 and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * effect =
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 3d4d4689..6f4b746f 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -569,10 +569,10 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or enum is not properly kinded"))
     | "register",_ ->
       (match args1 with
-	| [TA_typ t] -> 
-	  let t',cs = type_consistent l d_env t t2 in
-	  (t',cs,E_aux(E_cast(t_to_typ t',e),(l,Some(([],t2),External None,cs,pure_e))))
-	| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))			     
+	| [TA_typ t] ->
+          let new_e = E_aux(E_cast(t_to_typ t,e),(l,Some(([],t),External None,[],pure_e))) in (*Wrong effect, should be reading a register*)
+	  type_coerce l d_env t new_e t2
+	| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
     | _,_ -> 
       let t',cs' = type_consistent l d_env t1 t2 in (t',cs',e))
   | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->