From 0e5ded71389ac1d262f5ce911ce6b764c5b8e5be Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Thu, 19 Sep 2024 11:51:04 -0400
Subject: [PATCH] Benchmark z3 and cvc5

---
 .github/workflows/ci-bench.yml | 12 ++++++++----
 tests/run-ci-benchmarks.sh     | 18 ++++++++++++------
 2 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/ci-bench.yml b/.github/workflows/ci-bench.yml
index 88882ab7b..bb9effc39 100644
--- a/.github/workflows/ci-bench.yml
+++ b/.github/workflows/ci-bench.yml
@@ -94,19 +94,23 @@ jobs:
         opam pin --yes --no-action add cn .
         opam install --yes cn ocamlformat.0.26.2
 
-    - name: Run benchmark
+    - name: Run benchmarks
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh
+        cd tests; SOLVER='z3' ./run-ci-benchmarks.sh; SOLVER='cvc5' ./run-ci-benchmarks.sh
         cd ..
 
     - name: Store benchmark result
-      uses: benchmark-action/github-action-benchmark@v1
+      uses: GaloisInc/github-action-benchmark@00bf34008c7b91a09ea7f1ef93330ccb7bf2d4ab
       with:
         name: CN Benchmarks
         tool: 'customSmallerIsBetter'
-        output-file-path: tests/benchmark-data.json
+        output-file-path: |
+          {
+            "z3": "tests/benchmark-data-z3.json",
+            "cvc5": "tests/benchmark-data-cvc5.json"
+          }
         # Access token to deploy GitHub Pages branch
         github-token: ${{ secrets.GITHUB_TOKEN }}
         # Push and deploy GitHub pages branch automatically
diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
index 6bb1bb6f8..564c9b0d2 100755
--- a/tests/run-ci-benchmarks.sh
+++ b/tests/run-ci-benchmarks.sh
@@ -2,7 +2,13 @@
 set -euo pipefail -o noclobber
 # set -xv # uncomment to debug variables
 
-JSON_FILE="benchmark-data.json"
+if [[ -z "${SOLVER+x}" ]]; then
+  JSON_FILE="benchmark-data.json"
+  SOLVER_TYPE="--solver-type=z3"
+else
+  JSON_FILE="benchmark-data-${SOLVER}.json"
+  SOLVER_TYPE="--solver-type=${SOLVER}"
+fi
 TMP_FILE=$(mktemp)
 
 echo "[" >> "${JSON_FILE}"
@@ -21,14 +27,14 @@ TOTAL=0
 for TEST in ${TESTS}; do
 
   # Record wall clock time in seconds
-  /usr/bin/time --quiet -f "%e" -o /tmp/time cn verify "${TEST}" || true
+  /usr/bin/time --quiet -f "%e" -o /tmp/time cn verify "${SOLVER_TYPE}" "${TEST}" || true
   TIME=$(cat /tmp/time)
   TOTAL="$(echo "${TOTAL} + ${TIME}" | bc -l)"
 
   # If we're last, don't print a trailing comma.
   if [[ ${INDEX} -eq ${COUNT}-1 ]]; then
     # Hack to output JSON.
-    cat << EOF >> ${TMP_FILE}
+    cat << EOF >> "${TMP_FILE}"
     {
 	"name": "${TEST}",
         "unit": "Seconds",
@@ -36,7 +42,7 @@ for TEST in ${TESTS}; do
     }
 EOF
   else
-    cat << EOF >> ${TMP_FILE}
+    cat << EOF >> "${TMP_FILE}"
     {
 	"name": "${TEST}",
         "unit": "Seconds",
@@ -48,7 +54,7 @@ EOF
   let INDEX=${INDEX}+1
 done
 
-cat << EOF >> ${JSON_FILE}
+cat << EOF >> "${JSON_FILE}"
     {
         "name": "Total benchmark time",
         "unit": "Seconds",
@@ -56,7 +62,7 @@ cat << EOF >> ${JSON_FILE}
     },
 EOF
 
-cat ${TMP_FILE} >> ${JSON_FILE}
+cat "${TMP_FILE}" >> "${JSON_FILE}"
 
 echo "]" >> "${JSON_FILE}"