From ca22c4dee94552f65e6044341b0365a21d794d65 Mon Sep 17 00:00:00 2001
From: Peter Collingbourne
Date: Wed, 14 Jul 2010 18:54:38 +0000
Subject: Add option to use an external version of STP
This patch adds a new configure option, --with-stp, which configures
KLEE to use an external version of STP instead of the version in the
source tree. It includes documentation referring users to the STP
download location.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108347 91177308-0d34-0410-b5e6-96231b3b80d8
---
Makefile | 8 +-
Makefile.common | 9 +-
Makefile.config.in | 3 +
autoconf/configure.ac | 25 ++++
configure | 294 +++++++++++++++++++++++++++++++++++++++-
include/klee/Config/config.h.in | 6 +
lib/Solver/STPBuilder.h | 4 +
lib/Solver/Solver.cpp | 9 ++
tools/kleaver/Makefile | 13 +-
tools/klee/Makefile | 13 +-
www/GetStarted.html | 34 +++++
11 files changed, 410 insertions(+), 8 deletions(-)
diff --git a/Makefile b/Makefile
index 2c3ab72b..44a9b836 100644
--- a/Makefile
+++ b/Makefile
@@ -12,7 +12,13 @@
#
LEVEL = .
-DIRS = stp lib tools runtime
+include $(LEVEL)/Makefile.config
+
+DIRS = lib
+ifeq ($(ENABLE_EXT_STP),0)
+ DIRS += stp
+endif
+DIRS += tools runtime
EXTRA_DIST = include
# Only build support directories when building unittests.
diff --git a/Makefile.common b/Makefile.common
index f3a8f8be..ff83602c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -26,8 +26,13 @@ LLVMCC := $(LLVMGCC)
LLVMCXX := $(LLVMGXX)
endif
-LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
-CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
+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
CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\"
# For STP.
diff --git a/Makefile.config.in b/Makefile.config.in
index 0b858831..4d9718db 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -20,6 +20,9 @@ PROJ_OBJ_ROOT := $(subst //,/,@abs_top_objdir@)
# 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@
ENABLE_STPLOG := @ENABLE_STPLOG@
ENABLE_UCLIBC := @ENABLE_UCLIBC@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 4266ac47..015c4f44 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -262,6 +262,31 @@ AC_CHECK_HEADERS([selinux/selinux.h],
AC_SUBST(HAVE_SELINUX, 1),
AC_SUBST(HAVE_SELINUX, 0))
+AC_ARG_WITH(stp,
+ AS_HELP_STRING([--with-stp],
+ [Location of STP installation directory]),,)
+
+if test X$with_stp = X ; then
+ AC_SUBST(ENABLE_EXT_STP,[[0]])
+else
+ stp_root=`cd $with_stp 2> /dev/null; pwd`
+
+ old_CPPFLAGS="$CPPFLAGS"
+ CPPFLAGS="$CPPFLAGS -I$stp_root/include"
+ AC_CHECK_HEADER(stp/c_interface.h,, [
+ AC_MSG_ERROR([Unable to use stp/c_interface.h header])
+ ])
+ CPPFLAGS="$old_CPPFLAGS"
+
+ AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
+ 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
+
dnl **************************************************************************
dnl * Create the output files
dnl **************************************************************************
diff --git a/configure b/configure
index 4f24a6b6..e1622458 100755
--- a/configure
+++ b/configure
@@ -674,6 +674,8 @@ CXX
CXXFLAGS
ac_ct_CXX
CXXCPP
+ENABLE_EXT_STP
+STP_ROOT
LIBOBJS
LTLIBOBJS'
ac_subst_files=''
@@ -1275,6 +1277,7 @@ Optional Packages:
--with-uclibc Enable use of the klee uclibc at the given path
--with-runtime Select build configuration for runtime libraries
(default Release)
+ --with-stp Location of STP installation directory
Some influential environment variables:
CC C compiler command
@@ -4952,6 +4955,293 @@ done
+# Check whether --with-stp was given.
+if test "${with_stp+set}" = set; then
+ withval=$with_stp;
+fi
+
+
+if test X$with_stp = X ; then
+ ENABLE_EXT_STP=0
+
+else
+ stp_root=`cd $with_stp 2> /dev/null; pwd`
+
+ old_CPPFLAGS="$CPPFLAGS"
+ CPPFLAGS="$CPPFLAGS -I$stp_root/include"
+ if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+ { echo "$as_me:$LINENO: checking for stp/c_interface.h" >&5
+echo $ECHO_N "checking for stp/c_interface.h... $ECHO_C" >&6; }
+if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+ echo $ECHO_N "(cached) $ECHO_C" >&6
+fi
+{ echo "$as_me:$LINENO: result: $ac_cv_header_stp_c_interface_h" >&5
+echo "${ECHO_T}$ac_cv_header_stp_c_interface_h" >&6; }
+else
+ # Is the header compilable?
+{ echo "$as_me:$LINENO: checking stp/c_interface.h usability" >&5
+echo $ECHO_N "checking stp/c_interface.h usability... $ECHO_C" >&6; }
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h. */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* end confdefs.h. */
+$ac_includes_default
+#include
+_ACEOF
+rm -f conftest.$ac_objext
+if { (ac_try="$ac_compile"
+case "(($ac_try" in
+ *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+ *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+ (eval "$ac_compile") 2>conftest.er1
+ ac_status=$?
+ grep -v '^ *+' conftest.er1 >conftest.err
+ rm -f conftest.er1
+ cat conftest.err >&5
+ echo "$as_me:$LINENO: \$? = $ac_status" >&5
+ (exit $ac_status); } &&
+ { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err'
+ { (case "(($ac_try" in
+ *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+ *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+ (eval "$ac_try") 2>&5
+ ac_status=$?
+ echo "$as_me:$LINENO: \$? = $ac_status" >&5
+ (exit $ac_status); }; } &&
+ { ac_try='test -s conftest.$ac_objext'
+ { (case "(($ac_try" in
+ *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+ *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+ (eval "$ac_try") 2>&5
+ ac_status=$?
+ echo "$as_me:$LINENO: \$? = $ac_status" >&5
+ (exit $ac_status); }; }; then
+ ac_header_compiler=yes
+else
+ echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+ ac_header_compiler=no
+fi
+
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+{ echo "$as_me:$LINENO: result: $ac_header_compiler" >&5
+echo "${ECHO_T}$ac_header_compiler" >&6; }
+
+# Is the header present?
+{ echo "$as_me:$LINENO: checking stp/c_interface.h presence" >&5
+echo $ECHO_N "checking stp/c_interface.h presence... $ECHO_C" >&6; }
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h. */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* end confdefs.h. */
+#include
+_ACEOF
+if { (ac_try="$ac_cpp conftest.$ac_ext"
+case "(($ac_try" in
+ *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+ *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+ (eval "$ac_cpp conftest.$ac_ext") 2>conftest.er1
+ ac_status=$?
+ grep -v '^ *+' conftest.er1 >conftest.err
+ rm -f conftest.er1
+ cat conftest.err >&5
+ echo "$as_me:$LINENO: \$? = $ac_status" >&5
+ (exit $ac_status); } >/dev/null; then
+ if test -s conftest.err; then
+ ac_cpp_err=$ac_cxx_preproc_warn_flag
+ ac_cpp_err=$ac_cpp_err$ac_cxx_werror_flag
+ else
+ ac_cpp_err=
+ fi
+else
+ ac_cpp_err=yes
+fi
+if test -z "$ac_cpp_err"; then
+ ac_header_preproc=yes
+else
+ echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+ ac_header_preproc=no
+fi
+
+rm -f conftest.err conftest.$ac_ext
+{ echo "$as_me:$LINENO: result: $ac_header_preproc" >&5
+echo "${ECHO_T}$ac_header_preproc" >&6; }
+
+# So? What about this header?
+case $ac_header_compiler:$ac_header_preproc:$ac_cxx_preproc_warn_flag in
+ yes:no: )
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: accepted by the compiler, rejected by the preprocessor!" >&5
+echo "$as_me: WARNING: stp/c_interface.h: accepted by the compiler, rejected by the preprocessor!" >&2;}
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: proceeding with the compiler's result" >&5
+echo "$as_me: WARNING: stp/c_interface.h: proceeding with the compiler's result" >&2;}
+ ac_header_preproc=yes
+ ;;
+ no:yes:* )
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: present but cannot be compiled" >&5
+echo "$as_me: WARNING: stp/c_interface.h: present but cannot be compiled" >&2;}
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: check for missing prerequisite headers?" >&5
+echo "$as_me: WARNING: stp/c_interface.h: check for missing prerequisite headers?" >&2;}
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: see the Autoconf documentation" >&5
+echo "$as_me: WARNING: stp/c_interface.h: see the Autoconf documentation" >&2;}
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: section \"Present But Cannot Be Compiled\"" >&5
+echo "$as_me: WARNING: stp/c_interface.h: section \"Present But Cannot Be Compiled\"" >&2;}
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: proceeding with the preprocessor's result" >&5
+echo "$as_me: WARNING: stp/c_interface.h: proceeding with the preprocessor's result" >&2;}
+ { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: in the future, the compiler will take precedence" >&5
+echo "$as_me: WARNING: stp/c_interface.h: in the future, the compiler will take precedence" >&2;}
+ ( cat <<\_ASBOX
+## ------------------------------------- ##
+## Report this to daniel@minormatter.com ##
+## ------------------------------------- ##
+_ASBOX
+ ) | sed "s/^/$as_me: WARNING: /" >&2
+ ;;
+esac
+{ echo "$as_me:$LINENO: checking for stp/c_interface.h" >&5
+echo $ECHO_N "checking for stp/c_interface.h... $ECHO_C" >&6; }
+if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+ echo $ECHO_N "(cached) $ECHO_C" >&6
+else
+ ac_cv_header_stp_c_interface_h=$ac_header_preproc
+fi
+{ echo "$as_me:$LINENO: result: $ac_cv_header_stp_c_interface_h" >&5
+echo "${ECHO_T}$ac_cv_header_stp_c_interface_h" >&6; }
+
+fi
+if test $ac_cv_header_stp_c_interface_h = yes; then
+ :
+else
+
+ { { echo "$as_me:$LINENO: error: Unable to use stp/c_interface.h header" >&5
+echo "$as_me: error: Unable to use stp/c_interface.h header" >&2;}
+ { (exit 1); exit 1; }; }
+
+fi
+
+
+ CPPFLAGS="$old_CPPFLAGS"
+
+
+{ echo "$as_me:$LINENO: checking for vc_setInterfaceFlags in -lstp" >&5
+echo $ECHO_N "checking for vc_setInterfaceFlags in -lstp... $ECHO_C" >&6; }
+if test "${ac_cv_lib_stp_vc_setInterfaceFlags+set}" = set; then
+ echo $ECHO_N "(cached) $ECHO_C" >&6
+else
+ ac_check_lib_save_LIBS=$LIBS
+LIBS="-lstp -L$stp_root/lib $LIBS"
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h. */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* 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
+rm -f conftest.$ac_objext conftest$ac_exeext
+if { (ac_try="$ac_link"
+case "(($ac_try" in
+ *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+ *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+ (eval "$ac_link") 2>conftest.er1
+ ac_status=$?
+ grep -v '^ *+' conftest.er1 >conftest.err
+ rm -f conftest.er1
+ cat conftest.err >&5
+ echo "$as_me:$LINENO: \$? = $ac_status" >&5
+ (exit $ac_status); } &&
+ { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err'
+ { (case "(($ac_try" in
+ *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+ *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+ (eval "$ac_try") 2>&5
+ ac_status=$?
+ echo "$as_me:$LINENO: \$? = $ac_status" >&5
+ (exit $ac_status); }; } &&
+ { ac_try='test -s conftest$ac_exeext'
+ { (case "(($ac_try" in
+ *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+ *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+ (eval "$ac_try") 2>&5
+ ac_status=$?
+ echo "$as_me:$LINENO: \$? = $ac_status" >&5
+ (exit $ac_status); }; }; then
+ ac_cv_lib_stp_vc_setInterfaceFlags=yes
+else
+ echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+ 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
+{ echo "$as_me:$LINENO: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
+echo "${ECHO_T}$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
+if test $ac_cv_lib_stp_vc_setInterfaceFlags = yes; then
+ cat >>confdefs.h <<_ACEOF
+#define HAVE_LIBSTP 1
+_ACEOF
+
+ LIBS="-lstp $LIBS"
+
+else
+
+ { { echo "$as_me:$LINENO: error: Unable to link with libstp" >&5
+echo "$as_me: error: Unable to link with libstp" >&2;}
+ { (exit 1); exit 1; }; }
+
+fi
+
+
+
+cat >>confdefs.h <<\_ACEOF
+#define HAVE_EXT_STP 1
+_ACEOF
+
+ ENABLE_EXT_STP=1
+
+ STP_ROOT=$stp_root
+
+fi
+
+
ac_config_commands="$ac_config_commands Makefile"
@@ -5676,11 +5966,13 @@ CXX!$CXX$ac_delim
CXXFLAGS!$CXXFLAGS$ac_delim
ac_ct_CXX!$ac_ct_CXX$ac_delim
CXXCPP!$CXXCPP$ac_delim
+ENABLE_EXT_STP!$ENABLE_EXT_STP$ac_delim
+STP_ROOT!$STP_ROOT$ac_delim
LIBOBJS!$LIBOBJS$ac_delim
LTLIBOBJS!$LTLIBOBJS$ac_delim
_ACEOF
- if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 76; then
+ if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 78; then
break
elif $ac_last_try; then
{ { echo "$as_me:$LINENO: error: could not make $CONFIG_STATUS" >&5
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 88f92d96..653b27a4 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -3,9 +3,15 @@
/* 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 header file. */
#undef HAVE_INTTYPES_H
+/* Define to 1 if you have the `stp' library (-lstp). */
+#undef HAVE_LIBSTP
+
/* Define to 1 if you have the header file. */
#undef HAVE_MEMORY_H
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 30713253..4353857c 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -17,7 +17,11 @@
#include
+Building KLEE with a more recent version of STP
+
+If your benchmarks are running slowly or not terminating it may
+be worth trying a more recent version of KLEE's constraint solver
+STP,
+which offers performance improvements over the version supplied
+with KLEE.
+
+STP does not make frequent releases, and its Subversion repository
+is under constant development and may be unstable. The instructions
+below are for a particular revision which is known to pass the KLEE
+test suite, but you can try a more recent revision (at your own risk)
+by changing or removing the -r argument to the svn
+co command.
+
+
+ - Download and build STP.
+
+ $ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp
+ $ cd stp
+ $ scripts/configure --with-prefix=path/to/stp/inst --with-cryptominisat2
+ $ make OPTIMIZE=-O2 CFLAGS_M32= install
+
+
+
+ - Configure KLEE:
+
+ $ ./configure --with-llvm=path/to/llvm --with-stp=path/to/stp/inst
+
+
+
+ - Rebuild KLEE.
+
+