diff --git a/.github/actions/setup/action.yml b/.github/actions/setup/action.yml index 97189d72d5f1..940a8436da05 100644 --- a/.github/actions/setup/action.yml +++ b/.github/actions/setup/action.yml @@ -22,5 +22,7 @@ runs: - name: Update submodules run: | - cd ${{ inputs.kani_dir }} && git submodule update --init --depth 1 + cd ${{ inputs.kani_dir }} + git config --global --add safe.directory $(pwd) + git submodule update --init --depth 1 shell: bash diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index feecccf84ebc..ebbaf2d97292 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -17,7 +17,7 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [macos-11, ubuntu-18.04, ubuntu-20.04, ubuntu-22.04] + os: [macos-11, ubuntu-20.04, ubuntu-22.04] steps: - name: Checkout Kani uses: actions/checkout@v3 @@ -134,16 +134,14 @@ jobs: folder: docs/book/ single-commit: true - releasebundle: + releasebundle-macos: runs-on: ${{ matrix.os }} strategy: matrix: - os: [macos-11, ubuntu-18.04] + os: [macos-11] include: - os: macos-11 artifact: kani-latest-x86_64-apple-darwin.tar.gz - - os: ubuntu-18.04 - artifact: kani-latest-x86_64-unknown-linux-gnu.tar.gz steps: - name: Checkout Kani uses: actions/checkout@v3 @@ -158,29 +156,6 @@ jobs: cargo bundle -- latest cargo package -p kani-verifier - - name: Build container test - if: ${{ matrix.os == 'ubuntu-18.04' }} - run: | - docker build -t kani-20-04 -f scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 . - docker build -t kani-20-04-alt -f scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt . - docker build -t kani-18-04 -f scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 . - # this one does its tests automatically, for reasons documented in the file: - docker build -t kani-nixos -f scripts/ci/Dockerfile.bundle-test-nixos . - - - name: Run installed tests - if: ${{ matrix.os == 'ubuntu-18.04' }} - run: | - for tag in kani-20-04 kani-20-04-alt kani-18-04; do - docker run $tag cargo kani --version - docker run -w /tmp/kani/tests/cargo-kani/simple-lib $tag cargo kani - docker run -w /tmp/kani/tests/cargo-kani/simple-visualize $tag cargo kani - docker run -w /tmp/kani/tests/cargo-kani/build-rs-works $tag cargo kani - docker run -w /tmp/kani/tests/cargo-kani/simple-kissat $tag cargo kani - docker run $tag cargo-kani setup --use-local-bundle ./${{ matrix.artifact }} - done - # While the above test OS issues, now try testing with nightly as default: - docker run -w /tmp/kani/tests/cargo-kani/simple-lib kani-20-04 bash -c "rustup default nightly && cargo kani" - # 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 @@ -200,3 +175,73 @@ jobs: 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 diff --git a/scripts/ci/Dockerfile.bundle-release-20-04 b/scripts/ci/Dockerfile.bundle-release-20-04 index 33baaaf04b1e..aabbb2f4662f 100644 --- a/scripts/ci/Dockerfile.bundle-release-20-04 +++ b/scripts/ci/Dockerfile.bundle-release-20-04 @@ -8,6 +8,8 @@ ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true \ PATH="/root/.cargo/bin:${PATH}" WORKDIR /tmp/kani +COPY ./tests ./tests +COPY ./Cargo.toml ./Cargo.toml COPY ./kani-*-x86_64-unknown-linux-gnu.tar.gz ./kani-latest-x86_64-unknown-linux-gnu.tar.gz # Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` COPY ./target/package/kani-verifier-*[^e] ./kani-verifier @@ -23,5 +25,5 @@ RUN apt-get update && \ rustup default $(rustup toolchain list | awk '{ print $1 }') && \ cargo install --path ./kani-verifier && \ cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz && \ - apt-get clean && \ + apt-get clean rm -rf /tmp/kani/* /root/.rustup/toolchains/*/share diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 index 55bc77f0b06b..37c1cabbdb5f 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 @@ -13,8 +13,8 @@ ENV PATH="/root/.cargo/bin:${PATH}" WORKDIR /tmp/kani COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ +COPY ./kani-latest-*.tar.gz ./ # Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` COPY ./target/package/kani-verifier-*[^e] ./kani-verifier RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz +RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 index f2516acd6f48..0335d8a5036d 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 @@ -13,8 +13,8 @@ ENV PATH="/root/.cargo/bin:${PATH}" WORKDIR /tmp/kani COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ +COPY ./kani-latest-*.tar.gz ./ # Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` COPY ./target/package/kani-verifier-*[^e] ./kani-verifier RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz +RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt index 076adf3030f1..53a7ab5f7667 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt @@ -15,8 +15,8 @@ ENV PATH="/root/.cargo/bin:${PATH}" WORKDIR /tmp/kani COPY ./tests ./tests -COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./ +COPY ./kani-latest-*.tar.gz ./ # Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate` COPY ./target/package/kani-verifier-*[^e] ./kani-verifier RUN cargo install --path ./kani-verifier -RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz +RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz diff --git a/scripts/setup/ubuntu/install_cbmc.sh b/scripts/setup/ubuntu/install_cbmc.sh index 0e182baf23f7..9aefab019110 100755 --- a/scripts/setup/ubuntu/install_cbmc.sh +++ b/scripts/setup/ubuntu/install_cbmc.sh @@ -15,23 +15,36 @@ fi UBUNTU_VERSION=$(lsb_release -rs) MAJOR=${UBUNTU_VERSION%.*} -# CBMC currently only release a 18.04 and a 20.04 versions. -if [[ "${MAJOR}" -le "18" ]] +if [[ "${MAJOR}" -gt "18" ]] then - MIRROR_VERSION="18.04" -else - MIRROR_VERSION="20.04" + FILE="ubuntu-${UBUNTU_VERSION}-cbmc-${CBMC_VERSION}-Linux.deb" + URL="https://github.com/diffblue/cbmc/releases/download/cbmc-${CBMC_VERSION}/$FILE" + + set -x + + wget -O "$FILE" "$URL" + sudo dpkg -i "$FILE" + cbmc --version + rm $FILE + exit 0 fi -FILE="ubuntu-${MIRROR_VERSION}-cbmc-${CBMC_VERSION}-Linux.deb" -URL="https://github.com/diffblue/cbmc/releases/download/cbmc-${CBMC_VERSION}/$FILE" +# Binaries are no longer released for 18.04, so build from source + +WORK_DIR=$(mktemp -d) +git clone \ + --branch cbmc-${CBMC_VERSION} --depth 1 \ + https://github.com/diffblue/cbmc \ + "${WORK_DIR}" -set -x +pushd "${WORK_DIR}" -wget -O "$FILE" "$URL" -sudo dpkg -i "$FILE" +mkdir build +git submodule update --init -cbmc --version +cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" +make -C build -j$(nproc) +sudo make -C build install -# Clean up on success -rm $FILE +popd +rm -rf "${WORK_DIR}"