Add pair of CBMC proof-running GitHub Actions (#58)

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. This centralized GitHub Action can be used from each of the source code repositories.
FreeRTOS · Feb 28, 2023 · d823045 · d823045
1 parent 2503260
commit d823045
Show file tree

Hide file tree

Showing 2 changed files with 189 additions and 0 deletions.
diff --git a/run_cbmc/action.yml b/run_cbmc/action.yml
@@ -0,0 +1,55 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+# CBMC starter kit 2.9
+name: Run CBMC
+inputs:
+  proofs_dir:
+    required: true
+    description: >
+      The path to the cbmc/proofs directory, relative to the repository root
+      and including `/proofs` at the end.
+  run_cbmc_proofs_command:
+    required: true
+    default: ./run-cbmc-proofs.py
+    description: >
+      The path to a script that runs CBMC proofs by invoking Litani, relative
+      to the proofs directory
+
+runs:
+  using: composite
+  steps:
+    - name: Run CBMC
+      shell: bash
+      working-directory: ${{ inputs.proofs_dir }}
+      run: ${{ inputs.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
+      shell: bash
+      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="${{ inputs.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 ${{ inputs.proofs_dir }}/lib/summarize.py \
+          --run-file ${{ inputs.proofs_dir }}/output/latest/html/run.json
diff --git a/set_up_cbmc_runner/action.yml b/set_up_cbmc_runner/action.yml
@@ -0,0 +1,134 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+# CBMC starter kit 2.9
+name: Set up CBMC runner
+inputs:
+  cbmc_version:
+    description: Version number or 'latest' for CBMC
+    required: true
+    default: latest
+  cbmc_viewer_version:
+    description: Version number or 'latest' for CBMC Viewer
+    required: true
+    default: latest
+  litani_version:
+    description: Version number or 'latest' for Litani
+    required: true
+    default: latest
+  kissat_tag:
+    description: Git tag number or 'latest' for kissat SAT solver
+    required: true
+    default: ''
+  cadical_tag:
+    description: Git tag number or 'latest' for cadical SAT solver
+    required: true
+    default: ''
+
+runs:
+  using: composite
+  steps:
+    - name: Check out repository and submodules recursively
+      uses: actions/checkout@v3
+      with:
+        submodules: 'recursive'
+    - name: Install latest CBMC
+      if: ${{ inputs.cbmc_version == 'latest' }}
+      shell: bash
+      run: |
+        echo "Using latest CBMC"
+        # 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 ${{ inputs.cbmc_version }}
+      if: ${{ inputs.cbmc_version != 'latest' }}
+      shell: bash
+      run: |
+        echo "Using CBMC version ${{ inputs.cbmc_version }}"
+        curl -o cbmc.deb -L \
+          https://github.com/diffblue/cbmc/releases/download/cbmc-${{ inputs.cbmc_version }}/ubuntu-20.04-cbmc-${{ inputs.cbmc_version }}-Linux.deb
+        sudo dpkg -i ./cbmc.deb
+        rm ./cbmc.deb
+    - name: Install latest CBMC viewer
+      if: ${{ inputs.cbmc_viewer_version == 'latest' }}
+      shell: bash
+      run: |
+        echo "Using latest CBMC Viewer"
+        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 ${{ inputs.cbmc_viewer_version }}
+      if: ${{ inputs.cbmc_viewer_version != 'latest' }}
+      shell: bash
+      run: |
+        echo "Using CBMC Viewer version ${{ inputs.cbmc_version }}"
+        sudo apt-get update
+        sudo apt-get install --no-install-recommends --yes \
+          build-essential universal-ctags
+        pip3 install cbmc-viewer==${{ inputs.cbmc_viewer_version }}
+    - name: Install latest Litani
+      if: ${{ inputs.litani_version == 'latest' }}
+      shell: bash
+      run: |
+        echo "Using latest Litani"
+        # 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 ${{ inputs.litani_version }}
+      if: ${{ inputs.litani_version != 'latest' }}
+      shell: bash
+      run: |
+        echo "Using Litani version ${{ inputs.cbmc_version }}"
+        curl -o litani.deb -L \
+          https://github.com/awslabs/aws-build-accumulator/releases/download/${{ inputs.litani_version }}/litani-${{ inputs.litani_version }}.deb
+        sudo apt-get update
+        sudo apt-get install --no-install-recommends --yes ./litani.deb
+        rm ./litani.deb
+    - name: Install ${{ inputs.kissat_tag }} kissat
+      if: ${{ inputs.kissat_tag != '' }}
+      shell: bash
+      run: |
+        if ${{ inputs.kissat_tag == '' }}; then return 0; fi
+        if ${{ inputs.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=${{ inputs.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 ${{ inputs.cadical_tag }} cadical
+      if: ${{ inputs.cadical_tag != '' }}
+      shell: bash
+      run: |
+        if ${{ inputs.cadical_tag == '' }}; then return 0; fi
+        if ${{ inputs.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=${{ inputs.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