Skip to content

Commit

Permalink
[fix, bitwuzla, ci] Fixed Bitwuzla building.
Browse files Browse the repository at this point in the history
  • Loading branch information
S1eGa committed Nov 17, 2023
1 parent 12e32df commit 63224e0
Show file tree
Hide file tree
Showing 9 changed files with 32 additions and 21 deletions.
6 changes: 3 additions & 3 deletions cmake/find_bitwuzla.cmake
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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.")
Expand Down
14 changes: 14 additions & 0 deletions lib/Solver/BitwuzlaSolver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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()) {}
Expand Down
15 changes: 0 additions & 15 deletions lib/Solver/BitwuzlaSolver.h
Original file line number Diff line number Diff line change
@@ -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:
Expand Down
6 changes: 6 additions & 0 deletions scripts/build/p-bitwuzla-linux-ubuntu.inc
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ install_build_dependencies_bitwuzla() {
with_sudo apt update -y

dependencies=(
build-essential

ninja-build
python3
python3-pip
Expand All @@ -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"
Expand Down
3 changes: 2 additions & 1 deletion scripts/build/p-bitwuzla-osx.inc
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
5 changes: 3 additions & 2 deletions scripts/build/p-bitwuzla.inc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"
}

Expand Down
2 changes: 2 additions & 0 deletions scripts/build/p-klee-linux-ubuntu.inc
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ install_build_dependencies_klee() {
python3-setuptools
python3-pip
python3-wheel
pkg-config
cmake-data
)

if [[ "${SOLVERS:-}" == "metaSMT" ]]; then
Expand Down
1 change: 1 addition & 0 deletions scripts/build/p-klee-osx.inc
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions scripts/build/p-klee.inc
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down

0 comments on commit 63224e0

Please sign in to comment.