Add boogie_ast crate #614
Workflow file for this run
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 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 |