diff --git a/.github/actions/build-bundle/action.yml b/.github/actions/build-bundle/action.yml new file mode 100644 index 000000000000..5db3b50e7158 --- /dev/null +++ b/.github/actions/build-bundle/action.yml @@ -0,0 +1,91 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +name: Build bundle +description: "Build the Kani bundle for the current architecture and OS. The inputs must match the worker architecture." +inputs: + arch: + description: "Current architecture tuple" + os: + description: "Current operating system" +outputs: + version: + description: "The bundle version (latest or =crate_version)" + value: ${{ steps.set_output.outputs.version }} + crate_version: + description: "The current crate version" + value: ${{ steps.set_output.outputs.crate_version }} + bundle: + description: "The bundle file name" + value: ${{ steps.set_output.outputs.bundle }} + package: + description: "The package file name" + value: ${{ steps.set_output.outputs.package }} +runs: + using: composite + steps: + - name: Export crate version + shell: bash + run: | + echo "CRATE_VERSION=$(cargo pkgid | cut -d@ -f2)" >> $GITHUB_ENV + + - name: Export tag version + shell: bash + if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/v') }} + run: | + echo "VERSION=${TAG_VERSION}" >> $GITHUB_ENV + + - name: Check Version + shell: bash + if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/v') }} + 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 + + - name: Export latest version + shell: bash + if: ${{ !startsWith(github.ref, 'refs/tags/v') }} + run: | + echo "VERSION=latest" >> $GITHUB_ENV + + - name: Build bundle + shell: bash + run: | + cargo bundle -- ${{ env.VERSION }} + echo "BUNDLE=kani-${{ env.VERSION }}-${{ inputs.arch }}.tar.gz" >> $GITHUB_ENV + + - name: Build package + shell: bash + run: | + cargo package -p kani-verifier + mv target/package/kani-verifier-${{ env.CRATE_VERSION }}.crate ${{ inputs.os }}-kani-verifier.crate + echo "PKG=${{ inputs.os }}-kani-verifier.crate" >> $GITHUB_ENV + + - name: Upload bundle + uses: actions/upload-artifact@v3 + with: + name: ${{ env.BUNDLE }} + path: ${{ env.BUNDLE }} + if-no-files-found: error + # Aggressively short retention: we don't really need these + retention-days: 3 + + - name: Upload kani-verifier pkg + uses: actions/upload-artifact@v3 + with: + name: ${{ env.PKG }} + path: ${{ env.PKG }} + if-no-files-found: error + # Aggressively short retention: we don't really need these + retention-days: 3 + + - name: Export output + shell: bash + id: set_output + run: | + echo "version=${{ env.VERSION }}" >> ${GITHUB_OUTPUT} + echo "crate_version=${{ env.CRATE_VERSION }}" >> ${GITHUB_OUTPUT} + echo "bundle=${{ env.BUNDLE }}" >> ${GITHUB_OUTPUT} + echo "package=${{ env.PKG }}" >> ${GITHUB_OUTPUT} diff --git a/.github/actions/setup/action.yml b/.github/actions/setup/action.yml index 489b0cbd4a17..4adc7fd5f1e2 100644 --- a/.github/actions/setup/action.yml +++ b/.github/actions/setup/action.yml @@ -1,6 +1,7 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT name: Setup Kani Dependencies +description: "Setup the machine to run Kani. Install rustup, dependencies and sync submodules." inputs: os: description: In which Operating System is this running @@ -21,12 +22,15 @@ runs: sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup df -h - - name: Install dependencies - run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh + - name: Install Rust toolchain + run: | + cd ${{ inputs.kani_dir }} + ./scripts/setup/install_rustup.sh + echo "$HOME/.cargo/bin" >> $GITHUB_PATH shell: bash - - name: Install Rust toolchain - run: cd ${{ inputs.kani_dir }} && ./scripts/setup/install_rustup.sh + - name: Install dependencies + run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh shell: bash - name: Update submodules diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 173b7b73a5be..a22ed971ec12 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -144,123 +144,3 @@ jobs: branch: gh-pages folder: docs/book/ single-commit: true - - releasebundle-macos: - runs-on: ${{ matrix.os }} - strategy: - matrix: - os: [macos-12] - include: - - os: macos-12 - 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-12' }} - 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 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 9afb7a819400..0537b401d73d 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -1,60 +1,33 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -name: Release +# +# 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-* -jobs: - Release: - name: Release - runs-on: ubuntu-20.04 - permissions: - contents: write - outputs: - version: ${{ steps.versioning.outputs.version }} - upload_url: ${{ steps.create_release.outputs.upload_url }} - steps: - - name: Checkout code - uses: actions/checkout@v3 - - - 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 refs/tags/kani-0.1.0 - echo "TAG_VERSION=$(echo ${{ github.ref }} | cut -d "-" -f 2)" >> $GITHUB_ENV - # Note that the above env vars get set for future steps, not this one - - name: Version Check - id: versioning - run: | - # Output for upload scripts to see - echo "version=${{ env.TAG_VERSION }}" >> $GITHUB_OUTPUT - # 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 - - - name: Create release - id: create_release - uses: ncipollo/release-action@v1.12.0 - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - with: - name: kani-${{ env.TAG_VERSION }} - tag: kani-${{ env.TAG_VERSION }} - body: | - Kani Rust verifier release bundle version ${{ env.TAG_VERSION }}. - draft: true +env: + RUST_BACKTRACE: 1 - MacOs-Bundle: - name: MacOs-Bundle - needs: Release +jobs: + build_bundle_macos: + name: BuildBundle-MacOs runs-on: macos-12 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@v3 @@ -64,37 +37,36 @@ jobs: with: os: macos-12 - - name: Build release bundle - run: | - cargo bundle - - - name: Upload artifact - uses: actions/upload-release-asset@v1 - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + - name: Build bundle + id: bundle + uses: ./.github/actions/build-bundle with: - upload_url: ${{ needs.Release.outputs.upload_url }} - asset_path: kani-${{ needs.Release.outputs.version }}-x86_64-apple-darwin.tar.gz - asset_name: kani-${{ needs.Release.outputs.version }}-x86_64-apple-darwin.tar.gz - asset_content_type: application/gzip - - Linux-Bundle: - name: Linux-Bundle - needs: Release + os: macos-12 + arch: x86_64-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 - permissions: - contents: write steps: - - name: Remove unnecessary software to free up disk space + + - 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, so use the Git maintainers' PPA. @@ -107,11 +79,8 @@ jobs: 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 code + - name: Checkout Kani uses: actions/checkout@v3 - name: Setup Kani Dependencies @@ -119,23 +88,161 @@ jobs: with: os: ubuntu-18.04 - - name: Build release bundle + - name: Build bundle + id: bundle + uses: ./.github/actions/build-bundle + with: + os: linux + arch: x86_64-unknown-linux-gnu + + test_bundle: + name: TestBundle + needs: [build_bundle_macos, build_bundle_linux] + strategy: + matrix: + os: [macos-12, 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-12 + 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: | - PATH=/github/home/.cargo/bin:$PATH cargo bundle + ls -lh . - - name: Upload artifact - uses: actions/upload-release-asset@v1 + - 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@v3 + + - 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 + if: ${{ github.event_name == 'push' }} + 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@v3 + 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 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@v3 + + - 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 + + - 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.12.0 env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} with: - upload_url: ${{ needs.Release.outputs.upload_url }} - asset_path: kani-${{ needs.Release.outputs.version }}-x86_64-unknown-linux-gnu.tar.gz - asset_name: kani-${{ needs.Release.outputs.version }}-x86_64-unknown-linux-gnu.tar.gz - asset_content_type: application/gzip - - Package-Docker: - name: 'Package Docker' - needs: Release + 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 @@ -178,11 +285,11 @@ jobs: push: true github-token: ${{ secrets.GITHUB_TOKEN }} tags: | - ghcr.io/${{ env.OWNER_LC }}/kani-${{ env.os }}:${{ needs.Release.outputs.version }} + 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.Release.outputs.version }} + 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. diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 index 37c1cabbdb5f..c530a44d1fc1 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 @@ -2,6 +2,10 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT # Note: this file is intended only for testing the kani release bundle +# This docker assumes the following locations: +# - ./kani_src/: Kani source code +# - ./kani-*tar.bz/: The Kani release bundle. E.g. `kani-0.39.0-x86_64-unknown-linux-gnu.tar.gz` +# - ./linux-kani-verifier.crate: The kani-verifier package FROM ubuntu:18.04 ENV DEBIAN_FRONTEND=noninteractive \ @@ -12,9 +16,10 @@ RUN apt-get update && \ ENV PATH="/root/.cargo/bin:${PATH}" WORKDIR /tmp/kani -COPY ./tests ./tests -COPY ./kani-latest-*.tar.gz ./ +COPY ./kani_src/tests ./tests +COPY ./kani-*.tar.gz ./ # Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` -COPY ./target/package/kani-verifier-*[^e] ./kani-verifier +COPY ./linux-kani-verifier.crate ./kani-verifier.crate +RUN tar zxvf ./kani-verifier.crate RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz +RUN cargo-kani setup --use-local-bundle ./kani-*.tar.gz