diff --git a/proof_ci/action.yml b/proof_ci/action.yml deleted file mode 100644 index 58eefcbc..00000000 --- a/proof_ci/action.yml +++ /dev/null @@ -1,166 +0,0 @@ -# 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 diff --git a/run_cbmc/action.yml b/run_cbmc/action.yml new file mode 100644 index 00000000..d02b7647 --- /dev/null +++ b/run_cbmc/action.yml @@ -0,0 +1,52 @@ +# 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 + +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 new file mode 100644 index 00000000..95567dd7 --- /dev/null +++ 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