Towards Proving Memory Initialization #1561
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 | |
| # | |
| # This workflow will build, and, optionally, release Kani bundles in this order. | |
| # | |
| # The release will create a draft release and upload the bundles to it, and it will only run when we push a new | |
| # release tag (i.e.: tag named `kani-*`). | |
| name: Release Bundle | |
| on: | |
| pull_request: | |
| push: | |
| branches: | |
| - 'main' | |
| tags: | |
| - kani-* | |
| env: | |
| RUST_BACKTRACE: 1 | |
| jobs: | |
| build_bundle_macos: | |
| name: BuildBundle-MacOs | |
| runs-on: macos-13 | |
| permissions: | |
| contents: write | |
| outputs: | |
| version: ${{ steps.bundle.outputs.version }} | |
| bundle: ${{ steps.bundle.outputs.bundle }} | |
| package: ${{ steps.bundle.outputs.package }} | |
| crate_version: ${{ steps.bundle.outputs.crate_version }} | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: macos-13 | |
| - name: Build bundle | |
| id: bundle | |
| uses: ./.github/actions/build-bundle | |
| with: | |
| os: macos-13 | |
| arch: x86_64-apple-darwin | |
| build_bundle_macos_aarch64: | |
| name: BuildBundle-MacOs-ARM | |
| runs-on: macos-14 | |
| permissions: | |
| contents: write | |
| outputs: | |
| version: ${{ steps.bundle.outputs.version }} | |
| bundle: ${{ steps.bundle.outputs.bundle }} | |
| package: ${{ steps.bundle.outputs.package }} | |
| crate_version: ${{ steps.bundle.outputs.crate_version }} | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: macos-14 | |
| - name: Build bundle | |
| id: bundle | |
| uses: ./.github/actions/build-bundle | |
| with: | |
| os: macos-14 | |
| arch: aarch64-apple-darwin | |
| build_bundle_linux: | |
| name: BuildBundle-Linux | |
| runs-on: ubuntu-20.04 | |
| outputs: | |
| # The bundle version (latest or the version to be released) | |
| version: ${{ steps.bundle.outputs.version }} | |
| bundle: ${{ steps.bundle.outputs.bundle }} | |
| package: ${{ steps.bundle.outputs.package }} | |
| crate_version: ${{ steps.bundle.outputs.crate_version }} | |
| container: | |
| # Build using ubuntu 18 due to compatibility issues with older OS. | |
| image: ubuntu:18.04 | |
| volumes: | |
| - /usr/local:/mnt/host-local | |
| steps: | |
| - name: Free up docker 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 and python 3.7, so use the Git maintainers' PPA. | |
| # and the "deadsnakes" PPA, as the default version of python on ubuntu 22.04 is Python 3.10 | |
| - name: Install system dependencies | |
| run: | | |
| apt-get update | |
| apt-get install -y software-properties-common apt-utils | |
| add-apt-repository ppa:git-core/ppa | |
| add-apt-repository ppa:deadsnakes/ppa | |
| apt-get update | |
| apt-get install -y \ | |
| build-essential bash-completion curl lsb-release sudo g++ gcc flex \ | |
| bison make patch git python3.7 python3.7-dev python3.7-distutils | |
| update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1 | |
| curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py | |
| python3 get-pip.py --force-reinstall | |
| rm get-pip.py | |
| - name: Checkout Kani | |
| uses: actions/checkout@v3 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-18.04 | |
| - name: Build bundle | |
| id: bundle | |
| uses: ./.github/actions/build-bundle | |
| with: | |
| os: linux | |
| arch: x86_64-unknown-linux-gnu | |
| test-use-local-toolchain: | |
| name: TestLocalToolchain | |
| needs: [build_bundle_macos, build_bundle_linux] | |
| strategy: | |
| matrix: | |
| os: [macos-13, ubuntu-20.04, ubuntu-22.04] | |
| include: | |
| - os: macos-13 | |
| rust_target: x86_64-apple-darwin | |
| prev_job: ${{ needs.build_bundle_macos.outputs }} | |
| - os: ubuntu-20.04 | |
| rust_target: x86_64-unknown-linux-gnu | |
| prev_job: ${{ needs.build_bundle_linux.outputs }} | |
| - os: ubuntu-22.04 | |
| rust_target: x86_64-unknown-linux-gnu | |
| prev_job: ${{ needs.build_bundle_linux.outputs }} | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Download bundle | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ matrix.prev_job.bundle }} | |
| - name: Download kani-verifier crate | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ matrix.prev_job.package }} | |
| - name: Check download | |
| run: | | |
| ls -lh . | |
| - name: Get toolchain version used to setup kani | |
| run: | | |
| tar zxvf ${{ matrix.prev_job.bundle }} | |
| DATE=$(cat ./kani-${{ matrix.prev_job.version }}/rust-toolchain-version | cut -d'-' -f2,3,4) | |
| echo "Nightly date: $DATE" | |
| echo "DATE=$DATE" >> $GITHUB_ENV | |
| - name: Install Kani from path | |
| run: | | |
| tar zxvf ${{ matrix.prev_job.package }} | |
| cargo install --locked --path kani-verifier-${{ matrix.prev_job.crate_version }} | |
| - name: Create a custom toolchain directory | |
| run: mkdir -p ${{ github.workspace }}/../custom_toolchain | |
| - name: Fetch the nightly tarball | |
| run: | | |
| echo "Downloading Rust toolchain from rust server." | |
| curl --proto '=https' --tlsv1.2 -O https://static.rust-lang.org/dist/$DATE/rust-nightly-${{ matrix.rust_target }}.tar.gz | |
| tar -xzf rust-nightly-${{ matrix.rust_target }}.tar.gz | |
| ./rust-nightly-${{ matrix.rust_target }}/install.sh --prefix=${{ github.workspace }}/../custom_toolchain | |
| - name: Ensure installation is correct | |
| run: | | |
| cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }} --use-local-toolchain ${{ github.workspace }}/../custom_toolchain/ | |
| - name: Ensure that the rustup toolchain is not present | |
| run: | | |
| if [ ! -e "~/.rustup/toolchains/" ]; then | |
| echo "Default toolchain file does not exist. Proceeding with running tests." | |
| else | |
| echo "::error::Default toolchain exists despite not installing." | |
| exit 1 | |
| fi | |
| - name: Checkout tests | |
| uses: actions/checkout@v4 | |
| - name: Move rust-toolchain file to outside kani | |
| run: | | |
| mkdir -p ${{ github.workspace }}/../post-setup-tests | |
| cp -r tests/cargo-ui ${{ github.workspace }}/../post-setup-tests | |
| cp -r tests/kani/Assert ${{ github.workspace }}/../post-setup-tests | |
| ls ${{ github.workspace }}/../post-setup-tests | |
| - name: Run cargo-kani tests after moving | |
| run: | | |
| for dir in supported-lib-types/rlib multiple-harnesses verbose; do | |
| >&2 echo "Running test $dir" | |
| pushd ${{ github.workspace }}/../post-setup-tests/cargo-ui/$dir | |
| cargo kani | |
| popd | |
| done | |
| - name: Check --help and --version | |
| run: | | |
| >&2 echo "Running cargo kani --help and --version" | |
| pushd ${{ github.workspace }}/../post-setup-tests/Assert | |
| cargo kani --help && cargo kani --version | |
| popd | |
| - name: Run standalone kani test | |
| run: | | |
| >&2 echo "Running test on file bool_ref" | |
| pushd ${{ github.workspace }}/../post-setup-tests/Assert | |
| kani bool_ref.rs | |
| popd | |
| test_bundle: | |
| name: TestBundle | |
| needs: [build_bundle_macos, build_bundle_linux] | |
| strategy: | |
| matrix: | |
| os: [macos-13, ubuntu-20.04, ubuntu-22.04] | |
| include: | |
| # Stores the output of the previous job conditional to the OS | |
| - prev_job: ${{ needs.build_bundle_linux.outputs }} | |
| - os: macos-13 | |
| prev_job: ${{ needs.build_bundle_macos.outputs }} | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Download bundle | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ matrix.prev_job.bundle }} | |
| - name: Download kani-verifier crate | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ matrix.prev_job.package }} | |
| - name: Check download | |
| run: | | |
| ls -lh . | |
| - name: Install from bundle | |
| run: | | |
| tar zxvf ${{ matrix.prev_job.package }} | |
| cargo install --locked --path kani-verifier-${{ matrix.prev_job.crate_version }} | |
| cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }} | |
| - name: Checkout tests | |
| uses: actions/checkout@v4 | |
| - name: Run tests | |
| # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests. | |
| run: | | |
| for dir in simple-lib simple-visualize build-rs-works simple-kissat; do | |
| >&2 echo "Running test $dir" | |
| pushd tests/cargo-kani/$dir | |
| cargo kani | |
| popd | |
| done | |
| # This job will run tests for platforms that don't have a respective GitHub worker. | |
| # For now, we only test for Ubuntu-18.04 so we don't bother using matrix to configure the platform. | |
| test_alt_platform: | |
| name: TestAlternativePlatforms | |
| needs: [build_bundle_linux] | |
| runs-on: ubuntu-22.04 | |
| env: | |
| PKG: ${{ needs.build_bundle_linux.outputs.package }} | |
| BUNDLE: ${{ needs.build_bundle_linux.outputs.bundle }} | |
| VERSION: ${{ needs.build_bundle_linux.outputs.crate_version }} | |
| KANI_SRC: ./kani_src | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| with: | |
| path: ${{ env.KANI_SRC }} | |
| - name: Download bundle | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ env.BUNDLE }} | |
| - name: Download kani-verifier crate | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ env.PKG }} | |
| - name: Build container test | |
| run: | | |
| docker build -t kani-18-04 -f ${{ env.KANI_SRC }}/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 . | |
| - name: Run installed tests | |
| run: | | |
| for dir in simple-lib simple-visualize build-rs-works simple-kissat; do | |
| >&2 echo "Running test $dir" | |
| docker run -v /var/run/docker.sock:/var/run/docker.sock \ | |
| -w /tmp/kani/tests/cargo-kani/$dir kani-18-04 cargo kani | |
| 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-18-04 \ | |
| bash -c "rustup default nightly && cargo kani" | |
| kani_release: | |
| if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }} | |
| name: Release | |
| runs-on: ubuntu-20.04 | |
| needs: [build_bundle_macos, build_bundle_linux, test_bundle, test_alt_platform] | |
| permissions: | |
| contents: write | |
| outputs: | |
| version: ${{ steps.versioning.outputs.version }} | |
| upload_url: ${{ steps.create_release.outputs.upload_url }} | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Get version | |
| run: | | |
| # pkgid is something like file:///home/ubuntu/kani#kani-verifier:0.1.0 | |
| echo "CRATE_VERSION=$(cargo pkgid | cut -d@ -f2)" >> $GITHUB_ENV | |
| # GITHUB_REF is something like refs/tags/kani-0.1.0 | |
| echo "TAG_VERSION=$(echo ${{ github.ref }} | cut -d "-" -f 2)" >> $GITHUB_ENV | |
| - name: Check Version | |
| id: versioning | |
| run: | | |
| # Validate git tag & Cargo.toml are in sync on version number | |
| if [[ ${{ env.CRATE_VERSION }} != ${{ env.TAG_VERSION }} ]]; then | |
| echo "Git tag ${{env.TAG_VERSION}} did not match crate version ${{env.CRATE_VERSION}}" | |
| exit 1 | |
| fi | |
| echo "version=${{ env.TAG_VERSION }}" >> $GITHUB_OUTPUT | |
| - name: Download MacOS bundle | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ needs.build_bundle_macos.outputs.bundle }} | |
| - name: Download Linux bundle | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: ${{ needs.build_bundle_linux.outputs.bundle }} | |
| - name: Create release | |
| id: create_release | |
| uses: ncipollo/release-action@v1.14.0 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| name: kani-${{ env.TAG_VERSION }} | |
| tag: kani-${{ env.TAG_VERSION }} | |
| artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }}" | |
| body: | | |
| Kani Rust verifier release bundle version ${{ env.TAG_VERSION }}. | |
| draft: true | |
| package_docker: | |
| name: Package Docker | |
| needs: kani_release | |
| runs-on: ubuntu-20.04 | |
| permissions: | |
| contents: write | |
| packages: write | |
| env: | |
| os: ubuntu-20.04 | |
| target: x86_64-unknown-linux-gnu | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| - name: 'Build release bundle' | |
| run: | | |
| cargo bundle | |
| cargo package -p kani-verifier | |
| - name: 'Login to GitHub Container Registry' | |
| uses: docker/login-action@v3 | |
| with: | |
| registry: ghcr.io | |
| username: ${{ github.repository_owner }} | |
| password: ${{ secrets.GITHUB_TOKEN }} | |
| - name: 'Set lower case owner name. Needed for docker push.' | |
| run: | | |
| echo "OWNER_LC=${OWNER,,}" >>${GITHUB_ENV} | |
| env: | |
| OWNER: '${{ github.repository_owner }}' | |
| - name: Build and push | |
| uses: docker/build-push-action@v6 | |
| with: | |
| context: . | |
| file: scripts/ci/Dockerfile.bundle-release-20-04 | |
| push: true | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| tags: | | |
| ghcr.io/${{ env.OWNER_LC }}/kani-${{ env.os }}:${{ needs.kani_release.outputs.version }} | |
| ghcr.io/${{ env.OWNER_LC }}/kani-${{ env.os }}:latest | |
| labels: | | |
| org.opencontainers.image.source=${{ github.repositoryUrl }} | |
| org.opencontainers.image.version=${{ needs.kani_release.outputs.version }} | |
| org.opencontainers.image.licenses=Apache-2.0 OR MIT | |
| # This check will not work until #1655 is completed. | |
| # - name: Check action and image is updated. | |
| # uses: ./. | |
| # with: | |
| # command: | | |
| # [[ "$(cargo kani --version)" == 'cargo-kani ${{ needs.Release.outputs.version }}' ]] |