summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml29
-rw-r--r--src/lem_interp/interp.lem79
-rw-r--r--src/lexer.mll2
-rw-r--r--src/parser.mly17
-rw-r--r--src/pretty_print.ml42
-rw-r--r--src/process_file.ml2
-rw-r--r--src/test/regbits.sail7
-rw-r--r--src/type_check.ml91
-rw-r--r--src/type_internal.ml6
-rw-r--r--src/type_internal.mli4
10 files changed, 254 insertions, 25 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index b95bf279..d14fdc59 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -384,6 +384,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
| Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env exp, List.map (to_ast_case k_env) pexps)
| Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env leb, to_ast_exp k_env exp)
| Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env lexp, to_ast_exp k_env exp)
+ | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env exp)
), (l,NoTyp))
and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp =
@@ -609,10 +610,30 @@ let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : par
| Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs
| _,_ -> def_in_progress id defs)
-let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(Parse_ast.DEC_reg(typ,id),l)) =
- let t = to_ast_typ k_env typ in
- let id = to_ast_id id in
- (DEC_aux(DEC_reg(t,id),(l,NoTyp)))
+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)
+ | 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)
+ | 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)
+ | 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)
+ ), (le,NoTyp))
+
+let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(regdec,l)) =
+ DEC_aux(
+ (match regdec with
+ | Parse_ast.DEC_reg(typ,id) ->
+ DEC_reg(to_ast_typ k_env typ,to_ast_id id)
+ | Parse_ast.DEC_alias(id,e) ->
+ DEC_alias(to_ast_id id,to_ast_alias_spec k_env e)
+ | Parse_ast.DEC_typ_alias(typ,id,e) ->
+ DEC_typ_alias(to_ast_typ k_env typ,to_ast_id id,to_ast_alias_spec k_env e)
+ ),(l,NoTyp))
let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (id * partial_def) list =
let envs = (names,k_env,t_env) in
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index d4fcafb7..4a429423 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -116,7 +116,7 @@ type barrier_kind = | Barrier_plain (* ?? *)
(*top_level is a tuple of
(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))
+type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range)) * list (id * (alias_spec tannot))
type action =
| Read_reg of reg_form * maybe (integer * integer)
@@ -126,6 +126,7 @@ type action =
| Barrier of id * value
| Write_next_IA of value (* Perhaps not needed? *)
| Nondet of list (exp tannot)
+ | Exit of (exp tannot)
| Debug of l
| Call_extern of string * value
@@ -173,7 +174,19 @@ let rec to_registers (Defs defs) =
| DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
| _ -> to_registers (Defs defs)
end
- end
+ end
+
+val to_aliases : defs tannot -> list (id * (alias_spec tannot))
+let rec to_aliases (Defs defs) =
+ match defs with
+ | [] -> []
+ | def::defs ->
+ match def with
+ | DEF_reg_dec (DEC_aux (DEC_alias id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
+ | DEF_reg_dec (DEC_aux (DEC_typ_alias typ id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
+ | _ -> to_aliases (Defs defs)
+ end
+ end
val has_rmem_effect : list base_effect -> bool
val has_barr_effect : list base_effect -> bool
@@ -874,6 +887,7 @@ let rec find_case pexps value =
val interp_main : interp_mode -> top_level -> env -> lmem -> (exp tannot) -> (outcome * lmem * env)
val exp_list : interp_mode -> top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> lmem -> list value -> list (exp tannot) -> (outcome * lmem * env)
val interp_lbind : interp_mode -> top_level -> env -> lmem -> (letbind tannot) -> ((outcome * lmem * env) * (maybe ((exp tannot) -> (letbind tannot))))
+val interp_alias_read : interp_mode -> top_level -> env -> lmem -> (alias_spec tannot) -> (outcome * lmem * env)
let resolve_outcome to_match value_thunk action_thunk =
match to_match with
@@ -897,7 +911,7 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
end
and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
- let (Env defs lets regs ctors subregs) = t_level in
+ let (Env defs lets regs ctors subregs aliases) = t_level in
let (typ,tag,ncs,effect) = match annot with
| Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -962,6 +976,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(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),
l_mem,l_env)
+ | Tag_alias ->
+ match in_env aliases id with
+ | Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
+ | _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
| _ -> (Error l (String.stringAppend "Internal error: tag other than empty,enum,or extern " name),l_mem,l_env)
end
| E_if cond thn els ->
@@ -1500,7 +1518,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
end
and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
- let (Env defs lets regs ctors subregs) = t_level in
+ let (Env defs lets regs ctors subregs aliases) = t_level in
let (typ,tag,ncs,ef) = match annot with
| Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1729,15 +1747,60 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
| e -> (e,Nothing) end
end
+and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
+ let (Env defs lets regs ctors subregs aliases) = t_level in
+ 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
+ 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 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 " (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
+
let rec to_global_letbinds (Defs defs) t_level =
- let (Env defs' lets regs ctors subregs) = t_level in
+ let (Env defs' lets regs ctors subregs aliases) = t_level in
match defs with
| [] -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, emem, []),t_level)
| def::defs ->
match def with
| DEF_val lbind ->
match interp_letbind <|eager_eval=true|> t_level [] emem lbind with
- | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs)
+ | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs aliases)
| ((Action a s,lm,le),_) ->
((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
| (e,_) -> (e,t_level) end
@@ -1745,14 +1808,14 @@ let rec to_global_letbinds (Defs defs) t_level =
match tdef with
| TD_enum id ns ids _ ->
let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
- to_global_letbinds (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs)
+ to_global_letbinds (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs aliases)
| _ -> to_global_letbinds (Defs defs) t_level end
| _ -> to_global_letbinds (Defs defs) t_level
end
end
let to_top_env defs =
- let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) in
+ let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
let (o,t_level) = to_global_letbinds defs t_level in
match o with
| (Value _ _,_,_) -> (Nothing,t_level)
diff --git a/src/lexer.mll b/src/lexer.mll
index b53577c5..f7cd1272 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -59,6 +59,7 @@ let kw_table =
M.empty
[
("and", (fun _ -> And));
+ ("alias", (fun _ -> Alias));
("as", (fun _ -> As));
("bitzero", (fun _ -> Bitzero));
("bitone", (fun _ -> Bitone));
@@ -75,6 +76,7 @@ let kw_table =
("end", (fun _ -> End));
("enumerate", (fun _ -> Enumerate));
("else", (fun _ -> Else));
+ ("exit", (fun _ -> Exit));
("extern", (fun _ -> Extern));
("false", (fun _ -> False));
("forall", (fun _ -> Forall));
diff --git a/src/parser.mly b/src/parser.mly
index aa6c853d..b36085a5 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -122,10 +122,12 @@ let make_vector_sugar typ typ1 =
/*Terminals with no content*/
-%token And As Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End Enumerate Else Extern
-%token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
+%token And Alias As Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End
+%token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order
+%token Pure Rec Register Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef
+%token Undefined Union With Val
%token Barr Rreg Wreg Rmem Wmem Undef Unspec Nondet
-%token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val
+
/* Avoid shift/reduce conflict - see right_atomic_exp rule */
%nonassoc Then
@@ -541,9 +543,6 @@ atomic_exp:
{ eloc (E_cast($2,$4)) }
| Lparen comma_exps Rparen
{ eloc (E_tuple($2)) }
- /* XXX creates many conflicts
- | Lcurly semi_exps Rcurly
- { eloc (E_record($2)) } */
| Lcurly exp With semi_exps Rcurly
{ eloc (E_record_update($2,$4)) }
| Lsquare Rsquare
@@ -562,6 +561,8 @@ atomic_exp:
{ eloc (E_list($2)) }
| Switch exp Lcurly case_exps Rcurly
{ eloc (E_case($2,$4)) }
+ | Exit atomic_exp
+ { eloc (E_exit $2) }
field_exp:
| atomic_exp
@@ -1171,6 +1172,10 @@ def:
{ dloc (DEF_default($1)) }
| Register atomic_typ id
{ dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
+ | Register Alias id Eq exp
+ { dloc (DEF_reg_dec(DEC_aux(DEC_alias($3,$5),loc ()))) }
+ | Register Alias atomic_typ id Eq exp
+ { dloc (DEF_reg_dec(DEC_aux(DEC_typ_alias($3,$4,$6), loc ()))) }
| Scattered scattered_def
{ dloc (DEF_scattered $2) }
| Function_ Clause funcl
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 2a24dc3e..a537ff46 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -253,6 +253,7 @@ let pp_format_tag = function
| Default -> "Tag_default"
| Constructor -> "Tag_ctor"
| Enum -> "Tag_enum"
+ | Alias -> "Tag_alias"
| Spec -> "Tag_spec"
let rec pp_format_nes nes =
@@ -374,6 +375,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
| E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
| E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
+ | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
| E_internal_exp (l, Base((_,t),_,_,_)) ->
(match t.t with
| Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
@@ -493,8 +495,25 @@ let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
pp_lem_l l pp_annot annot
-let pp_lem_dec ppf (DEC_aux(DEC_reg(typ,id),(l,annot))) =
- fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot
+let pp_lem_aspec ppf (AL_aux(aspec,(l,annot))) =
+ 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
+ | 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
+ | 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
+ | 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
+
+let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) =
+ match reg with
+ | DEC_reg(typ,id) ->
+ fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot
+ | DEC_alias(id,alias_spec) ->
+ fprintf ppf "@[<0>(DEC_aux (DEC_alias %a %a) (%a, %a))@]" pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot
+ | DEC_typ_alias(typ,id,alias_spec) ->
+ fprintf ppf "@[<0>(DEC_aux (DEC_typ_alias %a %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot
let pp_lem_def ppf d =
match d with
@@ -827,7 +846,7 @@ let doc_exp, doc_let =
parens (separate_map comma exp exps)
| E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
(* XXX E_record is not handled by parser currently
- AAA I don't think the parser can handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *)
+ AAA The parser can't handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *)
braces (separate_map semi_sp doc_fexp fexps)
| E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
@@ -849,6 +868,8 @@ let doc_exp, doc_let =
let opening = separate space [string "switch"; exp e; lbrace] in
let cases = separate_map (break 1) doc_case pexps in
surround 2 1 opening cases rbrace
+ | E_exit e ->
+ separate space [string "exit"; exp e;]
(* adding parens and loop for lower precedence *)
| E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
| E_cons (_, _)|E_field (_, _)|E_assign (_, _)
@@ -1010,8 +1031,19 @@ let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
string "effect"; doc_effects_opt efa;
clauses]
-let doc_dec (DEC_aux(DEC_reg(typ,id),_)) =
- separate space [string "register"; doc_atomic_typ typ; doc_id id]
+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)
+
+let doc_dec (DEC_aux (reg,_)) =
+ match reg with
+ | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id]
+ | DEC_alias(id,alspec) -> separate space [string "register"; string "alias"; doc_id id; equals; doc_alias alspec]
+ | DEC_typ_alias(typ,id,alspec) ->
+ separate space [string "register"; string "alias"; doc_atomic_typ typ; doc_id id; equals; doc_alias alspec]
let doc_scattered (SD_aux (sdef, _)) = match sdef with
| SD_scattered_function (r, typa, efa, id) ->
diff --git a/src/process_file.ml b/src/process_file.ml
index 6d1729a5..98dd4db9 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -93,7 +93,7 @@ let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind
let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) : Type_internal.tannot Ast.defs =
let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
Type_internal.namesch = Envmap.empty; Type_internal.enum_env = Envmap.empty;
- Type_internal.rec_env = []; } in
+ Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty} in
Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env)) defs
let open_output_with_check file_name =
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index ed2a95e0..46343d67 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -8,12 +8,19 @@
register (xer) XER
register (bit) query
+register alias CA = XER.CA
+register alias Fo = XER[35]
+register alias foobar = XER[35..36]
+
function (bit[64]) main _ = {
XER := 0b0101010101010101010101010101010101010101010101010101010101010010;
f := XER;
(bit[7]) foo := XER[57..63];
query := XER.SO;
XER.SO := 0;
+ query := CA;
+ query := Fo;
XER.FOOBAR := 0b11;
+ XER.FOOBAR := foobar;
XER }
diff --git a/src/type_check.ml b/src/type_check.ml
index f8ec0642..e68337ab 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -28,6 +28,7 @@ let rec field_equivs fields fmaps =
if (List.mem_assoc (id_to_string id) fmaps)
then match (field_equivs fields fmaps) with
| None -> None
+ | Some [] -> None
| Some fs -> Some(((List.assoc (id_to_string id) fmaps),id,l,pat)::fs)
else None
@@ -1010,6 +1011,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let (exp',t'',_,cs',ef') = check_exp envs t' exp in
let (t',c') = type_consistent (Expr l) d_env unit_t expect_t in
(E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],ef)))),unit_t,t_env',cs@cs'@c',union_effects ef ef')
+ | E_exit e ->
+ let (e',t',_,_,_) = check_exp envs (new_t ()) e in
+ (E_aux (E_exit e',(l,(Base(([],expect_t),Emp_local,[],pure_e)))),expect_t,t_env,[],pure_e)
| E_internal_cast _ | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t * effect) =
@@ -1426,6 +1430,84 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
(FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)))
+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 i = id_to_string id in
+ (match Envmap.apply t_env i with
+ | Some(Base(([],t), External (Some j), [], _)) ->
+ let t,_ = get_abbrev d_env t in
+ let t_actual,t_id = match t.t with
+ | Tabbrev(i,t) -> t,i
+ | _ -> t,t in
+ (match t_actual.t with
+ | Tapp("register",[TA_typ t']) ->
+ if i = j then (i,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
+ (match reg_t.t with
+ | Tid i ->
+ (match lookup_record_typ i d_env.rec_env with
+ | None -> typ_error l ("Expected a register with bit fields, given " ^ i)
+ | Some(((i,rec_kind,fields) as r)) ->
+ let fi = id_to_string subreg in
+ (match lookup_field_type fi r with
+ | NoTyp -> typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
+ | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
+ | Base(([],et),tag,cs,ef) ->
+ let tannot = Base(([],et),Alias,[],pure_e) in
+ let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg,tannot))} in
+ (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 (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]) ->
+ match (base.nexp,len.nexp,order.order, bit) with
+ | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll))) ->
+ if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k
+ then let tannot = Base(([],item_t),Alias,[],pure_e) in
+ let d_env =
+ {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg,tannot))} in
+ (AL_aux(AL_bit(reg_a,(E_aux(bit,(le,eannot)))), (l,tannot)), tannot,d_env)
+ 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 (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
+ | Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
+ match (base.nexp,len.nexp,order.order, sl1,sl2) with
+ | (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll)),E_lit (L_aux((L_num k2), ll2))) ->
+ if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k2 && k < k2
+ then let t = {t = Tapp("vector",[TA_nexp (int_to_nexp k);TA_nexp (int_to_nexp ((k2-k) +1));
+ TA_ord order; TA_typ item_t])} in
+ let tannot = Base(([],t),Alias,[],pure_e) in
+ let d_env =
+ {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg,tannot))} in
+ (AL_aux(AL_slice(reg_a,(E_aux(sl1,(le1,eannot1))),(E_aux(sl2,(le2,eannot2)))),
+ (l,tannot)), tannot,d_env)
+ 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
+ (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])) ->
+ let _ = type_consistent (Specc l) d_env item_t item_t2 in
+ let t = {t= Tapp("vector",[TA_nexp b1; TA_nexp {nexp = Nadd(r,r2)}; TA_ord {order = Oinc}; TA_typ item_t])} in
+ let tannot = Base(([],t),Alias,[],pure_e) in
+ let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (reg1,tannot))} in
+ (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env))
+
(*val check_def : envs -> tannot def -> (tannot def) envs_out*)
let check_def envs def =
let (Env(d_env,t_env)) = envs in
@@ -1445,6 +1527,15 @@ let check_def envs def =
let i = id_to_string id in
let tannot = into_register d_env (Base(([],t),External (Some i),[],pure_e)) in
(DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
+ | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) ->
+ let i = id_to_string id in
+ let (aspec,tannot,d_env) = check_alias_spec envs i aspec None in
+ (DEF_reg_dec(DEC_aux(DEC_alias(id,aspec),(l,tannot))),(Env(d_env, Envmap.insert t_env (i,tannot))))
+ | DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) ->
+ let i = id_to_string id in
+ let t = typ_to_t typ in
+ let (aspec,tannot,d_env) = check_alias_spec envs i aspec (Some t) in
+ (DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
| DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 08eddc3f..880d317a 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -74,6 +74,7 @@ type tag =
| Default
| Constructor
| Enum
+ | Alias
| Spec
type constraint_origin =
@@ -98,7 +99,6 @@ type tannot =
| Base of (t_params * t) * tag * nexp_range list * effect
| Overload of tannot * bool * tannot list (* First tannot is the most polymorphic version; the boolean indicates whether the overloaded functions can use the return type; the list includes all variants. All t to be Tfn *)
-(*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*)
type 'a emap = 'a Envmap.t
type rec_kind = Record | Register
@@ -109,6 +109,7 @@ type def_envs = {
namesch : tannot emap;
enum_env : (string list) emap;
rec_env : rec_env list;
+ alias_env : (string * tannot) emap;
}
type exp = tannot Ast.exp
@@ -193,6 +194,7 @@ let tag_to_string = function
| Default -> "Default"
| Constructor -> "Constructor"
| Enum -> "Enum"
+ | Alias -> "Alias"
| Spec -> "Spec"
let rec tannot_to_string = function
@@ -496,6 +498,8 @@ let rec normalize_nexp n =
| Nneg _,_ | _,Nneg _ -> let _ = Printf.printf "neg case still around %s\n" (n_to_string n) in assert false (* If things are normal, neg should be gone. *)
)
+let int_to_nexp i = {nexp = Nconst (big_int_of_int i)}
+
let v_count = ref 0
let t_count = ref 0
let tuvars = ref []
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 7ddb082f..063ee088 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -70,6 +70,7 @@ type tag =
| Default
| Constructor
| Enum
+ | Alias
| Spec
type constraint_origin =
@@ -106,6 +107,7 @@ type def_envs = {
namesch : tannot emap;
enum_env : (string list) emap;
rec_env : rec_env list;
+ alias_env : (string * tannot) emap;
}
type exp = tannot Ast.exp
@@ -131,6 +133,8 @@ val t_to_string : t -> string
val tannot_to_string : tannot -> string
val t_to_typ : t -> Ast.typ
+val int_to_nexp : int -> nexp
+
val reset_fresh : unit -> unit
val new_t : unit -> t
val new_n : unit -> nexp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 05:59:21 +0000