From 08cf96137acefba183358c5ed867e18165b79aef Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 2 Oct 2018 10:55:02 +0100 Subject: Rough code to generate random instructions for testing (aimed at RISC-V) --- src/ocaml_backend.ml | 221 +++++++++++++++++++++++++++++++++++++++++++++++++-- src/sail.ml | 6 +- src/sail_lib.ml | 16 ++++ src/type_check.ml | 2 + src/type_check.mli | 2 + 5 files changed, 241 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 479fc821..51c9638a 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -648,7 +648,211 @@ let val_spec_typs (Defs defs) = ignore (vs_typs defs); !typs -let ocaml_defs (Defs defs) = +let orig_types_for_ocaml_generator (Defs defs) = + Some (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 = +let () = print_endline ("Looking at id " ^ string_of_id id) in + 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) = +let () = print_endline ("Looking at " ^ string_of_typ full_typ) in + 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),_)) -> +let () = print_endline ("Looking at alias " ^ string_of_typ typ) in + add_req_from_typ required typ + | TD_record (_, _, _, fields, _) -> +let () = print_endline ("Looking at " ^ string_of_int (List.length fields) ^ " fields") in + List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields + | TD_variant (_, _, _, variants, _) -> +let () = print_endline ("Looking at " ^ string_of_int (List.length variants) ^ " variants") in + List.fold_left (fun req (Tu_aux (Tu_ty_id (typ,_),_)) -> + add_req_from_typ req typ) required variants + | TD_enum _ -> +let () = print_endline "Nothing to do for enum" in +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 ^^ + string ";" + in + let fields = separate hardline (List.map make_gen_field (IdSet.elements required)) in + let gen_record_type_pp = + string "type generators = {" ^^ hardline ^^ fields ^^ hardline ^^ 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" ^^ space ^^ 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 (string ", ") (List.map make_subgen arg_typs))) + in + let make_args tqs = + separate space (string "g":: + List.map (fun kdid -> mk_arg (kopt_kid kdid)) (quant_kopts tqs)) + in + let top_args, body = + let TD_aux (td,_) = Bindings.find id typemap in + match td with + | TD_abbrev (_,_,TypSchm_aux (TypSchm_ts (tqs,typ),_)) -> + make_args tqs, gen_type typ + | TD_variant (_,_,tqs,variants,_) -> + empty, string "let c = rand_choice [" ^^ hardline ^^ + separate (string ";" ^^ hardline) + (List.map make_variant variants) ^^ hardline ^^ + string "] in fun " ^^ make_args tqs ^^ string " -> c () g" ^^ hardline + | TD_enum (_,_,variants,_) -> + empty, + string "let c = rand_choice [" ^^ hardline ^^ + separate (string ";" ^^ hardline) + (List.map (zencode_upper ctx) variants) ^^ hardline ^^ + string "] in fun g -> c ()" ^^ hardline + | _ -> empty, string "TODO" + in + separate space [string "let"; name; top_args] ^^ space ^^ equals ^^ hardline ^^ + body ^^ hardline + in + let rand_record_pp = + string "let rand_gens : generators = {" ^^ hardline ^^ + separate (string ";" ^^ hardline) + (List.map (fun id -> + string ("gen_" ^ type_name id) ^^ space ^^ equals ^^ space ^^ + string ("rand_" ^ type_name id)) (IdSet.elements required)) ^^ + hardline ^^ string "}" ^^ hardline + in + gen_record_type_pp ^^ hardline ^^ hardline ^^ + separate hardline (List.map make_rand_gen (IdSet.elements required)) ^^ + rand_record_pp + +let ocaml_defs (Defs defs) generator_types = let ctx = { register_inits = get_initialize_registers defs; externs = get_externs (Defs defs); val_specs = val_spec_typs (Defs defs) @@ -661,10 +865,16 @@ let ocaml_defs (Defs defs) = ^^ ocaml_def_end else empty in + let gen_pp = + match generator_types with + | None -> empty + | Some types -> ocaml_pp_generators ctx defs types [mk_id "ast"] + 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 +895,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 +912,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 +933,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..b535d1d3 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -299,6 +299,10 @@ let main() = | None, _ -> () end; + let orig_types_for_ocaml_generator = + Ocaml_backend.orig_types_for_ocaml_generator ast + in + (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) begin (if !(opt_interactive) @@ -317,7 +321,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 orig_types_for_ocaml_generator else ()); (if !(opt_print_c) then diff --git a/src/sail_lib.ml b/src/sail_lib.ml index fbe700aa..22f55e62 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 + fun () -> (List.nth l (Random.int n)) diff --git a/src/type_check.ml b/src/type_check.ml index 0e9f7dd8..71028f96 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 -- cgit v1.2.3 From 7bd3001e2490741388421353ac2e7e687db62d38 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 2 Oct 2018 11:39:15 +0100 Subject: Trigger random generator generation with a command line option --- src/ocaml_backend.ml | 10 +++++----- src/sail.ml | 12 +++++++++--- 2 files changed, 14 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 51c9638a..0da745ae 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -649,9 +649,9 @@ let val_spec_typs (Defs defs) = !typs let orig_types_for_ocaml_generator (Defs defs) = - Some (Util.map_filter (function + Util.map_filter (function | DEF_type td -> Some td - | _ -> None) defs) + | _ -> None) defs let ocaml_pp_generators ctx defs orig_types required = let add_def typemap td = @@ -852,7 +852,7 @@ required separate hardline (List.map make_rand_gen (IdSet.elements required)) ^^ rand_record_pp -let ocaml_defs (Defs defs) generator_types = +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) @@ -866,9 +866,9 @@ let ocaml_defs (Defs defs) generator_types = else empty in let gen_pp = - match generator_types with + match generator_info with | None -> empty - | Some types -> ocaml_pp_generators ctx defs types [mk_id "ast"] + | 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) diff --git a/src/sail.ml b/src/sail.ml index b535d1d3..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), + " produce random generators for the given types"); ( "-latex", Arg.Set opt_print_latex, " pretty print the input to latex"); @@ -299,8 +303,10 @@ let main() = | None, _ -> () end; - let orig_types_for_ocaml_generator = - Ocaml_backend.orig_types_for_ocaml_generator ast + 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*) @@ -321,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 orig_types_for_ocaml_generator + Ocaml_backend.ocaml_compile out ast_ocaml ocaml_generator_info else ()); (if !(opt_print_c) then -- cgit v1.2.3 From 90f1b17f64d640f37de8f2f9fe4043d2bc45145c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 2 Oct 2018 11:55:37 +0100 Subject: Remove some old debugging messages --- src/ocaml_backend.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 0da745ae..0fe10401 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -660,7 +660,6 @@ let ocaml_pp_generators ctx defs orig_types required = 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 = -let () = print_endline ("Looking at id " ^ string_of_id id) in match Bindings.find id typemap with | td -> add_req_from_td (IdSet.add id required) td | exception Not_found -> @@ -673,7 +672,6 @@ let () = print_endline ("Looking at id " ^ string_of_id id) in 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) = -let () = print_endline ("Looking at " ^ string_of_typ full_typ) in match typ with | Typ_id id -> add_req_from_id required id | Typ_var _ @@ -701,18 +699,13 @@ let () = print_endline ("Looking at " ^ string_of_typ full_typ) in and add_req_from_td required (TD_aux (td,(l,_))) = match td with | TD_abbrev (_, _, TypSchm_aux (TypSchm_ts (_,typ),_)) -> -let () = print_endline ("Looking at alias " ^ string_of_typ typ) in add_req_from_typ required typ | TD_record (_, _, _, fields, _) -> -let () = print_endline ("Looking at " ^ string_of_int (List.length fields) ^ " fields") in List.fold_left (fun req (typ,_) -> add_req_from_typ req typ) required fields | TD_variant (_, _, _, variants, _) -> -let () = print_endline ("Looking at " ^ string_of_int (List.length variants) ^ " variants") in List.fold_left (fun req (Tu_aux (Tu_ty_id (typ,_),_)) -> add_req_from_typ req typ) required variants - | TD_enum _ -> -let () = print_endline "Nothing to do for enum" in -required + | 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 -- cgit v1.2.3 From 2acb11428a4a224b8a468d8f4979cd7a5f655449 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 2 Oct 2018 12:47:07 +0100 Subject: Clean up generator pretty printing --- src/ocaml_backend.ml | 39 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 0fe10401..d608eb38 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -747,12 +747,11 @@ let ocaml_pp_generators ctx defs orig_types required = 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 ^^ - string ";" + gen_tyvars_pp ^^ separate (string " -> ") types in - let fields = separate hardline (List.map make_gen_field (IdSet.elements required)) in + let fields = separate_map (string ";" ^^ break 1) make_gen_field (IdSet.elements required) in let gen_record_type_pp = - string "type generators = {" ^^ hardline ^^ fields ^^ hardline ^^ string "}" + 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 @@ -806,7 +805,7 @@ let ocaml_pp_generators ctx defs orig_types required = | _ -> [typ] in parens (string "fun g -> " ^^ zencode_upper ctx id ^^ space ^^ - parens (separate (string ", ") (List.map make_subgen arg_typs))) + parens (separate_map (string ", ") make_subgen arg_typs)) in let make_args tqs = separate space (string "g":: @@ -818,31 +817,31 @@ let ocaml_pp_generators ctx defs orig_types required = | TD_abbrev (_,_,TypSchm_aux (TypSchm_ts (tqs,typ),_)) -> make_args tqs, gen_type typ | TD_variant (_,_,tqs,variants,_) -> - empty, string "let c = rand_choice [" ^^ hardline ^^ - separate (string ";" ^^ hardline) - (List.map make_variant variants) ^^ hardline ^^ + empty, string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^ + separate_map (string ";" ^^ break 1) make_variant variants) ^^ + break 0) ^^ string "] in fun " ^^ make_args tqs ^^ string " -> c () g" ^^ hardline | TD_enum (_,_,variants,_) -> empty, - string "let c = rand_choice [" ^^ hardline ^^ - separate (string ";" ^^ hardline) - (List.map (zencode_upper ctx) variants) ^^ hardline ^^ + string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^ + separate_map (string ";" ^^ break 1) (zencode_upper ctx) variants) ^^ + break 0) ^^ string "] in fun g -> c ()" ^^ hardline | _ -> empty, string "TODO" in - separate space [string "let"; name; top_args] ^^ space ^^ equals ^^ hardline ^^ - body ^^ hardline + hang 2 (separate space [string "let"; name; top_args] ^^ space ^^ equals ^^ break 1 ^^ + body) ^^ hardline in let rand_record_pp = - string "let rand_gens : generators = {" ^^ hardline ^^ - separate (string ";" ^^ hardline) - (List.map (fun id -> - string ("gen_" ^ type_name id) ^^ space ^^ equals ^^ space ^^ - string ("rand_" ^ type_name id)) (IdSet.elements required)) ^^ - hardline ^^ string "}" ^^ hardline + 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 hardline (List.map make_rand_gen (IdSet.elements required)) ^^ + separate_map hardline make_rand_gen (IdSet.elements required) ^^ rand_record_pp let ocaml_defs (Defs defs) generator_info = -- cgit v1.2.3 From 9cd621d347b7d6082dc640adc24b7809fd2dab39 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 2 Oct 2018 14:35:58 +0100 Subject: Tidy up some whitespace --- src/ocaml_backend.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index d608eb38..097aab79 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -795,7 +795,7 @@ let ocaml_pp_generators ctx defs orig_types required = in let args_pp = match args_pp with [] -> empty | _ -> space ^^ separate space args_pp - in string ("g.gen_" ^ typ_str) ^^ space ^^ string "g" ^^ 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 @@ -815,21 +815,21 @@ let ocaml_pp_generators ctx defs orig_types required = let TD_aux (td,_) = Bindings.find id typemap in match td with | TD_abbrev (_,_,TypSchm_aux (TypSchm_ts (tqs,typ),_)) -> - make_args tqs, gen_type typ + space ^^ make_args tqs, gen_type typ | TD_variant (_,_,tqs,variants,_) -> empty, string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^ separate_map (string ";" ^^ break 1) make_variant variants) ^^ break 0) ^^ - string "] in fun " ^^ make_args tqs ^^ string " -> c () g" ^^ hardline + string "] in fun " ^^ make_args tqs ^^ string " -> c () g" | TD_enum (_,_,variants,_) -> empty, string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^ separate_map (string ";" ^^ break 1) (zencode_upper ctx) variants) ^^ break 0) ^^ - string "] in fun g -> c ()" ^^ hardline + string "] in fun g -> c ()" | _ -> empty, string "TODO" in - hang 2 (separate space [string "let"; name; top_args] ^^ space ^^ equals ^^ break 1 ^^ + nest 2 (string "let" ^^ space ^^ name ^^ top_args ^^ space ^^ equals ^^ break 1 ^^ body) ^^ hardline in let rand_record_pp = @@ -842,7 +842,7 @@ let ocaml_pp_generators ctx defs orig_types required = in gen_record_type_pp ^^ hardline ^^ hardline ^^ separate_map hardline make_rand_gen (IdSet.elements required) ^^ - rand_record_pp + hardline ^^ rand_record_pp let ocaml_defs (Defs defs) generator_info = let ctx = { register_inits = get_initialize_registers defs; -- cgit v1.2.3 From f0d2765b19f710608153702303a20cbf0d342ed9 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 3 Oct 2018 12:25:34 +0100 Subject: Drop unnecessary thunking; more trouble than it's worth --- src/ocaml_backend.ml | 26 +++++++++++++++----------- src/sail_lib.ml | 2 +- 2 files changed, 16 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 097aab79..1d6954ce 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -808,28 +808,32 @@ let ocaml_pp_generators ctx defs orig_types required = parens (separate_map (string ", ") make_subgen arg_typs)) in let make_args tqs = - separate space (string "g":: - List.map (fun kdid -> mk_arg (kopt_kid kdid)) (quant_kopts tqs)) + string "g" ^^ + match quant_kopts tqs with + | [] -> empty + | kopts -> + space ^^ + separate_map space (fun kdid -> mk_arg (kopt_kid kdid)) kopts in - let top_args, body = + let tqs, body = let TD_aux (td,_) = Bindings.find id typemap in match td with | TD_abbrev (_,_,TypSchm_aux (TypSchm_ts (tqs,typ),_)) -> - space ^^ make_args tqs, gen_type typ + tqs, gen_type typ | TD_variant (_,_,tqs,variants,_) -> - empty, string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^ + tqs, string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^ separate_map (string ";" ^^ break 1) make_variant variants) ^^ break 0) ^^ - string "] in fun " ^^ make_args tqs ^^ string " -> c () g" + string "] in c g" | TD_enum (_,_,variants,_) -> - empty, - string "let c = rand_choice [" ^^ group (nest 2 (break 0 ^^ + 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 "] in fun g -> c ()" - | _ -> empty, string "TODO" + string "]" + | _ -> TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), string "TODO" in - nest 2 (string "let" ^^ space ^^ name ^^ top_args ^^ space ^^ equals ^^ break 1 ^^ + nest 2 (separate space [string "let"; name; make_args tqs; equals] ^^ break 1 ^^ body) ^^ hardline in let rand_record_pp = diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 22f55e62..28015945 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -1136,4 +1136,4 @@ let rand_zunit (g : 'generators) : unit = () let rand_choice l = let n = List.length l in - fun () -> (List.nth l (Random.int n)) + List.nth l (Random.int n) -- cgit v1.2.3 From 94ed5ae4b5e185e40b4bf6fbeb89cb7fe01b53ef Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 4 Oct 2018 11:50:36 +0100 Subject: Bit of commentary, proper TODO error --- src/ocaml_backend.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 1d6954ce..23e27e2b 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -648,6 +648,14 @@ let val_spec_typs (Defs defs) = ignore (vs_typs defs); !typs +(* 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 @@ -816,7 +824,7 @@ let ocaml_pp_generators ctx defs orig_types required = separate_map space (fun kdid -> mk_arg (kopt_kid kdid)) kopts in let tqs, body = - let TD_aux (td,_) = Bindings.find id typemap in + 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 @@ -831,7 +839,8 @@ let ocaml_pp_generators ctx defs orig_types required = separate_map (string ";" ^^ break 1) (zencode_upper ctx) variants) ^^ break 0) ^^ string "]" - | _ -> TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), string "TODO" + | _ -> + 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 -- cgit v1.2.3