.

GaloisInc · Sep 25, 2024 · bae4004 · bae4004
1 parent 84c1e0f
commit bae4004
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 10 deletions.
diff --git a/.github/workflows/ci-bench.yml b/.github/workflows/ci-bench.yml
@@ -94,11 +94,11 @@ 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
@@ -108,8 +108,8 @@ jobs:
         tool: 'customSmallerIsBetter'
         output-file-path: |
           {
-            "z3": "tests/benchmark-data.json",
-            "cvc5": "tests/benchmark-data.json"
+            "z3": "tests/benchmark-data-z3.json",
+            "cvc5": "tests/benchmark-data-cvc5.json"
           }
         # Access token to deploy GitHub Pages branch
         github-token: ${{ secrets.GITHUB_TOKEN }}

diff --git 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,22 +27,22 @@ 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",
 	"value": ${TIME}
     }
 EOF
   else
-    cat << EOF >> ${TMP_FILE}
+    cat << EOF >> "${TMP_FILE}"
     {
 	"name": "${TEST}",
         "unit": "Seconds",
@@ -48,15 +54,15 @@ EOF
   let INDEX=${INDEX}+1
 done
 
-cat << EOF >> ${JSON_FILE}
+cat << EOF >> "${JSON_FILE}"
     {
         "name": "Total benchmark time",
         "unit": "Seconds",
         "value": ${TOTAL}
     },
 EOF
 
-cat ${TMP_FILE} >> ${JSON_FILE}
+cat "${TMP_FILE}" >> "${JSON_FILE}"
 
 echo "]" >> "${JSON_FILE}"