STP: Switch build to using LLVM style Makefiles.

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

14 files changed, 104 insertions, 200 deletions

diff --git a/Makefile.common b/Makefile.common
index 4cbe3302..c54f1142 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -29,3 +29,6 @@ endif
 LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
 CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_SRC_ROOT)\"
+
+# For STP.
+CXX.Flags += -DEXT_HASH_MAP
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index d1f5446e..ceeffe05 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -20,7 +20,6 @@ AC_CONFIG_SRCDIR(["Makefile.config.in"])
 
 dnl Configure a common Makefile
 AC_CONFIG_FILES(Makefile.config)
-AC_CONFIG_FILES(stp/Makefile.common)
 
 dnl Configure project makefiles
 dnl List every Makefile that exists within your source tree
diff --git a/configure b/configure
index 6207a85e..644ee3e9 100755
--- a/configure
+++ b/configure
@@ -1784,8 +1784,6 @@ fi
 
 ac_config_files="$ac_config_files Makefile.config"
 
-ac_config_files="$ac_config_files stp/Makefile.common"
-
 
 ac_config_headers="$ac_config_headers include/klee/Config/config.h"
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 6382bc1f..30713253 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -17,7 +17,7 @@
 #include <map>
 
 #define Expr VCExpr
-#include "stp/c_interface.h"
+#include "../../stp/c_interface/c_interface.h"
 
 #if ENABLE_STPLOG == 1
 #include "stp/stplog.h"
diff --git a/stp/AST/Makefile b/stp/AST/Makefile
index 0218510b..66a0472c 100644
--- a/stp/AST/Makefile
+++ b/stp/AST/Makefile
@@ -1,54 +1,16 @@
-include ../Makefile.common
-
-SRCS = AST.cpp ASTKind.cpp  ASTUtil.cpp BitBlast.cpp SimpBool.cpp  ToCNF.cpp ToSAT.cpp Transform.cpp
-OBJS = $(SRCS:.cpp=.o)
-
-#Make the ast library for use by other modules
-libast.a:	$(OBJS)
-	-rm -rf $@
-	$(AR) rc libast.a $(OBJS)
-	$(RANLIB) libast.a
-
-ASTKind.o: ASTKind.h ASTKind.cpp
-	$(CXX) $(CXXFLAGS)   -c -o ASTKind.o ASTKind.cpp
-
-# ASTKind.h and ASTKind.cpp are automatically generated
-ASTKind.h ASTKind.cpp:	ASTKind.kinds genkinds.pl
-	./genkinds.pl
-
-# cnftest:	cnftest.o ToCNF.o AST.o ASTUtil.o ASTKind.o BitBlast.o AST.h
-#	$(CC) $(LDFLAGS) ToCNF.o BitBlast.o ASTKind.o  ASTUtil.o AST.o  cnftest.o  -o cnftest 
-
-# bbtest: $(OBJS)
-#	$(CC) $(LDFLAGS) BitBlast.o ASTKind.o  ASTUtil.o AST.o  bbtest.o -o bbtest 
-
-# asttest: $(OBJS)
-#	$(CC) $(LDFLAGS) ASTKind.o  ASTUtil.o AST.o asttest.o  -lstdc++ -o asttest
-
-clean:
-	rm -rf *.o *~ bbtest asttest cnftest *.a  ASTKind.h ASTKind.cpp .#*
-
-depend:
-	makedepend -Y -- $(CFLAGS) -- $(SRCS)
-# DO NOT DELETE
-
-AST.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h
-AST.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h
-AST.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h
-ASTUtil.o: ASTUtil.h
-BitBlast.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h
-BitBlast.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h
-BitBlast.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h
-SimpBool.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h
-SimpBool.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h
-SimpBool.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h
-ToCNF.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h
-ToCNF.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h
-ToCNF.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h
-ToSAT.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h
-ToSAT.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h
-ToSAT.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h
-ToSAT.o: ../simplifier/bvsolver.h ../AST/AST.h
-Transform.o: AST.h ASTUtil.h ASTKind.h ../sat/Solver.h ../sat/SolverTypes.h
-Transform.o: ../sat/Global.h ../sat/VarOrder.h ../sat/Solver.h ../sat/Heap.h
-Transform.o: ../AST/ASTUtil.h ../sat/SolverTypes.h ../constantbv/constantbv.h
+#===-- stp/AST/Makefile ------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+LEVEL=../..
+
+LIBRARYNAME=stp_AST
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
+
+include $(LEVEL)/Makefile.common
diff --git a/stp/Makefile b/stp/Makefile
index 23cdcd1b..c863d5b4 100644
--- a/stp/Makefile
+++ b/stp/Makefile
@@ -1,69 +1,14 @@
- # STP (Simple Theorem Prover) top level makefile
- #
- # To make in debug mode, type 'make "CLFAGS=-ggdb"
- # To make in optimized mode, type 'make "CFLAGS=-O2" 
+#===-- stp/Makefile ----------------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
 
-include Makefile.common
+LEVEL=..
 
-USE_PARSER := 0
-
-LIBS := AST/libast.a sat/libsatsolver.a simplifier/libsimplifier.a bitvec/libconsteval.a constantbv/libconstantbv.a c_interface/libcinterface.a
-DIRS := AST sat simplifier bitvec c_interface constantbv
-
-ifeq ($(USE_PARSER), 1)
-DIRS += parser
-endif
-
-# NB: the TAGS target is a hack to get around this recursive make nonsense
-# we want all the source and header files generated before we make tags
-.PHONY: all
-all: lib/libstp.a include/stp/c_interface.h
-
-AST/libast.a:
-	@$(MAKE) -q -C `dirname $@` || $(MAKE) -C `dirname $@`
-sat/libsatsolver.a: AST/libast.a
-	@$(MAKE) -q -C `dirname $@` || $(MAKE) -C `dirname $@`
-simplifier/libsimplifier.a: AST/libast.a
-	@$(MAKE) -q -C `dirname $@` || $(MAKE) -C `dirname $@`
-bitvec/libconsteval.a: AST/libast.a
-	@$(MAKE) -q -C `dirname $@` || $(MAKE) -C `dirname $@`
-constantbv/libconstantbv.a: AST/libast.a
-	@$(MAKE) -q -C `dirname $@` || $(MAKE) -C `dirname $@`
-c_interface/libcinterface.a: AST/libast.a
-	@$(MAKE) -q -C `dirname $@` || $(MAKE) -C `dirname $@`
-parser/parser: $(LIBS)
-	@$(MAKE) -q -C `dirname $@` || $(MAKE) -C `dirname $@`
-
-lib/libstp.a: $(LIBS)
-	@mkdir -p lib
-	rm -f $@
-	@for dir in $(DIRS); do \
-		$(AR) rc $@ $$dir/*.o; \
-	done
-	$(RANLIB) $@
-
-bin/stp: parser/parser $(LIBS)
-	@mkdir -p bin
-	@cp parser/parser $@
-
-include/stp/c_interface.h: $(LIBS)
-	@mkdir -p include/stp
-	@cp c_interface/c_interface.h $@
-
-.PHONY: clean
-clean:
-	rm -rf *~
-	rm -rf *.a
-	rm -rf lib/*.a
-	rm -rf bin/*~
-	rm -rf bin/stp
-	rm -rf *.log
-	rm -f TAGS
-	$(MAKE) clean -C AST
-	$(MAKE) clean -C sat
-	$(MAKE) clean -C simplifier
-	$(MAKE) clean -C bitvec
-	$(MAKE) clean -C parser
-	$(MAKE) clean -C c_interface
-	$(MAKE) clean -C constantbv
+PARALLEL_DIRS := AST bitvec c_interface constantbv sat simplifier
 
+include $(LEVEL)/Makefile.common
diff --git a/stp/Makefile.common.in b/stp/Makefile.common.in
deleted file mode 100644
index a88e35ed..00000000
--- a/stp/Makefile.common.in
+++ /dev/null
@@ -1,16 +0,0 @@
-# -*- Makefile -*-
-
-CFLAGS := @CFLAGS@
-CXXFLAGS := @CXXFLAGS@ -O2
-LDFLAGS := @LDFLAGS@ -lstdc++
-
-# use the darmin test as a proxy for detecting Mac OS X
-ifneq ($(shell uname -s), Darwin)
-  CFLAGS += -static
-endif
-
-CXXFLAGS += -Wall -DEXT_HASH_MAP
-
-LEX := flex
-YACC := bison -d -y --debug -v
-RANLIB := ranlib
diff --git a/stp/bitvec/Makefile b/stp/bitvec/Makefile
index eb6e1121..959d33cc 100644
--- a/stp/bitvec/Makefile
+++ b/stp/bitvec/Makefile
@@ -1,11 +1,16 @@
-include ../Makefile.common
+#===-- stp/bitvec/Makefile ---------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
 
-SRCS = consteval.cpp
-OBJS = $(SRCS:.cpp=.o)
+LEVEL=../..
 
-libconsteval.a: $(OBJS)
-	$(AR) rc $@ $^
-	$(RANLIB) $@
+LIBRARYNAME=stp_bitvec
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
 
-clean:	
-	rm -rf *.o *~ *.a .#*
+include $(LEVEL)/Makefile.common
diff --git a/stp/c_interface/Makefile b/stp/c_interface/Makefile
index cf6b09d1..3082f715 100644
--- a/stp/c_interface/Makefile
+++ b/stp/c_interface/Makefile
@@ -1,13 +1,16 @@
-include ../Makefile.common
+#===-- stp/c_interface/Makefile ----------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
 
-SRCS = c_interface.cpp
-OBJS = $(SRCS:.cpp=.o)
+LEVEL=../..
 
-libcinterface.a: $(OBJS)
-	$(AR) rc $@ $^
-	$(RANLIB) $@
+LIBRARYNAME=stp_c_interface
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
 
-clean:	
-	rm -rf *.o *~ *.a .#*
-
-c_interface.o: c_interface.h
+include $(LEVEL)/Makefile.common
diff --git a/stp/constantbv/Makefile b/stp/constantbv/Makefile
index cd94ad94..ee8155cf 100644
--- a/stp/constantbv/Makefile
+++ b/stp/constantbv/Makefile
@@ -1,13 +1,16 @@
-include ../Makefile.common
+#===-- stp/constantbv/Makefile -----------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
 
-SRCS = constantbv.cpp
-OBJS = $(SRCS:.cpp=.o)
+LEVEL=../..
 
-libconstantbv.a: $(OBJS)
-	$(AR) rc $@ $^
-	$(RANLIB) $@
+LIBRARYNAME=stp_constantbv
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
 
-clean:	
-	rm -rf *.o *~ *.a .#*
-
-constantbv.o: constantbv.h
+include $(LEVEL)/Makefile.common
diff --git a/stp/sat/Makefile b/stp/sat/Makefile
index 8298e05a..074cb8af 100644
--- a/stp/sat/Makefile
+++ b/stp/sat/Makefile
@@ -1,16 +1,16 @@
-include ../Makefile.common
+#===-- stp/sat/Makefile -----------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
 
-SRCS = Solver.C Simplifier.C
-OBJS = $(SRCS:.C=.o)
+LEVEL=../..
 
-libsatsolver.a: $(OBJS)
-	$(AR) rc $@ $^
-	$(RANLIB) $@
+LIBRARYNAME=stp_sat
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
 
-Solver.o: Solver.C Solver.h Sort.h SolverTypes.h VarOrder.h Global.h Heap.h
-Simplifier.o: Simplifier.C Solver.h Sort.h SolverTypes.h VarOrder.h Global.h Heap.h
-
-clean:
-	rm -rf *.o *~  *.a  depend.mak .#*
-depend:
-	makedepend -- $(CFLAGS) -- $(SRCS)
+include $(LEVEL)/Makefile.common
diff --git a/stp/simplifier/Makefile b/stp/simplifier/Makefile
index aba07e1b..fb6be7e1 100644
--- a/stp/simplifier/Makefile
+++ b/stp/simplifier/Makefile
@@ -1,11 +1,16 @@
-include ../Makefile.common
+#===-- stp/simplifier/Makefile -----------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
 
-SRCS = simplifier.cpp bvsolver.cpp
-OBJS = $(SRCS:.cpp=.o)
+LEVEL=../..
 
-libsimplifier.a: $(OBJS)
-	$(AR) rc $@ $^
-	$(RANLIB) $@
+LIBRARYNAME=stp_simplifier
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
 
-clean:	
-	rm -rf *.o *~ *.a .#*
+include $(LEVEL)/Makefile.common
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 0bb184bb..d9c417c1 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -9,11 +9,12 @@
 
 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
+USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a \
+	$(STP_LIBS)
 LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
-
-LIBS += -lstp
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index fbdcfd85..72188b79 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -9,14 +9,10 @@
 
 LEVEL=../..
 TOOLNAME = klee
-USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
+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)
 LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
 
 include $(LEVEL)/Makefile.common
-
-ifeq ($(ENABLE_STPLOG), 1)
-	LIBS += -lstplog
-endif
-
-LIBS += -lstp 
-#-ltcmalloc