[fix, bitwuzla, ci] Fixed Bitwuzla building.

S1eGa · Nov 17, 2023 · 7e7ca1c · 7e7ca1c
1 parent 12e32df
commit 7e7ca1c
Show file tree

Hide file tree

Showing 10 changed files with 33 additions and 22 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -29,7 +29,7 @@ env:
   USE_LIBCXX: 1
   Z3_VERSION: 4.8.15
   SQLITE_VERSION: 3400100
-  BITWUZLA_VERSION: 0.2.0
+  BITWUZLA_VERSION: main
 
 jobs:
   Linux:

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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"