Patch by Dan Liew that removes our internal copy of STP, and makes the --with-stp option mandatory:

"1. At configure time the --with-stp= option is now mandatory.
 2. The HAVE_EXT_STP macro has been removed.
 3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed."



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8

13 files changed, 39 insertions, 85 deletions

diff --git a/Makefile b/Makefile
index 44a9b836..ec197a4a 100644
--- a/Makefile
+++ b/Makefile
@@ -14,11 +14,7 @@ LEVEL = .
 
 include $(LEVEL)/Makefile.config
 
-DIRS = lib
-ifeq ($(ENABLE_EXT_STP),0)
-  DIRS += stp
-endif
-DIRS += tools runtime
+DIRS = lib tools runtime
 EXTRA_DIST = include
 
 # Only build support directories when building unittests.
diff --git a/Makefile.common b/Makefile.common
index c458f600..bf99b1f3 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -29,13 +29,8 @@ endif
 # Needed to build runtime library using clang (gnu89 is the gcc default)
 C.Flags += -std=gnu89
 
-ifeq ($(ENABLE_EXT_STP),1)
-  LD.Flags += -L$(STP_ROOT)/lib
-  CXX.Flags += -I$(STP_ROOT)/include
-else
-  LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
-  CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
-endif
+LD.Flags += -L$(STP_ROOT)/lib
+CXX.Flags += -I$(STP_ROOT)/include
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_LIB_DIR=\"$(PROJ_libdir)\"
 
 # For STP.
diff --git a/Makefile.config.in b/Makefile.config.in
index b4a5091c..c392136a 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -24,7 +24,6 @@ PROJ_OBJ_ROOT := $(subst //,/,@abs_top_builddir@)
 # Set the root directory of this project's install prefix
 PROJ_INSTALL_ROOT := @prefix@
 
-ENABLE_EXT_STP := @ENABLE_EXT_STP@
 STP_ROOT := @STP_ROOT@
 
 ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 2fa4fba0..928649b6 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -312,14 +312,26 @@ AC_CHECK_HEADERS([selinux/selinux.h],
         AC_SUBST(HAVE_SELINUX, 1),
         AC_SUBST(HAVE_SELINUX, 0))
 
+dnl **************************************************************************
+dnl Find an install of STP
+dnl **************************************************************************
+
 AC_ARG_WITH(stp,
   AS_HELP_STRING([--with-stp],
-    [Location of STP installation directory]),,)
+    [Location of STP installation directory]),,
+    [AC_MSG_ERROR([The --with-stp=<path> argument is mandatory where <path> is the path \
+to the root of your STP install])])
 
-if test X$with_stp = X ; then
-  AC_SUBST(ENABLE_EXT_STP,[[0]])
+#Check for empty argument
+if test "X$with_stp" = X ; then
+	AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
 else
-  stp_root=`cd $with_stp 2> /dev/null; pwd`
+  stp_root=`(cd $with_stp && 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])
+  fi
 
   old_CPPFLAGS="$CPPFLAGS"
   CPPFLAGS="$CPPFLAGS -I$stp_root/include"
@@ -332,8 +344,6 @@ else
          AC_MSG_ERROR([Unable to link with libstp])
   ], -L$stp_root/lib)
 
-  AC_DEFINE(HAVE_EXT_STP, 1, [Using external STP])
-  AC_SUBST(ENABLE_EXT_STP,[[1]])
   AC_SUBST(STP_ROOT,$stp_root)
 fi
 
@@ -346,7 +356,6 @@ AC_CONFIG_MAKEFILE(Makefile)
 AC_CONFIG_MAKEFILE(Makefile.common)
 AC_CONFIG_MAKEFILE(lib/Makefile)
 AC_CONFIG_MAKEFILE(runtime/Makefile)
-AC_CONFIG_MAKEFILE(stp/Makefile)
 AC_CONFIG_MAKEFILE(test/Makefile)
 AC_CONFIG_MAKEFILE(test/Makefile.tests)
 AC_CONFIG_MAKEFILE(tools/Makefile)
diff --git a/configure b/configure
index 594592ef..2ac22106 100755
--- a/configure
+++ b/configure
@@ -597,7 +597,6 @@ ac_includes_default="\
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
 STP_ROOT
-ENABLE_EXT_STP
 CXXCPP
 ac_ct_CXX
 CXXFLAGS
@@ -4366,17 +4365,26 @@ done
 
 
 
+
 # Check whether --with-stp was given.
 if test "${with_stp+set}" = set; then :
   withval=$with_stp;
+else
+  as_fn_error $? "The --with-stp=<path> argument is mandatory where <path> is the path \
+to the root of your STP install" "$LINENO" 5
 fi
 
 
-if test X$with_stp = X ; then
-  ENABLE_EXT_STP=0
-
+#Check for empty argument
+if test "X$with_stp" = X ; then
+	as_fn_error $? "<path> cannot be empty in --with-stp=<path>" "$LINENO" 5
 else
-  stp_root=`cd $with_stp 2> /dev/null; pwd`
+  stp_root=`(cd $with_stp && 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
+  fi
 
   old_CPPFLAGS="$CPPFLAGS"
   CPPFLAGS="$CPPFLAGS -I$stp_root/include"
@@ -4442,11 +4450,6 @@ else
 fi
 
 
-
-$as_echo "#define HAVE_EXT_STP 1" >>confdefs.h
-
-  ENABLE_EXT_STP=1
-
   STP_ROOT=$stp_root
 
 fi
@@ -4464,9 +4467,6 @@ ac_config_commands="$ac_config_commands lib/Makefile"
 ac_config_commands="$ac_config_commands runtime/Makefile"
 
 
-ac_config_commands="$ac_config_commands stp/Makefile"
-
-
 ac_config_commands="$ac_config_commands test/Makefile"
 
 
@@ -5180,7 +5180,6 @@ do
     "Makefile.common") CONFIG_COMMANDS="$CONFIG_COMMANDS Makefile.common" ;;
     "lib/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS lib/Makefile" ;;
     "runtime/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS runtime/Makefile" ;;
-    "stp/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS stp/Makefile" ;;
     "test/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS test/Makefile" ;;
     "test/Makefile.tests") CONFIG_COMMANDS="$CONFIG_COMMANDS test/Makefile.tests" ;;
     "tools/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS tools/Makefile" ;;
@@ -5740,8 +5739,6 @@ $as_echo "$as_me: executing $ac_file commands" >&6;}
    ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/lib/Makefile lib/Makefile ;;
     "runtime/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname runtime/Makefile`
    ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/runtime/Makefile runtime/Makefile ;;
-    "stp/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname stp/Makefile`
-   ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/stp/Makefile stp/Makefile ;;
     "test/Makefile":C) ${llvm_src}/autoconf/mkinstalldirs `dirname test/Makefile`
    ${SHELL} ${llvm_src}/autoconf/install-sh -m 0644 -c ${srcdir}/test/Makefile test/Makefile ;;
     "test/Makefile.tests":C) ${llvm_src}/autoconf/mkinstalldirs `dirname test/Makefile.tests`
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index ca81155f..4ce9714d 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -6,9 +6,6 @@
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
-/* Using external STP */
-#undef HAVE_EXT_STP
-
 /* Define to 1 if you have the <inttypes.h> header file. */
 #undef HAVE_INTTYPES_H
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 2b34c911..3a19a639 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -17,11 +17,7 @@
 #include <map>
 
 #define Expr VCExpr
-#ifdef HAVE_EXT_STP
 #include <stp/c_interface.h>
-#else
-#include "../../stp/c_interface/c_interface.h"
-#endif
 
 #if ENABLE_STPLOG == 1
 #include "stp/stplog.h"
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 9f0d89af..7430a58b 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -454,7 +454,6 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim
   assert(vc && "unable to create validity checker");
   assert(builder && "unable to create STPBuilder");
 
-#ifdef HAVE_EXT_STP
   // In newer versions of STP, a memory management mechanism has been
   // introduced that automatically invalidates certain C interface
   // pointers at vc_Destroy time.  This caused double-free errors
@@ -462,7 +461,7 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim
   // the pointers using vc_DeleteExpr.  By setting EXPRDELETE to 0
   // we restore the old behaviour.
   vc_setInterfaceFlags(vc, EXPRDELETE, 0);
-#endif
+
   vc_registerErrorHandler(::stp_error_handler);
 
   if (useForkedSTP) {
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 21d84cbe..3973a2e6 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -12,18 +12,11 @@ TOOLNAME = kleaver
 
 include $(LEVEL)/Makefile.config
 
-STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a stp_constantbv.a stp_sat.a \
-	stp_simplifier.a
 # FIXME: Ideally we wouldn't have any LLVM dependencies here, which
 # means kicking out klee's Support.
 USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
-ifeq ($(ENABLE_EXT_STP),0)
-  USEDLIBS += $(STP_LIBS)
-endif
 LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
 
-ifeq ($(ENABLE_EXT_STP),1)
-  LIBS += -lstp
-endif
+LIBS += -lstp
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index 23c8f1d9..6e05a5a9 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -12,16 +12,9 @@ TOOLNAME = klee
 
 include $(LEVEL)/Makefile.config
 
-STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a stp_constantbv.a stp_sat.a \
-	stp_simplifier.a
 USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
-ifeq ($(ENABLE_EXT_STP),0)
-  USEDLIBS += $(STP_LIBS)
-endif
 LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
 
 include $(LEVEL)/Makefile.common
 
-ifeq ($(ENABLE_EXT_STP),1)
-  LIBS += -lstp
-endif
+LIBS += -lstp
diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile
index cfd7d0c0..b5c6bdb3 100644
--- a/unittests/Expr/Makefile
+++ b/unittests/Expr/Makefile
@@ -4,16 +4,10 @@ LEVEL := ../..
 include $(LEVEL)/Makefile.config
 
 TESTNAME := Expr
-STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a \
-            stp_constantbv.a stp_sat.a stp_simplifier.a
 USEDLIBS := kleaverExpr.a kleeBasic.a
-ifeq ($(ENABLE_EXT_STP),0)
-  USEDLIBS += $(STP_LIBS)
-endif
+USEDLIBS += $(STP_LIBS)
 LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-ifeq ($(ENABLE_EXT_STP),1)
-  LIBS += -lstp
-endif
+LIBS += -lstp
diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile
index 3117a5fd..94bbb83c 100644
--- a/unittests/Ref/Makefile
+++ b/unittests/Ref/Makefile
@@ -4,16 +4,9 @@ LEVEL := ../..
 include $(LEVEL)/Makefile.config
 
 TESTNAME := RefTest
-STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a \
-            stp_constantbv.a stp_sat.a stp_simplifier.a
 USEDLIBS := kleaverExpr.a kleeBasic.a
-ifeq ($(ENABLE_EXT_STP),0)
-  USEDLIBS += $(STP_LIBS)
-endif
 LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-ifeq ($(ENABLE_EXT_STP),1)
-  LIBS += -lstp
-endif
+LIBS += -lstp
diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile
index 86283d24..00713691 100644
--- a/unittests/Solver/Makefile
+++ b/unittests/Solver/Makefile
@@ -4,16 +4,9 @@ LEVEL := ../..
 include $(LEVEL)/Makefile.config
 
 TESTNAME := Solver
-STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a \
-            stp_constantbv.a stp_sat.a stp_simplifier.a
 USEDLIBS := kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
-ifeq ($(ENABLE_EXT_STP),0)
-  USEDLIBS += $(STP_LIBS)
-endif
 LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-ifeq ($(ENABLE_EXT_STP),1)
-  LIBS += -lstp
-endif
+LIBS += -lstp