diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index dc2c95350c..1813a8ef4a 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -21,7 +21,7 @@ env: LLVM_VERSION: 11 MINISAT_VERSION: "master" REQUIRES_RTTI: 0 - SOLVERS: Z3:STP + SOLVERS: BITWUZLA:Z3:STP STP_VERSION: 2.3.3 TCMALLOC_VERSION: 2.9.1 UCLIBC_VERSION: klee_uclibc_v1.3 @@ -29,6 +29,8 @@ env: USE_LIBCXX: 1 Z3_VERSION: 4.8.15 SQLITE_VERSION: 3400100 + BITWUZLA_VERSION: main + BITWUZLA_COMMIT: 80ef7cd803e1c71b5939c3eb951f1736388f7090 jobs: Linux: @@ -48,6 +50,7 @@ jobs: "Z3 only", "metaSMT", "STP master", + "Bitwuzla only", "Latest klee-uclibc", "Asserts disabled", "No TCMalloc, optimised runtime", @@ -109,6 +112,10 @@ jobs: env: SOLVERS: STP STP_VERSION: master + # Test just using Bitwuzla only + - name: "Bitwuzla only" + env: + SOLVERS: BITWUZLA # Check we can build latest klee-uclibc branch - name: "Latest klee-uclibc" env: @@ -172,6 +179,7 @@ jobs: name: [ "STP", "Z3", + "Bitwuzla", ] include: - name: "STP" @@ -180,6 +188,9 @@ jobs: - name: "Z3" env: SOLVERS: Z3:STP + - name: "Bitwuzla" + env: + SOLVERS: BITWUZLA:Z3 env: ENABLE_OPTIMIZED: 0 COVERAGE: 1 diff --git a/CMakeLists.txt b/CMakeLists.txt index cad45136e7..5ce961bad5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -204,14 +204,19 @@ include(${CMAKE_SOURCE_DIR}/cmake/find_stp.cmake) include(${CMAKE_SOURCE_DIR}/cmake/find_z3.cmake) # metaSMT include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake) +# bitwuzla +include(${CMAKE_SOURCE_DIR}/cmake/find_bitwuzla.cmake) -if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT})) + +if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}) AND (NOT ${ENABLE_BITWUZLA})) message(FATAL_ERROR "No solver was specified. At least one solver is required." "You should enable a solver by passing one of more the following options" " to cmake:\n" "\"-DENABLE_SOLVER_STP=ON\"\n" "\"-DENABLE_SOLVER_Z3=ON\"\n" - "\"-DENABLE_SOLVER_METASMT=ON\"") + "\"-DENABLE_SOLVER_BITWUZLA=ON\"\n" + "\"-DENABLE_SOLVER_METASMT=ON\" + ") endif() ############################################################################### @@ -473,10 +478,10 @@ endif() ################################################################################ option(ENABLE_FLOATING_POINT "Enable KLEE's floating point extension" OFF) if (ENABLE_FLOATING_POINT) - if (NOT ${ENABLE_Z3}) + if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_BITWUZLA})) message (FATAL_ERROR "Floating point extension is availible only when using Z3 backend." - "You should enable Z3 by passing the following option to cmake:\n" - "\"-DENABLE_SOLVER_Z3=ON\"\n") + "You should enable either Z3 or Bitwuzla by passing the following options to cmake, respectively:\n" + "\"-DENABLE_SOLVER_Z3=ON\" or \"-DENABLE_SOLVER_BITWUZLA=ON\"\n") else() set(ENABLE_FP 1) # For config.h message(STATUS "Floating point extension enabled") diff --git a/build.sh b/build.sh index cc41037dcb..71df1df169 100755 --- a/build.sh +++ b/build.sh @@ -35,7 +35,7 @@ REQUIRES_RTTI=0 ## Solvers Required options # SOLVERS=STP -SOLVERS=STP:Z3 +SOLVERS=BITWUZLA:Z3:STP ## Google Test Required options GTEST_VERSION=1.11.0 @@ -46,7 +46,11 @@ UCLIBC_VERSION=klee_uclibc_v1.3 ## Z3 Required options Z3_VERSION=4.8.15 + STP_VERSION=2.3.3 MINISAT_VERSION=master -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 SQLITE_VERSION=$SQLITE_VERSION ./scripts/build/build.sh klee --install-system-deps +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 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 new file mode 100644 index 0000000000..82e9866dcc --- /dev/null +++ b/cmake/find_bitwuzla.cmake @@ -0,0 +1,46 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +find_package (PkgConfig REQUIRED) +pkg_check_modules(BITWUZLA IMPORTED_TARGET bitwuzla) + +# Set the default so that if the following is true: +# * Bitwuzla was found +# * ENABLE_SOLVER_BITWUZLA is not already set as a cache variable +# +# then the default is set to `ON`. Otherwise set the default to `OFF`. +# A consequence of this is if we fail to detect Bitwuzla the first time +# subsequent calls to CMake will not change the default. + +if(BITWUZLA_FOUND) + set(ENABLE_SOLVER_BITWUZLA_DEFAULT ON) +else() + set(ENABLE_SOLVER_BITWUZLA_DEFAULT OFF) +endif() + +option(ENABLE_SOLVER_BITWUZLA "Enable Bitwuzla solver support" ${ENABLE_SOLVER_BITWUZLA_DEFAULT}) + +if (ENABLE_SOLVER_BITWUZLA) + message(STATUS "Bitwuzla solver support enabled") + if (BITWUZLA_FOUND) + message(STATUS "Found Bitwuzla") + set(ENABLE_BITWUZLA 1) # For config.h + + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${BITWUZLA_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARIES ${BITWUZLA_LINK_LIBRARIES}) + list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${BITWUZLA_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${BITWUZLA_LINK_LIBRARIES}) + + else() + message(FATAL_ERROR "Bitwuzla not found.") + endif() +else() + message(STATUS "Bitwuzla solver support disabled") + set(ENABLE_BITWUZLA 0) # For config.h +endif() diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin index 91dbaf6868..1d3f1ac6dd 100644 --- a/include/klee/Config/config.h.cmin +++ b/include/klee/Config/config.h.cmin @@ -13,6 +13,9 @@ /* Using Z3 Solver backend */ #cmakedefine ENABLE_Z3 @ENABLE_Z3@ +/* Using Bitwuzla Solver backend */ +#cmakedefine ENABLE_BITWUZLA @ENABLE_BITWUZLA@ + /* Enable KLEE floating point extension */ #cmakedefine ENABLE_FP @ENABLE_FP@ diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h index 75769b3fb4..d81bd9cc7d 100644 --- a/include/klee/Expr/Constraints.h +++ b/include/klee/Expr/Constraints.h @@ -49,7 +49,11 @@ class ConstraintSet { bool isSymcretized(ref expr) const; void rewriteConcretization(const Assignment &a); - ConstraintSet withExpr(ref e) const; + ConstraintSet withExpr(ref e) const { + ConstraintSet copy = ConstraintSet(*this); + copy.addConstraint(e, Assignment()); + return copy; + } std::vector gatherArrays() const; std::vector gatherSymcretizedArrays() const; diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h index 692f741734..e4e5fdcf03 100644 --- a/include/klee/Solver/SolverCmdLine.h +++ b/include/klee/Solver/SolverCmdLine.h @@ -65,6 +65,8 @@ enum QueryLoggingSolverType { extern llvm::cl::bits QueryLoggingOptions; enum CoreSolverType { + BITWUZLA_SOLVER, + BITWUZLA_TREE_SOLVER, STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER, diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp new file mode 100644 index 0000000000..2c47a1440a --- /dev/null +++ b/lib/Solver/BitwuzlaBuilder.cpp @@ -0,0 +1,1314 @@ +//===-- BitwuzlaBuilder.cpp ---------------------------------*- C++ -*-====// +//-*-====// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/Config/config.h" + +#ifdef ENABLE_BITWUZLA + +#include "BitwuzlaBuilder.h" +#include "BitwuzlaHashConfig.h" +#include "klee/ADT/Bits.h" + +#include "klee/Expr/Expr.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" +#include "klee/Support/ErrorHandling.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/ADT/StringExtras.h" +#include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP + +namespace klee { + +BitwuzlaArrayExprHash::~BitwuzlaArrayExprHash() {} + +void BitwuzlaArrayExprHash::clear() { + _update_node_hash.clear(); + _array_hash.clear(); +} + +void BitwuzlaArrayExprHash::clearUpdates() { _update_node_hash.clear(); } + +BitwuzlaBuilder::BitwuzlaBuilder(bool autoClearConstructCache) + : autoClearConstructCache(autoClearConstructCache) {} + +BitwuzlaBuilder::~BitwuzlaBuilder() { + _arr_hash.clearUpdates(); + clearSideConstraints(); +} + +Sort BitwuzlaBuilder::getBoolSort() { + // FIXME: cache these + return mk_bool_sort(); +} + +Sort BitwuzlaBuilder::getBvSort(unsigned width) { + // FIXME: cache these + return mk_bv_sort(width); +} + +Sort BitwuzlaBuilder::getArraySort(Sort domainSort, Sort rangeSort) { + // FIXME: cache these + return mk_array_sort(domainSort, rangeSort); +} + +Term BitwuzlaBuilder::buildFreshBoolConst() { return mk_const(getBoolSort()); } + +Term BitwuzlaBuilder::buildArray(const char *name, unsigned indexWidth, + unsigned valueWidth) { + Sort domainSort = getBvSort(indexWidth); + Sort rangeSort = getBvSort(valueWidth); + Sort t = getArraySort(domainSort, rangeSort); + return mk_const(t, std::string(name)); +} + +Term BitwuzlaBuilder::buildConstantArray(const char *name, unsigned indexWidth, + unsigned valueWidth, unsigned value) { + Sort domainSort = getBvSort(indexWidth); + Sort rangeSort = getBvSort(valueWidth); + return mk_const_array(getArraySort(domainSort, rangeSort), + bvConst32(valueWidth, value)); +} + +Term BitwuzlaBuilder::getTrue() { return mk_true(); } + +Term BitwuzlaBuilder::getFalse() { return mk_false(); } + +Term BitwuzlaBuilder::bvOne(unsigned width) { + return mk_bv_one(getBvSort(width)); +} +Term BitwuzlaBuilder::bvZero(unsigned width) { + return mk_bv_zero(getBvSort(width)); +} +Term BitwuzlaBuilder::bvMinusOne(unsigned width) { + return bvZExtConst(width, (uint64_t)-1); +} +Term BitwuzlaBuilder::bvConst32(unsigned width, uint32_t value) { + if (width < 32) { + value &= ((1 << width) - 1); + } + return mk_bv_value_uint64(getBvSort(width), value); +} +Term BitwuzlaBuilder::bvConst64(unsigned width, uint64_t value) { + if (width < 64) { + value &= ((uint64_t(1) << width) - 1); + } + return mk_bv_value_uint64(getBvSort(width), value); +} +Term BitwuzlaBuilder::bvZExtConst(unsigned width, uint64_t value) { + if (width <= 64) { + return bvConst64(width, value); + } + std::vector terms = {bvConst64(64, value)}; + for (width -= 64; width > 64; width -= 64) { + terms.push_back(bvConst64(64, 0)); + } + terms.push_back(bvConst64(width, 0)); + return mk_term(Kind::BV_CONCAT, terms); +} + +Term BitwuzlaBuilder::bvSExtConst(unsigned width, uint64_t value) { + if (width <= 64) { + return bvConst64(width, value); + } + + Sort t = getBvSort(width - 64); + if (value >> 63) { + return mk_term(Kind::BV_CONCAT, + {bvMinusOne(width - 64), bvConst64(64, value)}); + } + return mk_term(Kind::BV_CONCAT, {bvZero(width - 64), bvConst64(64, value)}); +} + +Term BitwuzlaBuilder::bvBoolExtract(Term expr, int bit) { + return mk_term(Kind::EQUAL, {bvExtract(expr, bit, bit), bvOne(1)}); +} + +Term BitwuzlaBuilder::bvExtract(Term expr, unsigned top, unsigned bottom) { + return mk_term(Kind::BV_EXTRACT, {castToBitVector(expr)}, {top, bottom}); +} + +Term BitwuzlaBuilder::eqExpr(Term a, Term b) { + // Handle implicit bitvector/float coercision + Sort aSort = a.sort(); + Sort bSort = b.sort(); + + if (aSort.is_bool() && bSort.is_fp()) { + // Coerce `b` to be a bitvector + b = castToBitVector(b); + } + + if (aSort.is_fp() && bSort.is_bool()) { + // Coerce `a` to be a bitvector + a = castToBitVector(a); + } + return mk_term(Kind::EQUAL, {a, b}); +} + +// logical right shift +Term BitwuzlaBuilder::bvRightShift(Term expr, unsigned shift) { + Term exprAsBv = castToBitVector(expr); + unsigned width = getBVLength(exprAsBv); + + if (shift == 0) { + return expr; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + return mk_term(Kind::BV_SHR, {exprAsBv, bvConst32(width, shift)}); + } +} + +// logical left shift +Term BitwuzlaBuilder::bvLeftShift(Term expr, unsigned shift) { + Term exprAsBv = castToBitVector(expr); + unsigned width = getBVLength(exprAsBv); + + if (shift == 0) { + return expr; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + return mk_term(Kind::BV_SHL, {exprAsBv, bvConst32(width, shift)}); + } +} + +// left shift by a variable amount on an expression of the specified width +Term BitwuzlaBuilder::bvVarLeftShift(Term expr, Term shift) { + Term exprAsBv = castToBitVector(expr); + Term shiftAsBv = castToBitVector(shift); + + unsigned width = getBVLength(exprAsBv); + Term res = mk_term(Kind::BV_SHL, {exprAsBv, shiftAsBv}); + + // If overshifting, shift to zero + Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width)); + res = iteExpr(ex, res, bvZero(width)); + return res; +} + +// logical right shift by a variable amount on an expression of the specified +// width +Term BitwuzlaBuilder::bvVarRightShift(Term expr, Term shift) { + Term exprAsBv = castToBitVector(expr); + Term shiftAsBv = castToBitVector(shift); + + unsigned width = getBVLength(exprAsBv); + Term res = mk_term(Kind::BV_SHR, {exprAsBv, shiftAsBv}); + + // If overshifting, shift to zero + Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width)); + res = iteExpr(ex, res, bvZero(width)); + return res; +} + +// arithmetic right shift by a variable amount on an expression of the specified +// width +Term BitwuzlaBuilder::bvVarArithRightShift(Term expr, Term shift) { + Term exprAsBv = castToBitVector(expr); + Term shiftAsBv = castToBitVector(shift); + + unsigned width = getBVLength(exprAsBv); + + Term res = mk_term(Kind::BV_ASHR, {exprAsBv, shiftAsBv}); + + // If overshifting, shift to zero + Term ex = bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width)); + res = iteExpr(ex, res, bvZero(width)); + return res; +} + +Term BitwuzlaBuilder::notExpr(Term expr) { return mk_term(Kind::NOT, {expr}); } +Term BitwuzlaBuilder::andExpr(Term lhs, Term rhs) { + return mk_term(Kind::AND, {lhs, rhs}); +} +Term BitwuzlaBuilder::orExpr(Term lhs, Term rhs) { + return mk_term(Kind::OR, {lhs, rhs}); +} +Term BitwuzlaBuilder::iffExpr(Term lhs, Term rhs) { + return mk_term(Kind::IFF, {lhs, rhs}); +} + +Term BitwuzlaBuilder::bvNotExpr(Term expr) { + return mk_term(Kind::BV_NOT, {castToBitVector(expr)}); +} + +Term BitwuzlaBuilder::bvAndExpr(Term lhs, Term rhs) { + return mk_term(Kind::BV_AND, {castToBitVector(lhs), castToBitVector(rhs)}); +} + +Term BitwuzlaBuilder::bvOrExpr(Term lhs, Term rhs) { + return mk_term(Kind::BV_OR, {castToBitVector(lhs), castToBitVector(rhs)}); +} + +Term BitwuzlaBuilder::bvXorExpr(Term lhs, Term rhs) { + return mk_term(Kind::BV_XOR, {castToBitVector(lhs), castToBitVector(rhs)}); +} + +Term BitwuzlaBuilder::bvSignExtend(Term src, unsigned width) { + Term srcAsBv = castToBitVector(src); + unsigned src_width = srcAsBv.sort().bv_size(); + assert(src_width <= width && "attempted to extend longer data"); + + if (width <= 64) { + return mk_term(Kind::BV_SIGN_EXTEND, {srcAsBv}, {width - src_width}); + } + + Term signBit = bvBoolExtract(srcAsBv, src_width - 1); + Term zeroExtended = + mk_term(Kind::BV_CONCAT, {bvZero(width - src_width), src}); + Term oneExtended = + mk_term(Kind::BV_CONCAT, {bvMinusOne(width - src_width), src}); + + return mk_term(Kind::ITE, {signBit, oneExtended, zeroExtended}); +} + +Term BitwuzlaBuilder::writeExpr(Term array, Term index, Term value) { + return mk_term(Kind::ARRAY_STORE, {array, index, value}); +} + +Term BitwuzlaBuilder::readExpr(Term array, Term index) { + return mk_term(Kind::ARRAY_SELECT, {array, index}); +} + +unsigned BitwuzlaBuilder::getBVLength(Term expr) { + if (!expr.sort().is_bv()) { + klee_error("getBVLength() accepts only bitvector, given %s", + expr.sort().str().c_str()); + } + return expr.sort().bv_size(); +} + +Term BitwuzlaBuilder::iteExpr(Term condition, Term whenTrue, Term whenFalse) { + // Handle implicit bitvector/float coercision + Sort whenTrueSort = whenTrue.sort(); + Sort whenFalseSort = whenFalse.sort(); + + if (whenTrueSort.is_bv() && whenFalseSort.is_fp()) { + // Coerce `whenFalse` to be a bitvector + whenFalse = castToBitVector(whenFalse); + } + + if (whenTrueSort.is_fp() && whenFalseSort.is_bv()) { + // Coerce `whenTrue` to be a bitvector + whenTrue = castToBitVector(whenTrue); + } + return mk_term(Kind::ITE, {condition, whenTrue, whenFalse}); +} + +Term BitwuzlaBuilder::bvLtExpr(Term lhs, Term rhs) { + return mk_term(Kind::BV_ULT, {castToBitVector(lhs), castToBitVector(rhs)}); +} + +Term BitwuzlaBuilder::bvLeExpr(Term lhs, Term rhs) { + return mk_term(Kind::BV_ULE, {castToBitVector(lhs), castToBitVector(rhs)}); +} + +Term BitwuzlaBuilder::sbvLtExpr(Term lhs, Term rhs) { + return mk_term(Kind::BV_SLT, {castToBitVector(lhs), castToBitVector(rhs)}); +} + +Term BitwuzlaBuilder::sbvLeExpr(Term lhs, Term rhs) { + return mk_term(Kind::BV_SLE, {castToBitVector(lhs), castToBitVector(rhs)}); +} + +Term BitwuzlaBuilder::constructAShrByConstant(Term expr, unsigned shift, + Term isSigned) { + Term exprAsBv = castToBitVector(expr); + unsigned width = getBVLength(exprAsBv); + + if (shift == 0) { + return exprAsBv; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + // FIXME: Is this really the best way to interact with Bitwuzla? + Term signed_term = + mk_term(Kind::BV_CONCAT, + {bvMinusOne(shift), bvExtract(exprAsBv, width - 1, shift)}); + Term unsigned_term = bvRightShift(exprAsBv, shift); + + return mk_term(Kind::ITE, {isSigned, signed_term, unsigned_term}); + } +} + +Term BitwuzlaBuilder::getInitialArray(const Array *root) { + assert(root); + Term array_expr; + bool hashed = _arr_hash.lookupArrayExpr(root, array_expr); + + if (!hashed) { + // Unique arrays by name, so we make sure the name is unique by + // using the size of the array hash as a counter. + std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); + std::string unique_name = root->getIdentifier() + unique_id; + + auto source = dyn_cast(root->source); + auto value = (source ? source->constantValues.defaultV() : nullptr); + if (source) { + assert(value); + } + + if (source && !isa(root->size)) { + array_expr = buildConstantArray(unique_name.c_str(), root->getDomain(), + root->getRange(), value->getZExtValue(8)); + } else { + array_expr = + buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); + } + + if (source) { + if (auto constSize = dyn_cast(root->size)) { + std::vector array_assertions; + for (size_t i = 0; i < constSize->getZExtValue(); i++) { + auto value = source->constantValues.load(i); + // construct(= (select i root) root->value[i]) to be asserted in + // BitwuzlaSolver.cpp + int width_out; + Term array_value = construct(value, &width_out); + assert(width_out == (int)root->getRange() && + "Value doesn't match root range"); + array_assertions.push_back( + eqExpr(readExpr(array_expr, bvConst32(root->getDomain(), i)), + array_value)); + } + constant_array_assertions[root] = std::move(array_assertions); + } else { + for (auto &[index, value] : source->constantValues.storage()) { + int width_out; + Term array_value = construct(value, &width_out); + assert(width_out == (int)root->getRange() && + "Value doesn't match root range"); + array_expr = writeExpr( + array_expr, bvConst32(root->getDomain(), index), array_value); + } + } + } + + _arr_hash.hashArrayExpr(root, array_expr); + } + + return array_expr; +} + +Term BitwuzlaBuilder::getInitialRead(const Array *root, unsigned index) { + return readExpr(getInitialArray(root), bvConst32(32, index)); +} + +Term BitwuzlaBuilder::getArrayForUpdate(const Array *root, + const UpdateNode *un) { + // Iterate over the update nodes, until we find a cached version of the node, + // or no more update nodes remain + Term un_expr; + std::vector update_nodes; + for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr); + un = un->next.get()) { + update_nodes.push_back(un); + } + if (!un) { + un_expr = getInitialArray(root); + } + // `un_expr` now holds an expression for the array - either from cache or by + // virtue of being the initial array expression + + // Create and cache solver expressions based on the update nodes starting from + // the oldest + for (const auto &un : + llvm::make_range(update_nodes.crbegin(), update_nodes.crend())) { + un_expr = + writeExpr(un_expr, construct(un->index, 0), construct(un->value, 0)); + + _arr_hash.hashUpdateNodeExpr(un, un_expr); + } + + return un_expr; +} + +Term BitwuzlaBuilder::construct(ref e, int *width_out) { + if (!BitwuzlaHashConfig::UseConstructHashBitwuzla || isa(e)) { + return constructActual(e, width_out); + } else { + ExprHashMap>::iterator it = constructed.find(e); + if (it != constructed.end()) { + if (width_out) + *width_out = it->second.second; + return it->second.first; + } else { + int width; + if (!width_out) + width_out = &width; + Term res = constructActual(e, width_out); + constructed.insert(std::make_pair(e, std::make_pair(res, *width_out))); + return res; + } + } +} + +void BitwuzlaBuilder::FPCastWidthAssert(int *width_out, char const *msg) { + assert(&(ConstantExpr::widthToFloatSemantics(*width_out)) != + &(llvm::APFloat::Bogus()) && + msg); +} + +/** if *width_out!=1 then result is a bitvector, +otherwise it is a bool */ +Term BitwuzlaBuilder::constructActual(ref e, int *width_out) { + + int width; + if (!width_out) + width_out = &width; + ++stats::queryConstructs; + switch (e->getKind()) { + case Expr::Constant: { + ConstantExpr *CE = cast(e); + *width_out = CE->getWidth(); + + // Coerce to bool if necessary. + if (*width_out == 1) + return CE->isTrue() ? getTrue() : getFalse(); + + Term Res; + if (*width_out <= 32) { + // Fast path. + Res = bvConst32(*width_out, CE->getZExtValue(32)); + } else if (*width_out <= 64) { + // Fast path. + Res = bvConst64(*width_out, CE->getZExtValue()); + } else { + llvm::SmallString<129> CEUValue; + CE->getAPValue().toStringUnsigned(CEUValue); + Res = mk_bv_value(mk_bv_sort(CE->getWidth()), CEUValue.str().str(), 10); + } + // Coerce to float if necesary + if (CE->isFloat()) { + Res = castToFloat(Res); + } + return Res; + } + + // Special + case Expr::NotOptimized: { + NotOptimizedExpr *noe = cast(e); + return construct(noe->src, width_out); + } + + case Expr::Read: { + ReadExpr *re = cast(e); + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); + return readExpr(getArrayForUpdate(re->updates.root, re->updates.head.get()), + construct(re->index, 0)); + } + + case Expr::Select: { + SelectExpr *se = cast(e); + Term cond = construct(se->cond, 0); + Term tExpr = construct(se->trueExpr, width_out); + Term fExpr = construct(se->falseExpr, width_out); + return iteExpr(cond, tExpr, fExpr); + } + + case Expr::Concat: { + ConcatExpr *ce = cast(e); + unsigned numKids = ce->getNumKids(); + std::vector term_args; + term_args.reserve(numKids); + + for (unsigned i = 0; i < numKids; ++i) { + term_args.push_back(construct(ce->getKid(i), 0)); + } + + *width_out = ce->getWidth(); + return mk_term(Kind::BV_CONCAT, term_args); + } + + case Expr::Extract: { + ExtractExpr *ee = cast(e); + Term src = construct(ee->expr, width_out); + *width_out = ee->getWidth(); + if (*width_out == 1) { + return bvBoolExtract(src, ee->offset); + } else { + return bvExtract(src, ee->offset + *width_out - 1, ee->offset); + } + } + + // Casting + + case Expr::ZExt: { + int srcWidth; + CastExpr *ce = cast(e); + Term src = construct(ce->src, &srcWidth); + *width_out = ce->getWidth(); + if (srcWidth == 1) { + return iteExpr(src, bvOne(*width_out), bvZero(*width_out)); + } else { + assert(*width_out > srcWidth && "Invalid width_out"); + return mk_term(Kind::BV_CONCAT, + {bvZero(*width_out - srcWidth), castToBitVector(src)}); + } + } + + case Expr::SExt: { + int srcWidth; + CastExpr *ce = cast(e); + Term src = construct(ce->src, &srcWidth); + *width_out = ce->getWidth(); + if (srcWidth == 1) { + return iteExpr(src, bvMinusOne(*width_out), bvZero(*width_out)); + } else { + return bvSignExtend(src, *width_out); + } + } + + case Expr::FPExt: { + int srcWidth; + FPExtExpr *ce = cast(e); + Term src = castToFloat(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid FPExt width"); + assert(*width_out >= srcWidth && "Invalid FPExt"); + // Just use any arounding mode here as we are extending + auto out_widths = getFloatSortFromBitWidth(*width_out); + return mk_term( + Kind::FP_TO_FP_FROM_FP, + {getRoundingModeSort(llvm::APFloat::rmNearestTiesToEven), src}, + {out_widths.first, out_widths.second}); + } + + case Expr::FPTrunc: { + int srcWidth; + FPTruncExpr *ce = cast(e); + Term src = castToFloat(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid FPTrunc width"); + assert(*width_out <= srcWidth && "Invalid FPTrunc"); + + auto out_widths = getFloatSortFromBitWidth(*width_out); + return mk_term( + Kind::FP_TO_FP_FROM_FP, + {getRoundingModeSort(llvm::APFloat::rmNearestTiesToEven), src}, + {out_widths.first, out_widths.second}); + } + + case Expr::FPToUI: { + int srcWidth; + FPToUIExpr *ce = cast(e); + Term src = castToFloat(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid FPToUI width"); + return mk_term(Kind::FP_TO_UBV, + {getRoundingModeSort(ce->roundingMode), src}, + {ce->getWidth()}); + } + + case Expr::FPToSI: { + int srcWidth; + FPToSIExpr *ce = cast(e); + Term src = castToFloat(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid FPToSI width"); + return mk_term(Kind::FP_TO_SBV, + {getRoundingModeSort(ce->roundingMode), src}, + {ce->getWidth()}); + } + + case Expr::UIToFP: { + int srcWidth; + UIToFPExpr *ce = cast(e); + Term src = castToBitVector(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid UIToFP width"); + + auto out_widths = getFloatSortFromBitWidth(*width_out); + return mk_term(Kind::FP_TO_FP_FROM_UBV, + {getRoundingModeSort(ce->roundingMode), src}, + {out_widths.first, out_widths.second}); + } + + case Expr::SIToFP: { + int srcWidth; + SIToFPExpr *ce = cast(e); + Term src = castToBitVector(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid SIToFP width"); + + auto out_widths = getFloatSortFromBitWidth(*width_out); + return mk_term(Kind::FP_TO_FP_FROM_SBV, + {getRoundingModeSort(ce->roundingMode), src}, + {out_widths.first, out_widths.second}); + } + + // Arithmetic + case Expr::Add: { + AddExpr *ae = cast(e); + Term left = castToBitVector(construct(ae->left, width_out)); + Term right = castToBitVector(construct(ae->right, width_out)); + assert(*width_out != 1 && "uncanonicalized add"); + Term result = mk_term(Kind::BV_ADD, {left, right}); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::Sub: { + SubExpr *se = cast(e); + Term left = castToBitVector(construct(se->left, width_out)); + Term right = castToBitVector(construct(se->right, width_out)); + assert(*width_out != 1 && "uncanonicalized sub"); + Term result = mk_term(Kind::BV_SUB, {left, right}); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::Mul: { + MulExpr *me = cast(e); + Term right = castToBitVector(construct(me->right, width_out)); + assert(*width_out != 1 && "uncanonicalized mul"); + Term left = castToBitVector(construct(me->left, width_out)); + Term result = mk_term(Kind::BV_MUL, {left, right}); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::UDiv: { + UDivExpr *de = cast(e); + Term left = castToBitVector(construct(de->left, width_out)); + assert(*width_out != 1 && "uncanonicalized udiv"); + + if (ConstantExpr *CE = dyn_cast(de->right)) { + if (CE->getWidth() <= 64) { + uint64_t divisor = CE->getZExtValue(); + if (bits64::isPowerOfTwo(divisor)) + return bvRightShift(left, bits64::indexOfSingleBit(divisor)); + } + } + + Term right = castToBitVector(construct(de->right, width_out)); + Term result = mk_term(Kind::BV_UDIV, {left, right}); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::SDiv: { + SDivExpr *de = cast(e); + Term left = castToBitVector(construct(de->left, width_out)); + assert(*width_out != 1 && "uncanonicalized sdiv"); + Term right = castToBitVector(construct(de->right, width_out)); + Term result = mk_term(Kind::BV_SDIV, {left, right}); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::URem: { + URemExpr *de = cast(e); + Term left = castToBitVector(construct(de->left, width_out)); + assert(*width_out != 1 && "uncanonicalized urem"); + + if (ConstantExpr *CE = dyn_cast(de->right)) { + if (CE->getWidth() <= 64) { + uint64_t divisor = CE->getZExtValue(); + + if (bits64::isPowerOfTwo(divisor)) { + int bits = bits64::indexOfSingleBit(divisor); + assert(bits >= 0 && "bit index cannot be negative"); + assert(bits64::indexOfSingleBit(divisor) < INT32_MAX); + + // special case for modding by 1 or else we bvExtract -1:0 + if (bits == 0) { + return bvZero(*width_out); + } else { + assert(*width_out > bits && "invalid width_out"); + return mk_term(Kind::BV_CONCAT, {bvZero(*width_out - bits), + bvExtract(left, bits - 1, 0)}); + } + } + } + } + + Term right = castToBitVector(construct(de->right, width_out)); + Term result = mk_term(Kind::BV_UREM, {left, right}); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::SRem: { + SRemExpr *de = cast(e); + Term left = castToBitVector(construct(de->left, width_out)); + Term right = castToBitVector(construct(de->right, width_out)); + assert(*width_out != 1 && "uncanonicalized srem"); + Term result = mk_term(Kind::BV_SREM, {left, right}); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + // Bitwise + case Expr::Not: { + NotExpr *ne = cast(e); + Term expr = construct(ne->expr, width_out); + if (*width_out == 1) { + return notExpr(expr); + } else { + return bvNotExpr(expr); + } + } + + case Expr::And: { + AndExpr *ae = cast(e); + Term left = construct(ae->left, width_out); + Term right = construct(ae->right, width_out); + if (*width_out == 1) { + return andExpr(left, right); + } else { + return bvAndExpr(left, right); + } + } + + case Expr::Or: { + OrExpr *oe = cast(e); + Term left = construct(oe->left, width_out); + Term right = construct(oe->right, width_out); + if (*width_out == 1) { + return orExpr(left, right); + } else { + return bvOrExpr(left, right); + } + } + + case Expr::Xor: { + XorExpr *xe = cast(e); + Term left = construct(xe->left, width_out); + Term right = construct(xe->right, width_out); + + if (*width_out == 1) { + // XXX check for most efficient? + return iteExpr(left, Term(notExpr(right)), right); + } else { + return bvXorExpr(left, right); + } + } + + case Expr::Shl: { + ShlExpr *se = cast(e); + Term left = construct(se->left, width_out); + assert(*width_out != 1 && "uncanonicalized shl"); + + if (ConstantExpr *CE = dyn_cast(se->right)) { + return bvLeftShift(left, (unsigned)CE->getLimitedValue()); + } else { + int shiftWidth; + Term amount = construct(se->right, &shiftWidth); + return bvVarLeftShift(left, amount); + } + } + + case Expr::LShr: { + LShrExpr *lse = cast(e); + Term left = construct(lse->left, width_out); + assert(*width_out != 1 && "uncanonicalized lshr"); + + if (ConstantExpr *CE = dyn_cast(lse->right)) { + return bvRightShift(left, (unsigned)CE->getLimitedValue()); + } else { + int shiftWidth; + Term amount = construct(lse->right, &shiftWidth); + return bvVarRightShift(left, amount); + } + } + + case Expr::AShr: { + AShrExpr *ase = cast(e); + Term left = castToBitVector(construct(ase->left, width_out)); + assert(*width_out != 1 && "uncanonicalized ashr"); + + if (ConstantExpr *CE = dyn_cast(ase->right)) { + unsigned shift = (unsigned)CE->getLimitedValue(); + Term signedBool = bvBoolExtract(left, *width_out - 1); + return constructAShrByConstant(left, shift, signedBool); + } else { + int shiftWidth; + Term amount = construct(ase->right, &shiftWidth); + return bvVarArithRightShift(left, amount); + } + } + + // Comparison + + case Expr::Eq: { + EqExpr *ee = cast(e); + Term left = construct(ee->left, width_out); + Term right = construct(ee->right, width_out); + if (*width_out == 1) { + if (ConstantExpr *CE = dyn_cast(ee->left)) { + if (CE->isTrue()) + return right; + return notExpr(right); + } else { + return iffExpr(left, right); + } + } else { + *width_out = 1; + return eqExpr(left, right); + } + } + + case Expr::Ult: { + UltExpr *ue = cast(e); + Term left = construct(ue->left, width_out); + Term right = construct(ue->right, width_out); + assert(*width_out != 1 && "uncanonicalized ult"); + *width_out = 1; + return bvLtExpr(left, right); + } + + case Expr::Ule: { + UleExpr *ue = cast(e); + Term left = construct(ue->left, width_out); + Term right = construct(ue->right, width_out); + assert(*width_out != 1 && "uncanonicalized ule"); + *width_out = 1; + return bvLeExpr(left, right); + } + + case Expr::Slt: { + SltExpr *se = cast(e); + Term left = construct(se->left, width_out); + Term right = construct(se->right, width_out); + assert(*width_out != 1 && "uncanonicalized slt"); + *width_out = 1; + return sbvLtExpr(left, right); + } + + case Expr::Sle: { + SleExpr *se = cast(e); + Term left = construct(se->left, width_out); + Term right = construct(se->right, width_out); + assert(*width_out != 1 && "uncanonicalized sle"); + *width_out = 1; + return sbvLeExpr(left, right); + } + + case Expr::FOEq: { + FOEqExpr *fcmp = cast(e); + Term left = castToFloat(construct(fcmp->left, width_out)); + Term right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return mk_term(Kind::FP_EQUAL, {left, right}); + } + + case Expr::FOLt: { + FOLtExpr *fcmp = cast(e); + Term left = castToFloat(construct(fcmp->left, width_out)); + Term right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return mk_term(Kind::FP_LT, {left, right}); + } + + case Expr::FOLe: { + FOLeExpr *fcmp = cast(e); + Term left = castToFloat(construct(fcmp->left, width_out)); + Term right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return mk_term(Kind::FP_LEQ, {left, right}); + } + + case Expr::FOGt: { + FOGtExpr *fcmp = cast(e); + Term left = castToFloat(construct(fcmp->left, width_out)); + Term right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return mk_term(Kind::FP_GT, {left, right}); + } + + case Expr::FOGe: { + FOGeExpr *fcmp = cast(e); + Term left = castToFloat(construct(fcmp->left, width_out)); + Term right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return mk_term(Kind::FP_GEQ, {left, right}); + } + + case Expr::IsNaN: { + IsNaNExpr *ine = cast(e); + Term arg = castToFloat(construct(ine->expr, width_out)); + *width_out = 1; + return mk_term(Kind::FP_IS_NAN, {arg}); + } + + case Expr::IsInfinite: { + IsInfiniteExpr *iie = cast(e); + Term arg = castToFloat(construct(iie->expr, width_out)); + *width_out = 1; + return mk_term(Kind::FP_IS_INF, {arg}); + } + + case Expr::IsNormal: { + IsNormalExpr *ine = cast(e); + Term arg = castToFloat(construct(ine->expr, width_out)); + *width_out = 1; + return mk_term(Kind::FP_IS_NORMAL, {arg}); + } + + case Expr::IsSubnormal: { + IsSubnormalExpr *ise = cast(e); + Term arg = castToFloat(construct(ise->expr, width_out)); + *width_out = 1; + return mk_term(Kind::FP_IS_SUBNORMAL, {arg}); + } + + case Expr::FAdd: { + FAddExpr *fadd = cast(e); + Term left = castToFloat(construct(fadd->left, width_out)); + Term right = castToFloat(construct(fadd->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FAdd"); + return mk_term(Kind::FP_ADD, + {getRoundingModeSort(fadd->roundingMode), left, right}); + } + + case Expr::FSub: { + FSubExpr *fsub = cast(e); + Term left = castToFloat(construct(fsub->left, width_out)); + Term right = castToFloat(construct(fsub->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FSub"); + return mk_term(Kind::FP_SUB, + {getRoundingModeSort(fsub->roundingMode), left, right}); + } + + case Expr::FMul: { + FMulExpr *fmul = cast(e); + Term left = castToFloat(construct(fmul->left, width_out)); + Term right = castToFloat(construct(fmul->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FMul"); + return mk_term(Kind::FP_MUL, + {getRoundingModeSort(fmul->roundingMode), left, right}); + } + + case Expr::FDiv: { + FDivExpr *fdiv = cast(e); + Term left = castToFloat(construct(fdiv->left, width_out)); + Term right = castToFloat(construct(fdiv->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FDiv"); + return mk_term(Kind::FP_DIV, + {getRoundingModeSort(fdiv->roundingMode), left, right}); + } + case Expr::FRem: { + FRemExpr *frem = cast(e); + Term left = castToFloat(construct(frem->left, width_out)); + Term right = castToFloat(construct(frem->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FRem"); + return mk_term(Kind::FP_REM, {left, right}); + } + + case Expr::FMax: { + FMaxExpr *fmax = cast(e); + Term left = castToFloat(construct(fmax->left, width_out)); + Term right = castToFloat(construct(fmax->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FMax"); + return mk_term(Kind::FP_MAX, {left, right}); + } + + case Expr::FMin: { + FMinExpr *fmin = cast(e); + Term left = castToFloat(construct(fmin->left, width_out)); + Term right = castToFloat(construct(fmin->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FMin"); + return mk_term(Kind::FP_MIN, {left, right}); + } + + case Expr::FSqrt: { + FSqrtExpr *fsqrt = cast(e); + Term arg = castToFloat(construct(fsqrt->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FSqrt"); + return mk_term(Kind::FP_SQRT, + {getRoundingModeSort(fsqrt->roundingMode), arg}); + } + case Expr::FRint: { + FRintExpr *frint = cast(e); + Term arg = castToFloat(construct(frint->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FSqrt"); + return mk_term(Kind::FP_RTI, + {getRoundingModeSort(frint->roundingMode), arg}); + } + + case Expr::FAbs: { + FAbsExpr *fabsExpr = cast(e); + Term arg = castToFloat(construct(fabsExpr->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FAbs"); + return mk_term(Kind::FP_ABS, {arg}); + } + + case Expr::FNeg: { + FNegExpr *fnegExpr = cast(e); + Term arg = castToFloat(construct(fnegExpr->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FNeg"); + return mk_term(Kind::FP_NEG, {arg}); + } + +// unused due to canonicalization +#if 0 + case Expr::Ne: +case Expr::Ugt: +case Expr::Uge: +case Expr::Sgt: +case Expr::Sge: +#endif + + default: + assert(0 && "unhandled Expr type"); + return getTrue(); + } +} + +Term BitwuzlaBuilder::fpToIEEEBV(const Term &fp) { + if (!fp.sort().is_fp()) { + klee_error("BitwuzlaBuilder::fpToIEEEBV accepts only floats"); + } + + Term signBit = mk_const(getBvSort(1)); + Term exponentBits = mk_const(getBvSort(fp.sort().fp_exp_size())); + Term significandBits = mk_const(getBvSort(fp.sort().fp_sig_size() - 1)); + + Term floatTerm = + mk_term(Kind::FP_FP, {signBit, exponentBits, significandBits}); + sideConstraints.push_back(mk_term(Kind::EQUAL, {fp, floatTerm})); + + return mk_term(Kind::BV_CONCAT, {signBit, exponentBits, significandBits}); +} + +std::pair +BitwuzlaBuilder::getFloatSortFromBitWidth(unsigned bitWidth) { + switch (bitWidth) { + case Expr::Int16: { + return {5, 11}; + } + case Expr::Int32: { + return {8, 24}; + } + case Expr::Int64: { + return {11, 53}; + } + case Expr::Fl80: { + // Note this is an IEEE754 with a 15 bit exponent + // and 64 bit significand. This is not the same + // as x87 fp80 which has a different binary encoding. + // We can use this Bitwuzla type to get the appropriate + // amount of precision. We just have to be very + // careful which casting between floats and bitvectors. + // + // Note that the number of significand bits includes the "implicit" + // bit (which is not implicit for x87 fp80). + return {15, 64}; + } + case Expr::Int128: { + return {15, 113}; + } + default: + assert( + 0 && + "bitWidth cannot converted to a IEEE-754 binary-* number by Bitwuzla"); + std::abort(); + } +} + +Term BitwuzlaBuilder::castToFloat(const Term &e) { + Sort currentSort = e.sort(); + if (currentSort.is_fp()) { + // Already a float + return e; + } else if (currentSort.is_bv()) { + unsigned bitWidth = currentSort.bv_size(); + switch (bitWidth) { + case Expr::Int16: + case Expr::Int32: + case Expr::Int64: + case Expr::Int128: { + auto out_width = getFloatSortFromBitWidth(bitWidth); + return mk_term(Kind::FP_TO_FP_FROM_BV, {e}, + {out_width.first, out_width.second}); + } + case Expr::Fl80: { + // The bit pattern used by x87 fp80 and what we use in Bitwuzla are + // different + // + // x87 fp80 + // + // Sign Exponent Significand + // [1] [15] [1] [63] + // + // The exponent has bias 16383 and the significand has the integer portion + // as an explicit bit + // + // 79-bit IEEE-754 encoding used in Bitwuzla + // + // Sign Exponent [Significand] + // [1] [15] [63] + // + // Exponent has bias 16383 (2^(15-1) -1) and the significand has + // the integer portion as an implicit bit. + // + // We need to provide the mapping here and also emit a side constraint + // to make sure the explicit bit is appropriately constrained so when + // Bitwuzla generates a model we get the correct bit pattern back. + // + // This assumes Bitwuzla's IEEE semantics, x87 fp80 actually + // has additional semantics due to the explicit bit (See 8.2.2 + // "Unsupported Double Extended-Precision Floating-Point Encodings and + // Pseudo-Denormals" in the Intel 64 and IA-32 Architectures Software + // Developer's Manual) but this encoding means we can't model these + // unsupported values in Bitwuzla. + // + // Note this code must kept in sync with + // `BitwuzlaBuilder::castToBitVector()`. Which performs the inverse + // operation here. + // + // TODO: Experiment with creating a constraint that transforms these + // unsupported bit patterns into a Bitwuzla NaN to approximate the + // behaviour from those values. + + // Note we try very hard here to avoid calling into our functions + // here that do implicit casting so we can never recursively call + // into this function. + Term signBit = mk_term(Kind::BV_EXTRACT, {e}, {79, 79}); + Term exponentBits = mk_term(Kind::BV_EXTRACT, {e}, {78, 64}); + Term significandIntegerBit = mk_term(Kind::BV_EXTRACT, {e}, {63, 63}); + Term significandFractionBits = mk_term(Kind::BV_EXTRACT, {e}, {62, 0}); + + Term ieeeBitPatternAsFloat = mk_term( + Kind::FP_FP, {signBit, exponentBits, significandFractionBits}); + + // Generate side constraint on the significand integer bit. It is not + // used in `ieeeBitPatternAsFloat` so we need to constrain that bit to + // have the correct value so that when Bitwuzla gives a model the bit + // pattern has the right value for x87 fp80. + // + // If the number is a denormal or zero then the implicit integer bit + // is zero otherwise it is one. + Term significandIntegerBitConstrainedValue = + getx87FP80ExplicitSignificandIntegerBit(ieeeBitPatternAsFloat); + Term significandIntegerBitConstraint = + mk_term(Kind::EQUAL, {significandIntegerBit, + significandIntegerBitConstrainedValue}); + + sideConstraints.push_back(significandIntegerBitConstraint); + return ieeeBitPatternAsFloat; + } + default: + llvm_unreachable("Unhandled width when casting bitvector to float"); + } + } else { + llvm_unreachable("Sort cannot be cast to float"); + } +} + +Term BitwuzlaBuilder::castToBitVector(const Term &e) { + Sort currentSort = e.sort(); + if (currentSort.is_bool()) { + return mk_term(Kind::ITE, {e, bvOne(1), bvZero(1)}); + } else if (currentSort.is_bv()) { + // Already a bitvector + return e; + } else if (currentSort.is_fp()) { + // Note this picks a single representation for NaN which means + // `castToBitVector(castToFloat(e))` might not equal `e`. + unsigned exponentBits = currentSort.fp_exp_size(); + unsigned significandBits = + currentSort.fp_sig_size(); // Includes implicit bit + unsigned floatWidth = exponentBits + significandBits; + + switch (floatWidth) { + case Expr::Int16: + case Expr::Int32: + case Expr::Int64: + case Expr::Int128: + return fpToIEEEBV(e); + case 79: { + // This is Expr::Fl80 (64 bit exponent, 15 bit significand) but due to + // the "implicit" bit actually being implicit in x87 fp80 the sum of + // the exponent and significand bitwidth is 79 not 80. + + // Get Bitwuzla's IEEE representation + Term ieeeBits = fpToIEEEBV(e); + + // Construct the x87 fp80 bit representation + Term signBit = mk_term(Kind::BV_EXTRACT, {ieeeBits}, {78, 78}); + Term exponentBits = mk_term(Kind::BV_EXTRACT, {ieeeBits}, {77, 63}); + Term significandIntegerBit = getx87FP80ExplicitSignificandIntegerBit(e); + Term significandFractionBits = + mk_term(Kind::BV_EXTRACT, {ieeeBits}, {62, 0}); + Term x87FP80Bits = mk_term(Kind::BV_CONCAT, + {signBit, exponentBits, significandIntegerBit, + significandFractionBits}); + return x87FP80Bits; + } + default: + llvm_unreachable("Unhandled width when casting float to bitvector"); + } + } else { + llvm_unreachable("Sort cannot be cast to float"); + } +} + +Term BitwuzlaBuilder::getRoundingModeSort(llvm::APFloat::roundingMode rm) { + switch (rm) { + case llvm::APFloat::rmNearestTiesToEven: + return mk_rm_value(RoundingMode::RNE); + case llvm::APFloat::rmTowardPositive: + return mk_rm_value(RoundingMode::RTP); + case llvm::APFloat::rmTowardNegative: + return mk_rm_value(RoundingMode::RTN); + case llvm::APFloat::rmTowardZero: + return mk_rm_value(RoundingMode::RTZ); + case llvm::APFloat::rmNearestTiesToAway: + return mk_rm_value(RoundingMode::RNA); + default: + llvm_unreachable("Unhandled rounding mode"); + } +} + +Term BitwuzlaBuilder::getx87FP80ExplicitSignificandIntegerBit(const Term &e) { +#ifndef NDEBUG + // Check the passed in expression is the right type. + Sort currentSort = e.sort(); + assert(currentSort.is_fp()); + + unsigned exponentBits = currentSort.fp_exp_size(); + unsigned significandBits = currentSort.fp_sig_size(); + assert(exponentBits == 15); + assert(significandBits == 64); +#endif + // If the number is a denormal or zero then the implicit integer bit is zero + // otherwise it is one. Term isDenormal = + Term isDenormal = mk_term(Kind::FP_IS_SUBNORMAL, {e}); + Term isZero = mk_term(Kind::FP_IS_ZERO, {e}); + + // FIXME: Cache these constants somewhere + Sort oneBitBvSort = getBvSort(/*width=*/1); + + Term oneBvOne = mk_bv_value_uint64(oneBitBvSort, 1); + Term zeroBvOne = mk_bv_value_uint64(oneBitBvSort, 0); + + Term significandIntegerBitCondition = orExpr(isDenormal, isZero); + + Term significandIntegerBitConstrainedValue = + mk_term(Kind::ITE, {significandIntegerBitCondition, zeroBvOne, oneBvOne}); + + return significandIntegerBitConstrainedValue; +} +} // namespace klee + +#endif // ENABLE_BITWUZLA diff --git a/lib/Solver/BitwuzlaBuilder.h b/lib/Solver/BitwuzlaBuilder.h new file mode 100644 index 0000000000..9119832f3f --- /dev/null +++ b/lib/Solver/BitwuzlaBuilder.h @@ -0,0 +1,140 @@ +//===-- BitwuzlaBuilder.h --------------------------------------------*- C++ +//-*-====// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#ifndef BITWUZLABUILDER_H_ +#define BITWUZLABUILDER_H_ + +#include "klee/Config/config.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" + +#include +#include + +using namespace bitwuzla; + +namespace klee { + +class BitwuzlaArrayExprHash : public ArrayExprHash { + friend class BitwuzlaBuilder; + +public: + BitwuzlaArrayExprHash(){}; + virtual ~BitwuzlaArrayExprHash(); + void clear(); + void clearUpdates(); +}; + +class BitwuzlaBuilder { +private: + void FPCastWidthAssert(int *width_out, char const *msg); + Term fpToIEEEBV(const Term &); + +protected: + Term bvOne(unsigned width); + Term bvZero(unsigned width); + Term bvMinusOne(unsigned width); + Term bvConst32(unsigned width, uint32_t value); + Term bvConst64(unsigned width, uint64_t value); + Term bvZExtConst(unsigned width, uint64_t value); + Term bvSExtConst(unsigned width, uint64_t value); + Term bvBoolExtract(Term expr, int bit); + Term bvExtract(Term expr, unsigned top, unsigned bottom); + Term eqExpr(Term a, Term b); + + // logical left and right shift (not arithmetic) + Term bvLeftShift(Term expr, unsigned shift); + Term bvRightShift(Term expr, unsigned shift); + Term bvVarLeftShift(Term expr, Term shift); + Term bvVarRightShift(Term expr, Term shift); + Term bvVarArithRightShift(Term expr, Term shift); + + Term notExpr(Term expr); + Term andExpr(Term lhs, Term rhs); + Term orExpr(Term lhs, Term rhs); + Term iffExpr(Term lhs, Term rhs); + + Term bvNotExpr(Term expr); + Term bvAndExpr(Term lhs, Term rhs); + Term bvOrExpr(Term lhs, Term rhs); + Term bvXorExpr(Term lhs, Term rhs); + Term bvSignExtend(Term src, unsigned width); + + // Array operations + Term writeExpr(Term array, Term index, Term value); + Term readExpr(Term array, Term index); + + // ITE-expression constructor + Term iteExpr(Term condition, Term whenTrue, Term whenFalse); + + // Bitvector length + unsigned getBVLength(Term expr); + + // Bitvector comparison + Term bvLtExpr(Term lhs, Term rhs); + Term bvLeExpr(Term lhs, Term rhs); + Term sbvLtExpr(Term lhs, Term rhs); + Term sbvLeExpr(Term lhs, Term rhs); + + Term constructAShrByConstant(Term expr, unsigned shift, Term isSigned); + + Term getInitialArray(const Array *os); + Term getArrayForUpdate(const Array *root, const UpdateNode *un); + + Term constructActual(ref e, int *width_out); + Term construct(ref e, int *width_out); + Term buildArray(const char *name, unsigned indexWidth, unsigned valueWidth); + Term buildConstantArray(const char *name, unsigned indexWidth, + unsigned valueWidth, unsigned value); + + Sort getBoolSort(); + Sort getBvSort(unsigned width); + Sort getArraySort(Sort domainSort, Sort rangeSort); + + std::pair getFloatSortFromBitWidth(unsigned bitWidth); + + // Float casts + Term castToFloat(const Term &e); + Term castToBitVector(const Term &e); + + Term getRoundingModeSort(llvm::APFloat::roundingMode rm); + Term getx87FP80ExplicitSignificandIntegerBit(const Term &e); + + ExprHashMap> constructed; + BitwuzlaArrayExprHash _arr_hash; + bool autoClearConstructCache; + +public: + std::unordered_map> + constant_array_assertions; + // These are additional constraints that are generated during the + // translation to Bitwuzla's constraint language. Clients should assert + // these. + std::vector sideConstraints; + + BitwuzlaBuilder(bool autoClearConstructCache); + ~BitwuzlaBuilder(); + + Term getTrue(); + Term getFalse(); + Term buildFreshBoolConst(); + Term getInitialRead(const Array *os, unsigned index); + + Term construct(ref e) { + Term res = construct(std::move(e), nullptr); + if (autoClearConstructCache) + clearConstructCache(); + return res; + } + void clearConstructCache() { constructed.clear(); } + void clearSideConstraints() { sideConstraints.clear(); } +}; +} // namespace klee + +#endif diff --git a/lib/Solver/BitwuzlaHashConfig.cpp b/lib/Solver/BitwuzlaHashConfig.cpp new file mode 100644 index 0000000000..4ee8cfe429 --- /dev/null +++ b/lib/Solver/BitwuzlaHashConfig.cpp @@ -0,0 +1,20 @@ +//===-- BitwuzlaHashConfig.cpp ---------------------------------------*- C++ +//-*-====// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "BitwuzlaHashConfig.h" +#include + +namespace BitwuzlaHashConfig { +llvm::cl::opt UseConstructHashBitwuzla( + "use-construct-hash-bitwuzla", + llvm::cl::desc( + "Use hash-consing during Bitwuzla query construction (default=true)"), + llvm::cl::init(true), llvm::cl::cat(klee::ExprCat)); +} // namespace BitwuzlaHashConfig diff --git a/lib/Solver/BitwuzlaHashConfig.h b/lib/Solver/BitwuzlaHashConfig.h new file mode 100644 index 0000000000..a4a2d97bb1 --- /dev/null +++ b/lib/Solver/BitwuzlaHashConfig.h @@ -0,0 +1,25 @@ +//===-- BitwuzlaHashConfig.h -----------------------------------------*- C++ +//-*-====// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_BITWUZLAHASHCONFIG_H +#define KLEE_BITWUZLAHASHCONFIG_H + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/Support/CommandLine.h" +DISABLE_WARNING_POP + +#include + +namespace BitwuzlaHashConfig { +extern llvm::cl::opt UseConstructHashBitwuzla; +} // namespace BitwuzlaHashConfig +#endif // KLEE_BITWUZLAHASHCONFIG_H diff --git a/lib/Solver/BitwuzlaSolver.cpp b/lib/Solver/BitwuzlaSolver.cpp new file mode 100644 index 0000000000..3b5d9acfe1 --- /dev/null +++ b/lib/Solver/BitwuzlaSolver.cpp @@ -0,0 +1,991 @@ + +//===-- BitwuzlaSolver.cpp ---------------------------------------*-C++-*-====// +// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/Config/config.h" + +#ifdef ENABLE_BITWUZLA + +#include "BitwuzlaBuilder.h" +#include "BitwuzlaSolver.h" + +#include "klee/ADT/Incremental.h" +#include "klee/ADT/SparseStorage.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" +#include "klee/Support/ErrorHandling.h" +#include "klee/Support/FileHandling.h" +#include "klee/Support/OptionCategories.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" + +#include +#include +#include + +#include "bitwuzla/cpp/bitwuzla.h" + +namespace { +// NOTE: Very useful for debugging Bitwuzla behaviour. These files can be given +// to the Bitwuzla binary to replay all Bitwuzla API calls using its `-log` +// option. + +llvm::cl::opt BitwuzlaValidateModels( + "debug-bitwuzla-validate-models", llvm::cl::init(false), + llvm::cl::desc( + "When generating Bitwuzla models validate these against the query"), + llvm::cl::cat(klee::SolvingCat)); + +llvm::cl::opt BitwuzlaVerbosityLevel( + "debug-bitwuzla-verbosity", llvm::cl::init(0), + llvm::cl::desc("Bitwuzla verbosity level (default=0)"), + llvm::cl::cat(klee::SolvingCat)); +} // namespace + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/Support/ErrorHandling.h" +DISABLE_WARNING_POP + +namespace { +bool interrupted = false; + +void signal_handler(int signum) { interrupted = true; } +} // namespace + +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()) {} + +bool BitwuzlaTerminator::terminate() { + time::Point end = time::getWallTime(); + if ((end - start).toMicroseconds() >= time_limit_micro) { + _isTimeout = true; + return true; + } + if (interrupted) { + return true; + } + return false; +} + +using ConstraintFrames = inc_vector>; +using ExprIncMap = inc_umap>; +using BitwuzlaASTIncMap = inc_umap; +using ExprIncSet = + inc_uset, klee::util::ExprHash, klee::util::ExprCmp>; +using BitwuzlaASTIncSet = inc_uset; + +extern void dump(const ConstraintFrames &); + +class ConstraintQuery { +private: + // this should be used when only query is needed, se comment below + ref expr; + +public: + // KLEE Queries are validity queries i.e. + // ∀ X Constraints(X) → query(X) + // but Bitwuzla works in terms of satisfiability so instead we ask the + // negation of the equivalent i.e. + // ∃ X Constraints(X) ∧ ¬ query(X) + // so this `constraints` field contains: Constraints(X) ∧ ¬ query(X) + ConstraintFrames constraints; + + explicit ConstraintQuery() {} + + explicit ConstraintQuery(const ConstraintFrames &frames, const ref &e) + : expr(e), constraints(frames) {} + explicit ConstraintQuery(ConstraintFrames &&frames, ref &&e) + : expr(std::move(e)), constraints(std::move(frames)) {} + + explicit ConstraintQuery(const Query &q, bool incremental) : expr(q.expr) { + if (incremental) { + for (auto &constraint : q.constraints.cs()) { + constraints.v.push_back(constraint); + constraints.push(); + } + } else { + const auto &other = q.constraints.cs(); + constraints.v.reserve(other.size()); + constraints.v.insert(constraints.v.end(), other.begin(), other.end()); + } + if (q.expr->getWidth() == Expr::Bool && !q.expr->isFalse()) + constraints.v.push_back(NotExpr::create(q.expr)); + } + + size_t size() const { return constraints.v.size(); } + + ref getOriginalQueryExpr() const { return expr; } + + ConstraintQuery withFalse() const { + return ConstraintQuery(ConstraintFrames(constraints), Expr::createFalse()); + } + + std::vector gatherArrays() const { + std::vector arrays; + findObjects(constraints.v.begin(), constraints.v.end(), arrays); + return arrays; + } +}; + +enum class ObjectAssignment { + NotNeeded, + NeededForObjectsFromEnv, + NeededForObjectsFromQuery +}; + +struct BitwuzlaSolverEnv { + using arr_vec = std::vector; + inc_vector objects; + arr_vec objectsForGetModel; + ExprIncMap bitwuzla_ast_expr_to_klee_expr; + BitwuzlaASTIncSet expr_to_track; + inc_umap usedArrayBytes; + ExprIncSet symbolicObjects; + + explicit BitwuzlaSolverEnv() = default; + explicit BitwuzlaSolverEnv(const arr_vec &objects); + + void pop(size_t popSize); + void push(); + void clear(); + + const arr_vec *getObjectsForGetModel(ObjectAssignment oa) const; +}; + +BitwuzlaSolverEnv::BitwuzlaSolverEnv(const arr_vec &objects) + : objectsForGetModel(objects) {} + +void BitwuzlaSolverEnv::pop(size_t popSize) { + if (popSize == 0) + return; + objects.pop(popSize); + objectsForGetModel.clear(); + bitwuzla_ast_expr_to_klee_expr.pop(popSize); + expr_to_track.pop(popSize); + usedArrayBytes.pop(popSize); + symbolicObjects.pop(popSize); +} + +void BitwuzlaSolverEnv::push() { + objects.push(); + bitwuzla_ast_expr_to_klee_expr.push(); + expr_to_track.push(); + usedArrayBytes.push(); + symbolicObjects.push(); +} + +void BitwuzlaSolverEnv::clear() { + objects.clear(); + objectsForGetModel.clear(); + bitwuzla_ast_expr_to_klee_expr.clear(); + expr_to_track.clear(); + usedArrayBytes.clear(); + symbolicObjects.clear(); +} + +const BitwuzlaSolverEnv::arr_vec * +BitwuzlaSolverEnv::getObjectsForGetModel(ObjectAssignment oa) const { + switch (oa) { + case ObjectAssignment::NotNeeded: + return nullptr; + case ObjectAssignment::NeededForObjectsFromEnv: + return &objectsForGetModel; + case ObjectAssignment::NeededForObjectsFromQuery: + return &objects.v; + default: + llvm_unreachable("unknown object assignment"); + } +} + +class BitwuzlaSolverImpl : public SolverImpl { +protected: + std::unique_ptr builder; + Options solverParameters; + +private: + time::Span timeout; + SolverImpl::SolverRunStatus runStatusCode; + + bool internalRunSolver(const ConstraintQuery &query, BitwuzlaSolverEnv &env, + ObjectAssignment needObjects, + std::vector> *values, + ValidityCore *validityCore, bool &hasSolution); + + SolverImpl::SolverRunStatus handleSolverResponse( + Bitwuzla &theSolver, Result satisfiable, const BitwuzlaSolverEnv &env, + ObjectAssignment needObjects, + std::vector> *values, bool &hasSolution); + +protected: + BitwuzlaSolverImpl(); + + virtual Bitwuzla &initNativeBitwuzla(const ConstraintQuery &query, + BitwuzlaASTIncSet &assertions) = 0; + virtual void deinitNativeBitwuzla(Bitwuzla &theSolver) = 0; + virtual void push(Bitwuzla &s) = 0; + + bool computeTruth(const ConstraintQuery &, BitwuzlaSolverEnv &env, + bool &isValid); + bool computeValue(const ConstraintQuery &, BitwuzlaSolverEnv &env, + ref &result); + bool computeInitialValues(const ConstraintQuery &, BitwuzlaSolverEnv &env, + std::vector> &values, + bool &hasSolution); + bool check(const ConstraintQuery &query, BitwuzlaSolverEnv &env, + ref &result); + bool computeValidityCore(const ConstraintQuery &query, BitwuzlaSolverEnv &env, + ValidityCore &validityCore, bool &isValid); + +public: + char *getConstraintLog(const Query &) final; + SolverImpl::SolverRunStatus getOperationStatusCode() final; + void setCoreSolverTimeout(time::Span _timeout) final { timeout = _timeout; } + void enableUnsatCore() { + solverParameters.set(Option::PRODUCE_UNSAT_CORES, true); + } + void disableUnsatCore() { + solverParameters.set(Option::PRODUCE_UNSAT_CORES, false); + } + + // pass virtual functions to children + using SolverImpl::check; + using SolverImpl::computeInitialValues; + using SolverImpl::computeTruth; + using SolverImpl::computeValidityCore; + using SolverImpl::computeValue; +}; + +void deleteNativeBitwuzla(std::optional &theSolver) { + theSolver.reset(); +} + +BitwuzlaSolverImpl::BitwuzlaSolverImpl() + : runStatusCode(SolverImpl::SOLVER_RUN_STATUS_FAILURE) { + builder = std::unique_ptr(new BitwuzlaBuilder( + /*autoClearConstructCache=*/false)); + assert(builder && "unable to create BitwuzlaBuilder"); + + solverParameters.set(Option::PRODUCE_MODELS, true); + + setCoreSolverTimeout(timeout); + + if (ProduceUnsatCore) { + enableUnsatCore(); + } else { + disableUnsatCore(); + } + + // Set verbosity + if (BitwuzlaVerbosityLevel > 0) { + solverParameters.set(Option::VERBOSITY, BitwuzlaVerbosityLevel); + } + + if (BitwuzlaValidateModels) { + solverParameters.set(Option::DBG_CHECK_MODEL, true); + } +} + +char *BitwuzlaSolverImpl::getConstraintLog(const Query &query) { + std::stringstream outputLog; + + // We use a different builder here because we don't want to interfere + // with the solver's builder because it may change the solver builder's + // cache. + std::unique_ptr tempBuilder(new BitwuzlaBuilder(false)); + ConstantArrayFinder constant_arrays_in_query; + + std::function(const Term &)> constantsIn = + [&constantsIn](const Term &term) { + if (term.is_const()) { + return std::unordered_set{term}; + } + std::unordered_set symbols; + for (const auto &child : term.children()) { + for (const auto &childsSymbol : constantsIn(child)) { + symbols.emplace(childsSymbol); + } + } + return symbols; + }; + + std::function declareLog = + [&outputLog](const Term &term) { + outputLog << "(declare-fun " << term.str(10) << " () " + << term.sort().str() << ")\n"; + }; + std::function assertLog = [&outputLog](const Term &term) { + outputLog << "(assert " << term.str(10) << ")\n"; + }; + + std::vector assertions; + std::unordered_set assertionSymbols; + + for (auto const &constraint : query.constraints.cs()) { + Term constraintTerm = tempBuilder->construct(constraint); + assertions.push_back(std::move(constraintTerm)); + constant_arrays_in_query.visit(constraint); + } + + // KLEE Queries are validity queries i.e. + // ∀ X Constraints(X) → query(X) + // but Bitwuzla works in terms of satisfiability so instead we ask the + // the negation of the equivalent i.e. + // ∃ X Constraints(X) ∧ ¬ query(X) + assertions.push_back( + mk_term(Kind::NOT, {tempBuilder->construct(query.expr)})); + constant_arrays_in_query.visit(query.expr); + + for (auto const &constant_array : constant_arrays_in_query.results) { + for (auto const &arrayIndexValueExpr : + tempBuilder->constant_array_assertions[constant_array]) { + assertions.push_back(arrayIndexValueExpr); + } + } + + for (const Term &constraintTerm : assertions) { + std::unordered_set constantsInConstraintTerm = + constantsIn(constraintTerm); + assertionSymbols.insert(constantsInConstraintTerm.begin(), + constantsInConstraintTerm.end()); + } + + for (const Term &symbol : assertionSymbols) { + declareLog(symbol); + } + for (const Term &constraint : assertions) { + assertLog(constraint); + } + + outputLog << "(check-sat)\n"; + + // Client is responsible for freeing the returned C-string + return strdup(outputLog.str().c_str()); +} + +bool BitwuzlaSolverImpl::computeTruth(const ConstraintQuery &query, + BitwuzlaSolverEnv &env, bool &isValid) { + bool hasSolution = false; // to remove compiler warning + bool status = internalRunSolver(query, /*env=*/env, + ObjectAssignment::NotNeeded, /*values=*/NULL, + /*validityCore=*/NULL, hasSolution); + isValid = !hasSolution; + return status; +} + +bool BitwuzlaSolverImpl::computeValue(const ConstraintQuery &query, + BitwuzlaSolverEnv &env, + ref &result) { + std::vector> values; + bool hasSolution; + + // Find the object used in the expression, and compute an assignment + // for them. + findSymbolicObjects(query.getOriginalQueryExpr(), env.objectsForGetModel); + if (!computeInitialValues(query.withFalse(), env, values, hasSolution)) + return false; + assert(hasSolution && "state has invalid constraint set"); + + // Evaluate the expression with the computed assignment. + Assignment a(env.objectsForGetModel, values); + result = a.evaluate(query.getOriginalQueryExpr()); + + return true; +} + +bool BitwuzlaSolverImpl::computeInitialValues( + const ConstraintQuery &query, BitwuzlaSolverEnv &env, + std::vector> &values, bool &hasSolution) { + return internalRunSolver(query, env, + ObjectAssignment::NeededForObjectsFromEnv, &values, + /*validityCore=*/NULL, hasSolution); +} + +bool BitwuzlaSolverImpl::check(const ConstraintQuery &query, + BitwuzlaSolverEnv &env, + ref &result) { + std::vector> values; + ValidityCore validityCore; + bool hasSolution = false; + bool status = + internalRunSolver(query, env, ObjectAssignment::NeededForObjectsFromQuery, + &values, &validityCore, hasSolution); + if (status) { + result = hasSolution + ? (SolverResponse *)new InvalidResponse(env.objects.v, values) + : (SolverResponse *)new ValidResponse(validityCore); + } + return status; +} + +bool BitwuzlaSolverImpl::computeValidityCore(const ConstraintQuery &query, + BitwuzlaSolverEnv &env, + ValidityCore &validityCore, + bool &isValid) { + bool hasSolution = false; // to remove compiler warning + bool status = + internalRunSolver(query, /*env=*/env, ObjectAssignment::NotNeeded, + /*values=*/NULL, &validityCore, hasSolution); + isValid = !hasSolution; + return status; +} + +bool BitwuzlaSolverImpl::internalRunSolver( + const ConstraintQuery &query, BitwuzlaSolverEnv &env, + ObjectAssignment needObjects, + std::vector> *values, + ValidityCore *validityCore, bool &hasSolution) { + TimerStatIncrementer t(stats::queryTime); + runStatusCode = SolverImpl::SOLVER_RUN_STATUS_FAILURE; + + std::unordered_set all_constant_arrays_in_query; + BitwuzlaASTIncSet exprs; + + for (size_t i = 0; i < query.constraints.framesSize(); + i++, env.push(), exprs.push()) { + ConstantArrayFinder constant_arrays_in_query; + env.symbolicObjects.insert(query.constraints.begin(i), + query.constraints.end(i)); + // FIXME: findSymbolicObjects template does not support inc_uset::iterator + // findSymbolicObjects(env.symbolicObjects.begin(-1), + // env.symbolicObjects.end(-1), env.objects.v); + std::vector> tmp(env.symbolicObjects.begin(-1), + env.symbolicObjects.end(-1)); + findSymbolicObjects(tmp.begin(), tmp.end(), env.objects.v); + for (auto cs_it = query.constraints.begin(i), + cs_ite = query.constraints.end(i); + cs_it != cs_ite; cs_it++) { + const auto &constraint = *cs_it; + Term bitwuzlaConstraint = builder->construct(constraint); + if (ProduceUnsatCore && validityCore) { + env.bitwuzla_ast_expr_to_klee_expr.insert( + {bitwuzlaConstraint, constraint}); + env.expr_to_track.insert(bitwuzlaConstraint); + } + + exprs.insert(bitwuzlaConstraint); + + constant_arrays_in_query.visit(constraint); + + std::vector> reads; + findReads(constraint, true, reads); + for (const auto &readExpr : reads) { + auto readFromArray = readExpr->updates.root; + assert(readFromArray); + env.usedArrayBytes[readFromArray].insert(readExpr->index); + } + } + + for (auto constant_array : constant_arrays_in_query.results) { + if (all_constant_arrays_in_query.count(constant_array)) + continue; + all_constant_arrays_in_query.insert(constant_array); + const auto &cas = builder->constant_array_assertions[constant_array]; + exprs.insert(cas.begin(), cas.end()); + } + + // Assert an generated side constraints we have to this last so that all + // other constraints have been traversed so we have all the side constraints + // needed. + exprs.insert(builder->sideConstraints.begin(), + builder->sideConstraints.end()); + } + exprs.pop(1); // drop last empty frame + + ++stats::solverQueries; + if (!env.objects.v.empty()) + ++stats::queryCounterexamples; + + // Prepare signal handler and terminator fot bitwuzla + auto timeoutInMicroSeconds = static_cast(timeout.toMicroseconds()); + if (!timeoutInMicroSeconds) + timeoutInMicroSeconds = UINT_MAX; + BitwuzlaTerminator terminator(timeoutInMicroSeconds); + + struct sigaction action, old_action; + action.sa_handler = signal_handler; + action.sa_flags = 0; + sigaction(SIGINT, &action, &old_action); + + Bitwuzla &theSolver = initNativeBitwuzla(query, exprs); + theSolver.configure_terminator(&terminator); + + for (size_t i = 0; i < exprs.framesSize(); i++) { + push(theSolver); + for (auto it = exprs.begin(i), ie = exprs.end(i); it != ie; ++it) { + theSolver.assert_formula(*it); + } + } + + Result satisfiable = theSolver.check_sat(); + theSolver.configure_terminator(nullptr); + runStatusCode = handleSolverResponse(theSolver, satisfiable, env, needObjects, + values, hasSolution); + sigaction(SIGINT, &old_action, nullptr); + + if (runStatusCode == SolverImpl::SOLVER_RUN_STATUS_FAILURE) { + if (terminator.isTimeout()) { + runStatusCode = SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; + } + if (interrupted) { + runStatusCode = SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED; + } + } + + if (ProduceUnsatCore && validityCore && satisfiable == Result::UNSAT) { + const std::vector bitwuzla_unsat_core = theSolver.get_unsat_core(); + const std::unordered_set bitwuzla_term_unsat_core( + bitwuzla_unsat_core.begin(), bitwuzla_unsat_core.end()); + + constraints_ty unsatCore; + for (const auto &bitwuzla_constraint : env.expr_to_track) { + if (bitwuzla_term_unsat_core.count(bitwuzla_constraint)) { + ref constraint = + env.bitwuzla_ast_expr_to_klee_expr[bitwuzla_constraint]; + unsatCore.insert(constraint); + } + } + assert(validityCore && "validityCore cannot be nullptr"); + *validityCore = ValidityCore(unsatCore, query.getOriginalQueryExpr()); + + stats::validQueriesSize += theSolver.get_assertions().size(); + stats::validityCoresSize += bitwuzla_unsat_core.size(); + ++stats::queryValidityCores; + } + + deinitNativeBitwuzla(theSolver); + + // Clear the builder's cache to prevent memory usage exploding. + // By using ``autoClearConstructCache=false`` and clearning now + // we allow Term expressions to be shared from an entire + // ``Query`` rather than only sharing within a single call to + // ``builder->construct()``. + builder->clearConstructCache(); + builder->clearSideConstraints(); + if (runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE || + runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE) { + if (hasSolution) { + ++stats::queriesInvalid; + } else { + ++stats::queriesValid; + } + return true; // success + } + if (runStatusCode == SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED) { + raise(SIGINT); + } + return false; // failed +} + +SolverImpl::SolverRunStatus BitwuzlaSolverImpl::handleSolverResponse( + Bitwuzla &theSolver, Result satisfiable, const BitwuzlaSolverEnv &env, + ObjectAssignment needObjects, + std::vector> *values, bool &hasSolution) { + switch (satisfiable) { + case Result::SAT: { + hasSolution = true; + auto objects = env.getObjectsForGetModel(needObjects); + if (!objects) { + // No assignment is needed + assert(!values); + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + assert(values && "values cannot be nullptr"); + + values->reserve(objects->size()); + for (auto array : *objects) { + SparseStorage data; + + if (env.usedArrayBytes.count(array)) { + std::unordered_set offsetValues; + for (const ref &offsetExpr : env.usedArrayBytes.at(array)) { + Term arrayElementOffsetExpr = + theSolver.get_value(builder->construct(offsetExpr)); + + uint64_t concretizedOffsetValue = + std::stoull(arrayElementOffsetExpr.value(10)); + offsetValues.insert(concretizedOffsetValue); + } + + for (unsigned offset : offsetValues) { + // We can't use Term here so have to do ref counting manually + Term initial_read = builder->getInitialRead(array, offset); + Term initial_read_expr = theSolver.get_value(initial_read); + + uint64_t arrayElementValue = + std::stoull(initial_read_expr.value(10)); + data.store(offset, arrayElementValue); + } + } + + values->emplace_back(std::move(data)); + } + + assert(values->size() == objects->size()); + + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + case Result::UNSAT: + hasSolution = false; + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + case Result::UNKNOWN: { + return SolverImpl::SOLVER_RUN_STATUS_FAILURE; + } + default: + llvm_unreachable("unhandled Bitwuzla result"); + } +} + +SolverImpl::SolverRunStatus BitwuzlaSolverImpl::getOperationStatusCode() { + return runStatusCode; +} + +class BitwuzlaNonIncSolverImpl final : public BitwuzlaSolverImpl { +private: + std::optional theSolver; + +public: + BitwuzlaNonIncSolverImpl() = default; + + /// implementation of BitwuzlaSolverImpl interface + Bitwuzla &initNativeBitwuzla(const ConstraintQuery &query, + BitwuzlaASTIncSet &assertions) override { + theSolver.emplace(solverParameters); + return theSolver.value(); + } + + void deinitNativeBitwuzla(Bitwuzla &) override { + deleteNativeBitwuzla(theSolver); + } + + void push(Bitwuzla &s) override {} + + /// implementation of the SolverImpl interface + bool computeTruth(const Query &query, bool &isValid) override { + BitwuzlaSolverEnv env; + return BitwuzlaSolverImpl::computeTruth(ConstraintQuery(query, false), env, + isValid); + } + bool computeValue(const Query &query, ref &result) override { + BitwuzlaSolverEnv env; + return BitwuzlaSolverImpl::computeValue(ConstraintQuery(query, false), env, + result); + } + bool computeInitialValues(const Query &query, + const std::vector &objects, + std::vector> &values, + bool &hasSolution) override { + BitwuzlaSolverEnv env(objects); + return BitwuzlaSolverImpl::computeInitialValues( + ConstraintQuery(query, false), env, values, hasSolution); + } + bool check(const Query &query, ref &result) override { + BitwuzlaSolverEnv env; + return BitwuzlaSolverImpl::check(ConstraintQuery(query, false), env, + result); + } + bool computeValidityCore(const Query &query, ValidityCore &validityCore, + bool &isValid) override { + BitwuzlaSolverEnv env; + return BitwuzlaSolverImpl::computeValidityCore( + ConstraintQuery(query, false), env, validityCore, isValid); + } + void notifyStateTermination(std::uint32_t id) override {} +}; + +BitwuzlaSolver::BitwuzlaSolver() + : Solver(std::make_unique()) {} + +struct ConstraintDistance { + size_t toPopSize = 0; + ConstraintQuery toPush; + + explicit ConstraintDistance() {} + ConstraintDistance(const ConstraintQuery &q) : toPush(q) {} + explicit ConstraintDistance(size_t toPopSize, const ConstraintQuery &q) + : toPopSize(toPopSize), toPush(q) {} + + size_t getDistance() const { return toPopSize + toPush.size(); } + + bool isOnlyPush() const { return toPopSize == 0; } + + void dump() const { + llvm::errs() << "ConstraintDistance: pop: " << toPopSize << "; push:\n"; + klee::dump(toPush.constraints); + } +}; + +class BitwuzlaIncNativeSolver { +private: + std::optional nativeSolver; + Options solverParameters; + /// underlying solver frames + /// saved only for calculating distances from next queries + ConstraintFrames frames; + + void pop(size_t popSize); + +public: + BitwuzlaSolverEnv env; + std::uint32_t stateID = 0; + bool isRecycled = false; + + BitwuzlaIncNativeSolver(Options solverParameters) + : solverParameters(solverParameters) {} + ~BitwuzlaIncNativeSolver(); + + void clear(); + + void distance(const ConstraintQuery &query, ConstraintDistance &delta) const; + + void popPush(ConstraintDistance &delta); + + Bitwuzla &getOrInit(); + + bool isConsistent() const { + klee_warning("Empty isConsistent() check"); + return true; + } + + void dump() const { ::klee::dump(frames); } +}; + +void BitwuzlaIncNativeSolver::pop(size_t popSize) { + if (!nativeSolver.has_value() || !popSize) + return; + nativeSolver.value().pop(popSize); +} + +void BitwuzlaIncNativeSolver::popPush(ConstraintDistance &delta) { + env.pop(delta.toPopSize); + pop(delta.toPopSize); + frames.pop(delta.toPopSize); + frames.extend(delta.toPush.constraints); +} + +Bitwuzla &BitwuzlaIncNativeSolver::getOrInit() { + if (!nativeSolver.has_value()) { + nativeSolver.emplace(solverParameters); + } + return nativeSolver.value(); +} + +BitwuzlaIncNativeSolver::~BitwuzlaIncNativeSolver() { + if (nativeSolver.has_value()) { + deleteNativeBitwuzla(nativeSolver); + } +} + +void BitwuzlaIncNativeSolver::clear() { + if (!nativeSolver.has_value()) + return; + env.clear(); + frames.clear(); + nativeSolver.emplace(solverParameters); + isRecycled = false; +} + +void BitwuzlaIncNativeSolver::distance(const ConstraintQuery &query, + ConstraintDistance &delta) const { + auto sit = frames.v.begin(); + auto site = frames.v.end(); + auto qit = query.constraints.v.begin(); + auto qite = query.constraints.v.end(); + auto it = frames.begin(); + auto ite = frames.end(); + size_t intersect = 0; + for (; it != ite && sit != site && qit != qite && *sit == *qit; it++) { + size_t frame_size = *it; + for (size_t i = 0; + i < frame_size && sit != site && qit != qite && *sit == *qit; + i++, sit++, qit++, intersect++) { + } + } + for (; sit != site && qit != qite && *sit == *qit; + sit++, qit++, intersect++) { + } + size_t toPop, extraTakeFromOther; + ConstraintFrames d; + if (sit == site) { // solver frames ended + toPop = 0; + extraTakeFromOther = 0; + } else { + frames.takeBefore(intersect, toPop, extraTakeFromOther); + } + query.constraints.takeAfter(intersect - extraTakeFromOther, d); + ConstraintQuery q(std::move(d), query.getOriginalQueryExpr()); + delta = ConstraintDistance(toPop, std::move(q)); +} + +class BitwuzlaTreeSolverImpl final : public BitwuzlaSolverImpl { +private: + using solvers_ty = std::vector>; + using solvers_it = solvers_ty::iterator; + + const size_t maxSolvers; + std::unique_ptr currentSolver = nullptr; + solvers_ty solvers; + + void findSuitableSolver(const ConstraintQuery &query, + ConstraintDistance &delta); + void setSolver(solvers_it &it, bool recycle = false); + ConstraintQuery prepare(const Query &q); + +public: + BitwuzlaTreeSolverImpl(size_t maxSolvers) : maxSolvers(maxSolvers){}; + + /// implementation of BitwuzlaSolverImpl interface + Bitwuzla &initNativeBitwuzla(const ConstraintQuery &query, + BitwuzlaASTIncSet &assertions) override { + return currentSolver->getOrInit(); + } + void deinitNativeBitwuzla(Bitwuzla &theSolver) override { + assert(currentSolver->isConsistent()); + solvers.push_back(std::move(currentSolver)); + } + void push(Bitwuzla &s) override { s.push(1); } + + /// implementation of the SolverImpl interface + bool computeTruth(const Query &query, bool &isValid) override; + bool computeValue(const Query &query, ref &result) override; + bool computeInitialValues(const Query &query, + const std::vector &objects, + std::vector> &values, + bool &hasSolution) override; + bool check(const Query &query, ref &result) override; + bool computeValidityCore(const Query &query, ValidityCore &validityCore, + bool &isValid) override; + + void notifyStateTermination(std::uint32_t id) override; +}; + +void BitwuzlaTreeSolverImpl::setSolver(solvers_it &it, bool recycle) { + assert(it != solvers.end()); + currentSolver = std::move(*it); + solvers.erase(it); + currentSolver->isRecycled = false; + if (recycle) + currentSolver->clear(); +} + +void BitwuzlaTreeSolverImpl::findSuitableSolver(const ConstraintQuery &query, + ConstraintDistance &delta) { + ConstraintDistance min_delta; + auto min_distance = std::numeric_limits::max(); + auto min_it = solvers.end(); + auto free_it = solvers.end(); + for (auto it = solvers.begin(), ite = min_it; it != ite; it++) { + if ((*it)->isRecycled) + free_it = it; + (*it)->distance(query, delta); + if (delta.isOnlyPush()) { + setSolver(it); + return; + } + auto distance = delta.getDistance(); + if (distance < min_distance) { + min_delta = delta; + min_distance = distance; + min_it = it; + } + } + if (solvers.size() < maxSolvers) { + delta = ConstraintDistance(query); + if (delta.getDistance() < min_distance) { + // it is cheaper to create new solver + if (free_it == solvers.end()) + currentSolver = + std::make_unique(solverParameters); + else + setSolver(free_it, /*recycle=*/true); + return; + } + } + assert(min_it != solvers.end()); + delta = min_delta; + setSolver(min_it); +} + +ConstraintQuery BitwuzlaTreeSolverImpl::prepare(const Query &q) { + ConstraintDistance delta; + ConstraintQuery query(q, true); + findSuitableSolver(query, delta); + assert(currentSolver->isConsistent()); + currentSolver->stateID = q.id; + currentSolver->popPush(delta); + return delta.toPush; +} + +bool BitwuzlaTreeSolverImpl::computeTruth(const Query &query, bool &isValid) { + auto q = prepare(query); + return BitwuzlaSolverImpl::computeTruth(q, currentSolver->env, isValid); +} + +bool BitwuzlaTreeSolverImpl::computeValue(const Query &query, + ref &result) { + auto q = prepare(query); + return BitwuzlaSolverImpl::computeValue(q, currentSolver->env, result); +} + +bool BitwuzlaTreeSolverImpl::computeInitialValues( + const Query &query, const std::vector &objects, + std::vector> &values, bool &hasSolution) { + auto q = prepare(query); + currentSolver->env.objectsForGetModel = objects; + return BitwuzlaSolverImpl::computeInitialValues(q, currentSolver->env, values, + hasSolution); +} + +bool BitwuzlaTreeSolverImpl::check(const Query &query, + ref &result) { + auto q = prepare(query); + return BitwuzlaSolverImpl::check(q, currentSolver->env, result); +} + +bool BitwuzlaTreeSolverImpl::computeValidityCore(const Query &query, + ValidityCore &validityCore, + bool &isValid) { + auto q = prepare(query); + return BitwuzlaSolverImpl::computeValidityCore(q, currentSolver->env, + validityCore, isValid); +} + +void BitwuzlaTreeSolverImpl::notifyStateTermination(std::uint32_t id) { + for (auto &s : solvers) + if (s->stateID == id) + s->isRecycled = true; +} + +BitwuzlaTreeSolver::BitwuzlaTreeSolver(unsigned maxSolvers) + : Solver(std::make_unique(maxSolvers)) {} + +} // namespace klee +#endif // ENABLE_BITWUZLA diff --git a/lib/Solver/BitwuzlaSolver.h b/lib/Solver/BitwuzlaSolver.h new file mode 100644 index 0000000000..613b416c5a --- /dev/null +++ b/lib/Solver/BitwuzlaSolver.h @@ -0,0 +1,22 @@ +#ifndef BITWUZLASOLVER_H_ +#define BITWUZLASOLVER_H_ + +#include "klee/Solver/Solver.h" + +namespace klee { + +/// BitwuzlaSolver - A complete solver based on Bitwuzla +class BitwuzlaSolver : public Solver { +public: + /// BitwuzlaSolver - Construct a new BitwuzlaSolver. + BitwuzlaSolver(); +}; + +class BitwuzlaTreeSolver : public Solver { +public: + BitwuzlaTreeSolver(unsigned maxSolvers); +}; + +} // namespace klee + +#endif diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 9ee7805b64..b4523d1594 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -9,6 +9,9 @@ add_library(kleaverSolver AlphaEquivalenceSolver.cpp AssignmentValidatingSolver.cpp + BitwuzlaBuilder.cpp + BitwuzlaHashConfig.cpp + BitwuzlaSolver.cpp CachingSolver.cpp CexCachingSolver.cpp ConstantDivision.cpp @@ -49,7 +52,6 @@ target_include_directories(kleaverSolver PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INC target_compile_options(kleaverSolver PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions(kleaverSolver PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) - install(TARGETS kleaverSolver EXPORT run_klee DESTINATION "${RUN_KLEE_LIB_DEST}" diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index ff6f9cf76e..a82dfc6a44 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// +#include "BitwuzlaSolver.h" #include "MetaSMTSolver.h" #include "STPSolver.h" #include "Z3Solver.h" @@ -28,7 +29,7 @@ DISABLE_WARNING_POP namespace klee { std::unique_ptr createCoreSolver(CoreSolverType cst) { - bool isTreeSolver = cst == Z3_TREE_SOLVER; + bool isTreeSolver = (cst == Z3_TREE_SOLVER || cst == BITWUZLA_TREE_SOLVER); if (!isTreeSolver && MaxSolversApproxTreeInc > 0) klee_warning("--%s option is ignored because --%s is not z3-tree", MaxSolversApproxTreeInc.ArgStr.str().c_str(), @@ -74,13 +75,28 @@ std::unique_ptr createCoreSolver(CoreSolverType cst) { if (isTreeSolver) { if (MaxSolversApproxTreeInc > 0) return std::make_unique(type, MaxSolversApproxTreeInc); - klee_warning("--%s is 0, so falling back to non tree-incremental solver", + klee_warning("--%s is 0, so falling back to non tree-incremental solver ", MaxSolversApproxTreeInc.ArgStr.str().c_str()); } return std::make_unique(type); #else klee_message("Not compiled with Z3 support"); return NULL; +#endif + case BITWUZLA_TREE_SOLVER: + case BITWUZLA_SOLVER: +#ifdef ENABLE_BITWUZLA + klee_message("Using Bitwuzla solver backend"); + if (isTreeSolver) { + if (MaxSolversApproxTreeInc > 0) + return std::make_unique(MaxSolversApproxTreeInc); + klee_warning("--%s is 0, so falling back to non tree-incremental solver", + MaxSolversApproxTreeInc.ArgStr.str().c_str()); + } + return std::make_unique(); +#else + klee_message("Not compiled with Bitwuzla support"); + return NULL; #endif case NO_SOLVER: klee_message("Invalid solver"); diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index 4974abe1f8..41f8324e7c 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -186,15 +186,23 @@ cl::opt MetaSMTBackend( #endif /* ENABLE_METASMT */ // Pick the default core solver based on configuration -#ifdef ENABLE_Z3 +#ifdef ENABLE_BITWUZLA +#define STP_IS_DEFAULT_STR "" +#define METASMT_IS_DEFAULT_STR "" +#define Z3_IS_DEFAULT_STR "" +#define BITWUZLA_IS_DEFAULT_STR " (default)" +#define DEFAULT_CORE_SOLVER BITWUZLA_SOLVER +#elif ENABLE_Z3 #define STP_IS_DEFAULT_STR "" #define METASMT_IS_DEFAULT_STR "" #define Z3_IS_DEFAULT_STR " (default)" +#define BITWUZLA_IS_DEFAULT_STR "" #define DEFAULT_CORE_SOLVER Z3_SOLVER #elif ENABLE_STP #define STP_IS_DEFAULT_STR " (default)" #define METASMT_IS_DEFAULT_STR "" #define Z3_IS_DEFAULT_STR "" +#define BITWUZLA_IS_DEFAULT_STR "" #define DEFAULT_CORE_SOLVER STP_SOLVER #elif ENABLE_METASMT #define STP_IS_DEFAULT_STR "" @@ -202,6 +210,7 @@ cl::opt MetaSMTBackend( #define Z3_IS_DEFAULT_STR "" #define DEFAULT_CORE_SOLVER METASMT_SOLVER #define Z3_IS_DEFAULT_STR "" +#define BITWUZLA_IS_DEFAULT_STR "" #else #error "Unsupported solver configuration" #endif @@ -209,6 +218,10 @@ cl::opt MetaSMTBackend( cl::opt CoreSolverToUse( "solver-backend", cl::desc("Specifiy the core solver backend to use"), cl::values( + clEnumValN(BITWUZLA_SOLVER, "bitwuzla", + "Bitwuzla" BITWUZLA_IS_DEFAULT_STR), + clEnumValN(BITWUZLA_TREE_SOLVER, "bitwuzla-tree", + "Bitwuzla tree-incremental solver"), clEnumValN(STP_SOLVER, "stp", "STP" STP_IS_DEFAULT_STR), clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), @@ -224,6 +237,7 @@ cl::opt DebugCrossCheckCoreSolverWith( clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3"), + clEnumValN(BITWUZLA_SOLVER, "bitwuzla", "Bitwuzla"), clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)")), cl::init(NO_SOLVER), cl::cat(SolvingCat)); @@ -235,11 +249,12 @@ llvm::cl::opt llvm::cl::opt SymbolicAllocationThreshold( "symbolic-allocation-threshold", llvm::cl::desc("Maximum possible sum of sizes for all symbolic allocation " - "before minimazation (default 1Kb)"), + "before minimization (default 1Kb)"), llvm::cl::init(1024), llvm::cl::cat(klee::SolvingCat)); } // namespace klee #undef STP_IS_DEFAULT_STR #undef METASMT_IS_DEFAULT_STR #undef Z3_IS_DEFAULT_STR +#undef BITWUZLA_IS_DEFAULT_STR #undef DEFAULT_CORE_SOLVER diff --git a/scripts/build/common-functions b/scripts/build/common-functions index c964419f60..65027f0bd3 100644 --- a/scripts/build/common-functions +++ b/scripts/build/common-functions @@ -8,11 +8,18 @@ function git_clone_or_update() { if [[ ! -e "${destination}/.git" ]]; then git clone $([ "${branch}x" != "x" ] && echo "--depth 1 -b ${branch}" || echo "") "$url" "$destination" else - cd "$destination" + pushd "$destination" git pull if [[ ! -z "$branch" ]]; then git checkout "${branch}" fi + popd + fi + + if [[ $# -ge 4 ]]; then + pushd "$destination" + git checkout $4 + popd fi } @@ -20,12 +27,12 @@ function get_git_hash() { local url="$1" local branch="$2" local commit_id="" - + # List remote git branches and get the commit id of the branch - commit_id="$(git ls-remote -h "$url" |grep "$branch" | cut -d$'\t' -f 1)" - + commit_id="$(git ls-remote -h "$url" | grep "$branch" | cut -d$'\t' -f 1)" + # If that doesn't work use the branch instead of the commit id - if [[ -z "${commit_id}" ]]; then + if [[ -z "${commit_id}" ]]; then echo "${branch}" else echo "${commit_id:0:7}" @@ -33,10 +40,10 @@ function get_git_hash() { } function with_sudo() { - echo "Checking sudo $@" - if [[ $(whoami) != "root" ]]; then - sudo "$@" - else - "$@" - fi -} \ No newline at end of file + echo "Checking sudo $@" + if [[ $(whoami) != "root" ]]; then + sudo "$@" + else + "$@" + fi +} diff --git a/scripts/build/p-bitwuzla-linux-ubuntu.inc b/scripts/build/p-bitwuzla-linux-ubuntu.inc new file mode 100644 index 0000000000..cd585c7e31 --- /dev/null +++ b/scripts/build/p-bitwuzla-linux-ubuntu.inc @@ -0,0 +1,25 @@ +# Build dependencies Bitwuzla +install_build_dependencies_bitwuzla() { + source "${DIR}/common-functions" + with_sudo apt update -y + + dependencies=( + build-essential + + ninja-build + python3 + python3-pip + cmake + git + ) + + #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 m4 + + 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 new file mode 100644 index 0000000000..af4cc8f651 --- /dev/null +++ b/scripts/build/p-bitwuzla-osx.inc @@ -0,0 +1,14 @@ +install_build_dependencies_bitwuzla() { + dependencies=( + ninja + python3 + python3-pip + cmake + git + pkg-config + ) + 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 new file mode 100644 index 0000000000..87a28ea827 --- /dev/null +++ b/scripts/build/p-bitwuzla.inc @@ -0,0 +1,74 @@ +# Build scripts for Bitwuzla +# Variables that any artifact of this package might depend on +setup_build_variables_bitwuzla() { + BITWUZLA_SUFFIX="${SANITIZER_SUFFIX}" + + BITWUZLA_BUILD_PATH="${BASE}/bitwuzla-${BITWUZLA_VERSION}-build${BITWUZLA_SUFFIX}" + BITWUZLA_INSTALL_PATH="${BASE}/bitwuzla-${BITWUZLA_VERSION}-install${BITWUZLA_SUFFIX}" + bitwuzla_url="https://github.com/bitwuzla/bitwuzla.git" + + return 0 +} + +download_bitwuzla() { + source "${DIR}/common-functions" + # Download Bitwuzla + git_clone_or_update "${bitwuzla_url}" "${BASE}/bitwuzla-${BITWUZLA_VERSION}" "${BITWUZLA_VERSION}" "${BITWUZLA_COMMIT}" +} + +build_bitwuzla() { + pushd "${BASE}/bitwuzla-${BITWUZLA_VERSION}" + + args=(--build-dir "${BITWUZLA_BUILD_PATH}" --prefix "${BITWUZLA_INSTALL_PATH}" --static --no-unit-testing) + + if [[ -n "${SANITIZER_SUFFIX:-}" ]]; then + if [[ "${SANITIZER_BUILD:-}" == "address" ]]; then + args+=("--asan") + fi + if [[ "${SANITIZER_BUILD:-}" == "undefined" ]]; then + args+=("--ubsan") + fi + args+=("--assertions" "debug") + else + args+=("--no-assertions" "release") + fi + + ./configure.py "${args[@]}" + popd + cd "${BITWUZLA_BUILD_PATH}" || return 1 + yes n | ninja install + touch "${BITWUZLA_INSTALL_PATH}/.bitwuzla_installed" +} + +install_bitwuzla() { + return 0 +} + +# Check if the binary artifact is installed +is_installed_bitwuzla() { + ( + setup_build_variables_bitwuzla + [[ -f "${BITWUZLA_INSTALL_PATH}/.bitwuzla_installed" ]] + ) || return 1 +} + +setup_artifact_variables_bitwuzla() { + setup_build_variables_bitwuzla +} + +get_build_artifacts_bitwuzla() { + ( + setup_build_variables_bitwuzla + echo "${BITWUZLA_INSTALL_PATH}" + ) +} + +get_docker_config_id_bitwuzla() { + ( + source "${DIR}/common-functions" + setup_build_variables_bitwuzla + + biwuzla_remote_commit="$(get_git_hash "${bitwuzla_url}" "${BITWUZLA_VERSION}")" + echo "${biwuzla_remote_commit}" + ) +} diff --git a/scripts/build/p-klee-linux-ubuntu.inc b/scripts/build/p-klee-linux-ubuntu.inc index 8bf39a199b..a67a061615 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 0561e28f68..4f5b063599 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 248d3a9bb7..b484cc9281 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -67,6 +67,7 @@ fi local KLEE_Z3_CONFIGURE_OPTION=("-DENABLE_SOLVER_Z3=OFF") local KLEE_STP_CONFIGURE_OPTION=("-DENABLE_SOLVER_STP=OFF") local KLEE_METASMT_CONFIGURE_OPTION=("-DENABLE_SOLVER_METASMT=OFF") + local KLEE_BITWUZLA_CONFIGURE_OPTION=("-DENABLE_SOLVER_BITWUZLA=OFF") KLEE_FLOATING_POINT=( "-DENABLE_FLOATING_POINT=FALSE" "-DENABLE_FP_RUNTIME=FALSE" @@ -106,6 +107,18 @@ fi "-DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}" ) ;; + bitwuzla) + 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" + ) + echo "bitwuzla" + ;; *) echo "Unknown solver ${solver}" exit 1 @@ -116,6 +129,7 @@ fi "${KLEE_Z3_CONFIGURE_OPTION[@]}" "${KLEE_STP_CONFIGURE_OPTION[@]}" "${KLEE_METASMT_CONFIGURE_OPTION[@]}" + "${KLEE_BITWUZLA_CONFIGURE_OPTION[@]}" "${KLEE_FLOATING_POINT[@]}" ) diff --git a/scripts/build/v-bitwuzla.inc b/scripts/build/v-bitwuzla.inc new file mode 100644 index 0000000000..bccd375853 --- /dev/null +++ b/scripts/build/v-bitwuzla.inc @@ -0,0 +1,11 @@ +# Build information for Bitwuzla solver +required_variables_bitwuzla=( + "BITWUZLA_VERSION" + "BITWUZLA_COMMIT" +) + +artifact_dependency_bitwuzla=("sanitizer") + +install_build_dependencies_bitwuzla() { + return 0 +} diff --git a/scripts/build/v-solvers.inc b/scripts/build/v-solvers.inc index 9d6bfdc857..74cdac1f5a 100644 --- a/scripts/build/v-solvers.inc +++ b/scripts/build/v-solvers.inc @@ -15,7 +15,8 @@ required_variables_check_solvers() { [[ "${solver}" == "z3" ]] && continue [[ "${solver}" == "stp" ]] && continue [[ "${solver}" == "metasmt" ]] && continue - + [[ "${solver}" == "bitwuzla" ]] && continue + echo "Unknown solver: \"$solver\"" exit 1 done @@ -51,7 +52,7 @@ setup_variables_solvers() { [[ "${solver}" == "z3" ]] && SELECTED_SOLVERS+=("z3") && continue [[ "${solver}" == "stp" ]] && SELECTED_SOLVERS+=("stp") && continue [[ "${solver}" == "metasmt" ]] && SELECTED_SOLVERS+=("metasmt") && continue - + [[ "${solver}" == "bitwuzla" ]] && SELECTED_SOLVERS+=("bitwuzla") && continue echo "Unknown solver: \"$solver\"" exit 1 done diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c index 7482d48232..a70223e36d 100644 --- a/test/Feature/const_array_opt1.c +++ b/test/Feature/const_array_opt1.c @@ -1,5 +1,6 @@ // REQUIRES: not-msan // REQUIRES: not-ubsan +// REQUIRES: not-bitwuzla // Disabling msan and ubsan because it times out on CI // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out diff --git a/test/Solver/CrosscheckBitwuzlaAndBitwuzlaTreeInc.c b/test/Solver/CrosscheckBitwuzlaAndBitwuzlaTreeInc.c new file mode 100644 index 0000000000..f0e1dfc757 --- /dev/null +++ b/test/Solver/CrosscheckBitwuzlaAndBitwuzlaTreeInc.c @@ -0,0 +1,11 @@ +// REQUIRES: bitwuzla +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=4 --debug-crosscheck-core-solver=bitwuzla --debug-bitwuzla-validate-models --debug-assignment-validating-solver --use-cex-cache=false --use-guided-search=none %t1.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=64 --debug-crosscheck-core-solver=bitwuzla --debug-bitwuzla-validate-models --debug-assignment-validating-solver --use-cex-cache=false --use-guided-search=none %t1.bc 2>&1 | FileCheck %s + +#include "ExerciseSolver.c.inc" + +// CHECK: KLEE: done: completed paths = 18 +// CHECK: KLEE: done: partially completed paths = 0 diff --git a/test/Solver/CrosscheckCoreZ3Bitwuzla.c b/test/Solver/CrosscheckCoreZ3Bitwuzla.c new file mode 100644 index 0000000000..f50a0dd2fc --- /dev/null +++ b/test/Solver/CrosscheckCoreZ3Bitwuzla.c @@ -0,0 +1,10 @@ +// REQUIRES: z3 +// REQUIRES: bitwuzla +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --use-forked-solver=false --debug-crosscheck-core-solver=bitwuzla --use-guided-search=none %t1.bc 2>&1 | FileCheck %s + +#include "ExerciseSolver.c.inc" + +// CHECK: KLEE: done: completed paths = 18 +// CHECK: KLEE: done: partially completed paths = 0 diff --git a/test/Solver/NoBitwuzla.c b/test/Solver/NoBitwuzla.c new file mode 100644 index 0000000000..a4a915a9d6 --- /dev/null +++ b/test/Solver/NoBitwuzla.c @@ -0,0 +1,10 @@ +// REQUIRES: not-bitwuzla +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --solver-backend=bitwuzla %t1.bc 2>&1 | FileCheck %s +// CHECK: Not compiled with Bitwuzla support +// CHECK: ERROR: Failed to create core solver + +int main(int argc, char **argv) { + return 0; +} diff --git a/test/Solver/sina2f.c b/test/Solver/sina2f.c new file mode 100644 index 0000000000..fb7179d785 --- /dev/null +++ b/test/Solver/sina2f.c @@ -0,0 +1,67 @@ +// REQUIRES: bitwuzla +// REQUIRES: not-asan +// REQUIRES: not-msan +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --strip-unwanted-calls --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=16 --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=false --output-istats=false --use-sym-size-alloc=true --cex-cache-validity-cores --fp-runtime --x86FP-as-x87FP80 --symbolic-allocation-threshold=8192 --allocate-determ --allocate-determ-size=3072 --allocate-determ-start-address=0x00030000000 --mem-trigger-cof --use-alpha-equivalence=true --track-coverage=all --use-iterative-deepening-search=max-cycles --max-solver-time=5s --max-cycles-before-stuck=15 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --cover-on-the-fly=true --delay-cover-on-the-fly=27 --max-time=29 %t1.bc 2>&1 | FileCheck %s +#include "klee-test-comp.c" + +/* + * Benchmarks contributed by Divyesh Unadkat[1,2], Supratik Chakraborty[1], Ashutosh Gupta[1] + * [1] Indian Institute of Technology Bombay, Mumbai + * [2] TCS Innovation labs, Pune + * + */ + +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__((__nothrow__, __leaf__)) __attribute__((__noreturn__)); +void reach_error() { __assert_fail("0", "sina2f.c", 10, "reach_error"); } +extern void abort(void); +void assume_abort_if_not(int cond) { + if (!cond) { + abort(); + } +} +void __VERIFIER_assert(int cond) { + if (!(cond)) { + ERROR : { + reach_error(); + abort(); + } + } +} +extern int __VERIFIER_nondet_int(void); +void *malloc(unsigned int size); + +int N; + +int main() { + N = __VERIFIER_nondet_int(); + if (N <= 0) + return 1; + assume_abort_if_not(N <= 2147483647 / sizeof(int)); + + int i; + long long sum[1]; + long long *a = malloc(sizeof(long long) * N); + + sum[0] = 1; + for (i = 0; i < N; i++) { + a[i] = 1; + } + + for (i = 0; i < N; i++) { + sum[0] = sum[0] + a[i]; + } + + for (i = 0; i < N; i++) { + a[i] = a[i] + sum[0]; + } + + for (i = 0; i < N; i++) { + __VERIFIER_assert(a[i] == N); + } + return 1; +} + +// CHECK: KLEE: done diff --git a/test/lit.cfg b/test/lit.cfg index 11308ae424..d2af70f065 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -210,6 +210,10 @@ if config.enable_metasmt: config.available_features.add('metasmt') else: config.available_features.add('not-metasmt') +if config.enable_bitwuzla: + config.available_features.add('bitwuzla') +else: + config.available_features.add('not-bitwuzla') # Zlib config.available_features.add('zlib' if config.enable_zlib else 'not-zlib') diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index 0712644706..fb4ed1c586 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -52,6 +52,7 @@ config.have_selinux = True if @HAVE_SELINUX@ == 1 else False config.enable_stp = True if @ENABLE_STP@ == 1 else False config.enable_z3 = True if @ENABLE_Z3@ == 1 else False config.enable_metasmt = True if @ENABLE_METASMT@ == 1 else False +config.enable_bitwuzla = True if @ENABLE_BITWUZLA@ == 1 else False config.enable_zlib = True if @HAVE_ZLIB_H@ == 1 else False config.have_asan = True if @IS_ASAN_BUILD@ == 1 else False config.have_ubsan = True if @IS_UBSAN_BUILD@ == 1 else False