Merge branch 'ocaml-instruction-generation' into sail2

5 files changed, 252 insertions, 6 deletions

diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 479fc821..23e27e2b 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -648,7 +648,216 @@ let val_spec_typs (Defs defs) =
   ignore (vs_typs defs);
   !typs
 
-let ocaml_defs (Defs defs) =
+(* Code to produce test value generators for a given set of types.
+
+   This needs type definitions from the initial type checked Sail so that the
+   full type information is available.  For example, vectors are simplified to
+   lists, so to produce lists of the right length we need to know what the
+   size of the vector is.
+ *)
+
+let orig_types_for_ocaml_generator (Defs defs) =
+  Util.map_filter (function
+      | DEF_type td -> Some td
+      | _ -> None) defs
+
+let ocaml_pp_generators ctx defs orig_types required =
+  let add_def typemap td =
+    Bindings.add (id_of_type_def td) td typemap
+  in
+  let typemap = List.fold_left add_def Bindings.empty orig_types in
+  let required = IdSet.of_list required in
+  let rec always_add_req_from_id required id =
+    match Bindings.find id typemap with
+    | td -> add_req_from_td (IdSet.add id required) td
+    | exception Not_found ->
+       if Bindings.mem id Type_check.Env.builtin_typs
+       then IdSet.add id required
+       else
+         raise (Reporting_basic.err_unreachable (id_loc id) __POS__
+                  ("Required generator of unknown type " ^ string_of_id id))
+  and add_req_from_id required id =
+    if IdSet.mem id required then required
+    else always_add_req_from_id required id
+  and add_req_from_typ required (Typ_aux (typ,_) as full_typ) =
+    match typ with
+    | Typ_id id -> add_req_from_id required id
+    | Typ_var _
+      -> required
+    | Typ_internal_unknown
+    | Typ_fn _
+    | Typ_bidir _
+      -> raise (Reporting_basic.err_unreachable (typ_loc full_typ) __POS__
+                  ("Required generator for type that should not appear: " ^
+                     string_of_typ full_typ))
+    | Typ_tup typs ->
+       List.fold_left add_req_from_typ required typs
+    | Typ_exist _ ->
+       raise (Reporting_basic.err_todo (typ_loc full_typ)
+                ("Generators for existential types not yet supported: " ^
+                   string_of_typ full_typ))
+    | Typ_app (id,args) ->
+       List.fold_left add_req_from_typarg (add_req_from_id required id) args
+  and add_req_from_typarg required (Typ_arg_aux (arg,_)) =
+    match arg with
+    | Typ_arg_typ typ -> add_req_from_typ required typ
+    | Typ_arg_nexp _
+    | Typ_arg_order _
+      -> required
+  and add_req_from_td required (TD_aux (td,(l,_))) =
+    match td with
+    | TD_abbrev (_, _, TypSchm_aux (TypSchm_ts (_,typ),_)) ->
+       add_req_from_typ required typ
+    | TD_record (_, _, _, fields, _) ->
+       List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields
+    | TD_variant (_, _, _, variants, _) ->
+       List.fold_left (fun req (Tu_aux (Tu_ty_id (typ,_),_)) ->
+           add_req_from_typ req typ) required variants
+    | TD_enum _ -> required
+    | TD_bitfield _ -> raise (Reporting_basic.err_todo l "Generators for bitfields not yet supported")
+  in
+  let required = IdSet.fold (fun id req -> always_add_req_from_id req id) required required in
+  let type_name id = zencode_string (string_of_id id) in
+  let make_gen_field id =
+    let allquants =
+      match Bindings.find id typemap with
+      | TD_aux (td,_) ->
+         (match td with
+          | TD_abbrev (_,_,TypSchm_aux (TypSchm_ts (tqs,typ),_)) -> tqs
+          | TD_record (_,_,tqs,_,_) -> tqs
+          | TD_variant (_,_,tqs,_,_) -> tqs
+          | TD_enum _ -> TypQ_aux (TypQ_no_forall,Unknown)
+          | TD_bitfield _ -> assert false)
+      | exception Not_found ->
+         Bindings.find id Type_check.Env.builtin_typs
+    in
+    let tquants = quant_kopts allquants in
+    let gen_tyvars = List.map (fun k -> kopt_kid k |> zencode_kid)
+                       (List.filter is_typ_kopt tquants) in
+    let print_quant kindedid =
+      if is_nat_kopt kindedid then string "int" else
+      if is_order_kopt kindedid then string "bool" else
+      parens (separate space [string "generators"; string "->"; zencode_kid (kopt_kid kindedid)])
+    in
+    let name = "gen_" ^ type_name id in
+    let make_tyarg kindedid =
+      if is_nat_kopt kindedid
+      then mk_typ_arg (Typ_arg_nexp (nvar (kopt_kid kindedid)))
+      else if is_order_kopt kindedid
+      then mk_typ_arg (Typ_arg_order (mk_ord (Ord_var (kopt_kid kindedid))))
+      else mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var (kopt_kid kindedid))))
+    in
+    let targs = List.map make_tyarg tquants in
+    let gen_tyvars_pp, out_typ = match gen_tyvars with
+      | [] -> empty, mk_id_typ id
+      | _ -> separate space gen_tyvars ^^ dot ^^ space, mk_typ (Typ_app (id,targs))
+    in
+    let out_typ = Rewrites.simple_typ out_typ in
+    let types = string "generators" :: List.map print_quant tquants @ [ocaml_typ ctx out_typ] in
+    string name ^^ colon ^^ space ^^
+      gen_tyvars_pp ^^ separate (string " -> ") types
+  in
+  let fields = separate_map (string ";" ^^ break 1) make_gen_field (IdSet.elements required) in
+  let gen_record_type_pp =
+    string "type generators = {" ^^ group (nest 2 (break 0 ^^ fields) ^^ break 0) ^^ string "}"
+  in
+  let make_rand_gen id =
+    if Bindings.mem id Type_check.Env.builtin_typs
+    then empty
+    else
+      let name = string ("rand_" ^ type_name id) in
+      let mk_arg kid = string (zencode_string (string_of_kid kid)) in
+      let rec gen_type (Typ_aux (typ,l) as full_typ) =
+        let typ_str, args_pp = match typ with
+          | Typ_id id -> type_name id, [string "g"]
+          | Typ_app (id,args) -> type_name id, string "g"::List.map typearg args
+          | _ -> raise (Reporting_basic.err_todo l
+                          ("Unsupported type for generators: " ^ string_of_typ full_typ))
+        in
+        let args_pp = match args_pp with [] -> empty
+                                       | _ -> space ^^ separate space args_pp
+        in
+        string ("g.gen_" ^ typ_str) ^^ args_pp
+      and typearg (Typ_arg_aux (arg,_)) =
+        match arg with
+        | Typ_arg_nexp (Nexp_aux (nexp,l) as full_nexp) ->
+           (match nexp with
+            | Nexp_constant c -> string (Big_int.to_string c) (* TODO: overflow *)
+            | Nexp_var v -> mk_arg v
+            | _ -> raise (Reporting_basic.err_todo l
+                            ("Unsupported nexp for generators: " ^ string_of_nexp full_nexp)))
+        | Typ_arg_order (Ord_aux (ord,_)) ->
+           (match ord with
+            | Ord_var v -> mk_arg v
+            | Ord_inc -> string "true"
+            | Ord_dec -> string "false")
+        | Typ_arg_typ typ -> parens (string "fun g -> " ^^ gen_type typ)
+      in
+      let make_subgen (Typ_aux (typ,l) as full_typ) =
+        let typ_str, args_pp =
+          match typ with
+          | Typ_id id -> type_name id, []
+          | Typ_app (id,args) -> type_name id, List.map typearg args
+          | _ -> raise (Reporting_basic.err_todo l
+                          ("Unsupported type for generators: " ^ string_of_typ full_typ))
+        in
+        let args_pp = match args_pp with [] -> empty
+                                       | _ -> space ^^ separate space args_pp
+        in string ("g.gen_" ^ typ_str) ^^ space ^^ string "g" ^^ args_pp
+      in
+      let make_variant (Tu_aux (Tu_ty_id (typ,id),_)) =
+        let arg_typs = match typ with
+          | Typ_aux (Typ_fn (Typ_aux (Typ_tup typs,_),_,_),_) -> typs
+          | Typ_aux (Typ_fn (typ,_,_),_) -> [typ]
+          | Typ_aux (Typ_tup typs,_) -> typs
+          | _ -> [typ]
+        in
+        parens (string "fun g -> " ^^ zencode_upper ctx id ^^ space ^^
+          parens (separate_map (string ", ") make_subgen arg_typs))
+      in
+      let make_args tqs =
+        string "g" ^^
+        match quant_kopts tqs with
+        | [] -> empty
+        | kopts ->
+           space ^^
+             separate_map space (fun kdid -> mk_arg (kopt_kid kdid)) kopts
+      in
+      let tqs, body =
+        let TD_aux (td,(l,_)) = Bindings.find id typemap in
+        match td with
+        | TD_abbrev (_,_,TypSchm_aux (TypSchm_ts (tqs,typ),_)) ->
+           tqs, gen_type typ
+        | TD_variant (_,_,tqs,variants,_) ->
+           tqs, string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^
+                  separate_map (string ";" ^^ break 1) make_variant variants) ^^
+                    break 0) ^^
+                    string "] in c g"
+        | TD_enum (_,_,variants,_) ->
+           TypQ_aux (TypQ_no_forall, Parse_ast.Unknown),
+           string "rand_choice [" ^^ group (nest 2 (break 0 ^^
+             separate_map (string ";" ^^ break 1) (zencode_upper ctx) variants) ^^
+               break 0) ^^
+               string "]"
+        | _ ->
+           raise (Reporting_basic.err_todo l "Generators for records and bitfields not yet supported")
+      in
+      nest 2 (separate space [string "let"; name; make_args tqs; equals] ^^ break 1 ^^
+        body) ^^ hardline
+  in
+  let rand_record_pp =
+    string "let rand_gens : generators = {" ^^ group (nest 2 (break 0 ^^
+      separate_map (string ";" ^^ break 1)
+        (fun id ->
+          string ("gen_" ^ type_name id) ^^ space ^^ equals ^^ space ^^
+            string ("rand_" ^ type_name id)) (IdSet.elements required)) ^^
+        break 0) ^^ string "}" ^^ hardline
+  in
+  gen_record_type_pp ^^ hardline ^^ hardline ^^
+    separate_map hardline make_rand_gen (IdSet.elements required) ^^
+      hardline ^^ rand_record_pp
+
+let ocaml_defs (Defs defs) generator_info =
   let ctx = { register_inits = get_initialize_registers defs;
               externs = get_externs (Defs defs);
               val_specs = val_spec_typs (Defs defs)
@@ -661,10 +870,16 @@ let ocaml_defs (Defs defs) =
       ^^ ocaml_def_end
     else empty
   in
+  let gen_pp =
+    match generator_info with
+    | None -> empty
+    | Some (types, req) -> ocaml_pp_generators ctx defs types (List.map mk_id req)
+  in
   (string "open Sail_lib;;" ^^ hardline)
   ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end)
   ^^ concat (List.map (ocaml_def ctx) defs)
   ^^ empty_reg_init
+  ^^ gen_pp
 
 let ocaml_main spec sail_dir =
   let lines = ref [] in
@@ -685,8 +900,9 @@ let ocaml_main spec sail_dir =
        "  try zmain () with _ -> prerr_endline(\"Exiting due to uncaught exception\")\n";])
   |> String.concat "\n"
 
-let ocaml_pp_defs f defs =
-  ToChannel.pretty 1. 80 f (ocaml_defs defs)
+let ocaml_pp_defs f defs generator_types =
+  ToChannel.pretty 1. 80 f (ocaml_defs defs generator_types)
+
 
 let system_checked str =
   match Unix.system str with
@@ -701,7 +917,7 @@ let system_checked str =
      prerr_endline (str ^ " was stopped by a signal");
      exit 1
 
-let ocaml_compile spec defs =
+let ocaml_compile spec defs generator_types =
   let sail_dir =
     try Sys.getenv "SAIL_DIR" with
     | Not_found ->
@@ -722,7 +938,7 @@ let ocaml_compile spec defs =
   let out_chan = open_out (spec ^ ".ml") in
   if !opt_ocaml_coverage then 
     ignore(Unix.system ("cp -r " ^ sail_dir ^ "/lib/myocamlbuild_coverage.ml myocamlbuild.ml"));
-  ocaml_pp_defs out_chan defs;
+  ocaml_pp_defs out_chan defs generator_types;
   close_out out_chan;
   if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs)
   then
diff --git a/src/sail.ml b/src/sail.ml
index fc01d3b4..9526d6fe 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -71,6 +71,7 @@ let opt_libs_lem = ref ([]:string list)
 let opt_libs_coq = ref ([]:string list)
 let opt_file_arguments = ref ([]:string list)
 let opt_process_elf : string option ref = ref None
+let opt_ocaml_generators = ref ([]:string list)
 
 let options = Arg.align ([
   ( "-o",
@@ -104,6 +105,9 @@ let options = Arg.align ([
   ( "-ocaml-coverage",
     Arg.Set Ocaml_backend.opt_ocaml_coverage,
     " Build ocaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx).");
+  ( "-ocaml_generators",
+    Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators),
+    "<types> produce random generators for the given types");
   ( "-latex",
     Arg.Set opt_print_latex,
     " pretty print the input to latex");
@@ -299,6 +303,12 @@ let main() =
     | None, _ -> ()
     end;
 
+    let ocaml_generator_info =
+      match !opt_ocaml_generators with
+      | [] -> None
+      | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators)
+    in
+
     (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
     begin
       (if !(opt_interactive)
@@ -317,7 +327,7 @@ let main() =
        then
          let ast_ocaml = rewrite_ast_ocaml ast in
          let out = match !opt_file_out with None -> "out" | Some s -> s in
-         Ocaml_backend.ocaml_compile out ast_ocaml
+         Ocaml_backend.ocaml_compile out ast_ocaml ocaml_generator_info
        else ());
       (if !(opt_print_c)
        then
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index fbe700aa..28015945 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -1121,3 +1121,19 @@ let load_raw (paddr, file) =
 
 (* XXX this could count cycles and exit after given limit *)
 let cycle_count () = ()
+
+(* TODO range, atom, register(?), int, nat, bool, real(!), list, string, itself(?) *)
+let rand_zvector (g : 'generators) (size : int) (order : bool) (elem_gen : 'generators -> 'a) : 'a list =
+  List.init size (fun _ -> elem_gen g)
+
+let rand_zbit (g : 'generators) : bit =
+  if Random.bool() then B0 else B1
+
+let rand_zbool (g : 'generators) : bool =
+  Random.bool()
+
+let rand_zunit (g : 'generators) : unit = ()
+
+let rand_choice l =
+  let n = List.length l in
+  List.nth l (Random.int n)
diff --git a/src/type_check.ml b/src/type_check.ml
index 6db08006..765c41f9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -427,6 +427,8 @@ module Env : sig
   val empty : t
 
   val pattern_completeness_ctx : t -> Pattern_completeness.ctx
+
+  val builtin_typs : typquant Bindings.t
 end = struct
   type t =
     { top_val_specs : (typquant * typ) Bindings.t;
diff --git a/src/type_check.mli b/src/type_check.mli
index ff67b765..4fe6711c 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -195,6 +195,8 @@ module Env : sig
   val empty : t
 
   val pattern_completeness_ctx : t -> Pattern_completeness.ctx
+
+  val builtin_typs : typquant Bindings.t
 end
 
 (** Push all the type variables and constraints from a typquant into