Merge branch 'main' into update-other-rfcs

.github/workflows/kani.yml

@@ -127,6 +127,9 @@ jobs:
       - name: Detect unexpected book runner failures
         run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt
 
+      - name: Install book dependencies
+        run: ./scripts/setup/ubuntu/install_doc_deps.sh
+
       # On one OS only, build the documentation, too.
       - name: Build Documentation
         run: ./scripts/build-docs.sh

docs/src/SUMMARY.md

@@ -35,7 +35,6 @@
   - [Performance comparisons](./performance-comparisons.md)
     - [`benchcomp` command line](./benchcomp-cli.md)
     - [`benchcomp` configuration file](./benchcomp-conf.md)
-    - [Custom visualizations](./benchcomp-viz.md)
     - [Custom parsers](./benchcomp-parse.md)
 
 - [Limitations](./limitations.md)

docs/src/benchcomp-conf.md

@@ -1,7 +1,7 @@
 # `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 describes the file's schema and lists the different parsers and visualizations that are available.
+This page lists the different visualizations that are available.
 
 
 ## Built-in visualizations

kani-dependencies

@@ -1,4 +1,4 @@
-CBMC_VERSION="5.85.0"
+CBMC_VERSION="5.86.0"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.8"
 KISSAT_VERSION="3.0.0"

rfc/src/rfcs/0001-mir-linker.md

@@ -1,4 +1,4 @@
-- **Feature Name:** MIR Linker (mir_linker)
+- **Feature Name:** MIR Linker (`mir_linker`)
 - **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/1588>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1600>
 - **Status:** Stable

rfc/src/rfcs/0002-function-stubbing.md

@@ -1,10 +1,12 @@
-- **Feature Name:** Function and method stubbing (`function_stubbing`)
+- **Feature Name:** Function and method stubbing (`function-stubbing`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/1695>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1723> 
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 1
 - **Proof-of-concept:** <https://github.com/aaronbembenek-aws/kani/tree/mir_transform>
 
+-------------------
+
 ## Summary
 
 Allow users to specify that certain functions and methods should be replaced with mock functions (stubs) during verification.

rfc/src/rfcs/0003-cover-statement.md

@@ -1,9 +1,10 @@
-- **Feature Name:** Cover statement `cover_statement`
+- **Feature Name:** Cover statement (`cover-statement`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/696>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1906>
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 0
-- **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here*
+
+-------------------
 
 ## Summary
 

rfc/src/rfcs/0004-loop-contract-synthesis.md

@@ -1,10 +1,12 @@
-- **Feature Name:** Loop-contract synthesis
+- **Feature Name:** Loop-contract synthesis (`loop-contract-synthesis`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/2214>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2215>
 - **Status:** Under Review
 - **Version:** 0
 - **Proof-of-concept:** <https://github.com/qinheping/kani/tree/kani-synthesizer>
 
+-------------------
+
 ## Summary
 
 A new option that allows users to verify programs without unwinding loops by synthesizing loop contracts for those loops.

rfc/src/rfcs/0005-should-panic-attr.md

@@ -1,10 +1,12 @@
-- **Feature Name:** The `kani::should_panic` attribute (`should-panic-attr`)*
+- **Feature Name:** The `kani::should_panic` attribute (`should-panic-attr`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/600>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2272>
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 0
 - **Proof-of-concept:** <https://github.com/model-checking/kani/pull/2315>
 
+-------------------
+
 ## Summary
 
 Users may want to express that a verification harness should panic.

rfc/src/rfcs/0006-unstable-api.md

@@ -1,7 +1,7 @@
 - **Feature Name:** Unstable APIs (`unstable-api`)
 - **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/2279>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2281>
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 0
 
 -------------------

rfc/src/template.md

@@ -6,6 +6,8 @@
   Start with 0.*
 - **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here*
 
+-------------------
+
 ## Summary
 
 Short description of the feature, i.e.: the elevator pitch. What is this feature about?

scripts/kani-regression.sh

@@ -19,7 +19,7 @@ KANI_DIR=$SCRIPT_DIR/..
 export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
 
 # Required dependencies
-check-cbmc-version.py --major 5 --minor 85
+check-cbmc-version.py --major 5 --minor 86
 check-cbmc-viewer-version.py --major 3 --minor 8
 check_kissat_version.sh
 

scripts/setup/ubuntu/install_doc_deps.sh

@@ -0,0 +1,8 @@
+#!/bin/bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eux
+
+cargo install mdbook-graphviz
+DEBIAN_FRONTEND=noninteractive sudo apt-get install --no-install-recommends --yes graphviz

tools/benchcomp/benchcomp/visualizers/__init__.py

@@ -3,6 +3,8 @@
 
 
 import dataclasses
+import json
+import subprocess
 import textwrap
 
 import jinja2
@@ -12,8 +14,44 @@
 import benchcomp.visualizers.utils as viz_utils
 
 
-# TODO The doc comment should appear in the help output, which should list all
-# available checks.
+
+@dataclasses.dataclass
+class run_command:
+    """Run an executable command, passing the performance metrics as JSON on stdin.
+
+    This allows you to write your own visualization, which reads a result file
+    on stdin and does something with it, e.g. writing out a graph or other
+    output file.
+
+    Sample configuration:
+
+    ```
+    visualize:
+    - type: run_command
+      command: ./my_visualization.py
+    ```
+    """
+
+    command: str
+
+
+    def __call__(self, results):
+        results = json.dumps(results, indent=2)
+        try:
+            proc = subprocess.Popen(
+                self.command, shell=True, text=True, stdin=subprocess.PIPE)
+            _, _ = proc.communicate(input=results)
+        except (OSError, subprocess.SubprocessError) as exe:
+            logging.error(
+                "visualization command '%s' failed: %s", self.command, str(exe))
+            viz_utils.EXIT_CODE = 1
+        if proc.returncode:
+            logging.error(
+                "visualization command '%s' exited with code %d",
+                self.command, proc.returncode)
+            viz_utils.EXIT_CODE = 1
+
+
 
 @dataclasses.dataclass
 class error_on_regression:

tools/benchcomp/test/test_regression.py

@@ -10,6 +10,7 @@
 import tempfile
 import textwrap
 import unittest
+import uuid
 
 import yaml
 
@@ -737,3 +738,99 @@ def test_command_parser(self):
 
             for item in ["benchmarks", "metrics"]:
                 self.assertIn(item, result)
+
+
+    def test_run_command_visualization(self):
+        """Ensure that the run_command visualization can execute a command"""
+
+        with tempfile.TemporaryDirectory() as tmp:
+            out_file = pathlib.Path(tmp) / str(uuid.uuid4())
+            run_bc = Benchcomp({
+                "variants": {
+                    "v1": {
+                        "config": {
+                            "command_line": "true",
+                            "directory": tmp,
+                        }
+                    },
+                    "v2": {
+                        "config": {
+                            "command_line": "true",
+                            "directory": tmp,
+                        }
+                    }
+                },
+                "run": {
+                    "suites": {
+                        "suite_1": {
+                            "parser": {
+                                "command": """
+                                    echo '{
+                                        "benchmarks": {},
+                                        "metrics": {}
+                                    }'
+                                """
+                            },
+                            "variants": ["v2", "v1"]
+                        }
+                    }
+                },
+                "visualize": [{
+                    "type": "run_command",
+                    "command": f"cat - > {out_file}"
+                }],
+            })
+            run_bc()
+            self.assertEqual(
+                run_bc.proc.returncode, 0, msg=run_bc.stderr)
+
+            with open(out_file) as handle:
+                result = yaml.safe_load(handle)
+
+            for item in ["benchmarks", "metrics"]:
+                self.assertIn(item, result)
+
+
+    def test_run_failing_command_visualization(self):
+        """Ensure that benchcomp terminates with a non-zero return code when run_command visualization fails"""
+
+        with tempfile.TemporaryDirectory() as tmp:
+            out_file = pathlib.Path(tmp) / str(uuid.uuid4())
+            run_bc = Benchcomp({
+                "variants": {
+                    "v1": {
+                        "config": {
+                            "command_line": "true",
+                            "directory": tmp,
+                        }
+                    },
+                    "v2": {
+                        "config": {
+                            "command_line": "true",
+                            "directory": tmp,
+                        }
+                    }
+                },
+                "run": {
+                    "suites": {
+                        "suite_1": {
+                            "parser": {
+                                "command": """
+                                    echo '{
+                                        "benchmarks": {},
+                                        "metrics": {}
+                                    }'
+                                """
+                            },
+                            "variants": ["v2", "v1"]
+                        }
+                    }
+                },
+                "visualize": [{
+                    "type": "run_command",
+                    "command": f"cat - > {out_file}; false"
+                }],
+            })
+            run_bc()
+            self.assertNotEqual(
+                run_bc.proc.returncode, 0, msg=run_bc.stderr)