Skip to content

Commit

Permalink
[fix, bitwuzla, ci] Fixed Bitwuzla building. Added commit option for …
Browse files Browse the repository at this point in the history
…git clone util function.
  • Loading branch information
S1eGa committed Nov 17, 2023
1 parent 12e32df commit aaa1f56
Show file tree
Hide file tree
Showing 12 changed files with 40 additions and 24 deletions.
3 changes: 2 additions & 1 deletion .github/workflows/build.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
5 changes: 3 additions & 2 deletions build.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
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
5 changes: 5 additions & 0 deletions scripts/build/common-functions
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
Expand Down
3 changes: 3 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,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"
Expand Down
7 changes: 4 additions & 3 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 @@ -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"
}

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
2 changes: 2 additions & 0 deletions scripts/build/p-klee-osx.inc
Original file line number Diff line number Diff line change
Expand Up @@ -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"
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
1 change: 1 addition & 0 deletions scripts/build/v-bitwuzla.inc
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
# Build information for Bitwuzla solver
required_variables_bitwuzla=(
"BITWUZLA_VERSION"
"BITWUZLA_COMMIT"
)

artifact_dependency_bitwuzla=("")
Expand Down

0 comments on commit aaa1f56

Please sign in to comment.