diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index bbae4714b18..f9f26f6c1dc 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -29,7 +29,8 @@ env: USE_LIBCXX: 1 Z3_VERSION: 4.8.15 SQLITE_VERSION: 3400100 - BITWUZLA_VERSION: 0.2.0 + BITWUZLA_VERSION: main + BITWUZLA_COMMIT: 80ef7cd803e1c71b5939c3eb951f1736388f7090 jobs: Linux: diff --git a/build.sh b/build.sh index fdab7a66839..150cb6dcff2 100755 --- a/build.sh +++ b/build.sh @@ -50,6 +50,7 @@ Z3_VERSION=4.8.15 STP_VERSION=2.3.3 MINISAT_VERSION=master -BITWUZLA_VERSION=0.2.0 +BITWUZLA_VERSION=main +BITWUZLA_COMMIT=80ef7cd803e1c71b5939c3eb951f1736388f7090 -BASE="$BASE" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC 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 ./scripts/build/build.sh klee --install-system-deps +BASE="$BASE" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC 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 BITWUZLA_COMMIT=$BITWUZLA_COMMIT SQLITE_VERSION=$SQLITE_VERSION ./scripts/build/build.sh klee --install-system-deps diff --git a/cmake/find_bitwuzla.cmake b/cmake/find_bitwuzla.cmake index 1e6fb952192..82e9866dccc 100644 --- a/cmake/find_bitwuzla.cmake +++ b/cmake/find_bitwuzla.cmake @@ -6,8 +6,8 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# -include(FindPkgConfig) +find_package (PkgConfig REQUIRED) pkg_check_modules(BITWUZLA IMPORTED_TARGET bitwuzla) # Set the default so that if the following is true: @@ -33,9 +33,9 @@ if (ENABLE_SOLVER_BITWUZLA) set(ENABLE_BITWUZLA 1) # For config.h list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${BITWUZLA_INCLUDE_DIRS}) - list(APPEND KLEE_SOLVER_LIBRARIES ${BITWUZLA_LIBRARIES}) + list(APPEND KLEE_SOLVER_LIBRARIES ${BITWUZLA_LINK_LIBRARIES}) list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${BITWUZLA_INCLUDE_DIRS}) - list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${BITWUZLA_LIBRARIES}) + list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${BITWUZLA_LINK_LIBRARIES}) else() message(FATAL_ERROR "Bitwuzla not found.") diff --git a/lib/Solver/BitwuzlaSolver.cpp b/lib/Solver/BitwuzlaSolver.cpp index f3d442a1941..23a7e4ca65e 100644 --- a/lib/Solver/BitwuzlaSolver.cpp +++ b/lib/Solver/BitwuzlaSolver.cpp @@ -65,6 +65,20 @@ void signal_handler(int signum) { interrupted = true; } namespace klee { +class BitwuzlaTerminator : public bitwuzla::Terminator { +private: + uint64_t time_limit_micro; + time::Point start; + + bool _isTimeout = false; + +public: + BitwuzlaTerminator(uint64_t); + bool terminate() override; + + bool isTimeout() const { return _isTimeout; } +}; + BitwuzlaTerminator::BitwuzlaTerminator(uint64_t time_limit_micro) : Terminator(), time_limit_micro(time_limit_micro), start(time::getWallTime()) {} diff --git a/lib/Solver/BitwuzlaSolver.h b/lib/Solver/BitwuzlaSolver.h index 5293ad3c797..9d6e35ebd35 100644 --- a/lib/Solver/BitwuzlaSolver.h +++ b/lib/Solver/BitwuzlaSolver.h @@ -1,25 +1,10 @@ #ifndef BITWUZLASOLVER_H_ #define BITWUZLASOLVER_H_ -#include "bitwuzla/cpp/bitwuzla.h" #include "klee/Solver/Solver.h" namespace klee { -class BitwuzlaTerminator : public bitwuzla::Terminator { -private: - uint64_t time_limit_micro; - time::Point start; - - bool _isTimeout = false; - -public: - BitwuzlaTerminator(uint64_t); - bool terminate() override; - - bool isTimeout() const { return _isTimeout; } -}; - /// BitwuzlaSolver - A complete solver based on Bitwuzla class BitwuzlaSolver : public Solver { public: diff --git a/scripts/build/common-functions b/scripts/build/common-functions index c964419f604..c65e422257c 100644 --- a/scripts/build/common-functions +++ b/scripts/build/common-functions @@ -14,6 +14,11 @@ function git_clone_or_update() { git checkout "${branch}" fi fi + + if [[ $# -ge 4 ]]; then + cd "$destination" + git checkout "$4" + fi } function get_git_hash() { diff --git a/scripts/build/p-bitwuzla-linux-ubuntu.inc b/scripts/build/p-bitwuzla-linux-ubuntu.inc index 39a838e8171..60478cca0ac 100644 --- a/scripts/build/p-bitwuzla-linux-ubuntu.inc +++ b/scripts/build/p-bitwuzla-linux-ubuntu.inc @@ -13,6 +13,7 @@ install_build_dependencies_bitwuzla() { #Install essential dependencies with_sudo apt -y --no-install-recommends install "${dependencies[@]}" + with_sudo pip3 install --user meson base_path="$(python3 -m site --user-base)" export PATH="$PATH:${base_path}/bin" diff --git a/scripts/build/p-bitwuzla.inc b/scripts/build/p-bitwuzla.inc index 437363245e3..57b23724353 100644 --- a/scripts/build/p-bitwuzla.inc +++ b/scripts/build/p-bitwuzla.inc @@ -2,6 +2,7 @@ # Variables that any artifact of this package might depend on setup_build_variables_bitwuzla() { BITWUZLA_BUILD_PATH="${BASE}/bitwuzla-${BITWUZLA_VERSION}-build" + BITWUZLA_INSTALL_PATH="${BASE}/bitwuzla-${BITWUZLA_VERSION}-install" bitwuzla_url="https://github.com/bitwuzla/bitwuzla.git" return 0 @@ -10,15 +11,15 @@ setup_build_variables_bitwuzla() { download_bitwuzla() { source "${DIR}/common-functions" # Download Bitwuzla - git_clone_or_update "${bitwuzla_url}" "${BASE}/bitwuzla-${BITWUZLA_VERSION}" "${BITWUZLA_VERSION}" + git_clone_or_update "${bitwuzla_url}" "${BASE}/bitwuzla-${BITWUZLA_VERSION}" "${BITWUZLA_VERSION}" "${BITWUZLA_COMMIT}" } build_bitwuzla() { pushd "${BASE}/bitwuzla-${BITWUZLA_VERSION}" - ./configure.py --build-dir "${BITWUZLA_BUILD_PATH}" + ./configure.py --build-dir "${BITWUZLA_BUILD_PATH}" --prefix "${BITWUZLA_INSTALL_PATH}" popd cd "${BITWUZLA_BUILD_PATH}" || return 1 - yes n | with_sudo ninja install + yes n | ninja install touch "${BITWUZLA_BUILD_PATH}/.bitwuzla_installed" } diff --git a/scripts/build/p-klee-linux-ubuntu.inc b/scripts/build/p-klee-linux-ubuntu.inc index 8bf39a199b3..d687a549ee5 100644 --- a/scripts/build/p-klee-linux-ubuntu.inc +++ b/scripts/build/p-klee-linux-ubuntu.inc @@ -28,6 +28,9 @@ install_build_dependencies_klee() { with_sudo apt-get -y --no-install-recommends install "${dependencies[@]}" + with_sudo apt-get update -y + with_sudo apt-get -y --no-install-recommends install pkg-config cmake-data + pip3 install --user lit pip3 install --user tabulate base_path="$(python3 -m site --user-base)" diff --git a/scripts/build/p-klee-osx.inc b/scripts/build/p-klee-osx.inc index 0561e28f68c..dead72472e0 100644 --- a/scripts/build/p-klee-osx.inc +++ b/scripts/build/p-klee-osx.inc @@ -9,6 +9,8 @@ install_build_dependencies_klee() { pip3 install --user --upgrade lit tabulate + brew install pkg-config + # Get path of package location base_path=$(python3 -m site --user-base) export PATH="${base_path}/bin:$PATH" diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc index 6d81213ef9a..8544284bc50 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -111,6 +111,7 @@ 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" diff --git a/scripts/build/v-bitwuzla.inc b/scripts/build/v-bitwuzla.inc index fa957238ca1..7dd553d6143 100644 --- a/scripts/build/v-bitwuzla.inc +++ b/scripts/build/v-bitwuzla.inc @@ -1,6 +1,7 @@ # Build information for Bitwuzla solver required_variables_bitwuzla=( "BITWUZLA_VERSION" + "BITWUZLA_COMMIT" ) artifact_dependency_bitwuzla=("")