Config: Further documentation

doc/asciidoc/.gitignore

@@ -1,4 +1,6 @@
 sail_doc/
+sail_config/
+sail_schema/
 lib_sail_doc/
 module_sail_doc/
 

doc/asciidoc/Makefile

@@ -20,8 +20,16 @@ SAIL_DOCS += sail_doc/enum.json
 SAIL_DOCS += sail_doc/union.json
 SAIL_DOCS += sail_doc/config.json
 SAIL_DOCS += sail_doc/config_basic_types.json
+SAIL_DOCS += sail_doc/config_vector.json
+SAIL_DOCS += sail_doc/config_user_types.json
+SAIL_DOCS += sail_doc/config_schema.json
 SAIL_DOCS += sail_config/config.json
 SAIL_DOCS += sail_config/config_basic_types.json
+SAIL_DOCS += sail_config/config_vector.json
+SAIL_DOCS += sail_config/config_user_types.json
+SAIL_DOCS += sail_config/config_schema.json
+SAIL_DOCS += sail_schema/config_schema.json
+SAIL_DOCS += sail_schema/config_schema.output
 SAIL_DOCS += sail_doc/type_syn.json
 SAIL_DOCS += sail_doc/type_syn_xlen.json
 SAIL_DOCS += sail_doc/abstract_xlen.json
@@ -40,13 +48,20 @@ all: manual.html manual.pdf
 
 sail_doc/%.json: ../examples/%.sail
 	mkdir -p sail_doc
-	sail --no-color -doc --doc-file $< --doc-embed plain --doc-bundle $(notdir $@) $< 2> $(basename $@).warning
+	sail --no-color --doc --doc-file $< --doc-embed plain --doc-bundle $(notdir $@) $< 2> $(basename $@).warning
 
 sail_config/%.json: ../examples/%.json
 	mkdir -p sail_config
 	cp $< $@
 	-sail $(basename $<).sail --config $< 2> $(basename $@).error
 
+sail_schema/%.json: ../examples/%.sail
+	mkdir -p sail_schema
+	sail --no-color $< --output-schema $@
+
+sail_schema/%.output: sail_schema/%.json sail_config/%.json
+	-boon $(word 1,$^) $(word 2,$^) | sed '/jsonschema validation failed/d' > $@
+
 sail_doc/%.error: ../examples/%.sail
 	mkdir -p sail_doc
 	-sail --no-color $< 2> $@

doc/asciidoc/configuration.adoc

@@ -27,9 +27,9 @@ convert the Sail source to OCaml), we could run the following,
 assuming the configration file is called `file.json` and the Sail file
 containing the above code is `file.sail`.
 
-[source,sh]
+[source,console]
 ----
-sail --ocaml --config file.json file.sail
+$ sail --ocaml --config file.json file.sail
 ----
 
 === JSON representation of Sail types
@@ -68,11 +68,57 @@ prefixed literals, a decimal value can also be used (also supporting
 { "len" : 32, "value" : "1_000_000" }
 ----
 
+:confvec: sail_doc/config_vector.json
+
 There are some cases where a specification might need many
 configuration options. Consider the case of RISC-V PMP registers,
 where there are up to 64 such registers, and each one might be
 configured differently. To support this, we allow reading sequences of
-JSON values into Sail vectors and lists.
+JSON values into Sail vectors and lists. For example:
+
+sail::example[from=confvec,part=body,dedent]
+
+with the configuration file:
+
+[source,json]
+----
+include::sail_config/config_vector.json[]
+----
+
+:confuser: sail_doc/config_user_types.json
+
+More complex user defined types can also be read from the
+configuration file. For example, one can read a struct value:
+
+[source,sail]
+----
+include::sail:my_struct[from=confuser,type=type]
+
+include::sail:example1[from=confuser]
+----
+
+or a union value:
+
+[source,sail]
+----
+include::sail:my_union[from=confuser,type=type]
+
+include::sail:example2[from=confuser]
+----
+
+from the configuration file:
+
+[source,json]
+----
+include::sail_config/config_user_types.json[]
+----
+
+A Sail struct is represented as a JSON object with keys and values for
+each field in the struct. There must be a key in the JSON object for
+every field. A Sail union is represented as a JSON object with exactly
+one key/value pair. The key must be the name of a constructor in the
+union, and the value is parsed as the type of the constructor
+argument.
 
 === Runtime Configuration with Sail to C
 
@@ -91,3 +137,60 @@ void sail_config_cleanup(void);
 ----
 
 === Validating Configurations with JSON Schema
+
+:confschema: sail_doc/config_schema.json
+
+Above, we discussed how JSON values are mapped onto Sail types, but
+some questions remain:
+
+* What happens if the configuration we pass at runtime contains impossible values?
+* Are all Sail types representable in the JSON configuration?
+
+Note that what we are defining here will necessarily be a weaker
+notion (i.e. more permissive in the configurations that are possible)
+than one might consider as the valid configuration space for an ISA
+definition, as it cannot capture all possible dependencies between different
+configuration options.
+
+What we want to do is capture is some basic notion of _safety_, i.e.
+what values can we pass into the model at runtime that won't break
+Sail's typing rules. For example, we might have:
+
+sail::example[from=confschema,part=body,dedent]
+
+Then, using the configuration
+
+[source,json]
+----
+include::sail_config/config_schema.json[]
+----
+
+we would potentially have some serious problems. Sail could optimize
+the source using the type annotation that `n` is only 32 or 64, so
+when we pass 72 at runtime, type-safety would be violated and the
+model could potentially fail or even exhibit undefined-behaviour when
+compiled to C! Naturally, we want a way to prevent this from occuring.
+
+To do this we create a https://json-schema.org[JSON schema] from the
+way in which the Sail source interacts with the model. JSON schema is
+an open standard with a wide variety of validators and tooling written
+in multiple languages.
+
+For the above simple example, the following schema will be generated
+by Sail when using the `--output-schema` option:
+
+[source,json]
+----
+include::sail_schema/config_schema.json[]
+----
+
+Now if we attempt to validate the above schema using the JSON
+containing 72 as the value for the integer, we will get an error
+
+----
+include::sail_schema/config_schema.output[]
+----
+
+In general, whenever we have `config key : T` in the Sail source, we
+require that the type `T` can be converted into a JSON schema, and
+raise an error if this is not possible.

doc/examples/config_schema.json

@@ -0,0 +1,5 @@
+{
+    "some" : {
+        "integer" : 72
+    }
+}

doc/examples/config_schema.sail

@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+val example : unit -> unit
+
+function example() = {
+  let n : {32, 64} = config some.integer;
+}

doc/examples/config_user_types.json

@@ -0,0 +1,11 @@
+{
+    "some" : {
+        "json_struct" : {
+            "field1" : 3287589457,
+            "field2" : "A string value"
+        },
+        "json_union" : {
+            "Constructor2" : "Another string value"
+        }
+    }
+}

doc/examples/config_user_types.sail

@@ -0,0 +1,30 @@
+default Order dec
+
+$include <prelude.sail>
+
+struct my_struct = {
+  field1 : int,
+  field2 : string,
+}
+
+val example1 : unit -> unit
+
+function example1() = {
+  let v : my_struct = config some.json_struct;
+  print_endline(v.field2);
+}
+
+union my_union = {
+  Constructor1 : int,
+  Constructor2 : string,
+}
+
+val example2 : unit -> unit
+
+function example2() = {
+  let v : my_union = config some.json_union;
+  match v {
+    Constructor1(n) => print_int("Got integer ", n),
+    Constructor2(message) => print_endline(message),
+  }
+}

doc/examples/config_vector.sail

@@ -8,5 +8,5 @@ function example() = {
   let some_vector : vector(5, int) = config some.json_list;
 
   // We can also read the configuration value into a Sail list
-  let some_list = list(int) = config some.json_list;
+  let some_list : list(int) = config some.json_list;
 }

src/lib/config.ml

@@ -371,7 +371,7 @@ end = struct
         in
         let properties = List.sort (fun (p1, _) (p2, _) -> String.compare p1 p2) properties in
         let required = ("required", `List (List.map (fun (p, _) -> `String p) properties)) in
-        `Assoc (("type", `String "object") :: required :: properties)
+        `Assoc [("type", `String "object"); ("properties", `Assoc properties); required]
     | Sail_value (config_type, []) -> type_schema_or_error config_type
     | Sail_value (config_type, config_types) ->
         let schemas = config_type :: config_types |> List.map type_schema_or_error in