diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/power_extras.lem | 11 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 40 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 34 | ||||
| -rw-r--r-- | src/gen_lib/vector.lem | 24 | ||||
| -rw-r--r-- | src/pretty_print.ml | 247 | ||||
| -rw-r--r-- | src/process_file.ml | 6 | ||||
| -rw-r--r-- | src/rewriter.ml | 13 |
7 files changed, 225 insertions, 150 deletions
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem index f2941aff..8515a406 100644 --- a/src/gen_lib/power_extras.lem +++ b/src/gen_lib/power_extras.lem @@ -1,4 +1,5 @@ open import Pervasives +open import Vector open import State open import Sail_values @@ -33,3 +34,13 @@ let H_Sync () = return () let LW_Sync () = return () let EIEIO_Sync () = return () +let recalculate_dependency () = return () + +let trap () = () +(* this needs to change, but for that we'd have to make the type checker know about trap + * as an effect *) + +val countLeadingZeroes : vector bit * integer -> integer +let countLeadingZeroes (V bits _ _ ,n) = + let (_,bits) = List.splitAt (natFromInteger n) bits in + integerFromNat (List.length (takeWhile ((=) O) bits)) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index b02e47cb..481a4e5b 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -25,6 +25,10 @@ let (~) = bitwise_not_bit let bitwise_not (V bs start is_inc) = V (List.map bitwise_not_bit bs) start is_inc +val is_one : integer -> bit +let is_one i = + if i = 1 then I else O + let bool_to_bit b = if b then I else O let bitwise_binop_bit op = function @@ -106,15 +110,15 @@ let rec divide_by_2 bs (i : integer) (n : integer) = then bs else if (n mod 2 = 1) - then divide_by_2 (replace bs (natFromInteger i,I)) (i - 1) (n / 2) + then divide_by_2 (replace bs (i,I)) (i - 1) (n / 2) else divide_by_2 bs (i-1) (n div 2) let rec add_one_bit bs co (i : integer) = if i < 0 then bs else match (nth bs i,co) with - | (O,false) -> replace bs (natFromInteger i,I) - | (O,true) -> add_one_bit (replace bs (natFromInteger i,I)) true (i-1) - | (I,false) -> add_one_bit (replace bs (natFromInteger i,O)) true (i-1) + | (O,false) -> replace bs (i,I) + | (O,true) -> add_one_bit (replace bs (i,I)) true (i-1) + | (I,false) -> add_one_bit (replace bs (i,O)) true (i-1) | (I,true) -> add_one_bit bs true (i-1) | _ -> failwith "add_one_bit applied to list with undefined bit" (* | Vundef,_ -> assert false*) @@ -218,6 +222,8 @@ let add_VII = arith_op_vec_range_range integerAdd false let addS_VII = arith_op_vec_range_range integerAdd true let minus_VII = arith_op_vec_range_range integerMinus false + + let arith_op_vec_vec_range op sign l r = let (l',r') = (to_num sign l,to_num sign r) in op l' r' @@ -270,7 +276,7 @@ let minusO_VVV = arith_op_overflow_vec integerMinus false 1 let minusSO_VVV = arith_op_overflow_vec integerMinus true 1 let multO_VVV = arith_op_overflow_vec integerMult false 2 let multSO_VVV = arith_op_overflow_vec integerMult true 2 - + let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) (V _ _ is_inc as l) r_bit = let act_size = length l * size in @@ -373,7 +379,7 @@ let arith_op_overflow_no0_vec op sign size (((V _ start is_inc) as l),r) = let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1 let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1 -let arith_op_vec_range_no0 op sign size ((V _ _ is_inc as l),r) = +let arith_op_vec_range_no0 op sign size (V _ _ is_inc as l) r = arith_op_vec_no0 op sign size (l,to_vec is_inc (length l,r)) let mod_VIV = arith_op_vec_range_no0 integerMod false 1 @@ -438,3 +444,25 @@ let EXTS (v1,(V _ _ is_inc as v)) = to_vec is_inc (v1,signed v) let EXTZ = EXTS + +val make_indexed_vector_reg : list (integer * register) -> maybe register -> integer -> integer -> + vector register +let make_indexed_vector_reg entries default start length = + let length = natFromInteger length in + match default with + | Just v -> V (List.foldl replace (replicate length v) entries) start defaultDir + | Nothing -> failwith "make_indexed_vector used without default value" + end + +val make_indexed_vector_bit : list (integer * bit) -> maybe bit -> integer -> integer -> vector bit +let make_indexed_vector_bit entries default start length = + let length = natFromInteger length in + let default = match default with Nothing -> Undef | Just v -> v end in + V (List.foldl replace (replicate length default) entries) start defaultDir + +val make_bit_vector_undef : integer -> vector bit +let make_bitvector_undef length = + V (replicate (natFromInteger length) Undef) 0 true + + +let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 7777cf5e..f79f8eff 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -128,8 +128,8 @@ let rec foreach_dec (i,stop,by) vars body = else ((),vars) -val foreachM_inc : forall 's 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) +val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) let rec foreachM_inc (i,stop,by) vars body = if i <= stop then @@ -138,8 +138,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return ((),vars) -val foreachM_dec : forall 's 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) +val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) let rec foreachM_dec (i,stop,by) vars body = if i >= stop then @@ -153,11 +153,24 @@ let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfie val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield) -val read_reg_field_bit : forall 'e. register -> register_field_bit -> M state 'e bit -let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit) +val read_reg_bitfield : forall 'e. register -> register_bitfield -> M state 'e bit +let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit) + +val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M state 'e unit +let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit) + +val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer -> + vector bit -> M state 'e unit +let write_reg_field_range reg rfield i j v = + let (i',j') = field_indices rfield in + write_reg_range reg i' j' v + +val write_reg_field_bit : forall 'e. register -> register_field -> integer -> + bit -> M state 'e unit +let write_reg_field_bit reg rfield i v = + let (i',_) = field_indices rfield in + write_reg_bit reg (i + i') v -val write_reg_field_bit : forall 'e. register -> register_field_bit -> bit -> M state 'e unit -let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit) let length l = integerFromNat (length l) @@ -172,3 +185,8 @@ let write_two_regs r1 r2 vec = (if defaultDir then size - start else start - size) (if defaultDir then vsize - start else start - vsize) in write_reg r1 r1_v >> write_reg r2 r2_v + +let read_two_regs r1 r2 = + read_reg r1 >>= fun v1 -> + read_reg r2 >>= fun v2 -> + return (v1 ^^ v2) diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem index ad0ba1db..4044e23c 100644 --- a/src/gen_lib/vector.lem +++ b/src/gen_lib/vector.lem @@ -18,25 +18,15 @@ let to_bool = function let get_start (V _ s _) = s let length (V bs _ _) = length bs -let rec replace bs ((n : nat),b') = match (n,bs) with - | (_, []) -> [] - | (0, _::bs) -> b' :: bs - | (n+1, b::bs) -> b :: replace bs (n,b') +let rec replace bs ((n : integer),b') = match bs with + | [] -> [] + | b :: bs -> + if n = 0 then + b' :: bs + else + b :: replace bs (n - 1,b') end -let make_indexed_vector_reg entries default start length = - match default with - | Just v -> V (List.foldl replace (replicate length v) entries) start - | Nothing -> failwith "make_indexed_vector used without default value" - end - -let make_indexed_vector_bit entries default start length = - let default = match default with Nothing -> Undef | Just v -> v end in - V (List.foldl replace (replicate length default) entries) start - -let make_bitvector_undef length = - V (replicate length Undef) 0 true - let vector_concat (V bs start is_inc) (V bs' _ _) = V (bs ++ bs') start is_inc diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 1e8f185c..b9b32ac4 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1443,7 +1443,7 @@ let doc_exp_ocaml, doc_let_ocaml = else doc_id_ocaml id | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_ocaml_ctor i id | Base((_,t),Alias alias_info,_,_,_,_) -> - (match alias_info with + (match alias_info with | Alias_field(reg,field) -> let field_f = match t.t with | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "get_register_field_bit" @@ -1943,12 +1943,13 @@ let doc_pat_lem apat_needed = | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in lem*) in pat +let rec getregtyp_annot (Base ((_,t),_,_,_,_,_)) = + match t with + | {t = Tabbrev ({t = Tid name},_)} -> name + let rec getregtyp (LEXP_aux (le,(_,annot))) = match le with | LEXP_id _ - | LEXP_cast _ -> - let (Base ((_,t),_,_,_,_,_)) = annot in - (match t with - | {t = Tabbrev ({t = Tid name},_)} -> name) + | LEXP_cast _ -> getregtyp_annot annot | LEXP_memory _ -> failwith "This lexp writes memory" | LEXP_vector (le,_) | LEXP_vector_range (le,_,_) @@ -1962,47 +1963,69 @@ let doc_exp_lem, doc_let_lem = | E_assign((LEXP_aux(le_act,tannot) as le),e) -> (* can only be register writes *) let (_,(Base ((_,{t = t}),tag,_,_,_,_))) = tannot in - let E_aux (_,(_,(Base ((_,{t = et}),_,_,_,_,_)))) = e in - (match tag with - | External _ -> - (match le_act with - | LEXP_vector (le,e2) -> - (prefix 2 1) - (string "write_reg_bit") - (doc_lexp_deref_lem le ^^ space ^^ - exp e2 ^/^ exp e) - | LEXP_vector_range (le,e2,e3) -> + (match le_act, t, tag with + | LEXP_vector_range (le,e2,e3),_,_ -> + (match le with + | LEXP_aux (LEXP_field (le,id), (_,((Base ((_,{t = t}),_,_,_,_,_))))) -> + if t = Tid "bit" then + failwith "indexing a register's (single bit) bitfield not supported" + else + let typprefix = String.uncapitalize (getregtyp le) ^ "_" in + (prefix 2 1) + (string "write_reg_field_range") + (align (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^ + doc_id_lem id ^/^ exp e2 ^/^ exp e3 ^/^ exp e)) + | _ -> (prefix 2 1) (string "write_reg_range") - (align (doc_lexp_deref_lem le ^^ space ^^ - (parens (group (align (exp e2 ^^ comma ^^ break 0 ^^ exp e3)))) ^/^ - exp e)) - | LEXP_field (lexp,id) -> - let typprefix = String.uncapitalize (getregtyp lexp) ^ "_" in - (match et with - | Tid "bit" - | Tabbrev (_,{t=Tid "bit"}) -> - (prefix 2 1) - (string "write_reg_field_bit") - (doc_lexp_deref_lem lexp ^^ space ^^ string typprefix ^^ doc_id_lem id ^/^ - exp e) - | Tapp ("vector",_) - | Tabbrev (_,{t=Tapp ("vector",_)}) -> - (prefix 2 1) - (string "write_reg_field") - (doc_lexp_deref_lem lexp ^^ space ^^ string typprefix ^^ doc_id_lem id ^/^ - exp e) - | _ -> failwith (t_to_string {t = et}) - ) - | (LEXP_id _ | LEXP_cast _) -> + (align (doc_lexp_deref_lem le ^^ space ^^ exp e2 ^/^ exp e3 ^/^ exp e)) + ) + | LEXP_vector (le,e2), (Tid "bit" | Tabbrev (_,{t=Tid "bit"})),_ -> + (match le with + | LEXP_aux (LEXP_field (le,id), (_,((Base ((_,{t = t}),_,_,_,_,_))))) -> + if t = Tid "bit" then + failwith "indexing a register's (single bit) bitfield not supported" + else + let typprefix = String.uncapitalize (getregtyp le) ^ "_" in + (prefix 2 1) + (string "write_reg_field_bit") + (align (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^ + doc_id_lem id ^/^ exp e2 ^/^ exp e)) + | _ -> (prefix 2 1) - (string "write_reg") - (doc_lexp_deref_lem le ^/^ exp e)) - | _ -> - (prefix 2 1) - (string "write_reg") - (doc_lexp_deref_lem le ^/^ exp e) - ) + (string "write_reg_bit") + (doc_lexp_deref_lem le ^^ space ^^ exp e2 ^/^ exp e) + ) + | LEXP_field (le,id), (Tid "bit"| Tabbrev (_,{t=Tid "bit"})), _ -> + let typprefix = String.uncapitalize (getregtyp le) ^ "_" in + (prefix 2 1) + (string "write_reg_bitfield") + (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^ + doc_id_lem id ^/^ exp e) + | LEXP_field (le,id), _, _ -> + let typprefix = String.uncapitalize (getregtyp le) ^ "_" in + (prefix 2 1) + (string "write_reg_field") + (doc_lexp_deref_lem le ^^ space ^^ string typprefix ^^ + doc_id_lem id ^/^ exp e) + | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info -> + (match alias_info with + | Alias_field(reg,field) -> + let f = match t with + | (Tid "bit" | Tabbrev (_,{t=Tid "bit"})) -> + string "write_reg_bitfield" + | _ -> string "write_reg_bitfield" in + (prefix 2 1) + f + (separate space [string reg;string (String.lowercase reg ^ "_" ^ field);exp e]) + (* the type should go instead of the lowercase reg *) + | Alias_pair(reg1,reg2) -> + string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^ + string reg2 ^^ space ^^ exp e) + | _ -> + (prefix 2 1) + (string "write_reg") + (doc_lexp_deref_lem le ^/^ exp e)) | E_vector_append(l,r) -> let epp = align (separate space [exp l;string "^^"] ^/^ exp r) in @@ -2036,22 +2059,26 @@ let doc_exp_lem, doc_let_lem = match vars with | [v] -> v | _ -> parens (separate comma vars) in - (prefix 2 1) - (parens ((separate space) [string loopf;group (exp indices);exp e5])) - (parens - ((prefix 1 1) - (separate space [string "fun";exp id;varspp;arrow]) - (top_exp false body) - ) + parens ( + (prefix 2 1) + ((separate space) [string loopf;group (exp indices);exp e5]) + (parens + ((prefix 1 1) + (separate space [string "fun";exp id;varspp;arrow]) + (top_exp false body) + ) + ) ) | E_aux (E_lit (L_aux (L_unit,_)),_) -> - (prefix 2 1) - (parens ((separate space) [string loopf;group (exp indices);exp e5])) - (parens - ((prefix 1 1) - (separate space [string "fun";exp id;string "_";arrow]) - (top_exp false body) - ) + parens ( + (prefix 2 1) + ((separate space) [string loopf;group (exp indices);exp e5]) + (parens + ((prefix 1 1) + (separate space [string "fun";exp id;string "_";arrow]) + (top_exp false body) + ) + ) ) ) | _ -> @@ -2105,7 +2132,7 @@ let doc_exp_lem, doc_let_lem = let field_f = match annot with | Base((_,{t = Tid "bit"}),_,_,_,_,_) | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> - string "read_reg_field_bit" + string "read_reg_bitfield" | _ -> string "read_reg_field" in let epp = field_f ^^ space ^^ (exp fexp) ^^ space ^^ string (regtyp ^ "_") ^^ doc_id_lem id in @@ -2115,49 +2142,42 @@ let doc_exp_lem, doc_let_lem = | E_block exps -> failwith "Blocks should have been removed till now." | E_nondet exps -> failwith "Nondet blocks not supported." | E_id id -> - (match annot with - | Base((_, ({t = Tapp("reg",_)} | {t=Tabbrev(_,{t=Tapp("reg",_)})})),_,_,_,_,_) -> - doc_id_lem id - | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})),tag,_,_,_,_) -> - (match tag with - | External _ -> separate space [string "read_reg";doc_id_lem id] - | _ -> doc_id_lem id) - | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor aexp_needed id - | Base((_,t),Alias alias_info,_,_,_,_) -> - (match alias_info with - | Alias_field(reg,field) -> - let field_f = match t.t with - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "read_reg_field_bit" - | _ -> string "read_reg_field" in - separate space [field_f; string reg; string_lit (string field)] - | Alias_extract(reg,start,stop) -> - let epp = - if start = stop then - separate space [string "access";string reg;doc_int start] - else - separate space [string "slice"; string reg; doc_int start; doc_int stop] in - if aexp_needed then parens (align epp) else epp - | Alias_pair(reg1,reg2) -> - let epp = separate space [string "vector_concat";string reg1;string reg2] in - if aexp_needed then parens (align epp) else epp - | Alias_extract(reg,start,stop) -> - let epp = - if start = stop then - (separate space) - [string "access";doc_int start; - parens (string "read_reg" ^^ space ^^ string reg)] - else - (separate space) - [string "slice"; doc_int start; doc_int stop; - parens (string "read_reg" ^^ space ^^ string reg)] in - if aexp_needed then parens (align epp) else epp - | Alias_pair(reg1,reg2) -> - let epp = separate space [string "vector_concat"; - parens (string "read_reg" ^^ space ^^ string reg1); - parens (string "read_reg" ^^ space ^^ string reg2)] in - if aexp_needed then parens (align epp) else epp - ) - | _ -> doc_id_lem id) + (match annot with + | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})), + External _,_,eff,_,_) -> + separate space [string "read_reg";doc_id_lem id] + | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor aexp_needed id + | Base((_,t),Alias alias_info,_,_,_,_) -> + (match alias_info with + | Alias_field(reg,field) -> + let epp = match t.t with + | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> + (separate space) + [string "read_reg_bitfield"; string reg; + string (String.lowercase reg ^ "_" ^ field)] + (* the type should go instead of the lowercase reg *) + | _ -> + (separate space) + [string "read_reg_field"; string reg; + string (String.lowercase reg ^ "_" ^ field)] in + (* the type should go instead of the lowercase reg *) + if aexp_needed then parens (align epp) else epp + | Alias_pair(reg1,reg2) -> + let epp = separate space [string "read_two_regs";string reg1;string reg2] in + if aexp_needed then parens (align epp) else epp + | Alias_extract(reg,start,stop) -> + let epp = + if start = stop then + (separate space) + [string "access";doc_int start; + parens (string "read_reg" ^^ space ^^ string reg)] + else + (separate space) + [string "slice"; doc_int start; doc_int stop; + parens (string "read_reg" ^^ space ^^ string reg)] in + if aexp_needed then parens (align epp) else epp + ) + | _ -> doc_id_lem id) | E_lit lit -> doc_lit_lem false lit | E_cast(typ,e) -> (match annot with @@ -2287,7 +2307,7 @@ let doc_exp_lem, doc_let_lem = | "minus" -> aux "-" | "multiply" -> aux "*" | "quot" -> aux "/" - | "modulo" -> aux "(mod)" + | "modulo" -> aux "mod" | "add_vec" -> aux2 "add_VVV" | "add_vec_signed" -> aux2 "addS_VVV" @@ -2299,6 +2319,7 @@ let doc_exp_lem, doc_let_lem = | "minus_vec_range" -> aux2 "minus_VIV" | "mult_vec_range" -> aux2 "mult_VIV" | "mult_vec_range_signed" -> aux2 "multS_VIV" + | "mod_vec_range" -> aux2 "minus_VIV" | "add_range_vec" -> aux2 "add_IVV" | "add_range_vec_signed" -> aux2 "addS_IVV" | "minus_range_vec" -> aux2 "minus_IVV" @@ -2310,6 +2331,8 @@ let doc_exp_lem, doc_let_lem = | "add_vec_range_range" -> aux2 "add_VII" | "add_vec_range_range_signed" -> aux2 "addS_VII" | "minus_vec_range_range" -> aux2 "minus_VII" + | "add_vec_vec_range" -> aux2 "add_VVI" + | "add_vec_vec_range_signed" -> aux2 "addS_VVI" | "add_vec_bit" -> aux2 "add_VBV" | "add_vec_bit_signed" -> aux2 "addS_VBV" | "minus_vec_bit_signed" -> aux2 "minus_VBV" @@ -2319,6 +2342,8 @@ let doc_exp_lem, doc_let_lem = | "minus_overflow_vec_signed" -> aux2 "minusSO_VVV" | "mult_overflow_vec" -> aux2 "multO_VVV" | "mult_overflow_vec_signed" -> aux2 "multSO_VVV" + | "quot_overflow_vec" -> aux2 "quotO_VVV" + | "quot_overflow_vec_signed" -> aux2 "quot_SO_VVV" | "add_overflow_vec_bit_signed" -> aux2 "addSO_VBV" | "minus_overflow_vec_bit" -> aux2 "minusO_VBV" | "minus_overflow_vec_bit_signed" -> aux2 "minusSO_VBV" @@ -2371,8 +2396,9 @@ let doc_exp_lem, doc_let_lem = | LEXP_vector(le,e) -> parens ((separate space) [string "access";doc_lexp_deref_lem le;top_exp true e]) | LEXP_id id -> doc_id_lem id - | _ -> empty - + | LEXP_cast (typ,id) -> doc_id_lem id + | _ -> + raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen")) (* expose doc_exp_lem and doc_let *) in top_exp, let_exp @@ -2599,7 +2625,7 @@ let reg_decls (Defs defs) = if rsbits = [] then empty else (prefix 2 1) - (separate space [string "let";string "register_field_bit_to_string"; + (separate space [string "let";string "register_bitfield_to_string"; equals;string "function"]) ((separate_map (break 1)) (fun (fname,tname,_) -> @@ -2618,10 +2644,10 @@ let reg_decls (Defs defs) = let regfieldsbit_pp = if rsbits = [] then - string "type register_field_bit = | NO_REGISTER_FIELD_BITS" + string "type register_bitfield = | no_REGISTER_BITFIELDS" else (prefix 2 1) - (separate space [string "type";string "register_field_bit";equals]) + (separate space [string "type";string "register_bitfield";equals]) (separate_map space (fun (fname,tname,_) -> pipe ^^ space ^^ string (tname ^ "_" ^ fname)) rsbits) in @@ -2668,7 +2694,7 @@ let reg_decls (Defs defs) = else (prefix 2 1) ((separate space) [string "let";string "field_index_bit"; - colon;string "register_field_bit";arrow;string "integer"; + colon;string "register_bitfield";arrow;string "integer"; equals;string "function"]) ( ((separate_map (break 1)) @@ -2751,10 +2777,9 @@ let pp_defs_lem f_arch f d top_line opens = print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ ((separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) - ("Pervasives" :: "Vector" :: "State" :: "Arch" :: opens)) ^/^ defs); + (fun lib -> separate space [string "open import";string lib]) opens) ^/^ hardline ^^ defs); print f_arch (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ ((separate_map hardline) (fun lib -> separate space [string "open import";string lib]) - ["Pervasives";"Assert_extra";"Vector"]) ^/^ decls) + ["Pervasives";"Assert_extra";"Vector"]) ^/^ hardline ^^ decls) diff --git a/src/process_file.ml b/src/process_file.ml index 1a776cff..8dd6fd46 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -177,7 +177,8 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo open_output_with_check_unformatted ("arch.lem") in let ((o2,_, _) as ext_o2) = open_output_with_check_unformatted (f' ^ "embed.lem") in - Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename) ["Sail_values"]; + (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename)) + ["Pervasives";"Vector";"State";"Arch";"Sail_values";"Power_extras"]; close_output_with_check ext_o1; close_output_with_check ext_o2 | Lem_out (Some lib) -> @@ -185,7 +186,8 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo open_output_with_check_unformatted ("arch.lem") in let ((o2,_, _) as ext_o2) = open_output_with_check_unformatted (f' ^ "embed.lem") in - Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename) ["Sail_values"; lib]; + (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename)) + ["Pervasives";"Vector";"State";"Arch";"Sail_values";"Power_extras"; lib]; close_output_with_check ext_o1; close_output_with_check ext_o2 | Ocaml_out None -> diff --git a/src/rewriter.ml b/src/rewriter.ml index e1a1f5a2..5fbbe050 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1285,14 +1285,15 @@ and n_lexp (lexp : 'a lexp) (k : 'a lexp -> 'a exp) : 'a exp = k (fix_effsum_lexp (LEXP_aux (LEXP_memory (id,es),annot)))) | LEXP_cast (typ,id) -> k (fix_effsum_lexp (LEXP_aux (LEXP_cast (typ,id),annot))) - | LEXP_vector (lexp,id) -> + | LEXP_vector (lexp,e) -> n_lexp lexp (fun lexp -> - k (fix_effsum_lexp (LEXP_aux (LEXP_vector (lexp,id),annot)))) - | LEXP_vector_range (lexp,exp1,exp2) -> + n_exp_name e (fun e -> + k (fix_effsum_lexp (LEXP_aux (LEXP_vector (lexp,e),annot)))) + | LEXP_vector_range (lexp,e1,e2) -> n_lexp lexp (fun lexp -> - n_exp_name exp1 (fun exp1 -> - n_exp_name exp2 (fun exp2 -> - k (fix_effsum_lexp (LEXP_aux (LEXP_vector_range (lexp,exp1,exp2),annot)))))) + n_exp_name exp1 (fun e1 -> + n_exp_name exp2 (fun e2 -> + k (fix_effsum_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot)))))) | LEXP_field (lexp,id) -> n_lexp lexp (fun lexp -> k (fix_effsum_lexp (LEXP_aux (LEXP_field (lexp,id),annot)))) |