Skip to content

Commit 8d7f501

Browse files
karkhazkarkhaz
committed
Build in Ubuntu 18.04 container in 20.04 image
This is due to GitHub deprecating the Ubuntu 18.04 image. This commit fixes #1667.
1 parent a758084 commit 8d7f501

7 files changed

Lines changed: 111 additions & 49 deletions

File tree

‎.github/actions/setup/action.yml‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,5 +22,7 @@ runs:
2222

2323
- name: Update submodules
2424
run: |
25-
cd ${{ inputs.kani_dir }} && git submodule update --init --depth 1
25+
cd ${{ inputs.kani_dir }}
26+
git config --global --add safe.directory $(pwd)
27+
git submodule update --init --depth 1
2628
shell: bash

‎.github/workflows/kani.yml‎

Lines changed: 73 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ jobs:
1717
runs-on: ${{ matrix.os }}
1818
strategy:
1919
matrix:
20-
os: [macos-11, ubuntu-18.04, ubuntu-20.04, ubuntu-22.04]
20+
os: [macos-11, ubuntu-20.04, ubuntu-22.04]
2121
steps:
2222
- name: Checkout Kani
2323
uses: actions/checkout@v3
@@ -134,16 +134,14 @@ jobs:
134134
folder: docs/book/
135135
single-commit: true
136136

137-
releasebundle:
137+
releasebundle-macos:
138138
runs-on: ${{ matrix.os }}
139139
strategy:
140140
matrix:
141-
os: [macos-11, ubuntu-18.04]
141+
os: [macos-11]
142142
include:
143143
- os: macos-11
144144
artifact: kani-latest-x86_64-apple-darwin.tar.gz
145-
- os: ubuntu-18.04
146-
artifact: kani-latest-x86_64-unknown-linux-gnu.tar.gz
147145
steps:
148146
- name: Checkout Kani
149147
uses: actions/checkout@v3
@@ -158,29 +156,6 @@ jobs:
158156
cargo bundle -- latest
159157
cargo package -p kani-verifier
160158
161-
- name: Build container test
162-
if: ${{ matrix.os == 'ubuntu-18.04' }}
163-
run: |
164-
docker build -t kani-20-04 -f scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 .
165-
docker build -t kani-20-04-alt -f scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt .
166-
docker build -t kani-18-04 -f scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 .
167-
# this one does its tests automatically, for reasons documented in the file:
168-
docker build -t kani-nixos -f scripts/ci/Dockerfile.bundle-test-nixos .
169-
170-
- name: Run installed tests
171-
if: ${{ matrix.os == 'ubuntu-18.04' }}
172-
run: |
173-
for tag in kani-20-04 kani-20-04-alt kani-18-04; do
174-
docker run $tag cargo kani --version
175-
docker run -w /tmp/kani/tests/cargo-kani/simple-lib $tag cargo kani
176-
docker run -w /tmp/kani/tests/cargo-kani/simple-visualize $tag cargo kani
177-
docker run -w /tmp/kani/tests/cargo-kani/build-rs-works $tag cargo kani
178-
docker run -w /tmp/kani/tests/cargo-kani/simple-kissat $tag cargo kani
179-
docker run $tag cargo-kani setup --use-local-bundle ./${{ matrix.artifact }}
180-
done
181-
# While the above test OS issues, now try testing with nightly as default:
182-
docker run -w /tmp/kani/tests/cargo-kani/simple-lib kani-20-04 bash -c "rustup default nightly && cargo kani"
183-
184159
# We can't run macos in a container, so we can only test locally.
185160
# Hopefully any dependency issues won't be unique to macos.
186161
- name: Local install test
@@ -200,3 +175,73 @@ jobs:
200175
if-no-files-found: error
201176
# Aggressively short retention: we don't really need these
202177
retention-days: 3
178+
179+
releasebundle-ubuntu:
180+
runs-on: ubuntu-20.04
181+
container:
182+
image: ubuntu:18.04
183+
steps:
184+
# This is required before checkout because the container does not
185+
# have Git installed, so cannot run checkout action. The checkout
186+
# action requires Git >=2.18, so use the Git maintainers' PPA.
187+
- name: Install system dependencies
188+
run: |
189+
apt-get update
190+
apt-get install -y software-properties-common apt-utils
191+
add-apt-repository ppa:git-core/ppa
192+
apt-get update
193+
apt-get install -y \
194+
build-essential bash-completion curl lsb-release sudo g++ gcc flex \
195+
bison make patch git
196+
curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL \
197+
https://get.docker.com -o /tmp/install-docker.sh
198+
bash /tmp/install-docker.sh
199+
200+
- name: Checkout Kani
201+
uses: actions/checkout@v3
202+
203+
- name: Setup Kani Dependencies
204+
uses: ./.github/actions/setup
205+
with:
206+
os: ubuntu-18.04
207+
208+
- name: Build release bundle
209+
run: |
210+
PATH=/github/home/.cargo/bin:$PATH cargo bundle -- latest
211+
PATH=/github/home/.cargo/bin:$PATH cargo package -p kani-verifier
212+
213+
# -v flag: Use docker socket from host as we're running docker-in-docker
214+
- name: Build container test
215+
run: |
216+
for tag in 20-04 20-04-alt 18-04; do
217+
>&2 echo "Building test container for ${tag}"
218+
docker build -t kani-$tag -f scripts/ci/Dockerfile.bundle-test-ubuntu-$tag .
219+
done
220+
221+
- name: Run installed tests
222+
run: |
223+
for tag in kani-20-04 kani-20-04-alt kani-18-04; do
224+
for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
225+
>&2 echo "Tag $tag: running test $dir"
226+
docker run -v /var/run/docker.sock:/var/run/docker.sock \
227+
-w /tmp/kani/tests/cargo-kani/$dir $tag cargo kani
228+
done
229+
docker run -v /var/run/docker.sock:/var/run/docker.sock \
230+
$tag cargo-kani setup \
231+
--use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
232+
done
233+
234+
# While the above test OS issues, now try testing with nightly as
235+
# default:
236+
docker run -v /var/run/docker.sock:/var/run/docker.sock \
237+
-w /tmp/kani/tests/cargo-kani/simple-lib kani-20-04 \
238+
bash -c "rustup default nightly && cargo kani"
239+
240+
- name: Upload artifact
241+
uses: actions/upload-artifact@v3
242+
with:
243+
name: kani-latest-x86_64-unknown-linux-gnu.tar.gz
244+
path: kani-latest-x86_64-unknown-linux-gnu.tar.gz
245+
if-no-files-found: error
246+
# Aggressively short retention: we don't really need these
247+
retention-days: 3

‎scripts/ci/Dockerfile.bundle-release-20-04‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ ENV DEBIAN_FRONTEND=noninteractive \
88
DEBCONF_NONINTERACTIVE_SEEN=true \
99
PATH="/root/.cargo/bin:${PATH}"
1010
WORKDIR /tmp/kani
11+
COPY ./tests ./tests
12+
COPY ./Cargo.toml ./Cargo.toml
1113
COPY ./kani-*-x86_64-unknown-linux-gnu.tar.gz ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
1214
# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
1315
COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
@@ -23,5 +25,5 @@ RUN apt-get update && \
2325
rustup default $(rustup toolchain list | awk '{ print $1 }') && \
2426
cargo install --path ./kani-verifier && \
2527
cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz && \
26-
apt-get clean && \
28+
apt-get clean
2729
rm -rf /tmp/kani/* /root/.rustup/toolchains/*/share

‎scripts/ci/Dockerfile.bundle-test-ubuntu-18-04‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ ENV PATH="/root/.cargo/bin:${PATH}"
1313

1414
WORKDIR /tmp/kani
1515
COPY ./tests ./tests
16-
COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./
16+
COPY ./kani-latest-*.tar.gz ./
1717
# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
1818
COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
1919
RUN cargo install --path ./kani-verifier
20-
RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
20+
RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz

‎scripts/ci/Dockerfile.bundle-test-ubuntu-20-04‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ ENV PATH="/root/.cargo/bin:${PATH}"
1313

1414
WORKDIR /tmp/kani
1515
COPY ./tests ./tests
16-
COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./
16+
COPY ./kani-latest-*.tar.gz ./
1717
# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
1818
COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
1919
RUN cargo install --path ./kani-verifier
20-
RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
20+
RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz

‎scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ ENV PATH="/root/.cargo/bin:${PATH}"
1515

1616
WORKDIR /tmp/kani
1717
COPY ./tests ./tests
18-
COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./
18+
COPY ./kani-latest-*.tar.gz ./
1919
# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
2020
COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
2121
RUN cargo install --path ./kani-verifier
22-
RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
22+
RUN cargo-kani setup --use-local-bundle ./kani-latest-*.tar.gz

‎scripts/setup/ubuntu/install_cbmc.sh‎

Lines changed: 26 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -15,23 +15,36 @@ fi
1515
UBUNTU_VERSION=$(lsb_release -rs)
1616
MAJOR=${UBUNTU_VERSION%.*}
1717

18-
# CBMC currently only release a 18.04 and a 20.04 versions.
19-
if [[ "${MAJOR}" -le "18" ]]
18+
if [[ "${MAJOR}" -gt "18" ]]
2019
then
21-
MIRROR_VERSION="18.04"
22-
else
23-
MIRROR_VERSION="20.04"
20+
FILE="ubuntu-${UBUNTU_VERSION}-cbmc-${CBMC_VERSION}-Linux.deb"
21+
URL="https://github.com/diffblue/cbmc/releases/download/cbmc-${CBMC_VERSION}/$FILE"
22+
23+
set -x
24+
25+
wget -O "$FILE" "$URL"
26+
sudo dpkg -i "$FILE"
27+
cbmc --version
28+
rm $FILE
29+
exit 0
2430
fi
2531

26-
FILE="ubuntu-${MIRROR_VERSION}-cbmc-${CBMC_VERSION}-Linux.deb"
27-
URL="https://github.com/diffblue/cbmc/releases/download/cbmc-${CBMC_VERSION}/$FILE"
32+
# Binaries are no longer released for 18.04, so build from source
33+
34+
WORK_DIR=$(mktemp -d)
35+
git clone \
36+
--branch cbmc-${CBMC_VERSION} --depth 1 \
37+
https://github.com/diffblue/cbmc \
38+
"${WORK_DIR}"
2839

29-
set -x
40+
pushd "${WORK_DIR}"
3041

31-
wget -O "$FILE" "$URL"
32-
sudo dpkg -i "$FILE"
42+
mkdir build
43+
git submodule update --init
3344

34-
cbmc --version
45+
cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
46+
make -C build -j$(nproc)
47+
sudo make -C build install
3548

36-
# Clean up on success
37-
rm $FILE
49+
popd
50+
rm -rf "${WORK_DIR}"

0 commit comments

Comments
 (0)