From bd01118e8413d169a73542adc095dd2dd7cde932 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 24 Jan 2025 16:13:09 +0000 Subject: [PATCH] Config: Add configurable abstract types and add bit type --- doc/asciidoc/configuration.adoc | 41 +++++++++ language/jib.ott | 18 ++-- language/sail.ott | 6 +- lib/json/sail_config.c | 103 +++++++++++++++------ lib/json/sail_config.h | 14 ++- src/bin/repl.ml | 4 +- src/bin/sail.ml | 11 +-- src/lib/ast_util.ml | 2 +- src/lib/callgraph.ml | 2 +- src/lib/config.ml | 91 +++++++++++++++---- src/lib/config.mli | 2 +- src/lib/frontend.ml | 63 +++++++++++-- src/lib/frontend.mli | 6 +- src/lib/initial_check.ml | 24 ++--- src/lib/jib_compile.ml | 133 +++++++++++++++++++++++----- src/lib/jib_compile.mli | 2 + src/lib/jib_util.ml | 19 ++-- src/lib/jib_visitor.ml | 45 ++++++---- src/lib/monomorphise.ml | 2 +- src/lib/parse_ast.ml | 2 +- src/lib/parser.mly | 10 ++- src/lib/pretty_print_sail.ml | 7 +- src/lib/rewrites.ml | 2 +- src/lib/type_check.ml | 2 +- src/lib/type_check.mli | 6 ++ src/lib/type_env.ml | 3 + src/lib/type_env.mli | 1 + src/sail_c_backend/c_backend.ml | 41 +++++---- src/sail_latex_backend/latex.ml | 12 +-- src/sail_smt_backend/jib_smt.ml | 2 +- src/sail_sv_backend/jib_sv.ml | 2 +- test/c/config_abstract_type.expect | 1 + test/c/config_abstract_type.json | 10 +++ test/c/config_abstract_type.sail | 34 +++++++ test/c/config_abstract_type2.expect | 1 + test/c/config_abstract_type2.json | 10 +++ test/c/config_abstract_type2.sail | 34 +++++++ test/c/config_abstract_type3.expect | 1 + test/c/config_abstract_type3.json | 10 +++ test/c/config_abstract_type3.sail | 37 ++++++++ test/sailtest.py | 1 + 41 files changed, 652 insertions(+), 165 deletions(-) create mode 100644 test/c/config_abstract_type.expect create mode 100644 test/c/config_abstract_type.json create mode 100644 test/c/config_abstract_type.sail create mode 100644 test/c/config_abstract_type2.expect create mode 100644 test/c/config_abstract_type2.json create mode 100644 test/c/config_abstract_type2.sail create mode 100644 test/c/config_abstract_type3.expect create mode 100644 test/c/config_abstract_type3.json create mode 100644 test/c/config_abstract_type3.sail diff --git a/doc/asciidoc/configuration.adoc b/doc/asciidoc/configuration.adoc index da52bff3a..d640418da 100644 --- a/doc/asciidoc/configuration.adoc +++ b/doc/asciidoc/configuration.adoc @@ -136,6 +136,47 @@ void sail_config_set_file(const char *path); void sail_config_cleanup(void); ---- +=== Configurable abstract types + +The <> section we described how to write a type like +`xlen` below without providing a concrete value, in such a way that +the specification is parametric over the choice of `xlen`. + +[source,sail] +---- +type xlen : Int +---- + +In practice, we likely want to configure this type to have some +specific value at runtime. This can be done by associating a +configuration option with the abstract type as + +[source,sail] +---- +type xlen : Int = config arch.xlen +---- + +which could be instantiated using the following configuration JSON + +[source,json] +---- +{ "arch" : { "xlen" : 32 } } +---- + +We can then create (configurable) bitvector values of length `xlen`: +[source,sail] +---- +let x : bits(xlen) = config some.bitvector_value +---- + +In the configuration file, we specify these by using the string +`"xlen"` as the length: + +[source,json] +---- +{ "some" : { "bitvector_value" : { "len" : "xlen", "value": "0xFFFF_FFFF" } } } +---- + === Validating Configurations with JSON Schema :confschema: sail_doc/config_schema.json diff --git a/language/jib.ott b/language/jib.ott index c0adf860a..a23b824a9 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -209,13 +209,6 @@ clexp :: 'CL_' ::= | clexp . nat :: :: tuple | void : ctyp :: :: void -ctype_def :: 'CTD_' ::= - {{ com C type definition }} - | enum id = id0 '|' ... '|' idn :: :: enum - | struct id = { id0 : ctyp0 , ... , idn : ctypn } :: :: struct - | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant - | abstract id : ctyp :: :: abstract - iannot :: '' ::= {{ phantom }} {{ lem iannot }} @@ -271,6 +264,17 @@ instr :: 'I_' ::= | reset ctyp name :: :: reset | ctyp name = cval :: :: reinit +ctype_def_init :: 'CTDI_' ::= + | = { instr0 ; ... ; instrn } :: :: instrs + | :: :: none + +ctype_def :: 'CTD_' ::= + {{ com C type definition }} + | enum id = id0 '|' ... '|' idn :: :: enum + | struct id = { id0 : ctyp0 , ... , idn : ctypn } :: :: struct + | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant + | abstract id : ctyp ctype_def_init :: :: abstract + def_annot :: '' ::= {{ phantom }} {{ lem def_annot unit }} diff --git a/language/sail.ott b/language/sail.ott index 508edba31..2a40cc0c0 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -322,6 +322,10 @@ typschm :: 'TypSchm_' ::= grammar +opt_abstract_config :: 'TDC_' ::= + | = config string1 . ... . string2 :: :: key + | :: :: none + type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::= {{ ocaml TD_aux of type_def_aux * 'a annot }} {{ lem TD_aux of type_def_aux * annot 'a }} @@ -337,7 +341,7 @@ type_def_aux :: 'TD_' ::= {{ com tagged union type definition}} {{ texlong }} | typedef id = enumerate { id1 ; ... ; idn semi_opt } :: :: enum {{ com enumeration type definition}} {{ texlong }} - | typedef id : kind :: :: abstract + | typedef id : kind opt_abstract_config :: :: abstract {{ com abstract type }} | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield {{ com register mutable bitfield type definition }} {{ texlong }} diff --git a/lib/json/sail_config.c b/lib/json/sail_config.c index 343b9b6bc..1a13cb31f 100644 --- a/lib/json/sail_config.c +++ b/lib/json/sail_config.c @@ -184,6 +184,29 @@ bool sail_config_is_bits(const sail_config_json config) return is_bool_array || is_bv_object; } +bool sail_config_is_bits_abstract(const sail_config_json config) +{ + cJSON *json = (cJSON *)config; + + if (!(cJSON_IsObject(json) && cJSON_HasObjectItem(json, "len"))) { + return false; + } + + return cJSON_IsString(cJSON_GetObjectItemCaseSensitive(json, "len")); +} + +void sail_config_bits_abstract_len(sail_string *str, const sail_config_json config) +{ + cJSON *json = (cJSON *)config; + + cJSON *len_json = cJSON_GetObjectItemCaseSensitive(json, "len"); + sail_string len_str = cJSON_GetStringValue(len_json); + + size_t sz = strlen(len_str); + *str = (sail_string)realloc(*str, sz + 1); + *str = strcpy(*str, len_str); +} + void sail_config_unwrap_string(sail_string *str, const sail_config_json config) { sail_string conf_str = cJSON_GetStringValue((cJSON *)config); @@ -213,6 +236,57 @@ void sail_config_truncate(lbits *rop) { mpz_clear(tmp); } +void sail_config_unwrap_bit(lbits *bv, const sail_config_json config) +{ + cJSON *json = (cJSON *)config; + + bv->len = 1; + if (mpz_set_str(*bv->bits, json->valuestring, 10) == -1) { + sail_assert(false, "Failed to parse integer from configuration"); + } +} + +void sail_config_set_bits_value(lbits *bv, char *v) +{ + size_t i = 0; + for (char *c = v; *c != '\0'; c++) { + if (*c != '_') { + v[i] = *c; + i++; + } + } + v[i] = '\0'; + + if (strncmp(v, "0x", 2) == 0) { + gmp_sscanf(v, "0x%Zx", bv->bits); + } else if (strncmp(v, "0b", 2) == 0) { + mp_bitcnt_t b = 0; + i--; + do { + if (v[i] == '1') { + mpz_setbit(*bv->bits, b); + } + b++; + i--; + } while (i >= 2); + } else { + gmp_sscanf(v, "%Zd", bv->bits); + } + + sail_config_truncate(bv); +} + +void sail_config_unwrap_abstract_bits(lbits *bv, int64_t len, sail_config_json config) +{ + cJSON *json = (cJSON *)config; + cJSON *value_json = cJSON_GetObjectItemCaseSensitive(json, "value"); + char *v = value_json->valuestring; + + bv->len = (mp_bitcnt_t)len; + + sail_config_set_bits_value(bv, v); +} + void sail_config_unwrap_bits(lbits *bv, const sail_config_json config) { cJSON *json = (cJSON *)config; @@ -236,36 +310,13 @@ void sail_config_unwrap_bits(lbits *bv, const sail_config_json config) char *v = value_json->valuestring; bool has_separator = false; - bv->len = (mp_bitcnt_t)atoi(len_json->valuestring); - - size_t i = 0; - for (char *c = v; *c != '\0'; c++) { - if (*c != '_') { - v[i] = *c; - i++; - } - } - v[i] = '\0'; - - if (strncmp(v, "0x", 2) == 0) { + if (cJSON_IsNumber(len_json)) { bv->len = (mp_bitcnt_t)atoi(len_json->valuestring); - gmp_sscanf(v, "0x%Zx", bv->bits); - } else if (strncmp(v, "0b", 2) == 0) { - mp_bitcnt_t b = 0; - i--; - do { - if (v[i] == '1') { - mpz_setbit(*bv->bits, b); - } - b++; - i--; - } while (i >= 2); } else { - bv->len = (mp_bitcnt_t)atoi(len_json->valuestring); - gmp_sscanf(v, "%Zd", bv->bits); + bv->len = 32; } - sail_config_truncate(bv); + sail_config_set_bits_value(bv, v); } } diff --git a/lib/json/sail_config.h b/lib/json/sail_config.h index ce5d46628..1e316c4cf 100644 --- a/lib/json/sail_config.h +++ b/lib/json/sail_config.h @@ -8,7 +8,7 @@ /* The ASL derived parts of the ARMv8.3 specification in */ /* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ /* */ -/* Copyright (c) 2024 */ +/* Copyright (c) 2024-2025 */ /* Alasdair Armstrong */ /* */ /* All rights reserved. */ @@ -94,11 +94,23 @@ bool sail_config_is_bool_array(const sail_config_json config); bool sail_config_is_int(const sail_config_json config); bool sail_config_is_string(const sail_config_json config); +void sail_config_unwrap_bit(lbits *bv, const sail_config_json config); void sail_config_unwrap_bits(lbits *bv, const sail_config_json config); bool sail_config_unwrap_bool(const sail_config_json config); void sail_config_unwrap_int(sail_int *n, const sail_config_json config); void sail_config_unwrap_string(sail_string *str, const sail_config_json config); +/* + * Configurable abstract types require some special handling. + * + * Their length will be a string value like "xlen" or "mxlen". It is + * up to the user of this API to detect this and use the + * `unwrap_abstract_bits` variant after finding the correct width. + */ +bool sail_config_is_bits_abstract(const sail_config_json config); +void sail_config_bits_abstract_len(sail_string *str, const sail_config_json config); +void sail_config_unwrap_abstract_bits(lbits *bv, int64_t len, sail_config_json config); + #ifdef __cplusplus } #endif diff --git a/src/bin/repl.ml b/src/bin/repl.ml index 87054b467..fa2078be5 100644 --- a/src/bin/repl.ml +++ b/src/bin/repl.ml @@ -623,7 +623,9 @@ let handle_input' istate input = let ast, env = Type_check.check istate.env ast in { istate with ast = append_ast istate.ast ast; env; ctx } | ":instantiate" -> - let ast = Frontend.instantiate_abstract_types None !Sail_options.opt_instantiations istate.ast in + let ast, _ = + Frontend.instantiate_abstract_types None (`Assoc []) !Sail_options.opt_instantiations istate.ast + in let ast, env = Type_check.check istate.env (Type_check.strip_ast ast) in { istate with ast = append_ast istate.ast ast; env } | ":rewrite" -> diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 811d5e7f5..621547bd6 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -441,7 +441,7 @@ let file_to_string filename = close_in chan; Buffer.contents buf -let apply_model_config env ast = +let get_model_config () = match !opt_config_file with | Some file -> if Sys.file_exists file then ( @@ -453,10 +453,10 @@ let apply_model_config env ast = (Printf.sprintf "Failed to parse configuration file:\n%s" message) ) in - Config.rewrite_ast env json ast + json ) else raise (Reporting.err_general Parse_ast.Unknown (Printf.sprintf "Configuration file %s does not exist" file)) - | None -> Config.rewrite_ast env (`Assoc []) ast + | None -> `Assoc [] let run_sail (config : Yojson.Safe.t option) tgt = Target.run_pre_parse_hook tgt (); @@ -516,8 +516,9 @@ let run_sail (config : Yojson.Safe.t option) tgt = arguments with the appropriate extension, but not both!" ) in - let ast = Frontend.instantiate_abstract_types (Some tgt) !opt_instantiations ast in - let schema, ast = apply_model_config env ast in + let config_json = get_model_config () in + let ast, env_update = Frontend.instantiate_abstract_types (Some tgt) config_json !opt_instantiations ast in + let schema, ast = Config.rewrite_ast env env_update config_json 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 diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 29d475b67..d5371a785 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -1424,7 +1424,7 @@ let id_of_type_def_aux = function | TD_record (id, _, _, _) | TD_variant (id, _, _, _) | TD_enum (id, _, _) - | TD_abstract (id, _) + | TD_abstract (id, _, _) | TD_bitfield (id, _, _) -> id diff --git a/src/lib/callgraph.ml b/src/lib/callgraph.ml index 0f60e2e9b..873063ff7 100644 --- a/src/lib/callgraph.ml +++ b/src/lib/callgraph.ml @@ -273,7 +273,7 @@ let add_def_to_graph graph (DEF_aux (def, def_annot)) = scan_typquant (Type id) typq | TD_enum (id, ctors, _) -> List.iter (fun ctor_id -> graph := G.add_edge (Constructor ctor_id) (Type id) !graph) ctors - | TD_abstract (id, _) -> graph := G.add_edges (Type id) [] !graph + | TD_abstract (id, _, _) -> graph := G.add_edges (Type id) [] !graph | TD_bitfield (id, typ, ranges) -> graph := G.add_edges (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_ids typ))) !graph in diff --git a/src/lib/config.ml b/src/lib/config.ml index 1cdfb86b4..ec89163c3 100644 --- a/src/lib/config.ml +++ b/src/lib/config.ml @@ -73,7 +73,7 @@ module ConfigTypes : sig type t - val to_schema : t -> J.t + val to_schema : ?root:bool -> t -> J.t val create : unit -> t @@ -235,17 +235,19 @@ end = struct let schema_bool_array clauses = [("type", `String "array"); ("items", `Assoc [("type", `String "boolean")])] @ clauses in - let schema_hex_object clauses = + let schema_hex_object len_type clauses = [ ("type", `String "object"); ( "properties", - `Assoc [("len", `Assoc (("type", `String "integer") :: clauses)); ("value", bitvector_string_literal)] + `Assoc [("len", `Assoc (("type", `String len_type) :: 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_aux (Nexp_id id, _) when Env.is_abstract_typ id env -> + Some (`Assoc (schema_hex_object "string" [("const", `String (string_of_id id))])) | [], NC_aux (NC_true, _), nexp -> let* c = solve_unique env nexp in Some @@ -255,7 +257,7 @@ end = struct `List [ `Assoc (schema_bool_array (array_constraint ~min_length:c ~max_length:c ())); - `Assoc (schema_hex_object [("const", `Intlit (Big_int.to_string c))]); + `Assoc (schema_hex_object "integer" [("const", `Intlit (Big_int.to_string c))]); ] ); ] @@ -266,7 +268,7 @@ end = struct in let* hex_object_nc_logic = nc |> constraint_simp |> IntegerConstraint.constraint_schema v - |> Option.map (logic_type schema_hex_object) + |> Option.map (logic_type (schema_hex_object "integer")) in Some (`Assoc [("oneOf", `List [logic_to_schema bool_array_nc_logic; logic_to_schema hex_object_nc_logic])]) | _ -> None @@ -343,6 +345,7 @@ end = struct match string_of_id id with | "string" -> Some (`Assoc [("type", `String "string")]) | "unit" -> Some (`Assoc [("type", `String "null")]) + | "bit" -> Some (`Assoc [("type", `String "integer"); ("enum", `List [`Int 0; `Int 1])]) | _ -> None ) | _ -> None @@ -365,19 +368,22 @@ end = struct type t = Sail_value of config_type * config_type list | Object of (string, t) Hashtbl.t - let rec to_schema = function + let rec to_schema ?(root = true) = function | Object tbl -> let properties = Hashtbl.fold (fun key value props -> - let schema = to_schema value in + let schema = to_schema ~root:false 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"); ("properties", `Assoc properties); required] + let schema_version = + if root then [("$schema", `String "https://json-schema.org/draft/2020-12/schema")] else [] + in + `Assoc (schema_version @ [("type", `String "object"); ("properties", `Assoc properties); required]) | 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 @@ -472,8 +478,6 @@ 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 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 @@ -525,10 +529,48 @@ let parse_json_string_to_bits ~at:l ~len str = in Some (mk_lit_exp ~loc:l (L_bin (bitlist_to_string bitlist))) +let parse_json_string_to_abstract_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 mask bitlist = + mk_exp (E_app (mk_id "sail_mask", [mk_exp (E_sizeof (nid len)); mk_lit_exp (L_bin (bitlist_to_string bitlist))])) + |> locate (fun _ -> l) + in + let slice_int n = + mk_exp + (E_app + (mk_id "get_slice_int", [mk_exp (E_sizeof (nid len)); mk_lit_exp (L_num n); mk_lit_exp (L_num Big_int.zero)]) + ) + |> locate (fun _ -> l) + in + 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 |> mask) + 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 |> mask) + else + let* dec_chars = List.filter_map valid_dec_char chars |> Util.option_all in + let n = List.to_seq dec_chars |> String.of_seq |> Big_int.of_string in + Some (slice_int n) + 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)) + | `Int n -> ( + match typ with + | Typ_aux (Typ_id id, _) when string_of_id id = "bit" -> + if n = 0 then mk_lit_exp ~loc:l L_one + else if n = 1 then mk_lit_exp ~loc:l L_zero + else + raise + (Reporting.err_general l + ("Failed to interpret JSON integer " ^ string_of_int n ^ " as a bit (expected 0 or 1)") + ) + | _ -> 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)) @@ -597,10 +639,14 @@ let rec sail_exp_from_json ~at:l env typ = 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 + | "bitvector", _ -> ( + let* len = List.assoc_opt "len" obj in let* value = Option.bind (List.assoc_opt "value" obj) json_to_string in - parse_json_string_to_bits ~at:l ~len value + match len with + | `Int len -> parse_json_string_to_bits ~at:l ~len value + | `String len -> parse_json_string_to_abstract_bits ~at:l ~len:(mk_id len) value + | _ -> None + ) | _ -> None ) | _ -> None @@ -608,11 +654,18 @@ let rec sail_exp_from_json ~at:l env typ = 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)) + | None -> + raise + (Reporting.err_general l + (Printf.sprintf "Failed to interpret JSON object %s as Sail type %s" + (J.to_string (`Assoc obj)) + (string_of_typ typ) + ) + ) ) | _ -> assert false -let rewrite_exp global_env types json (aux, annot) = +let rewrite_exp global_env env_update types json (aux, annot) = match aux with | E_config parts -> ( let env = env_of_annot annot in @@ -623,15 +676,15 @@ let rewrite_exp global_env types json (aux, annot) = | Some json -> ( try let exp = sail_exp_from_json ~at:(fst annot) global_env typ json in - Type_check.check_exp (env_of_annot annot) exp typ + Type_check.check_exp (env_update (env_of_annot annot)) exp typ with Type_error.Type_error (l, err) -> raise (Type_error.to_reporting_exn l err) ) ) | _ -> E_aux (aux, annot) -let rewrite_ast global_env json ast = +let rewrite_ast global_env env_update json ast = let types = ConfigTypes.create () in - let alg = { id_exp_alg with e_aux = rewrite_exp global_env types json } in + let alg = { id_exp_alg with e_aux = rewrite_exp global_env env_update types json } in 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 5714f0e90..e09dcdde0 100644 --- a/src/lib/config.mli +++ b/src/lib/config.mli @@ -79,4 +79,4 @@ open Type_check 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 +val rewrite_ast : env -> (env -> env) -> Yojson.Safe.t -> typed_ast -> Yojson.Safe.t * typed_ast diff --git a/src/lib/frontend.ml b/src/lib/frontend.ml index a862519f7..7dde710ce 100644 --- a/src/lib/frontend.ml +++ b/src/lib/frontend.ml @@ -44,6 +44,7 @@ (* SPDX-License-Identifier: BSD-2-Clause *) (****************************************************************************) +open Ast open Ast_util open Ast_defs @@ -64,23 +65,75 @@ let finalize_ast asserts_termination ctx env ast = if !opt_ddump_tc_ast then Pretty_print_sail.output_ast stdout (Type_check.strip_ast ast); (ctx, ast, Type_check.Env.open_all_modules env, side_effects) -let instantiate_abstract_types tgt insts ast = +let rec json_lookup key json = + match (key, json) with + | [], _ -> Some json + | first :: rest, `Assoc obj -> ( + match List.assoc_opt first obj with Some json -> json_lookup rest json | None -> None + ) + | _ -> None + +let instantiate_from_json ~at:l (json : Yojson.Safe.t) = + let instantiate_error k = + let msg = + Printf.sprintf "Failed to instantiate abstract type of kind %s from JSON %s" (string_of_kind_aux k) + (Yojson.Safe.to_string json) + in + raise (Reporting.err_general l msg) + in + function + | K_int -> ( + match json with + | `Int n -> mk_typ_arg ~loc:l (A_nexp (nint n)) + | `Intlit s -> mk_typ_arg ~loc:l (A_nexp (nconstant (Big_int.of_string s))) + | _ -> instantiate_error K_int + ) + | K_bool -> ( + match json with + | `Bool true -> mk_typ_arg ~loc:l (A_bool nc_true) + | `Bool false -> mk_typ_arg ~loc:l (A_bool nc_false) + | _ -> instantiate_error K_bool + ) + | k -> instantiate_error k + +let instantiate_abstract_types tgt config insts ast = let open Ast in + let env_update = ref (fun env -> env) in + let add_to_env_update l id arg = + let prev_env_update = !env_update in + env_update := + Type_check.Env.( + fun env -> + prev_env_update env |> remove_abstract_typ id |> add_typ_synonym id (mk_empty_typquant ~loc:(gen_loc l)) arg + ) + in let instantiate = function - | DEF_aux (DEF_type (TD_aux (TD_abstract (id, kind), (l, _))), def_annot) as def -> begin + | DEF_aux (DEF_type (TD_aux (TD_abstract (id, kind, TDC_none), (l, _))), def_annot) as def -> ( match Bindings.find_opt id insts with | Some arg_fun -> let arg = arg_fun (unaux_kind kind) in + add_to_env_update l id arg; + DEF_aux + ( DEF_type (TD_aux (TD_abbrev (id, mk_empty_typquant ~loc:(gen_loc l), arg), (l, Type_check.empty_tannot))), + def_annot + ) + | None -> def + ) + | DEF_aux (DEF_type (TD_aux (TD_abstract (id, kind, TDC_key key), (l, _))), def_annot) as def -> ( + match json_lookup key config with + | Some json -> + let arg = instantiate_from_json ~at:l json (unaux_kind kind) in + add_to_env_update l id arg; DEF_aux ( DEF_type (TD_aux (TD_abbrev (id, mk_empty_typquant ~loc:(gen_loc l), arg), (l, Type_check.empty_tannot))), def_annot ) | None -> def - end + ) | def -> def in let defs = List.map instantiate ast.defs in - if Option.fold ~none:true ~some:Target.supports_abstract_types tgt then { ast with defs } + if Option.fold ~none:true ~some:Target.supports_abstract_types tgt then ({ ast with defs }, !env_update) else ( match List.find_opt (function DEF_aux (DEF_type (TD_aux (TD_abstract _, _)), _) -> true | _ -> false) defs with | Some (DEF_aux (_, def_annot)) -> @@ -92,7 +145,7 @@ let instantiate_abstract_types tgt insts ast = target_name ) ) - | None -> { ast with defs } + | None -> ({ ast with defs }, !env_update) ) type parse_continuation = { diff --git a/src/lib/frontend.mli b/src/lib/frontend.mli index 5146907dc..3ef2525a2 100644 --- a/src/lib/frontend.mli +++ b/src/lib/frontend.mli @@ -55,7 +55,11 @@ val opt_list_files : bool ref val opt_reformat : string option ref val instantiate_abstract_types : - Target.target option -> (kind_aux -> typ_arg) Bindings.t -> Type_check.typed_ast -> Type_check.typed_ast + Target.target option -> + Yojson.Safe.t -> + (kind_aux -> typ_arg) Bindings.t -> + Type_check.typed_ast -> + Type_check.typed_ast * (Type_check.env -> Type_check.env) (** The [FILE_HANDLER] module type allows plugins to define handlers for custom file types. It defines how those files are processed diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index c9647d6db..82d6c6311 100644 --- a/src/lib/initial_check.ml +++ b/src/lib/initial_check.ml @@ -1689,20 +1689,20 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_ ( fns @ [DEF_aux (DEF_type (TD_aux (TD_enum (id, enums, false), (l, empty_uannot))), def_annot)], { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors } ) - | P.TD_abstract (id, kind) -> + | P.TD_abstract (id, kind, instantiation) -> ( if not !opt_abstract_types then raise (Reporting.err_general l abstract_type_error); let id = to_ast_reserved_type_id ctx id in - begin - match to_ast_kind kind with - | Some kind -> - ( [DEF_aux (DEF_type (TD_aux (TD_abstract (id, kind), (l, empty_uannot))), def_annot)], - { - ctx with - type_constructors = Bindings.add id ([], to_parse_kind (Some (unaux_kind kind))) ctx.type_constructors; - } - ) - | None -> raise (Reporting.err_general l "Abstract type cannot have Order kind") - end + let instantiation = match instantiation with Some key -> TDC_key key | None -> TDC_none in + match to_ast_kind kind with + | Some kind -> + ( [DEF_aux (DEF_type (TD_aux (TD_abstract (id, kind, instantiation), (l, empty_uannot))), def_annot)], + { + ctx with + type_constructors = Bindings.add id ([], to_parse_kind (Some (unaux_kind kind))) ctx.type_constructors; + } + ) + | None -> raise (Reporting.err_general l "Abstract type cannot have Order kind") + ) | P.TD_bitfield (id, typ, ranges) -> let id = to_ast_reserved_type_id ctx id in let typ = to_ast_typ ctx typ in diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 5380c3581..f71086174 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -121,12 +121,14 @@ type ctx = { records : (kid list * ctyp Bindings.t) Bindings.t; enums : IdSet.t Bindings.t; variants : (kid list * ctyp Bindings.t) Bindings.t; + abstracts : ctyp Bindings.t; valspecs : (string option * ctyp list * ctyp * uannot) Bindings.t; quants : ctyp KBindings.t; local_env : Env.t; tc_env : Env.t; effect_info : Effects.side_effect_info; locals : (mut * ctyp) Bindings.t; + registers : ctyp Bindings.t; letbinds : int list; letbind_ids : IdSet.t; no_raw : bool; @@ -168,12 +170,14 @@ let initial_ctx ?for_target env effect_info = records = Bindings.empty; enums = Bindings.empty; variants = Bindings.empty; + abstracts = Bindings.empty; valspecs = initial_valspecs; quants = KBindings.empty; local_env = env; tc_env = env; effect_info; locals = Bindings.empty; + registers = Bindings.empty; letbinds = []; letbind_ids = IdSet.empty; no_raw = false; @@ -347,6 +351,13 @@ module Make (C : CONFIG) = struct let unit_cval = V_lit (VL_unit, CT_unit) + let get_variable_ctyp id ctx = + match Bindings.find_opt id ctx.locals with + | Some binding -> Some binding + | None -> ( + match Bindings.find_opt id ctx.registers with Some ctyp -> Some (Mutable, ctyp) | None -> None + ) + let rec compile_aval l ctx = function | AV_cval (cval, typ) -> let ctyp = cval_ctyp cval in @@ -358,7 +369,7 @@ module Make (C : CONFIG) = struct else ([], cval, []) | AV_id (id, Enum typ) -> ([], V_member (id, ctyp_of_typ ctx typ), []) | AV_id (id, typ) -> begin - match Bindings.find_opt id ctx.locals with + match get_variable_ctyp id ctx with | Some (_, ctyp) -> ([], V_id (name id, ctyp), []) | None -> ([], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), []) end @@ -637,17 +648,15 @@ module Make (C : CONFIG) = struct (List.rev !setup, (fun clexp -> iextern l clexp (id, []) setup_args), !cleanup) - let compile_config l ctx args typ = - let ctyp = ctyp_of_typ ctx typ in + let select_abstract l ctx string_id f = + let rec if_chain = function [] -> [] | [(_, e)] -> e | (i, t) :: e -> [iif l i t (if_chain e)] in + Bindings.bindings ctx.abstracts + |> List.map (fun (id, ctyp) -> + (V_call (String_eq, [V_id (string_id, CT_string); V_lit (VL_string (string_of_id id), CT_string)]), f id ctyp) + ) + |> if_chain - let key = - List.map - (function - | AV_lit (L_aux (L_string part, _), _) -> part - | _ -> Reporting.unreachable l __POS__ "Invalid argument when compiling config key" - ) - args - in + let compile_config' l ctx key ctyp = 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 @@ -674,16 +683,65 @@ module Make (C : CONFIG) = struct ) in + let config_extract_bits ctyp json = + let value = ngensym () in + let is_abstract = ngensym () in + let abstract_name = ngensym () in + let setup, non_abstract_call, cleanup = + config_extract ctyp json ~validate:("sail_config_is_bits", []) ~extract:"sail_config_unwrap_bits" + in + ( [ + idecl l CT_bool is_abstract; + iextern l (CL_id (is_abstract, CT_bool)) (mk_id "sail_config_is_bits_abstract", []) [V_id (json, CT_json)]; + idecl l ctyp value; + iif l + (V_id (is_abstract, CT_bool)) + ([ + idecl l CT_string abstract_name; + iextern l + (CL_id (abstract_name, CT_string)) + (mk_id "sail_config_bits_abstract_len", []) + [V_id (json, CT_json)]; + ] + @ select_abstract l ctx abstract_name (fun id abstract_ctyp -> + match abstract_ctyp with + | CT_fint 64 -> + [ + iextern l + (CL_id (value, ctyp)) + (mk_id "sail_config_unwrap_abstract_bits", []) + [V_call (Get_abstract, [V_id (name id, abstract_ctyp)]); V_id (json, CT_json)]; + ] + | CT_lint | CT_fint _ -> + let len = ngensym () in + [ + iinit l (CT_fint 64) len (V_call (Get_abstract, [V_id (name id, abstract_ctyp)])); + iextern l + (CL_id (value, ctyp)) + (mk_id "sail_config_unwrap_abstract_bits", []) + [V_id (len, CT_fint 64); V_id (json, CT_json)]; + ] + | _ -> [] + ) + @ [iclear CT_string abstract_name] + ) + (setup @ [non_abstract_call (CL_id (value, ctyp))] @ cleanup); + ], + (fun clexp -> icopy l clexp (V_id (value, ctyp))), + [iclear ctyp value] + ) + in + 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_int", []) ~extract:"sail_config_unwrap_int" | CT_fint _ -> config_extract CT_lint json ~validate:("sail_config_is_int", []) ~extract:"sail_config_unwrap_int" - | CT_lbits -> - config_extract CT_lbits json ~validate:("sail_config_is_bits", []) ~extract:"sail_config_unwrap_bits" - | CT_fbits _ -> - config_extract CT_lbits json ~validate:("sail_config_is_bits", []) ~extract:"sail_config_unwrap_bits" + | CT_lbits -> config_extract_bits CT_lbits json + | CT_sbits _ -> config_extract_bits CT_lbits json + | CT_fbits _ -> config_extract_bits CT_lbits json + | CT_bit -> config_extract CT_lbits json ~validate:("sail_config_is_int", []) ~extract:"sail_config_unwrap_bit" | CT_bool -> config_extract CT_bool json ~validate:("sail_config_is_bool", []) ~extract:"sail_config_unwrap_bool" | CT_enum (_, members) as enum_ctyp -> let enum_name = ngensym () in @@ -897,6 +955,18 @@ module Make (C : CONFIG) = struct let setup, call, cleanup = extract json ctyp in (init @ setup, call, cleanup @ [iclear CT_json json; iclear CT_json_key key_name]) + let compile_config l ctx args typ = + let ctyp = ctyp_of_typ ctx typ in + let key = + List.map + (function + | AV_lit (L_aux (L_string part, _), _) -> part + | _ -> Reporting.unreachable l __POS__ "Invalid argument when compiling config key" + ) + args + in + compile_config' l ctx key ctyp + let rec apat_ctyp ctx (AP_aux (apat, { env; _ })) = let ctx = { ctx with local_env = env } in match apat with @@ -1013,10 +1083,10 @@ module Make (C : CONFIG) = struct let rec compile_alexp ctx alexp = match alexp with | AL_id (id, typ) -> - let ctyp = match Bindings.find_opt id ctx.locals with Some (_, ctyp) -> ctyp | None -> ctyp_of_typ ctx typ in + let ctyp = match get_variable_ctyp id ctx with Some (_, ctyp) -> ctyp | None -> ctyp_of_typ ctx typ in CL_id (name id, ctyp) | AL_addr (id, typ) -> - let ctyp = match Bindings.find_opt id ctx.locals with Some (_, ctyp) -> ctyp | None -> ctyp_of_typ ctx typ in + let ctyp = match get_variable_ctyp id ctx with Some (_, ctyp) -> ctyp | None -> ctyp_of_typ ctx typ in CL_addr (CL_id (name id, ctyp)) | AL_field (alexp, field_id) -> CL_field (compile_alexp ctx alexp, field_id) @@ -1644,12 +1714,21 @@ module Make (C : CONFIG) = struct | TD_bitfield _ -> Reporting.unreachable l __POS__ "Cannot compile TD_bitfield" (* All type abbreviations are filtered out in compile_def *) | TD_abbrev _ -> Reporting.unreachable l __POS__ "Found TD_abbrev in compile_type_def" - | TD_abstract (id, K_aux (kind, _)) -> begin + | TD_abstract (id, K_aux (kind, _), inst) -> begin + let compile_inst ctyp = function + | TDC_key key -> + let setup, call, cleanup = compile_config' l ctx key ctyp in + CTDI_instrs (setup @ [call (CL_id (name id, ctyp))] @ cleanup) + | TDC_none -> CTDI_none + in match kind with | K_int -> let ctyp = ctyp_of_typ ctx (atom_typ (nid id)) in - (CTD_abstract (id, ctyp), ctx) - | K_bool -> (CTD_abstract (id, CT_bool), ctx) + let inst = compile_inst ctyp inst in + (CTD_abstract (id, ctyp, inst), { ctx with abstracts = Bindings.add id ctyp ctx.abstracts }) + | K_bool -> + let inst = compile_inst CT_bool inst in + (CTD_abstract (id, CT_bool, inst), { ctx with abstracts = Bindings.add id CT_bool ctx.abstracts }) | _ -> Reporting.unreachable l __POS__ "Found abstract type that was neither an integer nor a boolean" end @@ -2026,13 +2105,19 @@ module Make (C : CONFIG) = struct let ctx = { ctx with def_annot = Some def_annot } in match aux with | DEF_register (DEC_aux (DEC_reg (typ, id, None), _)) -> - ([CDEF_aux (CDEF_register (id, ctyp_of_typ ctx typ, []), def_annot)], ctx) + let ctyp = ctyp_of_typ ctx typ in + ( [CDEF_aux (CDEF_register (id, ctyp, []), def_annot)], + { ctx with registers = Bindings.add id ctyp ctx.registers } + ) | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), _)) -> + let ctyp = ctyp_of_typ ctx typ in let aexp = C.optimize_anf ctx (no_shadow ctx.letbind_ids (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in + let instrs = setup @ [call (CL_id (name id, ctyp))] @ cleanup in let instrs = unique_names instrs in - ([CDEF_aux (CDEF_register (id, ctyp_of_typ ctx typ, instrs), def_annot)], ctx) + ( [CDEF_aux (CDEF_register (id, ctyp, instrs), def_annot)], + { ctx with registers = Bindings.add id ctyp ctx.registers } + ) | DEF_val (VS_aux (VS_val_spec (_, id, ext), _)) -> let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in let extern = @@ -2646,7 +2731,7 @@ module Make (C : CONFIG) = struct let cdefs = List.filter (fun cdef -> not (is_ctype_def cdef)) cdefs in let ctdef_id = function - | CTD_abstract (id, _) | CTD_enum (id, _) | CTD_struct (id, _) | CTD_variant (id, _) -> id + | CTD_abstract (id, _, _) | CTD_enum (id, _) | CTD_struct (id, _) | CTD_variant (id, _) -> id in let ctdef_ids = function diff --git a/src/lib/jib_compile.mli b/src/lib/jib_compile.mli index 849af0db6..3895f73c1 100644 --- a/src/lib/jib_compile.mli +++ b/src/lib/jib_compile.mli @@ -77,12 +77,14 @@ type ctx = { records : (kid list * ctyp Bindings.t) Bindings.t; enums : IdSet.t Bindings.t; variants : (kid list * ctyp Bindings.t) Bindings.t; + abstracts : ctyp Bindings.t; valspecs : (string option * ctyp list * ctyp * uannot) Bindings.t; quants : ctyp KBindings.t; local_env : Env.t; tc_env : Env.t; effect_info : Effects.side_effect_info; locals : (mut * ctyp) Bindings.t; + registers : ctyp Bindings.t; letbinds : int list; letbind_ids : IdSet.t; no_raw : bool; diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index b6facf506..3da68eb35 100644 --- a/src/lib/jib_util.ml +++ b/src/lib/jib_util.ml @@ -865,6 +865,10 @@ let rec map_funcall f instrs = in I_aux (instr, aux) :: map_funcall f tail +let ctype_def_map_funcall f = function + | CTD_abstract (id, ctyp, CTDI_instrs instrs) -> CTD_abstract (id, ctyp, CTDI_instrs (map_funcall f instrs)) + | ctd -> ctd + let cdef_aux_map_funcall f = function | CDEF_register (id, ctyp, instrs) -> CDEF_register (id, ctyp, map_funcall f instrs) | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, map_funcall f instrs) @@ -872,11 +876,16 @@ let cdef_aux_map_funcall f = function | CDEF_startup (id, instrs) -> CDEF_startup (id, map_funcall f instrs) | CDEF_finish (id, instrs) -> CDEF_finish (id, map_funcall f instrs) | CDEF_val (id, extern, ctyps, ctyp) -> CDEF_val (id, extern, ctyps, ctyp) - | CDEF_type tdef -> CDEF_type tdef + | CDEF_type tdef -> CDEF_type (ctype_def_map_funcall f tdef) | CDEF_pragma (name, str) -> CDEF_pragma (name, str) let cdef_map_funcall f (CDEF_aux (aux, def_annot)) = CDEF_aux (cdef_aux_map_funcall f aux, def_annot) +let ctype_def_concatmap_instr f = function + | CTD_abstract (id, ctyp, CTDI_instrs instrs) -> + CTD_abstract (id, ctyp, CTDI_instrs (List.concat (List.map (concatmap_instr f) instrs))) + | ctd -> ctd + let cdef_aux_concatmap_instr f = function | CDEF_register (id, ctyp, instrs) -> CDEF_register (id, ctyp, List.concat (List.map (concatmap_instr f) instrs)) | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.concat (List.map (concatmap_instr f) instrs)) @@ -885,13 +894,13 @@ let cdef_aux_concatmap_instr f = function | CDEF_startup (id, instrs) -> CDEF_startup (id, List.concat (List.map (concatmap_instr f) instrs)) | CDEF_finish (id, instrs) -> CDEF_finish (id, List.concat (List.map (concatmap_instr f) instrs)) | CDEF_val (id, extern, ctyps, ctyp) -> CDEF_val (id, extern, ctyps, ctyp) - | CDEF_type tdef -> CDEF_type tdef + | CDEF_type tdef -> CDEF_type (ctype_def_concatmap_instr f tdef) | CDEF_pragma (name, str) -> CDEF_pragma (name, str) let cdef_concatmap_instr f (CDEF_aux (aux, def_annot)) = CDEF_aux (cdef_aux_concatmap_instr f aux, def_annot) let ctype_def_map_ctyp f = function - | CTD_abstract (id, ctyp) -> CTD_abstract (id, f ctyp) + | CTD_abstract (id, ctyp, inst) -> CTD_abstract (id, f ctyp, inst) | CTD_enum (id, ids) -> CTD_enum (id, ids) | CTD_struct (id, ctors) -> CTD_struct (id, List.map (fun (id, ctyp) -> (id, f ctyp)) ctors) | CTD_variant (id, ctors) -> CTD_variant (id, List.map (fun (id, ctyp) -> (id, f ctyp)) ctors) @@ -1094,12 +1103,12 @@ let ctype_def_ctyps = function | CTD_variant (_, ctors) -> List.map snd ctors let ctype_def_id = function - | CTD_abstract (id, _) | CTD_enum (id, _) -> id + | CTD_abstract (id, _, _) | CTD_enum (id, _) -> id | CTD_struct (id, _) -> id | CTD_variant (id, _) -> id let ctype_def_to_ctyp = function - | CTD_abstract (id, ctyp) -> ctyp + | CTD_abstract (id, ctyp, _) -> ctyp | CTD_enum (id, ids) -> CT_enum (id, ids) | CTD_struct (id, fields) -> CT_struct (id, fields) | CTD_variant (id, ctors) -> CT_variant (id, ctors) diff --git a/src/lib/jib_visitor.ml b/src/lib/jib_visitor.ml index f40c4961b..6396cdfff 100644 --- a/src/lib/jib_visitor.ml +++ b/src/lib/jib_visitor.ml @@ -63,25 +63,6 @@ and visit_binding vis ((id, ctyp) as binding) = let ctyp' = visit_ctyp vis ctyp in if id == id' && ctyp == ctyp' then binding else (id', ctyp') -let visit_ctype_def vis no_change = - match no_change with - | CTD_enum (id, members) -> - let id' = visit_id vis id in - let members' = map_no_copy (visit_id vis) members in - if id == id' && members == members' then no_change else CTD_enum (id', members') - | CTD_struct (id, fields) -> - let id' = visit_id vis id in - let fields' = map_no_copy (visit_binding vis) fields in - if id == id' && fields == fields' then no_change else CTD_struct (id', fields') - | CTD_variant (id, ctors) -> - let id' = visit_id vis id in - let ctors' = map_no_copy (visit_binding vis) ctors in - if id == id' && ctors == ctors' then no_change else CTD_variant (id', ctors') - | CTD_abstract (id, ctyp) -> - let id' = visit_id vis id in - let ctyp' = visit_ctyp vis ctyp in - if id == id' && ctyp == ctyp' then no_change else CTD_abstract (id', ctyp') - let rec visit_clexp vis outer_clexp = let aux vis no_change = match no_change with @@ -264,6 +245,32 @@ and visit_instrs vis outer_instrs = in do_visit vis (vis#vinstrs outer_instrs) aux outer_instrs +and visit_ctype_def vis no_change = + match no_change with + | CTD_enum (id, members) -> + let id' = visit_id vis id in + let members' = map_no_copy (visit_id vis) members in + if id == id' && members == members' then no_change else CTD_enum (id', members') + | CTD_struct (id, fields) -> + let id' = visit_id vis id in + let fields' = map_no_copy (visit_binding vis) fields in + if id == id' && fields == fields' then no_change else CTD_struct (id', fields') + | CTD_variant (id, ctors) -> + let id' = visit_id vis id in + let ctors' = map_no_copy (visit_binding vis) ctors in + if id == id' && ctors == ctors' then no_change else CTD_variant (id', ctors') + | CTD_abstract (id, ctyp, init) -> + let id' = visit_id vis id in + let ctyp' = visit_ctyp vis ctyp in + let init' = + match init with + | CTDI_none -> init + | CTDI_instrs instrs -> + let instrs' = map_no_copy (visit_instr vis) instrs in + if instrs == instrs' then init else CTDI_instrs instrs' + in + if id == id' && ctyp == ctyp' && init == init' then no_change else CTD_abstract (id', ctyp', init') + let visit_cdef vis outer_cdef = let aux vis (CDEF_aux (aux, def_annot) as no_change) = match aux with diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 5d0c7eea3..76fc35e73 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -4665,7 +4665,7 @@ module ToplevelNexpRewrites = struct | TD_abbrev (id, typq, A_aux (A_typ typ, l)) -> TD_aux (TD_abbrev (id, typq, A_aux (A_typ (expand_type typ), l)), annot) | TD_abbrev (id, typq, typ_arg) -> TD_aux (TD_abbrev (id, typq, typ_arg), annot) - | TD_abstract (id, kind) -> TD_aux (TD_abstract (id, kind), annot) + | TD_abstract (id, kind, instantiation) -> TD_aux (TD_abstract (id, kind, instantiation), annot) | TD_record (id, typq, typ_ids, flag) -> TD_aux (TD_record (id, typq, List.map (fun (typ, id) -> (expand_type typ, id)) typ_ids, flag), annot) | TD_variant (id, typq, tus, flag) -> TD_aux (TD_variant (id, typq, List.map rw_union tus, flag), annot) diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index 40501ed25..f0b175d78 100644 --- a/src/lib/parse_ast.ml +++ b/src/lib/parse_ast.ml @@ -385,7 +385,7 @@ type type_def_aux = | TD_record of id * typquant * (atyp * id) list (* struct type definition *) | TD_variant of id * typquant * type_union list (* union type definition *) | TD_enum of id * (id * atyp) list * (id * exp option) list (* enumeration type definition *) - | TD_abstract of id * kind + | TD_abstract of id * kind * string list option | TD_bitfield of id * atyp * (id * index_range) list (* register mutable bitfield type definition *) type val_spec_aux = (* Value type specification *) diff --git a/src/lib/parser.mly b/src/lib/parser.mly index 8ecbad9cb..a5209afc0 100644 --- a/src/lib/parser.mly +++ b/src/lib/parser.mly @@ -990,6 +990,12 @@ typaram: | Lparen separated_nonempty_list_trailing(Comma, param_kopt) Rparen { mk_typq $2 [] $startpos $endpos } +abstract_instantiation: + | Eq; Config; key=separated_nonempty_list(Dot, Id) + { Some key } + | + { None } + type_def: | Typedef id typaram Eq typ { mk_td (TD_abbrev ($2, $3, None, $5)) $startpos $endpos } @@ -999,8 +1005,8 @@ type_def: { mk_td (TD_abbrev ($2, $3, Some $5, $7)) $startpos $endpos } | Typedef id Colon kind Eq typ { mk_td (TD_abbrev ($2, mk_typqn, Some $4, $6)) $startpos $endpos } - | Typedef id Colon kind - { mk_td (TD_abstract ($2, $4)) $startpos $endpos } + | Typedef id Colon kind abstract_instantiation + { mk_td (TD_abstract ($2, $4, $5)) $startpos $endpos } | Struct id Eq Lcurly struct_fields Rcurly { mk_td (TD_record ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5)) $startpos $endpos } | Struct id typaram Eq Lcurly struct_fields Rcurly diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index c68334ff8..9cadba336 100644 --- a/src/lib/pretty_print_sail.ml +++ b/src/lib/pretty_print_sail.ml @@ -721,7 +721,12 @@ module Printer (Config : PRINT_CONFIG) = struct let doc_type_def (TD_aux (td, _)) = match td with - | TD_abstract (id, kind) -> begin doc_op colon (concat [string "type"; space; doc_id id]) (doc_kind kind) end + | TD_abstract (id, kind, instantiation) -> + let doc_inst = function + | TDC_key key -> space ^^ separate space [equals; string "config"; separate_map dot string key] + | TDC_none -> empty + in + doc_op colon (concat [string "type"; space; doc_id id]) (doc_kind kind) ^^ doc_inst instantiation | TD_abbrev (id, typq, typ_arg) -> begin match doc_typquant typq with | Some qdoc -> diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 95eade3e3..664b24be3 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -1977,7 +1977,7 @@ let rewrite_type_union_typs rw_typ (Tu_aux (Tu_ty_id (typ, id), annot)) = Tu_aux let rewrite_type_def_typs rw_typ rw_typquant (TD_aux (td, annot)) = match td with - | TD_abstract (id, kind) -> TD_aux (TD_abstract (id, kind), annot) + | TD_abstract (id, kind, instantiation) -> TD_aux (TD_abstract (id, kind, instantiation), annot) | TD_abbrev (id, typq, A_aux (A_typ typ, l)) -> TD_aux (TD_abbrev (id, rw_typquant typq, A_aux (A_typ (rw_typ typ), l)), annot) | TD_abbrev (id, typq, typ_arg) -> TD_aux (TD_abbrev (id, rw_typquant typq, typ_arg), annot) diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index d9c208ce5..459e4f7ef 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -4853,7 +4853,7 @@ let rec check_typedef : Env.t -> env def_annot -> uannot type_def -> typed_def l | _ -> () end; ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.add_typ_synonym id typq typ_arg env) - | TD_abstract (id, kind) -> begin + | TD_abstract (id, kind, _) -> begin match unaux_kind kind with | K_int | K_bool -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.add_abstract_typ id kind env) diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli index ca69d6f99..b70f6d414 100644 --- a/src/lib/type_check.mli +++ b/src/lib/type_check.mli @@ -121,6 +121,12 @@ module Env : sig val add_scattered_variant : id -> typquant -> t -> t + val add_typ_synonym : id -> typquant -> typ_arg -> t -> t + + val is_abstract_typ : id -> t -> bool + + val remove_abstract_typ : id -> t -> t + (** Check if a local variable is mutable. Throws Type_error if it isn't a local variable. Probably best to use Env.lookup_id instead *) diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml index 081eb8720..b9b327e1e 100644 --- a/src/lib/type_env.ml +++ b/src/lib/type_env.ml @@ -800,6 +800,9 @@ let add_abstract_typ id kind env = env ) +let remove_abstract_typ id env = + update_global (fun global -> { global with abstract_typs = Bindings.remove id global.abstract_typs }) env + let get_abstract_typs env = filter_items env env.global.abstract_typs let is_abstract_typ id env = Bindings.mem id env.global.abstract_typs diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli index b1bbd642f..bc031863e 100644 --- a/src/lib/type_env.mli +++ b/src/lib/type_env.mli @@ -126,6 +126,7 @@ val allow_user_undefined : id -> t -> t val add_abstract_typ : id -> kind -> t -> t val is_abstract_typ : id -> t -> bool val get_abstract_typs : t -> kind Bindings.t +val remove_abstract_typ : id -> t -> t val is_variant : id -> t -> bool val add_variant : id -> typquant * type_union list -> t -> t diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index cd36b50c7..c66a1d960 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -1394,19 +1394,26 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | I_end _ -> assert false | I_exit _ -> string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") -let codegen_type_def = +let codegen_type_def ctx = let open Printf in function - | CTD_abstract (id, ctyp) -> - ksprintf string "%s %s;" (sgen_ctyp ctyp) (sgen_id id) - ^^ twice hardline - ^^ c_function ~return:"void" - (ksprintf string "sail_set_abstract_%s(%s v)" (string_of_id id) (sgen_ctyp ctyp)) - [ - ( if is_stack_ctyp ctyp then ksprintf c_stmt "%s = v" (sgen_id id) - else sail_copy ~suffix:";" (sgen_ctyp_name ctyp) "&%s, v" (sgen_id id) - ); - ] + | CTD_abstract (id, ctyp, inst) -> + let setter = + match inst with + | CTDI_none -> + c_function ~return:"void" + (ksprintf string "sail_set_abstract_%s(%s v)" (string_of_id id) (sgen_ctyp ctyp)) + [ + ( if is_stack_ctyp ctyp then ksprintf c_stmt "%s = v" (sgen_id id) + else sail_copy ~suffix:";" (sgen_ctyp_name ctyp) "&%s, v" (sgen_id id) + ); + ] + | CTDI_instrs init -> + c_function ~return:"void" + (ksprintf string "sail_set_abstract_%s(void)" (string_of_id id)) + [separate_map hardline (codegen_instr (mk_id "set_abstract") ctx) init] + in + ksprintf string "%s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ twice hardline ^^ setter | CTD_enum (id, (first_id :: _ as ids)) -> let enum_name = sgen_id id in let enum_eq = @@ -1618,7 +1625,7 @@ let codegen_type_def = been translated to C. **) let generated = ref IdSet.empty -let codegen_tup ctyps = +let codegen_tup ctx ctyps = let id = mk_id ("tuple_" ^ string_of_ctyp (CT_tup ctyps)) in if IdSet.mem id !generated then empty else begin @@ -1628,7 +1635,7 @@ let codegen_tup ctyps = (0, Bindings.empty) ctyps in generated := IdSet.add id !generated; - codegen_type_def (CTD_struct (id, Bindings.bindings fields)) ^^ twice hardline + codegen_type_def ctx (CTD_struct (id, Bindings.bindings fields)) ^^ twice hardline end let codegen_list ctyp = @@ -1996,7 +2003,7 @@ let codegen_def' ctx (CDEF_aux (aux, _)) = function_header ^^ string "{" ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline ^^ string "}" - | CDEF_type ctype_def -> codegen_type_def ctype_def + | CDEF_type ctype_def -> codegen_type_def ctx ctype_def | CDEF_startup (id, instrs) -> let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" (static ()) (sgen_function_id id)) in separate_map hardline codegen_decl instrs @@ -2049,9 +2056,9 @@ let rec ctyp_dependencies = function | CT_enum _ | CT_poly _ | CT_constant _ | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_json | CT_json_key -> [] -let codegen_ctg = function +let codegen_ctg ctx = function | CTG_vector ctyp -> codegen_vector ctyp - | CTG_tup ctyps -> codegen_tup ctyps + | CTG_tup ctyps -> codegen_tup ctx ctyps | CTG_list ctyp -> codegen_list ctyp (** When we generate code for a definition, we need to first generate @@ -2068,7 +2075,7 @@ let codegen_def ctx def = ) else ( let deps = List.concat (List.map ctyp_dependencies ctyps) in - separate_map hardline codegen_ctg deps ^^ codegen_def' ctx def + separate_map hardline (codegen_ctg ctx) deps ^^ codegen_def' ctx def ) let is_cdef_startup = function CDEF_aux (CDEF_startup _, _) -> true | _ -> false diff --git a/src/sail_latex_backend/latex.ml b/src/sail_latex_backend/latex.ml index 02c8a1317..4e0d74dda 100644 --- a/src/sail_latex_backend/latex.ml +++ b/src/sail_latex_backend/latex.ml @@ -451,14 +451,6 @@ let process_pragma l command = Reporting.warn "Bad latex pragma at" l ""; None -let tdef_id = function - | TD_abstract (id, _) -> id - | TD_abbrev (id, _, _) -> id - | TD_record (id, _, _, _) -> id - | TD_variant (id, _, _, _) -> id - | TD_enum (id, _, _) -> id - | TD_bitfield (id, _, _) -> id - let defs { defs; _ } = reset_state state; @@ -510,8 +502,8 @@ let defs { defs; _ } = letdefs := IdSet.fold (fun id -> Bindings.add id base_id) ids !letdefs; Some (latex_command ~docstring Let base_id (Pretty_print_sail.doc_def def) (fst annot)) end - | DEF_type (TD_aux (tdef, annot)) -> - let id = tdef_id tdef in + | DEF_type (TD_aux (_, annot) as tdef) -> + let id = id_of_type_def tdef in typedefs := Bindings.add id id !typedefs; Some (latex_command ~docstring Type id (Pretty_print_sail.doc_def def) (fst annot)) | DEF_fundef (FD_aux (FD_function (_, _, funcls), annot)) as def -> Some (latex_funcls def funcls) diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 6887ad393..799aaf0c9 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -645,7 +645,7 @@ module Make (Config : CONFIG) = struct | _ -> return [] let smt_ctype_def = function - | CTD_abstract (id, _) -> Reporting.unreachable (id_loc id) __POS__ "Abstract types not supported for SMT target" + | CTD_abstract (id, _, _) -> Reporting.unreachable (id_loc id) __POS__ "Abstract types not supported for SMT target" | CTD_enum (id, elems) -> return (declare_datatypes (mk_enum (zencode_upper_id id) (List.map zencode_id elems))) | CTD_struct (id, fields) -> let* fields = diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index 172512a8f..dec07cf8e 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -741,7 +741,7 @@ module Make (Config : CONFIG) = struct | ty, Some index -> string ty ^^ space ^^ doc ^^ space ^^ string index let pp_type_def = function - | CTD_abstract (id, _) -> + | CTD_abstract (id, _, _) -> Reporting.unreachable (id_loc id) __POS__ "Abstract types not supported for SystemVerilog target" | CTD_enum (id, ids) -> string "typedef" ^^ space ^^ string "enum" ^^ space diff --git a/test/c/config_abstract_type.expect b/test/c/config_abstract_type.expect new file mode 100644 index 000000000..dafafe7b5 --- /dev/null +++ b/test/c/config_abstract_type.expect @@ -0,0 +1 @@ +R = 0x32323232 diff --git a/test/c/config_abstract_type.json b/test/c/config_abstract_type.json new file mode 100644 index 000000000..070be4924 --- /dev/null +++ b/test/c/config_abstract_type.json @@ -0,0 +1,10 @@ +{ + "arch" : { + "xlen" : 32 + }, + "registers" : { + "R" : { + "init" : { "len" : "xlen", "value" : "0x3232_3232" } + } + } +} diff --git a/test/c/config_abstract_type.sail b/test/c/config_abstract_type.sail new file mode 100644 index 000000000..0872682e5 --- /dev/null +++ b/test/c/config_abstract_type.sail @@ -0,0 +1,34 @@ +default Order dec +$include + +$option --abstract-types + +type xlen : Int = config arch.xlen + +constraint xlen in {32, 64} + +// This test is similar to abstract_type.sail, but instantiating the +// type from the configuration file rather than the command line. +$iftarget c +$c_in_main sail_config_set_file("config_abstract_type.json"); +$c_in_main sail_set_abstract_xlen(); +$c_in_main_post sail_config_cleanup(); +$else +$option --config ../c/config_abstract_type.json +$endif + +register R : bits(xlen) + +val main : unit -> unit + +function main() = { + let v : bits(xlen) = config registers.R.init; + + if sizeof(xlen) == 32 then { + R = v + } else { + R = 0x6464_6464_6464_6464 + }; + + print_bits("R = ", R) +} diff --git a/test/c/config_abstract_type2.expect b/test/c/config_abstract_type2.expect new file mode 100644 index 000000000..dafafe7b5 --- /dev/null +++ b/test/c/config_abstract_type2.expect @@ -0,0 +1 @@ +R = 0x32323232 diff --git a/test/c/config_abstract_type2.json b/test/c/config_abstract_type2.json new file mode 100644 index 000000000..070be4924 --- /dev/null +++ b/test/c/config_abstract_type2.json @@ -0,0 +1,10 @@ +{ + "arch" : { + "xlen" : 32 + }, + "registers" : { + "R" : { + "init" : { "len" : "xlen", "value" : "0x3232_3232" } + } + } +} diff --git a/test/c/config_abstract_type2.sail b/test/c/config_abstract_type2.sail new file mode 100644 index 000000000..86cd83eb5 --- /dev/null +++ b/test/c/config_abstract_type2.sail @@ -0,0 +1,34 @@ +default Order dec +$include + +$option --abstract-types + +type xlen : Int = config arch.xlen + +constraint xlen >= 0 + +// This test is similar to abstract_type.sail, but instantiating the +// type from the configuration file rather than the command line. +$iftarget c +$c_in_main sail_config_set_file("config_abstract_type.json"); +$c_in_main sail_set_abstract_xlen(); +$c_in_main_post sail_config_cleanup(); +$else +$option --config ../c/config_abstract_type.json +$endif + +register R : bits(xlen) + +val main : unit -> unit + +function main() = { + let v : bits(xlen) = config registers.R.init; + + if sizeof(xlen) == 32 then { + R = v + } else { + R = sail_mask(sizeof(xlen), 0x6464_6464_6464_6464) + }; + + print_bits("R = ", R) +} diff --git a/test/c/config_abstract_type3.expect b/test/c/config_abstract_type3.expect new file mode 100644 index 000000000..dafafe7b5 --- /dev/null +++ b/test/c/config_abstract_type3.expect @@ -0,0 +1 @@ +R = 0x32323232 diff --git a/test/c/config_abstract_type3.json b/test/c/config_abstract_type3.json new file mode 100644 index 000000000..070be4924 --- /dev/null +++ b/test/c/config_abstract_type3.json @@ -0,0 +1,10 @@ +{ + "arch" : { + "xlen" : 32 + }, + "registers" : { + "R" : { + "init" : { "len" : "xlen", "value" : "0x3232_3232" } + } + } +} diff --git a/test/c/config_abstract_type3.sail b/test/c/config_abstract_type3.sail new file mode 100644 index 000000000..c699e736c --- /dev/null +++ b/test/c/config_abstract_type3.sail @@ -0,0 +1,37 @@ +default Order dec +$include + +$option --abstract-types + +type other : Bool + +type xlen : Int = config arch.xlen + +constraint xlen in {32, 64} + +// This test is similar to abstract_type.sail, but instantiating the +// type from the configuration file rather than the command line. +$iftarget c +$c_in_main sail_config_set_file("config_abstract_type.json"); +$c_in_main sail_set_abstract_xlen(); +$c_in_main_post sail_config_cleanup(); +$else +$option --config ../c/config_abstract_type.json +$option --instantiate other=true +$endif + +register R : bits(xlen) + +val main : unit -> unit + +function main() = { + let v : bits(xlen) = config registers.R.init; + + if sizeof(xlen) == 32 then { + R = v + } else { + R = 0x6464_6464_6464_6464 + }; + + print_bits("R = ", R) +} diff --git a/test/sailtest.py b/test/sailtest.py index 1c802840b..94e8fa64c 100644 --- a/test/sailtest.py +++ b/test/sailtest.py @@ -137,6 +137,7 @@ def step(string, expected_status=0, stderr_file=''): print(content) except FileNotFoundError: print('File {} not found'.format(stderr_file)) + sys.exit(1) def banner(string): print('-' * len(string))