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..67c289d8a 100644
--- a/src/lib/parse_ast.ml
+++ b/src/lib/parse_ast.ml
@@ -65,8 +65,6 @@
 (*  SUCH DAMAGE.                                                            *)
 (****************************************************************************)
 
-(* generated by Ott 0.25 from: l2_parse.ott *)
-
 module Big_int = Nat_big_num
 
 type text = string
@@ -78,6 +76,19 @@ 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
+end
+
 type 'a annot = l * 'a
 
 type extern = { pure : bool; bindings : (string * string) list }
@@ -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 <string> OpId
 
 %token <string * string> Pragma
-%token <string * string> Attribute
+%token <string> Attribute
 
 %token <Parse_ast.fixity_token> Fixity
 
@@ -271,11 +272,13 @@ let set_syntax_deprecated l =
 %start typ_eof
 %start exp_eof
 %start def_eof
+%start config_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
 
 %%
 
@@ -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