diff options
Diffstat (limited to '.travis/klee.sh')
| -rwxr-xr-x | .travis/klee.sh | 209 |
1 files changed, 65 insertions, 144 deletions
diff --git a/.travis/klee.sh b/.travis/klee.sh index 119fbb47..33299780 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -3,9 +3,6 @@ set -e : ${SOLVERS?"Solvers must be specified"} -# Calculate LLVM branch name to retrieve missing files from -SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')" - ############################################################################### # Select the compiler to use to generate LLVM bitcode ############################################################################### @@ -28,18 +25,10 @@ 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 - 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 + KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE" cd ../ else - if [ "X${USE_CMAKE}" == "X1" ]; then - KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE" - else - KLEE_UCLIBC_CONFIGURE_OPTION="" - fi + KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE" fi COVERAGE_FLAGS="" @@ -53,60 +42,37 @@ fi ############################################################################### SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') -if [ "X${USE_CMAKE}" == "X1" ]; then - # Set CMake configure options - KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF" - KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF" - KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF" - 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 - KLEE_Z3_CONFIGURE_OPTION="" - KLEE_STP_CONFIGURE_OPTION="" - KLEE_METASMT_CONFIGURE_OPTION="" - 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 +# Set CMake configure options +KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF" +KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF" +KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF" +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 "--with-tcmalloc" || echo "--without-tcmalloc") -fi +############################################################################### +# Handle additional configure flags +############################################################################### +TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE") ############################################################################### # Handle Sanitizer flags @@ -133,95 +99,50 @@ fi mkdir klee cd klee -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 +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} ${SANITIZER_CXX_FLAGS}" \ - CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ - cmake \ - -DLLVM_CONFIG_BINARY="${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_UNIT_TESTS=TRUE \ - -DENABLE_SYSTEM_TESTS=TRUE \ - -DLIT_ARGS="-v" \ - ${KLEE_SRC} - make +if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then + CMAKE_BUILD_TYPE="RelWithDebInfo" 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=${LLVM_BUILD_DIR} \ - --with-llvmobj=${LLVM_BUILD_DIR} \ - --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} ${SANITIZER_CXX_FLAGS}" \ - CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ - LDFLAGS="${SANITIZER_LD_FLAGS}" - make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ - ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ - ENABLE_SHARED=0 + CMAKE_BUILD_TYPE="Debug" fi +# TODO: We should support Ninja too +# Configure KLEE +CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \ +CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ +cmake \ + -DLLVM_CONFIG_BINARY="${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_UNIT_TESTS=TRUE \ + -DENABLE_SYSTEM_TESTS=TRUE \ + -DLIT_ARGS="-v" \ + ${KLEE_SRC} +make + ############################################################################### # Unit tests ############################################################################### -if [ "X${USE_CMAKE}" == "X1" ]; then - make unittests -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 -fi +make unittests ############################################################################### # lit tests ############################################################################### -if [ "X${USE_CMAKE}" == "X1" ]; then - make systemtests -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 - cd ../ - lit -v test/ -fi +make systemtests # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends if [ "X${SOLVERS}" == "XmetaSMT" ]; then |