1 files changed, 187 insertions, 23 deletions

diff --git a/src/state.ml b/src/state.ml
index 59fb9995..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) ->
@@ -306,6 +392,85 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) =
   hardline ^^ hardline ^^
   separate_map (hardline ^^ hardline) register_lemmas registers
 
+let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with
+  | Typ_app _ when is_vector_typ typ && not (is_bitvector_typ typ) ->
+     let size, ord, etyp = vector_typ_args_of typ in
+     let size = string_of_nexp (nexp_simp size) in
+     let is_inc = if is_order_inc ord then "true" else "false" in
+     let etyp_of, of_etyp = regval_convs_coq etyp in
+     "(fun v => vector_of_regval " ^ etyp_of ^ " v)",
+     "(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)"
+  | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+    when string_of_id id = "list" ->
+     let etyp_of, of_etyp = regval_convs_coq etyp in
+     "(fun v => list_of_regval " ^ etyp_of ^ " v)",
+     "(fun v => regval_of_list " ^ of_etyp ^ " v)"
+  | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
+    when string_of_id id = "option" ->
+     let etyp_of, of_etyp = regval_convs_coq etyp in
+     "(fun v => option_of_regval " ^ etyp_of ^ " v)",
+     "(fun v => regval_of_option " ^ of_etyp ^ " v)"
+  | _ ->
+     let id = string_of_id (regval_constr_id true typ) in
+     "(fun v => " ^ id ^ "_of_regval v)", "(fun v => regval_of_" ^ id ^ " v)"
+
+let register_refs_coq registers =
+  let generic_convs =
+    separate_map hardline string [
+      "Definition vector_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
+      "  | Regval_vector (_, _, v) => just_list (List.map of_regval v)";
+      "  | _ => None";
+      "end.";
+      "";
+      "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : list a) : register_value := Regval_vector (size, is_inc, List.map regval_of xs).";
+      "";
+      "Definition list_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
+      "  | Regval_list v => just_list (List.map of_regval v)";
+      "  | _ => None";
+      "end.";
+      "";
+      "Definition regval_of_list {a} (regval_of : a -> register_value) (xs : list a) : register_value := Regval_list (List.map regval_of xs).";
+      "";
+      "Definition option_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (option a) := match rv with";
+      "  | Regval_option v => option_map of_regval v";
+      "  | _ => None";
+      "end.";
+      "";
+      "Definition regval_of_option {a} (regval_of : a -> register_value) (v : option a) := Regval_option (option_map regval_of v).";
+      "";
+      ""
+    ]
+  in
+  let register_ref (typ, id) =
+    let idd = string (string_of_id id) in
+    (* let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in *)
+    let of_regval, regval_of = regval_convs_coq typ in
+    concat [string "Definition "; idd; string "_ref := {|"; hardline;
+      string "  name := \""; idd; string "\";"; hardline;
+      string "  read_from := (fun s => s.("; idd; string "));"; hardline;
+      string "  write_to := (fun v s => ({[ s with "; idd; string " := v ]}));"; hardline;
+      string "  of_regval := "; string of_regval; string ";"; hardline;
+      string "  regval_of := "; string regval_of; string " |}."; hardline]
+  in
+  let refs = separate_map hardline register_ref registers in
+  let get_set_reg (_, id) =
+    let idd = string_of_id id in
+    string ("  if string_dec reg_name \"" ^ idd ^ "\" then Some (" ^ idd ^ "_ref.(regval_of) (" ^ idd ^ "_ref.(read_from) s)) else"),
+    string ("  if string_dec reg_name \"" ^ idd ^ "\" then option_map (fun v => " ^ idd ^ "_ref.(write_to) v s) (" ^ idd ^ "_ref.(of_regval) v) else")
+  in
+  let getters_setters =
+    let getters, setters = List.split (List.map get_set_reg registers) in
+    string "Local Open Scope string." ^^ hardline ^^
+    string "Definition get_regval (reg_name : string) (s : regstate) : option register_value :=" ^^ hardline ^^
+    separate hardline getters ^^ hardline ^^
+    string "  None." ^^ hardline ^^ hardline ^^
+    string "Definition set_regval (reg_name : string) (v : register_value) (s : regstate) : option regstate :=" ^^ hardline ^^
+    separate hardline setters ^^ hardline ^^
+    string "  None." ^^ hardline ^^ hardline ^^
+    string "Definition register_accessors := (get_regval, set_regval)." ^^ hardline ^^ hardline
+  in
+  separate hardline [generic_convs; refs; getters_setters]
+
 let generate_regstate_defs mwords defs =
   (* FIXME We currently don't want to generate undefined_type functions
      for register state and values.  For the Lem backend, this would require
@@ -314,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