Avoid global path conditions in Kani's library #5273

Workflow file for this run

	# 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
	env:
	RUST_TEST_THREADS: 1

	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
	volumes:
	- /usr/local:/mnt/host-local
	steps:
	- name: Remove unnecessary software to free up disk space
	run: \|
	# inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
	df -h
	rm -r /mnt/host-local/lib/android /mnt/host-local/.ghcup
	df -h
	# 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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Avoid global path conditions in Kani's library #5273

Workflow file

Avoid global path conditions in Kani's library #5273

Jobs

Run details

Workflow file for this run