Reading from an alias to two concatenated registers; not writing yet.

4 files changed, 48 insertions, 34 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index e150f70b..cf2ca43d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1808,45 +1808,50 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
   let stack = Hole_frame (Id_aux (Id "0") Unknown)
 		          (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
 			  t_level l_env l_mem Top in
+  let get_reg_typ_name typ =
+    match typ with
+      | T_id i -> i
+      | T_abbrev (T_id i) _ -> i
+    end in
   match alspec with
     | AL_subreg reg subreg ->
       (match in_env regs reg with
-	| Just (V_register (Reg _ (Just((T_id id),_,_,_)))) ->
-	  (match in_env subregs (Id_aux (Id id) Unknown) with
+	| Just (V_register (Reg _ (Just (t,_,_,_)))) ->
+	  let reg_ti = get_reg_typ_name t in
+	  (match in_env subregs (Id_aux (Id reg_ti) Unknown) with
 	    | Just indexes -> 
 	      (match in_env indexes subreg with
 		| Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot) ir) Nothing) stack, l_mem, l_env)
 		| _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
-	    | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
-	| Just (V_register ((Reg _ (Just((T_abbrev (T_id id) _),_,_,_))) as rf)) ->
-	  (match in_env subregs (Id_aux (Id id) Unknown) with
-	    | Just indexes -> 
-	      (match in_env indexes subreg with
-		| Just ir -> (Action (Read_reg (SubReg subreg rf ir) Nothing) stack, l_mem, l_env)
-		| _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
-	    | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
+	    | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), l_mem, l_env) end)
 	| _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register " (get_id reg)),l_mem,l_env) end)
- | AL_bit reg e ->
-   resolve_outcome (interp_main mode t_level l_env l_mem e) 
-                   (fun v le lm -> match v with 
-		     | V_lit (L_aux (L_num i) _) -> 
-		       (Action (Read_reg (Reg reg annot) (Just (i,i))) stack, l_mem, l_env) end)
-                   (fun a -> a)
- | AL_slice reg start stop -> 
-   resolve_outcome (interp_main mode t_level l_env l_mem start)
-                   (fun v lm le -> 
-		     match v with 
-		       | V_lit (L_aux (L_num start) _) ->
-			 (resolve_outcome (interp_main mode t_level l_env lm stop)
-			                  (fun v le lm ->
-					    (match v with
-					      | V_lit (L_aux (L_num stop) _) ->
-						(Action (Read_reg (Reg reg annot) (Just (start,stop))) stack,
-						 l_mem, l_env) end))
-					  (fun a -> a)) end)
-                    (fun a -> a)
- | AL_concat reg1 reg2 -> (Error l "Unimplemented yet, alias spec concat", l_mem, l_env)
-end
+    | AL_bit reg e ->
+      resolve_outcome (interp_main mode t_level l_env l_mem e) 
+                      (fun v le lm -> match v with 
+			| V_lit (L_aux (L_num i) _) -> 
+			  (Action (Read_reg (Reg reg annot) (Just (i,i))) stack, l_mem, l_env) end)
+                      (fun a -> a) (*Should not currently happen as type system enforces constants*)
+    | AL_slice reg start stop -> 
+      resolve_outcome (interp_main mode t_level l_env l_mem start)
+                      (fun v lm le -> 
+			match v with 
+			  | V_lit (L_aux (L_num start) _) ->
+			    (resolve_outcome 
+			       (interp_main mode t_level l_env lm stop)
+			       (fun v le lm ->
+				 (match v with
+				   | V_lit (L_aux (L_num stop) _) ->
+				     (Action (Read_reg (Reg reg annot) (Just (start,stop))) stack, l_mem, l_env) end))
+			       (fun a -> a)) end)
+                      (fun a -> a) (*Neither action function should occur, due to above*)
+    | AL_concat reg1 reg2 -> 
+      (Action (Read_reg (Reg reg1 annot) Nothing)
+	      (Hole_frame (Id_aux (Id "0") Unknown)
+		          (E_aux (E_vector_append (E_aux (E_id (Id_aux (Id "0") l)) (l, (intern_annot annot)))
+				                  (E_aux (E_id reg2) 
+						         (l, (Just ((T_app "register" (T_args [T_arg_typ (T_var "fresh")])),
+								   (Tag_extern (Just (get_id reg2))), [], pure)))))
+			        (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end
 
 let rec to_global_letbinds (Defs defs) t_level =
   let  (Env defs' lets regs ctors subregs aliases) = t_level in
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 54cd60e2..91a81634 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -147,6 +147,11 @@ module Reg = struct
   include Map.Make(struct type t = id let compare = id_compare end)
   let to_string id v =
     sprintf "%s -> %s" (id_to_string id) (val_to_string v)
+  let find id m =
+    eprintf "reg_find called with %s\n" (id_to_string id);
+    let v = find id m in
+    eprintf "%s -> %s\n" (id_to_string id) (val_to_string v);
+    v
 end ;;
 
 module Mem = struct
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index 0e6e0dea..53f03da8 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -11,6 +11,7 @@ register (bit) query
 register alias CA = XER.CA
 register alias Fo = XER[35]
 register alias foobar = XER[35..36]
+register alias doub = XER:XER
 
 function (bit[64]) main _ = {
   XER := 0b0101010101010101010101010101010101010101010101010101010101010010;
@@ -23,5 +24,6 @@ function (bit[64]) main _ = {
   CA := query;
   XER.FOOBAR := 0b11;
   XER.FOOBAR := foobar;
+  query := doub[13];
   XER }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index b58ab263..d0274d72 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -367,7 +367,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       | Some(Base(tp,Default,cs,ef)) | Some(Base(tp,Spec,cs,ef)) ->
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
       | Some(Base((params,t),tag,cs,ef)) ->
-	let t,cs,ef = match tag with | Emp_global | External _ -> subst params t cs ef | Alias -> t,cs, add_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) ef | _ -> t,cs,ef in
+	let ((t,cs,ef),is_alias) = 
+	  match tag with | Emp_global | External _ -> (subst params t cs ef),false 
+	    | Alias -> (t,cs, add_effect (BE_aux(BE_rreg, Parse_ast.Unknown)) ef),true | _ -> (t,cs,ef),false in
         let t,cs' = get_abbrev d_env t in
         let cs = cs@cs' in
         let t_actual,expect_actual = match t.t,expect_t.t with
@@ -383,12 +385,12 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
           (rebuild tannot,t,t_env,cs@cs',ef)
         | Tapp("register",[TA_typ(t')]),Tuvar _ ->
 	  let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
-          let tannot = Base(([],t),External (Some i),cs,ef') in
+          let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef') in
           let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild tannot) expect_actual in
           (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 = Base(([],t),External (Some i),cs,ef') in
+          let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef') in
           let t',cs',e' = type_coerce (Expr l) d_env false t' (rebuild tannot) expect_actual in
           (e',t',t_env,cs@cs',ef)
         | Tapp("reg",[TA_typ(t')]),_ ->