Generate benchcomp.yaml documentation from schema

docs/book.toml

@@ -12,6 +12,7 @@ multilingual = false
 site-url = "/kani/"
 git-repository-url = "https://github.com/model-checking/kani"
 edit-url-template = "https://github.com/model-checking/kani/edit/main/docs/{path}"
+additional-css = ["src/schema.css"]
 
 [output.html.playground]
 runnable = false

docs/src/benchcomp-conf.md

@@ -1,8 +1,41 @@
 # `benchcomp` configuration file
 
 `benchcomp`'s operation is controlled through a YAML file---`benchcomp.yaml` by default or a file passed to the `-c/--config` option.
-This page lists the different visualizations that are available.
+This section documents the top-level schema and the different visualizations
+that are available.
 
+## Configuration file
+
+The schema for `benchcomp.yaml` is shown below:
+
+{{#include ../gen_src/BenchcompYaml.md}}
+
+A minimal example of such a file is:
+
+```yaml
+run:
+  suites:
+    suite_1:
+      parser:
+        command: ./parse_suite1.py
+      variants:
+        - suite_1_old
+        - suite_1_new
+variants:
+  suite_1_old:
+    config:
+      command: ./scripts/run_benchmarks.sh
+      directory: suites/suite_1_old
+      env: {}
+  suite_1_new:
+    config:
+      command: ./scripts/run_benchmarks.sh
+      directory: suites/suite_1_new
+      env: {}
+visualize:
+- type: run_command
+  command: ./my_visualization.py
+```
 
 ## Built-in visualizations
 

docs/src/schema.css

@@ -0,0 +1,28 @@
+/* Copyright Kani Contributors
+ * SPDX-License-Identifier: Apache-2.0 OR MIT
+ */
+
+.schema_key {
+  font-weight: bold !important;
+  color: #dc322f !important;
+}
+.schema_type {
+  color: #6c71c4 !important;
+  text-decoration: underline !important;
+}
+.schema_desc {
+  opacity: 35% !important;
+  margin-left: 1em !important;
+  font-style: italic !important;
+}
+.schema_comb {
+  color: #268bd2 !important;
+}
+ul.schema li {
+  list-style: none !important;
+}
+ul.schema {
+  padding-left: 2em !important;
+  background-color: #00000005 !important;
+  border-left: solid 2px #00000005 !important;
+}

docs/src/schema.jinja2.html

@@ -0,0 +1,62 @@
+{# Copyright Kani Contributors #}
+{# SPDX-License-Identifier: Apache-2.0 OR MIT #}
+
+{% if schema.type_name == "list" %}
+<ul class="schema">
+  {% for sub_property in schema.iterate_properties %}
+  <li>- {{ sub_property.property_name }}</li>
+  {% endfor %}
+</ul>
+{% endif %}
+
+{% if schema.type_name == "object" %}
+<ul class="schema">
+  {% for sub_property in schema.iterate_properties %}
+    {% if sub_property.property_name %}
+    <li>
+      {% if sub_property.property_name == "_str" %}
+      {% set name = "string" %}
+      {% set type = "schema_type" %}
+      {% else %}
+      {% set name = sub_property.property_name %}
+      {% set type = "schema_key" %}
+      {% endif %}
+      <span class="{{ type }}">
+      {% if name == sub_property.property_name %}&quot;{% endif -%}
+      {{ name }}
+      {%- if name == sub_property.property_name %}&quot;{% endif -%}
+      </span>:
+      {% if sub_property.type_name != "object" %}
+      {% if name == sub_property.type_name %}
+      <span class="schema_key">{{ name }}</span>
+      {% endif %}
+      <span class="schema_type">{{ sub_property.type_name }}</span>
+      {% else %}
+      {% if name == sub_property.type_name %}
+      <span class="schema_key">{{ name }}</span>:
+      {% endif %}
+      {% endif %}
+      <span class="schema_desc">{{ sub_property.description }}</span>
+    </li>
+    {% endif %}
+    {% with schema=sub_property %}
+      {% include "schema.jinja2.html" %}
+    {% endwith %}
+  {% endfor %}
+</ul>
+{% endif %}
+
+{% if schema.kw_any_of%}
+<span class="schema_comb">One of:</span>
+  {% for sub_property in schema.kw_any_of.array_items %}
+    {% if sub_property.property_name %}
+    <li>
+      <span class="schema_key">{{ sub_property.property_name }}</span>
+      <span class="schema_desc">{{ sub_property.description }}</span>
+    </li>
+    {% endif %}
+    {% with schema=sub_property %}
+      {% include "schema.jinja2.html" %}
+    {% endwith %}
+  {% endfor %}
+{% endif %}

scripts/build-docs.sh

@@ -12,7 +12,7 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )"
 cd $SCRIPT_DIR
 
 if [ $(uname -m) = "arm64" ]; then
-  if ! $(which xmdbook >/dev/null 2>&1); then
+  if ! $(which mdbook >/dev/null 2>&1); then
     >&2 echo "Pre-built mdbook binaries for Apple ARM are not available."
     >&2 echo 'Run `cargo install mdbook` and try again.'
     exit 1
@@ -62,7 +62,8 @@ fi
 echo "Building user documentation..."
 # Generate benchcomp documentation from source code
 mkdir -p gen_src
-"${SCRIPT_DIR}/gen_benchcomp_schemas.py" gen_src
+"${SCRIPT_DIR}/gen_visualization_schemas.py" gen_src
+"${SCRIPT_DIR}/gen_format_schemas.py" gen_src
 
 # Build the book into ./book/
 mkdir -p book

scripts/ci/copyright_check.py

@@ -10,8 +10,8 @@
 
 COMMENT_OR_EMPTY_PATTERN = '^(//.*$|#.*$|\\s*$)'
 
-STANDARD_HEADER_PATTERN_1 = '(//|#) Copyright Kani Contributors'
-STANDARD_HEADER_PATTERN_2 = '(//|#) SPDX-License-Identifier: Apache-2.0 OR MIT'
+STANDARD_HEADER_PATTERN_1 = '(//|#|/\\*) Copyright Kani Contributors'
+STANDARD_HEADER_PATTERN_2 = '(//|#| \\*) SPDX-License-Identifier: Apache-2.0 OR MIT'
 
 MODIFIED_HEADER_PATTERN_1 = '(//|#) SPDX-License-Identifier: Apache-2.0 OR MIT'
 MODIFIED_HEADER_PATTERN_2 = COMMENT_OR_EMPTY_PATTERN

scripts/gen_format_schemas.py

@@ -0,0 +1,64 @@
+#!/usr/bin/env python3
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Generate documentation for every public class in the `benchcomp.schemas`
+# module. This script generates one Markdown file for each class; these Markdown
+# files can then be included in the Kani book.
+#
+# The script first dumps the schema into JSON Draft-07 [1] format, and then used
+# the json_schema_for_humans package to render that into Markdown.
+#
+# [1] https://json-schema.org/draft-07/json-schema-release-notes.html
+
+
+import inspect
+import json
+import pathlib
+import sys
+import tempfile
+
+import json_schema_for_humans as jsfh
+import json_schema_for_humans.generation_configuration
+import json_schema_for_humans.generate
+import schema
+
+sys.path.append(str(pathlib.Path(__file__).parent.parent / "tools" / "benchcomp"))
+
+# autopep8: off
+import benchcomp.schemas
+# autopep8: on
+
+
+def main():
+    out_dir = pathlib.Path(sys.argv[1]).resolve()
+    out_dir.mkdir(exist_ok=True, parents=True)
+
+    template = (
+        pathlib.Path(__file__).parent.parent /
+        "docs/src/schema.jinja2.html").resolve()
+    config = jsfh.generation_configuration.GenerationConfiguration(
+        template_name="md", examples_as_yaml=True, with_footer=False,
+        copy_css=False, copy_js=False, custom_template_path=template)
+
+    with tempfile.TemporaryDirectory() as tmpdir:
+        tmpdir = pathlib.Path(tmpdir)
+        for name, klass in inspect.getmembers(benchcomp.schemas):
+            if not inspect.isclass(klass):
+                continue
+            if name.startswith("_"):
+                continue
+
+            s = schema.Schema(klass().get_raw_schema()["schema"])
+            schema_docs = s.json_schema(
+                f"https://github.com/model-checking/kani/benchcomp/{name}")
+
+            with open(tmpdir / f"{name}.json", "w") as handle:
+                print(json.dumps(schema_docs, indent=2), file=handle)
+
+            jsfh.generate.generate_from_filename(
+                tmpdir, out_dir / f"{name}.md", config=config)
+
+
+if __name__ == "__main__":
+    main()

scripts/setup/ubuntu/install_doc_deps.sh

@@ -6,3 +6,10 @@ set -eux
 
 cargo install mdbook-graphviz
 DEBIAN_FRONTEND=noninteractive sudo apt-get install --no-install-recommends --yes graphviz
+
+PYTHON_DEPS=(
+  json_schema_for_humans  # Render a Draft-07 JSON schema to HTML
+  schema                  # Validate data structures
+)
+
+python3 -m pip install "${PYTHON_DEPS[@]}"

tools/benchcomp/benchcomp/__init__.py

@@ -16,56 +16,34 @@
 import yaml
 
 
-class ConfigFile(collections.UserDict):
-    _schema: str = textwrap.dedent("""\
-variants:
-  type: dict
-  keysrules:
-    type: string
-  valuesrules:
-    schema:
-      config:
-        type: dict
-        keysrules:
-          type: string
-        valuesrules:
-          allow_unknown: true
-          schema:
-            command_line:
-              type: string
-            directory:
-              type: string
-            env:
-              type: dict
-              keysrules:
-                type: string
-              valuesrules:
-                type: string
-run:
-  type: dict
-  keysrules:
-    type: string
-  schema:
-    suites:
-      type: dict
-      keysrules:
-        type: string
-      valuesrules:
-        schema:
-          variants:
-            type: list
-          parser:
-            type: dict
-            keysrules:
-              type: string
-            valuesrules:
-              anyof:
-                - schema:
-                    type: {}
-filter: {}
-visualize: {}
-""")
+class _SchemaValidator:
+    """Validate data structures with a schema
+
+    Objects of this class are callable, with a single `data` argument. The data
+    is validated and returned if the `schema` package is installed, or returned
+    if not.
+    """
+
+
+    def __init__(self, schema_name):
+        """
+        schema_name: the name of a class in benchcomp.schemas
+        """
+
+        try:
+            import benchcomp.schemas
+            klass = getattr(benchcomp.schemas, schema_name)
+            self.validate = klass()().validate
+        except ImportError:
+            self.validate = (lambda data: data)
 
+
+    def __call__(self, data):
+        return self.validate(data)
+
+
+
+class ConfigFile(collections.UserDict):
     def __init__(self, path):
         super().__init__()
 
@@ -76,27 +54,11 @@ def __init__(self, path):
             raise argparse.ArgumentTypeError(
                 f"{path}: file not found") from exc
 
-        schema = yaml.safe_load(self._schema)
+        validate = _SchemaValidator("BenchcompYaml")
         try:
-            import cerberus
-            validate = cerberus.Validator(schema)
-            if not validate(data):
-                for error in validate._errors:
-                    doc_path = "/".join(error.document_path)
-                    msg = (
-                        f"config file '{path}': key "
-                        f"'{doc_path}': expected "
-                        f"{error.constraint}, got '{error.value}'")
-                    if error.rule:
-                        msg += f" (rule {error.rule})"
-                    msg += f" while traversing {error.schema_path}"
-                    logging.error(msg)
-                logging.error(validate.document_error_tree["variants"])
-                raise argparse.ArgumentTypeError(
-                    "failed to validate configuration file")
-        except ImportError:
-            pass
-        self.data = data
+            self.data = validate(data)
+        except BaseException as exc:
+            sys.exit(exc.code)
 
 
 @dataclasses.dataclass