From a261d7c9a94171a9a9a8a298d0c1670c3e7fabd8 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 8 May 2024 06:19:50 +0100 Subject: [PATCH] Add some structure to attribute arguments Attribute arguments are now in a JSON-like language, so one can have $[attr { "key1" = value1, "key2" = value2 }] It's JSON-like because we make the sensible changes to JSON, i.e. trailing commas ok, comments allowed, numbers are not strictly floats, etc. Strings do not have to be quoted if they are valid identifiers, so $[attr foo] still works as before. The main advantage here is that we don't have to do ugly string-parsing things in Sail whenever we want to use attributes, and downstream tools like asciidoctor-sail can consume this information as JSON without duplicating the aformentioned string parsing logic. --- language/jib.ott | 17 ++++++- language/sail.ott | 19 +++++-- src/lib/anf.ml | 2 +- src/lib/ast.sed | 3 -- src/lib/ast_util.ml | 15 +++++- src/lib/ast_util.mli | 18 ++++--- src/lib/bitfield.ml | 2 +- src/lib/chunk_ast.ml | 6 +-- src/lib/dune | 10 ++-- src/lib/initial_check.ml | 2 +- src/lib/jib_compile.ml | 5 +- src/lib/lexer.mll | 5 +- src/lib/mappings.ml | 6 +-- src/lib/monomorphise.ml | 3 +- src/lib/parse_ast.ml | 23 ++++++--- src/lib/parser.mly | 43 +++++++++++++--- src/lib/pattern_completeness.ml | 4 +- src/lib/pattern_completeness.mli | 2 +- src/lib/pretty_print_sail.ml | 3 +- src/lib/rewrites.ml | 2 +- src/lib/scattered.ml | 4 +- src/lib/splice.ml | 2 +- src/lib/state.ml | 4 +- src/lib/type_check.ml | 85 ++++++++++++++++++-------------- src/sail_doc_backend/docinfo.ml | 7 ++- 25 files changed, 189 insertions(+), 103 deletions(-) delete mode 100644 src/lib/ast.sed diff --git a/language/jib.ott b/language/jib.ott index c85ac1c51..3af69bf03 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -50,12 +50,24 @@ metavar alpha ::= {{ phantom }} {{ lem 'a }} +embed +{{ ocaml + +open Ast +open Value2 + +type iannot = int * Parse_ast.l + +}} + embed {{ lem open import Ast open import Value2 +type iannot = int * ocaml_l + }} grammar @@ -189,8 +201,9 @@ ctype_def :: 'CTD_' ::= | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant iannot :: '' ::= - {{ lem nat * nat * nat }} - {{ ocaml int * int * int }} + {{ phantom }} + {{ lem iannot }} + {{ ocaml iannot }} instr :: 'I_' ::= {{ aux _ iannot }} diff --git a/language/sail.ott b/language/sail.ott index 8712c60b9..9d82b0756 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -77,6 +77,7 @@ open Value type text = string type l = Parse_ast.l +type config = Parse_ast.Config.config type 'a annot = l * 'a @@ -88,7 +89,7 @@ type visibility = Public | Private of l type def_annot = { doc_comment : string option; - attrs : (l * string * string) list; + attrs : (l * string * config) list; visibility : visibility; loc : l } @@ -100,9 +101,18 @@ type 'a clause_annot = def_annot * 'a embed {{ lem -type l = | Unknown +type ocaml_l +declare ocaml target_rep type ocaml_l = `Parse_ast.l` -type value = | Val +type l = ocaml_l + +type ocaml_config +declare ocaml target_rep type ocaml_config = `Parse_ast.Config.config` + +type config = ocaml_config + +type value +declare ocaml target_rep type value = `Value.value` type loop = While | Until @@ -114,7 +124,7 @@ type visibility = Public | Private of l type def_annot = <| doc_comment : maybe string; - attrs : list (l * string * string); + attrs : list (l * string * maybe config); visibility : visibility; loc : l |> @@ -569,7 +579,6 @@ E_let <= E_field E_app left E_app - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Function definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/src/lib/anf.ml b/src/lib/anf.ml index 7894ac916..92b665623 100644 --- a/src/lib/anf.ml +++ b/src/lib/anf.ml @@ -447,7 +447,7 @@ let rec pp_aexp (AE_aux (aexp, annot)) = ( match get_attributes annot.uannot with | [] -> empty | attrs -> - concat_map (fun (_, attr, arg) -> string (Printf.sprintf "$[%s %s]" attr arg |> Util.magenta |> Util.clear)) attrs + concat_map (fun (_, attr, arg) -> string (string_of_attribute attr arg |> Util.magenta |> Util.clear)) attrs ) ^^ match aexp with diff --git a/src/lib/ast.sed b/src/lib/ast.sed deleted file mode 100644 index 3f53dc787..000000000 --- a/src/lib/ast.sed +++ /dev/null @@ -1,3 +0,0 @@ -s/type l = | Unknown/type l = Parse_ast.l/ -s/type value = | Val/open Value/ -s/type iannot = int \* int \* int/type iannot = int \* Parse_ast.l/ \ No newline at end of file diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index a73fb0dd4..f57836f25 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -67,11 +67,24 @@ open Ast open Ast_defs +open Parse_ast.Config open Util module Big_int = Nat_big_num (* The type of annotations for untyped AST nodes *) -type uannot = { attrs : (l * string * string) list } +type uannot = { attrs : (l * string * config option) list } + +let rec string_of_config (Conf_aux (aux, _)) = + match aux with + | Conf_object kvs -> + "{ " ^ Util.string_of_list ", " (fun (k, v) -> Printf.sprintf "%s = %s" k (string_of_config v)) kvs ^ " }" + | Conf_string s -> "\"" ^ s ^ "\"" + | Conf_num n -> Big_int.to_string n + | Conf_list cs -> "[" ^ Util.string_of_list ", " string_of_config cs ^ "]" + +let string_of_attribute attr = function + | None -> Printf.sprintf "$[%s]" attr + | Some config -> Printf.sprintf "$[%s %s]" attr (string_of_config config) let empty_uannot = { attrs = [] } diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index 36062c49e..80f2f0cf3 100644 --- a/src/lib/ast_util.mli +++ b/src/lib/ast_util.mli @@ -80,6 +80,10 @@ type uannot val empty_uannot : uannot +val string_of_attribute : string -> config option -> string + +val string_of_config : config -> string + (** Add an attribute to an annotation. Attributes are attached to expressions in Sail via: {@sail[ $[attribute argument] expression @@ -87,21 +91,21 @@ val empty_uannot : uannot The location argument should be a span that corresponds to the attribute itself, and not include the expression. *) -val add_attribute : l -> string -> string -> uannot -> uannot +val add_attribute : l -> string -> config option -> uannot -> uannot val remove_attribute : string -> uannot -> uannot -val get_attribute : string -> uannot -> (l * string) option +val get_attribute : string -> uannot -> (l * config option) option -val get_attributes : uannot -> (l * string * string) list +val get_attributes : uannot -> (l * string * config option) list -val find_attribute_opt : string -> (l * string * string) list -> string option +val find_attribute_opt : string -> (l * string * config option) list -> config option option -val mk_def_annot : ?doc:string -> ?attrs:(l * string * string) list -> ?visibility:visibility -> l -> def_annot +val mk_def_annot : ?doc:string -> ?attrs:(l * string * config option) list -> ?visibility:visibility -> l -> def_annot -val add_def_attribute : l -> string -> string -> def_annot -> def_annot +val add_def_attribute : l -> string -> config option -> def_annot -> def_annot -val get_def_attribute : string -> def_annot -> (l * string) option +val get_def_attribute : string -> def_annot -> (l * config option) option val remove_def_attribute : string -> def_annot -> def_annot diff --git a/src/lib/bitfield.ml b/src/lib/bitfield.ml index 72458cadf..89f70cce6 100644 --- a/src/lib/bitfield.ml +++ b/src/lib/bitfield.ml @@ -94,7 +94,7 @@ let range_loc (BF_aux (_, l)) = l let fix_locations l defs = let rec go acc = function | DEF_aux (def, def_annot) :: defs -> - go (DEF_aux (def, add_def_attribute (gen_loc l) "fix_location" "" def_annot) :: acc) defs + go (DEF_aux (def, add_def_attribute (gen_loc l) "fix_location" None def_annot) :: acc) defs | [] -> acc in List.rev (go [] defs) diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index 3f91e9fb6..250b7ba98 100644 --- a/src/lib/chunk_ast.ml +++ b/src/lib/chunk_ast.ml @@ -707,7 +707,7 @@ let rec chunk_pat comments chunks (P_aux (aux, l)) = let fpats = chunk_delimit ~delim:"," ~get_loc:(fun (FP_aux (_, l)) -> l) ~chunk:chunk_fpat comments fpats in Queue.add (Tuple ("struct {", "}", 1, fpats)) chunks | P_attribute (attr, arg, pat) -> - Queue.add (Atom (Printf.sprintf "$[%s %s]" attr arg)) chunks; + Queue.add (Atom (Ast_util.string_of_attribute attr arg)) chunks; Queue.add (Spacer (false, 1)) chunks; chunk_pat comments chunks pat @@ -773,7 +773,7 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) = | E_ref id -> Queue.add (Atom ("ref " ^ string_of_id id)) chunks | E_lit lit -> Queue.add (chunk_of_lit lit) chunks | E_attribute (attr, arg, exp) -> - Queue.add (Atom (Printf.sprintf "$[%s %s]" attr arg)) chunks; + Queue.add (Atom (Ast_util.string_of_attribute attr arg)) chunks; Queue.add (Spacer (false, 1)) chunks; chunk_exp comments chunks exp | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> Queue.add (App (id, [])) chunks @@ -1074,7 +1074,7 @@ let chunk_funcl comments funcl = Queue.add (Spacer (false, 1)) chunks; chunk_funcl' comments funcl | FCL_attribute (attr, arg, funcl) -> - Queue.add (Atom (Printf.sprintf "$[%s %s]" attr arg)) chunks; + Queue.add (Atom (Ast_util.string_of_attribute attr arg)) chunks; Queue.add (Spacer (false, 1)) chunks; chunk_funcl' comments funcl | FCL_doc (_, funcl) -> chunk_funcl' comments funcl diff --git a/src/lib/dune b/src/lib/dune index c911e78de..022d440bb 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -44,12 +44,10 @@ (rule (target ast.ml) (deps - (:ast ast.lem) - (:sed ast.sed)) + (:ast ast.lem)) (action (progn - (run lem -ocaml %{ast}) - (run sed -i.bak -f %{sed} %{target})))) + (run lem -ocaml %{ast})))) (copy_files ../gen_lib/*.lem) @@ -86,13 +84,11 @@ (target jib.ml) (deps (:jib jib.lem) - (:sed ast.sed) value2.ml (glob_files lem/*.lem)) (action (progn - (run lem -ocaml %{jib} -lib . -lib lem/) - (run sed -i.bak -f %{sed} %{target})))) + (run lem -ocaml %{jib} -lib . -lib lem/)))) (menhir (modules parser project_parser)) diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index e306877d2..677e965de 100644 --- a/src/lib/initial_check.ml +++ b/src/lib/initial_check.ml @@ -1576,7 +1576,7 @@ let undefined_builtin_val_specs = ] let make_global (DEF_aux (def, def_annot)) = - DEF_aux (def, add_def_attribute (gen_loc def_annot.loc) "global" "" def_annot) + DEF_aux (def, add_def_attribute (gen_loc def_annot.loc) "global" None def_annot) let generate_undefineds vs_ids defs = let undefined_builtins = diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 431b23670..fbc150215 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -68,6 +68,7 @@ open Ast open Ast_defs open Ast_util +open Parse_ast.Config open Jib open Jib_util open Jib_visitor @@ -192,8 +193,8 @@ let initial_ctx env effect_info = } let update_coverage_override' ctx = function - | Some (_, "on") -> { ctx with coverage_override = true } - | Some (_, "off") -> { ctx with coverage_override = false } + | Some (_, Some (Conf_aux (Conf_string "on", _))) -> { ctx with coverage_override = true } + | Some (_, Some (Conf_aux (Conf_string "off", _))) -> { ctx with coverage_override = false } | _ -> ctx let update_coverage_override uannot ctx = update_coverage_override' ctx (get_attribute "coverage" uannot) diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index 940da46a7..4c76690ee 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -219,10 +219,7 @@ rule token comments = parse | "/*" { block_comment comments (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 lexbuf; token comments lexbuf } | "*/" { raise (Reporting.err_lex (Lexing.lexeme_start_p lexbuf) "Unbalanced comment") } | "$[" (ident+ as i) - { let startpos = Lexing.lexeme_start_p lexbuf in - let attr = attribute 0 (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf in - lexbuf.lex_start_p <- startpos; - Attribute(i, String.trim attr) } + { Attribute i } | "$" (ident+ as i) { let startpos = Lexing.lexeme_start_p lexbuf in let arg = pragma comments (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) false lexbuf in diff --git a/src/lib/mappings.ml b/src/lib/mappings.ml index 3fe1c3dfd..e72dd9d9f 100644 --- a/src/lib/mappings.ml +++ b/src/lib/mappings.ml @@ -211,7 +211,7 @@ let none_pexp exp = mk_pexp (Pat_exp (mk_pat (P_app (mk_id "None", [mk_pat (P_li let match_completeness c (E_aux (aux, (l, uannot))) = let uannot = - uannot |> remove_attribute "incomplete" |> remove_attribute "complete" |> add_attribute (gen_loc l) c "" + uannot |> remove_attribute "incomplete" |> remove_attribute "complete" |> add_attribute (gen_loc l) c None in match aux with | E_match _ -> E_aux (aux, (l, uannot)) @@ -297,7 +297,7 @@ and rewrite_arms is_mapping subst msa (l, uannot) = let outer_match = match msa.after_arms with | [] -> - E_aux (E_match (new_head_exp, [unwrap_some]), (l, add_attribute Parse_ast.Unknown "mapping_match" "" uannot)) + E_aux (E_match (new_head_exp, [unwrap_some]), (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot)) |> match_incomplete | _ -> let after_match = @@ -305,7 +305,7 @@ and rewrite_arms is_mapping subst msa (l, uannot) = in E_aux ( E_match (new_head_exp, [unwrap_some; none_pexp after_match]), - (l, add_attribute Parse_ast.Unknown "mapping_match" "" uannot) + (l, add_attribute Parse_ast.Unknown "mapping_match" None uannot) ) |> match_complete in diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 20ef112ba..997861125 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -4159,8 +4159,7 @@ module BitvectorSizeCasts = struct | P_aux (P_wild, (_, annot)), None -> begin (* Similar to the literal case *) match (body, untyped_annot annot |> get_attribute "int_wildcard") with - | _, Some (_, s) -> - let i = Big_int.of_string s in + | _, Some (_, Some (Conf_aux (Conf_num i, _))) -> let src_typ = fill_in_type (Env.add_constraint (nc_eq (nvar kid) (nconstant i)) env) result_typ in diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index deb48d6d0..2f671d597 100644 --- a/src/lib/parse_ast.ml +++ b/src/lib/parse_ast.ml @@ -124,6 +124,17 @@ type lit_aux = type lit = L_aux of lit_aux * l +module Config = struct + type config_aux = + (* JSON-style configuration structure *) + | Conf_object of (string * config) list + | Conf_list of config list + | Conf_num of Big_int.num + | Conf_string of string + + and config = Conf_aux of config_aux * l +end + type atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) | ATyp_id of id (* identifier *) @@ -192,7 +203,7 @@ type pat_aux = | P_cons of pat * pat (* cons pattern *) | P_string_append of pat list (* string append pattern, x ^^ y *) | P_struct of fpat list (* struct pattern *) - | P_attribute of string * string * pat + | P_attribute of string * Config.config option * pat and pat = P_aux of pat_aux * l @@ -247,7 +258,7 @@ and exp_aux = | E_return of exp | E_assert of exp * exp | E_var of exp * exp * exp - | E_attribute of string * string * exp + | E_attribute of string * Config.config option * exp | E_internal_plet of pat * exp * exp | E_internal_return of exp | E_internal_assume of atyp * exp @@ -295,7 +306,7 @@ type funcl = FCL_aux of funcl_aux * l and funcl_aux = (* Function clause *) | FCL_private of funcl - | FCL_attribute of string * string * funcl + | FCL_attribute of string * Config.config option * funcl | FCL_doc of string * funcl | FCL_funcl of id * pexp @@ -304,7 +315,7 @@ type type_union = Tu_aux of type_union_aux * l and type_union_aux = (* Type union constructors *) | Tu_private of type_union - | Tu_attribute of string * string * type_union + | Tu_attribute of string * Config.config option * type_union | Tu_doc of string * type_union | Tu_ty_id of atyp * id | Tu_ty_anon_rec of (atyp * id) list * id @@ -360,7 +371,7 @@ type mapcl = MCL_aux of mapcl_aux * l and mapcl_aux = (* mapping clause (bidirectional pattern-match) *) - | MCL_attribute of string * string * mapcl + | MCL_attribute of string * Config.config option * mapcl | MCL_doc of string * mapcl | MCL_bidir of mpexp * mpexp | MCL_forwards_deprecated of mpexp * exp @@ -447,7 +458,7 @@ type def_aux = | DEF_register of dec_spec (* register declaration *) | DEF_pragma of string * string * int | DEF_private of def - | DEF_attribute of string * string * def + | DEF_attribute of string * Config.config option * def | DEF_doc of string * def | DEF_internal_mutrec of fundef list diff --git a/src/lib/parser.mly b/src/lib/parser.mly index a4926a5b1..a28f9446f 100644 --- a/src/lib/parser.mly +++ b/src/lib/parser.mly @@ -71,6 +71,7 @@ module Big_int = Nat_big_num open Parse_ast +open Parse_ast.Config let loc n m = Range (n, m) @@ -262,7 +263,7 @@ let set_syntax_deprecated l = %token OpId %token Pragma -%token Attribute +%token Attribute %token Fixity @@ -271,11 +272,13 @@ let set_syntax_deprecated l = %start typ_eof %start exp_eof %start def_eof +%start config_eof %type typschm_eof %type typ_eof %type exp_eof %type def_eof %type file +%type config_eof %% @@ -547,7 +550,7 @@ pat1: pat: | pat1 { $1 } - | Attribute pat + | attribute pat { mk_pat (P_attribute (fst $1, snd $1, $2)) $startpos $endpos($1) } | pat1 As typ { mk_pat (P_var ($1, $3)) $startpos $endpos } @@ -639,7 +642,7 @@ internal_loop_measure: exp: | exp0 { $1 } - | Attribute exp + | attribute exp { mk_exp (E_attribute (fst $1, snd $1, $2)) $startpos $endpos($1) } | exp0 Eq exp { mk_exp (E_assign ($1, $3)) $startpos $endpos } @@ -864,10 +867,36 @@ vector_update_list: | vector_update Comma vector_update_list { $1 :: $3 } +config_key_value: + | key = String; Eq; value = config + { (key, value) } + +config: + | Lcurly; kvs = separated_list(Comma, config_key_value) Rcurly + { Conf_aux (Conf_object kvs, loc $startpos $endpos) } + | n = Num + { Conf_aux (Conf_num n, loc $startpos $endpos) } + | s = String + { Conf_aux (Conf_string s, loc $startpos $endpos) } + | id = Id + { Conf_aux (Conf_string id, loc $startpos $endpos) } + | Lsquare; xs = separated_list(Comma, config) Rsquare + { Conf_aux (Conf_list xs, loc $startpos $endpos) } + +attribute: + | attr = Attribute; Rsquare + { (attr, None) } + | attr = Attribute; c = config; Rsquare + { (attr, Some c) } + +config_eof: + | c = config; Eof + { c } + funcl_annotation: | visibility = Private { (fun funcl -> FCL_aux (FCL_private funcl, loc $startpos(visibility) $endpos(visibility))) } - | attr = Attribute + | attr = attribute { (fun funcl -> FCL_aux (FCL_attribute (fst attr, snd attr, funcl), loc $startpos(attr) $endpos(attr))) } | doc = Doc { (fun funcl -> FCL_aux (FCL_doc (doc, funcl), loc $startpos(doc) $endpos(doc))) } @@ -1036,7 +1065,7 @@ struct_fields: type_union: | visibility = Private; tu = type_union { Tu_aux (Tu_private tu, loc $startpos(visibility) $endpos(visibility)) } - | attr = Attribute; tu = type_union + | attr = attribute; tu = type_union { Tu_aux (Tu_attribute (fst attr, snd attr, tu), loc $startpos(attr) $endpos(attr)) } | doc = Doc; tu = type_union { Tu_aux (Tu_doc (doc, tu), loc $startpos(doc) $endpos(doc)) } @@ -1141,7 +1170,7 @@ fmpat: { mk_mpexp (MPat_when ($1, $3)) $startpos $endpos } mapcl: - | attr = Attribute; mcl = mapcl + | attr = attribute; mcl = mapcl { MCL_aux (MCL_attribute (fst attr, snd attr, mcl), loc $startpos(attr) $endpos(attr)) } | doc = Doc; mcl = mapcl { MCL_aux (MCL_doc (doc, mcl), loc $startpos(doc) $endpos(doc)) } @@ -1336,7 +1365,7 @@ def_aux: def: | visibility = Private; def = def { DEF_aux (DEF_private def, loc $startpos(visibility) $endpos(visibility)) } - | attr = Attribute; def = def + | attr = attribute; def = def { DEF_aux (DEF_attribute (fst attr, snd attr, def), loc $startpos(attr) $endpos(attr)) } | doc = Doc; def = def { DEF_aux (DEF_doc (doc, def), loc $startpos(doc) $endpos(doc)) } diff --git a/src/lib/pattern_completeness.ml b/src/lib/pattern_completeness.ml index 83b112c52..2377f8cb0 100644 --- a/src/lib/pattern_completeness.ml +++ b/src/lib/pattern_completeness.ml @@ -84,7 +84,7 @@ type ctx = { module type Config = sig type t val typ_of_t : t -> typ - val add_attribute : l -> string -> string -> t -> t + val add_attribute : l -> string -> config option -> t -> t end type row_index = { loc : l; num : int } @@ -298,7 +298,7 @@ module Make (C : Config) = struct | P_struct (fps, fwild) -> P_struct (List.map (fun (field, p) -> (field, go wild p)) fps, fwild) | P_id id -> P_id id | P_lit (L_aux (L_num n, _)) when wild -> - t := C.add_attribute (gen_loc l) "int_wildcard" (Big_int.to_string n) !t; + t := C.add_attribute (gen_loc l) "int_wildcard" (Some (Conf_aux (Conf_num n, gen_loc l))) !t; P_wild | P_lit _ when wild -> let typ = typ_of_pat full_pat in diff --git a/src/lib/pattern_completeness.mli b/src/lib/pattern_completeness.mli index 2cec79f79..2786a0ebb 100644 --- a/src/lib/pattern_completeness.mli +++ b/src/lib/pattern_completeness.mli @@ -85,7 +85,7 @@ type ctx = { module type Config = sig type t val typ_of_t : t -> typ - val add_attribute : l -> string -> string -> t -> t + val add_attribute : l -> string -> config option -> t -> t end module Make (C : Config) : sig diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index d31961985..8d48a8b90 100644 --- a/src/lib/pretty_print_sail.ml +++ b/src/lib/pretty_print_sail.ml @@ -81,8 +81,7 @@ let doc_id (Id_aux (id_aux, _)) = string (match id_aux with Id v -> v | Operator let doc_kid kid = string (Ast_util.string_of_kid kid) -let doc_attr attr arg = - if arg = "" then Printf.ksprintf string "$[%s]" attr ^^ space else Printf.ksprintf string "$[%s %s]" attr arg ^^ space +let doc_attr attr arg = string (string_of_attribute attr arg) ^^ space let doc_def_annot def_annot = (match def_annot.doc_comment with Some str -> string "/*!" ^^ string str ^^ string "*/" ^^ hardline | _ -> empty) diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 7a8baa002..8ff5207ff 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -1446,7 +1446,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp, (l, annot)) as full_exp) = -> let add_mapping_match (E_aux (e, (l, a)) as exp) = if Option.is_some (get_attribute "mapping_match" (untyped_annot annot)) then - E_aux (e, (l, map_uannot (add_attribute Parse_ast.Unknown "mapping_match" "") a)) + E_aux (e, (l, map_uannot (add_attribute Parse_ast.Unknown "mapping_match" None) a)) else exp in let clause = function diff --git a/src/lib/scattered.ml b/src/lib/scattered.ml index 56a29d990..165397ff7 100644 --- a/src/lib/scattered.ml +++ b/src/lib/scattered.ml @@ -196,8 +196,8 @@ let rec descatter' accumulator funcls mapcls = function | _ -> let def_annot = def_annot - |> add_def_attribute (gen_loc l) "no_enum_functions" "" - |> add_def_attribute (gen_loc l) "undefined_gen" "forbid" + |> add_def_attribute (gen_loc l) "no_enum_functions" None + |> add_def_attribute (gen_loc l) "undefined_gen" (Some (Conf_aux (Conf_string "forbid", gen_loc l))) in let accumulator = DEF_aux (DEF_type (TD_aux (TD_enum (id, members, false), (gen_loc l, Type_check.empty_tannot))), def_annot) diff --git a/src/lib/splice.ml b/src/lib/splice.ml index 88395ae52..eb3c187bc 100644 --- a/src/lib/splice.ml +++ b/src/lib/splice.ml @@ -124,7 +124,7 @@ let move_replacement_fundefs ast = { ast with defs = aux [] ast.defs } let annotate_ast ast = - let annotate_def (DEF_aux (d, a)) = DEF_aux (d, add_def_attribute a.loc "spliced" "" a) in + let annotate_def (DEF_aux (d, a)) = DEF_aux (d, add_def_attribute a.loc "spliced" None a) in { ast with defs = List.map annotate_def ast.defs } let splice ast file = diff --git a/src/lib/state.ml b/src/lib/state.ml index 2cf5bc33e..fda0cc5dc 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -145,7 +145,9 @@ let generate_regstate env registers = [ DEF_aux ( DEF_type (TD_aux (regstate_def, (Unknown, empty_uannot))), - add_def_attribute Unknown "undefined_gen" "forbid" (mk_def_annot Unknown) + add_def_attribute Unknown "undefined_gen" + (Some (Conf_aux (Conf_string "forbid", Unknown))) + (mk_def_annot Unknown) ); ] diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index e3fe8fd7b..20d382220 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -70,6 +70,7 @@ open Ast_defs open Ast_util open Util open Lazy +open Parse_ast.Config module Big_int = Nat_big_num @@ -1918,8 +1919,8 @@ let rec exp_unconditionally_returns (E_aux (aux, _)) = | E_block exps -> exp_unconditionally_returns (List.hd (List.rev exps)) | _ -> false -let forwards_attr l uannot = add_attribute l "forwards" "" (remove_attribute "forwards" uannot) -let backwards_attr l uannot = add_attribute l "backwards" "" (remove_attribute "backwards" uannot) +let forwards_attr l uannot = add_attribute l "forwards" None (remove_attribute "forwards" uannot) +let backwards_attr l uannot = add_attribute l "backwards" None (remove_attribute "backwards" uannot) let tc_assume nc (E_aux (aux, annot)) = E_aux (E_internal_assume (nc, E_aux (aux, annot)), annot) @@ -1969,8 +1970,8 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au let completeness_typ, env = bind_existential (exp_loc exp) None inferred_typ env in let ctx = pattern_completeness_ctx env in match PC.is_complete_wildcarded l ctx checked_cases completeness_typ with - | Some wildcarded -> (wildcarded, add_attribute (gen_loc l) "complete" "") - | None -> (checked_cases, add_attribute (gen_loc l) "incomplete" "") + | Some wildcarded -> (wildcarded, add_attribute (gen_loc l) "complete" None) + | None -> (checked_cases, add_attribute (gen_loc l) "incomplete" None) ) in annot_exp (E_match (inferred_exp, checked_cases)) typ |> update_uannot attr_update @@ -2451,13 +2452,11 @@ and bind_pat env (P_aux (pat_aux, (l, uannot)) as pat) typ = | P_wild -> let env = match get_attribute "int_wildcard" uannot with - | Some (_, arg) -> + | Some (_, Some (Conf_aux (Conf_num arg, _))) -> (* If the patterh completeness checker replaced an numeric pattern, modify the environment as if it hadn't *) - let _, env, _ = - bind_pat env (P_aux (P_lit (L_aux (L_num (Big_int.of_string arg), gen_loc l)), (l, uannot))) typ - in + let _, env, _ = bind_pat env (P_aux (P_lit (L_aux (L_num arg, gen_loc l)), (l, uannot))) typ in env - | None -> env + | _ -> env in (annot_pat P_wild typ, env, []) | P_or (pat1, pat2) -> @@ -4210,8 +4209,8 @@ let check_funcls_complete l env funcls typ = let typ_arg, _, env = bind_funcl_arg_typ l env typ in let ctx = pattern_completeness_ctx env in match PC.is_complete_funcls_wildcarded ~keyword:"function" l ctx funcls typ_arg with - | Some funcls -> (funcls, add_def_attribute (gen_loc l) "complete" "") - | None -> (funcls, add_def_attribute (gen_loc l) "incomplete" "") + | Some funcls -> (funcls, add_def_attribute (gen_loc l) "complete" None) + | None -> (funcls, add_def_attribute (gen_loc l) "incomplete" None) let empty_tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) @@ -4411,14 +4410,18 @@ let forbid_recursive_types type_l f = let extension_def_attribute env def_annot = match get_def_attribute "extension" def_annot with | Some (l, name) -> begin - match Env.get_current_visibility env with - | Private vis_l -> - raise - (Reporting.err_general - (Hint ("private scope started here", vis_l, l)) - "extension attribute within private scope" - ) - | Public -> Env.get_module_id_opt env name + match name with + | Some (Conf_aux (Conf_string name, _)) -> begin + match Env.get_current_visibility env with + | Private vis_l -> + raise + (Reporting.err_general + (Hint ("private scope started here", vis_l, l)) + "extension attribute within private scope" + ) + | Public -> Env.get_module_id_opt env name + end + | _ -> raise (Reporting.err_general l "Malformed extension attribute, expected a string argument") end | None -> None @@ -4440,8 +4443,8 @@ let check_record l env def_annot id typq fields = let env = try match get_def_attribute "bitfield" def_annot with - | Some (_, size) when not (Env.is_bitfield id env) -> - Env.add_bitfield id (bitvector_typ (nconstant (Big_int.of_string size))) Bindings.empty env + | Some (_, Some (Conf_aux (Conf_num size, _))) when not (Env.is_bitfield id env) -> + Env.add_bitfield id (bitvector_typ (nconstant size)) Bindings.empty env | _ -> env with _ -> env in @@ -4453,6 +4456,9 @@ let check_global_constraint env def_annot nc = typ_error def_annot.loc "Global constraint appears inconsistent with previous global constraints"; ([DEF_aux (DEF_constraint nc, def_annot)], env) +let undefined_skip l = Some (Conf_aux (Conf_string "skip", gen_loc l)) +let undefined_forbid l = Some (Conf_aux (Conf_string "forbid", gen_loc l)) + let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list * Env.t = fun env def_annot (TD_aux (tdef, (l, _))) -> typ_print (lazy ("\n" ^ Util.("Check type " |> cyan |> clear) ^ string_of_id (id_of_type_def_aux tdef))); @@ -4470,10 +4476,11 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list let env = check_record l env def_annot id typq fields in begin match get_def_attribute "undefined_gen" def_annot with - | Some (_, "forbid") -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) - | Some (_, "skip") -> + | Some (_, Some (Conf_aux (Conf_string "forbid", _))) -> + ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) + | Some (_, Some (Conf_aux (Conf_string "skip", _))) -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.allow_user_undefined id env) - | (Some (_, "generate") | None) as attr -> + | (Some (_, Some (Conf_aux (Conf_string "generate", _))) | None) as attr -> let field_env = Env.add_typquant l typq env in let field_env = List.fold_left @@ -4486,7 +4493,7 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list in if (not gen_undefined) && Option.is_none attr then ( (* If we cannot generate an undefined value, and we weren't explicitly asked to *) - let def_annot = add_def_attribute (gen_loc l) "undefined_gen" "forbid" def_annot in + let def_annot = add_def_attribute (gen_loc l) "undefined_gen" (undefined_forbid l) def_annot in ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) ) else if not gen_undefined then @@ -4499,21 +4506,23 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list let undefined_defs, env = check_defs env undefined_defs in let def_annot = def_annot |> remove_def_attribute "undefined_gen" - |> add_def_attribute (gen_loc l) "undefined_gen" "skip" + |> add_def_attribute (gen_loc l) "undefined_gen" (undefined_skip l) in ( DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot) :: undefined_defs, Env.allow_user_undefined id env ) with | Type_error _ when Option.is_none attr -> - let def_annot = add_def_attribute (gen_loc l) "undefined_gen" "forbid" def_annot in + let def_annot = add_def_attribute (gen_loc l) "undefined_gen" (undefined_forbid l) def_annot in ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) | Type_error _ -> typ_error l ("Cannot generate undefined function for struct " ^ string_of_id id) ) - | Some (attr_l, arg) -> + | Some (attr_l, Some arg) -> typ_error (Hint ("When checking this struct", l, attr_l)) - ("Unrecognized argument to undefined attribute: " ^ arg) + ("Unrecognized argument to undefined attribute: " ^ string_of_config arg) + | Some (attr_l, None) -> + typ_error (Hint ("When checking this struct", l, attr_l)) "No argument for undefined attribute" end | TD_variant (id, typq, arms, _) -> let rec_env = Env.add_variant id (typq, arms) env in @@ -4528,22 +4537,26 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list let env = Env.add_enum id ids env in begin match get_def_attribute "undefined_gen" def_annot with - | Some (_, "forbid") -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) - | Some (_, "skip") -> + | Some (_, Some (Conf_aux (Conf_string "forbid", _))) -> + ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) + | Some (_, Some (Conf_aux (Conf_string "skip", _))) -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.allow_user_undefined id env) - | Some (_, "generate") | None -> + | Some (_, Some (Conf_aux (Conf_string "generate", _))) | None -> let undefined_defs = Initial_check.generate_undefined_enum id ids in let undefined_defs, env = check_defs env undefined_defs in let def_annot = - def_annot |> remove_def_attribute "undefined_gen" |> add_def_attribute (gen_loc l) "undefined_gen" "skip" + def_annot |> remove_def_attribute "undefined_gen" + |> add_def_attribute (gen_loc l) "undefined_gen" (undefined_skip l) in ( DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot) :: undefined_defs, Env.allow_user_undefined id env ) - | Some (attr_l, arg) -> + | Some (attr_l, Some arg) -> typ_error (Hint ("When checking this enum", l, attr_l)) - ("Unrecognized argument to undefined attribute: " ^ arg) + ("Unrecognized argument to undefined attribute: " ^ string_of_config arg) + | Some (attr_l, None) -> + typ_error (Hint ("When checking this enum", l, attr_l)) "No argument for undefined attribute" end | TD_bitfield (id, typ, ranges) as unexpanded -> let typ = Env.expand_synonyms env typ in @@ -4566,7 +4579,7 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list let ranges = List.map (fun (f, r) -> (f, expand_range_synonyms r)) ranges |> List.to_seq |> Bindings.of_seq in - let def_annot = add_def_attribute l "bitfield" (Big_int.to_string size) def_annot in + let def_annot = add_def_attribute l "bitfield" (Some (Conf_aux (Conf_num size, l))) def_annot in let defs = DEF_aux (DEF_type (TD_aux (record_tdef, (l, empty_uannot))), def_annot) :: Bitfield.macro id size (Env.get_default_order env) ranges diff --git a/src/sail_doc_backend/docinfo.ml b/src/sail_doc_backend/docinfo.ml index 6b452cf76..bc9e075e7 100644 --- a/src/sail_doc_backend/docinfo.ml +++ b/src/sail_doc_backend/docinfo.ml @@ -75,6 +75,7 @@ open Libsail open Ast open Ast_defs open Ast_util +open Parse_ast.Config (** In the case of latex, we generate files containing a sequence of commands that can simply be included. For other documentation @@ -430,7 +431,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct in match find_attribute_opt "split" attrs with | None -> None - | Some split_id -> ( + | Some (Some (Conf_aux (Conf_string split_id, _))) -> ( let split_id = mk_id split_id in let env = Type_check.env_of exp in match Type_check.Env.lookup_id split_id env with @@ -452,6 +453,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct Some splits | _ -> raise (Reporting.err_general l ("Could not split on variable " ^ string_of_id split_id)) ) + | Some _ -> raise (Reporting.err_general l "Invalid argument for split attribute") let docinfo_for_funcl ~ast ?outer_annot n (FCL_aux (FCL_funcl (_, pexp), annot) as clause) = (* If we have just a single clause, we use the annotation for the @@ -520,7 +522,8 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct let docinfo_for_mapcl n (MCL_aux (aux, (def_annot, _)) as clause) = let source = doc_loc def_annot.loc Type_check.strip_mapcl Pretty_print_sail.doc_mapcl clause in - let wavedrom_attr = find_attribute_opt "wavedrom" def_annot.attrs in + let parse_wavedrom_attr = function Some (Conf_aux (Conf_string s, _)) -> Some s | Some _ | None -> None in + let wavedrom_attr = Option.bind (find_attribute_opt "wavedrom" def_annot.attrs) parse_wavedrom_attr in let left, left_wavedrom, right, right_wavedrom, body = match aux with