Skip to content
Kani CI

RFC: Global Conditions #4806

Sign in to view logs

RFC: Global Conditions

RFC: Global Conditions #4806

Workflow file for this run

.github/workflows/kani.yml at 1524e53
# 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