Merge pull request #461 from tautschnig/build-system

Support vpath builds and use them for coverage measurement

Author: Daniel Kroening

regression/get_coverage.sh

@@ -9,6 +9,7 @@ if [ $? -ne 0 ]; then
     printf "ERROR: Could not create output directoy"
     exit 1
 fi
+output_dir_abs=`cd $output_dir > /dev/null ; pwd`
 
 # Check that the previous command succeded, if not exit.
 command_status()
@@ -49,18 +50,21 @@ lcov -version > $output_dir/cbmc_coverage.out 2>&1
 command_status
 
 # Remove any previous build that may not have coverage in it.
-printf "INFO: Cleaning CBMC build "
-make clean -C ../src >> $output_dir/cbmc_coverage.out 2>&1
+printf "INFO: setting up vpath build "
+cd ../src
+../scripts/vpath-setup.sh coverage-build >> $output_dir_abs/cbmc_coverage.out 2>&1
 command_status
+cd ../regression
 
 printf "INFO: Building CBMC with Code Coverage enabled "
 # Run the usual make target with --coverage to add gcov instrumentation
-make CXXFLAGS="--coverage" LINKFLAGS="--coverage" -C ../src >> $output_dir/cbmc_coverage.out 2>&1
+make CXXFLAGS="--coverage" LINKFLAGS="--coverage" -C ../src/coverage-build/src \
+  >> $output_dir/cbmc_coverage.out 2>&1
 command_status
 
 printf "INFO: Running Regression tests "
 # Run regression tests which will collect the coverage metrics and put them in the src files
-make >> $output_dir/cbmc_coverage.out 2>&1
+make -C ../src/coverage-build/regression >> $output_dir/cbmc_coverage.out 2>&1
 printf "[DONE]\n"
 
 printf "INFO: Gathering coverage metrics "

scripts/vpath-setup.sh

@@ -0,0 +1,76 @@
+#!/bin/bash
+
+set -e
+
+if [ $# -ne 1 ]
+then
+  echo "Target directory required" 1>&2
+  exit 1
+fi
+
+if ! make -s generated_files
+then
+  echo "Failed to run 'make generated_files'" 1>&2
+  exit 1
+fi
+
+DEST=$1
+
+gen_makefile()
+{
+  local d=$1
+  local m=$2
+
+  mkdir -p $DEST/src/$d
+  cat > $DEST/src/$d/$m <<EOF
+VPATH =
+vpath %.cpp $PWD/$d
+vpath %.cc $PWD/$d
+vpath %.h $PWD/$d
+vpath %.y $PWD/$d
+vpath %.l $PWD/$d
+vpath %.txt $PWD/$d
+EOF
+  cat $d/$m >> $DEST/src/$d/$m
+}
+
+makefiles=$(find . -name Makefile | grep -v $DEST)
+
+for m in $makefiles
+do
+  dir=$(dirname $m)
+  gen_makefile $dir Makefile
+done
+
+gen_makefile big-int makefile
+
+cp common config.inc $DEST/src/
+
+# tweak include paths in config.inc
+perl -p -i -e 's/(= \.\.\/\.\.\/)/$1..\/..\//' $DEST/src/config.inc
+echo "INCLUDES += -I$PWD" >> $DEST/src/config.inc
+
+# tweak targets that aren't compatible with vpaths
+perl -p -i -e "s{(library/\\*.c)}{$PWD/ansi-c/\$1}" $DEST/src/ansi-c/Makefile
+perl -p -i -e 's/^(cprover_library.inc:)/%$1/' $DEST/src/ansi-c/Makefile
+perl -p -i -e 's/^(cprover_library.cpp:)/#$1/' $DEST/src/ansi-c/Makefile
+
+perl -p -i -e 's/^(irep_ids.cpp:)/#$1/' $DEST/src/util/Makefile
+
+# create sub-directories
+mkdir -p $DEST/src/ansi-c/library $DEST/src/ansi-c/literals
+mkdir -p $DEST/src/goto-instrument/{accelerate,wmm}
+mkdir -p $DEST/src/solvers/{cvc,flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt1,smt2}
+
+# copy generated files for coverage reports
+for f in \
+  ansi-c/ansi_c_lex.yy.cpp ansi-c/scanner.l ansi-c/ansi_c_y.tab.cpp \
+  assembler/scanner.l assembler/assembler_lex.yy.cpp \
+  jsil/jsil_lex.yy.cpp jsil/scanner.l jsil/jsil_y.tab.cpp \
+  json/parser.y json/json_lex.yy.cpp json/json_y.tab.cpp \
+  xmllang/scanner.l xmllang/xml_lex.yy.cpp xmllang/xml_y.tab.cpp xmllang/parser.y
+do
+  cp $f $DEST/src/$(dirname $f)/
+done
+
+cp -aL ../regression $DEST/

src/solvers/Makefile

@@ -120,7 +120,7 @@ SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \
       refinement/refine_arrays.cpp \
       miniBDD/miniBDD.cpp
 
-INCLUDES= -I .. \
+INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
   $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)

src/util/Makefile

@@ -37,11 +37,11 @@ all: util$(LIBEXT)
 
 ###############################################################################
 
-irep_ids.h: irep_ids_convert$(EXEEXT) irep_ids.txt
-	./irep_ids_convert$(EXEEXT) header < irep_ids.txt > $@
+irep_ids.h: irep_ids.txt irep_ids_convert$(EXEEXT)
+	./irep_ids_convert$(EXEEXT) header < $< > $@
 
-irep_ids.inc: irep_ids_convert$(EXEEXT) irep_ids.txt
-	./irep_ids_convert$(EXEEXT) table < irep_ids.txt > $@
+irep_ids.inc: irep_ids.txt irep_ids_convert$(EXEEXT)
+	./irep_ids_convert$(EXEEXT) table < $< > $@
 
 irep_ids.cpp: irep_ids.inc irep_ids.h