From c49f775d14dfd3304149095175faecd8302881c2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 Nov 2023 10:18:48 +0000
Subject: [PATCH] Run regression tests

---
 .github/workflows/cbmc-update.yml | 47 +++++++++++++++++++++++++------
 1 file changed, 39 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml
index ca0244e95902..619abe703c9e 100644
--- a/.github/workflows/cbmc-update.yml
+++ b/.github/workflows/cbmc-update.yml
@@ -11,6 +11,7 @@ on:
 permissions:
   checks: write
   contents: write
+  issues: write
   pull-requests: write
 
 jobs:
@@ -20,6 +21,11 @@ jobs:
       - name: Checkout Kani
         uses: actions/checkout@v3
 
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-22.04
+
       - name: Compare CBMC versions
         env:
           GH_TOKEN: ${{ github.token }}
@@ -27,17 +33,31 @@ jobs:
           grep ^CBMC_VERSION kani-dependencies >> $GITHUB_ENV
           CBMC_LATEST=$(gh -R diffblue/cbmc release list | grep Latest | awk '{print $1}' | cut -f2 -d-)
           echo "CBMC_LATEST=$CBMC_LATEST" >> $GITHUB_ENV
-          if [ x$CBMC_LATEST != x$CBMC_VERSION ] ; then
-            if ! git ls-remote --exit-code origin cbmc-$CBMC_LATEST ; then
-              CBMC_LATEST_MAJOR=$(echo $CBMC_LATEST | cut -f1 -d.)
-              CBMC_LATEST_MINOR=$(echo $CBMC_LATEST | cut -f2 -d.)
-              sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_MAJOR\"/" kani-dependencies
-              sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_MINOR\"/" kani-dependencies
-              sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies
-              git diff
+          if [ x$CBMC_LATEST = x$CBMC_VERSION ] ; then
+            echo "next_step=none" >> $GITHUB_ENV
+          elif gh issue list -S \
+              "CBMC upgrade to $CBMC_LATEST failed" \
+              --json number,title | grep title ; then
+            echo "next_step=none" >> $GITHUB_ENV
+          elif ! git ls-remote --exit-code origin cbmc-$CBMC_LATEST ; then
+            CBMC_LATEST_MAJOR=$(echo $CBMC_LATEST | cut -f1 -d.)
+            CBMC_LATEST_MINOR=$(echo $CBMC_LATEST | cut -f2 -d.)
+            sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_MAJOR\"/" kani-dependencies
+            sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_MINOR\"/" kani-dependencies
+            sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies
+            git diff
+            if ! cargo build-dev ; then
+              echo "next_step=create_issue" >> $GITHUB_ENV
+            elif ! ./scripts/kani-regression.sh ; then
+              echo "next_step=create_issue" >> $GITHUB_ENV
+            else
+              echo "next_step=create_pr" >> $GITHUB_ENV
             fi
+          else
+            echo "next_step=none" >> $GITHUB_ENV
           fi
       - name: Create Pull Request
+        if: ${{ env.next_step == 'create_pr' }}
         uses: peter-evans/create-pull-request@v5
         with:
           commit-message: Upgrade CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }}
@@ -46,3 +66,14 @@ jobs:
           title: 'Automatic upgrade of CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }}'
           body: >
             Upgrade CBMC to its latest release.
+      - name: Create Issue
+        if: ${{ env.next_step == 'create_issue' }}
+        uses: dacbd/create-issue-action@main
+        with:
+          token: ${{ github.token }}
+          title: 'CBMC upgrade to ${{ env.CBMC_LATEST }} failed'
+          body: >
+            Updating CBMC from ${{ evn.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
+
+            The failed automated run
+            [can be found here.](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }})