From 3ea8e72686ed8a5f33bfa48547454d9cbde2fda3 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Thu, 22 Aug 2024 13:07:13 -0400
Subject: [PATCH] Add benchmarking CI that generates graphs on updates to
 master

---
 .github/workflows/ci-bench.yml | 113 +++++++++++++++++++++++++++++++++
 tests/run-ci-benchmarks.sh     |  55 ++++++++++++++++
 2 files changed, 168 insertions(+)
 create mode 100644 .github/workflows/ci-bench.yml
 create mode 100755 tests/run-ci-benchmarks.sh

diff --git a/.github/workflows/ci-bench.yml b/.github/workflows/ci-bench.yml
new file mode 100644
index 000000000..711ac2d81
--- /dev/null
+++ b/.github/workflows/ci-bench.yml
@@ -0,0 +1,113 @@
+name: CI Benchmarks
+
+on:
+  push:
+    branches:
+      - master
+
+env:
+  CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release
+
+permissions:
+  # deployments permission to deploy GitHub pages website
+  deployments: write
+  # contents permission to update benchmark contents in gh-pages branch
+  contents: write
+
+# cancel in-progress job when a new push is performed
+concurrency:
+  group: ci-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  benchmark:
+    name: Performance benchmarks
+    strategy:
+      matrix:
+        # version: [4.12.0, 4.14.1]
+        version: [4.14.1]
+
+
+    runs-on: ubuntu-22.04
+
+    steps:
+    - uses: actions/checkout@v3
+
+    - name: System dependencies (ubuntu)
+      run: |
+        sudo apt install build-essential libgmp-dev z3 opam cmake
+
+    - name: Restore cached opam
+      id: cache-opam-restore
+      uses: actions/cache/restore@v4
+      with:
+        path: ~/.opam
+        key: ${{ matrix.version }}
+
+    - name: Setup opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      run: |
+        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
+        opam install --deps-only --yes ./cerberus-lib.opam
+        opam switch create with_coq ${{ matrix.version }}
+        eval $(opam env --switch=with_coq)
+        opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
+        opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
+        opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+        opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
+        opam pin --yes -n coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git
+        opam install --deps-only --yes ./cerberus-lib.opam ./cerberus-cheri.opam
+
+    - name: Save cached opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      id: cache-opam-save
+      uses: actions/cache/save@v4
+      with:
+        path: ~/.opam
+        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
+
+    - name: Install Cerberus
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam pin --yes --no-action add cerberus-lib .
+        opam pin --yes --no-action add cerberus .
+        opam install --yes cerberus
+
+    - name: Download cvc5 release
+      uses: robinraju/release-downloader@v1
+      with:
+        repository: cvc5/cvc5
+        tag: cvc5-1.1.2
+        fileName: cvc5-Linux-static.zip
+
+    - name: Unzip and install cvc5
+      run: |
+        unzip cvc5-Linux-static.zip
+        chmod +x cvc5-Linux-static/bin/cvc5
+        sudo cp cvc5-Linux-static/bin/cvc5 /usr/local/bin/
+
+    - name: Install CN
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam pin --yes --no-action add cn .
+        opam install --yes cn ocamlformat.0.26.2
+
+    - name: Run benchmark
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh
+        cd ..
+
+    - name: Store benchmark result
+      uses: benchmark-action/github-action-benchmark@v1
+      with:
+        name: CN Benchmarks
+        tool: 'customSmallerIsBetter'
+        output-file-path: tests/benchmark-data.json
+        # Access token to deploy GitHub Pages branch
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+        # Push and deploy GitHub pages branch automatically
+        auto-push: true
diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
new file mode 100755
index 000000000..2da701ade
--- /dev/null
+++ b/tests/run-ci-benchmarks.sh
@@ -0,0 +1,55 @@
+#!/bin/bash
+
+JSON_FILE="benchmark-data.json"
+
+cat << EOF >> ${JSON_FILE}
+[
+EOF
+
+DIRNAME=$(dirname "$0")
+
+SUCC=$(find "${DIRNAME}"/cn -name '*.c' | grep -v '\.error\.c')
+
+COUNT=0
+for TEST in ${SUCC}; do
+  let COUNT=${COUNT}+1
+done
+
+INDEX=0
+echo $SUCC
+echo $COUNT
+for TEST in ${SUCC}; do
+  echo ${INDEX}
+
+  # Record wall clock time in seconds
+  /usr/bin/time -f "%e" -o /tmp/time cn verify ${TEST}
+  TIME=$(cat /tmp/time)
+
+  # If we're last, don't print a trailing comma.
+  if [[ ${INDEX} -eq ${COUNT}-1 ]]; then
+    # Hack to output JSON.
+    cat << EOF >> ${JSON_FILE}
+    {
+	"name": "${TEST}",
+        "unit": "Seconds",
+	"value": ${TIME}
+    }
+EOF
+  else
+    cat << EOF >> ${JSON_FILE}
+    {
+	"name": "${TEST}",
+        "unit": "Seconds",
+	"value": ${TIME}
+    },
+EOF
+  fi
+
+  let INDEX=${INDEX}+1
+done
+
+cat << EOF >> ${JSON_FILE}
+]
+EOF
+
+cat ${JSON_FILE}