diff options
Diffstat (limited to '.travis')
| -rwxr-xr-x | .travis/klee.sh | 202 | ||||
| -rwxr-xr-x | .travis/testing-utils.sh | 8 |
2 files changed, 147 insertions, 63 deletions
diff --git a/.travis/klee.sh b/.travis/klee.sh index 98dbbc0d..64bfcb67 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -34,10 +34,18 @@ if [ "${KLEE_UCLIBC}" != "0" ]; then cd klee-uclibc ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION} make - KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime" + if [ "X${USE_CMAKE}" == "X1" ]; then + KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE" + else + KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime" + fi cd ../ else - KLEE_UCLIBC_CONFIGURE_OPTION="" + if [ "X${USE_CMAKE}" == "X1" ]; then + KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE" + else + KLEE_UCLIBC_CONFIGURE_OPTION="" + fi fi COVERAGE_FLAGS="" @@ -54,52 +62,110 @@ KLEE_STP_CONFIGURE_OPTION="" KLEE_METASMT_CONFIGURE_OPTION="" SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') -for solver in ${SOLVER_LIST}; do - echo "Setting configuration option for ${solver}" - case ${solver} in - STP) - KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build" - ;; - Z3) - echo "Z3" - KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr" - ;; - metaSMT) - echo "metaSMT" - KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}" - ;; - *) - echo "Unknown solver ${solver}" - exit 1 - esac -done - +if [ "X${USE_CMAKE}" == "X1" ]; then + # Set CMake configure options + for solver in ${SOLVER_LIST}; do + echo "Setting CMake configuration option for ${solver}" + case ${solver} in + STP) + KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build" + ;; + Z3) + echo "Z3" + KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE" + ;; + metaSMT) + echo "metaSMT" + if [ "X${METASMT_DEFAULT}" == "X" ]; then + METASMT_DEFAULT=STP + fi + KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}" + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac + done + TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE") +else + for solver in ${SOLVER_LIST}; do + echo "Setting configuration option for ${solver}" + case ${solver} in + STP) + KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build" + ;; + Z3) + echo "Z3" + KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr" + ;; + metaSMT) + echo "metaSMT" + KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}" + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac + done + + TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc") +fi -TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc") ############################################################################### # KLEE ############################################################################### mkdir klee cd klee -# Build KLEE -# Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged -# and is missing the shared library that was supposed to be built that the build -# system will try to use by default. -${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ - --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \ - --with-llvmcc=${KLEE_CC} \ - --with-llvmcxx=${KLEE_CXX} \ - ${KLEE_STP_CONFIGURE_OPTION} \ - ${KLEE_Z3_CONFIGURE_OPTION} \ - ${KLEE_METASMT_CONFIGURE_OPTION} \ - ${KLEE_UCLIBC_CONFIGURE_OPTION} \ - ${TCMALLOC_OPTION} \ - CXXFLAGS="${COVERAGE_FLAGS}" \ - && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 - +if [ "X${USE_CMAKE}" == "X1" ]; then + GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/" + if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then + KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE" + else + KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE" + fi + + if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then + CMAKE_BUILD_TYPE="RelWithDebInfo" + else + CMAKE_BUILD_TYPE="Debug" + fi + # Compute CMake build type + CXXFLAGS="${COVERAGE_FLAGS}" \ + cmake \ + -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \ + -DLLVMCC="${KLEE_CC}" \ + -DLLVMCXX="${KLEE_CXX}" \ + ${KLEE_STP_CONFIGURE_OPTION} \ + ${KLEE_Z3_CONFIGURE_OPTION} \ + ${KLEE_METASMT_CONFIGURE_OPTION} \ + ${KLEE_UCLIBC_CONFIGURE_OPTION} \ + ${TCMALLOC_OPTION} \ + -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \ + -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \ + ${KLEE_ASSERTS_OPTION} \ + -DENABLE_TESTS=TRUE \ + -DLIT_ARGS="-v" \ + ${KLEE_SRC} && make +else + # Build KLEE + # Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged + # and is missing the shared library that was supposed to be built that the build + # system will try to use by default. + ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ + --with-llvmobj=/usr/lib/llvm-${LLVM_VERSION}/build \ + --with-llvmcc=${KLEE_CC} \ + --with-llvmcxx=${KLEE_CXX} \ + ${KLEE_STP_CONFIGURE_OPTION} \ + ${KLEE_Z3_CONFIGURE_OPTION} \ + ${KLEE_METASMT_CONFIGURE_OPTION} \ + ${KLEE_UCLIBC_CONFIGURE_OPTION} \ + ${TCMALLOC_OPTION} \ + CXXFLAGS="${COVERAGE_FLAGS}" \ + && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 +fi ############################################################################### # Testing ############################################################################### @@ -108,32 +174,42 @@ set +e # We want to let all the tests run before we exit ############################################################################### # Unit tests ############################################################################### -# The unittests makefile doesn't seem to have been packaged so get it from SVN -sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ -svn export http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \ - ../Makefile.unittest -sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ - -make unittests \ - DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 -RETURN="$?" +if [ "X${USE_CMAKE}" == "X1" ]; then + make unittests + RETURN="$?" +else + # The unittests makefile doesn't seem to have been packaged so get it from SVN + sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ + svn export http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \ + ../Makefile.unittest + sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/ + + make unittests \ + DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 + RETURN="$?" +fi ############################################################################### # lit tests ############################################################################### -# Note can't use ``make check`` because llvm-lit is not available -cd test -# The build system needs to generate this file before we can run lit -make lit.site.cfg \ - DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 - -set +e # We want to let all the tests run before we exit -lit -v . -RETURN="${RETURN}$?" +if [ "X${USE_CMAKE}" == "X1" ]; then + make integrationtests + RETURN="${RETURN}$?" +else + # Note can't use ``make check`` because llvm-lit is not available + cd test + # The build system needs to generate this file before we can run lit + make lit.site.cfg \ + DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ + ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ + ENABLE_SHARED=0 + + set +e # We want to let all the tests run before we exit + lit -v . + RETURN="${RETURN}$?" +fi #generate and upload coverage if COVERAGE is set if [ ${COVERAGE} -eq 1 ]; then diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh index b2f608db..3d52457f 100755 --- a/.travis/testing-utils.sh +++ b/.travis/testing-utils.sh @@ -2,6 +2,14 @@ # Make sure we exit if there is a failure set -e +if [ "X${USE_CMAKE}" == "X1" ]; then + # The New CMake build system just needs the GTest sources regardless + # of LLVM version. + wget https://github.com/google/googletest/archive/release-1.7.0.zip + unzip release-1.7.0.zip + exit 0 +fi + if [ "${LLVM_VERSION}" != "2.9" ]; then # Using LLVM3.4 all we need is vanilla GoogleTest :) wget https://github.com/google/googletest/archive/release-1.7.0.zip |