continue sketching out API #1254
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
| # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | |
| # SPDX-License-Identifier: MIT-0 | |
| # CBMC starter kit 2.10 | |
| name: Run CBMC proofs | |
| on: | |
| push: | |
| branches-ignore: | |
| - gh-pages | |
| pull_request: | |
| branches-ignore: | |
| - gh-pages | |
| merge_group: | |
| types: [checks_requested] | |
| branches: [main] | |
| # 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_64-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@v4 | |
| 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 z3-version bitwuzla-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, Z3, Bitwuzla 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 [ "${{ env.Z3_VERSION }}" == "" ]; then | |
| echo "You must specify a Z3 version (e.g. '4.13.0')" | |
| should_exit=true | |
| fi | |
| if [ "${{ env.Z3_VERSION }}" == "latest" ]; then | |
| echo "Z3 latest not supported at this time. You must specify an exact Z3 version (e.g. '4.13.0')" | |
| should_exit=true | |
| fi | |
| if [ "${{ env.BITWUZLA_VERSION }}" == "" ]; then | |
| echo "You must specify a Bitwuzla version (e.g. '0.5.0')" | |
| should_exit=true | |
| fi | |
| if [ "${{ env.BITWUZLA_VERSION }}" == "latest" ]; then | |
| echo "Bitwuzla latest not supported at this time. You must specify an exact version (e.g. '0.5.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 --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | jq -r '.[]|select(.prerelease|not).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 --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | jq -r .name | sed 's/viewer-//') | |
| sudo 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 | |
| sudo 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 --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | jq -r '.[]|select(.prerelease|not).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 Z3 ${{ env.Z3_VERSION }} | |
| if: ${{ env.Z3_VERSION != 'latest' }} | |
| shell: bash | |
| run: | | |
| curl -o z3.zip -L \ | |
| https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-glibc-2.31.zip | |
| sudo apt-get install --no-install-recommends --yes unzip | |
| unzip z3.zip | |
| cd z3-${{ env.Z3_VERSION }}-x64-glibc-2.31/bin \ | |
| && echo "Adding $(pwd) to PATH for Z3" \ | |
| && echo "$(pwd)" >> $GITHUB_PATH | |
| rm ../../z3.zip | |
| - name: Build and Install Bitwuzla ${{ env.BITWUZLA_VERSION }} | |
| if: ${{ env.BITWUZLA_VERSION != 'latest' }} | |
| shell: bash | |
| run: | | |
| echo "Installing Bitwuzla dependencies" | |
| sudo apt-get update | |
| sudo apt-get install --no-install-recommends --yes libgmp-dev cmake | |
| sudo pip3 install meson | |
| echo "Building Bitwuzla" | |
| BITWUZLA_TAG_NAME=${{ env.BITWUZLA_VERSION }} | |
| git clone https://github.com/bitwuzla/bitwuzla.git \ | |
| && cd bitwuzla \ | |
| && git checkout $BITWUZLA_TAG_NAME \ | |
| && ./configure.py \ | |
| && cd build \ | |
| && ninja; | |
| cd src/main \ | |
| && echo "Adding $(pwd) to PATH for Bitwuzla" \ | |
| && echo "$(pwd)" >> $GITHUB_PATH | |
| - 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 --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | 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 --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | 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 |