Config: Generate JSON Schema based on spec configuration types

Second, for each type [T] attached to a configuration node (which
may have been inferred from context by the type system), we will
also attempt to synthesise a JSON Schema. If [T] cannot be turned
into a valid schema then this function raises a fatal type error
exception. This schema cannot capture every possible invariant of
an ISA configuration, but it does provide enough to guarantee that
a configuration applied at runtime will not break type-safety
assuming it validates against the schema.

Parse more kinds of JSON values, including vectors and lists

lib/json/sail_config.c

@@ -29,6 +29,8 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                   */
 /****************************************************************************/
 
+#include <string.h>
+
 #include "sail_config.h"
 #include "cJSON.h"
 
@@ -76,12 +78,11 @@ void sail_config_cleanup(void)
   sail_free(sail_config);
 }
 
-void sail_config_get_string(sail_string *str, size_t n, const char *key[])
+sail_config_json sail_config_get(size_t n, const char *key[])
 {
+  sail_config_json result;
   cJSON *json = (cJSON *)sail_config;
 
-  sail_free(*str);
-
   for (int i = 0; i < n; i++) {
     if (cJSON_IsObject(json)) {
       json = cJSON_GetObjectItemCaseSensitive(json, key[i]);
@@ -90,27 +91,26 @@ void sail_config_get_string(sail_string *str, size_t n, const char *key[])
     }
   }
 
-  if (cJSON_IsString(json)) {
-    *str = cJSON_GetStringValue(json);
-  } else {
-    sail_assert(false, "Expected string value in config");
-  }
+  return (sail_config_json)json;
 }
 
-sail_config_json sail_config_get(size_t n, const char *key[])
+int64_t sail_config_list_length(const sail_config_json config)
 {
-  sail_config_json result;
-  cJSON *json = (cJSON *)sail_config;
+  cJSON *json = (cJSON *)config;
 
-  for (int i = 0; i < n; i++) {
-    if (cJSON_IsObject(json)) {
-      json = cJSON_GetObjectItemCaseSensitive(json, key[i]);
-    } else {
-      sail_assert(false, "Failed to access config item");
-    }
+  if (cJSON_IsArray(json)) {
+    return (int64_t)cJSON_GetArraySize(json);
+  } else {
+    return INT64_C(-1);
   }
+}
 
-  return (sail_config_json)json;
+sail_config_json sail_config_list_nth(const sail_config_json config, int64_t index)
+{
+  // This is very inefficient, but works with how the Jib IR functions
+  cJSON *json = (cJSON *)config;
+  cJSON *item = cJSON_GetArrayItem(json, (int)index);
+  return (sail_config_json)item;
 }
 
 bool sail_config_is_object(const sail_config_json config)
@@ -169,7 +169,11 @@ bool sail_config_is_bool_array_with_size(const sail_config_json config, mach_int
 
 void sail_config_unwrap_string(sail_string *str, const sail_config_json config)
 {
-  *str = cJSON_GetStringValue((cJSON *)config);
+  sail_string conf_str = cJSON_GetStringValue((cJSON *)config);
+
+  size_t len = strlen(conf_str);
+  *str = (sail_string)realloc(*str, len + 1);
+  *str = strcpy(*str, conf_str);
 }
 
 void sail_config_unwrap_int(sail_int *n, const sail_config_json config)

lib/json/sail_config.h

@@ -67,37 +67,34 @@ void sail_config_set_file(const char *path);
 void sail_config_cleanup();
 
 /*
- * Extract a string value from the JSON configuration.
+ * Get the JSON corresponding to some key
  */
-void sail_config_get_string(sail_string *str, const size_t n, const_sail_string key[]);
+sail_config_json sail_config_get(const size_t n, const_sail_string key[]);
 
 /*
- * For more complex Sail types than just strings, Sail will generate code that will
- * destructure the JSON values using the following function calls.
+ * For each Sail type, Sail will generate code that will destructure
+ * the JSON values using the following function calls.
  *
  * In general, it will test if the JSON is the type it expects, and
  * only then access the fields. The behaviour of these functions is
  * not guaranteed if the JSON does not have the correct type.
  */
 
-sail_config_json sail_config_get(const size_t n, const_sail_string key[]);
-
 bool sail_config_is_object(const sail_config_json config);
-
 bool sail_config_object_has_key(const sail_config_json config, const sail_string key);
-
 sail_config_json sail_config_object_key(const sail_config_json config, const sail_string key);
 
+int64_t sail_config_list_length(const sail_config_json config);
+sail_config_json sail_config_list_nth(const sail_config_json config, int64_t index);
+
 bool sail_config_is_string(const sail_config_json config);
 
 bool sail_config_is_array(const sail_config_json config);
 bool sail_config_is_bool_array(const sail_config_json config);
 bool sail_config_is_bool_array_with_size(const sail_config_json config, mach_int expected);
 
 void sail_config_unwrap_string(sail_string *str, const sail_config_json config);
-
 void sail_config_unwrap_int(sail_int *n, const sail_config_json config);
-
 void sail_config_unwrap_bits(lbits *bv, const sail_config_json config);
 
 #ifdef __cplusplus

lib/sail.h

@@ -147,7 +147,6 @@ bool EQUAL(sail_string)(const_sail_string, const_sail_string);
 void concat_str(sail_string *stro, const_sail_string str1, const_sail_string str2);
 bool string_startswith(const_sail_string s, const_sail_string prefix);
 
-
 /* ***** Sail integers ***** */
 
 typedef int64_t mach_int;

src/bin/sail.ml

@@ -76,6 +76,8 @@ let opt_format_backup : string option ref = ref None
 let opt_format_only : string list ref = ref []
 let opt_format_skip : string list ref = ref []
 let opt_slice_instantiation_types : bool ref = ref false
+let opt_output_schema_file : string option ref = ref None
+
 let is_bytecode = Sys.backend_type = Bytecode
 
 (* Allow calling all options as either -foo_bar, -foo-bar, or
@@ -252,6 +254,10 @@ let rec options =
       ("-all_modules", Arg.Set opt_all_modules, " use all modules in project file");
       ("-list_files", Arg.Set Frontend.opt_list_files, " list files used in all project files");
       ("-config", Arg.String (fun file -> opt_config_file := Some file), "<file> configuration file");
+      ( "-output-schema",
+        Arg.String (fun file -> opt_output_schema_file := Some file),
+        "<file> output configuration schema"
+      );
       ("-abstract_types", Arg.Set Initial_check.opt_abstract_types, " (experimental) allow abstract types");
       ("-fmt", Arg.Set opt_format, " format input source code");
       ( "-fmt_backup",
@@ -506,11 +512,19 @@ let run_sail (config : Yojson.Safe.t option) tgt =
           )
   in
   let ast = Frontend.instantiate_abstract_types (Some tgt) !opt_instantiations ast in
-  let ast = apply_model_config env ast in
+  let schema, ast = apply_model_config env ast in
   let ast, env = Frontend.initial_rewrite effect_info env ast in
   let ast, env = match !opt_splice with [] -> (ast, env) | files -> Splice.splice_files ctx ast (List.rev files) in
   let effect_info = Effects.infer_side_effects (Target.asserts_termination tgt) ast in
 
+  ( match !opt_output_schema_file with
+  | None -> ()
+  | Some file ->
+      let out = Util.open_output_with_check file in
+      Yojson.Safe.pretty_to_channel ~std:true out.channel schema;
+      Util.close_output_with_check out
+  );
+
   (* Don't show warnings during re-writing for now *)
   Reporting.suppressed_warning_info ();
   Reporting.opt_warnings := false;