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