diff --git a/docs/book.toml b/docs/book.toml
index b7cfc21b9b64..c8e7c39af559 100644
--- a/docs/book.toml
+++ b/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
diff --git a/docs/src/benchcomp-conf.md b/docs/src/benchcomp-conf.md
index 77236d0917bf..963cc1f55f21 100644
--- a/docs/src/benchcomp-conf.md
+++ b/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
diff --git a/docs/src/schema.css b/docs/src/schema.css
new file mode 100644
index 000000000000..dd8fc47d04bb
--- /dev/null
+++ b/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;
+}
diff --git a/docs/src/schema.jinja2.html b/docs/src/schema.jinja2.html
new file mode 100644
index 000000000000..25a42d55f72d
--- /dev/null
+++ b/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" %}
+
+ {% for sub_property in schema.iterate_properties %}
+ - - {{ sub_property.property_name }}
+ {% endfor %}
+
+{% endif %}
+
+{% if schema.type_name == "object" %}
+
+ {% for sub_property in schema.iterate_properties %}
+ {% if sub_property.property_name %}
+ -
+ {% 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 %}
+
+ {% if name == sub_property.property_name %}"{% endif -%}
+ {{ name }}
+ {%- if name == sub_property.property_name %}"{% endif -%}
+ :
+ {% if sub_property.type_name != "object" %}
+ {% if name == sub_property.type_name %}
+ {{ name }}
+ {% endif %}
+ {{ sub_property.type_name }}
+ {% else %}
+ {% if name == sub_property.type_name %}
+ {{ name }}:
+ {% endif %}
+ {% endif %}
+ {{ sub_property.description }}
+
+ {% endif %}
+ {% with schema=sub_property %}
+ {% include "schema.jinja2.html" %}
+ {% endwith %}
+ {% endfor %}
+
+{% endif %}
+
+{% if schema.kw_any_of%}
+One of:
+ {% for sub_property in schema.kw_any_of.array_items %}
+ {% if sub_property.property_name %}
+
+ {{ sub_property.property_name }}
+ {{ sub_property.description }}
+
+ {% endif %}
+ {% with schema=sub_property %}
+ {% include "schema.jinja2.html" %}
+ {% endwith %}
+ {% endfor %}
+{% endif %}
diff --git a/scripts/build-docs.sh b/scripts/build-docs.sh
index cddd0480954e..0f2a58cc8527 100755
--- a/scripts/build-docs.sh
+++ b/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
diff --git a/scripts/gen_format_schemas.py b/scripts/gen_format_schemas.py
new file mode 100755
index 000000000000..3cc3e3d5b433
--- /dev/null
+++ b/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()
diff --git a/scripts/setup/ubuntu/install_doc_deps.sh b/scripts/setup/ubuntu/install_doc_deps.sh
index e3f4dd2c0d74..bafad3089688 100755
--- a/scripts/setup/ubuntu/install_doc_deps.sh
+++ b/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[@]}"
diff --git a/tools/benchcomp/benchcomp/schemas.py b/tools/benchcomp/benchcomp/schemas.py
new file mode 100644
index 000000000000..6c786d0c3c38
--- /dev/null
+++ b/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
+ built-in visualizations
+ below """)): [
+ dict
+ ]},
+ "name": "benchcomp.yaml",
+ "description": textwrap.dedent("""\
+ A configuration file that controls how benchcomp runs and combines
+ the results of benchmark suites.""")
+ }
diff --git a/tools/benchcomp/requirements.txt b/tools/benchcomp/requirements.txt
index b9666dbbaae5..5740eef76b4e 100644
--- a/tools/benchcomp/requirements.txt
+++ b/tools/benchcomp/requirements.txt
@@ -1,2 +1,3 @@
schema
+json-schema-for-humans
pyyaml