From 588baf06b3645faff1da9462c6269bc13076d16a Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@amazon.com>
Date: Wed, 19 Apr 2023 21:03:43 +0100
Subject: [PATCH] Run benchcomp unit and regression tests in CI (#2382)

This will ensure that benchcomp will continue to correctly parse future changes to Kani's output.
---
 .github/workflows/kani.yml       | 23 +++++++++++++++++++++++
 scripts/ci/copyright-exclude     |  3 ++-
 tools/benchcomp/requirements.txt |  2 ++
 3 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 tools/benchcomp/requirements.txt

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 570280637057..833a31fbd271 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -52,6 +52,29 @@ jobs:
           KANI_ENABLE_WRITE_JSON_SYMTAB: 1
         run: ./scripts/kani-regression.sh
 
+  benchcomp-tests:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Install benchcomp dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y python3-pip
+          pushd tools/benchcomp && pip3 install -r requirements.txt
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-20.04
+
+      - name: Build Kani using release mode
+        run: cargo build-dev -- --release
+
+      - name: Run benchcomp unit and regression tests
+        run: pushd tools/benchcomp && PATH=$(realpath ../../scripts):$PATH test/run
+
   perf:
     runs-on: ubuntu-20.04
     steps:
diff --git a/scripts/ci/copyright-exclude b/scripts/ci/copyright-exclude
index 5cc538031006..358edc372af2 100644
--- a/scripts/ci/copyright-exclude
+++ b/scripts/ci/copyright-exclude
@@ -5,8 +5,8 @@
 .png
 .props
 .public.key
-Cargo.lock
 CHANGELOG
+Cargo.lock
 LICENSE-APACHE
 LICENSE-MIT
 editorconfig
@@ -16,6 +16,7 @@ gitignore
 gitmodules
 ignore
 kani-dependencies
+requirements.txt
 scripts/ci/copyright-exclude
 tests/remote-target-lists/.*
 tools/build-kani/license-notes.txt
diff --git a/tools/benchcomp/requirements.txt b/tools/benchcomp/requirements.txt
new file mode 100644
index 000000000000..7f2c80e4e24f
--- /dev/null
+++ b/tools/benchcomp/requirements.txt
@@ -0,0 +1,2 @@
+cerberus
+pyyaml