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

Author: misonijnik

.cirrus.yml

@@ -1,16 +1,15 @@
 task:
   freebsd_instance:
     matrix:
-      - image_family: freebsd-13-2-snap
-      - image_family: freebsd-14-0-snap
+      - image_family: freebsd-15-0-snap
   deps_script:
     - sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf
     - env ASSUME_ALWAYS_YES=yes pkg update -f
     - 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
   build_script:
     - mkdir build
     - cd build
-    - 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 ..
+    - 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 ..
     - gmake
   test_script:
     - sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg

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

@@ -24,7 +24,8 @@ env:
   ENABLE_OPTIMIZED: 1
   ENABLE_DEBUG: 1
   ENABLE_WARNINGS_AS_ERRORS: ${{ github.event_name == 'workflow_dispatch' && inputs.warnings_as_errors || 1}}
-  GTEST_VERSION: 1.11.0
+  ENABLE_FP_RUNTIME: 1
+  GTEST_VERSION: 1.16.0
   KLEE_RUNTIME_BUILD: "Debug+Asserts"
   LLVM_VERSION: 11
   MINISAT_VERSION: "master"
@@ -43,7 +44,7 @@ env:
 
 jobs:
   Linux:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     strategy:
       matrix:
         name: [
@@ -160,7 +161,9 @@ jobs:
     env:
       LLVM_VERSION: 14
       BASE: /tmp
-      SOLVERS: STP
+      SOLVERS: Z3
+      Z3_VERSION: 4.14.1
+      ENABLE_FP_RUNTIME: 0
       UCLIBC_VERSION: 0
       USE_TCMALLOC: 0
       USE_LIBCXX: 0

.github/workflows/build.yaml

@@ -6,23 +6,24 @@ on:
 
 jobs:
   push_to_registry:
-    name: Push Docker Image to Docker Hub
+    name: Push Docker Image to Github Registry
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
         uses: actions/checkout@v3
 
-      - name: Log in to Docker Hub
+      - name: Log in to Github Registry
         uses: docker/login-action@f4ef78c080cd8ba55a85445d5b36e214a81df20a
         with:
-          username: ${{ secrets.DOCKER_USERNAME }}
-          password: ${{ secrets.DOCKER_PASSWORD }}
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GH_REGISTRY }}
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
         uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7
         with:
-          images: klee/klee
+          images: ghcr.io/unittestbot/klee/klee
 
       - name: Build and push Docker image
         uses: docker/build-push-action@3b5e8027fcad23fda98b2e3ac259d8d67585f671
@@ -31,4 +32,4 @@ jobs:
           file: ./Dockerfile
           push: true
           tags: ${{ steps.meta.outputs.tags }}
-          labels: ${{ steps.meta.outputs.labels }}
+          labels: ${{ steps.meta.outputs.labels }}

.github/workflows/docker_release_push.yml

@@ -1,33 +1,40 @@
-FROM ghcr.io/klee/llvm:130_O_D_A_ubuntu_jammy-20230126 as llvm_base
-FROM ghcr.io/klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_base
-FROM ghcr.io/klee/uclibc:klee_uclibc_v1.3_130_ubuntu_jammy-20230126 as uclibc_base
-FROM ghcr.io/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 as tcmalloc_base
-FROM ghcr.io/klee/stp:2.3.3_ubuntu_jammy-20230126 as stp_base
-FROM ghcr.io/klee/z3:4.8.15_ubuntu_jammy-20230126 as z3_base
-FROM ghcr.io/klee/libcxx:130_ubuntu_jammy-20230126 as libcxx_base
-FROM ghcr.io/klee/sqlite:3400100_ubuntu_jammy-20230126 as sqlite3_base
-FROM llvm_base as intermediate
+FROM ghcr.io/unittestbot/klee/llvm:140_O_D_A_ubuntu_jammy-20230126 AS llvm_base
+FROM ghcr.io/unittestbot/klee/gtest:1.16.0_ubuntu_jammy-20230126 AS gtest_base
+FROM ghcr.io/unittestbot/klee/uclibc:klee_uclibc_v1.4_140_ubuntu_jammy-20230126 AS uclibc_base
+FROM ghcr.io/unittestbot/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 AS tcmalloc_base
+FROM ghcr.io/unittestbot/klee/stp:2.3.3_ubuntu_jammy-20230126 AS stp_base
+FROM ghcr.io/unittestbot/klee/z3:4.8.15_ubuntu_jammy-20230126 AS z3_base
+FROM ghcr.io/unittestbot/klee/bitwuzla:0.7.0_ubuntu_jammy-20230126 AS bitwuzla_base
+FROM ghcr.io/unittestbot/klee/libcxx:140_ubuntu_jammy-20230126 AS libcxx_base
+FROM ghcr.io/unittestbot/klee/sqlite:3400100_ubuntu_jammy-20230126 AS sqlite3_base
+FROM ghcr.io/unittestbot/klee/immer:v0.8.1_ubuntu_jammy-20230126 AS immer_base
+FROM ghcr.io/unittestbot/klee/json:v3.11.3_ubuntu_jammy-20230126 AS json_base
+FROM llvm_base AS intermediate
 COPY --from=gtest_base /tmp /tmp/
 COPY --from=uclibc_base /tmp /tmp/
 COPY --from=tcmalloc_base /tmp /tmp/
 COPY --from=stp_base /tmp /tmp/
 COPY --from=z3_base /tmp /tmp/
+COPY --from=bitwuzla_base /tmp /tmp/
 COPY --from=libcxx_base /tmp /tmp/
 COPY --from=sqlite3_base /tmp /tmp/
+COPY --from=immer_base /tmp /tmp/
+COPY --from=json_base /tmp /tmp/
 ENV COVERAGE=0
 ENV USE_TCMALLOC=1
 ENV BASE=/tmp
 ENV BUILD_SUFFIX="default"
-ENV LLVM_VERSION=13.0
+ENV LLVM_VERSION=14
 ENV ENABLE_DOXYGEN=1
 ENV ENABLE_OPTIMIZED=1
 ENV ENABLE_DEBUG=1
 ENV DISABLE_ASSERTIONS=0
 ENV ENABLE_WARNINGS_AS_ERRORS=1
+ENV ENABLE_FP_RUNTIME=1
 ENV REQUIRES_RTTI=0
-ENV SOLVERS=STP:Z3
-ENV GTEST_VERSION=1.11.0
-ENV UCLIBC_VERSION=klee_uclibc_v1.3
+ENV SOLVERS=BITWUZLA:Z3:STP
+ENV GTEST_VERSION=1.16.0
+ENV UCLIBC_VERSION=klee_uclibc_v1.4
 ENV TCMALLOC_VERSION=2.9.1
 ENV SANITIZER_BUILD=
 ENV STP_VERSION=2.3.3
@@ -37,8 +44,9 @@ ENV USE_LIBCXX=1
 ENV KLEE_RUNTIME_BUILD="Debug+Asserts"
 ENV SQLITE_VERSION=3400100
 ENV JSON_VERSION=v3.11.3
+ENV BITWUZLA_VERSION=0.7.0
 ENV IMMER_VERSION=v0.8.1
-LABEL maintainer="KLEE Developers"
+LABEL maintainer="KLEEF Developers"
 
 # TODO remove adding sudo package
 # 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
     sudo rm -rf /var/lib/apt/lists/*
 
 
-ENV PATH="$PATH:/tmp/llvm-130-install_O_D_A/bin:/home/klee/klee_build/bin:/home/klee/.local/bin"
+ENV PATH="$PATH:/tmp/llvm-140-install_O_D_A/bin:/home/klee/klee_build/bin:/home/klee/.local/bin"
 ENV BASE=/tmp
 # Add path to local LLVM installation - let system install precede local install
 RUN /bin/bash -c 'echo "export \"PATH=$PATH:$(cd ${BASE}/llvm-*-install*/bin/ && pwd)\" >> /home/klee/.bashrc"'

Dockerfile

@@ -20,6 +20,7 @@ KLEE_RUNTIME_BUILD="Release"
 COVERAGE=0
 ENABLE_DOXYGEN=0
 USE_TCMALLOC=0
+ENABLE_FP_RUNTIME=1
 TCMALLOC_VERSION=2.9.1
 USE_LIBCXX=1
 # Also required despite not being mentioned in the guide
@@ -71,4 +72,4 @@ else
 fi
 done
 
-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
+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

build.sh

@@ -2528,8 +2528,9 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       uint64_t size = 0; // total size of variadic arguments
       bool requires16ByteAlignment = false;
 
-      uint64_t offsets[callingArgs]; // offsets of variadic arguments
-      uint64_t argWidth;             // width of current variadic argument
+      std::vector<uint64_t> offsets;
+      offsets.reserve(callingArgs); // offsets of variadic arguments
+      uint64_t argWidth;            // width of current variadic argument
 
       const CallBase &cb = cast<CallBase>(*i);
       for (unsigned k = funcArgs; k < callingArgs; k++) {

lib/Core/Executor.cpp

@@ -1,14 +1,13 @@
 setup_build_variables_gtest() {
-  GTEST_INSTALL_PATH="${BASE}/googletest-release-${GTEST_VERSION}"
+  GTEST_INSTALL_PATH="${BASE}/googletest-${GTEST_VERSION}"
   return 0
 }
 
 download_gtest() {
   cd "${BASE}" || exit 1
-  wget "https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip"
-  unzip -o "release-${GTEST_VERSION}.zip"
-  rm "release-${GTEST_VERSION}.zip"
-  touch "${GTEST_INSTALL_PATH}"/.is_installed
+  wget "https://github.com/google/googletest/archive/refs/tags/v${GTEST_VERSION}.zip"
+  unzip -o "v${GTEST_VERSION}.zip"
+  rm "v${GTEST_VERSION}.zip"
 }
 
 build_gtest() {
@@ -42,4 +41,4 @@ get_docker_config_id_gtest() {
     setup_build_variables_gtest
     echo "${GTEST_VERSION}"
   )
-}
+}

scripts/build/p-gtest.inc

@@ -91,12 +91,11 @@ fi
       echo "Z3"
       KLEE_Z3_CONFIGURE_OPTION=(
         "-DENABLE_SOLVER_Z3=TRUE"
-        "-DZ3_INCLUDE_DIRS=${Z3_INSTALL_PATH}/include"
-        "-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib/libz3.so"
       )
+      CMAKE_PREFIX_PATH+=("${Z3_INSTALL_PATH}")
       KLEE_FLOATING_POINT=(
-        "-DENABLE_FLOATING_POINT=TRUE"
-        "-DENABLE_FP_RUNTIME=TRUE"
+        "-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}"
+        "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"
       )
       ;;
     metasmt)
@@ -114,11 +113,10 @@ fi
       KLEE_BITWUZLA_CONFIGURE_OPTION=(
         "-DENABLE_SOLVER_BITWUZLA=TRUE"
       )
-      
       CMAKE_PREFIX_PATH+=("${BITWUZLA_INSTALL_PATH}")
       KLEE_FLOATING_POINT=(
-        "-DENABLE_FLOATING_POINT=TRUE"
-        "-DENABLE_FP_RUNTIME=TRUE"
+        "-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}"
+        "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"
       )
       echo "bitwuzla"
       ;;

scripts/build/p-klee.inc

@@ -1,13 +1,14 @@
-install_binary_artifact_z3 () {
-  set +e
-  brew install python@2
-  if [[ "X$?" != "X0" ]]; then
-     brew link --overwrite python@2
-  fi
-  set -e
+#!/usr/bin/env bash
+# shellcheck disable=SC2034
+
+install_binary_artifact_z3() {
   brew install z3
 }
 
-is_installed_z3() {
-    [[ -f "/usr/local/opt/z3/bin/z3" ]]
-}
+setup_artifact_variables_z3() {
+  Z3_INSTALL_PATH="$(brew --cellar z3)/${Z3_VERSION}"
+}
+
+install_build_dependencies_z3() {
+  return 0
+}

scripts/build/p-z3-osx.inc

@@ -7,6 +7,7 @@ required_variables_klee=(
   "USE_LIBCXX"
   "ENABLE_DOXYGEN"
   "ENABLE_WARNINGS_AS_ERRORS"
+  "ENABLE_FP_RUNTIME"
 )
 
 required_variables_check_klee() {
@@ -15,6 +16,7 @@ required_variables_check_klee() {
   check_bool "USE_LIBCXX"
   check_bool "ENABLE_DOXYGEN"
   check_bool "ENABLE_WARNINGS_AS_ERRORS"
+  check_bool "ENABLE_FP_RUNTIME"
 }
 
 # On which artifacts does KLEE depend on

scripts/build/v-klee.inc

@@ -78,6 +78,7 @@ int main() {
 // REQUIRES: bitwuzla
 // REQUIRES: not-asan
 // REQUIRES: not-msan
+// REQUIRES: not-ubsan
 // REQUIRES: not-darwin
 // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=60 --32 --debug --write-ktests %s 2>&1 | FileCheck %s
 // CHECK: KLEE: WARNING: 100.00% Reachable Reachable

test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c

@@ -1,6 +1,7 @@
 // REQUIRES: bitwuzla
 // REQUIRES: not-asan
 // REQUIRES: not-msan
+// REQUIRES: not-ubsan
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --strip-unwanted-calls --delete-dead-loops=false --emit-all-errors --mock-policy=all --use-forked-solver=false --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=16 --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=false --output-istats=false --use-sym-size-alloc=true --cex-cache-validity-cores --fp-runtime --x86FP-as-x87FP80 --symbolic-allocation-threshold=8192 --allocate-determ --allocate-determ-size=3072 --allocate-determ-start-address=0x00030000000 --mem-trigger-cof --use-alpha-equivalence=true --track-coverage=all --use-iterative-deepening-search=max-cycles --max-solver-time=5s --max-cycles-before-stuck=15 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --cover-on-the-fly=true --delay-cover-on-the-fly=27 --max-time=29 %t1.bc 2>&1 | FileCheck %s