This patch modifies KLEE to use an external version of STP as specified
by the --with-stp configure option. It includes documentation
referring users to the STP download location.
Apart from applying this patch, these two things also need to be done.
I did not include them in this patch for space reasons.
- delete the entire contents of the stp directory
- rerun the autotools using the autoconf/AutoRegen.sh script
---
Makefile | 4 ++--
Makefile.common | 7 ++-----
Makefile.config.in | 2 ++
autoconf/configure.ac | 22 +++++++++++++++++++++-
lib/Solver/STPBuilder.h | 2 +-
lib/Solver/Solver.cpp | 1 +
tools/kleaver/Makefile | 7 +++----
tools/klee/Makefile | 8 ++++----
www/GetStarted.html | 13 +++++++++++--
9 files changed, 47 insertions(+), 19 deletions(-)
diff --git a/Makefile b/Makefile
index 2c3ab72..ced91c8 100644
--- a/Makefile
+++ b/Makefile
@@ -12,7 +12,7 @@
#
LEVEL = .
-DIRS = stp lib tools runtime
+DIRS = lib tools runtime
EXTRA_DIST = include
# Only build support directories when building unittests.
@@ -33,7 +33,7 @@ doxygen:
.PHONY: cscope.files
cscope.files:
find \
- lib include stp tools runtime examples unittests test \
+ lib include tools runtime examples unittests test \
-name Makefile -or \
-name \*.in -or \
-name \*.c -or \
diff --git a/Makefile.common b/Makefile.common
index f3a8f8b..5694fd6 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -26,9 +26,6 @@ LLVMCC := $(LLVMGCC)
LLVMCXX := $(LLVMGXX)
endif
-LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
-CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
+LD.Flags += -L$(STP_ROOT)/lib
+CXX.Flags += -I$(STP_ROOT)/include
CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\"
-
-# For STP.
-CXX.Flags += -DEXT_HASH_MAP
diff --git a/Makefile.config.in b/Makefile.config.in
index 0b85883..8296e38 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -20,6 +20,8 @@ PROJ_OBJ_ROOT := $(subst //,/, at abs_top_objdir@)
# Set the root directory of this project's install prefix
PROJ_INSTALL_ROOT := @prefix@
+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 4266ac4..6256181 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -238,6 +238,27 @@ fi
AC_DEFINE_UNQUOTED(RUNTIME_CONFIGURATION, "$with_runtime", [Configuration for
runtime libraries])
AC_SUBST(RUNTIME_CONFIGURATION)
+AC_ARG_WITH(stp,
+ AS_HELP_STRING([--with-stp],
+ [Location of STP installation directory]),,[
+ AC_MSG_ERROR([--with-stp option required])
+])
+
+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_setFlags,, [
+ AC_MSG_ERROR([Unable to link with libstp])
+], -L$stp_root/lib)
+
+AC_SUBST(STP_ROOT,$stp_root)
+
dnl **************************************************************************
dnl See if we should support __ctype_b_loc externals.
@@ -271,7 +292,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/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 3071325..6382bc1 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -17,7 +17,7 @@
#include <map>
#define Expr VCExpr
-#include "../../stp/c_interface/c_interface.h"
+#include "stp/c_interface.h"
#if ENABLE_STPLOG == 1
#include "stp/stplog.h"
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 5dd2427..176da3b 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -453,6 +453,7 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool
_useForkedSTP)
assert(vc && "unable to create validity checker");
assert(builder && "unable to create STPBuilder");
+ vc_setInterfaceFlags(vc, EXPRDELETE, 0);
vc_registerErrorHandler(::stp_error_handler);
if (useForkedSTP) {
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index d9c417c..0bb184b 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -9,12 +9,11 @@
LEVEL=../..
TOOLNAME = kleaver
-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 \
- $(STP_LIBS)
+USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
LINK_COMPONENTS = support
include $(LEVEL)/Makefile.common
+
+LIBS += -lstp
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index 72188b7..6a24bc1 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -9,10 +9,10 @@
LEVEL=../..
TOOLNAME = klee
-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 \
- $(STP_LIBS)
+USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a
kleeBasic.a
LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
include $(LEVEL)/Makefile.common
+
+LIBS += -lstp
+#-ltcmalloc
diff --git a/www/GetStarted.html b/www/GetStarted.html
index 9e03e1d..669d77d 100644
--- a/www/GetStarted.html
+++ b/www/GetStarted.html
@@ -58,6 +58,15 @@ targets.<p>
KLEE runs very slowly in Debug mode).
</li>
+ <li><a href="http://sites.google.com/site/stpfastprover/";>Download and build
+ the STP constraint solver</a>.
+ <div class="instr">
+ $ svn co
https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp
stp <br>
+ $ cd stp <br>
+ $ ./clean-install.sh --with-prefix=<i>path/to/stp/inst</i>
+ </div>
+ </li>
+
<li>Checkout KLEE (to any path you like):
<div class="instr">
$ svn co http://llvm.org/svn/llvm-project/klee/trunk klee
@@ -66,13 +75,13 @@ targets.<p>
<li>Configure KLEE (from the KLEE source directory):
<div class="instr">
- $ ./configure --with-llvm=<i>path/to/llvm</i>
+ $ ./configure --with-llvm=<i>path/to/llvm</i>
--with-stp=<i>path/to/stp/inst</i>
</div>
<p>This assumes that you compiled LLVM in-place. If you used a
different directory for the object files then use:
<div class="instr">
- $ ./configure --with-llvmsrc=<i>path/to/llvm/src</i>
--with-llvmobj=<i>path/to/llvm/obj</i>
+ $ ./configure --with-llvmsrc=<i>path/to/llvm/src</i>
--with-llvmobj=<i>path/to/llvm/obj</i> --with-stp=<i>path/to/stp/inst</i>
</div>
</li>
--
1.6.5
--GvXjxJ+pjyke8COw--
