Upstream STP now depends on an external build of minisat. Attempt to

fix travis build of upstream STP and also how KLEE links against STP.

9 files changed, 98 insertions, 8 deletions

diff --git a/.travis/stp.sh b/.travis/stp.sh
index abc4e566..1c8fdb48 100755
--- a/.travis/stp.sh
+++ b/.travis/stp.sh
@@ -6,6 +6,18 @@ set -e
 STP_LOG="$(pwd)/stp-build.log"
 
 if [ "${STP_VERSION}" == "UPSTREAM" ]; then
+    # Build minisat
+    git clone https://github.com/niklasso/minisat
+    cd minisat
+    mkdir build
+    cd build
+    MINISAT_DIR=`pwd`
+    cmake -DCMAKE_INSTALL_PREFIX=/usr ..
+    make
+    sudo make install
+    cd ../../
+
+    # Build STP
     git clone --depth 1 git://github.com/stp/stp.git src
     mkdir build
     cd build
diff --git a/Makefile.common b/Makefile.common
index 92f5118b..964a7475 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -38,7 +38,6 @@ endif
 # This is filename that KLEE will look for when trying to load klee-uclibc
 KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca"
 
-LD.Flags += $(STP_LDFLAGS)
 CXX.Flags += $(STP_CFLAGS)
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\"
 CXX.Flags += -DKLEE_INSTALL_LIB_DIR=\"$(PROJ_libdir)\"
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 5b9c4e58..8d4f465c 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -576,10 +576,27 @@ AC_CHECK_HEADER(stp/c_interface.h,,
     ])
 CPPFLAGS="$old_CPPFLAGS"
 
+STP_NEEDS_MINISAT=0
 AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
-       AC_MSG_ERROR([Could not link with libstp])
+       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"
+else
+  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+fi
+
+
 AC_SUBST(STP_CFLAGS)
 AC_SUBST(STP_LDFLAGS)
 
diff --git a/configure b/configure
index 82657008..85d10756 100755
--- a/configure
+++ b/configure
@@ -5085,6 +5085,7 @@ fi
 
 CPPFLAGS="$old_CPPFLAGS"
 
+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 :
@@ -5130,11 +5131,72 @@ _ACEOF
 
 else
 
-       as_fn_error $? "Could not link with libstp" "$LINENO" 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
 
 
+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_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
+if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_check_lib_save_LIBS=$LIBS
+LIBS="-lstp "$STP_LDFLAGS" "-lminisat"  $LIBS"
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+/* Override any GCC internal prototype to avoid an error.
+   Use char because int might match the return type of a GCC
+   builtin and then its argument prototype would still apply.  */
+#ifdef __cplusplus
+extern "C"
+#endif
+char vc_setInterfaceFlags ();
+int
+main ()
+{
+return vc_setInterfaceFlags ();
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_cxx_try_link "$LINENO"; then :
+  ac_cv_lib_stp_vc_setInterfaceFlags=yes
+else
+  ac_cv_lib_stp_vc_setInterfaceFlags=no
+fi
+rm -f core conftest.err conftest.$ac_objext \
+    conftest$ac_exeext conftest.$ac_ext
+LIBS=$ac_check_lib_save_LIBS
+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
+
+fi
+
+
+  STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+else
+  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+fi
+
+
 
 
 
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index f66d0598..10b19a20 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -19,7 +19,7 @@ LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index b9506b47..eb80d845 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -20,7 +20,7 @@ LINK_COMPONENTS += irreader
 endif
 include $(LEVEL)/Makefile.common
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile
index a9bfeda1..e52aea31 100644
--- a/unittests/Expr/Makefile
+++ b/unittests/Expr/Makefile
@@ -10,4 +10,4 @@ LINK_COMPONENTS := support
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
 CXXFLAGS += -DLLVM_29_UNITTEST
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile
index 94bbb83c..14dcc8bd 100644
--- a/unittests/Ref/Makefile
+++ b/unittests/Ref/Makefile
@@ -9,4 +9,4 @@ LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile
index 00713691..aeac34ac 100644
--- a/unittests/Solver/Makefile
+++ b/unittests/Solver/Makefile
@@ -9,4 +9,4 @@ LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-LIBS += -lstp
+LIBS += $(STP_LDFLAGS)