From 8a7705ad979096d4e611fb2b8b397c48dd5fffc1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 20:14:01 +0000 Subject: Make it possible to build KLEE without using STP and only MetaSMT. The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency. --- Makefile.common | 9 +++-- Makefile.config.in | 1 + autoconf/configure.ac | 90 +++++++++++++++++++++++++---------------- configure | 78 +++++++++++++++++++---------------- include/klee/CommandLine.h | 4 +- include/klee/Config/config.h.in | 12 +++--- include/klee/Solver.h | 6 ++- lib/Basic/CmdLineOptions.cpp | 27 ++++++++++--- lib/Solver/CoreSolver.cpp | 11 +++-- lib/Solver/MetaSMTBuilder.h | 4 +- lib/Solver/MetaSMTSolver.cpp | 6 +-- lib/Solver/STPBuilder.cpp | 5 ++- lib/Solver/STPSolver.cpp | 4 +- tools/kleaver/Makefile | 4 +- tools/kleaver/main.cpp | 4 +- tools/klee/Makefile | 4 +- unittests/Expr/Makefile | 1 - unittests/Ref/Makefile | 2 - unittests/Solver/Makefile | 4 +- 19 files changed, 169 insertions(+), 107 deletions(-) diff --git a/Makefile.common b/Makefile.common index 7b210118..4ec1d4c6 100644 --- a/Makefile.common +++ b/Makefile.common @@ -61,7 +61,11 @@ endif # This is filename that KLEE will look for when trying to load klee-uclibc KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca" -CXX.Flags += $(STP_CFLAGS) +ifneq ($(ENABLE_STP),0) + CXX.Flags += $(STP_CFLAGS) + CXX.Flags += -DEXT_HASH_MAP +endif + CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\" CXX.Flags += -DKLEE_INSTALL_RUNTIME_DIR=\"$(BYTECODE_DESTINATION)\" @@ -69,9 +73,6 @@ ifeq ($(ENABLE_UCLIBC),1) CXX.Flags += -DKLEE_UCLIBC_BCA_NAME=\"$(KLEE_UCLIBC_BCA_NAME)\" endif -# For STP. -CXX.Flags += -DEXT_HASH_MAP - # For metaSMT ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile diff --git a/Makefile.config.in b/Makefile.config.in index 5b9f929c..745b4cc1 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -29,6 +29,7 @@ PROJ_INSTALL_ROOT := @prefix@ KLEE_USE_CXX11 := @KLEE_USE_CXX11@ +ENABLE_STP := @ENABLE_STP@ STP_CFLAGS := @STP_CFLAGS@ STP_LDFLAGS := @STP_LDFLAGS@ diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 3d4becc8..8ba6a029 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -553,58 +553,70 @@ dnl ************************************************************************** dnl Find an install of STP dnl ************************************************************************** +ENABLE_STP=0 AC_ARG_WITH(stp, AS_HELP_STRING([--with-stp], [Location of STP installation directory]),[ #Check for empty argument if test "X$withval" = X ; then - AC_MSG_ERROR([ cannot be empty in --with-stp=]) + AC_MSG_ERROR([ cannot be empty in --with-stp=]) fi stp_root=`(cd $withval && pwd) 2> /dev/null` #Check for bad path if test "X$stp_root" = X ; then - AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp]) + AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp]) fi STP_CFLAGS="-I$stp_root/include" STP_LDFLAGS="-L$stp_root/lib" + ENABLE_STP=1 ]) -old_CPPFLAGS="$CPPFLAGS" -CPPFLAGS="$CPPFLAGS $STP_CFLAGS" -AC_CHECK_HEADER(stp/c_interface.h,, - [ - AC_MSG_ERROR([Unable to use stp/c_interface.h header]) - ]) -CPPFLAGS="$old_CPPFLAGS" - -STP_NEEDS_MINISAT=0 -AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [ - STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp]) -], "$STP_LDFLAGS") - -dnl Try linking again with minisat if necessary -if test "X$STP_NEEDS_MINISAT" != X0 ; then - # Need to clear cached result - unset ac_cv_lib_stp_vc_setInterfaceFlags - - AC_CHECK_LIB(stp, - vc_setInterfaceFlags,, [ - AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong]) - ], "$STP_LDFLAGS" "-lminisat" ) - - STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" +if test "X$ENABLE_STP" != X0; then + old_CPPFLAGS="$CPPFLAGS" + CPPFLAGS="$CPPFLAGS $STP_CFLAGS" + AC_CHECK_HEADER(stp/c_interface.h,, + [ + AC_MSG_ERROR([Unable to use stp/c_interface.h header]) + ]) + + dnl we use [:] as a no-op so that AC_CHECK_LIB doesn't append -lstp + dnl automatically which would break subsequent uses of AC_CHECK_LIB() + STP_NEEDS_MINISAT=0 + AC_CHECK_LIB(stp, vc_setInterfaceFlags, [:], [ + STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp]) + ], "$STP_LDFLAGS") + CPPFLAGS="$old_CPPFLAGS" + + dnl Try linking again with minisat if necessary + if test "X$STP_NEEDS_MINISAT" != X0 ; then + # Need to clear cached result + unset ac_cv_lib_stp_vc_setInterfaceFlags + + AC_CHECK_LIB(stp, + vc_setInterfaceFlags,[:], [ + AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong]) + ], "$STP_LDFLAGS" "-lminisat" ) + + STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" + else + STP_LDFLAGS="${STP_LDFLAGS} -lstp" + fi + AC_MSG_NOTICE([Using STP solver backend]) + CPPFLAGS="$old_CPPFLAGS" + AC_DEFINE(ENABLE_STP, [1], [Using STP Solver backend]) else - STP_LDFLAGS="${STP_LDFLAGS} -lstp" + AC_MSG_NOTICE([Not using STP solver backend]) fi - +AC_SUBST(ENABLE_STP) AC_SUBST(STP_CFLAGS) AC_SUBST(STP_LDFLAGS) + dnl ************************************************************************** -dnl User option to enable metaSMT constraint solvers and to specify the +dnl User option to enable metaSMT constraint solvers and to specify the dnl the location of the metaSMT root directory dnl ************************************************************************** @@ -613,13 +625,13 @@ AC_ARG_WITH(metasmt, [Location of metaSMT installation directory]),,) if test X$with_metasmt = X ; then - AC_SUBST(ENABLE_METASMT,[[0]]) + ENABLE_METASMT=0 else metasmt_root=`cd $with_metasmt 2> /dev/null; pwd` dnl AC_LANG(C++) old_CPPFLAGS="$CPPFLAGS" - old_LDFLAGS="$LDFLAGS" + old_LDFLAGS="$LDFLAGS" CPPFLAGS="$CPPFLAGS -I$metasmt_root/include" LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT" AC_CHECK_HEADERS([$metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp],, [ @@ -627,14 +639,24 @@ else ]) AC_LINK_IFELSE( [AC_LANG_PROGRAM([#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp], [metaSMT::logic::QF_BV::new_bitvector(3)])], - [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])]) + [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])]) CPPFLAGS="$old_CPPFLAGS" LDFLAGS="$old_LDFLAGS" - AC_DEFINE(SUPPORT_METASMT, 1, [Supporting metaSMT API]) - AC_SUBST(ENABLE_METASMT,[[1]]) + AC_DEFINE(ENABLE_METASMT, 1, [Enable metaSMT API]) AC_SUBST(METASMT_ROOT,$metasmt_root) AC_SUBST(REQUIRES_RTTI,[[1]]) + ENABLE_METASMT=1 +fi + +AC_SUBST(ENABLE_METASMT) + +dnl ************************************************************************** +dnl Check at least one solver backend is enabled +dnl ************************************************************************** + +if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then + AC_MSG_ERROR([At least one solver backend must be enabled, try using --with-stp or --with-metasmt]) fi diff --git a/configure b/configure index 72ed1883..af871ce6 100755 --- a/configure +++ b/configure @@ -624,10 +624,11 @@ ac_includes_default="\ ac_subst_vars='LTLIBOBJS LIBOBJS -METASMT_ROOT ENABLE_METASMT +METASMT_ROOT STP_LDFLAGS STP_CFLAGS +ENABLE_STP CXXCPP HAVE_SELINUX EGREP @@ -4865,43 +4866,45 @@ fi +ENABLE_STP=0 # Check whether --with-stp was given. if test "${with_stp+set}" = set; then : withval=$with_stp; #Check for empty argument if test "X$withval" = X ; then - as_fn_error $? " cannot be empty in --with-stp=" "$LINENO" 5 + as_fn_error $? " cannot be empty in --with-stp=" "$LINENO" 5 fi stp_root=`(cd $withval && pwd) 2> /dev/null` #Check for bad path if test "X$stp_root" = X ; then - as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5 + as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5 fi STP_CFLAGS="-I$stp_root/include" STP_LDFLAGS="-L$stp_root/lib" + ENABLE_STP=1 fi -old_CPPFLAGS="$CPPFLAGS" -CPPFLAGS="$CPPFLAGS $STP_CFLAGS" -ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default" +if test "X$ENABLE_STP" != X0; then + old_CPPFLAGS="$CPPFLAGS" + CPPFLAGS="$CPPFLAGS $STP_CFLAGS" + ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default" if test "x$ac_cv_header_stp_c_interface_h" = xyes; then : else - as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5 + as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5 fi -CPPFLAGS="$old_CPPFLAGS" -STP_NEEDS_MINISAT=0 -{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 + STP_NEEDS_MINISAT=0 + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; } if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then : $as_echo_n "(cached) " >&6 @@ -4938,25 +4941,21 @@ fi { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; } if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then : - cat >>confdefs.h <<_ACEOF -#define HAVE_LIBSTP 1 -_ACEOF - - LIBS="-lstp $LIBS" - + : else - STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5 + STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5 $as_echo "Could not link with libstp" >&6; } fi + CPPFLAGS="$old_CPPFLAGS" -if test "X$STP_NEEDS_MINISAT" != X0 ; then - # Need to clear cached result - unset ac_cv_lib_stp_vc_setInterfaceFlags + if test "X$STP_NEEDS_MINISAT" != X0 ; then + # Need to clear cached result + unset ac_cv_lib_stp_vc_setInterfaceFlags - { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; } if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then : $as_echo_n "(cached) " >&6 @@ -4993,22 +4992,27 @@ fi { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; } if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then : - cat >>confdefs.h <<_ACEOF -#define HAVE_LIBSTP 1 -_ACEOF - - LIBS="-lstp $LIBS" - + : else - as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5 + as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5 fi - STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" + STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat" + else + STP_LDFLAGS="${STP_LDFLAGS} -lstp" + fi + { $as_echo "$as_me:${as_lineno-$LINENO}: Using STP solver backend" >&5 +$as_echo "$as_me: Using STP solver backend" >&6;} + CPPFLAGS="$old_CPPFLAGS" + +$as_echo "#define ENABLE_STP 1" >>confdefs.h + else - STP_LDFLAGS="${STP_LDFLAGS} -lstp" + { $as_echo "$as_me:${as_lineno-$LINENO}: Not using STP solver backend" >&5 +$as_echo "$as_me: Not using STP solver backend" >&6;} fi @@ -5017,6 +5021,7 @@ fi + # Check whether --with-metasmt was given. if test "${with_metasmt+set}" = set; then : withval=$with_metasmt; @@ -5025,7 +5030,6 @@ fi if test X$with_metasmt = X ; then ENABLE_METASMT=0 - else metasmt_root=`cd $with_metasmt 2> /dev/null; pwd` @@ -5073,14 +5077,20 @@ rm -f core conftest.err conftest.$ac_objext \ LDFLAGS="$old_LDFLAGS" -$as_echo "#define SUPPORT_METASMT 1" >>confdefs.h - - ENABLE_METASMT=1 +$as_echo "#define ENABLE_METASMT 1" >>confdefs.h METASMT_ROOT=$metasmt_root REQUIRES_RTTI=1 + ENABLE_METASMT=1 +fi + + + + +if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then + as_fn_error $? "At least one solver backend must be enabled, try using --with-stp or --with-metasmt" "$LINENO" 5 fi diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index 44f1afd4..dc0f135a 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -47,7 +47,7 @@ extern llvm::cl::list queryLoggingOptions; enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER }; extern llvm::cl::opt CoreSolverToUse; -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT enum MetaSMTBackendType { @@ -58,7 +58,7 @@ enum MetaSMTBackendType extern llvm::cl::opt MetaSMTBackend; -#endif /* SUPPORT_METASMT */ +#endif /* ENABLE_METASMT */ //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions template diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index 978c901f..9d34e7b6 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -6,15 +6,18 @@ /* Enable KLEE DEBUG checks */ #undef ENABLE_KLEE_DEBUG +/* Enable metaSMT API */ +#undef ENABLE_METASMT + +/* Using STP Solver backend */ +#undef ENABLE_STP + /* Does the platform use __ctype_b_loc, etc. */ #undef HAVE_CTYPE_EXTERNALS /* Define to 1 if you have the header file. */ #undef HAVE_INTTYPES_H -/* Define to 1 if you have the `stp' library (-lstp). */ -#undef HAVE_LIBSTP - /* Define if mallinfo() is available on this platform. */ #undef HAVE_MALLINFO @@ -93,7 +96,4 @@ /* klee-uclibc is supported */ #undef SUPPORT_KLEE_UCLIBC -/* Supporting metaSMT API */ -#undef SUPPORT_METASMT - #endif diff --git a/include/klee/Solver.h b/include/klee/Solver.h index e3adac6a..fed6191a 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -203,6 +203,7 @@ namespace klee { virtual void setCoreSolverTimeout(double timeout); }; +#ifdef ENABLE_STP /// STPSolver - A complete solver based on STP. class STPSolver : public Solver { public: @@ -222,9 +223,10 @@ namespace klee { /// is off. virtual void setCoreSolverTimeout(double timeout); }; +#endif // ENABLE_STP -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT template class MetaSMTSolver : public Solver { @@ -236,7 +238,7 @@ namespace klee { virtual void setCoreSolverTimeout(double timeout); }; -#endif /* SUPPORT_METASMT */ +#endif /* ENABLE_METASMT */ /* *** */ diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index d7157b25..2f97b200 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -73,7 +73,7 @@ llvm::cl::list queryLoggingOptions( llvm::cl::CommaSeparated ); -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT llvm::cl::opt MetaSMTBackend( "metasmt-backend", @@ -86,16 +86,31 @@ llvm::cl::opt MetaSMTBackend( clEnumValEnd), llvm::cl::init(METASMT_BACKEND_STP)); -#endif /* SUPPORT_METASMT */ - +#endif /* ENABLE_METASMT */ + +// Pick the default core solver based on configuration +#ifdef ENABLE_STP +#define STP_IS_DEFAULT_STR " (default)" +#define METASMT_IS_DEFAULT_STR "" +#define DEFAULT_CORE_SOLVER STP_SOLVER +#elif ENABLE_METASMT +#define STP_IS_DEFAULT_STR "" +#define METASMT_IS_DEFAULT_STR " (default)" +#define DEFAULT_CORE_SOLVER METASMT_SOLVER +#else +#error "Unsupported solver configuration" +#endif llvm::cl::opt CoreSolverToUse( "solver-backend", llvm::cl::desc("Specifiy the core solver backend to use"), - llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp (default)"), - clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"), + llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp" STP_IS_DEFAULT_STR), + clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValEnd), - llvm::cl::init(STP_SOLVER)); + llvm::cl::init(DEFAULT_CORE_SOLVER)); } +#undef STP_IS_DEFAULT_STR +#undef METASMT_IS_DEFAULT_STR +#undef DEFAULT_CORE_SOLVER diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 9d21931d..0d451f27 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -13,7 +13,7 @@ #include "llvm/Support/raw_ostream.h" #include -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT #include #include @@ -61,17 +61,22 @@ static Solver *handleMetaSMT() { llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; return coreSolver; } -#endif /* SUPPORT_METASMT */ +#endif /* ENABLE_METASMT */ namespace klee { Solver *createCoreSolver(CoreSolverType cst) { switch (cst) { case STP_SOLVER: +#ifdef ENABLE_STP llvm::errs() << "Using STP solver backend\n"; return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); +#else + llvm::errs() << "Not compiled with STP support\n"; + return NULL; +#endif case METASMT_SOLVER: -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT llvm::errs() << "Using MetaSMT solver backend\n"; return handleMetaSMT(); #else diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 6da1b492..ffd3cfe9 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -15,7 +15,7 @@ #include "klee/util/ExprHashMap.h" #include "ConstantDivision.h" -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT #include "llvm/Support/CommandLine.h" @@ -1177,6 +1177,6 @@ typename SolverContext::result_type MetaSMTBuilder::constructActu } /* end of namespace klee */ -#endif /* SUPPORT_METASMT */ +#endif /* ENABLE_METASMT */ #endif /* METASMTBUILDER_H_ */ diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 8394bbf3..971ef371 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -6,8 +6,8 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// - -#ifdef SUPPORT_METASMT +#include "klee/Config/config.h" +#ifdef ENABLE_METASMT #include "MetaSMTBuilder.h" #include "klee/Constraints.h" @@ -463,4 +463,4 @@ void MetaSMTSolver::setCoreSolverTimeout(double timeout) { impl->setCoreSolverTimeout(timeout); } } -#endif // SUPPORT_METASMT +#endif // ENABLE_METASMT diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 2f51c2b9..2b07f391 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -6,7 +6,8 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// - +#include "klee/Config/config.h" +#ifdef ENABLE_STP #include "STPBuilder.h" #include "klee/Expr.h" @@ -902,5 +903,5 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { return vc_trueExpr(vc); } } - +#endif // ENABLE_STP diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index cb15a23c..5c49521e 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -6,7 +6,8 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// - +#include "klee/Config/config.h" +#ifdef ENABLE_STP #include "STPBuilder.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" @@ -382,3 +383,4 @@ void STPSolver::setCoreSolverTimeout(double timeout) { impl->setCoreSolverTimeout(timeout); } } +#endif // ENABLE_STP diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index 10b19a20..a72c4c9d 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -19,7 +19,9 @@ LINK_COMPONENTS = support include $(LEVEL)/Makefile.common -LIBS += $(STP_LDFLAGS) +ifneq ($(ENABLE_STP),0) + LIBS += $(STP_LDFLAGS) +endif ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index f91693c5..ea9be41f 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -36,7 +36,7 @@ using namespace llvm; using namespace klee; using namespace klee::expr; -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT #include #include @@ -53,7 +53,7 @@ using namespace klee::expr; using namespace metaSMT; using namespace metaSMT::solver; -#endif /* SUPPORT_METASMT */ +#endif /* ENABLE_METASMT */ diff --git a/tools/klee/Makefile b/tools/klee/Makefile index eb80d845..8e9ac6b7 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -20,7 +20,9 @@ LINK_COMPONENTS += irreader endif include $(LEVEL)/Makefile.common -LIBS += $(STP_LDFLAGS) +ifneq ($(ENABLE_STP),0) + LIBS += $(STP_LDFLAGS) +endif ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile index e52aea31..ca92271a 100644 --- a/unittests/Expr/Makefile +++ b/unittests/Expr/Makefile @@ -10,4 +10,3 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest CXXFLAGS += -DLLVM_29_UNITTEST -LIBS += $(STP_LDFLAGS) diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile index 14dcc8bd..10c4bebd 100644 --- a/unittests/Ref/Makefile +++ b/unittests/Ref/Makefile @@ -8,5 +8,3 @@ USEDLIBS := kleaverExpr.a kleeBasic.a LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest - -LIBS += $(STP_LDFLAGS) diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile index aeac34ac..65edbe7a 100644 --- a/unittests/Solver/Makefile +++ b/unittests/Solver/Makefile @@ -9,4 +9,6 @@ LINK_COMPONENTS := support include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest -LIBS += $(STP_LDFLAGS) +ifneq ($(ENABLE_STP),0) + LIBS += $(STP_LDFLAGS) +endif -- cgit 1.4.1