diff --git a/.cirrus.yml b/.cirrus.yml deleted file mode 100644 index 3f7e0c0423..0000000000 --- a/.cirrus.yml +++ /dev/null @@ -1,17 +0,0 @@ -task: - freebsd_instance: - matrix: - - image_family: freebsd-15-0-snap - deps_script: - - sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf - - env ASSUME_ALWAYS_YES=yes pkg update -f - - env ASSUME_ALWAYS_YES=yes pkg install -y llvm13 gmake z3 cmake pkgconf google-perftools python3 py311-sqlite3 py311-tabulate nlohmann-json bash coreutils immer - build_script: - - mkdir build - - cd build - - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DWARNINGS_AS_ERRORS:BOOL=OFF .. - - gmake - test_script: - - sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg - - cd build - - gmake check diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index cae4b2b634..b4ef7e7a6f 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -39,6 +39,7 @@ env: Z3_VERSION: 4.8.15 SQLITE_VERSION: 3400100 BITWUZLA_VERSION: 0.7.0 + SMITHRIL_VERSION: v0.1.1 JSON_VERSION: v3.11.3 IMMER_VERSION: v0.8.1 @@ -59,8 +60,9 @@ jobs: "MSan", "Z3 only", "metaSMT", - "STP master", + # "STP master", "Bitwuzla only", + "Smithril only", "Latest klee-uclibc", "Asserts disabled", "No TCMalloc, optimised runtime", @@ -118,14 +120,18 @@ jobs: METASMT_DEFAULT: STP REQUIRES_RTTI: 1 # Test we can build against STP master - - name: "STP master" - env: - SOLVERS: STP - STP_VERSION: master + # - name: "STP master" + # env: + # SOLVERS: STP + # STP_VERSION: master # Test just using Bitwuzla only - name: "Bitwuzla only" env: SOLVERS: BITWUZLA + # Test just using Smithril only + - name: "Smithril only" + env: + SOLVERS: SMITHRIL # Check we can build latest klee-uclibc branch - name: "Latest klee-uclibc" env: diff --git a/CMakeLists.txt b/CMakeLists.txt index ce26032373..768780de1a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -208,15 +208,18 @@ include(${CMAKE_SOURCE_DIR}/cmake/find_z3.cmake) include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake) # bitwuzla include(${CMAKE_SOURCE_DIR}/cmake/find_bitwuzla.cmake) +# smithril +include(${CMAKE_SOURCE_DIR}/cmake/find_smithril.cmake) -if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}) AND (NOT ${ENABLE_BITWUZLA})) +if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT}) AND (NOT ${ENABLE_BITWUZLA}) AND (NOT ${ENABLE_SMITHRIL})) 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_BITWUZLA=ON\"\n" + "\"-DENABLE_SOLVER_SMITHRIL=ON\"\n" "\"-DENABLE_SOLVER_METASMT=ON\" ") endif() @@ -490,8 +493,8 @@ endif() ################################################################################ option(ENABLE_FLOATING_POINT "Enable KLEE's floating point extension" OFF) if (ENABLE_FLOATING_POINT) - if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_BITWUZLA})) - message (FATAL_ERROR "Floating point extension is availible only when using Z3 backend." + if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_BITWUZLA}) AND (NOT ${ENABLE_SMITHRIL})) + message (FATAL_ERROR "Floating point extension is availible only when using Z3, Bitwuzla or Smithril backend." "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() diff --git a/build.sh b/build.sh index eca0276cfc..975eeff8c8 100755 --- a/build.sh +++ b/build.sh @@ -27,7 +27,7 @@ USE_LIBCXX=1 SQLITE_VERSION="3400100" ## LLVM Required options -LLVM_VERSION=16 +LLVM_VERSION=14 ENABLE_OPTIMIZED=1 ENABLE_DEBUG=0 DISABLE_ASSERTIONS=1 @@ -36,7 +36,7 @@ ENABLE_WARNINGS_AS_ERRORS=0 ## Solvers Required options # SOLVERS=STP -SOLVERS=BITWUZLA:Z3:STP +SOLVERS=SMITHRIL:BITWUZLA:Z3 ## Google Test Required options GTEST_VERSION=1.16.0 @@ -58,6 +58,7 @@ STP_VERSION=2.3.3 MINISAT_VERSION=master BITWUZLA_VERSION=0.7.0 +SMITHRIL_VERSION=v0.1.1 KEEP_PARSE="true" while [ $KEEP_PARSE = "true" ]; do @@ -72,4 +73,4 @@ else fi done -BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME ./scripts/build/build.sh klee --install-system-deps +BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION 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 SMITHRIL_VERSION=$SMITHRIL_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME ./scripts/build/build.sh klee --install-system-deps diff --git a/cmake/find_smithril.cmake b/cmake/find_smithril.cmake new file mode 100644 index 0000000000..c7a72f49d1 --- /dev/null +++ b/cmake/find_smithril.cmake @@ -0,0 +1,40 @@ +#===------------------------------------------------------------------------===# +# +# 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(SMITHRIL IMPORTED_TARGET smithril) + +if (SMITHRIL_FOUND) + set(ENABLE_SOLVER_SMITHRIL_DEFAULT ON) +else() + set(ENABLE_SOLVER_SMITHRIL_DEFAULT OFF) +endif() + +option(ENABLE_SOLVER_SMITHRIL "Enable Smithril solver support" ${ENABLE_SOLVER_SMITHRIL_DEFAULT}) + +if (ENABLE_SOLVER_SMITHRIL) + message(STATUS "Smithril solver support enabled") + if (SMITHRIL_FOUND) + message(STATUS "Found Smithril") + set(ENABLE_SMITHRIL 1) # For config.h + + message(STATUS "Found Smithril libraries: \"${SMITHRIL_LIBRARIES}\"") + message(STATUS "Found Smithril include path: \"${SMITHRIL_INCLUDE_DIRS}\"") + list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${SMITHRIL_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARIES ${SMITHRIL_LINK_LIBRARIES}) + list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${SMITHRIL_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${SMITHRIL_LINK_LIBRARIES}) + + else() + message(FATAL_ERROR "Smithril not found.") + endif() +else() + message(STATUS "Smithril solver support disabled") + set(ENABLE_SMITHRIL 0) # For config.h +endif() diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin index 1d3f1ac6dd..1aff5ebe07 100644 --- a/include/klee/Config/config.h.cmin +++ b/include/klee/Config/config.h.cmin @@ -16,6 +16,9 @@ /* Using Bitwuzla Solver backend */ #cmakedefine ENABLE_BITWUZLA @ENABLE_BITWUZLA@ +/* Using Bitwuzla Solver backend */ +#cmakedefine ENABLE_SMITHRIL @ENABLE_SMITHRIL@ + /* Enable KLEE floating point extension */ #cmakedefine ENABLE_FP @ENABLE_FP@ diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h index 69b7a64bef..ecee0c2ee3 100644 --- a/include/klee/Solver/SolverCmdLine.h +++ b/include/klee/Solver/SolverCmdLine.h @@ -65,6 +65,8 @@ enum CoreSolverType { BITWUZLA_SOLVER, BITWUZLA_TREE_SOLVER, STP_SOLVER, + SMITHRIL_SOLVER, + SMITHRIL_TREE_SOLVER, METASMT_SOLVER, DUMMY_SOLVER, Z3_SOLVER, diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 9fb6edb865..0c4762fdc2 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -25,6 +25,9 @@ add_library(kleaverSolver MetaSMTSolver.cpp KQueryLoggingSolver.cpp QueryLoggingSolver.cpp + SmithrilBuilder.cpp + SmithrilHashConfig.cpp + SmithrilSolver.cpp SMTLIBLoggingSolver.cpp Solver.cpp SolverCmdLine.cpp diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index ae3c9ceaf1..8c5b939262 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -13,6 +13,10 @@ #include "BitwuzlaSolver.h" #endif +#ifdef ENABLE_SMITHRIL +#include "SmithrilSolver.h" +#endif + #ifdef ENABLE_METASMT #include "MetaSMTSolver.h" #endif @@ -102,8 +106,20 @@ std::unique_ptr createCoreSolver(CoreSolverType cst) { MaxSolversApproxTreeInc.ArgStr.str().c_str()); } return std::make_unique(); +#endif + case SMITHRIL_TREE_SOLVER: + case SMITHRIL_SOLVER: +#ifdef ENABLE_SMITHRIL + klee_message("Using Smithril 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"); + klee_message("Not compiled with Smithril support"); return NULL; #endif case NO_SOLVER: diff --git a/lib/Solver/SmithrilBuilder.cpp b/lib/Solver/SmithrilBuilder.cpp new file mode 100644 index 0000000000..47b14be4f2 --- /dev/null +++ b/lib/Solver/SmithrilBuilder.cpp @@ -0,0 +1,1345 @@ +//===-- SmithrilBuilder.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_SMITHRIL + +#include "SmithrilBuilder.h" +#include "SmithrilHashConfig.h" +#include "klee/ADT/Bits.h" + +#include "klee/Expr/Expr.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" + +#include "llvm/ADT/APFloat.h" +#include "llvm/ADT/StringExtras.h" + +using namespace smithril; + +namespace klee { + +SmithrilArrayExprHash::~SmithrilArrayExprHash() {} + +void SmithrilArrayExprHash::clear() { + _update_node_hash.clear(); + _array_hash.clear(); +} + +void SmithrilArrayExprHash::clearUpdates() { _update_node_hash.clear(); } + +SmithrilBuilder::SmithrilBuilder(bool autoClearConstructCache) + : autoClearConstructCache(autoClearConstructCache) { + ctx = smithril_new_context(); +} + +SmithrilBuilder::~SmithrilBuilder() { + _arr_hash.clearUpdates(); + clearSideConstraints(); +} + +SmithrilSort SmithrilBuilder::getBoolSort() { + // FIXME: cache these + return smithril_mk_bool_sort(ctx); +} + +SmithrilSort SmithrilBuilder::getBvSort(unsigned width) { + // FIXME: cache these + return smithril_mk_bv_sort(ctx, width); +} + +SmithrilSort SmithrilBuilder::getArraySort(SmithrilSort domainSort, + SmithrilSort rangeSort) { + // FIXME: cache these + return smithril_mk_array_sort(ctx, domainSort, rangeSort); +} + +SmithrilTerm SmithrilBuilder::buildFreshBoolConst() { + return smithril_mk_fresh_smt_symbol(ctx, getBoolSort()); +} + +SmithrilTerm SmithrilBuilder::buildArray(const char *name, unsigned indexWidth, + unsigned valueWidth) { + SmithrilSort domainSort = getBvSort(indexWidth); + SmithrilSort rangeSort = getBvSort(valueWidth); + SmithrilSort t = getArraySort(domainSort, rangeSort); + return smithril_mk_smt_symbol(ctx, name, + t); // mk_const(t, std::string(name)); +} + +SmithrilTerm SmithrilBuilder::buildConstantArray(const char *, + unsigned indexWidth, + unsigned valueWidth, + unsigned value) { + SmithrilSort domainSort = getBvSort(indexWidth); + SmithrilSort rangeSort = getBvSort(valueWidth); + return smithril_mk_smt_const_symbol(ctx, bvConst32(valueWidth, value), + getArraySort(domainSort, rangeSort)); +} + +SmithrilTerm SmithrilBuilder::getTrue() { + return smithril_mk_smt_bool(ctx, true); +} + +SmithrilTerm SmithrilBuilder::getFalse() { + return smithril_mk_smt_bool(ctx, false); +} + +SmithrilTerm SmithrilBuilder::bvOne(unsigned width) { + return bvZExtConst(width, 1); +} +SmithrilTerm SmithrilBuilder::bvZero(unsigned width) { + return bvZExtConst(width, 0); +} +SmithrilTerm SmithrilBuilder::bvMinusOne(unsigned width) { + return bvZExtConst(width, (uint64_t)-1); +} +SmithrilTerm SmithrilBuilder::bvConst32(unsigned width, uint32_t value) { + if (width < 32) { + value &= ((1 << width) - 1); + } + return smithril_mk_bv_value_uint64(ctx, getBvSort(width), value); +} +SmithrilTerm SmithrilBuilder::bvConst64(unsigned width, uint64_t value) { + if (width < 64) { + value &= ((uint64_t(1) << width) - 1); + } + return smithril_mk_bv_value_uint64(ctx, getBvSort(width), value); +} +SmithrilTerm SmithrilBuilder::bvZExtConst(unsigned width, uint64_t value) { + if (width <= 64) { + return bvConst64(width, value); + } + SmithrilTerm expr = bvConst64(64, value); + SmithrilTerm zero = bvConst64(64, 0); + for (width -= 64; width > 64; width -= 64) { + expr = smithril_mk_concat(ctx, zero, expr); + } + return smithril_mk_concat(ctx, bvConst64(width, 0), expr); +} + +SmithrilTerm SmithrilBuilder::bvSExtConst(unsigned width, uint64_t value) { + if (width <= 64) { + return bvConst64(width, value); + } + + if (value >> 63) { + return smithril_mk_concat(ctx, bvMinusOne(width - 64), + bvConst64(64, value)); + } + return smithril_mk_concat(ctx, bvZero(width - 64), bvConst64(64, value)); +} + +SmithrilTerm SmithrilBuilder::bvBoolExtract(SmithrilTerm expr, int bit) { + return smithril_mk_eq(ctx, bvExtract(expr, bit, bit), bvOne(1)); +} + +SmithrilTerm SmithrilBuilder::bvExtract(SmithrilTerm expr, unsigned top, + unsigned bottom) { + return smithril_mk_extract(ctx, top, bottom, castToBitVector(expr)); +} + +SmithrilTerm SmithrilBuilder::eqExpr(SmithrilTerm a, SmithrilTerm b) { + // Handle implicit bitvector/float coercision + SmithrilSort aSort = smithril_get_sort(ctx, a); + SmithrilSort bSort = smithril_get_sort(ctx, b); + + if (smithril_get_sort_kind(aSort) == SortKind::Bv && + smithril_get_sort_kind(bSort) == SortKind::Fp) { + // Coerce `b` to be a bitvector + b = castToBitVector(b); + } + + if (smithril_get_sort_kind(aSort) == SortKind::Fp && + smithril_get_sort_kind(bSort) == SortKind::Bv) { + // Coerce `a` to be a bitvector + a = castToBitVector(a); + } + return smithril_mk_eq(ctx, a, b); +} + +// logical right shift +SmithrilTerm SmithrilBuilder::bvRightShift(SmithrilTerm expr, unsigned shift) { + SmithrilTerm exprAsBv = castToBitVector(expr); + unsigned width = getBVLength(exprAsBv); + + if (shift == 0) { + return expr; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + return smithril_mk_bvlshr(ctx, exprAsBv, bvConst32(width, shift)); + } +} + +// logical left shift +SmithrilTerm SmithrilBuilder::bvLeftShift(SmithrilTerm expr, unsigned shift) { + SmithrilTerm exprAsBv = castToBitVector(expr); + unsigned width = getBVLength(exprAsBv); + + if (shift == 0) { + return expr; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + return smithril_mk_bvshl(ctx, exprAsBv, bvConst32(width, shift)); + } +} + +// left shift by a variable amount on an expression of the specified width +SmithrilTerm SmithrilBuilder::bvVarLeftShift(SmithrilTerm expr, + SmithrilTerm shift) { + SmithrilTerm exprAsBv = castToBitVector(expr); + SmithrilTerm shiftAsBv = castToBitVector(shift); + + unsigned width = getBVLength(exprAsBv); + SmithrilTerm res = smithril_mk_bvshl(ctx, exprAsBv, shiftAsBv); + + // If overshifting, shift to zero + SmithrilTerm 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 +SmithrilTerm SmithrilBuilder::bvVarRightShift(SmithrilTerm expr, + SmithrilTerm shift) { + SmithrilTerm exprAsBv = castToBitVector(expr); + SmithrilTerm shiftAsBv = castToBitVector(shift); + + unsigned width = getBVLength(exprAsBv); + SmithrilTerm res = smithril_mk_bvlshr(ctx, exprAsBv, shiftAsBv); + + // If overshifting, shift to zero + SmithrilTerm 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 +SmithrilTerm SmithrilBuilder::bvVarArithRightShift(SmithrilTerm expr, + SmithrilTerm shift) { + SmithrilTerm exprAsBv = castToBitVector(expr); + SmithrilTerm shiftAsBv = castToBitVector(shift); + + unsigned width = getBVLength(exprAsBv); + + SmithrilTerm res = smithril_mk_bvashr(ctx, exprAsBv, shiftAsBv); + + // If overshifting, shift to zero + SmithrilTerm ex = + bvLtExpr(shiftAsBv, bvConst32(getBVLength(shiftAsBv), width)); + res = iteExpr(ex, res, bvZero(width)); + return res; +} + +SmithrilTerm SmithrilBuilder::notExpr(SmithrilTerm expr) { + return smithril_mk_not(ctx, expr); +} +SmithrilTerm SmithrilBuilder::andExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_and(ctx, lhs, rhs); +} +SmithrilTerm SmithrilBuilder::orExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_or(ctx, lhs, rhs); +} +SmithrilTerm SmithrilBuilder::iffExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_iff(ctx, lhs, rhs); +} + +SmithrilTerm SmithrilBuilder::bvNotExpr(SmithrilTerm expr) { + return smithril_mk_bvnot(ctx, castToBitVector(expr)); +} + +SmithrilTerm SmithrilBuilder::bvAndExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_bvand(ctx, castToBitVector(lhs), castToBitVector(rhs)); +} + +SmithrilTerm SmithrilBuilder::bvOrExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_bvor(ctx, castToBitVector(lhs), castToBitVector(rhs)); +} + +SmithrilTerm SmithrilBuilder::bvXorExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_bvxor(ctx, castToBitVector(lhs), castToBitVector(rhs)); +} + +SmithrilTerm SmithrilBuilder::bvSignExtend(SmithrilTerm src, unsigned width) { + SmithrilTerm srcAsBv = castToBitVector(src); + SmithrilSort srcAsBvSort = smithril_get_sort(ctx, srcAsBv); + unsigned src_width = smithril_get_bv_sort_size(srcAsBvSort); + assert(src_width <= width && "attempted to extend longer data"); + return smithril_mk_sign_extend(ctx, width - src_width, srcAsBv); +} + +SmithrilTerm SmithrilBuilder::writeExpr(SmithrilTerm array, SmithrilTerm index, + SmithrilTerm value) { + return smithril_mk_store(ctx, array, index, value); +} + +SmithrilTerm SmithrilBuilder::readExpr(SmithrilTerm array, SmithrilTerm index) { + return smithril_mk_select(ctx, array, index); +} + +unsigned SmithrilBuilder::getBVLength(SmithrilTerm expr) { + SmithrilSort exprSort = smithril_get_sort(ctx, expr); + return smithril_get_bv_sort_size(exprSort); +} + +SmithrilTerm SmithrilBuilder::iteExpr(SmithrilTerm condition, + SmithrilTerm whenTrue, + SmithrilTerm whenFalse) { + // Handle implicit bitvector/float coercision + SmithrilSort whenTrueSort = smithril_get_sort(ctx, whenTrue); + SmithrilSort whenFalseSort = smithril_get_sort(ctx, whenFalse); + + if (smithril_get_sort_kind(whenTrueSort) == SortKind::Bv && + smithril_get_sort_kind(whenFalseSort) == SortKind::Fp) { + // Coerce `whenFalse` to be a bitvector + whenFalse = castToBitVector(whenFalse); + } + + if (smithril_get_sort_kind(whenTrueSort) == SortKind::Fp && + smithril_get_sort_kind(whenFalseSort) == SortKind::Bv) { + // Coerce `whenTrue` to be a bitvector + whenTrue = castToBitVector(whenTrue); + } + return smithril_mk_ite(ctx, condition, whenTrue, whenFalse); +} + +SmithrilTerm SmithrilBuilder::bvLtExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_bvult(ctx, castToBitVector(lhs), castToBitVector(rhs)); +} + +SmithrilTerm SmithrilBuilder::bvLeExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_bvule(ctx, castToBitVector(lhs), castToBitVector(rhs)); +} + +SmithrilTerm SmithrilBuilder::sbvLtExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_bvslt(ctx, castToBitVector(lhs), castToBitVector(rhs)); +} + +SmithrilTerm SmithrilBuilder::sbvLeExpr(SmithrilTerm lhs, SmithrilTerm rhs) { + return smithril_mk_bvsle(ctx, castToBitVector(lhs), castToBitVector(rhs)); +} + +SmithrilTerm SmithrilBuilder::constructAShrByConstant(SmithrilTerm expr, + unsigned shift, + SmithrilTerm isSigned) { + SmithrilTerm 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 Smithril? + SmithrilTerm signed_term = smithril_mk_concat( + ctx, bvMinusOne(shift), bvExtract(exprAsBv, width - 1, shift)); + SmithrilTerm unsigned_term = bvRightShift(exprAsBv, shift); + + return smithril_mk_ite(ctx, isSigned, signed_term, unsigned_term); + } +} + +SmithrilTerm SmithrilBuilder::getInitialArray(const Array *root) { + assert(root); + SmithrilTerm 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 + // SmithrilSolver.cpp + int width_out; + SmithrilTerm 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 (const auto &[index, value] : source->constantValues->storage()) { + int width_out; + SmithrilTerm 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; +} + +SmithrilTerm SmithrilBuilder::getInitialRead(const Array *root, + unsigned index) { + return readExpr(getInitialArray(root), bvConst32(32, index)); +} + +SmithrilTerm SmithrilBuilder::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 + SmithrilTerm 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; +} + +SmithrilTerm SmithrilBuilder::construct(ref e, int *width_out) { + if (!SmithrilHashConfig::UseConstructHashSmithril || 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; + SmithrilTerm res = constructActual(e, width_out); + constructed.insert(std::make_pair(e, std::make_pair(res, *width_out))); + return res; + } + } +} + +void SmithrilBuilder::FPCastWidthAssert([[maybe_unused]] int *width_out, + [[maybe_unused]] 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 */ +SmithrilTerm SmithrilBuilder::constructActual(ref e, int *width_out) { + + int width; + if (!width_out) + width_out = &width; + ++stats::queryConstructs; + switch (e->getKind()) { + case Expr::Pointer: + case Expr::ConstantPointer: { + assert(0 && "unreachable"); + } + + 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(); + + SmithrilTerm 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 { + ref Tmp = CE; + Res = bvConst64(64, Tmp->Extract(0, 64)->getZExtValue()); + while (Tmp->getWidth() > 64) { + Tmp = Tmp->Extract(64, Tmp->getWidth() - 64); + unsigned Width = std::min(64U, Tmp->getWidth()); + Res = smithril_mk_concat( + ctx, bvConst64(Width, Tmp->Extract(0, Width)->getZExtValue()), Res); + } + } + // 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); + SmithrilTerm cond = construct(se->cond, 0); + SmithrilTerm tExpr = construct(se->trueExpr, width_out); + SmithrilTerm fExpr = construct(se->falseExpr, width_out); + return iteExpr(cond, tExpr, fExpr); + } + + case Expr::Concat: { + ConcatExpr *ce = cast(e); + unsigned numKids = ce->getNumKids(); + SmithrilTerm res = construct(ce->getKid(numKids - 1), 0); + for (int i = numKids - 2; i >= 0; i--) { + res = smithril_mk_concat(ctx, construct(ce->getKid(i), 0), res); + } + *width_out = ce->getWidth(); + return res; + } + + case Expr::Extract: { + ExtractExpr *ee = cast(e); + SmithrilTerm 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); + SmithrilTerm 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 smithril_mk_concat(ctx, bvZero(*width_out - srcWidth), + castToBitVector(src)); + } + } + + case Expr::SExt: { + int srcWidth; + CastExpr *ce = cast(e); + SmithrilTerm 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); + SmithrilTerm 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 smithril_mk_fp_to_fp_from_fp( + ctx, getRoundingModeSort(llvm::APFloat::rmNearestTiesToEven), src, + out_widths.first, out_widths.second); + } + + case Expr::FPTrunc: { + int srcWidth; + FPTruncExpr *ce = cast(e); + SmithrilTerm 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 smithril_mk_fp_to_fp_from_fp( + ctx, getRoundingModeSort(llvm::APFloat::rmNearestTiesToEven), src, + out_widths.first, out_widths.second); + } + + case Expr::FPToUI: { + int srcWidth; + FPToUIExpr *ce = cast(e); + SmithrilTerm src = castToFloat(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid FPToUI width"); + return smithril_mk_fp_to_ubv(ctx, getRoundingModeSort(ce->roundingMode), + src, ce->getWidth()); + } + + case Expr::FPToSI: { + int srcWidth; + FPToSIExpr *ce = cast(e); + SmithrilTerm src = castToFloat(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid FPToSI width"); + return smithril_mk_fp_to_sbv(ctx, getRoundingModeSort(ce->roundingMode), + src, ce->getWidth()); + } + + case Expr::UIToFP: { + int srcWidth; + UIToFPExpr *ce = cast(e); + SmithrilTerm src = castToBitVector(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid UIToFP width"); + + auto out_widths = getFloatSortFromBitWidth(*width_out); + return smithril_mk_fp_to_fp_from_ubv( + ctx, getRoundingModeSort(ce->roundingMode), src, out_widths.first, + out_widths.second); + } + + case Expr::SIToFP: { + int srcWidth; + SIToFPExpr *ce = cast(e); + SmithrilTerm src = castToBitVector(construct(ce->src, &srcWidth)); + *width_out = ce->getWidth(); + FPCastWidthAssert(width_out, "Invalid SIToFP width"); + + auto out_widths = getFloatSortFromBitWidth(*width_out); + return smithril_mk_fp_to_fp_from_sbv( + ctx, getRoundingModeSort(ce->roundingMode), src, out_widths.first, + out_widths.second); + } + + // Arithmetic + case Expr::Add: { + AddExpr *ae = cast(e); + SmithrilTerm left = castToBitVector(construct(ae->left, width_out)); + SmithrilTerm right = castToBitVector(construct(ae->right, width_out)); + assert(*width_out != 1 && "uncanonicalized add"); + SmithrilTerm result = smithril_mk_bvadd(ctx, left, right); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::Sub: { + SubExpr *se = cast(e); + SmithrilTerm left = castToBitVector(construct(se->left, width_out)); + SmithrilTerm right = castToBitVector(construct(se->right, width_out)); + assert(*width_out != 1 && "uncanonicalized sub"); + SmithrilTerm result = smithril_mk_bvsub(ctx, left, right); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::Mul: { + MulExpr *me = cast(e); + SmithrilTerm right = castToBitVector(construct(me->right, width_out)); + assert(*width_out != 1 && "uncanonicalized mul"); + SmithrilTerm left = castToBitVector(construct(me->left, width_out)); + SmithrilTerm result = smithril_mk_bvmul(ctx, left, right); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::UDiv: { + UDivExpr *de = cast(e); + SmithrilTerm 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)); + } + } + + SmithrilTerm right = castToBitVector(construct(de->right, width_out)); + SmithrilTerm result = smithril_mk_bvudiv(ctx, left, right); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::SDiv: { + SDivExpr *de = cast(e); + SmithrilTerm left = castToBitVector(construct(de->left, width_out)); + assert(*width_out != 1 && "uncanonicalized sdiv"); + SmithrilTerm right = castToBitVector(construct(de->right, width_out)); + SmithrilTerm result = smithril_mk_bvsdiv(ctx, left, right); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::URem: { + URemExpr *de = cast(e); + SmithrilTerm 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 smithril_mk_concat(ctx, bvZero(*width_out - bits), + bvExtract(left, bits - 1, 0)); + } + } + } + } + + SmithrilTerm right = castToBitVector(construct(de->right, width_out)); + SmithrilTerm result = smithril_mk_bvurem(ctx, left, right); + + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::SRem: { + SRemExpr *de = cast(e); + SmithrilTerm left = castToBitVector(construct(de->left, width_out)); + SmithrilTerm right = castToBitVector(construct(de->right, width_out)); + assert(*width_out != 1 && "uncanonicalized srem"); + SmithrilTerm result = smithril_mk_bvsrem(ctx, left, right); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + // Bitwise + case Expr::Not: { + NotExpr *ne = cast(e); + SmithrilTerm expr = construct(ne->expr, width_out); + if (*width_out == 1) { + return notExpr(expr); + } else { + return bvNotExpr(expr); + } + } + + case Expr::And: { + AndExpr *ae = cast(e); + SmithrilTerm left = construct(ae->left, width_out); + SmithrilTerm 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); + SmithrilTerm left = construct(oe->left, width_out); + SmithrilTerm 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); + SmithrilTerm left = construct(xe->left, width_out); + SmithrilTerm right = construct(xe->right, width_out); + + if (*width_out == 1) { + // XXX check for most efficient? + return iteExpr(left, SmithrilTerm(notExpr(right)), right); + } else { + return bvXorExpr(left, right); + } + } + + case Expr::Shl: { + ShlExpr *se = cast(e); + SmithrilTerm 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; + SmithrilTerm amount = construct(se->right, &shiftWidth); + return bvVarLeftShift(left, amount); + } + } + + case Expr::LShr: { + LShrExpr *lse = cast(e); + SmithrilTerm 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; + SmithrilTerm amount = construct(lse->right, &shiftWidth); + return bvVarRightShift(left, amount); + } + } + + case Expr::AShr: { + AShrExpr *ase = cast(e); + SmithrilTerm 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(); + SmithrilTerm signedBool = bvBoolExtract(left, *width_out - 1); + return constructAShrByConstant(left, shift, signedBool); + } else { + int shiftWidth; + SmithrilTerm amount = construct(ase->right, &shiftWidth); + return bvVarArithRightShift(left, amount); + } + } + + // Comparison + + case Expr::Eq: { + EqExpr *ee = cast(e); + SmithrilTerm left = construct(ee->left, width_out); + SmithrilTerm 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); + SmithrilTerm left = construct(ue->left, width_out); + SmithrilTerm 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); + SmithrilTerm left = construct(ue->left, width_out); + SmithrilTerm 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); + SmithrilTerm left = construct(se->left, width_out); + SmithrilTerm 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); + SmithrilTerm left = construct(se->left, width_out); + SmithrilTerm 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); + SmithrilTerm left = castToFloat(construct(fcmp->left, width_out)); + SmithrilTerm right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return smithril_mk_fp_eq(ctx, left, right); + } + + case Expr::FOLt: { + FOLtExpr *fcmp = cast(e); + SmithrilTerm left = castToFloat(construct(fcmp->left, width_out)); + SmithrilTerm right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return smithril_mk_fp_lt(ctx, left, right); + } + + case Expr::FOLe: { + FOLeExpr *fcmp = cast(e); + SmithrilTerm left = castToFloat(construct(fcmp->left, width_out)); + SmithrilTerm right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return smithril_mk_fp_leq(ctx, left, + right); // mixa117 RoundingMode does not matter + } + + case Expr::FOGt: { + FOGtExpr *fcmp = cast(e); + SmithrilTerm left = castToFloat(construct(fcmp->left, width_out)); + SmithrilTerm right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return smithril_mk_fp_gt(ctx, left, + right); // mixa117 RoundingMode does not matter + } + + case Expr::FOGe: { + FOGeExpr *fcmp = cast(e); + SmithrilTerm left = castToFloat(construct(fcmp->left, width_out)); + SmithrilTerm right = castToFloat(construct(fcmp->right, width_out)); + *width_out = 1; + return smithril_mk_fp_geq(ctx, left, + right); // mixa117 RoundingMode does not matter + } + + case Expr::IsNaN: { + IsNaNExpr *ine = cast(e); + SmithrilTerm arg = castToFloat(construct(ine->expr, width_out)); + *width_out = 1; + return smithril_fp_is_nan(ctx, arg); + } + + case Expr::IsInfinite: { + IsInfiniteExpr *iie = cast(e); + SmithrilTerm arg = castToFloat(construct(iie->expr, width_out)); + *width_out = 1; + return smithril_fp_is_inf(ctx, arg); + } + + case Expr::IsNormal: { + IsNormalExpr *ine = cast(e); + SmithrilTerm arg = castToFloat(construct(ine->expr, width_out)); + *width_out = 1; + return smithril_fp_is_normal(ctx, arg); + } + + case Expr::IsSubnormal: { + IsSubnormalExpr *ise = cast(e); + SmithrilTerm arg = castToFloat(construct(ise->expr, width_out)); + *width_out = 1; + return smithril_fp_is_subnormal(ctx, arg); + } + + case Expr::FAdd: { + FAddExpr *fadd = cast(e); + SmithrilTerm left = castToFloat(construct(fadd->left, width_out)); + SmithrilTerm right = castToFloat(construct(fadd->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FAdd"); + return smithril_mk_fp_add(ctx, getRoundingModeSort(fadd->roundingMode), + left, right); + } + + case Expr::FSub: { + FSubExpr *fsub = cast(e); + SmithrilTerm left = castToFloat(construct(fsub->left, width_out)); + SmithrilTerm right = castToFloat(construct(fsub->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FSub"); + return smithril_mk_fp_sub(ctx, getRoundingModeSort(fsub->roundingMode), + left, right); + } + + case Expr::FMul: { + FMulExpr *fmul = cast(e); + SmithrilTerm left = castToFloat(construct(fmul->left, width_out)); + SmithrilTerm right = castToFloat(construct(fmul->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FMul"); + return smithril_mk_fp_mul(ctx, getRoundingModeSort(fmul->roundingMode), + left, right); + } + + case Expr::FDiv: { + FDivExpr *fdiv = cast(e); + SmithrilTerm left = castToFloat(construct(fdiv->left, width_out)); + SmithrilTerm right = castToFloat(construct(fdiv->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FDiv"); + return smithril_mk_fp_div(ctx, getRoundingModeSort(fdiv->roundingMode), + left, right); + } + case Expr::FRem: { + FRemExpr *frem = cast(e); + SmithrilTerm left = castToFloat(construct(frem->left, width_out)); + SmithrilTerm right = castToFloat(construct(frem->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FRem"); + return smithril_mk_fp_rem(ctx, left, + right); // mixa117 RoundingMode does not matter + } + + case Expr::FMax: { + FMaxExpr *fmax = cast(e); + SmithrilTerm left = castToFloat(construct(fmax->left, width_out)); + SmithrilTerm right = castToFloat(construct(fmax->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FMax"); + return smithril_mk_fp_max(ctx, left, + right); // mixa117 RoundingMode does not matter + } + + case Expr::FMin: { + FMinExpr *fmin = cast(e); + SmithrilTerm left = castToFloat(construct(fmin->left, width_out)); + SmithrilTerm right = castToFloat(construct(fmin->right, width_out)); + assert(*width_out != 1 && "uncanonicalized FMin"); + return smithril_mk_fp_min(ctx, left, + right); // mixa117 RoundingMode does not matter + } + + case Expr::FSqrt: { + FSqrtExpr *fsqrt = cast(e); + SmithrilTerm arg = castToFloat(construct(fsqrt->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FSqrt"); + return smithril_mk_fp_sqrt(ctx, getRoundingModeSort(fsqrt->roundingMode), + arg); + } + case Expr::FRint: { + FRintExpr *frint = cast(e); + SmithrilTerm arg = castToFloat(construct(frint->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FSqrt"); + return smithril_mk_fp_rti(ctx, getRoundingModeSort(frint->roundingMode), + arg); + } + + case Expr::FAbs: { + FAbsExpr *fabsExpr = cast(e); + SmithrilTerm arg = castToFloat(construct(fabsExpr->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FAbs"); + return smithril_mk_fp_abs(ctx, + arg); // mixa117 RoundingMode does not matter + } + + case Expr::FNeg: { + FNegExpr *fnegExpr = cast(e); + SmithrilTerm arg = castToFloat(construct(fnegExpr->expr, width_out)); + assert(*width_out != 1 && "uncanonicalized FNeg"); + return smithril_mk_fp_neg(ctx, + arg); // mixa117 RoundingMode does not matter + } + +// 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(); + } +} + +SmithrilTerm SmithrilBuilder::fpToIEEEBV(const SmithrilTerm &fp) { + SmithrilTerm signBit = smithril_mk_fresh_smt_symbol(ctx, getBvSort(1)); + SmithrilTerm exponentBits = smithril_mk_fresh_smt_symbol( + ctx, getBvSort(smithril_fp_get_bv_exp_size(fp))); + SmithrilTerm significandBits = smithril_mk_fresh_smt_symbol( + ctx, getBvSort(smithril_fp_get_bv_sig_size(fp) - 1)); + + SmithrilTerm floatTerm = + smithril_mk_fp(ctx, signBit, exponentBits, significandBits); + sideConstraints.push_back(smithril_mk_eq(ctx, fp, floatTerm)); + SmithrilTerm ieeeBits = smithril_mk_concat(ctx, signBit, exponentBits); + ieeeBits = smithril_mk_concat(ctx, ieeeBits, significandBits); + + return ieeeBits; +} + +std::pair +SmithrilBuilder::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 Smithril 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 " + "Smithril"); + std::abort(); + } +} + +SmithrilTerm SmithrilBuilder::castToFloat(const SmithrilTerm &e) { + SmithrilSort currentSort = smithril_get_sort(ctx, e); + if (smithril_get_sort_kind(currentSort) == SortKind::Fp) { + // Already a float + return e; + } else if (smithril_get_sort_kind(currentSort) == SortKind::Bv) { + unsigned bitWidth = + smithril_get_bv_sort_size(currentSort); // mixa117 no such? + switch (bitWidth) { + case Expr::Int16: + case Expr::Int32: + case Expr::Int64: + case Expr::Int128: { + auto out_width = getFloatSortFromBitWidth(bitWidth); + return smithril_mk_fp_to_fp_from_bv(ctx, e, out_width.first, + out_width.second); + } + case Expr::Fl80: { + // The bit pattern used by x87 fp80 and what we use in Smithril 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 Smithril + // + // 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 + // Smithril generates a model we get the correct bit pattern back. + // + // This assumes Smithril'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 Smithril. + // + // Note this code must kept in sync with + // `SmithrilBuilder::castToBitVector()`. Which performs the inverse + // operation here. + // + // TODO: Experiment with creating a constraint that transforms these + // unsupported bit patterns into a Smithril 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. + SmithrilTerm signBit = smithril_mk_extract(ctx, 79, 79, e); + SmithrilTerm exponentBits = smithril_mk_extract(ctx, 78, 64, e); + SmithrilTerm significandIntegerBit = smithril_mk_extract(ctx, 63, 63, e); + SmithrilTerm significandFractionBits = smithril_mk_extract(ctx, 62, 0, e); + + SmithrilTerm ieeeBitPatternAsFloat = + smithril_mk_fp(ctx, 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 Smithril 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. + SmithrilTerm significandIntegerBitConstrainedValue = + getx87FP80ExplicitSignificandIntegerBit(ieeeBitPatternAsFloat); + SmithrilTerm significandIntegerBitConstraint = smithril_mk_eq( + ctx, 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"); + } +} + +SmithrilTerm SmithrilBuilder::castToBitVector(const SmithrilTerm &e) { + SmithrilSort currentSort = smithril_get_sort(ctx, e); + if (smithril_get_sort_kind(currentSort) == SortKind::Bool) { + return smithril_mk_ite(ctx, e, bvOne(1), bvZero(1)); + } else if (smithril_get_sort_kind(currentSort) == SortKind::Bv) { + // Already a bitvector + return e; + } else if (smithril_get_sort_kind(currentSort) == SortKind::Fp) { + // Note this picks a single representation for NaN which means + // `castToBitVector(castToFloat(e))` might not equal `e`. + unsigned exponentBits = smithril_fp_get_bv_exp_size(e); + unsigned significandBits = smithril_fp_get_bv_sig_size(e); + 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 Smithril's IEEE representation + SmithrilTerm ieeeBits = fpToIEEEBV(e); + + // Construct the x87 fp80 bit representation + SmithrilTerm signBit = smithril_mk_extract(ctx, 78, 78, ieeeBits); + SmithrilTerm exponentBits = smithril_mk_extract(ctx, 77, 63, ieeeBits); + SmithrilTerm significandIntegerBit = + getx87FP80ExplicitSignificandIntegerBit(e); + SmithrilTerm significandFractionBits = + smithril_mk_extract(ctx, 62, 0, ieeeBits); + SmithrilTerm x87FP80Bits = smithril_mk_concat(ctx, signBit, exponentBits); + x87FP80Bits = smithril_mk_concat(ctx, x87FP80Bits, significandIntegerBit); + x87FP80Bits = + smithril_mk_concat(ctx, x87FP80Bits, significandFractionBits); + // mixa117 3 concats vs 1 concat in bitwuzla? + return x87FP80Bits; + } + default: + llvm_unreachable("Unhandled width when casting float to bitvector"); + } + } else { + llvm_unreachable("Sort cannot be cast to float"); + } +} + +RoundingMode +SmithrilBuilder::getRoundingModeSort(llvm::APFloat::roundingMode rm) { + switch (rm) { + case llvm::APFloat::rmNearestTiesToEven: + return RoundingMode::RNE; + case llvm::APFloat::rmTowardPositive: + return RoundingMode::RTP; + case llvm::APFloat::rmTowardNegative: + return RoundingMode::RTN; + case llvm::APFloat::rmTowardZero: + return RoundingMode::RTZ; + case llvm::APFloat::rmNearestTiesToAway: + return RoundingMode::RNA; + default: + llvm_unreachable("Unhandled rounding mode"); + } +} + +SmithrilTerm SmithrilBuilder::getx87FP80ExplicitSignificandIntegerBit( + const SmithrilTerm &e) { +#ifndef NDEBUG + // Check the passed in expression is the right type. + SmithrilSort currentSort = smithril_get_sort(ctx, e); + assert(smithril_get_sort_kind(currentSort) == Fp); + + unsigned exponentBits = smithril_fp_get_bv_exp_size(e); + unsigned significandBits = smithril_fp_get_bv_sig_size(e); + assert(exponentBits == 15); + llvm::errs() << "significandBits: " << significandBits << "\n"; + assert(significandBits == 64); +#endif + // If the number is a denormal or zero then the implicit integer bit is zero + // otherwise it is one. SmithrilTerm isDenormal = + SmithrilTerm isDenormal = smithril_fp_is_subnormal(ctx, e); + SmithrilTerm isZero = smithril_fp_is_zero(ctx, e); + + // FIXME: Cache these constants somewhere + SmithrilSort oneBitBvSort = getBvSort(/*width=*/1); + + SmithrilTerm oneBvOne = smithril_mk_bv_value_uint64(ctx, oneBitBvSort, 1); + SmithrilTerm zeroBvOne = smithril_mk_bv_value_uint64(ctx, oneBitBvSort, 0); + + SmithrilTerm significandIntegerBitCondition = orExpr(isDenormal, isZero); + + SmithrilTerm significandIntegerBitConstrainedValue = + smithril_mk_ite(ctx, significandIntegerBitCondition, zeroBvOne, oneBvOne); + + return significandIntegerBitConstrainedValue; +} +} // namespace klee + +#endif // ENABLE_SMITHRIL diff --git a/lib/Solver/SmithrilBuilder.h b/lib/Solver/SmithrilBuilder.h new file mode 100644 index 0000000000..1dc7bce63d --- /dev/null +++ b/lib/Solver/SmithrilBuilder.h @@ -0,0 +1,186 @@ +//===-- SmithrilBuilder.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 SMITHRIL_BUILDER_H +#define SMITHRIL_BUILDER_H + +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" + +#include "llvm/ADT/APFloat.h" + +namespace smithril { +#include +} + +#include + +namespace klee { + +class SmithrilArrayExprHash : public ArrayExprHash { + friend class SmithrilBuilder; + +public: + SmithrilArrayExprHash(){}; + virtual ~SmithrilArrayExprHash(); + void clear(); + void clearUpdates(); +}; + +struct SmithrilTermHash { + unsigned operator()(const smithril::SmithrilTerm &e) const { + return (unsigned long)(e._0); + } +}; + +struct SmithrilTermCmp { + bool operator()(const smithril::SmithrilTerm &a, + const smithril::SmithrilTerm &b) const { + return a._0 == b._0; + } +}; +class SmithrilBuilder { +private: + void FPCastWidthAssert(int *width_out, char const *msg); + smithril::SmithrilTerm fpToIEEEBV(const smithril::SmithrilTerm &); + +protected: + smithril::SmithrilTerm bvOne(unsigned width); + smithril::SmithrilTerm bvZero(unsigned width); + smithril::SmithrilTerm bvMinusOne(unsigned width); + smithril::SmithrilTerm bvConst32(unsigned width, uint32_t value); + smithril::SmithrilTerm bvConst64(unsigned width, uint64_t value); + smithril::SmithrilTerm bvZExtConst(unsigned width, uint64_t value); + smithril::SmithrilTerm bvSExtConst(unsigned width, uint64_t value); + smithril::SmithrilTerm bvBoolExtract(smithril::SmithrilTerm expr, int bit); + smithril::SmithrilTerm bvExtract(smithril::SmithrilTerm expr, unsigned top, + unsigned bottom); + smithril::SmithrilTerm eqExpr(smithril::SmithrilTerm a, + smithril::SmithrilTerm b); + + // logical left and right shift (not arithmetic) + smithril::SmithrilTerm bvLeftShift(smithril::SmithrilTerm expr, + unsigned shift); + smithril::SmithrilTerm bvRightShift(smithril::SmithrilTerm expr, + unsigned shift); + smithril::SmithrilTerm bvVarLeftShift(smithril::SmithrilTerm expr, + smithril::SmithrilTerm shift); + smithril::SmithrilTerm bvVarRightShift(smithril::SmithrilTerm expr, + smithril::SmithrilTerm shift); + smithril::SmithrilTerm bvVarArithRightShift(smithril::SmithrilTerm expr, + smithril::SmithrilTerm shift); + + smithril::SmithrilTerm notExpr(smithril::SmithrilTerm expr); + smithril::SmithrilTerm andExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm orExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm iffExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + + smithril::SmithrilTerm bvNotExpr(smithril::SmithrilTerm expr); + smithril::SmithrilTerm bvAndExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm bvOrExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm bvXorExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm bvSignExtend(smithril::SmithrilTerm src, + unsigned width); + + // Array operations + smithril::SmithrilTerm writeExpr(smithril::SmithrilTerm array, + smithril::SmithrilTerm index, + smithril::SmithrilTerm value); + smithril::SmithrilTerm readExpr(smithril::SmithrilTerm array, + smithril::SmithrilTerm index); + + // ITE-expression constructor + smithril::SmithrilTerm iteExpr(smithril::SmithrilTerm condition, + smithril::SmithrilTerm whenTrue, + smithril::SmithrilTerm whenFalse); + + // Bitvector length + unsigned getBVLength(smithril::SmithrilTerm expr); + + // Bitvector comparison + smithril::SmithrilTerm bvLtExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm bvLeExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm sbvLtExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + smithril::SmithrilTerm sbvLeExpr(smithril::SmithrilTerm lhs, + smithril::SmithrilTerm rhs); + + smithril::SmithrilTerm + constructAShrByConstant(smithril::SmithrilTerm expr, unsigned shift, + smithril::SmithrilTerm isSigned); + + smithril::SmithrilTerm getInitialArray(const Array *os); + smithril::SmithrilTerm getArrayForUpdate(const Array *root, + const UpdateNode *un); + + smithril::SmithrilTerm constructActual(ref e, int *width_out); + smithril::SmithrilTerm construct(ref e, int *width_out); + smithril::SmithrilTerm buildArray(const char *name, unsigned indexWidth, + unsigned valueWidth); + smithril::SmithrilTerm buildConstantArray(const char *name, + unsigned indexWidth, + unsigned valueWidth, + unsigned value); + + smithril::SmithrilSort getBoolSort(); + smithril::SmithrilSort getBvSort(unsigned width); + smithril::SmithrilSort getArraySort(smithril::SmithrilSort domainSort, + smithril::SmithrilSort rangeSort); + + std::pair getFloatSortFromBitWidth(unsigned bitWidth); + + // Float casts + smithril::SmithrilTerm castToFloat(const smithril::SmithrilTerm &e); + smithril::SmithrilTerm castToBitVector(const smithril::SmithrilTerm &e); + + smithril::RoundingMode getRoundingModeSort(llvm::APFloat::roundingMode rm); + smithril::SmithrilTerm + getx87FP80ExplicitSignificandIntegerBit(const smithril::SmithrilTerm &e); + + ExprHashMap> constructed; + SmithrilArrayExprHash _arr_hash; + bool autoClearConstructCache; + +public: + smithril::SmithrilContext ctx; + std::unordered_map> + constant_array_assertions; + // These are additional constraints that are generated during the + // translation to Smithril's constraint language. Clients should assert + // these. + std::vector sideConstraints; + + SmithrilBuilder(bool autoClearConstructCache); + ~SmithrilBuilder(); + + smithril::SmithrilTerm getTrue(); + smithril::SmithrilTerm getFalse(); + smithril::SmithrilTerm buildFreshBoolConst(); + smithril::SmithrilTerm getInitialRead(const Array *os, unsigned index); + + smithril::SmithrilTerm construct(ref e) { + smithril::SmithrilTerm 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/SmithrilHashConfig.cpp b/lib/Solver/SmithrilHashConfig.cpp new file mode 100644 index 0000000000..a4917ddc7b --- /dev/null +++ b/lib/Solver/SmithrilHashConfig.cpp @@ -0,0 +1,20 @@ +//===-- SmithrilHashConfig.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 "SmithrilHashConfig.h" +#include + +namespace SmithrilHashConfig { +llvm::cl::opt UseConstructHashSmithril( + "use-construct-hash-smithril", + llvm::cl::desc( + "Use hash-consing during Smithril query construction (default=true)"), + llvm::cl::init(true), llvm::cl::cat(klee::ExprCat)); +} // namespace SmithrilHashConfig diff --git a/lib/Solver/SmithrilHashConfig.h b/lib/Solver/SmithrilHashConfig.h new file mode 100644 index 0000000000..2558479802 --- /dev/null +++ b/lib/Solver/SmithrilHashConfig.h @@ -0,0 +1,19 @@ +//===-- SmithrilHashConfig.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_SMITHRILHASHCONFIG_H +#define KLEE_SMITHRILHASHCONFIG_H + +#include "llvm/Support/CommandLine.h" + +namespace SmithrilHashConfig { +extern llvm::cl::opt UseConstructHashSmithril; +} // namespace SmithrilHashConfig +#endif // KLEE_SMITHRILHASHCONFIG_H diff --git a/lib/Solver/SmithrilSolver.cpp b/lib/Solver/SmithrilSolver.cpp new file mode 100644 index 0000000000..4540bd5762 --- /dev/null +++ b/lib/Solver/SmithrilSolver.cpp @@ -0,0 +1,903 @@ + +//===-- SmithrilSolver.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" +#include "klee/Solver/SolverStats.h" +#include "klee/Statistics/TimerStatIncrementer.h" + +#ifdef ENABLE_SMITHRIL + +#include "SmithrilBuilder.h" +#include "SmithrilSolver.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/OptionCategories.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" + +#include "llvm/Support/ErrorHandling.h" + +namespace smithril { +#include +} + +#include +#include + +namespace { +llvm::cl::opt SmithrilVerbosityLevel( + "debug-smithril-verbosity", llvm::cl::init(0), + llvm::cl::desc("smithril verbosity level (default=0)"), + llvm::cl::cat(klee::SolvingCat)); +} + +namespace klee { + +using ConstraintFrames = inc_vector>; +using ExprIncMap = inc_umap, SmithrilTermHash, + SmithrilTermCmp>; +using SmithrilASTIncMap = + inc_umap; +using ExprIncSet = + inc_uset, klee::util::ExprHash, klee::util::ExprCmp>; +using SmithrilASTIncSet = + 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 Smithril 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 SmithrilSolverEnv { + using arr_vec = std::vector; + inc_vector objects; + arr_vec objectsForGetModel; + inc_vector smithril_ast_expr_constraints; + ExprIncMap smithril_ast_expr_to_klee_expr; + SmithrilASTIncSet expr_to_track; + inc_umap usedArrayBytes; + ExprIncSet symbolicObjects; + + explicit SmithrilSolverEnv() = default; + explicit SmithrilSolverEnv(const arr_vec &objects); + + void pop(size_t popSize); + void push(); + void clear(); + + const arr_vec *getObjectsForGetModel(ObjectAssignment oa) const; +}; + +SmithrilSolverEnv::SmithrilSolverEnv(const arr_vec &objects) + : objectsForGetModel(objects) {} + +void SmithrilSolverEnv::pop(size_t popSize) { + if (popSize == 0) + return; + objects.pop(popSize); + objectsForGetModel.clear(); + smithril_ast_expr_constraints.pop(popSize); + smithril_ast_expr_to_klee_expr.pop(popSize); + expr_to_track.pop(popSize); + usedArrayBytes.pop(popSize); + symbolicObjects.pop(popSize); +} + +void SmithrilSolverEnv::push() { + objects.push(); + smithril_ast_expr_constraints.push(); + smithril_ast_expr_to_klee_expr.push(); + expr_to_track.push(); + usedArrayBytes.push(); + symbolicObjects.push(); +} + +void SmithrilSolverEnv::clear() { + objects.clear(); + objectsForGetModel.clear(); + smithril_ast_expr_constraints.clear(); + smithril_ast_expr_to_klee_expr.clear(); + expr_to_track.clear(); + usedArrayBytes.clear(); + symbolicObjects.clear(); +} + +const SmithrilSolverEnv::arr_vec * +SmithrilSolverEnv::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 SmithrilSolverImpl : public SolverImpl { +protected: + std::unique_ptr builder; + smithril::SmithrilOptions solverParameters; + +private: + time::Span timeout; + SolverImpl::SolverRunStatus runStatusCode; + + bool internalRunSolver(const ConstraintQuery &query, SmithrilSolverEnv &env, + ObjectAssignment needObjects, + std::vector> *values, + ValidityCore *validityCore, bool &hasSolution); + + SolverImpl::SolverRunStatus handleSolverResponse( + smithril::SmithrilSolver theSolver, smithril::SolverResult satisfiable, + const SmithrilSolverEnv &env, ObjectAssignment needObjects, + std::vector> *values, bool &hasSolution); + +protected: + SmithrilSolverImpl(); + ~SmithrilSolverImpl(); + + virtual smithril::SmithrilSolver + initNativeSmithril(const ConstraintQuery &query, + SmithrilASTIncSet &assertions) = 0; + virtual void deinitNativeSmithril(smithril::SmithrilSolver theSolver) = 0; + virtual void push(smithril::SmithrilSolver s) = 0; + + bool computeTruth(const ConstraintQuery &, SmithrilSolverEnv &env, + bool &isValid); + bool computeValue(const ConstraintQuery &, SmithrilSolverEnv &env, + ref &result); + bool + computeInitialValues(const ConstraintQuery &, SmithrilSolverEnv &env, + std::vector> &values, + bool &hasSolution); + bool check(const ConstraintQuery &query, SmithrilSolverEnv &env, + ref &result); + bool computeValidityCore(const ConstraintQuery &query, SmithrilSolverEnv &env, + ValidityCore &validityCore, bool &isValid); + +public: + std::string getConstraintLog(const Query &) final; + SolverImpl::SolverRunStatus getOperationStatusCode() final; + void setCoreSolverTimeout(time::Span _timeout) final { + timeout = _timeout; + auto timeoutInSeconds = static_cast((timeout.toSeconds())); + if (timeoutInSeconds) { + std::string timeoutInSecondsString = + std::to_string(timeoutInSeconds) + "s"; + smithril::smithril_set_timeout(solverParameters, + timeoutInSecondsString.c_str()); + } + } + void enableUnsatCore() { + smithril::smithril_set_produce_unsat_core(solverParameters, true); + } + void disableUnsatCore() { + smithril::smithril_set_produce_unsat_core(solverParameters, false); + } + + // pass virtual functions to children + using SolverImpl::check; + using SolverImpl::computeInitialValues; + using SolverImpl::computeTruth; + using SolverImpl::computeValidityCore; + using SolverImpl::computeValue; +}; + +void deleteNativeSmithril(smithril::SmithrilSolver theSolver) { + smithril::smithril_delete_solver(theSolver); +} + +SmithrilSolverImpl::SmithrilSolverImpl() + : runStatusCode(SolverImpl::SOLVER_RUN_STATUS_FAILURE) { + builder = std::unique_ptr(new SmithrilBuilder( + /*autoClearConstructCache=*/false)); + assert(builder && "unable to create SmithrilBuilder"); + solverParameters = smithril::smithril_new_options(); + + setCoreSolverTimeout(timeout); + + if (ProduceUnsatCore) { + enableUnsatCore(); + } else { + disableUnsatCore(); + } + + // Set verbosity + // if (SmithrilVerbosityLevel > 0) { + // solverParameters.set(Option::VERBOSITY, + // SmithrilVerbosityLevel); // mixa117 no such thing? + // } + + // if (SmithrilVerbosityLevel) { + // solverParameters.set(Option::DBG_CHECK_MODEL, + // true); // mixa117 no such thing? + // } +} + +SmithrilSolverImpl::~SmithrilSolverImpl() { + smithril::smithril_delete_options(solverParameters); +} + +std::string SmithrilSolver::getConstraintLog(const Query &query) { + return impl->getConstraintLog(query); +} + +std::string SmithrilSolverImpl::getConstraintLog(const Query &) { return ""; } + +bool SmithrilSolverImpl::computeTruth(const ConstraintQuery &query, + SmithrilSolverEnv &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 SmithrilSolverImpl::computeValue(const ConstraintQuery &query, + SmithrilSolverEnv &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 SmithrilSolverImpl::computeInitialValues( + const ConstraintQuery &query, SmithrilSolverEnv &env, + std::vector> &values, bool &hasSolution) { + return internalRunSolver(query, env, + ObjectAssignment::NeededForObjectsFromEnv, &values, + /*validityCore=*/NULL, hasSolution); +} + +bool SmithrilSolverImpl::check(const ConstraintQuery &query, + SmithrilSolverEnv &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 SmithrilSolverImpl::computeValidityCore(const ConstraintQuery &query, + SmithrilSolverEnv &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 SmithrilSolverImpl::internalRunSolver( + const ConstraintQuery &query, SmithrilSolverEnv &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; + SmithrilASTIncSet 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; + smithril::SmithrilTerm smithrilConstraint = + builder->construct(constraint); + if (ProduceUnsatCore && validityCore) { + env.smithril_ast_expr_to_klee_expr.insert( + {smithrilConstraint, constraint}); + env.smithril_ast_expr_constraints.v.push_back(smithrilConstraint); + env.expr_to_track.insert(smithrilConstraint); + } + + exprs.insert(smithrilConstraint); + + 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; + + smithril::SmithrilSolver theSolver = initNativeSmithril(query, exprs); + + for (size_t i = 0; i < exprs.framesSize(); i++) { + push(theSolver); + for (auto it = exprs.begin(i), ie = exprs.end(i); it != ie; ++it) { + smithril_assert(theSolver, (*it)); + } + } + + smithril::SolverResult satisfiable = smithril_check_sat(theSolver); + + runStatusCode = handleSolverResponse(theSolver, satisfiable, env, needObjects, + values, hasSolution); + + if (ProduceUnsatCore && validityCore && + satisfiable == smithril::SolverResult::Unsat) { + constraints_ty unsatCore; + const smithril::SmithrilTermVector smithril_unsat_core_vec = + smithril_unsat_core(theSolver); + unsigned size = smithril_unsat_core_size(smithril_unsat_core_vec); + + std::unordered_set + smithril_ast_expr_unsat_core; + + for (unsigned index = 0; index < size; ++index) { + smithril::SmithrilTerm constraint = + smithril_unsat_core_get(builder->ctx, smithril_unsat_core_vec, index); + smithril_ast_expr_unsat_core.insert(constraint); + } + + for (const auto &z3_constraint : env.smithril_ast_expr_constraints.v) { + if (smithril_ast_expr_unsat_core.find(z3_constraint) != + smithril_ast_expr_unsat_core.end()) { + ref constraint = + env.smithril_ast_expr_to_klee_expr[z3_constraint]; + if (Expr::createIsZero(constraint) != query.getOriginalQueryExpr()) { + unsatCore.insert(constraint); + } + } + } + + assert(validityCore && "validityCore cannot be nullptr"); + *validityCore = ValidityCore(unsatCore, query.getOriginalQueryExpr()); + + // Z3_ast_vector assertions = + // Z3_solver_get_assertions(builder->ctx, theSolver); + // Z3_ast_vector_inc_ref(builder->ctx, assertions); + // unsigned assertionsCount = Z3_ast_vector_size(builder->ctx, assertions); + unsigned assertionsCount = 0; // mixa117 impl smithril_solver_get_assertions + + stats::validQueriesSize += assertionsCount; + stats::validityCoresSize += size; + ++stats::queryValidityCores; + } + + deinitNativeSmithril(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 + } + + return false; // failed +} + +// mixa117 handleSolverResponse - double check (for me) +SolverImpl::SolverRunStatus SmithrilSolverImpl::handleSolverResponse( + smithril::SmithrilSolver theSolver, smithril::SolverResult satisfiable, + const SmithrilSolverEnv &env, ObjectAssignment needObjects, + std::vector> *values, bool &hasSolution) { + switch (satisfiable) { + case smithril::SolverResult::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) { + SparseStorageImpl data; + + if (env.usedArrayBytes.count(array)) { + std::unordered_set offsetValues; + for (const ref &offsetExpr : env.usedArrayBytes.at(array)) { + std::string arrayElementOffsetExpr = + smithril_eval(theSolver, builder->construct(offsetExpr)); + + uint64_t concretizedOffsetValue = std::stoull(arrayElementOffsetExpr); + offsetValues.insert(concretizedOffsetValue); + } + + for (unsigned offset : offsetValues) { + // We can't use Term here so have to do ref counting manually + smithril::SmithrilTerm initial_read = + builder->getInitialRead(array, offset); + + std::string initial_read_expr = + smithril_eval(theSolver, initial_read); + + uint64_t arrayElementValue = std::stoull(initial_read_expr); + data.store(offset, arrayElementValue); + } + } + + values->emplace_back(std::move(data)); + } + + assert(values->size() == objects->size()); + + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + case smithril::SolverResult::Unsat: + hasSolution = false; + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + case smithril::SolverResult::Unknown: { + return SolverImpl::SOLVER_RUN_STATUS_FAILURE; + } + default: + llvm_unreachable("unhandled smithril result"); + } +} + +SolverImpl::SolverRunStatus SmithrilSolverImpl::getOperationStatusCode() { + return runStatusCode; +} + +class SmithrilNonIncSolverImpl final : public SmithrilSolverImpl { +private: +public: + SmithrilNonIncSolverImpl() = default; + + /// implementation of BitwuzlaSolverImpl interface + smithril::SmithrilSolver initNativeSmithril(const ConstraintQuery &, + SmithrilASTIncSet &) override { + auto ctx = builder->ctx; + + smithril::SmithrilSolver theSolver = + smithril_new_solver(ctx, solverParameters); + return theSolver; + } + + void deinitNativeSmithril(smithril::SmithrilSolver theSolver) override { + deleteNativeSmithril(theSolver); + } + + void push(smithril::SmithrilSolver) override {} + + /// implementation of the SolverImpl interface + bool computeTruth(const Query &query, bool &isValid) override { + SmithrilSolverEnv env; + return SmithrilSolverImpl::computeTruth(ConstraintQuery(query, false), env, + isValid); + } + bool computeValue(const Query &query, ref &result) override { + SmithrilSolverEnv env; + return SmithrilSolverImpl::computeValue(ConstraintQuery(query, false), env, + result); + } + bool + computeInitialValues(const Query &query, + const std::vector &objects, + std::vector> &values, + bool &hasSolution) override { + SmithrilSolverEnv env(objects); + return SmithrilSolverImpl::computeInitialValues( + ConstraintQuery(query, false), env, values, hasSolution); + } + bool check(const Query &query, ref &result) override { + SmithrilSolverEnv env; + return SmithrilSolverImpl::check(ConstraintQuery(query, false), env, + result); + } + bool computeValidityCore(const Query &query, ValidityCore &validityCore, + bool &isValid) override { + SmithrilSolverEnv env; + return SmithrilSolverImpl::computeValidityCore( + ConstraintQuery(query, false), env, validityCore, isValid); + } + void notifyStateTermination(std::uint32_t) override {} +}; + +SmithrilSolver::SmithrilSolver() + : 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 SmithrilIncNativeSolver { +private: + std::optional nativeSolver; + smithril::SmithrilContext solverContext; + + smithril::SmithrilOptions solverParameters; + /// underlying solver frames + /// saved only for calculating distances from next queries + ConstraintFrames frames; + + void pop(size_t popSize); + +public: + SmithrilSolverEnv env; + std::uint32_t stateID = 0; + bool isRecycled = false; + + SmithrilIncNativeSolver(smithril::SmithrilOptions solverParameters) + : solverParameters(solverParameters) {} + ~SmithrilIncNativeSolver(); + + void clear(); + + void distance(const ConstraintQuery &query, ConstraintDistance &delta) const; + + void popPush(ConstraintDistance &delta); + + smithril::SmithrilSolver getOrInit(); + + bool isConsistent() const { + return frames.framesSize() == env.objects.framesSize(); + } + + void dump() const { ::klee::dump(frames); } +}; + +void SmithrilIncNativeSolver::pop(size_t popSize) { + if (!nativeSolver || !popSize) + return; + smithril::smithril_pop(nativeSolver.value(), popSize); +} + +void SmithrilIncNativeSolver::popPush(ConstraintDistance &delta) { + env.pop(delta.toPopSize); + pop(delta.toPopSize); + frames.pop(delta.toPopSize); + frames.extend(delta.toPush.constraints); +} + +smithril::SmithrilSolver SmithrilIncNativeSolver::getOrInit() { + if (!nativeSolver.has_value()) { + nativeSolver = + smithril::smithril_new_solver(solverContext, solverParameters); + } + return nativeSolver.value(); +} + +SmithrilIncNativeSolver::~SmithrilIncNativeSolver() { + if (nativeSolver.has_value()) { + deleteNativeSmithril(nativeSolver.value()); + } +} + +void SmithrilIncNativeSolver::clear() { + if (!nativeSolver.has_value()) + return; + env.clear(); + frames.clear(); + smithril_reset(nativeSolver.value()); + isRecycled = false; +} + +void SmithrilIncNativeSolver::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 SmithrilTreeSolverImpl final : public SmithrilSolverImpl { +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: + SmithrilTreeSolverImpl(size_t maxSolvers) : maxSolvers(maxSolvers){}; + + /// implementation of SmithrilSolverImpl interface + smithril::SmithrilSolver initNativeSmithril(const ConstraintQuery &, + SmithrilASTIncSet &) override { + return currentSolver->getOrInit(); + } + + void deinitNativeSmithril(smithril::SmithrilSolver) override { + assert(currentSolver->isConsistent()); + solvers.push_back(std::move(currentSolver)); + } + void push(smithril::SmithrilSolver s) override { smithril_push(s); } + + /// 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 SmithrilTreeSolverImpl::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 SmithrilTreeSolverImpl::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 SmithrilTreeSolverImpl::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 SmithrilTreeSolverImpl::computeTruth(const Query &query, bool &isValid) { + auto q = prepare(query); + return SmithrilSolverImpl::computeTruth(q, currentSolver->env, isValid); +} + +bool SmithrilTreeSolverImpl::computeValue(const Query &query, + ref &result) { + auto q = prepare(query); + return SmithrilSolverImpl::computeValue(q, currentSolver->env, result); +} + +bool SmithrilTreeSolverImpl::computeInitialValues( + const Query &query, const std::vector &objects, + std::vector> &values, bool &hasSolution) { + auto q = prepare(query); + currentSolver->env.objectsForGetModel = objects; + return SmithrilSolverImpl::computeInitialValues(q, currentSolver->env, values, + hasSolution); +} + +bool SmithrilTreeSolverImpl::check(const Query &query, + ref &result) { + auto q = prepare(query); + return SmithrilSolverImpl::check(q, currentSolver->env, result); +} + +bool SmithrilTreeSolverImpl::computeValidityCore(const Query &query, + ValidityCore &validityCore, + bool &isValid) { + auto q = prepare(query); + return SmithrilSolverImpl::computeValidityCore(q, currentSolver->env, + validityCore, isValid); +} + +void SmithrilTreeSolverImpl::notifyStateTermination(std::uint32_t id) { + for (auto &s : solvers) + if (s->stateID == id) + s->isRecycled = true; +} + +SmithrilTreeSolver::SmithrilTreeSolver(unsigned maxSolvers) + : Solver(std::make_unique(maxSolvers)) {} + +} // namespace klee +#endif // ENABLE_SMITHRIL diff --git a/lib/Solver/SmithrilSolver.h b/lib/Solver/SmithrilSolver.h new file mode 100644 index 0000000000..90658e8b7d --- /dev/null +++ b/lib/Solver/SmithrilSolver.h @@ -0,0 +1,23 @@ +#ifndef SMITHRILSOLVER_H_ +#define SMITHRILSOLVER_H_ + +#include "klee/Solver/Solver.h" + +namespace klee { + +/// SmithrilCompleteSolver - A complete solver based on Smithril +class SmithrilSolver : public Solver { +public: + /// SmithrilSolver - Construct a new SmithrilSolver. + SmithrilSolver(); + std::string getConstraintLog(const Query &) final; +}; + +class SmithrilTreeSolver : public Solver { +public: + SmithrilTreeSolver(unsigned maxSolvers); +}; + +} // namespace klee + +#endif diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index 54e7902869..66d45ce100 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -196,10 +196,18 @@ cl::opt MetaSMTBackend( #endif /* ENABLE_METASMT */ // Pick the default core solver based on configuration -#ifdef ENABLE_BITWUZLA +#ifdef ENABLE_SMITHRIL #define STP_IS_DEFAULT_STR "" #define METASMT_IS_DEFAULT_STR "" #define Z3_IS_DEFAULT_STR "" +#define BITWUZLA_IS_DEFAULT_STR "" +#define SMITHRIL_IS_DEFAULT_STR " (default)" +#define DEFAULT_CORE_SOLVER SMITHRIL_SOLVER +#elif ENABLE_BITWUZLA +#define STP_IS_DEFAULT_STR "" +#define METASMT_IS_DEFAULT_STR "" +#define Z3_IS_DEFAULT_STR "" +#define SMITHRIL_IS_DEFAULT_STR "" #define BITWUZLA_IS_DEFAULT_STR " (default)" #define DEFAULT_CORE_SOLVER BITWUZLA_SOLVER #elif ENABLE_Z3 @@ -207,19 +215,21 @@ cl::opt MetaSMTBackend( #define METASMT_IS_DEFAULT_STR "" #define Z3_IS_DEFAULT_STR " (default)" #define BITWUZLA_IS_DEFAULT_STR "" +#define SMITHRIL_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 SMITHRIL_IS_DEFAULT_STR "" #define DEFAULT_CORE_SOLVER STP_SOLVER #elif ENABLE_METASMT #define STP_IS_DEFAULT_STR "" +#define SMITHRIL_IS_DEFAULT_STR "" #define METASMT_IS_DEFAULT_STR " (default)" #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" @@ -232,6 +242,10 @@ cl::opt CoreSolverToUse( "Bitwuzla" BITWUZLA_IS_DEFAULT_STR), clEnumValN(BITWUZLA_TREE_SOLVER, "bitwuzla-tree", "Bitwuzla tree-incremental solver"), + clEnumValN(SMITHRIL_SOLVER, "smithril", + "Smithril" SMITHRIL_IS_DEFAULT_STR), + clEnumValN(SMITHRIL_TREE_SOLVER, "smithril-tree", + "Smithril 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"), @@ -248,6 +262,7 @@ cl::opt DebugCrossCheckCoreSolverWith( clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValN(Z3_SOLVER, "z3", "Z3"), clEnumValN(BITWUZLA_SOLVER, "bitwuzla", "Bitwuzla"), + clEnumValN(SMITHRIL_SOLVER, "smithril", "Smithril"), clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)")), cl::init(NO_SOLVER), cl::cat(SolvingCat)); @@ -267,4 +282,5 @@ llvm::cl::opt SymbolicAllocationThreshold( #undef METASMT_IS_DEFAULT_STR #undef Z3_IS_DEFAULT_STR #undef BITWUZLA_IS_DEFAULT_STR +#undef SMITHRIL_IS_DEFAULT_STR #undef DEFAULT_CORE_SOLVER diff --git a/lib/Solver/Z3BitvectorBuilder.cpp b/lib/Solver/Z3BitvectorBuilder.cpp index 1a59444091..e87066c553 100644 --- a/lib/Solver/Z3BitvectorBuilder.cpp +++ b/lib/Solver/Z3BitvectorBuilder.cpp @@ -1044,10 +1044,9 @@ Z3ASTHandle Z3BitvectorBuilder::castToFloat(const Z3ASTHandle &e) { assert(Z3_get_bv_sort_size(ctx, ieeeBitPatternSort) == 79); #endif - Z3ASTHandle ieeeBitPatternAsFloat = - Z3ASTHandle(Z3_mk_fpa_to_fp_bv(ctx, ieeeBitPattern, - getFloatSortFromBitWidth(bitWidth)), - ctx); + Z3ASTHandle ieeeBitPatternAsFloat = Z3ASTHandle( + Z3_mk_fpa_fp(ctx, signBit, exponentBits, significandFractionBits), + ctx); // Generate side constraint on the significand integer bit. It is not // used in `ieeeBitPatternAsFloat` so we need to constrain that bit to diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc index 5be1cd292e..97bab94212 100644 --- a/scripts/build/p-klee.inc +++ b/scripts/build/p-klee.inc @@ -71,6 +71,7 @@ fi 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") + local KLEE_SMITHRIL_CONFIGURE_OPTION=("-DENABLE_SOLVER_SMITHRIL=OFF") KLEE_FLOATING_POINT=( "-DENABLE_FLOATING_POINT=FALSE" "-DENABLE_FP_RUNTIME=FALSE" @@ -98,6 +99,17 @@ fi "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}" ) ;; + smithril) + echo "smithril" + KLEE_SMITHRIL_CONFIGURE_OPTION=( + "-DENABLE_SOLVER_SMITHRIL=TRUE" + ) + CMAKE_PREFIX_PATH+=("${SMITHRIL_INSTALL_PATH}") + KLEE_FLOATING_POINT=( + "-DENABLE_FLOATING_POINT=TRUE" + "-DENABLE_FP_RUNTIME=TRUE" + ) + ;; metasmt) echo "metaSMT" if [ "X${METASMT_DEFAULT}" == "X" ]; then @@ -131,6 +143,7 @@ fi "${KLEE_STP_CONFIGURE_OPTION[@]}" "${KLEE_METASMT_CONFIGURE_OPTION[@]}" "${KLEE_BITWUZLA_CONFIGURE_OPTION[@]}" + "${KLEE_SMITHRIL_CONFIGURE_OPTION[@]}" "${KLEE_FLOATING_POINT[@]}" ) diff --git a/scripts/build/p-smithril-linux-ubuntu.inc b/scripts/build/p-smithril-linux-ubuntu.inc new file mode 100644 index 0000000000..4c7d5cc14d --- /dev/null +++ b/scripts/build/p-smithril-linux-ubuntu.inc @@ -0,0 +1,35 @@ +# Build dependencies Smithril +install_build_dependencies_smithril() { + source "${DIR}/common-functions" + with_sudo apt update -y + + dependencies=( + build-essential + + ninja-build + python3 + python3-pip + cmake + curl + git + wget + ca-certificates + libclang-dev + libssl-dev + ) + + + #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 + + pip3 install --user meson + base_path="$(python3 -m site --user-base)" + export PATH="$PATH:${base_path}/bin" + + curl https://sh.rustup.rs -sSf | sh -s -- -y + . "$HOME/.cargo/env" + cargo install cargo-c +} diff --git a/scripts/build/p-smithril-osx.inc b/scripts/build/p-smithril-osx.inc new file mode 100644 index 0000000000..27df98058e --- /dev/null +++ b/scripts/build/p-smithril-osx.inc @@ -0,0 +1,14 @@ +install_build_dependencies_bitwuzla() { + dependencies=( + ninja + python3 + python3-pip + cmake + git + pkg-config + ) + brew install "${dependencies[@]}" + pip3 install --user meson + base_path="$(python3 -m site --user-base)" + export PATH="$PATH:${base_path}/bin" +} diff --git a/scripts/build/p-smithril.inc b/scripts/build/p-smithril.inc new file mode 100644 index 0000000000..c96c9c8e08 --- /dev/null +++ b/scripts/build/p-smithril.inc @@ -0,0 +1,62 @@ +# Build scripts for Smithril +# Variables that any artifact of this package might depend on +setup_build_variables_smithril() { + SMITHRIL_BUILD_PATH="${BASE}/smithril-${SMITHRIL_VERSION}" + SMITHRIL_INSTALL_PATH="${BASE}/smithril-${SMITHRIL_VERSION}-install" + SMITHRIL_SYS_INSTALL_PATH="${BASE}/smithril-sys" + smithril_url="https://github.com/smithril/smithril.git" + + return 0 +} + +download_smithril() { + source "${DIR}/common-functions" + # Download Smithril + git_clone_or_update "${smithril_url}" "${BASE}/smithril-${SMITHRIL_VERSION}" "${SMITHRIL_VERSION}" +} + +build_smithril() { + pushd "${BASE}/smithril-${SMITHRIL_VERSION}" + + ( + rustup default nightly + cargo cinstall --destdir="/" --prefix="${SMITHRIL_INSTALL_PATH}" --features ipc-runner + cargo install --path "smithril-runner" --root "${SMITHRIL_INSTALL_PATH}" + ) + popd + cd "${SMITHRIL_INSTALL_PATH}" || return 1 + touch "${SMITHRIL_INSTALL_PATH}/.smithril_installed" +} + +install_smithril() { + return 0 +} + +# Check if the binary artifact is installed +is_installed_smithril() { + ( + setup_build_variables_smithril + [[ -f "${SMITHRIL_INSTALL_PATH}/.smithril_installed" ]] + ) || return 1 +} + +setup_artifact_variables_smithril() { + setup_build_variables_smithril +} + +get_build_artifacts_smithril() { + ( + setup_build_variables_smithril + echo "${SMITHRIL_INSTALL_PATH}" + ) +} + +get_docker_config_id_smithril() { + ( + source "${DIR}/common-functions" + setup_build_variables_smithril + + smithril_remote_commit="$(get_git_hash "${smithril_url}" "${SMITHRIL_VERSION}")" + echo "${smithril_remote_commit}" + ) +} diff --git a/scripts/build/v-smithril.inc b/scripts/build/v-smithril.inc new file mode 100644 index 0000000000..98fd267bd1 --- /dev/null +++ b/scripts/build/v-smithril.inc @@ -0,0 +1,10 @@ +# Build information for Smithril solver +required_variables_smithril=( + "SMITHRIL_VERSION" +) + +artifact_dependency_smithril=("") + +install_build_dependencies_smithril() { + return 0 +} diff --git a/scripts/build/v-solvers.inc b/scripts/build/v-solvers.inc index 74cdac1f5a..8ab5f3a5c2 100644 --- a/scripts/build/v-solvers.inc +++ b/scripts/build/v-solvers.inc @@ -16,6 +16,7 @@ required_variables_check_solvers() { [[ "${solver}" == "stp" ]] && continue [[ "${solver}" == "metasmt" ]] && continue [[ "${solver}" == "bitwuzla" ]] && continue + [[ "${solver}" == "smithril" ]] && continue echo "Unknown solver: \"$solver\"" exit 1 @@ -53,6 +54,7 @@ setup_variables_solvers() { [[ "${solver}" == "stp" ]] && SELECTED_SOLVERS+=("stp") && continue [[ "${solver}" == "metasmt" ]] && SELECTED_SOLVERS+=("metasmt") && continue [[ "${solver}" == "bitwuzla" ]] && SELECTED_SOLVERS+=("bitwuzla") && continue + [[ "${solver}" == "smithril" ]] && SELECTED_SOLVERS+=("smithril") && continue echo "Unknown solver: \"$solver\"" exit 1 done @@ -61,4 +63,4 @@ setup_variables_solvers() { SELECTED_SOLVERS=( $( for e in "${SELECTED_SOLVERS[@]}"; do echo "$e"; done | sort|uniq) ) # TODO Add specific suffix of each solver SOLVER_SUFFIX=$(IFS=_ ; echo "${SELECTED_SOLVERS[*]}") -} \ No newline at end of file +} diff --git a/scripts/build/v-z3.inc b/scripts/build/v-z3.inc index 92e68658b7..d7c98569e4 100644 --- a/scripts/build/v-z3.inc +++ b/scripts/build/v-z3.inc @@ -4,4 +4,4 @@ required_variables_z3=( ) # Artifacts Z3 depends on -artifact_dependency_z3=("sanitizer") \ No newline at end of file +artifact_dependency_z3=("sanitizer") diff --git a/scripts/kleef b/scripts/kleef index a559517f71..044e9b28a1 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -34,7 +34,8 @@ def klee_options( "--use-forked-solver=false", # "--solver-backend=stp", # "--solver-backend=z3-tree", - "--solver-backend=bitwuzla", + # "--solver-backend=bitwuzla-tree", + # "--solver-backend=smithril-tree", "--max-solvers-approx-tree-inc=16", # Just use half of the memory in case we have to fork f"--max-memory={int(max_memory * 0.7)}", diff --git a/test/Feature/LargeArrayBecomesSym.c b/test/Feature/LargeArrayBecomesSym.c index d96d1a2598..478255a8b0 100644 --- a/test/Feature/LargeArrayBecomesSym.c +++ b/test/Feature/LargeArrayBecomesSym.c @@ -4,7 +4,8 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out /* The solver timeout is needed as some solvers, such as metaSMT+CVC4, time out here. */ -// RUN: %klee --max-solver-time=2 --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --max-solver-time=2 --output-dir=%t.klee-out %t1.bc > %t-output.txt 2>&1 +// RUN: FileCheck -input-file=%t-output.txt %s #include "klee/klee.h" diff --git a/test/Feature/LazyInitialization/PointerOffset.c b/test/Feature/LazyInitialization/PointerOffset.c index 3575b02173..e5e56995af 100644 --- a/test/Feature/LazyInitialization/PointerOffset.c +++ b/test/Feature/LazyInitialization/PointerOffset.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc +// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc > %t-output.txt 2>&1 // RUN: %ktest-tool %t.klee-out/test*.ktest > %t.log // RUN: FileCheck %s -input-file=%t.log // CHECK: pointers: [(0, 1, 4)] diff --git a/test/Feature/LazyInitialization/SingleInitializationAndAccess.c b/test/Feature/LazyInitialization/SingleInitializationAndAccess.c index b185a6071e..c4ca308f81 100644 --- a/test/Feature/LazyInitialization/SingleInitializationAndAccess.c +++ b/test/Feature/LazyInitialization/SingleInitializationAndAccess.c @@ -1,6 +1,7 @@ // RUN: %clang %s -emit-llvm -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --skip-local=false --use-sym-size-li --min-number-elements-li=1 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --skip-local=false --use-sym-size-li --min-number-elements-li=1 %t1.bc > %t-output.txt 2>&1 +// RUN: FileCheck -input-file=%t-output.txt %s #include "klee/klee.h" #include diff --git a/test/Feature/LazyInitialization/TwoObjectsInitialization.c b/test/Feature/LazyInitialization/TwoObjectsInitialization.c index 957f4bd7da..c971d68389 100644 --- a/test/Feature/LazyInitialization/TwoObjectsInitialization.c +++ b/test/Feature/LazyInitialization/TwoObjectsInitialization.c @@ -1,6 +1,7 @@ // RUN: %clang %s -emit-llvm -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t1.bc > %t-output.txt 2>&1 +// RUN: FileCheck -input-file=%t-output.txt %s #include "klee/klee.h" #include diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c index b7ac1f4aee..5d1b107d08 100644 --- a/test/Feature/SolverTimeout.c +++ b/test/Feature/SolverTimeout.c @@ -1,6 +1,7 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t.bc > %t-output.txt 2>&1 +// RUN: FileCheck -input-file=%t-output.txt %s // // Note: This test occasionally fails when using Z3 4.4.1 #include "klee/klee.h" diff --git a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c index 596ed0dff2..4d91046fae 100644 --- a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c +++ b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c @@ -1,6 +1,3 @@ -// freebsd on cirrus ci has problems with gcov, so disabling -// REQUIRES: not-freebsd - // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --delete-dead-loops=false --use-forked-solver=false --max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=all %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s diff --git a/test/Industry/CoverageBranches/CostasArray-17.c b/test/Industry/CoverageBranches/CostasArray-17.c index e2b1bd6c8d..4527144a2b 100644 --- a/test/Industry/CoverageBranches/CostasArray-17.c +++ b/test/Industry/CoverageBranches/CostasArray-17.c @@ -1,6 +1,3 @@ -// freebsd on cirrus ci has problems with gcov, so disabling -// REQUIRES: not-freebsd - // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs %t1.bc diff --git a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c index a34dedae03..1ba831c70a 100644 --- a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c +++ b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c @@ -1,6 +1,3 @@ -// freebsd on cirrus ci has problems with gcov, so disabling -// REQUIRES: not-freebsd - // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-policy=all --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc diff --git a/test/Industry/CoverageBranches/matrix-2-2.c b/test/Industry/CoverageBranches/matrix-2-2.c index 1946bfc20c..b8f9b71e1d 100644 --- a/test/Industry/CoverageBranches/matrix-2-2.c +++ b/test/Industry/CoverageBranches/matrix-2-2.c @@ -1,6 +1,3 @@ -// freebsd on cirrus ci has problems with gcov, so disabling -// REQUIRES: not-freebsd - // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=all --max-cycles=2 --optimize=true --emit-all-errors --delete-dead-loops=false --use-forked-solver=false --max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=all --use-sym-size-alloc=true --symbolic-allocation-threshold=8192 %t1.bc 2>&1 diff --git a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c index 1559177c06..458c9dc80a 100644 --- a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c +++ b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c @@ -1,6 +1,3 @@ -// freebsd on cirrus ci has problems with gcov, so disabling -// REQUIRES: not-freebsd - // REQUIRES: lt-llvm-15.0 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index fa226f9e56..ac57449ef4 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -58,6 +58,7 @@ 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_smithril = True if @ENABLE_SMITHRIL@ == 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