Attribute improvements

language/sail.ott

@@ -77,7 +77,7 @@ open Value
 type text = string
 
 type l = Parse_ast.l
-type config = Parse_ast.Config.config
+type attribute_data = Parse_ast.Attribute_data.attribute_data
 
 type 'a annot = l * 'a
 
@@ -106,10 +106,10 @@ declare ocaml target_rep type ocaml_l = `Parse_ast.l`
 
 type l = ocaml_l
 
-type ocaml_config
-declare ocaml target_rep type ocaml_config = `Parse_ast.Config.config`
+type ocaml_attribute_data
+declare ocaml target_rep type ocaml_attribute_data = `Parse_ast.Attribute_data.attribute_data`
 
-type config = ocaml_config
+type attribute_data = ocaml_attribute_data
 
 type value
 declare ocaml target_rep type value = `Value.value`
@@ -124,7 +124,7 @@ type visibility = Public | Private of l
 
 type def_annot = <|
     doc_comment : maybe string;
-    attrs : list (l * string * maybe config);
+    attrs : list (l * string * maybe attribute_data);
     visibility : visibility;
     loc : l
 |>

src/lib/ast_util.ml

@@ -67,24 +67,27 @@
 
 open Ast
 open Ast_defs
-open Parse_ast.Config
+open Parse_ast.Attribute_data
 open Util
 module Big_int = Nat_big_num
 
 (* The type of annotations for untyped AST nodes *)
-type uannot = { attrs : (l * string * config option) list }
+type uannot = { attrs : (l * string * attribute_data option) list }
 
-let rec string_of_config (Conf_aux (aux, _)) =
+let rec string_of_attribute_data (AD_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 ^ "]"
+  | AD_object kvs ->
+      "{ "
+      ^ Util.string_of_list ", " (fun (k, v) -> Printf.sprintf "\"%s\" = %s" k (string_of_attribute_data v)) kvs
+      ^ " }"
+  | AD_string s -> "\"" ^ s ^ "\""
+  | AD_num n -> Big_int.to_string n
+  | AD_list cs -> "[" ^ Util.string_of_list ", " string_of_attribute_data cs ^ "]"
+  | AD_bool b -> string_of_bool b
 
 let string_of_attribute attr = function
   | None -> Printf.sprintf "$[%s]" attr
-  | Some config -> Printf.sprintf "$[%s %s]" attr (string_of_config config)
+  | Some data -> Printf.sprintf "$[%s %s]" attr (string_of_attribute_data data)
 
 let empty_uannot = { attrs = [] }
 

src/lib/ast_util.mli

@@ -80,9 +80,9 @@ type uannot
 
 val empty_uannot : uannot
 
-val string_of_attribute : string -> config option -> string
+val string_of_attribute : string -> attribute_data option -> string
 
-val string_of_config : config -> string
+val string_of_attribute_data : attribute_data -> string
 
 (** Add an attribute to an annotation. Attributes are attached to expressions in Sail  via:
     {@sail[
@@ -91,21 +91,22 @@ val string_of_config : config -> string
     The location argument should be a span that corresponds to the attribute itself, and not
     include the expression.
 *)
-val add_attribute : l -> string -> config option -> uannot -> uannot
+val add_attribute : l -> string -> attribute_data option -> uannot -> uannot
 
 val remove_attribute : string -> uannot -> uannot
 
-val get_attribute : string -> uannot -> (l * config option) option
+val get_attribute : string -> uannot -> (l * attribute_data option) option
 
-val get_attributes : uannot -> (l * string * config option) list
+val get_attributes : uannot -> (l * string * attribute_data option) list
 
-val find_attribute_opt : string -> (l * string * config option) list -> config option option
+val find_attribute_opt : string -> (l * string * attribute_data option) list -> attribute_data option option
 
-val mk_def_annot : ?doc:string -> ?attrs:(l * string * config option) list -> ?visibility:visibility -> l -> def_annot
+val mk_def_annot :
+  ?doc:string -> ?attrs:(l * string * attribute_data option) list -> ?visibility:visibility -> l -> def_annot
 
-val add_def_attribute : l -> string -> config option -> def_annot -> def_annot
+val add_def_attribute : l -> string -> attribute_data option -> def_annot -> def_annot
 
-val get_def_attribute : string -> def_annot -> (l * config option) option
+val get_def_attribute : string -> def_annot -> (l * attribute_data option) option
 
 val remove_def_attribute : string -> def_annot -> def_annot
 

src/lib/jib_compile.ml

@@ -68,7 +68,7 @@
 open Ast
 open Ast_defs
 open Ast_util
-open Parse_ast.Config
+open Parse_ast.Attribute_data
 open Jib
 open Jib_util
 open Jib_visitor
@@ -193,8 +193,8 @@ let initial_ctx env effect_info =
   }
 
 let update_coverage_override' ctx = function
-  | Some (_, Some (Conf_aux (Conf_string "on", _))) -> { ctx with coverage_override = true }
-  | Some (_, Some (Conf_aux (Conf_string "off", _))) -> { ctx with coverage_override = false }
+  | Some (_, Some (AD_aux (AD_string "on", _))) -> { ctx with coverage_override = true }
+  | Some (_, Some (AD_aux (AD_string "off", _))) -> { ctx with coverage_override = false }
   | _ -> ctx
 
 let update_coverage_override uannot ctx = update_coverage_override' ctx (get_attribute "coverage" uannot)

src/lib/monomorphise.ml

@@ -4159,7 +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 (_, Some (Conf_aux (Conf_num i, _))) ->
+                        | _, Some (_, Some (AD_aux (AD_num i, _))) ->
                             let src_typ =
                               fill_in_type (Env.add_constraint (nc_eq (nvar kid) (nconstant i)) env) result_typ
                             in

src/lib/parse_ast.ml

@@ -76,19 +76,24 @@ type l =
   | Hint of string * l * l
   | Range of Lexing.position * Lexing.position
 
-(* Put the config type in it's own module, so other modules can import
-   it unqualified. *)
-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
+(** We put the attribute data type in it's own module, so other
+    modules can import it unqualified. The parse AST and the main AST
+    share this type, so modules that wouldn't normally import this
+    module will want to use it. *)
+module Attribute_data = struct
+  type attribute_data_aux =
+    | AD_object of (string * attribute_data) list
+    | AD_list of attribute_data list
+    | AD_num of Big_int.num
+    | AD_string of string
+    | AD_bool of bool
+
+  (** JSON-style data structure for attributes *)
+  and attribute_data = AD_aux of attribute_data_aux * l
 end
 
+open Attribute_data
+
 type 'a annot = l * 'a
 
 type extern = { pure : bool; bindings : (string * string) list }
@@ -203,7 +208,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 * Config.config option * pat
+  | P_attribute of string * attribute_data option * pat
 
 and pat = P_aux of pat_aux * l
 
@@ -258,7 +263,7 @@ and exp_aux =
   | E_return of exp
   | E_assert of exp * exp
   | E_var of exp * exp * exp
-  | E_attribute of string * Config.config option * exp
+  | E_attribute of string * attribute_data option * exp
   | E_internal_plet of pat * exp * exp
   | E_internal_return of exp
   | E_internal_assume of atyp * exp
@@ -306,7 +311,7 @@ type funcl = FCL_aux of funcl_aux * l
 and funcl_aux =
   (* Function clause *)
   | FCL_private of funcl
-  | FCL_attribute of string * Config.config option * funcl
+  | FCL_attribute of string * attribute_data option * funcl
   | FCL_doc of string * funcl
   | FCL_funcl of id * pexp
 
@@ -315,7 +320,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 * Config.config option * type_union
+  | Tu_attribute of string * attribute_data option * type_union
   | Tu_doc of string * type_union
   | Tu_ty_id of atyp * id
   | Tu_ty_anon_rec of (atyp * id) list * id
@@ -371,7 +376,7 @@ type mapcl = MCL_aux of mapcl_aux * l
 
 and mapcl_aux =
   (* mapping clause (bidirectional pattern-match) *)
-  | MCL_attribute of string * Config.config option * mapcl
+  | MCL_attribute of string * attribute_data option * mapcl
   | MCL_doc of string * mapcl
   | MCL_bidir of mpexp * mpexp
   | MCL_forwards_deprecated of mpexp * exp
@@ -458,7 +463,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 * Config.config option * def
+  | DEF_attribute of string * attribute_data option * def
   | DEF_doc of string * def
   | DEF_internal_mutrec of fundef list
 

src/lib/parser.mly

@@ -71,7 +71,7 @@
 
 module Big_int = Nat_big_num
 open Parse_ast
-open Parse_ast.Config
+open Parse_ast.Attribute_data
 
 let loc n m = Range (n, m)
 
@@ -272,13 +272,13 @@ let set_syntax_deprecated l =
 %start typ_eof
 %start exp_eof
 %start def_eof
-%start config_eof
+%start attribute_data_eof
 %type <Parse_ast.typschm> typschm_eof
 %type <Parse_ast.atyp> typ_eof
 %type <Parse_ast.exp> exp_eof
 %type <Parse_ast.def> def_eof
 %type <Parse_ast.def list> file
-%type <Parse_ast.Config.config> config_eof
+%type <Parse_ast.Attribute_data.attribute_data> attribute_data_eof
 
 %%
 
@@ -867,31 +867,35 @@ vector_update_list:
   | vector_update Comma vector_update_list
     { $1 :: $3 }
 
-config_key_value:
-  | key = String; Eq; value = config
+attribute_data_key_value:
+  | key = String; Eq; value = attribute_data
     { (key, value) }
 
-config:
-  | Lcurly; kvs = separated_list(Comma, config_key_value) Rcurly
-    { Conf_aux (Conf_object kvs, loc $startpos $endpos) }
+attribute_data:
+  | Lcurly; kvs = separated_list(Comma, attribute_data_key_value) Rcurly
+    { AD_aux (AD_object kvs, loc $startpos $endpos) }
   | n = Num
-    { Conf_aux (Conf_num n, loc $startpos $endpos) }
+    { AD_aux (AD_num n, loc $startpos $endpos) }
   | s = String
-    { Conf_aux (Conf_string s, loc $startpos $endpos) }
+    { AD_aux (AD_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) }
+    { AD_aux (AD_string id, loc $startpos $endpos) }
+  | True
+    { AD_aux (AD_bool true, loc $startpos $endpos) }
+  | False
+    { AD_aux (AD_bool false, loc $startpos $endpos) }
+  | Lsquare; xs = separated_list(Comma, attribute_data) Rsquare
+    { AD_aux (AD_list xs, loc $startpos $endpos) }
 
 attribute:
   | attr = Attribute; Rsquare
     { (attr, None) }
-  | attr = Attribute; c = config; Rsquare
-    { (attr, Some c) }
+  | attr = Attribute; d = attribute_data; Rsquare
+    { (attr, Some d) }
 
-config_eof:
-  | c = config; Eof
-    { c }
+attribute_data_eof:
+  | d = attribute_data; Eof
+    { d }
 
 funcl_annotation:
   | visibility = Private

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 -> config option -> t -> t
+  val add_attribute : l -> string -> attribute_data 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" (Some (Conf_aux (Conf_num n, gen_loc l))) !t;
+            t := C.add_attribute (gen_loc l) "int_wildcard" (Some (AD_aux (AD_num n, gen_loc l))) !t;
             P_wild
         | P_lit _ when wild ->
             let typ = typ_of_pat full_pat in

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 -> config option -> t -> t
+  val add_attribute : l -> string -> attribute_data option -> t -> t
 end
 
 module Make (C : Config) : sig

src/lib/reporting.mli

@@ -143,12 +143,12 @@ val err_lex : Lexing.position -> string -> exn
 
 (** Raise an unreachable exception.
 
-This should always be used over an assert false or a generic OCaml failwith exception when appropriate *)
+This should always be used over an assert false or a generic OCaml failwith exception when appropriate. *)
 val unreachable : Parse_ast.l -> string * int * int * int -> string -> 'a
 
 (** Print an error to stdout.
 
-@param interactive If this is true (default false) then unreachable errors are reported as general errors. 
+@param interactive If this is true (default false) then unreachable errors are reported as general errors.
 This is used by the interactive read-eval-print loop. The interactive mode exposes a lot of internal features, so
 it's possible to excute code paths from the interactive mode that would otherwise be unreachable during normal execution. *)
 val print_error : ?interactive:bool -> error -> unit

src/lib/scattered.ml

@@ -197,7 +197,7 @@ let rec descatter' accumulator funcls mapcls = function
             let def_annot =
               def_annot
               |> 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)))
+              |> add_def_attribute (gen_loc l) "undefined_gen" (Some (AD_aux (AD_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)

src/lib/state.ml

@@ -145,9 +145,7 @@ let generate_regstate env registers =
   [
     DEF_aux
       ( DEF_type (TD_aux (regstate_def, (Unknown, empty_uannot))),
-        add_def_attribute Unknown "undefined_gen"
-          (Some (Conf_aux (Conf_string "forbid", Unknown)))
-          (mk_def_annot Unknown)
+        add_def_attribute Unknown "undefined_gen" (Some (AD_aux (AD_string "forbid", Unknown))) (mk_def_annot Unknown)
       );
   ]