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

@@ -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 }}

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                                         %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

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 = [] }
 

src/lib/ast_util.mli

@@ -80,28 +80,32 @@ 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
     ]}
     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
 

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)

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

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))

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 =

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)

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

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,15 +297,15 @@ 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 =
           rewrite_match_untyped is_mapping subst (mk_exp (E_id head_exp_tmp)) msa.after_arms (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

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

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