From c209835410c323f90258fcb8ccf84514dda831af Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Wed, 12 Mar 2014 14:16:48 +0000 Subject: 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) --- src/lem_interp/interp.lem | 44 ++++++++++++++++++++++++++++++++------------ src/test/regbits.sail | 2 +- src/test/vectors.sail | 2 +- src/type_check.ml | 9 ++++++--- src/type_internal.ml | 8 ++++---- 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") -> -- cgit v1.2.3