From ac8bd762f29348c13ceec78ec5d31987cee1eac0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 23 Jun 2023 11:40:41 -0400 Subject: [PATCH 1/4] Minor edits for all RFCs (#2560) --- rfc/src/rfcs/0001-mir-linker.md | 2 +- rfc/src/rfcs/0002-function-stubbing.md | 6 ++++-- rfc/src/rfcs/0003-cover-statement.md | 7 ++++--- rfc/src/rfcs/0004-loop-contract-synthesis.md | 4 +++- rfc/src/rfcs/0005-should-panic-attr.md | 6 ++++-- rfc/src/rfcs/0006-unstable-api.md | 2 +- rfc/src/template.md | 2 ++ 7 files changed, 19 insertions(+), 10 deletions(-) diff --git a/rfc/src/rfcs/0001-mir-linker.md b/rfc/src/rfcs/0001-mir-linker.md index 1c12d8ee7b68..d951f6243809 100644 --- a/rfc/src/rfcs/0001-mir-linker.md +++ b/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**: - **RFC PR:** - **Status:** Stable diff --git a/rfc/src/rfcs/0002-function-stubbing.md b/rfc/src/rfcs/0002-function-stubbing.md index 2103ad3b632c..e92e3c06178b 100644 --- a/rfc/src/rfcs/0002-function-stubbing.md +++ b/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:** - **RFC PR:** -- **Status:** Under Review +- **Status:** Unstable - **Version:** 1 - **Proof-of-concept:** +------------------- + ## Summary Allow users to specify that certain functions and methods should be replaced with mock functions (stubs) during verification. diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index bbb7a8904e6e..320bc53aebe3 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/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:** - **RFC PR:** -- **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 diff --git a/rfc/src/rfcs/0004-loop-contract-synthesis.md b/rfc/src/rfcs/0004-loop-contract-synthesis.md index 2ac828f06eec..0286dd71b2d2 100644 --- a/rfc/src/rfcs/0004-loop-contract-synthesis.md +++ b/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:** - **RFC PR:** - **Status:** Under Review - **Version:** 0 - **Proof-of-concept:** +------------------- + ## Summary A new option that allows users to verify programs without unwinding loops by synthesizing loop contracts for those loops. diff --git a/rfc/src/rfcs/0005-should-panic-attr.md b/rfc/src/rfcs/0005-should-panic-attr.md index a5dcff085d2d..1f4aafb599e6 100644 --- a/rfc/src/rfcs/0005-should-panic-attr.md +++ b/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:** - **RFC PR:** -- **Status:** Under Review +- **Status:** Unstable - **Version:** 0 - **Proof-of-concept:** +------------------- + ## Summary Users may want to express that a verification harness should panic. diff --git a/rfc/src/rfcs/0006-unstable-api.md b/rfc/src/rfcs/0006-unstable-api.md index 2c055d4d9333..c964b050bfe1 100644 --- a/rfc/src/rfcs/0006-unstable-api.md +++ b/rfc/src/rfcs/0006-unstable-api.md @@ -1,7 +1,7 @@ - **Feature Name:** Unstable APIs (`unstable-api`) - **RFC Tracking Issue**: - **RFC PR:** -- **Status:** Under Review +- **Status:** Unstable - **Version:** 0 ------------------- diff --git a/rfc/src/template.md b/rfc/src/template.md index 1ace8208d46e..4f50f7b72f0c 100644 --- a/rfc/src/template.md +++ b/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? From a071df1ea22cd611d97860926c805c854b4e106c Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Fri, 23 Jun 2023 14:05:50 -0700 Subject: [PATCH 2/4] Bump CBMC version to 5.86.0 (#2561) --- kani-dependencies | 2 +- scripts/kani-regression.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-dependencies b/kani-dependencies index 9ffb59eff968..0c2264b0f9b2 100644 --- a/kani-dependencies +++ b/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" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 022f7e6b8518..6710937004b8 100755 --- a/scripts/kani-regression.sh +++ b/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 From 987c9cef5e21762941b8f288fda7b95623b37080 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Mon, 26 Jun 2023 18:23:30 +0100 Subject: [PATCH 3/4] Install doc dependencies before building (#2564) This fixes a Graphviz graph not being rendered in the Kani book. --- .github/workflows/kani.yml | 3 +++ scripts/setup/ubuntu/install_doc_deps.sh | 8 ++++++++ 2 files changed, 11 insertions(+) create mode 100755 scripts/setup/ubuntu/install_doc_deps.sh diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index eac9372905cc..81403735e1cd 100644 --- a/.github/workflows/kani.yml +++ b/.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 diff --git a/scripts/setup/ubuntu/install_doc_deps.sh b/scripts/setup/ubuntu/install_doc_deps.sh new file mode 100755 index 000000000000..e3f4dd2c0d74 --- /dev/null +++ b/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 From d4a624f77d629e2ce8402e884b766337d6e7c258 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Mon, 26 Jun 2023 19:33:09 +0100 Subject: [PATCH 4/4] Add run_command benchcomp visualization (#2542) This allows users to write their own custom visualization script to run after running the benchmarks. Prior to this commit, visualizations had to be checked into the Kani repository. When run_command is specified as a visualization, benchcomp runs the specified command and passes the result of the run as a JSON file on stdin. The command can then process the result however it likes. This resolves #2518. --- docs/src/SUMMARY.md | 1 - docs/src/benchcomp-conf.md | 2 +- .../benchcomp/visualizers/__init__.py | 42 +++++++- tools/benchcomp/test/test_regression.py | 97 +++++++++++++++++++ 4 files changed, 138 insertions(+), 4 deletions(-) diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 8ff6608445a9..d4609a87c23b 100644 --- a/docs/src/SUMMARY.md +++ b/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) diff --git a/docs/src/benchcomp-conf.md b/docs/src/benchcomp-conf.md index 489ae34a5550..77236d0917bf 100644 --- a/docs/src/benchcomp-conf.md +++ b/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 diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py index da9effcba426..af973379f19d 100644 --- a/tools/benchcomp/benchcomp/visualizers/__init__.py +++ b/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: diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py index a5b02a5b09b1..c5cb61ae8190 100644 --- a/tools/benchcomp/test/test_regression.py +++ b/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)