forked from FreeRTOS/CI-CD-Github-Actions
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information
Showing
1 changed file
with
166 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,166 @@ | ||
| # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| # SPDX-License-Identifier: MIT-0 | ||
| # CBMC starter kit 2.9 | ||
| name: Run CBMC proofs | ||
| runs: | ||
| using: composite | ||
| steps: | ||
| - name: Check out repository and submodules recursively | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| submodules: 'recursive' | ||
| - name: Parse config file | ||
| shell: bash | ||
| 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 | ||
| 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=$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 |