Build in Ubuntu 18.04 container in 20.04 image

.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

.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

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

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

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

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

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}"