Config: Support enumerations in configuration files

language/jib.ott

@@ -96,6 +96,7 @@ op :: '' ::=
   | neq               :: :: neq
   | ite               :: :: ite
   | get_abstract      :: :: get_abstract
+  | string_eq         :: :: string_eq
 % Integer ops
   | lt                :: :: ilt
   | lteq              :: :: ilteq

src/lib/config.ml

@@ -61,6 +61,8 @@ let typ_is_variant env = function
   | Typ_aux (Typ_app (id, _), _) -> Env.is_variant id env
   | _ -> false
 
+let typ_is_enum env = function Typ_aux (Typ_id id, _) -> Env.is_enum id env | _ -> false
+
 let destruct_typ_args = function
   | Typ_aux (Typ_id id, _) -> Some (id, [])
   | Typ_aux (Typ_app (id, args), _) -> Some (id, args)
@@ -333,6 +335,10 @@ end = struct
             ]
           in
           Some (`Assoc variant_schema)
+      | [], NC_aux (NC_true, _), Typ_aux (Typ_id id, _) when Env.is_enum id env ->
+          let members = Env.get_enum id env in
+          Some
+            (`Assoc [("type", `String "string"); ("enum", `List (List.map (fun m -> `String (string_of_id m)) members))])
       | [], NC_aux (NC_true, _), Typ_aux (Typ_id id, _) -> (
           match string_of_id id with
           | "string" -> Some (`Assoc [("type", `String "string")])
@@ -526,6 +532,7 @@ let rec sail_exp_from_json ~at:l env typ =
   | `Intlit n -> mk_lit_exp ~loc:l (L_num (Big_int.of_string n))
   | `String s ->
       if Option.is_some (Type_check.destruct_numeric typ) then mk_lit_exp ~loc:l (L_num (Big_int.of_string s))
+      else if typ_is_enum env typ then mk_exp ~loc:l (E_id (mk_id ~loc:l s))
       else mk_lit_exp ~loc:l (L_string s)
   | `Bool true -> mk_lit_exp ~loc:l L_true
   | `Bool false -> mk_lit_exp ~loc:l L_false

src/lib/jib_compile.ml

@@ -685,6 +685,31 @@ module Make (C : CONFIG) = struct
       | CT_fbits _ ->
           config_extract CT_lbits json ~validate:("sail_config_is_bits", []) ~extract:"sail_config_unwrap_bits"
       | CT_bool -> config_extract CT_bool json ~validate:("sail_config_is_bool", []) ~extract:"sail_config_unwrap_bool"
+      | CT_enum (_, members) as enum_ctyp ->
+          let enum_name = ngensym () in
+          let enum_str = ngensym () in
+          let setup, get_string, cleanup =
+            config_extract CT_string json ~validate:("sail_config_is_string", []) ~extract:"sail_config_unwrap_string"
+          in
+          let enum_compare =
+            List.fold_left
+              (fun rest m ->
+                [
+                  iif l
+                    (V_call (String_eq, [V_id (enum_str, CT_string); V_lit (VL_string (string_of_id m), CT_string)]))
+                    [icopy l (CL_id (enum_name, enum_ctyp)) (V_member (m, enum_ctyp))]
+                    rest;
+                ]
+              )
+              [] members
+          in
+          ( [idecl l enum_ctyp enum_name; idecl l CT_string enum_str]
+            @ setup
+            @ [get_string (CL_id (enum_str, CT_string))]
+            @ enum_compare,
+            (fun clexp -> icopy l clexp (V_id (enum_name, enum_ctyp))),
+            cleanup @ [iclear CT_string enum_str; iclear enum_ctyp enum_name]
+          )
       | CT_variant (_, constructors) as variant_ctyp ->
           let variant_name = ngensym () in
           let ctor_checks, ctor_extracts =

src/lib/jib_util.ml

@@ -244,6 +244,7 @@ let string_of_op = function
   | Concat -> "@concat"
   | Ite -> "@ite"
   | Get_abstract -> "@get_abstract"
+  | String_eq -> "@string_eq"
 
 (* String representation of ctyps here is only for debugging and
    intermediate language pretty-printer. *)
@@ -1014,6 +1015,7 @@ let rec infer_call op vs =
     end
   | Ite, [_; t; _] -> cval_ctyp t
   | Get_abstract, [v] -> cval_ctyp v
+  | String_eq, _ -> CT_bool
   | _, _ -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Invalid call to function " ^ string_of_op op)
 
 and cval_ctyp = function

src/lib/type_check.mli

@@ -155,6 +155,8 @@ module Env : sig
 
   val is_record : id -> t -> bool
 
+  val is_enum : id -> t -> bool
+
   (** Returns record quantifiers and fields *)
   val get_record : id -> t -> typquant * (typ * id) list
 

src/lib/type_env.ml

@@ -1328,6 +1328,8 @@ let get_enum id env =
 
 let get_enums env = filter_items_with snd env env.global.enums
 
+let is_enum id env = Bindings.mem id env.global.enums
+
 let add_scattered_id id attrs env =
   let updater = function None -> Some (Ok attrs) | previous -> previous in
   update_global (fun global -> { global with scattered_ids = Bindings.update id updater global.scattered_ids }) env

src/lib/type_env.mli

@@ -212,6 +212,7 @@ val add_enum_clause : id -> id -> t -> t
 val get_enum_opt : id -> t -> id list option
 val get_enum : id -> t -> id list
 val get_enums : t -> IdSet.t Bindings.t
+val is_enum : id -> t -> bool
 
 val lookup_id : id -> t -> typ lvar
 

src/sail_c_backend/c_backend.ml

@@ -1096,6 +1096,7 @@ and sgen_call op cvals =
     end
   | Get_abstract, [v] -> sgen_cval v
   | Ite, [i; t; e] -> sprintf "(%s ? %s : %s)" (sgen_cval i) (sgen_cval t) (sgen_cval e)
+  | String_eq, [s1; s2] -> sprintf "(strcmp(%s, %s) == 0)" (sgen_cval s1) (sgen_cval s2)
   | _, _ -> failwith "Could not generate cval primop"
 
 let sgen_cval_param cval =

test/c/config_enum.expect

@@ -0,0 +1 @@
+B

test/c/config_enum.json

@@ -0,0 +1,5 @@
+{
+    "some" : {
+        "member" : "B"
+    }
+}

test/c/config_enum.sail

@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+$include <option.sail>
+
+$iftarget c
+$c_in_main sail_config_set_file("config_enum.json");
+$c_in_main_post sail_config_cleanup();
+$else
+$option --config ../c/config_enum.json
+$endif
+
+enum E = {A, B, C}
+
+val main : unit -> unit
+
+function main() = {
+  let x : E = config some.member;
+  match x {
+    A => print_endline("A"),
+    B => print_endline("B"),
+    C => print_endline("C"),
+  }
+}