From 63224e0d3ef3eb3abb8b6160ca644a8cf31ab77a Mon Sep 17 00:00:00 2001 From: Sergey Morozov Date: Fri, 17 Nov 2023 17:51:37 +0300 Subject: [PATCH] [fix, bitwuzla, ci] Fixed Bitwuzla building. --- cmake/find_bitwuzla.cmake | 6 +++--- lib/Solver/BitwuzlaSolver.cpp | 14 ++++++++++++++ lib/Solver/BitwuzlaSolver.h | 15 --------------- scripts/build/p-bitwuzla-linux-ubuntu.inc | 6 ++++++ scripts/build/p-bitwuzla-osx.inc | 3 ++- scripts/build/p-bitwuzla.inc | 5 +++-- scripts/build/p-klee-linux-ubuntu.inc | 2 ++ scripts/build/p-klee-osx.inc | 1 + scripts/build/p-klee.inc | 1 + 9 files changed, 32 insertions(+), 21 deletions(-) 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/p-bitwuzla-linux-ubuntu.inc b/scripts/build/p-bitwuzla-linux-ubuntu.inc index 39a838e8171..2b4cd6a14fb 100644 --- a/scripts/build/p-bitwuzla-linux-ubuntu.inc +++ b/scripts/build/p-bitwuzla-linux-ubuntu.inc @@ -4,6 +4,8 @@ install_build_dependencies_bitwuzla() { with_sudo apt update -y dependencies=( + build-essential + ninja-build python3 python3-pip @@ -13,6 +15,10 @@ install_build_dependencies_bitwuzla() { #Install essential dependencies with_sudo apt -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 libgmp-dev + 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-osx.inc b/scripts/build/p-bitwuzla-osx.inc index 148601ccc3e..af4cc8f6514 100644 --- a/scripts/build/p-bitwuzla-osx.inc +++ b/scripts/build/p-bitwuzla-osx.inc @@ -5,8 +5,9 @@ install_build_dependencies_bitwuzla() { python3-pip cmake git + pkg-config ) - brew install "${dependencies[@]}" + brew 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..b9a528b71e7 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 @@ -15,10 +16,10 @@ download_bitwuzla() { 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..a67a061615b 100644 --- a/scripts/build/p-klee-linux-ubuntu.inc +++ b/scripts/build/p-klee-linux-ubuntu.inc @@ -10,6 +10,8 @@ install_build_dependencies_klee() { python3-setuptools python3-pip python3-wheel + pkg-config + cmake-data ) if [[ "${SOLVERS:-}" == "metaSMT" ]]; then diff --git a/scripts/build/p-klee-osx.inc b/scripts/build/p-klee-osx.inc index 0561e28f68c..4f5b063599a 100644 --- a/scripts/build/p-klee-osx.inc +++ b/scripts/build/p-klee-osx.inc @@ -9,6 +9,7 @@ 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"