Generate benchcomp documentation from schemas

This commit adds the schema of benchcomp.yaml to the Kani book to
document how benchcomp configuration files are written. The code will be
used in future commits for documenting the parser and visualizer
formats.

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,58 @@
 # `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
+    suite_2:
+      parser:
+        module: kani_perf
+      variants:
+        - suite_2_env
+        - suite_2_noenv
+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: {}
+  suite_2_env:
+    config:
+      command: make benchmarks
+      directory: suites/suite_2
+      env:
+        RUN_FAST: "true"
+  suite_2_noenv:
+    config:
+      command: make benchmarks
+      directory: suites/suite_2
+      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: #d00 !important;
+}
+.schema_type {
+  color: #0a0 !important;
+  text-decoration: underline !important;
+}
+.schema_desc {
+  opacity: 35% !important;
+  margin-left: 1em !important;
+  font-style: italic !important;
+}
+.schema_comb {
+  color: #06d !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

@@ -63,6 +63,7 @@ echo "Building user documentation..."
 # Generate benchcomp documentation from source code
 mkdir -p 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
@@ -74,6 +75,7 @@ echo "Building RFC book..."
 cd $RFC_DIR
 ${MDBOOK} build -d $KANI_DIR/docs/book/rfc
 
+
 # Testing of the code in the documentation is done via the usual
 # ./scripts/kani-regression.sh script. A note on running just the
 # doc tests is in README.md. We don't run them here because

scripts/gen_format_schemas.py

@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+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)
+            with open(f"/tmp/{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/schemas.py

@@ -0,0 +1,102 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Schemas for different file formats. Contained in a separate file so that
+# validation is optional.
+
+
+import textwrap
+
+import schema
+
+
+
+class _Schema:
+
+    # This is to work around a problem with `schema` where it does not dump a
+    # sub-schema to JSON when it is a schema.Literal with a type (e.g.
+    # schema.Literal(str, ...). All subclasses of _Schema should use `_str` in
+    # place of `str`; this method will transform it to the correct type for
+    # validation. The documentation generator (which uses the JSON dumper)
+    # avoids doing this and renders the raw schema directly.
+
+    def _replace_types(self, schema_dict):
+        if not isinstance(schema_dict, (dict, schema.Literal)):
+            return schema_dict
+
+        if not isinstance(schema_dict, (dict, )):
+            if schema_dict.schema == "_str":
+                return schema.Literal(str, schema_dict.description)
+            return schema_dict
+
+        tmp = {}
+        for k, v in schema_dict.items():
+            if k == "_str":
+                tmp[str] = self._replace_types(v)
+            elif isinstance(k, (schema.Literal)):
+                if k.schema == "_str":
+                    new_lit = schema.Literal(str, k.description)
+                    tmp[new_lit] = self._replace_types(v)
+                else:
+                    tmp[k] = self._replace_types(v)
+            else:
+                tmp[k] = self._replace_types(v)
+        return tmp
+
+
+    def __call__(self):
+        s = self.get_raw_schema()
+        name, description = s["name"], s["description"]
+        ret = self._replace_types(s["schema"])
+        return schema.Schema(ret, name=name, description=description)
+
+
+
+class BenchcompYaml(_Schema):
+    def get_raw_schema(self):
+      return {
+        "schema": {
+          "run": {
+            schema.Literal("suites", description=(
+              "a collection of benchmarks in a directory")): {
+              schema.Literal("_str", description="ID for the suite"): {
+                schema.Literal("variants", description=(
+                  "list of variant IDs to run for this suite")): [ str ],
+              schema.Literal("parser", description=textwrap.dedent(
+                "program used to read the results of a suite after the run.")):
+                schema.Or({
+                    schema.Literal("command", description=(
+                      "path to an executable parser")): str
+                }, {
+                    schema.Literal("module", description=(
+                      "name of a parser module in benchcomp.parsers")): str
+                })
+              },
+            },
+          },
+          schema.Literal("variants", description=(
+          "configurations under which benchcomp will run the suites")): {
+            schema.Literal("_str", description="ID for the variant"): {
+              "config": {
+                schema.Literal("command_line", description=(
+                  "command for running a suite using this variant")): str,
+                schema.Literal("directory", description=(
+                  "path where this variant runs")): str,
+                schema.Optional(schema.Literal("env", description=(
+                  "overrides for environment variables"))): {
+                  schema.Literal("_str"): schema.Literal("_str"),
+                },
+              },
+            },
+          },
+          schema.Literal("visualize", description=textwrap.dedent("""\
+            visualizations to apply to the result, see
+            <a href="#built-in-visualizations">built-in visualizations</a>
+            below """)): [
+            dict
+        ]},
+        "name": "benchcomp.yaml",
+        "description": textwrap.dedent("""\
+          A configuration file that controls how benchcomp runs and combines
+          the results of benchmark suites.""")
+      }

tools/benchcomp/requirements.txt

@@ -1,2 +1,3 @@
 schema
+json-schema-for-humans
 pyyaml