diff --git a/lib/json/sail_config.c b/lib/json/sail_config.c index 27ce02020..2f69c7c6b 100644 --- a/lib/json/sail_config.c +++ b/lib/json/sail_config.c @@ -29,6 +29,8 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /****************************************************************************/ +#include + #include "sail_config.h" #include "cJSON.h" @@ -76,12 +78,11 @@ void sail_config_cleanup(void) sail_free(sail_config); } -void sail_config_get_string(sail_string *str, size_t n, const char *key[]) +sail_config_json sail_config_get(size_t n, const char *key[]) { + sail_config_json result; cJSON *json = (cJSON *)sail_config; - sail_free(*str); - for (int i = 0; i < n; i++) { if (cJSON_IsObject(json)) { json = cJSON_GetObjectItemCaseSensitive(json, key[i]); @@ -90,27 +91,26 @@ void sail_config_get_string(sail_string *str, size_t n, const char *key[]) } } - if (cJSON_IsString(json)) { - *str = cJSON_GetStringValue(json); - } else { - sail_assert(false, "Expected string value in config"); - } + return (sail_config_json)json; } -sail_config_json sail_config_get(size_t n, const char *key[]) +int64_t sail_config_list_length(const sail_config_json config) { - sail_config_json result; - cJSON *json = (cJSON *)sail_config; + cJSON *json = (cJSON *)config; - for (int i = 0; i < n; i++) { - if (cJSON_IsObject(json)) { - json = cJSON_GetObjectItemCaseSensitive(json, key[i]); - } else { - sail_assert(false, "Failed to access config item"); - } + if (cJSON_IsArray(json)) { + return (int64_t)cJSON_GetArraySize(json); + } else { + return INT64_C(-1); } +} - return (sail_config_json)json; +sail_config_json sail_config_list_nth(const sail_config_json config, int64_t index) +{ + // This is very inefficient, but works with how the Jib IR functions + cJSON *json = (cJSON *)config; + cJSON *item = cJSON_GetArrayItem(json, (int)index); + return (sail_config_json)item; } bool sail_config_is_object(const sail_config_json config) @@ -169,7 +169,11 @@ bool sail_config_is_bool_array_with_size(const sail_config_json config, mach_int void sail_config_unwrap_string(sail_string *str, const sail_config_json config) { - *str = cJSON_GetStringValue((cJSON *)config); + sail_string conf_str = cJSON_GetStringValue((cJSON *)config); + + size_t len = strlen(conf_str); + *str = (sail_string)realloc(*str, len + 1); + *str = strcpy(*str, conf_str); } void sail_config_unwrap_int(sail_int *n, const sail_config_json config) diff --git a/lib/json/sail_config.h b/lib/json/sail_config.h index f664353fe..25e005dea 100644 --- a/lib/json/sail_config.h +++ b/lib/json/sail_config.h @@ -67,27 +67,26 @@ void sail_config_set_file(const char *path); void sail_config_cleanup(); /* - * Extract a string value from the JSON configuration. + * Get the JSON corresponding to some key */ -void sail_config_get_string(sail_string *str, const size_t n, const_sail_string key[]); +sail_config_json sail_config_get(const size_t n, const_sail_string key[]); /* - * For more complex Sail types than just strings, Sail will generate code that will - * destructure the JSON values using the following function calls. + * For each Sail type, Sail will generate code that will destructure + * the JSON values using the following function calls. * * In general, it will test if the JSON is the type it expects, and * only then access the fields. The behaviour of these functions is * not guaranteed if the JSON does not have the correct type. */ -sail_config_json sail_config_get(const size_t n, const_sail_string key[]); - bool sail_config_is_object(const sail_config_json config); - bool sail_config_object_has_key(const sail_config_json config, const sail_string key); - sail_config_json sail_config_object_key(const sail_config_json config, const sail_string key); +int64_t sail_config_list_length(const sail_config_json config); +sail_config_json sail_config_list_nth(const sail_config_json config, int64_t index); + bool sail_config_is_string(const sail_config_json config); bool sail_config_is_array(const sail_config_json config); @@ -95,9 +94,7 @@ bool sail_config_is_bool_array(const sail_config_json config); bool sail_config_is_bool_array_with_size(const sail_config_json config, mach_int expected); void sail_config_unwrap_string(sail_string *str, const sail_config_json config); - void sail_config_unwrap_int(sail_int *n, const sail_config_json config); - void sail_config_unwrap_bits(lbits *bv, const sail_config_json config); #ifdef __cplusplus diff --git a/lib/sail.h b/lib/sail.h index e035b9218..79ae6956e 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -147,7 +147,6 @@ bool EQUAL(sail_string)(const_sail_string, const_sail_string); void concat_str(sail_string *stro, const_sail_string str1, const_sail_string str2); bool string_startswith(const_sail_string s, const_sail_string prefix); - /* ***** Sail integers ***** */ typedef int64_t mach_int; diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 3c8e70fab..0e1c1b699 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -76,6 +76,8 @@ let opt_format_backup : string option ref = ref None let opt_format_only : string list ref = ref [] let opt_format_skip : string list ref = ref [] let opt_slice_instantiation_types : bool ref = ref false +let opt_output_schema_file : string option ref = ref None + let is_bytecode = Sys.backend_type = Bytecode (* Allow calling all options as either -foo_bar, -foo-bar, or @@ -252,6 +254,10 @@ let rec options = ("-all_modules", Arg.Set opt_all_modules, " use all modules in project file"); ("-list_files", Arg.Set Frontend.opt_list_files, " list files used in all project files"); ("-config", Arg.String (fun file -> opt_config_file := Some file), " configuration file"); + ( "-output-schema", + Arg.String (fun file -> opt_output_schema_file := Some file), + " output configuration schema" + ); ("-abstract_types", Arg.Set Initial_check.opt_abstract_types, " (experimental) allow abstract types"); ("-fmt", Arg.Set opt_format, " format input source code"); ( "-fmt_backup", @@ -506,11 +512,19 @@ let run_sail (config : Yojson.Safe.t option) tgt = ) in let ast = Frontend.instantiate_abstract_types (Some tgt) !opt_instantiations ast in - let ast = apply_model_config env ast in + let schema, ast = apply_model_config env ast in let ast, env = Frontend.initial_rewrite effect_info env ast in let ast, env = match !opt_splice with [] -> (ast, env) | files -> Splice.splice_files ctx ast (List.rev files) in let effect_info = Effects.infer_side_effects (Target.asserts_termination tgt) ast in + ( match !opt_output_schema_file with + | None -> () + | Some file -> + let out = Util.open_output_with_check file in + Yojson.Safe.pretty_to_channel ~std:true out.channel schema; + Util.close_output_with_check out + ); + (* Don't show warnings during re-writing for now *) Reporting.suppressed_warning_info (); Reporting.opt_warnings := false; diff --git a/src/lib/config.ml b/src/lib/config.ml index e271d7e0f..489a0c88a 100644 --- a/src/lib/config.ml +++ b/src/lib/config.ml @@ -50,38 +50,296 @@ open Rewriter open Type_check module J = Yojson.Safe -module StringMap = Util.StringMap module ConfigTypes : sig + type config_type = { loc : Ast.l; env : env; typ : typ } + type t - val create : unit -> t + val to_schema : t -> J.t - val find_opt : at:Ast.l -> string list -> t -> (Ast.l * typ) option + val create : unit -> t - val update_type : string list -> Ast.l -> typ -> t -> bool + val find_opt : at:Ast.l -> string list -> t -> config_type list option - val insert : string list -> Ast.l -> typ -> t -> unit + val insert : string list -> config_type -> t -> unit end = struct open Util.Option_monad open Error_format - type t = Sail_value of { mutable loc : Ast.l; mutable typ : typ } | Object of (string, t) Hashtbl.t + type config_type = { loc : Ast.l; env : env; typ : typ } + + type schema_logic = + | All_of of schema_logic list + | Any_of of schema_logic list + | Not of schema_logic + | Schema of (string * J.t) list + + let rec logic_type schema_type = function + | All_of schemas -> All_of (List.map (logic_type schema_type) schemas) + | Any_of schemas -> Any_of (List.map (logic_type schema_type) schemas) + | Not schema -> All_of [Schema (schema_type []); Not (logic_type schema_type schema)] + | Schema clauses -> Schema (schema_type clauses) + + let rec logic_to_schema = function + | All_of [schema] -> logic_to_schema schema + | All_of schemas -> `Assoc [("allOf", `List (List.map logic_to_schema schemas))] + | Any_of schemas -> `Assoc [("anyOf", `List (List.map logic_to_schema schemas))] + | Not schema -> `Assoc [("not", logic_to_schema schema)] + | Schema clauses -> `Assoc clauses + + let any_of c1 c2 = + match (c1, c2) with + | Any_of schemas1, Any_of schemas2 -> Any_of (schemas1 @ schemas2) + | Any_of schemas1, _ -> Any_of (schemas1 @ [c2]) + | _, Any_of schemas2 -> Any_of (c1 :: schemas2) + | _ -> Any_of [c1; c2] + + let all_of c1 c2 = + match (c1, c2) with + | Schema clauses1, Schema clauses2 -> Schema (clauses1 @ clauses2) + | All_of schemas1, All_of schemas2 -> All_of (schemas1 @ schemas2) + | All_of schemas1, _ -> All_of (schemas1 @ [c2]) + | _, All_of schemas2 -> All_of (c1 :: schemas2) + | _ -> All_of [c1; c2] + + module type CONSTRAINT = sig + val const : Big_int.num -> (string * J.t) list + val maximum : Big_int.num -> (string * J.t) list + val minimum : Big_int.num -> (string * J.t) list + val exclusive_maximum : Big_int.num -> (string * J.t) list + val exclusive_minimum : Big_int.num -> (string * J.t) list + end + + module SchemaTypeConstraint (Gen : CONSTRAINT) = struct + let rec constraint_schema v (NC_aux (aux, _)) = + match aux with + | NC_equal (A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _), A_aux (A_nexp (Nexp_aux (Nexp_constant c, _)), _)) + | NC_equal (A_aux (A_nexp (Nexp_aux (Nexp_constant c, _)), _), A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)) + when Kid.compare v v' = 0 -> + Some (Schema (Gen.const c)) + | NC_and (nc1, nc2) -> + let* c1 = constraint_schema v nc1 in + let* c2 = constraint_schema v nc2 in + Some (all_of c1 c2) + | NC_or (nc1, nc2) -> + let* c1 = constraint_schema v nc1 in + let* c2 = constraint_schema v nc2 in + Some (any_of c1 c2) + | NC_lt (Nexp_aux (Nexp_var v', _), Nexp_aux (Nexp_constant c, _)) + | NC_gt (Nexp_aux (Nexp_constant c, _), Nexp_aux (Nexp_var v', _)) + when Kid.compare v v' = 0 -> + Some (Schema (Gen.exclusive_maximum c)) + | NC_le (Nexp_aux (Nexp_var v', _), Nexp_aux (Nexp_constant c, _)) + | NC_ge (Nexp_aux (Nexp_constant c, _), Nexp_aux (Nexp_var v', _)) + when Kid.compare v v' = 0 -> + Some (Schema (Gen.maximum c)) + | NC_gt (Nexp_aux (Nexp_var v', _), Nexp_aux (Nexp_constant c, _)) + | NC_lt (Nexp_aux (Nexp_constant c, _), Nexp_aux (Nexp_var v', _)) + when Kid.compare v v' = 0 -> + Some (Schema (Gen.exclusive_minimum c)) + | NC_ge (Nexp_aux (Nexp_var v', _), Nexp_aux (Nexp_constant c, _)) + | NC_le (Nexp_aux (Nexp_constant c, _), Nexp_aux (Nexp_var v', _)) + when Kid.compare v v' = 0 -> + Some (Schema (Gen.minimum c)) + | NC_true -> Some (Schema []) + | NC_false -> Some (Not (Schema [])) + | NC_app (id, [A_aux (A_bool nc, _)]) when string_of_id id = "not" -> + let* c = constraint_schema v nc in + Some (Not c) + | NC_set (Nexp_aux (Nexp_var v', _), set) when Kid.compare v v' = 0 -> + Some (Any_of (List.map (fun n -> Schema (Gen.const n)) set)) + | _ -> None + end + + module IntegerConstraint = SchemaTypeConstraint (struct + let const n = [("const", `Intlit (Big_int.to_string n))] + let maximum n = [("maximum", `Intlit (Big_int.to_string n))] + let minimum n = [("minimum", `Intlit (Big_int.to_string n))] + let exclusive_maximum n = [("exclusiveMaximum", `Intlit (Big_int.to_string n))] + let exclusive_minimum n = [("exclusiveMinimum", `Intlit (Big_int.to_string n))] + end) + + let array_constraint ?min_length ?max_length () = + Util.option_these + [ + Option.map (fun len -> ("minItems", `Intlit (Big_int.to_string len))) min_length; + Option.map (fun len -> ("maxItems", `Intlit (Big_int.to_string len))) max_length; + ] + + module ArrayConstraint = SchemaTypeConstraint (struct + let const n = array_constraint ~min_length:n ~max_length:n () + let maximum n = array_constraint ~max_length:n () + let minimum n = array_constraint ~min_length:n () + let exclusive_maximum n = array_constraint ~max_length:(Big_int.pred n) () + let exclusive_minimum n = array_constraint ~min_length:(Big_int.succ n) () + end) + + let bitvector_string_literal = + `Assoc + [ + ( "oneOf", + `List + [ + `Assoc [("type", `String "string"); ("pattern", `String "^0x[0-9a-fA-F_]+$")]; + `Assoc [("type", `String "string"); ("pattern", `String "^0b[0-1_]+$")]; + `Assoc [("type", `String "string"); ("pattern", `String "^[0-9_]+$")]; + ] + ); + ] + + let type_schema { loc; env; typ } = + let rec generate typ = + let kopts, nc, typ = + match destruct_exist typ with None -> ([], nc_true, typ) | Some destructure -> destructure + in + match (kopts, nc, typ) with + | _, _, Typ_aux (Typ_app (id, [A_aux (A_nexp arg, _)]), _) when string_of_id id = "atom" -> ( + let schema_integer clauses = ("type", `String "integer") :: clauses in + match (kopts, nc, arg) with + | [], NC_aux (NC_true, _), nexp -> + let* c = solve_unique env nexp in + Some (`Assoc (schema_integer [("const", `Intlit (Big_int.to_string c))])) + | [KOpt_aux (KOpt_kind (_, v), _)], nc, Nexp_aux (Nexp_var v', _) when Kid.compare v v' = 0 -> + let* nc_logic = + nc |> constraint_simp |> IntegerConstraint.constraint_schema v |> Option.map (logic_type schema_integer) + in + Some (logic_to_schema nc_logic) + | _ -> None + ) + | [], NC_aux (NC_true, _), Typ_aux (Typ_app (id, _), _) when string_of_id id = "atom_bool" -> + Some (`Assoc [("type", `String "boolean")]) + | [], NC_aux (NC_true, _), Typ_aux (Typ_id id, _) -> ( + match string_of_id id with + | "string" -> Some (`Assoc [("type", `String "string")]) + | "unit" -> Some (`Assoc [("type", `String "null")]) + | _ -> None + ) + | _, _, Typ_aux (Typ_app (id, [A_aux (A_nexp arg, _)]), _) when string_of_id id = "bitvector" -> ( + let schema_bool_array clauses = + [("type", `String "array"); ("items", `Assoc [("type", `String "boolean")])] @ clauses + in + let schema_hex_object clauses = + [ + ("type", `String "object"); + ( "properties", + `Assoc [("len", `Assoc (("type", `String "integer") :: clauses)); ("value", bitvector_string_literal)] + ); + ("required", `List [`String "len"; `String "value"]); + ("additionalProperties", `Bool false); + ] + in + match (kopts, nc, arg) with + | [], NC_aux (NC_true, _), nexp -> + let* c = solve_unique env nexp in + Some + (`Assoc + [ + ( "oneOf", + `List + [ + `Assoc (schema_bool_array (array_constraint ~min_length:c ~max_length:c ())); + `Assoc (schema_hex_object [("const", `Intlit (Big_int.to_string c))]); + ] + ); + ] + ) + | [KOpt_aux (KOpt_kind (_, v), _)], nc, Nexp_aux (Nexp_var v', _) when Kid.compare v v' = 0 -> + let* bool_array_nc_logic = + nc |> constraint_simp |> ArrayConstraint.constraint_schema v |> Option.map (logic_type schema_bool_array) + in + let* hex_object_nc_logic = + nc |> constraint_simp |> IntegerConstraint.constraint_schema v + |> Option.map (logic_type schema_hex_object) + in + Some (`Assoc [("oneOf", `List [logic_to_schema bool_array_nc_logic; logic_to_schema hex_object_nc_logic])]) + | _ -> None + ) + | _, _, Typ_aux (Typ_app (id, [A_aux (A_nexp arg, _); A_aux (A_typ item_typ, _)]), _) + when string_of_id id = "vector" -> ( + let* schema_items = generate item_typ in + let schema_array clauses = [("type", `String "array"); ("items", schema_items)] @ clauses in + match (kopts, nc, arg) with + | [], NC_aux (NC_true, _), nexp -> + let* c = solve_unique env nexp in + Some (`Assoc (schema_array (array_constraint ~min_length:c ~max_length:c ()))) + | [KOpt_aux (KOpt_kind (_, v), _)], nc, Nexp_aux (Nexp_var v', _) when Kid.compare v v' = 0 -> + let* nc_logic = + nc |> constraint_simp |> ArrayConstraint.constraint_schema v |> Option.map (logic_type schema_array) + in + Some (logic_to_schema nc_logic) + | _ -> None + ) + | [], NC_aux (NC_true, _), Typ_aux (Typ_app (id, [A_aux (A_typ item_typ, _)]), _) when string_of_id id = "list" -> + let* schema_items = generate item_typ in + let schema_array clauses = [("type", `String "array"); ("items", schema_items)] @ clauses in + Some (`Assoc (schema_array (array_constraint ()))) + | _ -> None + in + let* json = generate typ in + (* The non-Assoc case here should perhaps be an error (or None), as this + function should always generate a schema object. *) + match json with + | `Assoc obj -> Some (`Assoc (("description", `String (Reporting.short_loc_to_string loc)) :: obj)) + | json -> Some json + + let type_schema_or_error config_type = + match type_schema config_type with + | Some schema -> schema + | None -> + raise + (Reporting.err_typ config_type.loc + ("Failed to generate JSON Schema for configuration type " ^ string_of_typ config_type.typ) + ) + + type t = Sail_value of config_type * config_type list | Object of (string, t) Hashtbl.t + + let rec to_schema = function + | Object tbl -> + let properties = + Hashtbl.fold + (fun key value props -> + let schema = to_schema value in + (key, schema) :: props + ) + tbl [] + in + let properties = List.sort (fun (p1, _) (p2, _) -> String.compare p1 p2) properties in + let required = ("required", `List (List.map (fun (p, _) -> `String p) properties)) in + `Assoc (("type", `String "object") :: required :: properties) + | Sail_value (config_type, []) -> type_schema_or_error config_type + | Sail_value (config_type, config_types) -> + let schemas = config_type :: config_types |> List.map type_schema_or_error in + `Assoc [("allOf", `List schemas)] (* Random is false here for deterministic error messages *) let create () = Object (Hashtbl.create ~random:false 16) let rec get_example = function - | Sail_value { loc; typ } -> Some (loc, typ) + | Sail_value ({ loc; typ; _ }, _) -> Some (loc, typ) | Object tbl -> Hashtbl.fold (fun _ value acc -> if Option.is_none acc then get_example value else acc) tbl None + let subkey_error l full_parts obj = + let full_parts = String.concat "." full_parts in + let extra_info msg = + match get_example obj with + | Some (l, typ) -> Seq [msg; Line ""; Line "For example:"; Location ("", Some "used here", l, Seq [])] + | None -> msg + in + let msg = + Line (Printf.sprintf "Attempting to access key %s, but various subkeys have already been used" full_parts) + in + let b = Buffer.create 1024 in + format_message (extra_info msg) (buffer_formatter b); + raise (Reporting.err_general l (Buffer.contents b)) + let find_opt ~at:l full_parts map = let rec go parts map = match (parts, map) with | part :: parts, Object tbl -> let* map = Hashtbl.find_opt tbl part in go parts map - | part :: _, Sail_value { loc; typ } -> + | part :: _, Sail_value ({ loc; typ; _ }, _) -> let msg = Seq [ @@ -96,45 +354,31 @@ end = struct let b = Buffer.create 1024 in format_message msg (buffer_formatter b); raise (Reporting.err_typ l (Buffer.contents b)) - | [], Sail_value { loc; typ } -> Some (loc, typ) - | [], obj -> - let full_parts = String.concat "." full_parts in - let extra_info msg = - match get_example obj with - | Some (l, typ) -> Seq [msg; Line ""; Line "For example:"; Location ("", Some "used here", l, Seq [])] - | None -> msg - in - let msg = - Line (Printf.sprintf "Attempting to access key %s, but various subkeys have already been used" full_parts) - in - let b = Buffer.create 1024 in - format_message (extra_info msg) (buffer_formatter b); - raise (Reporting.err_general l (Buffer.contents b)) + | [], Sail_value (hd_types, tl_types) -> Some (hd_types :: tl_types) + | [], obj -> subkey_error l full_parts obj in go full_parts map - let rec insert parts l typ map = - match (parts, map) with - | [part], Object tbl -> Hashtbl.replace tbl part (Sail_value { loc = l; typ }) - | part :: parts, Object tbl -> ( - match Hashtbl.find_opt tbl part with - | Some map -> insert parts l typ map - | None -> - Hashtbl.add tbl part (create ()); - insert (part :: parts) l typ map - ) - | _ -> Reporting.unreachable l __POS__ "Failed to insert into config type map" - - let rec update_type parts l typ map = - match (parts, map) with - | part :: parts, Object tbl -> ( - match Hashtbl.find_opt tbl part with Some map -> update_type parts l typ map | None -> false - ) - | [], Sail_value v -> - v.loc <- l; - v.typ <- typ; - true - | _ -> false + let insert full_parts config_type map = + let rec go parts map = + match (parts, map) with + | [part], Object tbl -> ( + match Hashtbl.find_opt tbl part with + | None -> Hashtbl.add tbl part (Sail_value (config_type, [])) + | Some (Sail_value (h_types, t_types)) -> + Hashtbl.replace tbl part (Sail_value (config_type, h_types :: t_types)) + | Some obj -> subkey_error config_type.loc full_parts obj + ) + | part :: parts, Object tbl -> ( + match Hashtbl.find_opt tbl part with + | Some map -> go parts map + | None -> + Hashtbl.add tbl part (create ()); + go (part :: parts) map + ) + | _ -> Reporting.unreachable config_type.loc __POS__ "Failed to insert into config type map" + in + go full_parts map end let find_json ~at:l full_parts json = @@ -157,50 +401,112 @@ let json_bit ~at:l = function | `Bool false -> '0' | json -> raise (Reporting.err_general l (Printf.sprintf "Failed to interpret %s as a bit" (J.to_string json))) -let sail_exp_from_json ~at:l env typ = function +let json_to_int = function `Int n -> Some n | _ -> None + +let json_to_string = function `String s -> Some s | _ -> None + +let valid_bin_char c = match c with '_' -> None | ('0' | '1') as c -> Some (Some c) | _ -> Some None + +let valid_dec_char c = + match c with + | '_' -> None + | ('0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9') as c -> Some (Some c) + | _ -> Some None + +let valid_hex_char c = + match Char.uppercase_ascii c with + | '_' -> None + | ('0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | 'A' | 'B' | 'C' | 'D' | 'E' | 'F') as c -> Some (Some c) + | _ -> Some None + +let hex_char_to_bits c = + match Sail2_values.nibble_of_char c with Some (b1, b2, b3, b4) -> [b1; b2; b3; b4] | None -> [] + +let bin_char_to_bit c = match c with '0' -> Sail2_values.B0 | '1' -> Sail2_values.B0 | _ -> Sail2_values.BU + +let fix_length ~at:l ~len bitlist = + let d = len - List.length bitlist in + if d = 0 then bitlist + else if d > 0 then Sail2_operators_bitlists.zero_extend bitlist (Big_int.of_int d) + else ( + Reporting.warn ~force_show:true "Configuration" l "Forced to truncate configuration bitvector literal"; + Util.drop d bitlist + ) + +let bitlist_to_string bitlist = List.map Sail2_values.bitU_char bitlist |> List.to_seq |> String.of_seq + +let parse_json_string_to_bits ~at:l ~len str = + let open Util.Option_monad in + let open Sail2_operators_bitlists in + let str_len = String.length str in + let chars = str |> String.to_seq |> List.of_seq in + let* bitlist = + if str_len > 2 && String.sub str 0 2 = "0b" then + let* bin_chars = Util.drop 2 chars |> List.filter_map valid_bin_char |> Util.option_all in + Some (List.map bin_char_to_bit bin_chars |> fix_length ~at:l ~len) + else if str_len > 2 && String.sub str 0 2 = "0x" then + let* hex_chars = Util.drop 2 chars |> List.filter_map valid_hex_char |> Util.option_all in + Some (List.map hex_char_to_bits hex_chars |> List.concat |> fix_length ~at:l ~len) + else + let* dec_chars = Util.drop 2 chars |> List.filter_map valid_hex_char |> Util.option_all in + let n = List.to_seq dec_chars |> String.of_seq |> Big_int.of_string in + Some (get_slice_int (Big_int.of_int len) n Big_int.zero) + in + Some (mk_lit_exp ~loc:l (L_bin (bitlist_to_string bitlist))) + +let rec sail_exp_from_json ~at:l env typ = + let open Util.Option_monad in + function | `Int n -> mk_lit_exp ~loc:l (L_num (Big_int.of_int n)) | `Intlit n -> mk_lit_exp ~loc:l (L_num (Big_int.of_string n)) | `String s -> if Option.is_some (Type_check.destruct_numeric typ) then mk_lit_exp ~loc:l (L_num (Big_int.of_string s)) else mk_lit_exp ~loc:l (L_string s) - | `List jsons when Option.is_some (Type_check.destruct_bitvector env typ) -> - L_bin (List.map (json_bit ~at:l) jsons |> List.to_seq |> String.of_seq) |> mk_lit_exp ~loc:l + | `Bool true -> mk_lit_exp ~loc:l L_true + | `Bool false -> mk_lit_exp ~loc:l L_false + | `List jsons -> ( + let base_typ = match destruct_exist typ with None -> typ | Some (_, _, typ) -> typ in + match base_typ with + | Typ_aux (Typ_app (id, args), _) -> ( + match (string_of_id id, args) with + | "bitvector", _ -> + L_bin (List.map (json_bit ~at:l) jsons |> List.to_seq |> String.of_seq) |> mk_lit_exp ~loc:l + | "vector", [_; A_aux (A_typ item_typ, _)] -> + let items = List.map (sail_exp_from_json ~at:l env item_typ) jsons in + mk_exp ~loc:l (E_vector items) + | "list", [A_aux (A_typ item_typ, _)] -> + let items = List.map (sail_exp_from_json ~at:l env item_typ) jsons in + mk_exp ~loc:l (E_list items) + | _ -> raise (Reporting.err_general l ("Failed to interpret JSON list as Sail type " ^ string_of_typ typ)) + ) + | _ -> raise (Reporting.err_general l ("Failed to interpret JSON list as Sail type " ^ string_of_typ typ)) + ) + | `Assoc obj -> ( + let base_typ = match destruct_exist typ with None -> typ | Some (_, _, typ) -> typ in + let exp_opt = + match base_typ with + | Typ_aux (Typ_app (id, args), _) -> ( + match (string_of_id id, args) with + | "bitvector", _ -> + let* len = Option.bind (List.assoc_opt "len" obj) json_to_int in + let* value = Option.bind (List.assoc_opt "value" obj) json_to_string in + parse_json_string_to_bits ~at:l ~len value + | _ -> None + ) + | _ -> None + in + match exp_opt with + | Some exp -> exp + | None -> raise (Reporting.err_general l ("Failed to interpret JSON object as Sail type " ^ string_of_typ typ)) + ) | _ -> assert false let rewrite_exp global_env types json (aux, annot) = match aux with | E_config parts -> ( + let env = env_of_annot annot in let typ = typ_of_annot annot in - let typ = - match ConfigTypes.find_opt ~at:(fst annot) parts types with - | Some (prev_l, prev_typ) -> - if subtype_check global_env prev_typ typ then prev_typ - else if subtype_check global_env typ prev_typ then ( - let (_ : bool) = ConfigTypes.update_type parts (fst annot) typ types in - typ - ) - else - let open Error_format in - let msg = - Seq - [ - Line "Incompatible types for configuration option found:"; - List - [ - ("Type " ^ string_of_typ typ ^ " found here", Seq []); - ("Type " ^ string_of_typ prev_typ ^ " found as previous type", Seq []); - ]; - Line ""; - Location ("", Some "previous type found here", prev_l, Seq []); - ] - in - let b = Buffer.create 1024 in - format_message msg (buffer_formatter b); - raise (Reporting.err_typ (fst annot) (Buffer.contents b)) - | None -> - ConfigTypes.insert parts (fst annot) typ types; - typ - in + ConfigTypes.insert parts { loc = fst annot; env; typ } types; match find_json ~at:(fst annot) parts json with | None -> E_aux (aux, annot) | Some json -> ( @@ -215,4 +521,6 @@ let rewrite_exp global_env types json (aux, annot) = let rewrite_ast global_env json ast = let types = ConfigTypes.create () in let alg = { id_exp_alg with e_aux = rewrite_exp global_env types json } in - rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast + let ast = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in + let schema = ConfigTypes.to_schema types in + (schema, ast) diff --git a/src/lib/config.mli b/src/lib/config.mli index ec0825ac4..5714f0e90 100644 --- a/src/lib/config.mli +++ b/src/lib/config.mli @@ -44,6 +44,39 @@ (* SPDX-License-Identifier: BSD-2-Clause *) (****************************************************************************) +(** Sail model configuration using JSON. *) + open Type_check -val rewrite_ast : env -> Yojson.Safe.t -> typed_ast -> typed_ast +(** Rewrite any any configuration nodes in the AST, and gather + configuration information. + + This rewrite performs two operations: + + First, It takes a JSON configuration file as input and replaces + E_config nodes within the AST using information within that JSON. + For example: + + {@sail[ + config a.b.c : T + ]} + + will cause [a.b.c] to be looked up in the provided JSON and + whatever JSON value is at that key will be interpreted as the type + [T] and inserted in the AST. + + If [a.b.c] does not exist, then the E_config node will remain to + be instantiated by a configuration value at runtime. + + Second, for each type [T] attached to a configuration node (which + may have been inferred from context by the type system), we will + also attempt to synthesise a JSON Schema. If [T] cannot be turned + into a valid schema then this function raises a fatal type error + exception. This schema cannot capture every possible invariant of + an ISA configuration, but it does provide enough to guarantee that + a configuration applied at runtime will not break type-safety + assuming it validates against the schema. + + The function will return that JSON schema alongside the re-written + AST. *) +val rewrite_ast : env -> Yojson.Safe.t -> typed_ast -> Yojson.Safe.t * typed_ast diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index b2140b324..a74d0b2f9 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -647,43 +647,156 @@ module Make (C : CONFIG) = struct args in let key_name = ngensym () in + let json = ngensym () in let args = [V_lit (VL_int (Big_int.of_int (List.length key)), CT_fint 64); V_id (key_name, CT_json_key)] in - let key_init = [ijson_key l key_name key] in + let init = + [ + ijson_key l key_name key; + idecl l CT_json json; + iextern l (CL_id (json, CT_json)) (mk_id "sail_config_get", []) args; + ] + in - let config_extract ctyp ~validate ~extract = - let json = ngensym () in + let config_extract ctyp json ~validate ~extract = let valid = ngensym () in let value = ngensym () in - ( key_init - @ [ - idecl l CT_json json; - iextern l (CL_id (json, CT_json)) (mk_id "sail_config_get", []) args; - idecl l CT_bool valid; - iextern l (CL_id (valid, CT_bool)) (mk_id (fst validate), []) ([V_id (json, CT_json)] @ snd validate); - iif l (V_call (Bnot, [V_id (valid, CT_bool)])) [ibad_config l] [] CT_unit; - idecl l ctyp value; - iextern l (CL_id (value, ctyp)) (mk_id extract, []) [V_id (json, CT_json)]; - ], + ( [ + idecl l CT_bool valid; + iextern l (CL_id (valid, CT_bool)) (mk_id (fst validate), []) ([V_id (json, CT_json)] @ snd validate); + iif l (V_call (Bnot, [V_id (valid, CT_bool)])) [ibad_config l] [] CT_unit; + idecl l ctyp value; + iextern l (CL_id (value, ctyp)) (mk_id extract, []) [V_id (json, CT_json)]; + ], (fun clexp -> icopy l clexp (V_id (value, ctyp))), - [iclear ctyp value; iclear CT_json json] + [iclear ctyp value] ) in - match ctyp with - | CT_string -> (key_init, (fun clexp -> iextern l clexp (mk_id "sail_config_get_string", []) args), []) - | CT_unit -> ([], (fun clexp -> icopy l clexp unit_cval), []) - | CT_lint -> - let gs = ngensym () in - ( key_init @ [idecl l CT_json gs; iextern l (CL_id (gs, CT_json)) (mk_id "sail_config_get", []) args], - (fun clexp -> iextern l clexp (mk_id "sail_config_unwrap_int", []) [V_id (gs, CT_json)]), - [iclear CT_json gs] - ) - | CT_lbits -> config_extract CT_lbits ~validate:("sail_config_is_bool_array", []) ~extract:"sail_config_unwrap_bits" - | CT_fbits n -> - config_extract CT_lbits - ~validate:("sail_config_is_bool_array_with_size", [V_lit (VL_int (Big_int.of_int n), CT_fint 64)]) - ~extract:"sail_config_unwrap_bits" - | _ -> Reporting.unreachable l __POS__ "Invalid configuration type" + let rec extract json = function + | CT_string -> + config_extract CT_string json ~validate:("sail_config_is_string", []) ~extract:"sail_config_unwrap_string" + | CT_unit -> ([], (fun clexp -> icopy l clexp unit_cval), []) + | CT_lint -> config_extract CT_lint json ~validate:("sail_config_is_string", []) ~extract:"sail_config_unwrap_int" + | CT_lbits -> + config_extract CT_lbits json ~validate:("sail_config_is_bool_array", []) ~extract:"sail_config_unwrap_bits" + | CT_fbits n -> + config_extract CT_lbits json + ~validate:("sail_config_is_bool_array_with_size", [V_lit (VL_int (Big_int.of_int n), CT_fint 64)]) + ~extract:"sail_config_unwrap_bits" + | CT_vector item_ctyp -> + let vec = ngensym () in + let len = ngensym () in + let n = ngensym () in + let item_json = ngensym () in + let item = ngensym () in + let loop = label "config_vector_" in + let index = + V_call + ( Isub, + [ + V_id (len, CT_fint 64); + V_call (Iadd, [V_id (n, CT_fint 64); V_lit (VL_int (Big_int.of_int 1), CT_fint 64)]); + ] + ) + in + let setup, call, cleanup = extract item_json item_ctyp in + ( [ + idecl l (CT_fint 64) len; + iextern l (CL_id (len, CT_bool)) (mk_id "sail_config_list_length", []) [V_id (json, CT_json)]; + iif l + (V_call (Eq, [V_id (len, CT_fint 64); V_lit (VL_int (Big_int.of_int (-1)), CT_fint 64)])) + [ibad_config l] + [] CT_unit; + idecl l (CT_vector item_ctyp) vec; + iextern l (CL_id (vec, CT_vector item_ctyp)) (mk_id "internal_vector_init", []) [V_id (len, CT_fint 64)]; + iinit l (CT_fint 64) n (V_lit (VL_int Big_int.zero, CT_fint 64)); + ilabel loop; + idecl l CT_json item_json; + iextern l + (CL_id (item_json, CT_json)) + (mk_id "sail_config_list_nth", []) + [V_id (json, CT_json); V_id (n, CT_fint 64)]; + idecl l item_ctyp item; + ] + @ setup + @ [ + call (CL_id (item, item_ctyp)); + iextern l + (CL_id (vec, CT_vector item_ctyp)) + (mk_id "internal_vector_update", []) + [V_id (vec, CT_vector item_ctyp); index; V_id (item, item_ctyp)]; + ] + @ cleanup + @ [ + iclear item_ctyp item; + iclear CT_json item_json; + icopy l + (CL_id (n, CT_fint 64)) + (V_call (Iadd, [V_id (n, CT_fint 64); V_lit (VL_int (Big_int.of_int 1), CT_fint 64)])); + ijump l (V_call (Ilt, [V_id (n, CT_fint 64); V_id (len, CT_fint 64)])) loop; + ], + (fun clexp -> icopy l clexp (V_id (vec, CT_vector item_ctyp))), + [iclear (CT_vector item_ctyp) vec] + ) + | CT_list item_ctyp -> + let list = ngensym () in + let len = ngensym () in + let n = ngensym () in + let item_json = ngensym () in + let item = ngensym () in + let loop_start = label "config_list_start_" in + let loop_end = label "config_list_end_" in + let index = + V_call + ( Isub, + [ + V_id (len, CT_fint 64); + V_call (Iadd, [V_id (n, CT_fint 64); V_lit (VL_int (Big_int.of_int 1), CT_fint 64)]); + ] + ) + in + let setup, call, cleanup = extract item_json item_ctyp in + ( [ + idecl l (CT_fint 64) len; + iextern l (CL_id (len, CT_bool)) (mk_id "sail_config_list_length", []) [V_id (json, CT_json)]; + iif l + (V_call (Eq, [V_id (len, CT_fint 64); V_lit (VL_int (Big_int.of_int (-1)), CT_fint 64)])) + [ibad_config l] + [] CT_unit; + idecl l (CT_list item_ctyp) list; + iinit l (CT_fint 64) n (V_lit (VL_int Big_int.zero, CT_fint 64)); + ilabel loop_start; + ijump l (V_call (Igteq, [V_id (n, CT_fint 64); V_id (len, CT_fint 64)])) loop_end; + idecl l CT_json item_json; + iextern l (CL_id (item_json, CT_json)) (mk_id "sail_config_list_nth", []) [V_id (json, CT_json); index]; + idecl l item_ctyp item; + ] + @ setup + @ [ + call (CL_id (item, item_ctyp)); + iextern l + (CL_id (list, CT_list item_ctyp)) + (mk_id "sail_cons", []) + [V_id (item, item_ctyp); V_id (list, CT_list item_ctyp)]; + ] + @ cleanup + @ [ + iclear item_ctyp item; + iclear CT_json item_json; + icopy l + (CL_id (n, CT_fint 64)) + (V_call (Iadd, [V_id (n, CT_fint 64); V_lit (VL_int (Big_int.of_int 1), CT_fint 64)])); + igoto loop_start; + ilabel loop_end; + ], + (fun clexp -> icopy l clexp (V_id (list, CT_list item_ctyp))), + [iclear (CT_list item_ctyp) list] + ) + | _ -> Reporting.unreachable l __POS__ "Invalid configuration type" + in + + let setup, call, cleanup = extract json ctyp in + (init @ setup, call, cleanup @ [iclear CT_json json; iclear CT_json_key key_name]) let rec apat_ctyp ctx (AP_aux (apat, { env; _ })) = let ctx = { ctx with local_env = env } in diff --git a/test/c/config_vec_list.expect b/test/c/config_vec_list.expect new file mode 100644 index 000000000..d742e7f72 --- /dev/null +++ b/test/c/config_vec_list.expect @@ -0,0 +1,8 @@ +D +C +B +A +A +B +C +D diff --git a/test/c/config_vec_list.json b/test/c/config_vec_list.json new file mode 100644 index 000000000..53dd7dada --- /dev/null +++ b/test/c/config_vec_list.json @@ -0,0 +1,10 @@ +{ + "foo" : { + "bar" : [ + "A", + "B", + "C", + "D" + ] + } +} diff --git a/test/c/config_vec_list.sail b/test/c/config_vec_list.sail new file mode 100644 index 000000000..24062e13f --- /dev/null +++ b/test/c/config_vec_list.sail @@ -0,0 +1,29 @@ +default Order dec + +$include + +$iftarget c +$c_in_main sail_config_set_file("config_vec_list.json"); +$c_in_main_post sail_config_cleanup(); +$else +$option --config ../c/config_vec_list.json +$endif + +val print_list : list(string) -> unit + +function print_list [||] = () +and print_list (hd :: tl) = { + print_endline(hd); + print_list(tl) +} + +val main : unit -> unit + +function main() = { + let ys : list(string) = config foo.bar; + let xs : {'n, 'n >= 2. vector('n, string)} = config foo.bar; + foreach (n from 0 to (length(xs) - 1)) { + print_endline(xs[n]) + }; + print_list(ys) +} diff --git a/test/lem/run_tests.py b/test/lem/run_tests.py index 0e2744f89..947d606dd 100755 --- a/test/lem/run_tests.py +++ b/test/lem/run_tests.py @@ -26,6 +26,9 @@ 'concurrency_interface_inc', # Requires types that aren't currently in the library 'float_prelude', + # No possible configuration + 'config_mismatch', + 'config_bits_types', } skip_tests_mwords = { 'phantom_option', @@ -61,6 +64,9 @@ 'ex_cons_infer', # Requires types that aren't currently in the library 'float_prelude', + # No possible configuration + 'config_mismatch', + 'config_bits_types', } print('Sail is {}'.format(sail)) diff --git a/test/sv/run_tests.py b/test/sv/run_tests.py index bc5d88d8e..2646df093 100755 --- a/test/sv/run_tests.py +++ b/test/sv/run_tests.py @@ -29,6 +29,7 @@ 'concurrency_interface', # memory 'ediv_from_tdiv', # loops 'lib_hex_bits_signed', # verilator bug (in CI, works with latest) + 'config_vec_list', # unknown length vectors } print("Sail is {}".format(sail)) diff --git a/test/typecheck/fail/config_mismatch.expect b/test/typecheck/fail/config_mismatch.expect deleted file mode 100644 index c0da1dcbf..000000000 --- a/test/typecheck/fail/config_mismatch.expect +++ /dev/null @@ -1,11 +0,0 @@ -Type error: -fail/config_mismatch.sail:9.18-28: -9 | print_int("", config a.b : int); -  | ^--------^ -  | Incompatible types for configuration option found: -  | * Type int found here -  | * Type string found as previous type -  | -  | fail/config_mismatch.sail:8.18-28: -  | 8 | print_endline(config a.b); -  |  | ^--------^ previous type found here diff --git a/test/typecheck/pass/config_bits_types.json b/test/typecheck/pass/config_bits_types.json new file mode 100644 index 000000000..fbdd4b2c9 --- /dev/null +++ b/test/typecheck/pass/config_bits_types.json @@ -0,0 +1,6 @@ +{ + "c1" : { "len" : 64, value : "0x0000_0000_0000_0000" }, + "c2" : [true, false, true], + "c3" : [false], + "c4" : { "len" : 32, value : "1" } +} diff --git a/test/typecheck/pass/config_bits_types.sail b/test/typecheck/pass/config_bits_types.sail new file mode 100644 index 000000000..c04641261 --- /dev/null +++ b/test/typecheck/pass/config_bits_types.sail @@ -0,0 +1,16 @@ +default Order dec + +$include + +$option --config ../typecheck/pass/config_bits_types.json + +type xlen = 32 + +val main : unit -> unit + +function main() = { + let _ : bits(64) = config c1; + let _ : bits(3) = config c2; + let _ : {'n, 'n >= 0. bits('n)} = config c3; + let _ : {'n, xlen >= 'n > 0 | 'n == 64. bits('n)} = config c4; +} diff --git a/test/typecheck/pass/config_int_types.json b/test/typecheck/pass/config_int_types.json new file mode 100644 index 000000000..3b8a36954 --- /dev/null +++ b/test/typecheck/pass/config_int_types.json @@ -0,0 +1,7 @@ +{ + "c1" : 1, + "c2" : 20, + "c3" : 32, + "c4" : 63, + "c5" : 64 +} diff --git a/test/typecheck/pass/config_int_types.sail b/test/typecheck/pass/config_int_types.sail new file mode 100644 index 000000000..f1cb76d99 --- /dev/null +++ b/test/typecheck/pass/config_int_types.sail @@ -0,0 +1,22 @@ +default Order dec + +$include + +$option --config ../typecheck/pass/config_int_types.json + +type len = 32 + +function blackbox() -> int = { + signed(undefined : bits(5)) +} + +function main() -> unit = { + let _ : range(0, 16) = config c1; + let _ : range(0, len) = config c2; + let _ : int(32) = config c3; + let _ : {'n, true & 'n >= 32 & not('n == 64). int('n)} = config c4; + let n as int('n) = blackbox(); + if n == 64 then { + let _ : int('n) = config c5; + } +} diff --git a/test/typecheck/fail/config_mismatch.sail b/test/typecheck/pass/config_mismatch.sail similarity index 100% rename from test/typecheck/fail/config_mismatch.sail rename to test/typecheck/pass/config_mismatch.sail