From 9fea45722d58132cc484d9421fb3407286dc4f01 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 4 May 2018 16:18:01 +0100 Subject: Generate initial register state record Filled with default values (e.g., 0) and used to initialise the state monad. There is already code to generate a Sail function "initialize_registers", but this is monadic itself, so it cannot be used to initialise the monad. --- src/state.ml | 131 ++++++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 108 insertions(+), 23 deletions(-) (limited to 'src/state.ml') diff --git a/src/state.ml b/src/state.ml index 49fa5a99..5a360456 100644 --- a/src/state.ml +++ b/src/state.ml @@ -60,6 +60,11 @@ open Pretty_print_sail let defs_of_string = ast_of_def_string Ast_util.inc_ord +let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs)) + +let has_default_order defs = + List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs + let find_registers defs = List.fold_left (fun acc def -> @@ -77,18 +82,100 @@ let generate_regstate = function | [] -> ["type regstate = unit"] | registers -> let reg (typ, id) = Printf.sprintf "%s : %s" (string_of_id id) (to_string (doc_typ typ)) in - let initreg (_, id) = Printf.sprintf "%s = undefined" (string_of_id id) in - let regstate = - "struct regstate = { " ^ - (String.concat ", " (List.map reg registers)) ^ - " }" - in - let initstate = - "let initial_regstate : regstate = struct { " ^ - (String.concat ", " (List.map initreg registers)) ^ - " }" - in - regstate :: (if !Initial_check.opt_undefined_gen then [initstate] else []) + ["struct regstate = { " ^ (String.concat ", " (List.map reg registers)) ^ " }"] + +let generate_initial_regstate defs = + let registers = find_registers defs in + if registers = [] then [] else + try + (* Recursively choose a default value for every type in the spec. + vals, constructed below, maps user-defined types to default values. *) + let rec lookup_init_val vals (Typ_aux (typ_aux, _) as typ) = + match typ_aux with + | Typ_id id -> + if string_of_id id = "bool" then "false" else + if string_of_id id = "bit" then "bitzero" else + if string_of_id id = "int" then "0" else + if string_of_id id = "nat" then "0" else + if string_of_id id = "real" then "0" else + if string_of_id id = "string" then "\"\"" else + if string_of_id id = "unit" then "()" else + Bindings.find id vals [] + | Typ_app (id, _) when string_of_id id = "list" -> "[||]" + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) when string_of_id id = "atom" -> + string_of_nexp nexp + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _); _]) when string_of_id id = "range" -> + string_of_nexp nexp + | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ; + Typ_arg_aux (Typ_arg_typ etyp, _)]) + when string_of_id id = "vector" -> + (* Output a list of initial values of the vector elements, or a + literal binary zero value if this is a bitvector and the + environment has a default indexing order (required by the + typechecker for binary and hex literals) *) + let literal_bitvec = is_bit_typ etyp && has_default_order defs in + let init_elem = if literal_bitvec then "0" else lookup_init_val vals etyp in + let rec elems len = + if (Nat_big_num.less_equal len Nat_big_num.zero) then [] else + init_elem :: elems (Nat_big_num.pred len) + in + if literal_bitvec then "0b" ^ (String.concat "" (elems len)) else + "[" ^ (String.concat ", " (elems len)) ^ "]" + | Typ_app (id, args) -> Bindings.find id vals args + | Typ_tup typs -> + "(" ^ (String.concat ", " (List.map (lookup_init_val vals) typs)) ^ ")" + | Typ_exist (_, _, typ) -> lookup_init_val vals typ + | _ -> raise Not_found + in + (* Helper functions to instantiate type arguments *) + let typ_subst_targ kid (Typ_arg_aux (arg, _)) typ = match arg with + | Typ_arg_nexp (Nexp_aux (nexp, _)) -> typ_subst_nexp kid nexp typ + | Typ_arg_typ (Typ_aux (typ', _)) -> typ_subst_typ kid typ' typ + | Typ_arg_order (Ord_aux (ord, _)) -> typ_subst_order kid ord typ + in + let typ_subst_quant_item typ (QI_aux (qi, _)) arg = match qi with + | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) -> + typ_subst_targ kid arg typ + | _ -> typ + in + let typ_subst_typquant tq args typ = + List.fold_left2 typ_subst_quant_item typ (quant_items tq) args + in + let add_typ_init_val vals = function + | TD_enum (id, _, id1 :: _, _) -> + (* Choose the first value of an enumeration type as default *) + Bindings.add id (fun _ -> string_of_id id1) vals + | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) -> + (* Choose the first variant of a union type as default *) + let init_val args = + let typ1 = typ_subst_typquant tq args typ1 in + string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")" + in + Bindings.add id init_val vals + | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (tq, typ), _)) -> + let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in + Bindings.add id init_val vals + | TD_record (id, _, tq, fields, _) -> + let init_val args = + let init_field (typ, id) = + let typ = typ_subst_typquant tq args typ in + string_of_id id ^ " = " ^ lookup_init_val vals typ + in + "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }" + in + Bindings.add id init_val vals + | TD_bitfield (id, typ, _) -> + Bindings.add id (fun _ -> lookup_init_val vals typ) vals + | _ -> vals + in + let init_vals = List.fold_left (fun vals def -> match def with + | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td + | _ -> vals) Bindings.empty defs + in + let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in + ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"] + with + | _ -> [] (* Do not generate an initial register state if anything goes wrong *) let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with | Typ_id id -> id @@ -135,9 +222,8 @@ let generate_regval_typ typs = (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^ " }"] -let add_regval_conv id typ defs = +let add_regval_conv id typ (Defs defs) = let id = string_of_id id in - let is_defined name = IdSet.mem (mk_id name) (ids_of_defs defs) in let typ_str = to_string (doc_typ typ) in (* Create a function that converts from regval to the target type. *) let from_name = id ^ "_of_regval" in @@ -146,14 +232,14 @@ let add_regval_conv id typ defs = Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id; Printf.sprintf "and %s _ = None()" from_name ] in - let from_defs = if is_defined from_name then [] else [from_val; from_function] in + let from_defs = if is_defined defs from_name then [] else [from_val; from_function] in (* Create a function that converts from target type to regval. *) let to_name = "regval_of_" ^ id in let to_val = Printf.sprintf "val %s : %s -> register_value" to_name typ_str in let to_function = Printf.sprintf "function %s v = Regval_%s(v)" to_name id in - let to_defs = if is_defined to_name then [] else [to_val; to_function] in + let to_defs = if is_defined defs to_name then [] else [to_val; to_function] in let cdefs = concat_ast (List.map defs_of_string (from_defs @ to_defs)) in - append_ast defs cdefs + append_ast (Defs defs) cdefs let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) -> @@ -393,17 +479,16 @@ let generate_regstate_defs mwords defs = let gen_undef = !Initial_check.opt_undefined_gen in Initial_check.opt_undefined_gen := false; let registers = find_registers defs in - let def_ids = ids_of_defs (Defs defs) in - let has_def name = IdSet.mem (mk_id name) def_ids in let regtyps = register_base_types mwords (List.map fst registers) in let option_typ = - if has_def "option" then [] else + if is_defined defs "option" then [] else ["union option ('a : Type) = {None : unit, Some : 'a}"] in - let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in - let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in + let regval_typ = if is_defined defs "register_value" then [] else generate_regval_typ regtyps in + let regstate_typ = if is_defined defs "regstate" then [] else generate_regstate registers in + let initregstate = if is_defined defs "initial_regstate" then [] else generate_initial_regstate defs in let defs = - option_typ @ regval_typ @ regstate_typ + option_typ @ regval_typ @ regstate_typ @ initregstate |> List.map defs_of_string |> concat_ast |> Bindings.fold add_regval_conv regtyps -- cgit v1.2.3