diff options
| -rw-r--r-- | .travis.yml | 40 | ||||
| -rwxr-xr-x | .travis/klee.sh | 28 | ||||
| -rwxr-xr-x | .travis/solvers.sh | 27 | ||||
| -rw-r--r-- | Dockerfile | 10 |
4 files changed, 83 insertions, 22 deletions
diff --git a/.travis.yml b/.travis.yml index 07ef8a01..9a17f968 100644 --- a/.travis.yml +++ b/.travis.yml @@ -19,30 +19,35 @@ env: # Check the matrix of: # LLVM : {2.9, 3.4} - # STP : {2.1.0, master} + # SOLVERS : {Z3, STP, STP:Z3} + # STP_VERSION : {2.1.0, master} # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # with Asserts enabled. # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set - # FIXME: Enable when we want to test LLVM3.5 matrix: - #- LLVM_VERSION=3.5 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 + # Test experimental Z3 support + - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + # FIXME: Enable when we want to test LLVM3.5 + #- LLVM_VERSION=3.5 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 #- LLVM_VERSION=3.5 STP_VERSION=master KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1 - - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=3.4 STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=3.4 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1 + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + # Check at least one build with Asserts disabled. - - LLVM_VERSION=2.9 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 # Check at least one Debug+Asserts build - - LLVM_VERSION=3.4 STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 global: - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I= - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw= @@ -58,11 +63,13 @@ before_install: - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list' - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' + - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list" # Needed for CMake - sudo add-apt-repository -y ppa:ubuntu-sdk-team/ppa # Needed for new libstdc++ and gcc4.8 - sudo add-apt-repository --yes ppa:ubuntu-toolchain-r/test/ - wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add - + - wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_12.04/Release.key | sudo apt-key add - - sudo apt-get update ########################################################################### # Set up out of source build directory @@ -87,11 +94,8 @@ before_install: - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh # Install lit (llvm-lit is not available) - sudo pip install lit - # Build STP - - mkdir stp - - cd stp - - ${KLEE_SRC}/.travis/stp.sh - - cd ../ + # Get SMT solvers + - ${KLEE_SRC}/.travis/solvers.sh script: # Get needed utlities/libraries for testing KLEE - mkdir test-utils/ diff --git a/.travis/klee.sh b/.travis/klee.sh index fbce61e7..0f855b46 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -1,6 +1,7 @@ #!/bin/bash -x # Make sure we exit if there is a failure 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')" @@ -43,6 +44,30 @@ COVERAGE_FLAGS="" if [ ${COVERAGE} -eq 1 ]; then COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage' fi + + +############################################################################### +# Handle setting up solver configure flags for KLEE +############################################################################### +KLEE_Z3_CONFIGURE_OPTION="" +KLEE_STP_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" + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac +done ############################################################################### # KLEE ############################################################################### @@ -57,7 +82,8 @@ ${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} \ - --with-stp="${BUILD_DIR}/stp/build" \ + ${KLEE_STP_CONFIGURE_OPTION} \ + ${KLEE_Z3_CONFIGURE_OPTION} \ ${KLEE_UCLIBC_CONFIGURE_OPTION} \ CXXFLAGS="${COVERAGE_FLAGS}" \ && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ diff --git a/.travis/solvers.sh b/.travis/solvers.sh new file mode 100755 index 00000000..db717f2d --- /dev/null +++ b/.travis/solvers.sh @@ -0,0 +1,27 @@ +#!/bin/bash -x +# Make sure we exit if there is a failure +set -e +: ${SOLVERS?"Solvers must be specified"} + +SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') + +for solver in ${SOLVER_LIST}; do + echo "Getting solver ${solver}" + case ${solver} in + STP) + echo "STP" + mkdir stp + cd stp + ${KLEE_SRC}/.travis/stp.sh + cd ../ + ;; + Z3) + echo "Z3" + # Should we install libz3-dbg too? + sudo apt-get -y install libz3 libz3-dev + ;; + *) + echo "Unknown solver ${solver}" + exit 1 + esac +done diff --git a/Dockerfile b/Dockerfile index a61f8353..aa3ca6b6 100644 --- a/Dockerfile +++ b/Dockerfile @@ -6,6 +6,7 @@ MAINTAINER Dan Liew <daniel.liew@imperial.ac.uk> # the resulting image is unnecessarily large! ENV LLVM_VERSION=3.4 \ + SOLVERS=STP:Z3 \ STP_VERSION=master \ DISABLE_ASSERTIONS=0 \ ENABLE_OPTIMIZED=1 \ @@ -40,7 +41,10 @@ RUN apt-get update && \ unzip \ binutils && \ pip3 install -U lit tabulate && \ - update-alternatives --install /usr/bin/python python /usr/bin/python3 50 + update-alternatives --install /usr/bin/python python /usr/bin/python3 50 && \ + ( wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key | apt-key add - ) && \ + echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /' >> /etc/apt/sources.list.d/z3.list && \ + apt-get update # Create ``klee`` user for container with password ``klee``. # and give it password-less sudo access (temporarily so we can use the TravisCI scripts) @@ -79,8 +83,8 @@ RUN sudo chown --recursive klee: ${KLEE_SRC} # Create build directory RUN mkdir -p ${BUILD_DIR} -# Build STP (use TravisCI script) -RUN cd ${BUILD_DIR} && mkdir stp && cd stp && ${KLEE_SRC}/.travis/stp.sh +# Build/Install SMT solvers (use TravisCI script) +RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/solvers.sh # Install testing utils (use TravisCI script) RUN cd ${BUILD_DIR} && mkdir testing-utils && cd testing-utils && \ |