Skip to content

Commit 8098ea8

Browse files
misonijnikmisonijnik
authored
ci: Fix docker release workflow (#203)
* ci: Fix `freebsd` image version on cirrus * ci: Pin Ubuntu version to set Z3 as a default solver for macOS * chore: Update gtest version * ci: Update llvm version in Dockerfile * fix(scripts): Fix ShellCheck warning * feat(build): Add `ENABLE_FP_RUNTIME` option * style: Use a vector instead of an array as a variable-length container * chore(docker): Update Dockerfile * test: Require `not-ubsan` for a couple of tests with 32-bit binaries
1 parent 8513a6d commit 8098ea8

13 files changed

Lines changed: 68 additions & 78 deletions

File tree

‎.cirrus.yml‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,15 @@
11
task:
22
freebsd_instance:
33
matrix:
4-
- image_family: freebsd-13-2-snap
5-
- image_family: freebsd-14-0-snap
4+
- image_family: freebsd-15-0-snap
65
deps_script:
76
- sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf
87
- env ASSUME_ALWAYS_YES=yes pkg update -f
98
- env ASSUME_ALWAYS_YES=yes pkg install -y llvm13 gmake z3 cmake pkgconf google-perftools python3 py311-sqlite3 py311-tabulate nlohmann-json bash coreutils immer
109
build_script:
1110
- mkdir build
1211
- cd build
13-
- cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DENABLE_WARNINGS_AS_ERRORS=1 ..
12+
- cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DENABLE_WARNINGS_AS_ERRORS=1 -DENABLE_FP_RUNTIME=1 ..
1413
- gmake
1514
test_script:
1615
- sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg

‎.github/workflows/build-in-base-env.yml‎

Lines changed: 0 additions & 25 deletions
This file was deleted.

‎.github/workflows/build.yaml‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,8 @@ env:
2424
ENABLE_OPTIMIZED: 1
2525
ENABLE_DEBUG: 1
2626
ENABLE_WARNINGS_AS_ERRORS: ${{ github.event_name == 'workflow_dispatch' && inputs.warnings_as_errors || 1}}
27-
GTEST_VERSION: 1.11.0
27+
ENABLE_FP_RUNTIME: 1
28+
GTEST_VERSION: 1.16.0
2829
KLEE_RUNTIME_BUILD: "Debug+Asserts"
2930
LLVM_VERSION: 11
3031
MINISAT_VERSION: "master"
@@ -43,7 +44,7 @@ env:
4344

4445
jobs:
4546
Linux:
46-
runs-on: ubuntu-latest
47+
runs-on: ubuntu-22.04
4748
strategy:
4849
matrix:
4950
name: [
@@ -160,7 +161,9 @@ jobs:
160161
env:
161162
LLVM_VERSION: 14
162163
BASE: /tmp
163-
SOLVERS: STP
164+
SOLVERS: Z3
165+
Z3_VERSION: 4.14.1
166+
ENABLE_FP_RUNTIME: 0
164167
UCLIBC_VERSION: 0
165168
USE_TCMALLOC: 0
166169
USE_LIBCXX: 0

‎.github/workflows/docker_release_push.yml‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,23 +6,24 @@ on:
66

77
jobs:
88
push_to_registry:
9-
name: Push Docker Image to Docker Hub
9+
name: Push Docker Image to Github Registry
1010
runs-on: ubuntu-latest
1111
steps:
1212
- name: Check out the repo
1313
uses: actions/checkout@v3
1414

15-
- name: Log in to Docker Hub
15+
- name: Log in to Github Registry
1616
uses: docker/login-action@f4ef78c080cd8ba55a85445d5b36e214a81df20a
1717
with:
18-
username: ${{ secrets.DOCKER_USERNAME }}
19-
password: ${{ secrets.DOCKER_PASSWORD }}
18+
registry: ghcr.io
19+
username: ${{ github.actor }}
20+
password: ${{ secrets.GH_REGISTRY }}
2021

2122
- name: Extract metadata (tags, labels) for Docker
2223
id: meta
2324
uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7
2425
with:
25-
images: klee/klee
26+
images: ghcr.io/unittestbot/klee/klee
2627

2728
- name: Build and push Docker image
2829
uses: docker/build-push-action@3b5e8027fcad23fda98b2e3ac259d8d67585f671
@@ -31,4 +32,4 @@ jobs:
3132
file: ./Dockerfile
3233
push: true
3334
tags: ${{ steps.meta.outputs.tags }}
34-
labels: ${{ steps.meta.outputs.labels }}
35+
labels: ${{ steps.meta.outputs.labels }}

‎Dockerfile‎

Lines changed: 23 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,40 @@
1-
FROM ghcr.io/klee/llvm:130_O_D_A_ubuntu_jammy-20230126 as llvm_base
2-
FROM ghcr.io/klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_base
3-
FROM ghcr.io/klee/uclibc:klee_uclibc_v1.3_130_ubuntu_jammy-20230126 as uclibc_base
4-
FROM ghcr.io/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 as tcmalloc_base
5-
FROM ghcr.io/klee/stp:2.3.3_ubuntu_jammy-20230126 as stp_base
6-
FROM ghcr.io/klee/z3:4.8.15_ubuntu_jammy-20230126 as z3_base
7-
FROM ghcr.io/klee/libcxx:130_ubuntu_jammy-20230126 as libcxx_base
8-
FROM ghcr.io/klee/sqlite:3400100_ubuntu_jammy-20230126 as sqlite3_base
9-
FROM llvm_base as intermediate
1+
FROM ghcr.io/unittestbot/klee/llvm:140_O_D_A_ubuntu_jammy-20230126 AS llvm_base
2+
FROM ghcr.io/unittestbot/klee/gtest:1.16.0_ubuntu_jammy-20230126 AS gtest_base
3+
FROM ghcr.io/unittestbot/klee/uclibc:klee_uclibc_v1.4_140_ubuntu_jammy-20230126 AS uclibc_base
4+
FROM ghcr.io/unittestbot/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 AS tcmalloc_base
5+
FROM ghcr.io/unittestbot/klee/stp:2.3.3_ubuntu_jammy-20230126 AS stp_base
6+
FROM ghcr.io/unittestbot/klee/z3:4.8.15_ubuntu_jammy-20230126 AS z3_base
7+
FROM ghcr.io/unittestbot/klee/bitwuzla:0.7.0_ubuntu_jammy-20230126 AS bitwuzla_base
8+
FROM ghcr.io/unittestbot/klee/libcxx:140_ubuntu_jammy-20230126 AS libcxx_base
9+
FROM ghcr.io/unittestbot/klee/sqlite:3400100_ubuntu_jammy-20230126 AS sqlite3_base
10+
FROM ghcr.io/unittestbot/klee/immer:v0.8.1_ubuntu_jammy-20230126 AS immer_base
11+
FROM ghcr.io/unittestbot/klee/json:v3.11.3_ubuntu_jammy-20230126 AS json_base
12+
FROM llvm_base AS intermediate
1013
COPY --from=gtest_base /tmp /tmp/
1114
COPY --from=uclibc_base /tmp /tmp/
1215
COPY --from=tcmalloc_base /tmp /tmp/
1316
COPY --from=stp_base /tmp /tmp/
1417
COPY --from=z3_base /tmp /tmp/
18+
COPY --from=bitwuzla_base /tmp /tmp/
1519
COPY --from=libcxx_base /tmp /tmp/
1620
COPY --from=sqlite3_base /tmp /tmp/
21+
COPY --from=immer_base /tmp /tmp/
22+
COPY --from=json_base /tmp /tmp/
1723
ENV COVERAGE=0
1824
ENV USE_TCMALLOC=1
1925
ENV BASE=/tmp
2026
ENV BUILD_SUFFIX="default"
21-
ENV LLVM_VERSION=13.0
27+
ENV LLVM_VERSION=14
2228
ENV ENABLE_DOXYGEN=1
2329
ENV ENABLE_OPTIMIZED=1
2430
ENV ENABLE_DEBUG=1
2531
ENV DISABLE_ASSERTIONS=0
2632
ENV ENABLE_WARNINGS_AS_ERRORS=1
33+
ENV ENABLE_FP_RUNTIME=1
2734
ENV REQUIRES_RTTI=0
28-
ENV SOLVERS=STP:Z3
29-
ENV GTEST_VERSION=1.11.0
30-
ENV UCLIBC_VERSION=klee_uclibc_v1.3
35+
ENV SOLVERS=BITWUZLA:Z3:STP
36+
ENV GTEST_VERSION=1.16.0
37+
ENV UCLIBC_VERSION=klee_uclibc_v1.4
3138
ENV TCMALLOC_VERSION=2.9.1
3239
ENV SANITIZER_BUILD=
3340
ENV STP_VERSION=2.3.3
@@ -37,8 +44,9 @@ ENV USE_LIBCXX=1
3744
ENV KLEE_RUNTIME_BUILD="Debug+Asserts"
3845
ENV SQLITE_VERSION=3400100
3946
ENV JSON_VERSION=v3.11.3
47+
ENV BITWUZLA_VERSION=0.7.0
4048
ENV IMMER_VERSION=v0.8.1
41-
LABEL maintainer="KLEE Developers"
49+
LABEL maintainer="KLEEF Developers"
4250

4351
# TODO remove adding sudo package
4452
# Create ``klee`` user for container with password ``klee``.
@@ -60,7 +68,7 @@ RUN /tmp/klee_src/scripts/build/build.sh --debug --install-system-deps klee && p
6068
sudo rm -rf /var/lib/apt/lists/*
6169

6270

63-
ENV PATH="$PATH:/tmp/llvm-130-install_O_D_A/bin:/home/klee/klee_build/bin:/home/klee/.local/bin"
71+
ENV PATH="$PATH:/tmp/llvm-140-install_O_D_A/bin:/home/klee/klee_build/bin:/home/klee/.local/bin"
6472
ENV BASE=/tmp
6573
# Add path to local LLVM installation - let system install precede local install
6674
RUN /bin/bash -c 'echo "export \"PATH=$PATH:$(cd ${BASE}/llvm-*-install*/bin/ && pwd)\" >> /home/klee/.bashrc"'

‎build.sh‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ KLEE_RUNTIME_BUILD="Release"
2020
COVERAGE=0
2121
ENABLE_DOXYGEN=0
2222
USE_TCMALLOC=0
23+
ENABLE_FP_RUNTIME=1
2324
TCMALLOC_VERSION=2.9.1
2425
USE_LIBCXX=1
2526
# Also required despite not being mentioned in the guide
@@ -71,4 +72,4 @@ else
7172
fi
7273
done
7374

74-
BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ./scripts/build/build.sh klee --install-system-deps
75+
BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME ./scripts/build/build.sh klee --install-system-deps

‎lib/Core/Executor.cpp‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2528,8 +2528,9 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
25282528
uint64_t size = 0; // total size of variadic arguments
25292529
bool requires16ByteAlignment = false;
25302530

2531-
uint64_t offsets[callingArgs]; // offsets of variadic arguments
2532-
uint64_t argWidth; // width of current variadic argument
2531+
std::vector<uint64_t> offsets;
2532+
offsets.reserve(callingArgs); // offsets of variadic arguments
2533+
uint64_t argWidth; // width of current variadic argument
25332534

25342535
const CallBase &cb = cast<CallBase>(*i);
25352536
for (unsigned k = funcArgs; k < callingArgs; k++) {

‎scripts/build/p-gtest.inc‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
11
setup_build_variables_gtest() {
2-
GTEST_INSTALL_PATH="${BASE}/googletest-release-${GTEST_VERSION}"
2+
GTEST_INSTALL_PATH="${BASE}/googletest-${GTEST_VERSION}"
33
return 0
44
}
55

66
download_gtest() {
77
cd "${BASE}" || exit 1
8-
wget "https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip"
9-
unzip -o "release-${GTEST_VERSION}.zip"
10-
rm "release-${GTEST_VERSION}.zip"
11-
touch "${GTEST_INSTALL_PATH}"/.is_installed
8+
wget "https://github.com/google/googletest/archive/refs/tags/v${GTEST_VERSION}.zip"
9+
unzip -o "v${GTEST_VERSION}.zip"
10+
rm "v${GTEST_VERSION}.zip"
1211
}
1312

1413
build_gtest() {
@@ -42,4 +41,4 @@ get_docker_config_id_gtest() {
4241
setup_build_variables_gtest
4342
echo "${GTEST_VERSION}"
4443
)
45-
}
44+
}

‎scripts/build/p-klee.inc‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -91,12 +91,11 @@ fi
9191
echo "Z3"
9292
KLEE_Z3_CONFIGURE_OPTION=(
9393
"-DENABLE_SOLVER_Z3=TRUE"
94-
"-DZ3_INCLUDE_DIRS=${Z3_INSTALL_PATH}/include"
95-
"-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib/libz3.so"
9694
)
95+
CMAKE_PREFIX_PATH+=("${Z3_INSTALL_PATH}")
9796
KLEE_FLOATING_POINT=(
98-
"-DENABLE_FLOATING_POINT=TRUE"
99-
"-DENABLE_FP_RUNTIME=TRUE"
97+
"-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}"
98+
"-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"
10099
)
101100
;;
102101
metasmt)
@@ -114,11 +113,10 @@ fi
114113
KLEE_BITWUZLA_CONFIGURE_OPTION=(
115114
"-DENABLE_SOLVER_BITWUZLA=TRUE"
116115
)
117-
118116
CMAKE_PREFIX_PATH+=("${BITWUZLA_INSTALL_PATH}")
119117
KLEE_FLOATING_POINT=(
120-
"-DENABLE_FLOATING_POINT=TRUE"
121-
"-DENABLE_FP_RUNTIME=TRUE"
118+
"-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}"
119+
"-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"
122120
)
123121
echo "bitwuzla"
124122
;;

‎scripts/build/p-z3-osx.inc‎

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,14 @@
1-
install_binary_artifact_z3 () {
2-
set +e
3-
brew install python@2
4-
if [[ "X$?" != "X0" ]]; then
5-
brew link --overwrite python@2
6-
fi
7-
set -e
1+
#!/usr/bin/env bash
2+
# shellcheck disable=SC2034
3+
4+
install_binary_artifact_z3() {
85
brew install z3
96
}
107

11-
is_installed_z3() {
12-
[[ -f "/usr/local/opt/z3/bin/z3" ]]
13-
}
8+
setup_artifact_variables_z3() {
9+
Z3_INSTALL_PATH="$(brew --cellar z3)/${Z3_VERSION}"
10+
}
11+
12+
install_build_dependencies_z3() {
13+
return 0
14+
}

0 commit comments

Comments
 (0)