diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 8 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 129 | ||||
| -rw-r--r-- | src/pretty_print.mli | 2 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 203 | ||||
| -rw-r--r-- | src/process_file.ml | 63 |
5 files changed, 270 insertions, 135 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index b4a15432..b5019df6 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -884,6 +884,14 @@ type register = | UndefinedRegister of integer (* length *) | RegisterPair of register * register +type register_ref 'regstate 'a = + <| read_from : 'regstate -> 'a; + write_to : 'regstate -> 'a -> 'regstate |> + +type field_ref 'regtype 'a = + <| get_field : 'regtype -> 'a; + set_field : 'regtype -> 'a -> 'regtype |> + let name_of_reg = function | Register name _ _ _ _ -> name | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 140258d8..3cbcd4c8 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -6,53 +6,54 @@ open import Sail_values type memstate = map integer memory_byte type tagstate = map integer bitU -type regstate = map string (vector bitU) +(* type regstate = map string (vector bitU) *) -type sequential_state = <| regstate : regstate; - memstate : memstate; - tagstate : tagstate; - write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool|> +type sequential_state 'regs = + <| regstate : 'regs; + memstate : memstate; + tagstate : tagstate; + write_ea : maybe (write_kind * integer * integer); + last_exclusive_operation_was_load : bool|> (* State, nondeterminism and exception monad with result type 'a and exception type 'e. *) -type ME 'a 'e = sequential_state -> list ((either 'a 'e) * sequential_state) +type ME 'regs 'a 'e = sequential_state 'regs -> list ((either 'a 'e) * sequential_state 'regs) (* Most of the time, we don't distinguish between different types of exceptions *) -type M 'a = ME 'a unit +type M 'regs 'a = ME 'regs 'a unit (* For early return, we abuse exceptions by throwing and catching the return value. The exception type is "maybe 'r", where "Nothing" represents a proper exception and "Just r" an early return of value "r". *) -type MR 'a 'r = ME 'a (maybe 'r) +type MR 'regs 'a 'r = ME 'regs 'a (maybe 'r) -val liftR : forall 'a 'r. M 'a -> MR 'a 'r +val liftR : forall 'a 'r 'regs. M 'regs 'a -> MR 'regs 'a 'r let liftR m s = List.map (function | (Left a, s') -> (Left a, s') | (Right (), s') -> (Right Nothing, s') end) (m s) -val return : forall 'a 'e. 'a -> ME 'a 'e +val return : forall 'regs 'a 'e. 'a -> ME 'regs 'a 'e let return a s = [(Left a,s)] -val bind : forall 'a 'b 'e. ME 'a 'e -> ('a -> ME 'b 'e) -> ME 'b 'e -let bind m f (s : sequential_state) = +val bind : forall 'regs 'a 'b 'e. ME 'regs 'a 'e -> ('a -> ME 'regs 'b 'e) -> ME 'regs 'b 'e +let bind m f (s : sequential_state 'regs) = List.concatMap (function | (Left a, s') -> f a s' | (Right e, s') -> [(Right e, s')] end) (m s) let inline (>>=) = bind -val (>>): forall 'b 'e. ME unit 'e -> ME 'b 'e -> ME 'b 'e +val (>>): forall 'regs 'b 'e. ME 'regs unit 'e -> ME 'regs 'b 'e -> ME 'regs 'b 'e let inline (>>) m n = m >>= fun _ -> n -val exit : forall 'e 'a. 'e -> M 'a +val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a let exit _ s = [(Right (), s)] -val early_return : forall 'r. 'r -> MR unit 'r +val early_return : forall 'regs 'r. 'r -> MR 'regs unit 'r let early_return r s = [(Right (Just r), s)] -val catch_early_return : forall 'a. MR 'a 'a -> M 'a +val catch_early_return : forall 'regs 'a 'r. MR 'regs 'a 'a -> M 'regs 'a let catch_early_return m s = List.map (function @@ -66,15 +67,15 @@ let rec range i j = if i = j then [i] else i :: range (i+1) j -val get_reg : sequential_state -> string -> vector bitU -let get_reg state reg = Map_extra.find reg state.regstate +val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a +let get_reg state reg = reg.read_from state.regstate -val set_reg : sequential_state -> string -> vector bitU -> sequential_state -let set_reg state reg bitv = - <| state with regstate = Map.insert reg bitv state.regstate |> +val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs +let set_reg state reg v = + <| state with regstate = reg.write_to state.regstate v |> -val read_mem : forall 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M (bitvector 'b) +val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M 'regs (bitvector 'b) let read_mem dir read_kind addr sz state = let addr = unsigned addr in let addrs = range addr (addr+sz-1) in @@ -96,7 +97,7 @@ let read_mem dir read_kind addr sz state = (* caps are aligned at 32 bytes *) let cap_alignment = (32 : integer) -val read_tag : forall 'a. bool -> read_kind -> bitvector 'a -> M bitU +val read_tag : forall 'regs 'a. bool -> read_kind -> bitvector 'a -> M 'regs bitU let read_tag dir read_kind addr state = let addr = (unsigned addr) / cap_alignment in let tag = match (Map.lookup addr state.tagstate) with @@ -117,18 +118,18 @@ let read_tag dir read_kind addr state = then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)] else [(Left tag, state)] -val excl_result : unit -> M bool +val excl_result : forall 'regs. unit -> M 'regs bool let excl_result () state = let success = (Left true, <| state with last_exclusive_operation_was_load = false |>) in (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else [] -val write_mem_ea : forall 'a. write_kind -> bitvector 'a -> integer -> M unit +val write_mem_ea : forall 'regs 'a. write_kind -> bitvector 'a -> integer -> M 'regs unit let write_mem_ea write_kind addr sz state = let addr = unsigned addr in [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)] -val write_mem_val : forall 'b. bitvector 'b -> M bool +val write_mem_val : forall 'regs 'b. bitvector 'b -> M 'regs bool let write_mem_val v state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" @@ -140,7 +141,7 @@ let write_mem_val v state = state.memstate addresses_with_value in [(Left true, <| state with memstate = memstate |>)] -val write_tag : bitU -> M bool +val write_tag : forall 'regs. bitU -> M 'regs bool let write_tag t state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" @@ -149,10 +150,10 @@ let write_tag t state = let tagstate = Map.insert taddr t state.tagstate in [(Left true, <| state with tagstate = tagstate |>)] -val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a) +val read_reg : forall 'regs 'a. register_ref 'regs 'a -> M 'regs 'a let read_reg reg state = - let v = get_reg state (name_of_reg reg) in - [(Left (vec_to_bvec v),state)] + let v = reg.read_from state.regstate in + [(Left v,state)] (*let read_reg_range reg i j state = let v = slice (get_reg state (name_of_reg reg)) i j in [(Left (vec_to_bvec v),state)] @@ -168,41 +169,47 @@ let read_reg_bitfield reg regfield = let reg_deref = read_reg -val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit +val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit let write_reg reg v state = - [(Left (), set_reg state (name_of_reg reg) (bvec_to_vec v))] + [(Left (), <| state with regstate = reg.write_to state.regstate v |>)] +val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit +let update_reg reg f v state = + let current_value = get_reg state reg in + let new_value = f current_value v in + [(Left (), set_reg state reg new_value)] let write_reg_range reg i j v state = - let current_value = get_reg state (name_of_reg reg) in - let new_value = update current_value i j (bvec_to_vec v) in - [(Left (), set_reg state (name_of_reg reg) new_value)] + let current_value = get_reg state reg in + let new_value = bvupdate current_value i j v in + [(Left (), set_reg state reg new_value)] let write_reg_bit reg i bit state = - let current_value = get_reg state (name_of_reg reg) in - let new_value = update_pos current_value i bit in - [(Left (), set_reg state (name_of_reg reg) new_value)] + let current_value = get_reg state reg in + let new_value = bvupdate_pos current_value i bit in + [(Left (), set_reg state reg new_value)] let write_reg_field reg regfield = - let (i,j) = register_field_indices reg regfield in - write_reg_range reg i j -let write_reg_bitfield reg regfield = - let (i,_) = register_field_indices reg regfield in - write_reg_bit reg i -let write_reg_field_range reg regfield i j v state = - let (i0,j0) = register_field_indices reg regfield in - let current_value = get_reg state (name_of_reg reg) in - let current_field_value = slice current_value i0 j0 in - let new_field_value = update current_field_value i j (bvec_to_vec v) in - let new_value = update current_value i j new_field_value in - [(Left (), set_reg state (name_of_reg reg) new_value)] - - -val barrier : barrier_kind -> M unit + update_reg reg regfield.set_field +let write_reg_field_range reg regfield i j = + let upd regval v = + let current_field_value = regfield.get_field regval in + let new_field_value = bvupdate current_field_value i j v in + regfield.set_field regval new_field_value in + update_reg reg upd +let write_reg_field_bit reg regfield i = + let upd regval v = + let current_field_value = regfield.get_field regval in + let new_field_value = bvupdate_pos current_field_value i v in + regfield.set_field regval new_field_value in + update_reg reg upd + + +val barrier : forall 'regs. barrier_kind -> M 'regs unit let barrier _ = return () -val footprint : M unit +val footprint : forall 'regs. M 'regs unit let footprint = return () -val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> ME 'vars 'e) -> ME 'vars 'e +val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e let rec foreachM_inc (i,stop,by) vars body = if i <= stop then @@ -211,8 +218,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return vars -val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> ME 'vars 'e) -> ME 'vars 'e +val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e let rec foreachM_dec (i,stop,by) vars body = if i >= stop then @@ -220,7 +227,7 @@ let rec foreachM_dec (i,stop,by) vars body = foreachM_dec (i - by,stop,by) vars body else return vars -let write_two_regs r1 r2 bvec state = +(*let write_two_regs r1 r2 bvec state = let vec = bvec_to_vec bvec in let is_inc = let is_inc_r1 = is_inc_of_reg r1 in @@ -242,4 +249,4 @@ let write_two_regs r1 r2 bvec state = else slice vec (start_vec - size_r1) (start_vec - size_vec) in let state1 = set_reg state (name_of_reg r1) r1_v in let state2 = set_reg state1 (name_of_reg r2) r2_v in - [(Left (), state2)] + [(Left (), state2)]*) diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 24816206..37de5241 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -52,4 +52,4 @@ val pat_to_string : 'a pat -> string val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit -val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit +val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 1b6c67c5..30d30f4a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -140,6 +140,12 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with | Typ_id(id) when Env.is_regtyp id env -> true | _ -> false +let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with + | Nexp_constant i -> string ("ty" ^ string_of_int i) + | Nexp_var v -> string (string_of_kid v) + | _ -> raise (Reporting_basic.err_unreachable l + ("cannot pretty-print non-atomic nexp \"" ^ string_of_nexp full_nexp ^ "\"")) + let doc_typ_lem, doc_atomic_typ_lem = (* following the structure of parser for precedence *) let rec typ regtypes ty = fn_typ regtypes true ty @@ -168,17 +174,19 @@ let doc_typ_lem, doc_atomic_typ_lem = Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> - (match simplify_nexp m with + string "bitvector " ^^ doc_nexp_lem (simplify_nexp m) + (* (match simplify_nexp m with | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m] | _ -> raise (Reporting_basic.err_unreachable l - "cannot pretty-print bitvector type with non-constant length")) + "cannot pretty-print bitvector type with non-constant length")) *) | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> (* TODO: Better distinguish register names and contents? *) (* fn_typ regtypes atyp_needed etyp *) - (string "register") + let tpp = (string "register_ref regstate " ^^ typ regtypes etyp) in + if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "range", _),_) -> (string "integer") | Typ_app(Id_aux (Id "implicit", _),_) -> @@ -206,7 +214,7 @@ let doc_typ_lem, doc_atomic_typ_lem = if atyp_needed then parens tpp else tpp and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ regtypes true t - | Typ_arg_nexp n -> empty + | Typ_arg_nexp n -> doc_nexp_lem (simplify_nexp n) | Typ_arg_order o -> empty | Typ_arg_effect e -> empty in typ', atomic_typ @@ -234,10 +242,10 @@ and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with | _ -> false let doc_tannot_lem regtypes eff typ = - if contains_t_pp_var typ then empty - else + (* if contains_t_pp_var typ then empty + else *) let ta = doc_typ_lem regtypes typ in - if eff then string " : M " ^^ parens ta + if eff then string " : _M " ^^ parens ta else string " : " ^^ ta (* doc_lit_lem gets as an additional parameter the type information from the @@ -346,6 +354,13 @@ let contains_early_return exp = { (Rewriter.compute_exp_alg false (||)) with e_return = (fun (_, r) -> (true, E_return r)) } exp) +let typ_id_of (Typ_aux (typ, l)) = match typ with + | Typ_id id -> id + | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) + when string_of_id register = "register" -> id + | Typ_app (id, _) -> id + | _ -> raise (Reporting_basic.err_unreachable l "failed to get type id") + let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = @@ -365,14 +380,18 @@ let doc_exp_lem, doc_let_lem = (match le_act (*, t, tag*) with | LEXP_vector_range (le,e2,e3) -> (match le with - | LEXP_aux (LEXP_field (le,id), lannot) -> - if is_bit_typ (typ_of_annot lannot) then + | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> + if is_bit_typ (typ_of_annot fannot) then raise (report l "indexing a register's (single bit) bitfield not supported") else + let field_ref = + doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field_range") (align (doc_lexp_deref_lem regtypes early_ret le ^^ space^^ - string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e))) + field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e))) | _ -> liftR ((prefix 2 1) (string "write_reg_range") @@ -380,27 +399,35 @@ let doc_exp_lem, doc_let_lem = ) | LEXP_vector (le,e2) when is_bit_typ t -> (match le with - | LEXP_aux (LEXP_field (le,id), lannot) -> - if is_bit_typ (typ_of_annot lannot) then + | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> + if is_bit_typ (typ_of_annot fannot) then raise (report l "indexing a register's (single bit) bitfield not supported") else + let field_ref = + doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field_bit") - (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e))) + (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e))) | _ -> liftR ((prefix 2 1) (string "write_reg_bit") (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e)) ) - | LEXP_field (le,id) when is_bit_typ t -> + (* | LEXP_field (le,id) when is_bit_typ t -> liftR ((prefix 2 1) (string "write_reg_bitfield") - (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) - | LEXP_field (le,id) -> + (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *) + | LEXP_field ((LEXP_aux (_, lannot) as le),id) -> + let field_ref = + doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field") (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ - string_lit(doc_id_lem id) ^/^ expY e)) + field_ref ^/^ expY e)) (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info -> (match alias_info with | Alias_field(reg,field) -> @@ -562,8 +589,7 @@ let doc_exp_lem, doc_let_lem = when Env.is_regtyp tid env -> let t = (* Env.base_typ_of (env_of full_exp) *) (typ_of full_exp) in let eff = effect_of full_exp in - let field_f = string "get" ^^ underscore ^^ - doc_id_lem tid ^^ underscore ^^ doc_id_lem id in + let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in let (ta,aexp_needed) = if contains_bitvector_typ t && not (contains_t_pp_var t) then (doc_tannot_lem regtypes (effectful eff) t, true) @@ -986,15 +1012,41 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with doc_op equals (concat [string "type"; space; doc_id_lem_type id]) (doc_typschm_lem regtypes false typschm) | TD_record(id,nm,typq,fs,_) -> - let f_pp (typ,fid) = - let fname = if prefix_recordtype - then concat [doc_id_lem id;string "_";doc_id_lem_type fid;] - else doc_id_lem_type fid in - concat [fname;space;colon;space;doc_typ_lem regtypes typ; semi] in - let fs_doc = group (separate_map (break 1) f_pp fs) in + let fname fid = if prefix_recordtype + then concat [doc_id_lem id;string "_";doc_id_lem_type fid;] + else doc_id_lem_type fid in + let f_pp (typ,fid) = + concat [fname fid;space;colon;space;doc_typ_lem regtypes typ; semi] in + let rectyp = match typq with + | TypQ_aux (TypQ_tq qs, _) -> + let quant_item = function + | QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l) + | QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) -> + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, l)), l)] + | _ -> [] in + let targs = List.concat (List.map quant_item qs) in + mk_typ (Typ_app (id, targs)) + | TypQ_aux (TypQ_no_forall, _) -> mk_id_typ id in + let fs_doc = group (separate_map (break 1) f_pp fs) in + let doc_field (ftyp, fid) = + let reftyp = + mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), + [mk_typ_arg (Typ_arg_typ rectyp); + mk_typ_arg (Typ_arg_typ ftyp)])) in + let rfannot = doc_tannot_lem regtypes false reftyp in + let get, set = + string "rec_val" ^^ dot ^^ fname fid, + anglebars (space ^^ string "rec_val with " ^^ + (doc_op equals (fname fid) (string "v")) ^^ space) in doc_op equals - (concat [string "type"; space; doc_id_lem_type id;]) - ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) + (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) + (anglebars (concat [space; + doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; + doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in + doc_op equals + (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq]) + ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^ + separate_map hardline doc_field fs | TD_variant(id,nm,typq,ar,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty @@ -1198,27 +1250,38 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td 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 fsize = if dir_b then j-i+1 else i-j+1 in + let ftyp = vector_typ (nconstant i) (nconstant fsize) ord bit_typ in + let reftyp = + mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), + [mk_typ_arg (Typ_arg_typ (mk_id_typ id)); + mk_typ_arg (Typ_arg_typ ftyp)])) in + let rfannot = doc_tannot_lem regtypes false reftyp in let get, set = "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")", "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in doc_op equals - (concat [string "let get_"; doc_id_lem id; underscore; doc_id_lem fid; - space; parens (string "reg" ^^ tannot)]) (string get) ^^ - hardline ^^ - doc_op equals + (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) + (concat [ + space; langlebar; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline; + space; space; space; string (" set_field = (fun reg v -> " ^ set ^ ") "); ranglebar]) + (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^ + string (" get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^ + string (" set_field = (fun reg v -> " ^ set ^") |>") *) + (* doc_op equals (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid; - space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) + space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *) in doc_op equals (concat [string "type";space;doc_id_lem id]) (doc_typ_lem regtypes vtyp) ^^ hardline ^^ - doc_op equals + (* 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; dir; break 0 ^^ brackets (align doc_rids)])) - ^^ hardline ^^ + ^^ hardline ^^ *) doc_op equals (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"]) (string "reg") @@ -1333,7 +1396,8 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = match reg with | DEC_reg(typ,id) -> - let env = env_of_annot annot in + empty + (* let env = env_of_annot annot in (match typ with | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env -> separate space [string "let";doc_id_lem id;equals; @@ -1356,7 +1420,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) else raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ))) + ("can't deal with register type " ^ string_of_typ typ))) *) | DEC_alias(id,alspec) -> empty | DEC_typ_alias(typ,id,alspec) -> empty @@ -1399,9 +1463,50 @@ let find_regtypes (Defs defs) = | _ -> acc ) [] defs -let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = +let find_registers (Defs defs) = + List.fold_left + (fun acc def -> + match def with + | DEF_reg_dec (DEC_aux(DEC_reg (typ, id),_)) -> (typ, id) :: acc + | _ -> acc + ) [] defs + +let doc_regstate_lem regtypes registers = + let l = Parse_ast.Unknown in + let annot = (l, None) in + let regstate = match registers with + | [] -> + TD_abbrev ( + Id_aux (Id "regstate", l), + Name_sect_aux (Name_sect_none, l), + TypSchm_aux (TypSchm_ts (TypQ_aux (TypQ_tq [], l), unit_typ), l)) + | _ -> + TD_record ( + Id_aux (Id "regstate", l), + Name_sect_aux (Name_sect_none, l), + TypQ_aux (TypQ_tq [], l), + registers, + false) in + concat [ + doc_typdef_lem regtypes (TD_aux (regstate, annot)); hardline; + hardline; + string "type _M 'a = M regstate 'a" + ] + +let doc_register_refs_lem regtypes registers = + let doc_register_ref (typ, id) = + let idd = doc_id_lem id in + let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in + concat [string "let "; idd; string " = <|"; hardline; + string " read_from = (fun s -> s."; field; string ");"; hardline; + string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in + separate_map hardline doc_register_ref registers + +let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = let regtypes = find_regtypes d in let (typdefs,valdefs) = doc_defs_lem regtypes d in + let regstate_def = doc_regstate_lem regtypes (find_registers d) in + let register_refs = doc_register_refs_lem regtypes (find_registers d) in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; @@ -1420,6 +1525,30 @@ let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_f hardline] else empty; typdefs]); + (print types_seq_file) + (concat + [string "(*" ^^ (string top_line) ^^ string "*)";hardline; + (separate_map hardline) + (fun lib -> separate space [string "open import";string lib]) types_seq_modules;hardline; + if !print_to_from_interp_value + then + concat + [(separate_map hardline) + (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"]; + string "open import Deep_shallow_convert"; + hardline; + hardline; + string "module SI = Interp"; hardline; + string "module SIA = Interp_ast"; hardline; + hardline] + else empty; + typdefs; + hardline; + hardline; + regstate_def; + hardline; + hardline; + register_refs]); (print prompt_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; diff --git a/src/process_file.ml b/src/process_file.ml index 95562969..b63f7ba0 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -129,6 +129,31 @@ let close_output_with_check (o, temp_file_name, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f +let output_lem filename libs libs_seq defs = + let generated_line = generated_line filename in + let types_module = (filename ^ "_embed_types") in + let types_module_sequential = (filename ^ "_embed_types_sequential") in + let ((ot,_, _) as ext_ot) = + open_output_with_check_unformatted (filename ^ "_embed_types.lem") in + let ((ots,_, _) as ext_ots) = + open_output_with_check_unformatted (filename ^ "_embed_types_sequential.lem") in + let ((o,_, _) as ext_o) = + open_output_with_check_unformatted (filename ^ "_embed.lem") in + let ((os,_, _) as ext_os) = + open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in + (Pretty_print.pp_defs_lem + (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"]) + (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"]) + (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"; + String.capitalize types_module] @ libs) + (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"; + String.capitalize types_module_sequential] @ libs_seq) + defs generated_line); + close_output_with_check ext_ot; + close_output_with_check ext_ots; + close_output_with_check ext_o; + close_output_with_check ext_os + let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with @@ -175,43 +200,9 @@ let output1 libpath out_arg filename defs = close_output_with_check ext_o end | Lem_out None -> - let generated_line = generated_line filename in - let types_module = (f' ^ "_embed_types") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (f' ^ "_embed_types.lem") in - let ((o',_, _) as ext_o') = - open_output_with_check_unformatted (f' ^ "_embed.lem") in - let ((o'',_, _) as ext_o'') = - open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in - (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) - (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"; - String.capitalize types_module]) - (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"; - String.capitalize types_module]) - defs generated_line); - close_output_with_check ext_o; - close_output_with_check ext_o'; - close_output_with_check ext_o''; + output_lem f' [] [] defs | Lem_out (Some lib) -> - let generated_line = generated_line filename in - let types_module = (f' ^ "_embed_types") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (f' ^ "_embed_types.lem") in - let ((o',_, _) as ext_o') = - open_output_with_check_unformatted (f' ^ "_embed.lem") in - let ((o'',_, _) as ext_o'') = - open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in - (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) - (o',["Pervasives_extra";"Sail_impl_base";"Prompt"; - "Sail_values";String.capitalize types_module;lib]) - (o'',["Pervasives_extra";"Sail_impl_base";"State"; - "Sail_values";String.capitalize types_module;lib ^ "_sequential"]) - defs generated_line); - close_output_with_check ext_o; - close_output_with_check ext_o'; - close_output_with_check ext_o'' + output_lem f' [lib] [lib ^ "_sequential"] defs | Ocaml_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; |