kani.yml

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
name: Kani CI
on:
  pull_request:
  push:
    # Not just any push, as that includes tags.
    # We don't want to re-trigger this workflow when tagging an existing commit.
    branches:
      - '**'

env:
  RUST_BACKTRACE: 1

jobs:
  regression:
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        os: [macos-11, ubuntu-20.04, ubuntu-22.04]
    steps:
      - name: Checkout Kani
        uses: actions/checkout@v3

      - name: Setup Kani Dependencies
        uses: ./.github/actions/setup
        with:
          os: ${{ matrix.os }}

      - name: Build Kani
        run: cargo build-dev

      - name: Execute Kani regression
        run: ./scripts/kani-regression.sh

  write-json-symtab-regression:
    runs-on: ubuntu-20.04
    steps:
      - name: Checkout Kani
        uses: actions/checkout@v3

      - name: Setup Kani Dependencies
        uses: ./.github/actions/setup
        with:
          os: ubuntu-20.04

      - name: Build Kani
        run: cargo build-dev -- --features write_json_symtab

      - name: Run tests
        run: |
          cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast
          cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast
          cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast


  benchcomp-tests:
    runs-on: ubuntu-20.04
    steps:
      - name: Checkout Kani
        uses: actions/checkout@v3

      - name: Install benchcomp dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y python3-pip
          pushd tools/benchcomp && pip3 install -r requirements.txt

      - name: Setup Kani Dependencies
        uses: ./.github/actions/setup
        with:
          os: ubuntu-20.04

      - name: Build Kani using release mode
        run: cargo build-dev -- --release

      - name: Run benchcomp unit and regression tests
        run: pushd tools/benchcomp && PATH=$(realpath ../../scripts):$PATH test/run

  perf:
    runs-on: ubuntu-20.04
    steps:
      - name: Checkout Kani
        uses: actions/checkout@v3

      - name: Setup Kani Dependencies
        uses: ./.github/actions/setup
        with:
          os: ubuntu-20.04

      - name: Build Kani using release mode
        run: cargo build-dev -- --release

      - name: Execute Kani performance tests
        run: ./scripts/kani-perf.sh

  bookrunner:
    runs-on: ubuntu-20.04
    permissions:
      contents: write
    steps:
      - name: Checkout Kani
        uses: actions/checkout@v3

      - name: Setup Kani Dependencies
        uses: ./.github/actions/setup
        with:
          os: ubuntu-20.04

      - name: Build Kani
        run: cargo build-dev

      - name: Install book runner dependencies
        run: ./scripts/setup/install_bookrunner_deps.sh

      - name: Generate book runner report
        run: cargo run -p bookrunner
        env:
          DOC_RUST_LANG_ORG_CHANNEL: nightly

      - name: Print book runner text results
        run: cat build/output/latest/html/bookrunner.txt

      - name: Print book runner failures grouped by stage
        run: python3 scripts/ci/bookrunner_failures_by_stage.py build/output/latest/html/index.html

      - name: Detect unexpected book runner failures
        run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt

      - name: Install book dependencies
        run: ./scripts/setup/ubuntu/install_doc_deps.sh

      # On one OS only, build the documentation, too.
      - name: Build Documentation
        run: ./scripts/build-docs.sh

      # When we're pushed to main branch, only then actually publish the docs.
      - name: Publish Documentation
        if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
        uses: JamesIves/github-pages-deploy-action@v4
        with:
          branch: gh-pages
          folder: docs/book/
          single-commit: true

  releasebundle-macos:
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        os: [macos-11]
        include:
          - os: macos-11
            artifact: kani-latest-x86_64-apple-darwin.tar.gz
    steps:
      - name: Checkout Kani
        uses: actions/checkout@v3

      - name: Setup Kani Dependencies
        uses: ./.github/actions/setup
        with:
          os: ${{ matrix.os }}

      - name: Build release bundle
        run: |
          cargo bundle -- latest
          cargo package -p kani-verifier

      # We can't run macos in a container, so we can only test locally.
      # Hopefully any dependency issues won't be unique to macos.
      - name: Local install test
        if: ${{ matrix.os == 'macos-11' }}
        run: |
          cargo install --path ./target/package/kani-verifier-*[^e]
          cargo-kani setup --use-local-bundle ./${{ matrix.artifact }}
          (cd tests/cargo-kani/simple-lib && cargo kani)
          (cd tests/cargo-kani/simple-visualize && cargo kani)
          (cd tests/cargo-kani/build-rs-works && cargo kani)

      - name: Upload artifact
        uses: actions/upload-artifact@v3
        with:
          name: ${{ matrix.artifact }}
          path: ${{ matrix.artifact }}
          if-no-files-found: error
          # Aggressively short retention: we don't really need these
          retention-days: 3

  releasebundle-ubuntu:
    runs-on: ubuntu-20.04
    container:
      image: ubuntu:18.04
    steps:
      # This is required before checkout because the container does not
      # have Git installed, so cannot run checkout action. The checkout
      # action requires Git >=2.18, so use the Git maintainers' PPA.
      - name: Install system dependencies
        run: |
          apt-get update
          apt-get install -y software-properties-common apt-utils
          add-apt-repository ppa:git-core/ppa
          apt-get update
          apt-get install -y \
            build-essential bash-completion curl lsb-release sudo g++ gcc flex \
            bison make patch git
          curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL \
            https://get.docker.com -o /tmp/install-docker.sh
          bash /tmp/install-docker.sh

      - name: Checkout Kani
        uses: actions/checkout@v3

      - name: Setup Kani Dependencies
        uses: ./.github/actions/setup
        with:
          os: ubuntu-18.04

      - name: Build release bundle
        run: |
          PATH=/github/home/.cargo/bin:$PATH cargo bundle -- latest
          PATH=/github/home/.cargo/bin:$PATH cargo package -p kani-verifier

      # -v flag: Use docker socket from host as we're running docker-in-docker
      - name: Build container test
        run: |
          for tag in 20-04 20-04-alt 18-04; do
            >&2 echo "Building test container for ${tag}"
            docker build -t kani-$tag -f scripts/ci/Dockerfile.bundle-test-ubuntu-$tag .
          done

      - name: Run installed tests
        run: |
          for tag in kani-20-04 kani-20-04-alt kani-18-04; do
            for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
              >&2 echo "Tag $tag: running test $dir"
              docker run -v /var/run/docker.sock:/var/run/docker.sock \
                -w /tmp/kani/tests/cargo-kani/$dir $tag cargo kani
            done
            docker run -v /var/run/docker.sock:/var/run/docker.sock \
              $tag cargo-kani setup \
                --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
          done

          # While the above test OS issues, now try testing with nightly as
          # default:
          docker run -v /var/run/docker.sock:/var/run/docker.sock \
            -w /tmp/kani/tests/cargo-kani/simple-lib kani-20-04  \
            bash -c "rustup default nightly && cargo kani"

      - name: Upload artifact
        uses: actions/upload-artifact@v3
        with:
          name: kani-latest-x86_64-unknown-linux-gnu.tar.gz
          path: kani-latest-x86_64-unknown-linux-gnu.tar.gz
          if-no-files-found: error
          # Aggressively short retention: we don't really need these
          retention-days: 3

  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"
          # We want to compare with $NEW_REF~. But we can't know what
          # that ref actually is until we clone the repository, so for
          # now make it equal to $NEW_REF
          echo "OLD_REF=${{ github.event.after }}" | tee -a "$GITHUB_ENV"

      - name: Save pull request HEAD and target to environment variables
        if: ${{ github.event_name == 'pull_request' }}
        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 Kani (old variant)
        uses: actions/checkout@v3
        with:
          path: ./old
          ref: ${{ env.OLD_REF }}
          fetch-depth: 2

      - name: Check out HEAD~ of push event as 'old' variant
        if: ${{ github.event_name == 'push' }}
        run: pushd old && git checkout "${NEW_REF}^"

      - name: Check out Kani (new variant)
        uses: actions/checkout@v3
        with:
          path: ./new
          ref: ${{ env.NEW_REF }}

      - name: Set up Kani Dependencies (old variant)
        uses: ./old/.github/actions/setup
        with:
          os: ubuntu-20.04
          kani_dir: old

      - name: Set up Kani Dependencies (new variant)
        uses: ./new/.github/actions/setup
        with:
          os: ubuntu-20.04
          kani_dir: new

      - name: Build Kani (new variant)
        run: pushd new && cargo build-dev

      - name: Build Kani (old variant)
        run: pushd old && cargo build-dev

      - name: Copy benchmarks from new to old
        run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/

      - name: Run benchcomp
        run: |
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            run
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            collate

      - name: Perf Regression Results Table
        run: |
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"

      - name: Run other visualizations
        run: |
          new/tools/benchcomp/bin/benchcomp \
            --config new/tools/benchcomp/configs/perf-regression.yaml \
            visualize --except dump_markdown_results_table