From 182929844419cf7ccbb428c780b17453a7fc3b14 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 28 Feb 2024 11:39:11 -0800
Subject: [PATCH] ebmc: benchmarking in CI

This runs the HWMCC 2008 competition benchmarks in CI, using the results
by abc as expected outcome.
---
 .github/workflows/pull-request-checks.yaml | 34 +++++++++++
 benchmarking/hwmcc08.sh                    | 71 ++++++++++++++++++++++
 2 files changed, 105 insertions(+)
 create mode 100755 benchmarking/hwmcc08.sh

diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index efd423d65..5f59a873d 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -106,6 +106,40 @@ jobs:
         run: make -C regression/verilog test-z3
       - name: Print ccache stats
         run: ccache -s
+      - name: Upload the ebmc binary
+        uses: actions/upload-artifact@v4
+        with:
+          name: ebmc-binary
+          retention-days: 5
+          path: src/ebmc/ebmc
+
+  # This job takes approximately 10 minutes
+  benchmarking:
+    runs-on: ubuntu-20.04
+    needs: check-ubuntu-20_04-make-clang
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Get the ebmc binary
+        uses: actions/download-artifact@v4
+        with:
+          name: ebmc-binary
+          path: ebmc
+      - name: Try the ebmc binary
+        run: chmod a+x ./ebmc/ebmc ; ./ebmc/ebmc --version
+      - name: HWMCC08 benchmarks
+        run: PATH=$PATH:$PWD/ebmc benchmarking/hwmcc08.sh
 
   # This job takes approximately 15 minutes
   check-centos8-make-gcc:
diff --git a/benchmarking/hwmcc08.sh b/benchmarking/hwmcc08.sh
new file mode 100755
index 000000000..4228d498a
--- /dev/null
+++ b/benchmarking/hwmcc08.sh
@@ -0,0 +1,71 @@
+#!/bin/sh
+
+if [ ! -e aiger/. ] ; then
+  echo Downloading and building the AIGER tools
+  git clone https://github.com/arminbiere/aiger
+  (cd aiger ; ./configure.sh ; make aigtosmv )
+fi
+
+if [ ! -e hwmcc08/. ] ; then
+  echo Downloading HWMCC08 benchmark archive
+  wget -q http://fmv.jku.at/hwmcc/hwmcc08public.tar.bz2
+  bunzip2 hwmcc08public.tar.bz2
+  tar xf hwmcc08public.tar
+  rm hwmcc08public.tar
+fi
+
+if [ ! -e hwmcc08public-smv/. ] ; then
+  echo Converting AIGER to SMV
+  mkdir hwmcc08public-smv
+  (cd hwmcc08; for FILE in *.aig ; do
+    SMV=`echo "$FILE" | sed s/.aig/.smv/`
+    ../aiger/aigtosmv -b "$FILE" "../hwmcc08public-smv/$SMV"
+  done)
+fi
+
+# expected answers
+# from the abc result column in https://fmv.jku.at/hwmcc08/hwmcc08results.csv
+
+if [ ! -e hwmcc08results.csv ] ; then
+  echo Downloading HWMCC08 result table
+  wget -q https://fmv.jku.at/hwmcc08/hwmcc08results.csv
+fi
+
+echo Running ebmc on the HWMCC08 benchmarks
+
+(# ignore first three lines of hwmcc08results.csv
+read -r line
+read -r line
+read -r line
+# now process the lines
+while read -r line; do
+  BENCHMARK=` echo "$line" | cut -d ',' -f 1 | tr -d '"'`
+  if [ ! -e "hwmcc08public-smv/${BENCHMARK}.smv" ] ; then
+    echo benchmark $BENCHMARK not found
+  else
+    RESULT=` echo "$line" | cut -d ',' -f 3 | tr -d '"'`
+    if [ "$RESULT" = "uns" ] ; then
+      ebmc --bound 2 "hwmcc08public-smv/${BENCHMARK}.smv" > ebmc.out
+      if [ $? = 10 ] ; then
+        echo $BENCHMARK: got unexpected couterexample
+        exit 1
+      else
+        echo $BENCHMARK: ok "(UNSAT)"
+      fi
+    fi
+    if [ "$RESULT" = "sat" ] ; then
+      LENGTH=` echo "$line" | cut -d ',' -f 2`
+      if [ "$LENGTH" = "\"*\"" ] ; then 
+        echo $BENCHMARK: no counterexample length
+      else
+        ebmc --bound $LENGTH "hwmcc08public-smv/${BENCHMARK}.smv" > ebmc.out
+        if [ $? = 10 ] ; then
+          echo $BENCHMARK: ok "(SAT $LENGTH)"
+        else
+          echo $BENCHMARK: failed to find couterexample at bound $LENGTH
+          exit 1
+        fi
+      fi
+    fi
+  fi
+done ) < hwmcc08results.csv