From cf267a6d0f0b65c74c78fc3cf13e2175e49aea68 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Fri, 18 Jul 2014 12:04:22 +0100 Subject: Writing to concatenated aliases --- language/l2.lem | 218 ++++++++++++++++++++++++---------------------- language/l2.ml | 62 +++++++------ language/l2.ott | 14 +-- src/initial_check.ml | 9 +- src/lem_interp/interp.lem | 164 +++++++++++++++++----------------- src/pretty_print.ml | 18 ++-- src/test/regbits.sail | 1 + src/type_check.ml | 18 ++-- 8 files changed, 267 insertions(+), 237 deletions(-) diff --git a/language/l2.lem b/language/l2.lem index 60b566a9..a9bba453 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -29,24 +29,20 @@ type base_kind_aux = (* base kind *) | BK_effect (* kind of effect sets *) -type base_kind = - | BK_aux of base_kind_aux * l - - type kid_aux = (* variables with kind, ticked to differntiate from program variables *) | Var of x -type kind_aux = (* kinds *) - | K_kind of list base_kind +type base_kind = + | BK_aux of base_kind_aux * l type kid = | Kid_aux of kid_aux * l -type kind = - | K_aux of kind_aux * l +type kind_aux = (* kinds *) + | K_kind of list base_kind type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) @@ -61,6 +57,10 @@ and nexp = | Nexp_aux of nexp_aux * l +type kind = + | K_aux of kind_aux * l + + type base_effect_aux = (* effect *) | BE_rreg (* read register *) | BE_wreg (* write register *) @@ -109,11 +109,6 @@ let effect_union e1 e2 = end -type kinded_id_aux = (* optionally kind-annotated identifier *) - | KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) - - type n_constraint_aux = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp @@ -121,14 +116,19 @@ type n_constraint_aux = (* constraint over kind $Nat$ *) | NC_nat_set_bounded of kid * list integer -type kinded_id = - | KOpt_aux of kinded_id_aux * l +type kinded_id_aux = (* optionally kind-annotated identifier *) + | KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type n_constraint = | NC_aux of n_constraint_aux * l +type kinded_id = + | KOpt_aux of kinded_id_aux * l + + type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) | QI_id of kinded_id (* An optionally kinded identifier *) | QI_const of n_constraint (* A constraint for this type *) @@ -143,6 +143,19 @@ type typquant_aux = (* type quantifiers and constraints *) | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +type lit_aux = (* Literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of integer (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* constant representing undefined values *) + | L_string of string (* string constant *) + + type typquant = | TypQ_aux of typquant_aux * l @@ -168,29 +181,12 @@ and typ_arg = | Typ_arg_aux of typ_arg_aux * l -type lit_aux = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of integer (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) - - -type typschm_aux = (* type scheme *) - | TypSchm_ts of typquant * typ - - type lit = | L_aux of lit_aux * l -type typschm = - | TypSchm_aux of typschm_aux * l +type typschm_aux = (* type scheme *) + | TypSchm_ts of typquant * typ type pat_aux 'a = (* Pattern *) @@ -217,7 +213,22 @@ and fpat 'a = | FP_aux of (fpat_aux 'a) * annot 'a -type exp_aux 'a = (* Expression *) +type typschm = + | TypSchm_aux of typschm_aux * l + + +type reg_id_aux 'a = + | RI_id of id + + +type letbind_aux 'a = (* Let binding *) + | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) + | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) + +and letbind 'a = + | LB_aux of (letbind_aux 'a) * annot 'a + +and exp_aux 'a = (* Expression *) | E_block of list (exp 'a) (* block *) | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) | E_id of id (* identifier *) @@ -286,34 +297,29 @@ and pexp_aux 'a = (* Pattern match *) and pexp 'a = | Pat_aux of (pexp_aux 'a) * annot 'a -and letbind_aux 'a = (* Let binding *) - | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) - | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) -and letbind 'a = - | LB_aux of (letbind_aux 'a) * annot 'a +type reg_id 'a = + | RI_aux of (reg_id_aux 'a) * annot 'a type alias_spec_aux 'a = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) - | AL_subreg of id * id (* id must refer to a register, id' to a declared subregister of id *) - | AL_bit of id * (exp 'a) - | AL_slice of id * (exp 'a) * (exp 'a) - | AL_concat of id * id (* both id and id' must refer to a register *) + | AL_subreg of (reg_id 'a) * id + | AL_bit of (reg_id 'a) * (exp 'a) + | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) + | AL_concat of (reg_id 'a) * (reg_id 'a) -type type_union_aux = (* Type union constructors *) - | Tu_id of id - | Tu_ty_id of typ * id +type rec_opt_aux = (* Optional recursive annotation for functions *) + | Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) -type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string +type funcl_aux 'a = (* Function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) -type rec_opt_aux = (* Optional recursive annotation for functions *) - | Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +type tannot_opt_aux = (* Optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ type effect_opt_aux = (* Optional effect annotation for functions *) @@ -321,55 +327,51 @@ type effect_opt_aux = (* Optional effect annotation for functions *) | Effect_opt_effect of effect -type tannot_opt_aux = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ +type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string -type funcl_aux 'a = (* Function clause *) - | FCL_Funcl of id * (pat 'a) * (exp 'a) +type type_union_aux = (* Type union constructors *) + | Tu_id of id + | Tu_ty_id of typ * id type alias_spec 'a = | AL_aux of (alias_spec_aux 'a) * annot 'a -type type_union = - | Tu_aux of type_union_aux * l - - -type name_scm_opt = - | Name_sect_aux of name_scm_opt_aux * l - +type rec_opt = + | Rec_aux of rec_opt_aux * l -type index_range_aux = (* index specification, for bitfields in register types *) - | BF_single of integer (* single index *) - | BF_range of integer * integer (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) -and index_range = - | BF_aux of index_range_aux * l +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * l -type rec_opt = - | Rec_aux of rec_opt_aux * l +type tannot_opt = + | Typ_annot_opt_aux of tannot_opt_aux * l type effect_opt = | Effect_opt_aux of effect_opt_aux * l -type tannot_opt = - | Typ_annot_opt_aux of tannot_opt_aux * l +type name_scm_opt = + | Name_sect_aux of name_scm_opt_aux * l -type funcl 'a = - | FCL_aux of (funcl_aux 'a) * l +type type_union = + | Tu_aux of type_union_aux * l -type val_spec_aux 'a = (* Value type specification *) - | VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) +type index_range_aux = (* index specification, for bitfields in register types *) + | BF_single of integer (* single index *) + | BF_range of integer * integer (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + | BF_aux of index_range_aux * l type dec_spec_aux 'a = (* Register declarations *) @@ -378,14 +380,6 @@ type dec_spec_aux 'a = (* Register declarations *) | DEC_typ_alias of typ * id * (alias_spec 'a) -type type_def_aux 'a = (* Type definition body *) - | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - type fundef_aux 'a = (* Function definition *) | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) @@ -399,23 +393,29 @@ type scattered_def_aux 'a = (* Function and type union definitions that can be | SD_scattered_end of id (* scattered definition end *) +type type_def_aux 'a = (* Type definition body *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + + type default_spec_aux 'a = (* Default kinding or typing assumption *) | DT_kind of base_kind * kid | DT_typ of typschm * id -type val_spec 'a = - | VS_aux of (val_spec_aux 'a) * annot 'a +type val_spec_aux 'a = (* Value type specification *) + | VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) type dec_spec 'a = | DEC_aux of (dec_spec_aux 'a) * annot 'a -type type_def 'a = - | TD_aux of (type_def_aux 'a) * annot 'a - - type fundef 'a = | FD_aux of (fundef_aux 'a) * annot 'a @@ -424,10 +424,18 @@ type scattered_def 'a = | SD_aux of (scattered_def_aux 'a) * annot 'a +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a + + type default_spec 'a = | DT_aux of (default_spec_aux 'a) * l +type val_spec 'a = + | VS_aux of (val_spec_aux 'a) * annot 'a + + type def 'a = (* Top-level definition *) | DEF_type of (type_def 'a) (* type definition *) | DEF_fundef of (fundef 'a) (* function definition *) @@ -502,17 +510,6 @@ type tid = (* A type identifier or type variable *) | Tid_var of kid -type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) - | Tag_empty - | Tag_global (* Globally let-bound or enumeration based value/variable *) - | Tag_ctor (* Data constructor from a type union *) - | Tag_extern of maybe string (* External function, specied only with a val statement *) - | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) - | Tag_spec - | Tag_enum - | Tag_alias - - type t = (* Internal types *) | T_id of x | T_var of x @@ -531,6 +528,17 @@ and t_args = (* Arguments to type constructors *) | T_args of list t_arg +type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) + | Tag_empty + | Tag_global (* Globally let-bound or enumeration based value/variable *) + | Tag_ctor (* Data constructor from a type union *) + | Tag_extern of maybe string (* External function, specied only with a val statement *) + | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) + | Tag_spec + | Tag_enum + | Tag_alias + + type tinf = (* Type variables, type, and constraints, bound to an identifier *) | Tinf_typ of t | Tinf_quant_typ of (map tid kinf) * list nec * tag * t diff --git a/language/l2.ml b/language/l2.ml index 60343397..a00e2f84 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -80,6 +80,12 @@ id_aux = (* Identifier *) | DeIid of x (* remove infix status *) +type +effect_aux = (* effect set, of kind Effects *) + Effect_var of kid + | Effect_set of (base_effect) list (* effect set *) + + type order_aux = (* vector order specifications, of kind Order *) Ord_var of kid (* variable *) @@ -87,25 +93,19 @@ order_aux = (* vector order specifications, of kind Order *) | Ord_dec (* decreasing (big-endian) *) -type -effect_aux = (* effect set, of kind Effects *) - Effect_var of kid - | Effect_set of (base_effect) list (* effect set *) - - type id = Id_aux of id_aux * l type -order = - Ord_aux of order_aux * l +effect = + Effect_aux of effect_aux * l type -effect = - Effect_aux of effect_aux * l +order = + Ord_aux of order_aux * l type @@ -230,6 +230,11 @@ typschm = TypSchm_aux of typschm_aux * l +type +'a reg_id_aux = + RI_id of id + + type 'a exp_aux = (* Expression *) E_block of ('a exp) list (* block *) @@ -309,11 +314,8 @@ and 'a letbind = type -'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) - AL_subreg of id * id (* id must refer to a register, id' to a declared subregister of id *) - | AL_bit of id * 'a exp - | AL_slice of id * 'a exp * 'a exp - | AL_concat of id * id (* both id and id' must refer to a register *) +'a reg_id = + RI_aux of 'a reg_id_aux * 'a annot type @@ -351,8 +353,11 @@ rec_opt_aux = (* Optional recursive annotation for functions *) type -'a alias_spec = - AL_aux of 'a alias_spec_aux * 'a annot +'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) + AL_subreg of 'a reg_id * id + | AL_bit of 'a reg_id * 'a exp + | AL_slice of 'a reg_id * 'a exp * 'a exp + | AL_concat of 'a reg_id * 'a reg_id type @@ -396,10 +401,8 @@ and index_range = type -'a dec_spec_aux = (* Register declarations *) - DEC_reg of typ * id - | DEC_alias of id * 'a alias_spec - | DEC_typ_alias of typ * id * 'a alias_spec +'a alias_spec = + AL_aux of 'a alias_spec_aux * 'a annot type @@ -432,6 +435,13 @@ type FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list +type +'a dec_spec_aux = (* Register declarations *) + DEC_reg of typ * id + | DEC_alias of id * 'a alias_spec + | DEC_typ_alias of typ * id * 'a alias_spec + + type 'a val_spec_aux = (* Value type specification *) VS_val_spec of typschm * id @@ -439,11 +449,6 @@ type | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) -type -'a dec_spec = - DEC_aux of 'a dec_spec_aux * 'a annot - - type 'a scattered_def = SD_aux of 'a scattered_def_aux * 'a annot @@ -464,6 +469,11 @@ type FD_aux of 'a fundef_aux * 'a annot +type +'a dec_spec = + DEC_aux of 'a dec_spec_aux * 'a annot + + type 'a val_spec = VS_aux of 'a val_spec_aux * 'a annot diff --git a/language/l2.ott b/language/l2.ott index 1a4d2038..7a50877b 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -828,15 +828,17 @@ scattered_def :: 'SD_' ::= | end id :: :: scattered_end {{ com scattered definition end }} +reg_id :: 'RI_' ::= + {{ aux _ annot }} {{ auxparam 'a }} + | id :: :: id + alias_spec :: 'AL_' ::= {{ com Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector }} {{ aux _ annot }} {{ auxparam 'a }} - | id . id' :: :: subreg - {{ com id must refer to a register, id' to a declared subregister of id }} - | id [ exp ] :: :: bit - | id [ exp '..' exp' ] :: :: slice - | id : id' :: :: concat - {{ com both id and id' must refer to a register }} + | reg_id . id :: :: subreg + | reg_id [ exp ] :: :: bit + | reg_id [ exp '..' exp' ] :: :: slice + | reg_id : reg_id' :: :: concat dec_spec :: 'DEC_' ::= {{ com Register declarations }} diff --git a/src/initial_check.ml b/src/initial_check.ml index d14fdc59..3c1ab601 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -614,14 +614,15 @@ let to_ast_alias_spec k_env (Parse_ast.E_aux(e,le)) = AL_aux( (match e with | Parse_ast.E_field(Parse_ast.E_aux(Parse_ast.E_id id,li), field) -> - AL_subreg(to_ast_id id,to_ast_id field) + AL_subreg(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_id field) | Parse_ast.E_vector_access(Parse_ast.E_aux(Parse_ast.E_id id,li),range) -> - AL_bit(to_ast_id id,to_ast_exp k_env range) + AL_bit(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env range) | Parse_ast.E_vector_subrange(Parse_ast.E_aux(Parse_ast.E_id id,li),base,stop) -> - AL_slice(to_ast_id id,to_ast_exp k_env base,to_ast_exp k_env stop) + AL_slice(RI_aux(RI_id (to_ast_id id),(li,NoTyp)),to_ast_exp k_env base,to_ast_exp k_env stop) | Parse_ast.E_vector_append(Parse_ast.E_aux(Parse_ast.E_id first,lf), Parse_ast.E_aux(Parse_ast.E_id second,ls)) -> - AL_concat(to_ast_id first,to_ast_id second) + AL_concat(RI_aux(RI_id (to_ast_id first),(lf,NoTyp)), + RI_aux(RI_id (to_ast_id second),(ls,NoTyp))) ), (le,NoTyp)) let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(regdec,l)) = diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index cf2ca43d..e2d6b781 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1560,53 +1560,62 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( (match in_env aliases id with | Just (AL_aux aspec (l,_)) -> (match aspec 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 indexes -> - (match in_env indexes subreg with - | Just ir -> - (Action (Write_reg (SubReg subreg (Reg reg annot) ir) Nothing value) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) - t_level l_env l_mem Top), 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 (Write_reg (SubReg subreg (Reg reg annot) ir) Nothing value) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) - t_level l_env l_mem Top), 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 " (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 (Write_reg (Reg reg annot) (Just (i,i)) value) + | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_id id),_,_,_)) as annot'))) subreg -> + (match in_env subregs (Id_aux (Id id) Unknown) with + | Just indexes -> + (match in_env indexes subreg with + | Just ir -> + (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) - t_level l_env l_mem Top), 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 (Write_reg (Reg reg annot) (Just (start,stop)) value) - (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) - t_level l_env l_mem Top), - 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) + t_level l_env l_mem Top), 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) + | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_abbrev (T_id id) _),_,_,_)) as annot'))) subreg -> + (match in_env subregs (Id_aux (Id id) Unknown) with + | Just indexes -> + (match in_env indexes subreg with + | Just ir -> + (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) + (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) + t_level l_env l_mem Top), 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) + | AL_bit (RI_aux (RI_id reg) (_,annot')) 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 (Write_reg (Reg reg annot') (Just (i,i)) value) + (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) + t_level l_env l_mem Top), l_mem, l_env) end) + (fun a -> a) + | AL_slice (RI_aux (RI_id reg) (_,annot')) 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 (Write_reg (Reg reg annot') (Just (start,stop)) value) + (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot)) + t_level l_env l_mem Top), + l_mem, l_env) end)) + (fun a -> a)) end) + (fun a -> a) + | AL_concat (RI_aux (RI_id reg1) (l1,annot1)) (RI_aux (RI_id reg2) annot2) -> + let val_typ t = match t with + | T_app "register" (T_args [T_arg_typ t]) -> t + | T_abbrev _ (T_app "register" (T_args [T_arg_typ t])) -> t end in + let (t1,t2) = match (annot1,annot2) with + | (Just (t1,_,_,_), (_,(Just (t2,_,_,_)))) -> (val_typ t1,val_typ t2) end in + (match (t1,t2) with + | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]), + T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) -> + (Action (Write_reg (Reg reg1 annot1) Nothing (slice_vector value b1 r1)) + (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2) + (to_exp (slice_vector value (r1+1) r2))) annot2) + t_level l_env l_mem Top), l_mem,l_env) end) end) | _ -> (Error l (String.stringAppend "Internal error: alias not found for id " (get_id id)),l_mem,l_env) end) in (request,Nothing) | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern, empty, or alias " (get_id id)),l_mem,l_env),Nothing) @@ -1814,43 +1823,38 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) = | 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,_,_,_)))) -> - 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 " 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 -> + | AL_subreg (RI_aux (RI_id reg) (li,((Just (t,_,_,_)) as annot'))) subreg -> + 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 " reg_ti), l_mem, l_env) end) + | AL_bit (RI_aux (RI_id reg) (_,annot')) 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 -> + (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 (RI_aux (RI_id reg) (_,annot')) 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) + (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 (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) -> + (Action (Read_reg (Reg reg1 annot1) 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))))) + (E_aux (E_vector_append (E_aux (E_id (Id_aux (Id "0") l1)) (l1, (intern_annot annot1))) + (E_aux (E_id reg2) annot2)) (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 = diff --git a/src/pretty_print.ml b/src/pretty_print.ml index ea6a893b..f4729814 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -496,15 +496,17 @@ let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) = pp_lem_l l pp_annot annot let pp_lem_aspec ppf (AL_aux(aspec,(l,annot))) = + let pp_reg_id ppf (RI_aux((RI_id ri),(l,annot))) = + fprintf ppf "@[<0>(RI_aux (RI_id %a) (%a,%a))@]" pp_lem_id ri pp_lem_l l pp_annot annot in match aspec with | AL_subreg(reg,subreg) -> - fprintf ppf "@[<0>(AL_aux (AL_subreg %a %a) (%a,%a))@]" pp_lem_id reg pp_lem_id subreg pp_lem_l l pp_annot annot + fprintf ppf "@[<0>(AL_aux (AL_subreg %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_id subreg pp_lem_l l pp_annot annot | AL_bit(reg,ac) -> - fprintf ppf "@[<0>(AL_aux (AL_bit %a %a) (%a,%a))@]" pp_lem_id reg pp_lem_exp ac pp_lem_l l pp_annot annot + fprintf ppf "@[<0>(AL_aux (AL_bit %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp ac pp_lem_l l pp_annot annot | AL_slice(reg,b,e) -> - fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]" pp_lem_id reg pp_lem_exp b pp_lem_exp e pp_lem_l l pp_annot annot + fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp b pp_lem_exp e pp_lem_l l pp_annot annot | AL_concat(f,s) -> - fprintf ppf "@[<0>(AL_aux (AL_concat %a %a) (%a,%a))@]" pp_lem_id f pp_lem_id s pp_lem_l l pp_annot annot + fprintf ppf "@[<0>(AL_aux (AL_concat %a %a) (%a,%a))@]" pp_reg_id f pp_reg_id s pp_lem_l l pp_annot annot let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) = match reg with @@ -1033,10 +1035,10 @@ let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) = let doc_alias (AL_aux (alspec,_)) = match alspec with - | AL_subreg(id,subid) -> doc_id id ^^ dot ^^ doc_id subid - | AL_bit(id,ac) -> doc_id id ^^ brackets (doc_exp ac) - | AL_slice(id,b,e) -> doc_id id ^^ brackets (doc_op dotdot (doc_exp b) (doc_exp e)) - | AL_concat(f,s) -> doc_op colon (doc_id f) (doc_id s) + | AL_subreg((RI_aux (RI_id id,_)),subid) -> doc_id id ^^ dot ^^ doc_id subid + | AL_bit((RI_aux (RI_id id,_)),ac) -> doc_id id ^^ brackets (doc_exp ac) + | AL_slice((RI_aux (RI_id id,_)),b,e) -> doc_id id ^^ brackets (doc_op dotdot (doc_exp b) (doc_exp e)) + | AL_concat((RI_aux (RI_id f,_)),(RI_aux (RI_id s,_))) -> doc_op colon (doc_id f) (doc_id s) let doc_dec (DEC_aux (reg,_)) = match reg with diff --git a/src/test/regbits.sail b/src/test/regbits.sail index 53f03da8..469f0f79 100644 --- a/src/test/regbits.sail +++ b/src/test/regbits.sail @@ -25,5 +25,6 @@ function (bit[64]) main _ = { XER.FOOBAR := 0b11; XER.FOOBAR := foobar; query := doub[13]; + doub := XER:XER; XER } diff --git a/src/type_check.ml b/src/type_check.ml index d0274d72..40a5f04c 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1062,7 +1062,9 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef)))), t, Envmap.empty, External (Some reg),[],ef) | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_)))) -> let ef = {effect=Eset [BE_aux(BE_wreg,l)]} in - (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef))), t, Envmap.empty, External None,[],ef) + let u = match t.t with + | Tapp("register", [TA_typ u]) -> u in + (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef))), u, Envmap.empty, External None,[],ef) | _ -> assert false) | Some(Base((parms,t),tag,cs,_)) -> let t,cs,_ = match tag with | External _ | Emp_global -> subst parms t cs pure_e | _ -> t,cs,pure_e in @@ -1444,7 +1446,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, (*TODO Only works for inc vectors, need to add support for dec*) let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = let (Env(d_env,t_env)) = envs in - let check_reg (Id_aux(_,l) as id) : (string * typ * typ) = + let check_reg (RI_aux ((RI_id (Id_aux(_,l) as id)), _)) : (string * tannot reg_id * typ * typ) = let i = id_to_string id in (match Envmap.apply t_env i with | Some(Base(([],t), External (Some j), [], _)) -> @@ -1454,14 +1456,14 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = | _ -> t,t in (match t_actual.t with | Tapp("register",[TA_typ t']) -> - if i = j then (i,t_id,t') + if i = j then (i,(RI_aux (RI_id id, (l,Base(([],t),External (Some j), [], pure_e)))),t_id,t') else assert false | _ -> typ_error l ("register alias " ^ alias ^ " to " ^ i ^ " expected a register, found " ^ (t_to_string t))) | _ -> typ_error l ("register alias " ^ alias ^ " to " ^ i ^ " exepcted a register.")) in match al with | AL_subreg(reg_a,subreg) -> - let (reg,reg_t,t) = check_reg reg_a in + let (reg,reg_a,reg_t,t) = check_reg reg_a in (match reg_t.t with | Tid i -> (match lookup_record_typ i d_env.rec_env with @@ -1477,7 +1479,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = (AL_aux(AL_subreg(reg_a,subreg),(l,tannot)),tannot,d_env))) | _ -> let _ = Printf.printf "%s\n" (t_to_string reg_t) in assert false) | AL_bit(reg_a,bit) -> - let (reg,reg_t,t) = check_reg reg_a in + let (reg,reg_a,reg_t,t) = check_reg reg_a in let (E_aux(bit,(le,eannot)),_,_,_,_) = check_exp envs (new_t ()) bit in (match t.t with | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) -> @@ -1491,7 +1493,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = else typ_error ll ("Alias bit lookup must be in the range of the vector in the register") | _ -> assert false) | AL_slice(reg_a,sl1,sl2) -> - let (reg,reg_t,t) = check_reg reg_a in + let (reg,reg_a,reg_t,t) = check_reg reg_a in let (E_aux(sl1,(le1,eannot1)),_,_,_,_) = check_exp envs (new_t ()) sl1 in let (E_aux(sl2,(le2,eannot2)),_,_,_,_) = check_exp envs (new_t ()) sl2 in (match t.t with @@ -1509,8 +1511,8 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = else typ_error ll ("Alias slices must be in the range of the vector in the register") | _ -> assert false) | AL_concat(reg1_a,reg2_a) -> - let (reg1,reg_t,t1) = check_reg reg1_a in - let (reg2,reg_t,t2) = check_reg reg2_a in + let (reg1,reg1_a,reg_t,t1) = check_reg reg1_a in + let (reg2,reg2_a,reg_t,t2) = check_reg reg2_a in (match (t1.t,t2.t) with | (Tapp("vector",[TA_nexp b1;TA_nexp r; TA_ord {order = Oinc}; TA_typ item_t]), Tapp("vector",[TA_nexp _ ;TA_nexp r2; TA_ord {order = Oinc}; TA_typ item_t2])) -> -- cgit v1.2.3