From 2856db3b02e1e3437bdfee144f2dccbcd355f4f0 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 14:57:39 +0200 Subject: [PATCH 01/29] ci: Update docker release workflow --- .github/workflows/build-in-base-env.yml | 25 ------------------ .github/workflows/docker_release_push.yml | 9 ++++--- Dockerfile | 31 ++++++++++++++--------- 3 files changed, 24 insertions(+), 41 deletions(-) delete mode 100644 .github/workflows/build-in-base-env.yml diff --git a/.github/workflows/build-in-base-env.yml b/.github/workflows/build-in-base-env.yml deleted file mode 100644 index daf22bff94..0000000000 --- a/.github/workflows/build-in-base-env.yml +++ /dev/null @@ -1,25 +0,0 @@ -name: Build in UTBot base_env - -on: - pull_request: - branches: [utbot-main] - push: - branches: [utbot-main] - -jobs: - build: - runs-on: ubuntu-latest - container: - image: ghcr.io/unittestbot/utbotcpp/base_env:02-02-2022 - credentials: - username: ${{ github.actor }} - password: ${{ secrets.GITHUB_TOKEN }} - steps: - - name: Checkout repository - uses: actions/checkout@v2 - - name: Run build.sh - run: | - ./build.sh - - name: Run tests - run: | - cd build && ninja check diff --git a/.github/workflows/docker_release_push.yml b/.github/workflows/docker_release_push.yml index 7337e3d436..78b1224b4c 100644 --- a/.github/workflows/docker_release_push.yml +++ b/.github/workflows/docker_release_push.yml @@ -15,14 +15,15 @@ jobs: - name: Log in to Docker Hub uses: docker/login-action@f4ef78c080cd8ba55a85445d5b36e214a81df20a with: - username: ${{ secrets.DOCKER_USERNAME }} - password: ${{ secrets.DOCKER_PASSWORD }} + registry: ghcr.io + username: ${{ github.actor }} + password: ${{ secrets.GITHUB_TOKEN }} - name: Extract metadata (tags, labels) for Docker id: meta uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7 with: - images: klee/klee + images: 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 }} \ No newline at end of file + labels: ${{ steps.meta.outputs.labels }} diff --git a/Dockerfile b/Dockerfile index 7055a9d77b..1c4c4ff6e5 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,19 +1,25 @@ -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 ghcr.io/unittestbot/klee/llvm:140_O_D_A_ubuntu_jammy-20230126 as llvm_base +FROM ghcr.io/unittestbot/klee/gtest:1.11.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.3.1_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=binwuzla_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 @@ -25,9 +31,9 @@ ENV ENABLE_DEBUG=1 ENV DISABLE_ASSERTIONS=0 ENV ENABLE_WARNINGS_AS_ERRORS=1 ENV REQUIRES_RTTI=0 -ENV SOLVERS=STP:Z3 +ENV SOLVERS=BITWUZLA:Z3:STP ENV GTEST_VERSION=1.11.0 -ENV UCLIBC_VERSION=klee_uclibc_v1.3 +ENV UCLIBC_VERSION=klee_uclibc_v1.4 ENV TCMALLOC_VERSION=2.9.1 ENV SANITIZER_BUILD= ENV STP_VERSION=2.3.3 @@ -37,8 +43,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 +67,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"' From 3997ad582f8392328ff688aa522429d5425b3768 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:00:20 +0200 Subject: [PATCH 02/29] ci: Fix `freebsd` image version on cirrus --- .cirrus.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.cirrus.yml b/.cirrus.yml index f1244a2410..9727ae745d 100644 --- a/.cirrus.yml +++ b/.cirrus.yml @@ -1,8 +1,7 @@ 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 From d1688dcefd4a7ccc0aec2b370b80e1a2c65cf92c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:00:52 +0200 Subject: [PATCH 03/29] style: Fix typo --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 1c4c4ff6e5..f3739a978f 100644 --- a/Dockerfile +++ b/Dockerfile @@ -15,7 +15,7 @@ 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=binwuzla_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/ From 0141de12bab7748f4b9cab21f6ef28f0fb8685bc Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:07:39 +0200 Subject: [PATCH 04/29] ci: Pin ubuntu version set Z3 as a deafult solver fo macOS --- .github/workflows/build.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index 376929fb22..c3aa818c72 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -43,7 +43,7 @@ env: jobs: Linux: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 strategy: matrix: name: [ @@ -160,7 +160,7 @@ jobs: env: LLVM_VERSION: 14 BASE: /tmp - SOLVERS: STP + SOLVERS: Z3 UCLIBC_VERSION: 0 USE_TCMALLOC: 0 USE_LIBCXX: 0 From 63f87506e407dcf3a5cbfe8679aeb86719b35a18 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:11:10 +0200 Subject: [PATCH 05/29] chore: Update gtest version --- .github/workflows/build.yaml | 2 +- Dockerfile | 2 +- scripts/build/p-gtest.inc | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index c3aa818c72..e57eb732a7 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -24,7 +24,7 @@ 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 + GTEST_VERSION: 1.16.0 KLEE_RUNTIME_BUILD: "Debug+Asserts" LLVM_VERSION: 11 MINISAT_VERSION: "master" diff --git a/Dockerfile b/Dockerfile index f3739a978f..4f331a6e13 100644 --- a/Dockerfile +++ b/Dockerfile @@ -32,7 +32,7 @@ ENV DISABLE_ASSERTIONS=0 ENV ENABLE_WARNINGS_AS_ERRORS=1 ENV REQUIRES_RTTI=0 ENV SOLVERS=BITWUZLA:Z3:STP -ENV GTEST_VERSION=1.11.0 +ENV GTEST_VERSION=1.16.0 ENV UCLIBC_VERSION=klee_uclibc_v1.4 ENV TCMALLOC_VERSION=2.9.1 ENV SANITIZER_BUILD= diff --git a/scripts/build/p-gtest.inc b/scripts/build/p-gtest.inc index d4a2d498d5..2366191df5 100644 --- a/scripts/build/p-gtest.inc +++ b/scripts/build/p-gtest.inc @@ -5,10 +5,10 @@ setup_build_variables_gtest() { 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" + mv "googletest-${GTEST_VERSION}" "googletest-release-${GTEST_VERSION}" } build_gtest() { @@ -42,4 +42,4 @@ get_docker_config_id_gtest() { setup_build_variables_gtest echo "${GTEST_VERSION}" ) -} \ No newline at end of file +} From 47eb81561f9f5bcba681c4c99479397e202e65c9 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:12:28 +0200 Subject: [PATCH 06/29] ci: Update llvm version in Dockerfile --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 4f331a6e13..151ccb288f 100644 --- a/Dockerfile +++ b/Dockerfile @@ -24,7 +24,7 @@ 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 From 674c15cd1c9489892ae6ce455f54ae7272a1fc8c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:33:01 +0200 Subject: [PATCH 07/29] fix: Prefer new naming of github releases --- scripts/build/p-gtest.inc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/build/p-gtest.inc b/scripts/build/p-gtest.inc index 2366191df5..da274a2f86 100644 --- a/scripts/build/p-gtest.inc +++ b/scripts/build/p-gtest.inc @@ -1,5 +1,5 @@ setup_build_variables_gtest() { - GTEST_INSTALL_PATH="${BASE}/googletest-release-${GTEST_VERSION}" + GTEST_INSTALL_PATH="${BASE}/googletest-${GTEST_VERSION}" return 0 } @@ -8,7 +8,6 @@ download_gtest() { wget "https://github.com/google/googletest/archive/refs/tags/v${GTEST_VERSION}.zip" unzip -o "v${GTEST_VERSION}.zip" rm "v${GTEST_VERSION}.zip" - mv "googletest-${GTEST_VERSION}" "googletest-release-${GTEST_VERSION}" } build_gtest() { From 9642b2bf5616f61366018b2f93539525653437d3 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:52:27 +0200 Subject: [PATCH 08/29] fix: Fix build z3 for macOS --- .github/workflows/build.yaml | 1 + scripts/build/p-z3-osx.inc | 18 ++++++------------ 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index e57eb732a7..cbfaa44b0d 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -161,6 +161,7 @@ jobs: LLVM_VERSION: 14 BASE: /tmp SOLVERS: Z3 + Z3_VERSION: 4.14.1 UCLIBC_VERSION: 0 USE_TCMALLOC: 0 USE_LIBCXX: 0 diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index bce11aabad..72b033d85e 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -1,13 +1,7 @@ -install_binary_artifact_z3 () { - set +e - brew install python@2 - if [[ "X$?" != "X0" ]]; then - brew link --overwrite python@2 - fi - set -e - brew install z3 +download_z3() { + mkdir -p "${Z3_SRC_PATH}" + cd "${Z3_SRC_PATH}" + wget "https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}-arm64-osx.zip" + unzip -o "z3-${Z3_VERSION}-arm64-osx.zip" + rm "z3-${Z3_VERSION}-arm64-osx.zip" } - -is_installed_z3() { - [[ -f "/usr/local/opt/z3/bin/z3" ]] -} \ No newline at end of file From 35f67a848f5be8cf74e4c80d10c2a298548c2f52 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 15:57:54 +0200 Subject: [PATCH 09/29] fix: Maybe? --- scripts/build/p-z3-osx.inc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index 72b033d85e..32f081a519 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -5,3 +5,10 @@ download_z3() { unzip -o "z3-${Z3_VERSION}-arm64-osx.zip" rm "z3-${Z3_VERSION}-arm64-osx.zip" } + +#!/usr/bin/env bash +install_build_dependencies_z3() { + # Install essential dependency + # Ignore if already installed + brew install wget || /usr/bin/true +} From e36f03df26ce5c5987c88b99c1df54393d0fb2f8 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 16:00:35 +0200 Subject: [PATCH 10/29] fix(scripts): Fix ShellCheck warning --- scripts/build/p-z3-osx.inc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index 32f081a519..a4010ddff5 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -10,5 +10,5 @@ download_z3() { install_build_dependencies_z3() { # Install essential dependency # Ignore if already installed - brew install wget || /usr/bin/true + brew install wget || exit } From edbd7efacfc24c187e4aaf81c6abb217c2180bbf Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 16:02:46 +0200 Subject: [PATCH 11/29] fix(scripts): Fix URL to z3 binaries for osx --- scripts/build/p-z3-osx.inc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index a4010ddff5..b3fb4b9e22 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -1,7 +1,7 @@ download_z3() { mkdir -p "${Z3_SRC_PATH}" cd "${Z3_SRC_PATH}" - wget "https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}-arm64-osx.zip" + wget "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" unzip -o "z3-${Z3_VERSION}-arm64-osx.zip" rm "z3-${Z3_VERSION}-arm64-osx.zip" } From e6e205dc8e7e618d6c96d0989f809f1ee12e0969 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 16:06:04 +0200 Subject: [PATCH 12/29] fix(scripts): --- scripts/build/p-z3-osx.inc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index b3fb4b9e22..fdde78b718 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -2,8 +2,8 @@ download_z3() { mkdir -p "${Z3_SRC_PATH}" cd "${Z3_SRC_PATH}" wget "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" - unzip -o "z3-${Z3_VERSION}-arm64-osx.zip" - rm "z3-${Z3_VERSION}-arm64-osx.zip" + unzip -o "z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" + rm "z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" } #!/usr/bin/env bash From f76a5b50f336d5241d7965477022459d0b618d85 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 16:15:54 +0200 Subject: [PATCH 13/29] fix(scripts): Install z3 in the rigth path --- scripts/build/p-z3-osx.inc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index fdde78b718..1d83518715 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -1,6 +1,6 @@ -download_z3() { - mkdir -p "${Z3_SRC_PATH}" - cd "${Z3_SRC_PATH}" +install_binary_artifact_z3() { + mkdir -p "${Z3_INSTALL_PATH}" + cd "${Z3_INSTALL_PATH}" wget "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" unzip -o "z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" rm "z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" From bb5f5b1154d24e855321f6798ffcd116da0278b8 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 1 May 2025 16:20:35 +0200 Subject: [PATCH 14/29] fix(scripts): Install z3 in the rigth path --- scripts/build/p-z3-osx.inc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index 1d83518715..daebbb7be2 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -1,4 +1,6 @@ install_binary_artifact_z3() { + local Z3_SUFFIX="${SANITIZER_SUFFIX}" + local Z3_INSTALL_PATH="${BASE}/z3-${Z3_VERSION}-install${Z3_SUFFIX}" mkdir -p "${Z3_INSTALL_PATH}" cd "${Z3_INSTALL_PATH}" wget "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" @@ -6,6 +8,11 @@ install_binary_artifact_z3() { rm "z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" } +setup_artifact_variables_llvm() { + Z3_SUFFIX="${SANITIZER_SUFFIX}" + Z3_INSTALL_PATH="${BASE}/z3-${Z3_VERSION}-install${Z3_SUFFIX}" +} + #!/usr/bin/env bash install_build_dependencies_z3() { # Install essential dependency From 90c718314800395af6b4c2a8bb5c70ebbd665b16 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 4 May 2025 15:33:52 +0200 Subject: [PATCH 15/29] ci(scripts): Try to find the right wat to use Z3 on macOS --- scripts/build/p-klee.inc | 3 ++- scripts/build/p-z3-osx.inc | 19 +++++-------------- 2 files changed, 7 insertions(+), 15 deletions(-) diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc index 89d1b5f0df..216859856a 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -92,7 +92,8 @@ fi KLEE_Z3_CONFIGURE_OPTION=( "-DENABLE_SOLVER_Z3=TRUE" "-DZ3_INCLUDE_DIRS=${Z3_INSTALL_PATH}/include" - "-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib/libz3.so" + "-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib" + // TODO: Set the right path to the libraries for macOS ) KLEE_FLOATING_POINT=( "-DENABLE_FLOATING_POINT=TRUE" diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index daebbb7be2..edb7f8b9f6 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -1,21 +1,12 @@ +#!/usr/bin/env bash install_binary_artifact_z3() { - local Z3_SUFFIX="${SANITIZER_SUFFIX}" - local Z3_INSTALL_PATH="${BASE}/z3-${Z3_VERSION}-install${Z3_SUFFIX}" - mkdir -p "${Z3_INSTALL_PATH}" - cd "${Z3_INSTALL_PATH}" - wget "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" - unzip -o "z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" - rm "z3-${Z3_VERSION}-arm64-osx-13.7.4.zip" + brew install z3 } -setup_artifact_variables_llvm() { - Z3_SUFFIX="${SANITIZER_SUFFIX}" - Z3_INSTALL_PATH="${BASE}/z3-${Z3_VERSION}-install${Z3_SUFFIX}" +setup_artifact_variables_z3() { + Z3_INSTALL_PATH="$(brew --cellar z3)/${Z3_VERSION}" } -#!/usr/bin/env bash install_build_dependencies_z3() { - # Install essential dependency - # Ignore if already installed - brew install wget || exit + return 0 } From 57e2e9f69c4fbc498b0148320c3601a2abeca081 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 4 May 2025 15:54:16 +0200 Subject: [PATCH 16/29] fix(scripts): Try to find the right wat to use Z3 on macOS --- scripts/build/p-klee.inc | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc index 216859856a..c5999f3125 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -91,10 +91,8 @@ fi echo "Z3" KLEE_Z3_CONFIGURE_OPTION=( "-DENABLE_SOLVER_Z3=TRUE" - "-DZ3_INCLUDE_DIRS=${Z3_INSTALL_PATH}/include" - "-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib" - // TODO: Set the right path to the libraries for macOS ) + CMAKE_PREFIX_PATH+=("${Z3_INSTALL_PATH}") KLEE_FLOATING_POINT=( "-DENABLE_FLOATING_POINT=TRUE" "-DENABLE_FP_RUNTIME=TRUE" @@ -115,7 +113,6 @@ fi KLEE_BITWUZLA_CONFIGURE_OPTION=( "-DENABLE_SOLVER_BITWUZLA=TRUE" ) - CMAKE_PREFIX_PATH+=("${BITWUZLA_INSTALL_PATH}") KLEE_FLOATING_POINT=( "-DENABLE_FLOATING_POINT=TRUE" From d53996f3d104740a24529d09a557b6d81289fd46 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 4 May 2025 16:06:46 +0200 Subject: [PATCH 17/29] ci: Disable FP warning --- scripts/build/p-z3-osx.inc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc index edb7f8b9f6..5abaadcb5d 100644 --- a/scripts/build/p-z3-osx.inc +++ b/scripts/build/p-z3-osx.inc @@ -1,4 +1,6 @@ #!/usr/bin/env bash +# shellcheck disable=SC2034 + install_binary_artifact_z3() { brew install z3 } From fa8fad933e11c623ae7f8194711fbcae362f7297 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 4 May 2025 16:24:20 +0200 Subject: [PATCH 18/29] feat(build): Add `ENABLE_FP_RUNTIME` option --- .github/workflows/build.yaml | 2 ++ Dockerfile | 1 + build.sh | 3 ++- scripts/build/p-klee.inc | 8 ++++---- scripts/build/v-klee.inc | 2 ++ 5 files changed, 11 insertions(+), 5 deletions(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index cbfaa44b0d..433923b8b5 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -24,6 +24,7 @@ env: ENABLE_OPTIMIZED: 1 ENABLE_DEBUG: 1 ENABLE_WARNINGS_AS_ERRORS: ${{ github.event_name == 'workflow_dispatch' && inputs.warnings_as_errors || 1}} + ENABLE_FP_RUNTIME: 1 GTEST_VERSION: 1.16.0 KLEE_RUNTIME_BUILD: "Debug+Asserts" LLVM_VERSION: 11 @@ -162,6 +163,7 @@ jobs: BASE: /tmp SOLVERS: Z3 Z3_VERSION: 4.14.1 + ENABLE_FP_RUNTIME: 0 UCLIBC_VERSION: 0 USE_TCMALLOC: 0 USE_LIBCXX: 0 diff --git a/Dockerfile b/Dockerfile index 151ccb288f..0b279d8a54 100644 --- a/Dockerfile +++ b/Dockerfile @@ -30,6 +30,7 @@ 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=BITWUZLA:Z3:STP ENV GTEST_VERSION=1.16.0 diff --git a/build.sh b/build.sh index 33cf59ce8c..0c79bb5a2d 100755 --- a/build.sh +++ b/build.sh @@ -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 diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc index c5999f3125..bf20129987 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -94,8 +94,8 @@ fi ) 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) @@ -115,8 +115,8 @@ fi ) 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" ;; diff --git a/scripts/build/v-klee.inc b/scripts/build/v-klee.inc index 4a1107e18e..b653419f1b 100644 --- a/scripts/build/v-klee.inc +++ b/scripts/build/v-klee.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 From 697560732c926ef1f846a07a8abc9148111a2eed Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 4 May 2025 16:52:56 +0200 Subject: [PATCH 19/29] fix: Fix typo --- scripts/build/p-klee.inc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc index bf20129987..b00cf714c3 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -95,7 +95,7 @@ fi CMAKE_PREFIX_PATH+=("${Z3_INSTALL_PATH}") KLEE_FLOATING_POINT=( "-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}" - "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"" + "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}" ) ;; metasmt) From 1d92f55aaabe2ba2a091fefa79617ecd6637413b Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 4 May 2025 16:54:45 +0200 Subject: [PATCH 20/29] fix: Fix typo --- scripts/build/p-klee.inc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc index b00cf714c3..5be1cd292e 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -115,8 +115,8 @@ fi ) CMAKE_PREFIX_PATH+=("${BITWUZLA_INSTALL_PATH}") KLEE_FLOATING_POINT=( - "-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}"" - "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"" + "-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}" + "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}" ) echo "bitwuzla" ;; From c9355ed5f46bed6796ec6ee2ed5ed23069ba707d Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 4 May 2025 23:08:21 +0200 Subject: [PATCH 21/29] style: Use a vector instead of an array as a variable length container --- lib/Core/Executor.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b06d2fee5b..79f7e7ce6f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -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 offsets; + offsets.reserve(callingArgs); // offsets of variadic arguments + uint64_t argWidth; // width of current variadic argument const CallBase &cb = cast(*i); for (unsigned k = funcArgs; k < callingArgs; k++) { From d7d1122229a7c184f6b2f38a72801c724421c617 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 01:09:09 +0300 Subject: [PATCH 22/29] ci: Update docker_release_push.yml --- .github/workflows/docker_release_push.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/docker_release_push.yml b/.github/workflows/docker_release_push.yml index 78b1224b4c..199d91fdcb 100644 --- a/.github/workflows/docker_release_push.yml +++ b/.github/workflows/docker_release_push.yml @@ -33,3 +33,5 @@ jobs: push: true tags: ${{ steps.meta.outputs.tags }} labels: ${{ steps.meta.outputs.labels }} + secrets: | + GIT_AUTH_TOKEN=${{ secrets.GH_REGISTRY }} From 37e6b85ddd0032e92a6deddaf2d54b0c7597a601 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 11:03:52 +0200 Subject: [PATCH 23/29] ci(release): Update registry --- .github/workflows/docker_release_push.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker_release_push.yml b/.github/workflows/docker_release_push.yml index 199d91fdcb..a89ed83bf2 100644 --- a/.github/workflows/docker_release_push.yml +++ b/.github/workflows/docker_release_push.yml @@ -15,7 +15,7 @@ jobs: - name: Log in to Docker Hub uses: docker/login-action@f4ef78c080cd8ba55a85445d5b36e214a81df20a with: - registry: ghcr.io + registry: ghcr.io/unittestbot/klee username: ${{ github.actor }} password: ${{ secrets.GITHUB_TOKEN }} @@ -23,7 +23,7 @@ jobs: id: meta uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7 with: - images: unittestbot/klee/klee + images: klee - name: Build and push Docker image uses: docker/build-push-action@3b5e8027fcad23fda98b2e3ac259d8d67585f671 From 369e01ed17dea74d88582d5e815ab9d384ae0763 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 11:05:38 +0200 Subject: [PATCH 24/29] ci(cirrus): Update cmake parameters --- .cirrus.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.cirrus.yml b/.cirrus.yml index 9727ae745d..6de1dc52cf 100644 --- a/.cirrus.yml +++ b/.cirrus.yml @@ -9,7 +9,7 @@ task: 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 From 35fd181a1aa950660a4c221c95e55186e30030bf Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 11:09:22 +0200 Subject: [PATCH 25/29] chore(docker): Update Dockerfile --- Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Dockerfile b/Dockerfile index 0b279d8a54..6ce15753f7 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,10 +1,10 @@ FROM ghcr.io/unittestbot/klee/llvm:140_O_D_A_ubuntu_jammy-20230126 as llvm_base -FROM ghcr.io/unittestbot/klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_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.3.1_ubuntu_jammy-20230126 as bitwuzla_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 8afd44928e4ecaadd6b6067cf4ea2660f23e5bd1 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 11:30:02 +0200 Subject: [PATCH 26/29] ci(release): Update registry --- .github/workflows/docker_release_push.yml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/.github/workflows/docker_release_push.yml b/.github/workflows/docker_release_push.yml index a89ed83bf2..4dc0f7ee66 100644 --- a/.github/workflows/docker_release_push.yml +++ b/.github/workflows/docker_release_push.yml @@ -17,13 +17,13 @@ jobs: with: registry: ghcr.io/unittestbot/klee username: ${{ github.actor }} - password: ${{ secrets.GITHUB_TOKEN }} + password: ${{ secrets.GH_REGISTRY }} - name: Extract metadata (tags, labels) for Docker id: meta uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7 with: - images: klee + images: unittestbot/klee - name: Build and push Docker image uses: docker/build-push-action@3b5e8027fcad23fda98b2e3ac259d8d67585f671 @@ -33,5 +33,3 @@ jobs: push: true tags: ${{ steps.meta.outputs.tags }} labels: ${{ steps.meta.outputs.labels }} - secrets: | - GIT_AUTH_TOKEN=${{ secrets.GH_REGISTRY }} From 7e114e42ffdc328df939c87bcc3d737d000ba703 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 11:31:50 +0200 Subject: [PATCH 27/29] chore(docker): Update Dockerfile --- Dockerfile | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Dockerfile b/Dockerfile index 6ce15753f7..2ef2629fd5 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,15 +1,15 @@ -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 +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/ From 8500e7837a2a1337b79c545e71cb28219c8e8acd Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 11:52:06 +0200 Subject: [PATCH 28/29] ci(release): Update registry --- .github/workflows/docker_release_push.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/docker_release_push.yml b/.github/workflows/docker_release_push.yml index 4dc0f7ee66..31d05363c9 100644 --- a/.github/workflows/docker_release_push.yml +++ b/.github/workflows/docker_release_push.yml @@ -6,16 +6,16 @@ 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: - registry: ghcr.io/unittestbot/klee + registry: ghcr.io username: ${{ github.actor }} password: ${{ secrets.GH_REGISTRY }} @@ -23,7 +23,7 @@ jobs: id: meta uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7 with: - images: unittestbot/klee + images: ghcr.io/unittestbot/klee/klee - name: Build and push Docker image uses: docker/build-push-action@3b5e8027fcad23fda98b2e3ac259d8d67585f671 From aa1db9fb0edc6ba9820319234a746a17b0d4cd27 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 5 May 2025 12:34:44 +0200 Subject: [PATCH 29/29] test: Require `not-ubsan` for a couple of tests with 32-bit binaries --- test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c | 1 + test/Solver/sina2f.c | 1 + 2 files changed, 2 insertions(+) diff --git a/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c b/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c index dfb550f73e..7596f62d60 100644 --- a/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c +++ b/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c @@ -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 diff --git a/test/Solver/sina2f.c b/test/Solver/sina2f.c index c732bf2ddb..93e3ecbb69 100644 --- a/test/Solver/sina2f.c +++ b/test/Solver/sina2f.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