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

8 files changed, 92 insertions, 185 deletions

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