Merge pull request #3 from GaloisInc/benchmarking

Benchmarking

.github/workflows/ci-bench.yml

@@ -98,15 +98,15 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        cd tests; USE_OPAM='' ./run-ci-benchmarks.sh | tee output.txt
+        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/output.txt
+        output-file-path: tests/benchmark-data.json
         comment-on-alert: true
         # Access token to deploy GitHub Pages branch
         github-token: ${{ secrets.GITHUB_TOKEN }}

tests/run-ci-benchmarks.sh

@@ -1,18 +1,32 @@
 #!/bin/bash
 
-cat << EOF
+JSON_FILE="benchmark-data.json"
+
+cat << EOF >> ${JSON_FILE}
 [
+EOF
+
+DIRNAME=$(dirname "$0")
+
+SUCC=$(find "${DIRNAME}"/cn -name '*.c' | grep -v '\.error\.c')
+
+for TEST in ${SUCC}; do
+  # Record wall clock time in seconds
+  /usr/bin/time -f "%e" -o /tmp/time cn verify ${TEST}
+  TIME=$(cat /tmp/time)
+
+  # Hack to output JSON.
+  cat << EOF >> ${JSON_FILE}
     {
-        "name": "My Custom Smaller Is Better Benchmark - CPU Load",
+	"name": "${TEST}",
         "unit": "Seconds",
-        "value": 500
+	"value": ${TIME}
     },
-    {
-        "name": "My Custom Smaller Is Better Benchmark - Memory Used",
-        "unit": "Megabytes",
-        "value": 100,
-        "range": "3",
-        "extra": "Value for Tooltip: 25\nOptional Num #2: 100\nAnything Else!"
-    }
+EOF
+done
+
+cat << EOF >> ${JSON_FILE}
 ]
 EOF
+
+cat ${JSON_FILE}