summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml1
-rw-r--r--src/bitfield.ml79
-rw-r--r--src/initial_check.ml52
-rw-r--r--src/initial_check.mli1
-rw-r--r--src/lexer2.mll1
-rw-r--r--src/parse_ast.ml3
-rw-r--r--src/parser.mly2
-rw-r--r--src/parser2.mly29
-rw-r--r--src/pretty_print_lem.ml34
-rw-r--r--src/pretty_print_lem_ast.ml8
-rw-r--r--src/pretty_print_sail.ml10
-rw-r--r--src/rewrites.ml50
-rw-r--r--src/spec_analysis.ml4
-rw-r--r--src/type_check.ml52
14 files changed, 196 insertions, 130 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 7e966bf2..e502f86f 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -726,6 +726,7 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
| LEXP_vector_range (lexp, e1, e2) -> rewrap (E_vector_subrange (lexp_to_exp lexp, e1, e2))
| LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id))
| LEXP_memory (id, exps) -> rewrap (E_app (id, exps))
+ | LEXP_deref exp -> rewrap (E_app (mk_id "reg_deref", [exp]))
let destruct_range (Typ_aux (typ_aux, _)) =
match typ_aux with
diff --git a/src/bitfield.ml b/src/bitfield.ml
new file mode 100644
index 00000000..0a32654d
--- /dev/null
+++ b/src/bitfield.ml
@@ -0,0 +1,79 @@
+
+module Big_int = Nat_big_num
+
+open Initial_check
+open Ast
+open Ast_util
+
+let bitvec size order =
+ Printf.sprintf "vector(%i, %s, bit)" size (string_of_order order)
+
+let rec combine = function
+ | [] -> Defs []
+ | (Defs defs) :: ast ->
+ let (Defs defs') = combine ast in
+ Defs (defs @ defs')
+
+let newtype name size order =
+ let nt = Printf.sprintf "newtype %s = Mk_%s : %s" name name (bitvec size order) in
+ ast_of_def_string order nt
+
+let full_getter name size order =
+ let fg_val = Printf.sprintf "val _get_%s : %s -> %s" name name (bitvec size order) in
+ let fg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v" name name in
+ combine [ast_of_def_string order fg_val; ast_of_def_string order fg_function]
+
+let full_setter name size order =
+ let fs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" name name (bitvec size order) in
+ let fs_function = String.concat "\n"
+ [ Printf.sprintf "function _set_%s (r_ref, v) = {" name;
+ " r = _reg_deref(r_ref);";
+ Printf.sprintf " r = Mk_%s(v);" name;
+ " (*r_ref) = r";
+ "}"
+ ]
+ in
+ combine [ast_of_def_string order fs_val; ast_of_def_string order fs_function]
+
+let full_overload name order =
+ ast_of_def_string order (Printf.sprintf "overload _mod_bits = {_get_%s, _set_%s}" name name)
+
+let full_accessor name size order =
+ combine [full_getter name size order; full_setter name size order; full_overload name order]
+
+let index_range_getter' name field order start stop =
+ let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+ let irg_val = Printf.sprintf "val _get_%s : %s -> %s" field name (bitvec size order) in
+ let irg_function = Printf.sprintf "function _get_%s Mk_%s(v) = v[%i .. %i]" field name start stop in
+ combine [ast_of_def_string order irg_val; ast_of_def_string order irg_function]
+
+let index_range_setter' name field order start stop =
+ let size = if start > stop then start - (stop - 1) else stop - (start - 1) in
+ let irs_val = Printf.sprintf "val _set_%s : (register(%s), %s) -> unit effect {wreg}" field name (bitvec size order) in
+ let irs_function = String.concat "\n"
+ [ Printf.sprintf "function _set_%s (r_ref, v) = {" field;
+ Printf.sprintf " r = _get_%s(_reg_deref(r_ref));" name;
+ Printf.sprintf " r[%i .. %i] = v;" start stop;
+ Printf.sprintf " (*r_ref) = Mk_%s(r)" name;
+ "}"
+ ]
+ in
+ combine [ast_of_def_string order irs_val; ast_of_def_string order irs_function]
+
+let index_range_overload field order =
+ ast_of_def_string order (Printf.sprintf "overload _mod_%s = {_get_%s, _set_%s}" field field field)
+
+let index_range_accessor name field order (BF_aux (bf_aux, l)) =
+ let getter n m = index_range_getter' name field order (Big_int.to_int n) (Big_int.to_int m) in
+ let setter n m = index_range_setter' name field order (Big_int.to_int n) (Big_int.to_int m) in
+ let overload = index_range_overload field order in
+ match bf_aux with
+ | BF_single n -> combine [getter n n; setter n n; overload]
+ | BF_range (n, m) -> combine [getter n m; setter n m; overload]
+ | BF_concat _ -> failwith "Unimplemented"
+
+let field_accessor name order (id, ir) = index_range_accessor name (string_of_id id) order ir
+
+let macro id size order ranges =
+ let name = string_of_id id in
+ combine ([newtype name size order; full_accessor name size order] @ List.map (field_accessor name order) ranges)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 0cea64a1..52ed1da1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -691,13 +691,12 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_de
let td_enum = TD_aux(TD_enum(id,to_ast_namescm name_scm_opt,enums,false),(l,())) in (* Add check that all enums have unique names *)
let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
td_enum, (names,k_env,def_ord)
- | Parse_ast.TD_register(id,t1,t2,ranges) ->
+ | Parse_ast.TD_bitfield(id,typ,ranges) ->
let id = to_ast_id id in
let key = id_to_string id in
- let n1 = to_ast_nexp k_env t1 in
- let n2 = to_ast_nexp k_env t2 in
- let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in
- TD_aux(TD_register(id,n1,n2,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
+ let typ = to_ast_typ k_env def_ord typ in
+ let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in
+ TD_aux(TD_bitfield(id,typ,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def) envs_out =
match td with
@@ -1000,25 +999,34 @@ let undefined_typschm id typq =
let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in
mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef])))
+let have_undefined_builtins = ref false
+
let generate_undefineds vs_ids (Defs defs) =
let gen_vs id str =
if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
in
- let undefined_builtins = List.concat
- [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
- gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
- gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
- gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
- gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}";
- gen_vs (mk_id "undefined_real") "unit -> real effect {undef}";
- gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
- gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
- gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
- (* FIXME: How to handle inc/dec order correctly? *)
- gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type). (atom('n), 'a) -> vector('n, dec,'a) effect {undef}";
- (* Only used with lem_mwords *)
- gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
- gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+ let undefined_builtins =
+ if !have_undefined_builtins then
+ []
+ else
+ begin
+ have_undefined_builtins := true;
+ List.concat
+ [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
+ gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
+ gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
+ gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
+ gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}";
+ gen_vs (mk_id "undefined_real") "unit -> real effect {undef}";
+ gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
+ gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
+ gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
+ (* FIXME: How to handle inc/dec order correctly? *)
+ gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type). (atom('n), 'a) -> vector('n, dec,'a) effect {undef}";
+ (* Only used with lem_mwords *)
+ gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+ gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
+ end
in
let undefined_tu = function
| Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
@@ -1088,3 +1096,7 @@ let process_ast order defs =
let ast = generate_undefineds vs_ids ast in
generate_initialize_registers vs_ids ast
end
+
+let ast_of_def_string order str =
+ let def = Parser2.def_eof Lexer2.token (Lexing.from_string str) in
+ process_ast order (Defs [def])
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 6059b0ac..9d1e0d30 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -54,6 +54,7 @@ open Ast_util
val opt_undefined_gen : bool ref
val opt_magic_hash : bool ref
+val ast_of_def_string : order -> string -> unit defs
val process_ast : order -> Parse_ast.defs -> unit defs
val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/lexer2.mll b/src/lexer2.mll
index e24de0d0..3a1f7066 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -155,6 +155,7 @@ let kw_table =
("while", (fun _ -> While));
("do", (fun _ -> Do));
("mutual", (fun _ -> Mutual));
+ ("bitfield", (fun _ -> Bitfield));
("barr", (fun x -> Barr));
("depend", (fun x -> Depend));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index e84e8a60..362333f3 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -429,8 +429,7 @@ type_def_aux = (* Type definition body *)
| TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
| TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
| TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
+ | TD_bitfield of id * atyp * (id * index_range) list (* register mutable bitfield type definition *)
type
val_spec_aux = (* Value type specification *)
diff --git a/src/parser.mly b/src/parser.mly
index 43dc0a74..d2a5933a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1247,8 +1247,6 @@ type_def:
{ tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
| Typedef tid name_sect Eq Enumerate Lcurly enum_body Rcurly
{ tdloc (TD_enum($2,$3,$7,false)) }
- | Typedef tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
- { tdloc (TD_register($2, $7, $9, $12)) }
default_typ:
| Default atomic_kind tyvar
diff --git a/src/parser2.mly b/src/parser2.mly
index 521da6f8..7af70687 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -93,6 +93,7 @@ let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m
let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m)
let mk_nc nc n m = NC_aux (nc, loc n m)
let mk_sd s n m = SD_aux (s, loc n m)
+let mk_ir r n m = BF_aux (r, loc n m)
let mk_funcl f n m = FCL_aux (f, loc n m)
let mk_fun fn n m = FD_aux (fn, loc n m)
@@ -154,7 +155,7 @@ let rec desugar_rchain chain s e =
%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
%token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast
%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
%token Repeat Until While Do Record Mutual Var Ref
@@ -185,8 +186,10 @@ let rec desugar_rchain chain s e =
%start file
%start typschm_eof
%start exp_eof
+%start def_eof
%type <Parse_ast.typschm> typschm_eof
%type <Parse_ast.exp> exp_eof
+%type <Parse_ast.def> def_eof
%type <Parse_ast.defs> file
%%
@@ -1045,6 +1048,24 @@ funcls:
| id funcl_patexp And funcls
{ mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4 }
+index_range:
+ | Num
+ { mk_ir (BF_single $1) $startpos $endpos }
+ | Num DotDot Num
+ { mk_ir (BF_range ($1, $3)) $startpos $endpos }
+
+r_id_def:
+ | id Colon index_range
+ { $1, $3 }
+
+r_def_body:
+ | r_id_def
+ { [$1] }
+ | r_id_def Comma
+ { [$1] }
+ | r_id_def Comma r_def_body
+ { $1 :: $3 }
+
type_def:
| Typedef id typquant Eq typ
{ mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
@@ -1066,6 +1087,8 @@ type_def:
{ mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
| Union id typquant Eq Lcurly type_unions Rcurly
{ mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+ | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly
+ { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos }
enum_bar:
| id
@@ -1197,6 +1220,10 @@ defs_list:
| def defs_list
{ $1::$2 }
+def_eof:
+ | def Eof
+ { $1 }
+
defs:
| defs_list
{ (Defs $1) }
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 8f789c14..a79ae0eb 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1150,36 +1150,6 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
fromInterpValuePP ^^ hardline ^^ hardline ^^
fromToInterpValuePP ^^ hardline
else empty)
- | TD_register(id,n1,n2,rs) ->
- match n1, n2 with
- | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
- let dir_b = i1 < i2 in
- let dir = (if dir_b then "true" else "false") in
- let dir_suffix = (if dir_b then "_inc" else "_dec") in
- let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
- let size = if dir_b then Big_int.add (Big_int.sub i2 i1) (Big_int.of_int 1) else Big_int.add (Big_int.sub i1 i2) (Big_int.of_int 1) in
- let vtyp = vector_typ (nconstant size) ord bit_typ in
- let tannot = doc_tannot_lem sequential mwords false vtyp in
- let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
- doc_range_lem r;]) in
- let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
- doc_op equals
- (concat [string "type";space;doc_id_lem id])
- (doc_typ_lem sequential mwords vtyp)
- ^^ hardline ^^
- doc_op equals
- (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"])
- (string "reg")
- ^^ hardline ^^
- doc_op equals
- (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"])
- (string "reg")
- ^^ hardline ^^
- doc_op equals
- (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
- (string "Register" ^^ space ^^
- align (separate space [string "regname"; doc_int size; doc_int i1; string dir;
- break 0 ^^ brackets (align doc_rids)]))
| _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
let doc_rec_lem (Rec_aux(r,_)) = match r with
@@ -1354,7 +1324,8 @@ let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) =
(* | VS_val_spec (_,_,Some _,_) -> empty *)
| _ -> empty
-let find_regtypes defs =
+let find_regtypes defs = []
+ (*
List.fold_left
(fun acc def ->
match def with
@@ -1362,6 +1333,7 @@ let find_regtypes defs =
(tname, (n1, n2, fields)) :: acc
| _ -> acc
) [] defs
+ *)
let is_field_accessor regtypes fdef =
let is_field_of regtyp field =
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 176fcd2e..d42cd2a5 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -526,11 +526,11 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
- | TD_register(id,n1,n2,rs) ->
- let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
+ | TD_bitfield(id,typ,rs) ->
+ let pp_rid ppf (id, r) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
let pp_rids = (list_pp pp_rid pp_rid) in
- fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
- kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
+ fprintf ppf "@[<0>(%a %a %a [%a])@]"
+ kwd "TD_bitfield" pp_lem_id id pp_lem_typ typ pp_rids rs
in
fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 30eb71e0..38b9e134 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -432,16 +432,6 @@ let doc_typdef (TD_aux(td,_)) = match td with
doc_op equals
(concat [string "typedef"; space; doc_id id; doc_namescm nm])
(string "enumerate" ^^ space ^^ braces enums_doc)
- | TD_register(id,n1,n2,rs) ->
- let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in
- let doc_rids = group (separate_map (break 1) doc_rid rs) in
- doc_op equals
- (string "typedef" ^^ space ^^ doc_id id)
- (separate space [
- string "register bits";
- brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2);
- braces doc_rids;
- ])
let doc_kindef (KD_aux(kd,_)) = match kd with
| KD_nabbrev(kind,id,nm,n) ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 9b97b88b..2ecaf91d 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1527,46 +1527,8 @@ let rewrite_register_ref_writes (Defs defs) =
| None -> E_assign (lexp, exp) in
let rewrite_exp _ = fold_exp { id_exp_alg with e_assign = e_assign } in
- let generate_field_accessors l env id n1 n2 fields =
- let i1, i2 = match n1, n2 with
- | Nexp_aux(Nexp_constant i1, _),Nexp_aux(Nexp_constant i2, _) -> i1, i2
- | _ -> raise (Reporting_basic.err_typ l
- ("Non-constant indices in register type " ^ string_of_id id)) in
- let dir_b = i1 < i2 in
- let dir = (if dir_b then "true" else "false") in
- let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
- let size = if dir_b then Big_int.succ (Big_int.sub i2 i1) else Big_int.succ (Big_int.sub i1 i2) in
- let rtyp = mk_id_typ id in
- let vtyp = vector_typ (nconstant size) ord bit_typ in
- let accessors (fr, fid) =
- let i, j = match fr with
- | BF_aux (BF_single i, _) -> (i, i)
- | BF_aux (BF_range (i, j), _) -> (i, j)
- | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in
- let mk_num_exp i = mk_lit_exp (L_num i) in
- let reg_pat, reg_env = bind_pat env (mk_pat (P_typ (rtyp, mk_pat (P_id (mk_id "reg"))))) rtyp in
- let inferred_get = infer_exp reg_env (mk_exp (E_vector_subrange
- (mk_exp (E_id (mk_id "reg")), mk_num_exp i, mk_num_exp j))) in
- let ftyp = typ_of inferred_get in
- let v_pat, v_env = bind_pat reg_env (mk_pat (P_typ (ftyp, mk_pat (P_id (mk_id "v"))))) ftyp in
- let inferred_set = infer_exp v_env (mk_exp (E_vector_update_subrange
- (mk_exp (E_id (mk_id "reg")), mk_num_exp i, mk_num_exp j, mk_exp (E_id (mk_id "v"))))) in
- let set_args = P_aux (P_tup [reg_pat; v_pat], (l, Some (env, tuple_typ [rtyp; ftyp], no_effect))) in
- let fsuffix = "_" ^ string_of_id id ^ "_" ^ string_of_id fid in
- let rec_opt = Rec_aux (Rec_nonrec, l) in
- let tannot ret_typ = Typ_annot_opt_aux (Typ_annot_opt_some (TypQ_aux (TypQ_tq [], l), ret_typ), l) in
- let eff_opt = Effect_opt_aux (Effect_opt_pure, l) in
- let mk_funcl id pat exp = FCL_aux (FCL_Funcl (mk_id id, Pat_aux (Pat_exp (pat, exp),(l,None))), (l, None)) in
- let mk_fundef id pat exp ret_typ = DEF_fundef (FD_aux (FD_function (rec_opt, tannot ret_typ, eff_opt, [mk_funcl id pat exp]), (l, None))) in
- [mk_fundef ("get" ^ fsuffix) reg_pat inferred_get ftyp;
- mk_fundef ("set" ^ fsuffix) set_args inferred_set (typ_of inferred_set)] in
- List.concat (List.map accessors fields) in
-
let rewriters = { rewriters_base with rewrite_exp = rewrite_exp } in
let rec rewrite ds = match ds with
- | (DEF_type (TD_aux (TD_register (id, n1, n2, fields), (l, Some (env, _, _)))) as d) :: ds ->
- let (Defs d), env = check env (Defs [d]) in
- d @ (generate_field_accessors l env id n1 n2 fields) @ rewrite ds
| d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds)
| [] -> [] in
Defs (rewrite (write_reg_spec @ defs))
@@ -1883,7 +1845,7 @@ let rewrite_type_def_typs rw_typ rw_typquant rw_typschm (TD_aux (td, annot)) =
| TD_variant (id, nso, typq, tus, flag) ->
TD_aux (TD_variant (id, nso, rw_typquant typq, List.map (rewrite_type_union_typs rw_typ) tus, flag), annot)
| TD_enum (id, nso, ids, flag) -> TD_aux (TD_enum (id, nso, ids, flag), annot)
- | TD_register (id, n1, n2, ranges) -> TD_aux (TD_register (id, n1, n2, ranges), annot)
+ | TD_bitfield _ -> assert false (* Processed before re-writing *)
(* FIXME: other reg_dec types *)
let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) =
@@ -2146,8 +2108,8 @@ let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list
match l with
| [] -> k []
| exp :: exps -> f exp (fun exp -> mapCont f exps (fun exps -> k (exp :: exps)))
-
-let rewrite_defs_letbind_effects =
+
+let rewrite_defs_letbind_effects =
let rec value ((E_aux (exp_aux,_)) as exp) =
not (effectful exp || updates_vars exp)
@@ -2169,7 +2131,7 @@ let rewrite_defs_letbind_effects =
and n_fexp (fexp : 'a fexp) (k : 'a fexp -> 'a exp) : 'a exp =
let (FE_aux (FE_Fexp (id,exp),annot)) = fexp in
- n_exp_name exp (fun exp ->
+ n_exp_name exp (fun exp ->
k (fix_eff_fexp (FE_aux (FE_Fexp (id,exp),annot))))
and n_fexpL (fexps : 'a fexp list) (k : 'a fexp list -> 'a exp) : 'a exp =
@@ -2209,6 +2171,9 @@ let rewrite_defs_letbind_effects =
let (LEXP_aux (lexp_aux,annot)) = lexp in
match lexp_aux with
| LEXP_id _ -> k lexp
+ | LEXP_deref exp ->
+ n_exp exp (fun exp ->
+ k (fix_eff_lexp (LEXP_aux (LEXP_deref exp, annot))))
| LEXP_memory (id,es) ->
n_exp_nameL es (fun es ->
k (fix_eff_lexp (LEXP_aux (LEXP_memory (id,es),annot))))
@@ -2254,6 +2219,7 @@ let rewrite_defs_letbind_effects =
| E_block es -> failwith "E_block should have been removed till now"
| E_nondet _ -> failwith "E_nondet not supported"
| E_id id -> k exp
+ | E_ref id -> k exp
| E_lit _ -> k exp
| E_cast (typ,exp') ->
n_exp_name exp' (fun exp' ->
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index b9affe12..3d3b13e3 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -432,8 +432,8 @@ let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
typ_variants consider_var bindings tunions
| TD_enum(id,_,ids,_) ->
Nameset.of_list (List.map string_of_id (id::ids)),mt
- | TD_register(id,n1,n2,_) ->
- init_env (string_of_id id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2
+ | TD_bitfield(id,typ,_) ->
+ init_env (string_of_id id), Nameset.empty (* fv_of_typ consider_var mt typ *)
let fv_of_tannot_opt consider_var (Typ_annot_opt_aux (t,_)) =
match t with
diff --git a/src/type_check.ml b/src/type_check.ml
index 0c1d55ce..3269de1d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3453,32 +3453,50 @@ let mk_synonym typq typ =
^ " in type synonym " ^ string_of_typ typ
^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
-let check_typedef env (TD_aux (tdef, (l, _))) =
+let check_kinddef env (KD_aux (kdef, (l, _))) =
+ let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
+ match kdef with
+ | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_nat, _)]),_) as kind), id, nmscm, nexp) ->
+ [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
+ Env.add_num_def id nexp env
+ | _ -> kd_err ()
+
+let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
+ fun env (TD_aux (tdef, (l, _))) ->
let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Typedef") in
match tdef with
- | TD_abbrev(id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) ->
+ | TD_abbrev (id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ) env
- | TD_record(id, nmscm, typq, fields, _) ->
+ | TD_record (id, nmscm, typq, fields, _) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env
- | TD_variant(id, nmscm, typq, arms, _) ->
+ | TD_variant (id, nmscm, typq, arms, _) ->
let env =
env
|> Env.add_variant id (typq, arms)
|> (fun env -> List.fold_left (fun env tu -> check_type_union env id typq tu) env arms)
in
[DEF_type (TD_aux (tdef, (l, None)))], env
- | TD_enum(id, nmscm, ids, _) ->
+ | TD_enum (id, nmscm, ids, _) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_enum id ids env
+ | TD_bitfield (id, typ, ranges) ->
+ let typ = Env.expand_synonyms env typ in
+ begin
+ match typ with
+ (* The type of a bitfield must be a constant-width bitvector *)
+ | Typ_aux (Typ_app (v, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant size, _)), _);
+ Typ_arg_aux (Typ_arg_order order, _);
+ Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id b, _)), _)]), _)
+ when string_of_id v = "vector" && string_of_id b = "bit" ->
+ let size = Big_int.to_int size in
+ let (Defs defs), env = check' env (Bitfield.macro id size order ranges) in
+ defs, env
+ | _ ->
+ typ_error l "Bad bitfield type"
+ end
+ | _ -> td_err ()
-let check_kinddef env (KD_aux (kdef, (l, _))) =
- let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
- match kdef with
- | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_nat, _)]),_) as kind), id, nmscm, nexp) ->
- [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
- Env.add_num_def id nexp env
- | _ -> kd_err ()
-
-let rec check_def env def =
+and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
+ fun env def ->
let cd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Case") in
match def with
| DEF_kind kdef -> check_kinddef env kdef
@@ -3507,7 +3525,8 @@ let rec check_def env def =
let defs, env = check_def env def
in List.map (fun def -> DEF_comm (DC_comm_struct def)) defs, env
-let rec check' env (Defs defs) =
+and check' : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+ fun env (Defs defs) ->
match defs with
| [] -> (Defs []), env
| def :: defs ->
@@ -3515,7 +3534,8 @@ let rec check' env (Defs defs) =
let (Defs defs, env) = check' env (Defs defs) in
(Defs (def @ defs)), env
-let check env defs =
+let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+ fun env defs ->
try check' env defs with
| Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:34:45 +0000