From e44552576b1619d8186dbc1835ace4ef3ab6d011 Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 27 Aug 2024 11:42:37 -0400
Subject: [PATCH 1/4] Address @dc-mak's comments

---
 .github/workflows/ci-bench.yml |  4 ++--
 tests/run-ci-benchmarks.sh     | 19 +++++++------------
 2 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/ci-bench.yml b/.github/workflows/ci-bench.yml
index 711ac2d81..88882ab7b 100644
--- a/.github/workflows/ci-bench.yml
+++ b/.github/workflows/ci-bench.yml
@@ -16,7 +16,7 @@ permissions:
 
 # cancel in-progress job when a new push is performed
 concurrency:
-  group: ci-${{ github.workflow }}-${{ github.ref }}
+  group: ci-bench-${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
@@ -35,7 +35,7 @@ jobs:
 
     - name: System dependencies (ubuntu)
       run: |
-        sudo apt install build-essential libgmp-dev z3 opam cmake
+        sudo apt install build-essential libgmp-dev z3 opam cmake jq
 
     - name: Restore cached opam
       id: cache-opam-restore
diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
index 2da701ade..0634f71be 100755
--- a/tests/run-ci-benchmarks.sh
+++ b/tests/run-ci-benchmarks.sh
@@ -1,10 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
+set -euo pipefail -o noclobber
+# set -xv # uncomment to debug variables
 
 JSON_FILE="benchmark-data.json"
 
-cat << EOF >> ${JSON_FILE}
-[
-EOF
+echo "[" >> "${JSON_FILE}"
 
 DIRNAME=$(dirname "$0")
 
@@ -16,13 +16,10 @@ for TEST in ${SUCC}; do
 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}
+  /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.
@@ -48,8 +45,6 @@ EOF
   let INDEX=${INDEX}+1
 done
 
-cat << EOF >> ${JSON_FILE}
-]
-EOF
+echo "]" >> "${JSON_FILE}"
 
-cat ${JSON_FILE}
+jq . "${JSON_FILE}"

From 7e87d3cabe855de42137b0c36deeaa8c5a7b96ba Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 27 Aug 2024 11:43:30 -0400
Subject: [PATCH 2/4] Run failing tests for benchmarks too

---
 tests/run-ci-benchmarks.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
index 0634f71be..32e824bad 100755
--- a/tests/run-ci-benchmarks.sh
+++ b/tests/run-ci-benchmarks.sh
@@ -8,15 +8,15 @@ echo "[" >> "${JSON_FILE}"
 
 DIRNAME=$(dirname "$0")
 
-SUCC=$(find "${DIRNAME}"/cn -name '*.c' | grep -v '\.error\.c')
+TESTS=$(find "${DIRNAME}"/cn -name '*.c')
 
 COUNT=0
-for TEST in ${SUCC}; do
+for TEST in ${TESTS}; do
   let COUNT=${COUNT}+1
 done
 
 INDEX=0
-for TEST in ${SUCC}; do
+for TEST in ${TESTS}; do
 
   # Record wall clock time in seconds
   /usr/bin/time -f "%e" -o /tmp/time cn verify "${TEST}"

From 6469868feaefb8b44331356fcc095c70465f280a Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 27 Aug 2024 12:03:22 -0400
Subject: [PATCH 3/4] Update benchmarking script for failing tests

---
 tests/run-ci-benchmarks.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
index 32e824bad..6230713c3 100755
--- a/tests/run-ci-benchmarks.sh
+++ b/tests/run-ci-benchmarks.sh
@@ -19,7 +19,7 @@ INDEX=0
 for TEST in ${TESTS}; do
 
   # Record wall clock time in seconds
-  /usr/bin/time -f "%e" -o /tmp/time cn verify "${TEST}"
+  /usr/bin/time -f "%e" -o /tmp/time cn verify "${TEST}" || true
   TIME=$(cat /tmp/time)
 
   # If we're last, don't print a trailing comma.

From 3a1c0bb68a696a457f1bfe7b1ee1b5fa8c31458e Mon Sep 17 00:00:00 2001
From: James Parker <james@galois.com>
Date: Tue, 27 Aug 2024 14:18:55 -0400
Subject: [PATCH 4/4] Fix benchmarking for failing tests

---
 tests/run-ci-benchmarks.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/run-ci-benchmarks.sh b/tests/run-ci-benchmarks.sh
index 6230713c3..f209dfd05 100755
--- a/tests/run-ci-benchmarks.sh
+++ b/tests/run-ci-benchmarks.sh
@@ -19,7 +19,7 @@ INDEX=0
 for TEST in ${TESTS}; do
 
   # Record wall clock time in seconds
-  /usr/bin/time -f "%e" -o /tmp/time cn verify "${TEST}" || true
+  /usr/bin/time --quiet -f "%e" -o /tmp/time cn verify "${TEST}" || true
   TIME=$(cat /tmp/time)
 
   # If we're last, don't print a trailing comma.