From a008fb78987a4675d12f5934f3d51bbd84c3f653 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Mon, 5 Apr 2010 04:02:31 +0000 Subject: 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 --- Makefile.common | 3 ++ autoconf/configure.ac | 1 - configure | 2 -- lib/Solver/STPBuilder.h | 2 +- stp/AST/Makefile | 70 ++++++++++--------------------------------- stp/Makefile | 77 +++++++----------------------------------------- stp/Makefile.common.in | 16 ---------- stp/bitvec/Makefile | 21 ++++++++----- stp/c_interface/Makefile | 23 ++++++++------- stp/constantbv/Makefile | 23 ++++++++------- stp/sat/Makefile | 26 ++++++++-------- stp/simplifier/Makefile | 21 ++++++++----- tools/kleaver/Makefile | 7 +++-- tools/klee/Makefile | 12 +++----- 14 files changed, 104 insertions(+), 200 deletions(-) delete mode 100644 stp/Makefile.common.in 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 #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 -- cgit 1.4.1