performance.yaml

# Run performance benchmarks comparing two different CBMC versions.
name: Performance Benchmarking
on:
  push:
    branches: [ develop ]
  pull_request:
    branches: [ develop ]

jobs:
  perf-benchcomp:
    runs-on: ubuntu-20.04
    steps:
      - name: Save push event HEAD and HEAD~ to environment variables
        if: ${{ github.event_name == 'push' }}
        run: |
          echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
          echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"

      - name: Save pull request HEAD and base to environment variables
        if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }}
        run: |
          echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
          echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"

      - name: Check out CBMC (old variant)
        uses: actions/checkout@v4
        with:
          submodules: recursive
          path: ./old
          ref: ${{ env.OLD_REF }}
          fetch-depth: 2

      - name: Check out CBMC (new variant)
        uses: actions/checkout@v4
        with:
          submodules: recursive
          path: ./new
          ref: ${{ env.NEW_REF }}
          fetch-depth: 1

      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison ccache

      - name: Prepare ccache
        uses: actions/cache/restore@v4
        with:
          path: .ccache
          key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-20.04-Release-${{ github.ref }}
            ${{ runner.os }}-20.04-Release
      - name: ccache environment
        run: echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M

      - name: Configure using CMake (new variant)
        run: cmake -S new/ -B new/build -G Ninja -DWITH_JBMC=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
      - name: ccache environment (new variant)
        run: echo "CCACHE_BASEDIR=$PWD/new" >> $GITHUB_ENV
      - name: Build with Ninja (new variant)
        run: ninja -C new/build -j4
      - name: Print ccache stats (new variant)
        run: ccache -s

      - name: Configure using CMake (old variant)
        run: cmake -S old/ -B old/build -G Ninja -DWITH_JBMC=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
      - name: ccache environment (old variant)
        run: echo "CCACHE_BASEDIR=$PWD/old" >> $GITHUB_ENV
      - name: Build with Ninja (old variant)
        run: ninja -C old/build -j4
      - name: Print ccache stats (old variant)
        run: ccache -s

      - name: Obtain benchcomp
        run: git clone --depth 1 https://github.com/model-checking/kani kani.git

      - name: Fetch benchmarks
        run: |
          git clone --depth 1 https://github.com/awslabs/aws-c-common aws-c-common.git
          pushd aws-c-common.git/verification/cbmc/proofs/
          # keep 6 proofs of each kind of data structure
          for c in $(ls -d aws_* | cut -f2 -d_ | uniq) ; do rm -rf $(ls -d aws_${c}_* | tail -n+7) ; done
          popd
          sudo apt-get install --no-install-recommends -yq gnuplot graphviz universal-ctags python3-pip
          curl -L --remote-name \
            https://github.com/awslabs/aws-build-accumulator/releases/download/1.29.0/litani-1.29.0.deb
          sudo dpkg -i litani-1.29.0.deb
          sudo python3 -m pip install cbmc-viewer

      - name: Run benchcomp
        run: |
          kani.git/tools/benchcomp/bin/benchcomp \
            --config new/.github/performance/benchcomp-config.yaml \
            run
          kani.git/tools/benchcomp/bin/benchcomp \
            --config new/.github/performance/benchcomp-config.yaml \
            collate

      - name: Perf Regression Results Table
        run: |
          kani.git/tools/benchcomp/bin/benchcomp \
            --config new/.github/performance/benchcomp-config.yaml \
            visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"

      - name: Run other visualizations
        run: |
          kani.git/tools/benchcomp/bin/benchcomp \
            --config new/.github/performance/benchcomp-config.yaml \
            visualize --except dump_markdown_results_table