Add CBMC proof-running GitHub Action

This commit adds a GitHub Action that runs the CBMC proofs upon every
push and pull request. This is intended to replace the current CBMC CI.

.github/workflows/proof_ci.yaml

@@ -0,0 +1,188 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+# CBMC starter kit 2.9
+name: Run CBMC proofs
+on:
+  push:
+    branches-ignore:
+      - gh-pages
+  pull_request:
+    branches-ignore:
+      - gh-pages
+  workflow_dispatch:
+
+# USAGE
+#
+# If you need to use different versions for tools like CBMC, modify this file:
+# .github/workflows/proof_ci_resources/config.yaml
+#
+# If you want the CI to use a different GitHub-hosted runner (which must still
+# be running Ubuntu 20.04), modify the value of this key:
+# jobs.run_cbmc_proofs.runs-on
+
+jobs:
+  run_cbmc_proofs:
+    runs-on: cbmc_ubuntu-latest_32-core
+    name: run_cbmc_proofs
+    permissions:
+      contents: read
+      id-token: write
+      pull-requests: read
+    steps:
+      - name: Check out repository and submodules recursively
+        uses: actions/checkout@v3
+        with:
+          submodules: 'recursive'
+      - name: Parse config file
+        run: |
+          CONFIG_FILE='.github/workflows/proof_ci_resources/config.yaml'
+          for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version proofs-dir run-cbmc-proofs-command; do
+            VAR=$(echo $setting | tr "[:lower:]" "[:upper:]" | tr - _)
+            echo "${VAR}"=$(yq .$setting $CONFIG_FILE) >> $GITHUB_ENV
+          done
+      - name: Ensure CBMC, CBMC viewer, Litani versions have been specified
+        shell: bash
+        run: |
+          should_exit=false
+          if [ "${{ env.CBMC_VERSION }}" == "" ]; then
+            echo "You must specify a CBMC version (e.g. 'latest' or '5.70.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.CBMC_VIEWER_VERSION }}" == "" ]; then
+            echo "You must specify a CBMC viewer version (e.g. 'latest' or '3.6')"
+            should_exit=true
+          fi
+          if [ "${{ env.LITANI_VERSION }}" == "" ]; then
+            echo "You must specify a Litani version (e.g. 'latest' or '1.27.0')"
+            should_exit=true
+          fi
+          if [[ "$should_exit" == true ]]; then exit 1; fi
+      - name: Install latest CBMC
+        if: ${{ env.CBMC_VERSION == 'latest' }}
+        shell: bash
+        run: |
+          # Search within 5 most recent releases for latest available package
+          CBMC_REL="https://api.github.com/repos/diffblue/cbmc/releases?page=1&per_page=5"
+          CBMC_DEB=$(curl -s $CBMC_REL | jq -r '.[].assets[].browser_download_url' | grep -e 'ubuntu-20.04' | head -n 1)
+          CBMC_ARTIFACT_NAME=$(basename $CBMC_DEB)
+          curl -o $CBMC_ARTIFACT_NAME -L $CBMC_DEB
+          sudo dpkg -i $CBMC_ARTIFACT_NAME
+          rm ./$CBMC_ARTIFACT_NAME
+      - name: Install CBMC ${{ env.CBMC_VERSION }}
+        if: ${{ env.CBMC_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          curl -o cbmc.deb -L \
+            https://github.com/diffblue/cbmc/releases/download/cbmc-${{ env.CBMC_VERSION }}/ubuntu-20.04-cbmc-${{ env.CBMC_VERSION }}-Linux.deb
+          sudo dpkg -i ./cbmc.deb
+          rm ./cbmc.deb
+      - name: Install latest CBMC viewer
+        if: ${{ env.CBMC_VIEWER_VERSION == 'latest' }}
+        shell: bash
+        run: |
+          CBMC_VIEWER_REL="https://api.github.com/repos/model-checking/cbmc-viewer/releases/latest"
+          CBMC_VIEWER_VERSION=$(curl -s $CBMC_VIEWER_REL | jq -r .name | sed  's/viewer-//')
+          pip3 install cbmc-viewer==$CBMC_VIEWER_VERSION
+      - name: Install CBMC viewer ${{ env.CBMC_VIEWER_VERSION }}
+        if: ${{ env.CBMC_VIEWER_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends --yes \
+            build-essential universal-ctags
+          pip3 install cbmc-viewer==${{ env.CBMC_VIEWER_VERSION }}
+      - name: Install latest Litani
+        if: ${{ env.LITANI_VERSION == 'latest' }}
+        shell: bash
+        run: |
+          # Search within 5 most recent releases for latest available package
+          LITANI_REL="https://api.github.com/repos/awslabs/aws-build-accumulator/releases?page=1&per_page=5"
+          LITANI_DEB=$(curl -s $LITANI_REL | jq -r '.[].assets[0].browser_download_url' | head -n 1)
+          DBN_PKG_FILENAME=$(basename $LITANI_DEB)
+          curl -L $LITANI_DEB -o $DBN_PKG_FILENAME
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends --yes ./$DBN_PKG_FILENAME
+          rm ./$DBN_PKG_FILENAME
+      - name: Install Litani ${{ env.LITANI_VERSION }}
+        if: ${{ env.LITANI_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          curl -o litani.deb -L \
+            https://github.com/awslabs/aws-build-accumulator/releases/download/${{ env.LITANI_VERSION }}/litani-${{ env.LITANI_VERSION }}.deb
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends --yes ./litani.deb
+          rm ./litani.deb
+      - name: Install ${{ env.KISSAT_TAG }} kissat
+        if: ${{ env.KISSAT_TAG != '' }}
+        shell: bash
+        run: |
+          if ${{ env.KISSAT_TAG == 'latest' }}
+          then
+            KISSAT_REL="https://api.github.com/repos/arminbiere/kissat/releases/latest"
+            KISSAT_TAG_NAME=$(curl -s $KISSAT_REL | jq -r '.tag_name')
+          else
+            KISSAT_TAG_NAME=${{ env.KISSAT_TAG }}
+          fi
+          echo "Installing kissat $KISSAT_TAG_NAME"
+          git clone https://github.com/arminbiere/kissat.git \
+            && cd kissat \
+            && git checkout $KISSAT_TAG_NAME \
+            && ./configure \
+            && cd build \
+            && make -j;
+          echo "$(pwd)" >> $GITHUB_PATH
+      - name: Install ${{ env.CADICAL_TAG }} cadical
+        if: ${{ env.CADICAL_TAG != '' }}
+        shell: bash
+        run: |
+          if ${{ env.CADICAL_TAG == 'latest' }}
+          then
+            CADICAL_REL="https://api.github.com/repos/arminbiere/cadical/releases/latest"
+            CADICAL_TAG_NAME=$(curl -s $CADICAL_REL | jq -r '.tag_name')
+          else
+            CADICAL_TAG_NAME=${{ env.CADICAL_TAG }}
+          fi
+          echo "Installing cadical $CADICAL_TAG_NAME"
+          git clone https://github.com/arminbiere/cadical.git \
+            && cd cadical \
+            && git checkout $CADICAL_TAG_NAME \
+            && ./configure \
+            && cd build \
+            && make -j;
+          echo "$(pwd)" >> $GITHUB_PATH
+      - name: Run CBMC proofs
+        shell: bash
+        env:
+          EXTERNAL_SAT_SOLVER: kissat
+        working-directory: ${{ env.PROOFS_DIR }}
+        run: ${{ env.RUN_CBMC_PROOFS_COMMAND }}
+      - name: Check repository visibility
+        shell: bash
+        run: |
+          VIZ="${{ fromJson(toJson(github.event.repository)).visibility }}";
+          echo "REPO_VISIBILITY=${VIZ}" | tee -a "${GITHUB_ENV}";
+      - name: Set name for zip artifact with CBMC proof results
+        id: artifact
+        if: ${{ env.REPO_VISIBILITY == 'public' }}
+        run: |
+          echo "name=cbmc_proof_results_${{ fromJson(toJson(github.event.repository)).name }}_$(date +%Y_%m_%d_%H_%M_%S)" >> $GITHUB_OUTPUT
+      - name: Create zip artifact with CBMC proof results
+        if: ${{ env.REPO_VISIBILITY == 'public' }}
+        shell: bash
+        run: |
+          FINAL_REPORT_DIR=$PROOFS_DIR/output/latest/html
+          pushd $FINAL_REPORT_DIR \
+            && zip -r ${{ steps.artifact.outputs.name }}.zip . \
+            && popd \
+            && mv $FINAL_REPORT_DIR/${{ steps.artifact.outputs.name }}.zip .
+      - name: Upload zip artifact of CBMC proof results to GitHub Actions
+        if: ${{ env.REPO_VISIBILITY == 'public' }}
+        uses: actions/upload-artifact@v3
+        with:
+          name: ${{ steps.artifact.outputs.name }}
+          path: ${{ steps.artifact.outputs.name }}.zip
+      - name: CBMC proof results
+        shell: bash
+        run: |
+          python3 ${{ env.PROOFS_DIR }}/lib/summarize.py \
+            --run-file ${{ env.PROOFS_DIR }}/output/latest/html/run.json

.github/workflows/proof_ci_resources/config.yaml

@@ -0,0 +1,7 @@
+cadical-tag: latest
+cbmc-version: "5.63.0"
+cbmc-viewer-version: latest
+kissat-tag: latest
+litani-version: latest
+proofs-dir: verification/cbmc/proofs
+run-cbmc-proofs-command: ./run-cbmc-proofs.py

verification/cbmc/proofs/lib/print_tool_versions.py

@@ -0,0 +1,74 @@
+#!/usr/bin/env python3
+#
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+
+import logging
+import pathlib
+import shutil
+import subprocess
+
+
+_TOOLS = [
+    "cadical",
+    "cbmc",
+    "cbmc-viewer",
+    "cbmc-starter-kit-update",
+    "kissat",
+    "litani",
+]
+
+
+def _format_versions(table):
+    lines = [
+        "<table>",
+        '<tr><td colspan="2" style="font-weight: bold">Tool Versions</td></tr>',
+    ]
+    for tool, version in table.items():
+        if version:
+            v_str = f'<code><pre style="margin: 0">{version}</pre></code>'
+        else:
+            v_str = '<em>not found</em>'
+        lines.append(
+            f'<tr><td style="font-weight: bold; padding-right: 1em; '
+            f'text-align: right;">{tool}:</td>'
+            f'<td>{v_str}</td></tr>')
+    lines.append("</table>")
+    return "\n".join(lines)
+
+
+def _get_tool_versions():
+    ret = {}
+    for tool in _TOOLS:
+        err = f"Could not determine version of {tool}: "
+        ret[tool] = None
+        if not shutil.which(tool):
+            logging.error("%s'%s' not found on $PATH", err, tool)
+            continue
+        cmd = [tool, "--version"]
+        proc = subprocess.Popen(cmd, text=True, stdout=subprocess.PIPE)
+        try:
+            out, _ = proc.communicate(timeout=10)
+        except subprocess.TimeoutExpired:
+            logging.error("%s'%s --version' timed out", err, tool)
+            continue
+        if proc.returncode:
+            logging.error(
+                "%s'%s --version' returned %s", err, tool, str(proc.returncode))
+            continue
+        ret[tool] = out.strip()
+    return ret
+
+
+def main():
+    exe_name = pathlib.Path(__file__).name
+    logging.basicConfig(format=f"{exe_name}: %(message)s")
+
+    table = _get_tool_versions()
+    out = _format_versions(table)
+    print(out)
+
+
+if __name__ == "__main__":
+    main()

verification/cbmc/proofs/lib/summarize.py

@@ -1,8 +1,28 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
 
+import argparse
 import json
 import logging
+import os
+import sys
+
+
+DESCRIPTION = """Print 2 tables in GitHub-flavored Markdown that summarize
+an execution of CBMC proofs."""
+
+
+def get_args():
+    """Parse arguments for summarize script."""
+    parser = argparse.ArgumentParser(description=DESCRIPTION)
+    for arg in [{
+            "flags": ["--run-file"],
+            "help": "path to the Litani run.json file",
+            "required": True,
+    }]:
+        flags = arg.pop("flags")
+        parser.add_argument(*flags, **arg)
+    return parser.parse_args()
 
 
 def _get_max_length_per_column_list(data):
@@ -56,6 +76,7 @@ def _get_status_and_proof_summaries(run_dict):
     run_dict
         A dictionary representing a Litani run.
 
+
     Returns
     -------
     A list of 2 lists.
@@ -70,8 +91,9 @@ def _get_status_and_proof_summaries(run_dict):
             count_statuses[status_pretty_name] += 1
         except KeyError:
             count_statuses[status_pretty_name] = 1
-        proof = proof_pipeline["name"]
-        proofs.append([proof, status_pretty_name])
+        if proof_pipeline["name"] == "print_tool_versions":
+            continue
+        proofs.append([proof_pipeline["name"], status_pretty_name])
     statuses = [["Status", "Count"]]
     for status, count in count_statuses.items():
         statuses.append([status, str(count)])
@@ -83,10 +105,39 @@ def print_proof_results(out_file):
     Print 2 strings that summarize the proof results.
     When printing, each string will render as a GitHub flavored Markdown table.
     """
+    output = "## Summary of CBMC proof results\n\n"
+    with open(out_file, encoding='utf-8') as run_json:
+        run_dict = json.load(run_json)
+    status_table, proof_table = _get_status_and_proof_summaries(run_dict)
+    for summary in (status_table, proof_table):
+        output += _get_rendered_table(summary)
+
+    print(output)
+    sys.stdout.flush()
+
+    github_summary_file = os.getenv("GITHUB_STEP_SUMMARY")
+    if github_summary_file:
+        with open(github_summary_file, "a") as handle:
+            print(output, file=handle)
+            handle.flush()
+    else:
+        logging.warning(
+            "$GITHUB_STEP_SUMMARY not set, not writing summary file")
+
+    msg = (
+        "Click the 'Summary' button to view a Markdown table "
+        "summarizing all proof results")
+    if run_dict["status"] != "success":
+        logging.error("Not all proofs passed.")
+        logging.error(msg)
+        sys.exit(1)
+    logging.info(msg)
+
+
+if __name__ == '__main__':
+    args = get_args()
+    logging.basicConfig(format="%(levelname)s: %(message)s")
     try:
-        with open(out_file, encoding='utf-8') as run_json:
-            run_dict = json.load(run_json)
-            for summary in _get_status_and_proof_summaries(run_dict):
-                print(_get_rendered_table(summary))
+        print_proof_results(args.run_file)
     except Exception as ex: # pylint: disable=broad-except
         logging.critical("Could not print results. Exception: %s", str(ex))