Merge branch 'main' into new-assigns-check

model-checking · Feb 1, 2024 · 8db7d20 · 8db7d20
2 parents 40e3abe + e09993b
commit 8db7d20
Show file tree

Hide file tree

Showing 9 changed files with 107 additions and 27 deletions.
diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml
@@ -19,7 +19,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-12, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani under "kani"
         uses: actions/checkout@v4

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-12, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -20,7 +20,7 @@ env:
 jobs:
   build_bundle_macos:
     name: BuildBundle-MacOs
-    runs-on: macos-12
+    runs-on: macos-13
     permissions:
       contents: write
     outputs:
@@ -35,13 +35,13 @@ jobs:
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
         with:
-          os: macos-12
+          os: macos-13
 
       - name: Build bundle
         id: bundle
         uses: ./.github/actions/build-bundle
         with:
-          os: macos-12
+          os: macos-13
           arch: x86_64-apple-darwin
 
   build_bundle_linux:
@@ -106,11 +106,11 @@ jobs:
     needs: [build_bundle_macos, build_bundle_linux]
     strategy:
       matrix:
-        os: [macos-12, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
         include:
           # Stores the output of the previous job conditional to the OS
           - prev_job: ${{ needs.build_bundle_linux.outputs }}
-          - os: macos-12
+          - os: macos-13
             prev_job: ${{ needs.build_bundle_macos.outputs }}
     runs-on: ${{ matrix.os }}
     steps:

diff --git a/.github/workflows/slow-tests.yml b/.github/workflows/slow-tests.yml
@@ -18,7 +18,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-12, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4

diff --git a/Cargo.lock b/Cargo.lock
@@ -407,9 +407,9 @@ dependencies = [
 
 [[package]]
 name = "indexmap"
-version = "2.1.0"
+version = "2.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d530e1a18b1cb4c484e6e34556a0d948706958449fca0cab753d649f2bce3d1f"
+checksum = "433de089bd45971eecf4668ee0ee8f4cec17db4f8bd8f7bc3197a6ce37aa7d9b"
 dependencies = [
  "equivalent",
  "hashbrown 0.14.3",
@@ -765,11 +765,11 @@ dependencies = [
 
 [[package]]
 name = "pulldown-cmark"
-version = "0.9.3"
+version = "0.9.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "77a1a2f1f0a7ecff9c31abbe177637be0e97a0aef46cf8738ece09327985d998"
+checksum = "57206b407293d2bcd3af849ce869d52068623f19e1b5ff8e8778e3309439682b"
 dependencies = [
- "bitflags 1.3.2",
+ "bitflags 2.4.2",
  "memchr",
  "unicase",
 ]
@@ -850,7 +850,7 @@ checksum = "b62dbe01f0b06f9d8dc7d49e05a0785f153b00b2c227856282f671e0318c9b15"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-automata 0.4.4",
+ "regex-automata 0.4.5",
  "regex-syntax 0.8.2",
 ]
 
@@ -865,9 +865,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.4.4"
+version = "0.4.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3b7fa1134405e2ec9353fd416b17f8dacd46c473d7d3fd1cf202706a14eb792a"
+checksum = "5bb987efffd3c6d0d8f5f89510bb458559eab11e4f869acb20bf845e016259cd"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -950,18 +950,18 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.195"
+version = "1.0.196"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "63261df402c67811e9ac6def069e4786148c4563f4b50fd4bf30aa370d626b02"
+checksum = "870026e60fa08c69f064aa766c10f10b1d62db9ccd4d0abb206472bee0ce3b32"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.195"
+version = "1.0.196"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "46fe8f8603d81ba86327b23a2e9cdf49e1255fb94a4c5f297f6ee0547178ea2c"
+checksum = "33c85360c95e7d137454dc81d9a4ed2b8efd8fbe19cee57357b32b9771fccb67"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -970,9 +970,9 @@ dependencies = [
 
 [[package]]
 name = "serde_json"
-version = "1.0.111"
+version = "1.0.112"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "176e46fa42316f18edd598015a5166857fc835ec732f5215eac6b7bdbf0a84f4"
+checksum = "4d1bd37ce2324cf3bf85e5a25f96eb4baf0d5aa6eba43e7ae8958870c4ec48ed"
 dependencies = [
  "itoa",
  "ryu",
@@ -999,9 +999,9 @@ dependencies = [
 
 [[package]]
 name = "serde_yaml"
-version = "0.9.30"
+version = "0.9.31"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b1bf28c79a99f70ee1f1d83d10c875d2e70618417fda01ad1785e027579d9d38"
+checksum = "adf8a49373e98a4c5f0ceb5d05aa7c648d75f63774981ed95b7c7443bbd50c6e"
 dependencies = [
  "indexmap",
  "itoa",
@@ -1495,9 +1495,9 @@ checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04"
 
 [[package]]
 name = "winnow"
-version = "0.5.34"
+version = "0.5.35"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b7cf47b659b318dccbd69cc4797a39ae128f533dce7902a1096044d1967b9c16"
+checksum = "1931d78a9c73861da0134f453bb1f790ce49b2e30eba8410b4b79bac72b46a2d"
 dependencies = [
  "memchr",
 ]
diff --git a/scripts/setup/macos-13 b/scripts/setup/macos-13
@@ -0,0 +1 @@
+macos
diff --git a/scripts/setup/macos/install_viewer.sh b/scripts/setup/macos/install_viewer.sh
@@ -18,5 +18,8 @@ set -x
 
 # brew doesn't recognize specific versions of viewer
 # Build from source, since there's only a macos-12 bottle which doesn't seem to work.
+# Install Python 3.12 first while ignoring errors: the system may provide this
+# version, which will hinder brew from installing symlinks
+brew install python@3.12 || true
 brew install -s aws/tap/cbmc-viewer
 echo "Installed: $(cbmc-viewer --version)"
diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py
@@ -6,6 +6,7 @@
 import json
 import logging
 import subprocess
+import sys
 import textwrap
 
 import jinja2
@@ -232,12 +233,19 @@ def _organize_results_into_metrics(results):
         for bench, bench_result in results["benchmarks"].items():
             for variant, variant_result in bench_result["variants"].items():
                 for metric, value in variant_result["metrics"].items():
+                    if metric not in ret:
+                        ret[metric] = {}
+                        logging.warning(
+                            "Benchmark '%s' contained a metric '%s' in the "
+                            "'%s' variant result that was not declared in "
+                            "the 'metrics' dict. Add '%s: {}' to the metrics "
+                            "dict", bench, metric, variant, metric)
                     try:
                         ret[metric][bench][variant] = variant_result["metrics"][metric]
                     except KeyError:
                         ret[metric][bench] = {
                             variant: variant_result["metrics"][metric]
-                    }
+                        }
         return ret
 
 

diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py
@@ -6,6 +6,7 @@
 # tests.
 
 import pathlib
+import re
 import subprocess
 import tempfile
 import textwrap
@@ -834,3 +835,70 @@ def test_run_failing_command_visualization(self):
             run_bc()
             self.assertNotEqual(
                 run_bc.proc.returncode, 0, msg=run_bc.stderr)
+
+
+    def test_unknown_metric_in_benchmark(self):
+        """Ensure that benchcomp continues with warning if a benchmark result contained an unknown metric"""
+
+        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 '{
+                                      metrics: {
+                                        foo: {},
+                                        bar: {},
+                                      },
+                                      benchmarks: {
+                                        bench_1: {
+                                          metrics: {
+                                            baz: 11
+                                          }
+                                        }
+                                      }
+                                    }'
+                                """
+                            },
+                            "variants": ["v2", "v1"]
+                        }
+                    }
+                },
+                "visualize": [{
+                    "type": "dump_markdown_results_table",
+                    "out_file": "-",
+                    "extra_columns": {},
+                }],
+            })
+
+            output_pat = re.compile(
+                "Benchmark 'bench_1' contained a metric 'baz' in the 'v1' "
+                "variant result that was not declared in the 'metrics' dict.")
+
+            run_bc()
+            self.assertRegex(run_bc.stderr, output_pat)
+
+            self.assertEqual(run_bc.proc.returncode, 0, msg=run_bc.stderr)
+
+            with open(run_bc.working_directory / "result.yaml") as handle:
+                result = yaml.safe_load(handle)
+
+            for item in ["benchmarks", "metrics"]:
+                self.assertIn(item, result)