diff options
74 files changed, 1485 insertions, 544 deletions
diff --git a/.gitignore b/.gitignore index 60f71858..a3037485 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,9 @@ Debug/ Debug+Asserts/ Output/ +# commonly used as cmake build directory +/build + cscope.* *~ diff --git a/.travis.yml b/.travis.yml index a0b5e7ae..9a337952 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,10 +20,12 @@ env: ########################################################################### # Check a subset of the matrix of: - # LLVM : {2.9, 3.4} + # LLVM : {2.9, 3.4, 3.5, 3.6} # SOLVERS : {Z3, STP, STP:Z3, metaSMT} # STP_VERSION : {2.1.2, master} + # METASMT_VERSION : {v4.rc1} # METASMT_DEFAULT : {btor, stp, z3} + # METASMT_BOOST_VERSION : {x.y.z} // e.g. 1.60.0, libboost-dev will be used if unspecified # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # DISABLE_ASSERTIONS: {0, 1} # ENABLE_OPTIMIZED: {0, 1} @@ -34,22 +36,25 @@ env: # COVERAGE set indicated that coverage data should be uploaded to the server, only ONE job should have COVERAGE set matrix: - # FIXME: Enable when we want to test LLVM3.5 - #- LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - #- LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 USE_CMAKE=1 # TODO: Add coverage build # TODO: Add Doxygen build # Check KLEE CMake build in a few configurations + - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 - - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 - LLVM_VERSION=2.9 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1 # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_CMAKE=1 USE_TCMALLOC=0 ASAN_BUILD=1 - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_CMAKE=0 USE_TCMALLOC=0 ASAN_BUILD=1 + # legacy build system + - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 + # TODO: Port all configurations below to CMake build system # Test we can still build with Z3 in the old build sytem @@ -64,8 +69,8 @@ env: - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Test metaSMT support - - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 METASMT_BOOST_VERSION=1.60.0 # Check at least one build with Asserts disabled. - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 @@ -81,6 +86,12 @@ env: - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw= - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg= +matrix: + include: + - os: osx + osx_image: xcode8.2 + env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0 USE_CMAKE=1 + addons: apt: sources: @@ -92,6 +103,7 @@ addons: - gcc-4.8 - g++-4.8 - libcap-dev + - libedit-dev - libselinux1-dev - cmake @@ -102,7 +114,8 @@ before_install: # We assume the Travis image uses Ubuntu 14.04 LTS ########################################################################### # Update package information - - sudo apt-get update + - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then sudo apt-get update; fi + - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update && brew tap andreamattavelli/klee; fi ########################################################################### # Set up out of source build directory ########################################################################### diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh index 1068d158..8e8e9863 100755 --- a/.travis/install-llvm-and-runtime-compiler.sh +++ b/.travis/install-llvm-and-runtime-compiler.sh @@ -1,13 +1,14 @@ #!/bin/bash -x set -ev -sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev -if [ "${LLVM_VERSION}" != "2.9" ]; then + if [ "${LLVM_VERSION}" != "2.9" ]; then sudo apt-get install -y llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION} sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_VERSION} 20 sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_VERSION} 20 -else + else # Get llvm-gcc. We don't bother installing it wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 tar -xjf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 @@ -27,4 +28,16 @@ else export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu llvm-gcc/bin/llvm-gcc test.c -o hello_world ./hello_world + fi +elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + # NOTE: We should not easily generalize, since we need the corresponding support of bottled formulas + if [ "${LLVM_VERSION}" == "3.4" ]; then + brew install llvm34 + else + echo "Error: Requested to install LLVM ${LLVM_VERSION} on macOS, which is not supported" + exit 1 + fi +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 fi diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh index 5a86380b..0bc26616 100755 --- a/.travis/install-tcmalloc.sh +++ b/.travis/install-tcmalloc.sh @@ -1,12 +1,22 @@ #!/bin/bash -x set -ev -if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then - # Get tcmalloc release - wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz - tar xfz gperftools-2.4.tar.gz - cd gperftools-2.4 - ./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc --enable-minimal --prefix=/usr - make - sudo make install +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then + # Get tcmalloc release + wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz + tar xfz gperftools-2.4.tar.gz + cd gperftools-2.4 + ./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc --enable-minimal --prefix=/usr + make + sudo make install + fi +elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then + echo "Error: Requested to install TCMalloc on macOS, which is not supported" + exit 1 + fi +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 fi diff --git a/.travis/klee.sh b/.travis/klee.sh index 61806df3..5ee631fa 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -10,8 +10,16 @@ SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')" # Select the compiler to use to generate LLVM bitcode ############################################################################### if [ "${LLVM_VERSION}" != "2.9" ]; then + if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then KLEE_CC=/usr/bin/clang-${LLVM_VERSION} KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION} + elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + KLEE_CC=/usr/local/bin/clang-${LLVM_VERSION} + KLEE_CXX=/usr/local/bin/clang++-${LLVM_VERSION} + else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 + fi else # Just use pre-built llvm-gcc downloaded earlier KLEE_CC=${BUILD_DIR}/llvm-gcc/bin/llvm-gcc @@ -117,6 +125,20 @@ fi source ${KLEE_SRC}/.travis/sanitizer_flags.sh ############################################################################### +# Handling LLVM configuration +############################################################################### +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + LLVM_CONFIG="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" + LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION}/build" +elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}" + LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)" +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 +fi + +############################################################################### # KLEE ############################################################################### mkdir klee @@ -139,7 +161,7 @@ if [ "X${USE_CMAKE}" == "X1" ]; then CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \ CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \ cmake \ - -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \ + -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" \ -DLLVMCC="${KLEE_CC}" \ -DLLVMCXX="${KLEE_CXX}" \ ${KLEE_STP_CONFIGURE_OPTION} \ @@ -160,8 +182,8 @@ else # 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 \ + ${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} \ @@ -234,14 +256,14 @@ if [ ${COVERAGE} -eq 1 ]; then cd zcov #these files are not where zcov expects them to be after install so we move them - sudo cp js/sorttable.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sorttable.js - sudo cp js/sourceview.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sourceview.js + sudo cp js/sorttable.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sorttable.js + sudo cp js/sourceview.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sourceview.js sudo cp style.css /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/style.css #install zcov dependency sudo apt-get install -y enscript -#update gcov from v4.6 to v4.8. This is becauase gcda files are made for v4.8 and cause +#update gcov from v4.6 to v4.8. This is becauase gcda files are made for v4.8 and cause #a segmentation fault in v4.6 sudo apt-get install -y ggcov sudo rm /usr/bin/gcov diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh index 8e1cb341..f0748919 100755 --- a/.travis/metaSMT.sh +++ b/.travis/metaSMT.sh @@ -1,17 +1,28 @@ #!/bin/bash -x -# Get Boost, Z3, libgmp -sudo apt-get -y install libboost1.55-dev libz3 libz3-dev libgmp-dev +set -e + +: ${METASMT_VERSION?"METASMT_VERSION not specified"} + +# Get Z3, libgmp +sudo apt-get -y install libz3 libz3-dev libgmp-dev + +# Get Boost +if [ "X${METASMT_BOOST_VERSION}" != "X" ]; then + # Taken from boost/hana/.travis.yml + BOOST_URL="http://sourceforge.net/projects/boost/files/boost/${METASMT_BOOST_VERSION}/boost_${METASMT_BOOST_VERSION//\./_}.tar.gz" + BOOST_DIR=`pwd`/boost-${METASMT_BOOST_VERSION} + mkdir -p ${BOOST_DIR} + wget --quiet -O - ${BOOST_URL} | tar --strip-components=1 -xz -C ${BOOST_DIR} + sudo ln -s ${BOOST_DIR}/boost /usr/include/boost +else + sudo apt-get -y install libboost1.55-dev +fi # Clone -git clone git://github.com/hoangmle/metaSMT.git +git clone -b ${METASMT_VERSION} --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git cd metaSMT -## FIXME: define and use an environment variable METASMT_VERSION instead, when a proper version of metaSMT is available -git checkout 1f9e399 -git clone git://github.com/agra-uni-bremen/dependencies.git -cd dependencies -git checkout 45bc658 -cd .. +git submodule update --init source ${KLEE_SRC}/.travis/sanitizer_flags.sh if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then @@ -22,11 +33,11 @@ fi # Bootstrap export BOOST_ROOT=/usr sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack -./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr +./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off -DmetaSMT_REQUIRE_CXX11=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr sudo cp deps/boolector-2.2.0/lib/* /usr/lib/ # sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ # sudo cp deps/minisat-git/lib/* /usr/lib/ # hack -sudo cp deps/stp-git-basic/lib/* /usr/lib/ # +sudo cp -r deps/stp-git-basic/lib/lib* /usr/lib/ # # Build make -C build install diff --git a/.travis/solvers.sh b/.travis/solvers.sh index 04f3276f..b419d679 100755 --- a/.travis/solvers.sh +++ b/.travis/solvers.sh @@ -16,15 +16,8 @@ for solver in ${SOLVER_LIST}; do cd ../ ;; Z3) - # FIXME: Move this into its own script - source ${KLEE_SRC}/.travis/sanitizer_flags.sh - if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then - echo "Error: Requested Sanitized build but Z3 being used is not sanitized" - exit 1 - fi echo "Z3" - # Should we install libz3-dbg too? - sudo apt-get -y install libz3 libz3-dev + ${KLEE_SRC}/.travis/z3.sh ;; metaSMT) echo "metaSMT" diff --git a/.travis/stp.sh b/.travis/stp.sh index 4cc55c62..6df59ebe 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -1,46 +1,74 @@ #!/bin/bash -x +# TODO: For OSX we can prepare bottled formulas for STP and minisat + # Make sure we exit if there is a failure set -e STP_LOG="$(pwd)/stp-build.log" if [ "x${STP_VERSION}" != "x" ]; then - # Get Sanitizer flags - source ${KLEE_SRC}/.travis/sanitizer_flags.sh - - # Build minisat - git clone https://github.com/stp/minisat - cd minisat - mkdir build - cd build - MINISAT_DIR=`pwd` + # Get Sanitizer flags + source ${KLEE_SRC}/.travis/sanitizer_flags.sh + + # Build minisat + git clone https://github.com/stp/minisat + cd minisat + mkdir build + cd build + MINISAT_DIR=`pwd` + if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then CFLAGS="${SANITIZER_C_FLAGS}" \ CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ cmake -DCMAKE_INSTALL_PREFIX=/usr .. - make - sudo make install - cd ../../ - - # Build STP - git clone --depth 1 -b "${STP_VERSION}" git://github.com/stp/stp.git src - mkdir build - cd build - # Disabling building of shared libs is a workaround. - # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 + elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then CFLAGS="${SANITIZER_C_FLAGS}" \ CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ - cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF -DNO_BOOST:BOOL=ON ../src + cmake -DCMAKE_INSTALL_PREFIX=/usr/local .. + else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 + fi + make + sudo make install + cd ../../ - set +e # Do not exit if build fails because we need to display the log - make >> "${STP_LOG}" 2>&1 + # Determine STP build flags + if [ "X${STP_VERSION}" = "Xmaster" ]; then + # 7e0b096ee79d59bb5c344b7dd4d51b5b8d226221 s/NO_BOOST/ONLY_SIMPLE/ + # 5e9ca6339a2b3b000aa7a90c18601fdcf1212fe1 Silently BUILD_SHARED_LIBS removed. STATICCOMPILE does something similar + STP_CMAKE_FLAGS=( \ + "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \ + "-DONLY_SIMPLE:BOOL=ON" \ + "-DSTATICCOMPILE:BOOL=ON" \ + ) + else + STP_CMAKE_FLAGS=( \ + "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \ + "-DNO_BOOST:BOOL=ON" \ + "-DBUILD_SHARED_LIBS:BOOL=OFF" \ + ) + fi + + # Build STP + git clone --depth 1 -b "${STP_VERSION}" git://github.com/stp/stp.git src + mkdir build + cd build + # Disabling building of shared libs is a workaround. + # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8 + CFLAGS="${SANITIZER_C_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ + cmake "${STP_CMAKE_FLAGS[@]}" ../src + + set +e # Do not exit if build fails because we need to display the log + make >> "${STP_LOG}" 2>&1 else - echo "No STP_VERSION given or empty" - exit 1 + echo "No STP_VERSION given or empty" + exit 1 fi # Only show build output if something went wrong to keep log output short if [ $? -ne 0 ]; then - echo "Build error" - cat "${STP_LOG}" + echo "Build error" + cat "${STP_LOG}" fi diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh index 3d52457f..153a5546 100755 --- a/.travis/testing-utils.sh +++ b/.travis/testing-utils.sh @@ -18,11 +18,19 @@ if [ "${LLVM_VERSION}" != "2.9" ]; then cmake . make # Normally I wouldn't do something like this but hey we're running on a temporary virtual machine, so who cares? - sudo cp lib* /usr/lib/ - sudo cp -r include/gtest /usr/include + if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + sudo cp lib* /usr/lib/ + sudo cp -r include/gtest /usr/include + elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + sudo cp lib* /usr/local/lib/ + sudo cp -r include/gtest /usr/local/include + else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 + fi else # LLVM2.9 on the other hand is a pain - + # We need the version of GoogleTest used in LLVM2.9 # This is a hack old_dir=`pwd` @@ -45,4 +53,3 @@ else cd "${old_dir}" fi - diff --git a/.travis/z3.sh b/.travis/z3.sh new file mode 100755 index 00000000..a4c00f82 --- /dev/null +++ b/.travis/z3.sh @@ -0,0 +1,20 @@ +#!/bin/bash -x + +# Make sure we exit if there is a failure +set -e + +source ${KLEE_SRC}/.travis/sanitizer_flags.sh +if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then + echo "Error: Requested Sanitized build but Z3 being used is not sanitized" + exit 1 +fi + +if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then + # Should we install libz3-dbg too? + sudo apt-get -y install libz3 libz3-dev +elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then + brew install z3 +else + echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\"" + exit 1 +fi diff --git a/CMakeLists.txt b/CMakeLists.txt index 97c51a2e..6fc3878a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -64,6 +64,13 @@ else() set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "") endif() +if (("${CMAKE_VERSION}" VERSION_EQUAL "3.4") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.4")) + # In CMake >= 3.4 ExternalProject_Add_Step() supports a `USES_TERMINAL` argument + set(EXTERNAL_PROJECT_ADD_STEP_USES_TERMINAL_ARG "USES_TERMINAL" "1") +else() + set(EXTERNAL_PROJECT_ADD_STEP_USES_TERMINAL_ARG "") +endif() + ################################################################################ # Sanity check - Disallow building in source. # Otherwise we would overwrite the Makefiles of the old build system. @@ -387,10 +394,9 @@ endif() # RTTI ############################################################################### if (NOT LLVM_ENABLE_RTTI) - if (ENABLE_SOLVER_METASMT) - message(WARNING "Not disabling RTTI because metaSMT uses them") - # FIXME: Should this be FATAL_ERROR rather than ERROR? - message(WARNING + if (ENABLE_SOLVER_METASMT AND metaSMT_REQUIRE_RTTI) + message(FATAL_ERROR + "RTTI cannot be disabled because metaSMT uses them." "This build configuration is not supported and will likely not work." "You should recompile LLVM with RTTI enabled.") else() diff --git a/Dockerfile b/Dockerfile index d42b09c8..11174e6c 100644 --- a/Dockerfile +++ b/Dockerfile @@ -16,7 +16,8 @@ ENV LLVM_VERSION=3.4 \ BUILD_DIR=/home/klee/klee_build \ USE_CMAKE=1 \ ASAN_BUILD=0 \ - UBSAN_BUILD=0 + UBSAN_BUILD=0 \ + TRAVIS_OS_NAME=linux RUN apt-get update && \ apt-get -y --no-install-recommends install \ diff --git a/MetaSMT.mk b/MetaSMT.mk index 817fa663..32f60ac0 100644 --- a/MetaSMT.mk +++ b/MetaSMT.mk @@ -8,6 +8,8 @@ ifeq ($(ENABLE_METASMT),1) CXX.Flags += $(metaSMT_CXXFLAGS) CXX.Flags += $(metaSMT_INCLUDES) CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) - CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) + ifeq ($(metaSMT_REQUIRE_RTTI),true) + CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) + endif LIBS += $(metaSMT_LDLIBS) endif diff --git a/README-CMake.md b/README-CMake.md index c2893004..2d438546 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -7,6 +7,7 @@ its autoconf/Makefile based build system. * `check` - Build and run all tests. * `clean` - Clean the build tree. Note this won't clean the runtime build. +* `clean_runtime` - Clean the runtime build tree. * `docs` - Build documentation * `edit_cache` - Show cmake/ccmake/cmake-gui interface for chaning configure options. * `help` - Show list of top level targets diff --git a/cmake/find_llvm.cmake b/cmake/find_llvm.cmake index 0df6b4b5..770fca84 100644 --- a/cmake/find_llvm.cmake +++ b/cmake/find_llvm.cmake @@ -86,7 +86,7 @@ else() "${LLVM_PACKAGE_VERSION}") else() # try x.y pattern - set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)$") + set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)(svn)?$") if ("${LLVM_PACKAGE_VERSION}" MATCHES "${_llvm_version_regex}") string(REGEX REPLACE "${_llvm_version_regex}" diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index a0a02cb9..6751b31d 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -18,46 +18,17 @@ list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS # FIXME: We should test linking list(APPEND KLEE_SOLVER_LIBRARIES ${metaSMT_LIBRARIES}) -# THIS IS HORRIBLE. The ${metaSMT_CXXFLAGS} variable -# is badly formed. It is a string but we can't just split -# on spaces because its contents looks like this -# " -DmetaSMT_BOOLECTOR_1_API -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS". -# So handle defines specially -string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_broken_list) -list(LENGTH _metaSMT_CXXFLAGS_broken_list _metaSMT_CXXFLAGS_broken_list_length) -math(EXPR _metaSMT_CXXFLAGS_broken_list_last_index "${_metaSMT_CXXFLAGS_broken_list_length} -1") +# Separate flags and defines from ${metaSMT_CXXFLAGS} +string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_list) set(_metasmt_flags "") set(_metasmt_defines "") -set(_index_to_skip "") -foreach (index RANGE 0 ${_metaSMT_CXXFLAGS_broken_list_last_index}) - list(FIND _index_to_skip "${index}" _should_skip) - if ("${_should_skip}" EQUAL "-1") - list(GET _metaSMT_CXXFLAGS_broken_list ${index} _current_flag) - if ("${_current_flag}" MATCHES "^-D") - # This is a define - if ("${_current_flag}" MATCHES "^-D$") - # This is a bad define. We have just `-D` and the next item - # is the actually definition. - if ("${index}" EQUAL "${_metaSMT_CXXFLAGS_broken_list_last_index}") - message(FATAL_ERROR "Stray -D flag!") - else() - # Get next value - math(EXPR _next_index "${index} + 1") - list(GET _metaSMT_CXXFLAGS_broken_list ${_next_index} _next_flag) - if ("${_next_flag}" STREQUAL "") - message(FATAL_ERROR "Next flag shouldn't be empty!") - endif() - list(APPEND _metasmt_defines "-D${_next_flag}") - list(APPEND _index_to_skip "${_next_index}") - endif() - else() - # This is well formed defined (e.g. `-DHELLO`) - list(APPEND _metasmt_defines "${_current_flag}") - endif() - else() - # Regular flag - list(APPEND _metasmt_flags "${_current_flag}") - endif() +foreach (flag ${_metaSMT_CXXFLAGS_list}) + if ("${flag}" MATCHES "^-D") + # This is a define + list(APPEND _metasmt_defines "${flag}") + else() + # Regular flag + list(APPEND _metasmt_flags "${flag}") endif() endforeach() diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index cc186db7..6a72692d 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -29,6 +29,8 @@ extern llvm::cl::opt<bool> UseForkedCoreSolver; extern llvm::cl::opt<bool> CoreSolverOptimizeDivides; +extern llvm::cl::opt<bool> UseAssignmentValidatingSolver; + ///The different query logging solvers that can switched on/off enum QueryLoggingSolverType { diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h index 62f514ff..1cad98fd 100644 --- a/include/klee/Internal/Module/KInstruction.h +++ b/include/klee/Internal/Module/KInstruction.h @@ -11,7 +11,11 @@ #define KLEE_KINSTRUCTION_H #include "klee/Config/Version.h" +#include "klee/Internal/Module/InstructionInfoTable.h" + #include "llvm/Support/DataTypes.h" +#include "llvm/Support/raw_ostream.h" + #include <vector> namespace llvm { @@ -39,7 +43,9 @@ namespace klee { unsigned dest; public: - virtual ~KInstruction(); + virtual ~KInstruction(); + void printFileLine(llvm::raw_ostream &); + }; struct KGEPInstruction : KInstruction { diff --git a/include/klee/Internal/Support/FileHandling.h b/include/klee/Internal/Support/FileHandling.h new file mode 100644 index 00000000..bee06b9b --- /dev/null +++ b/include/klee/Internal/Support/FileHandling.h @@ -0,0 +1,19 @@ +//===-- FileHandling.h ------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#ifndef __KLEE_FILE_HANDLING_H__ +#define __KLEE_FILE_HANDLING_H__ +#include "llvm/Support/raw_ostream.h" +#include <string> + +namespace klee { +llvm::raw_fd_ostream *klee_open_output_file(std::string &path, + std::string &error); +} + +#endif diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index 4c428994..40f59ff1 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -138,6 +138,8 @@ public: virtual void setInhibitForking(bool value) = 0; + virtual void prepareForEarlyExit() = 0; + /*** State accessor methods ***/ virtual unsigned getPathStreamID(const ExecutionState &state) = 0; diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 2f613992..e669c6f4 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -203,60 +203,6 @@ namespace klee { virtual void setCoreSolverTimeout(double timeout); }; -#ifdef ENABLE_STP - /// STPSolver - A complete solver based on STP. - class STPSolver : public Solver { - public: - /// STPSolver - Construct a new STPSolver. - /// - /// \param useForkedSTP - Whether STP should be run in a separate process - /// (required for using timeouts). - /// \param optimizeDivides - Whether constant division operations should - /// be optimized into add/shift/multiply operations. - STPSolver(bool useForkedSTP, bool optimizeDivides = true); - - /// getConstraintLog - Return the constraint log for the given state in CVC - /// format. - virtual char *getConstraintLog(const Query&); - - /// setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0 - /// is off. - virtual void setCoreSolverTimeout(double timeout); - }; -#endif // ENABLE_STP - -#ifdef ENABLE_Z3 - /// Z3Solver - A solver complete solver based on Z3 - class Z3Solver : public Solver { - public: - /// Z3Solver - Construct a new Z3Solver. - Z3Solver(); - - /// Get the query in SMT-LIBv2 format. - /// \return A C-style string. The caller is responsible for freeing this. - virtual char *getConstraintLog(const Query &); - - /// setCoreSolverTimeout - Set constraint solver timeout delay to the given - /// value; 0 - /// is off. - virtual void setCoreSolverTimeout(double timeout); - }; -#endif // ENABLE_Z3 - -#ifdef ENABLE_METASMT - - template<typename SolverContext> - class MetaSMTSolver : public Solver { - public: - MetaSMTSolver(bool useForked, bool optimizeDivides); - virtual ~MetaSMTSolver(); - - virtual char *getConstraintLog(const Query&); - virtual void setCoreSolverTimeout(double timeout); -}; - -#endif /* ENABLE_METASMT */ - /* *** */ /// createValidatingSolver - Create a solver which will validate all query @@ -268,6 +214,12 @@ namespace klee { /// \param oracle - The solver to check query results against. Solver *createValidatingSolver(Solver *s, Solver *oracle); + /// createAssignmentValidatingSolver - Create a solver that when requested + /// for an assignment will check that the computed assignment satisfies + /// the Query. + /// \param s - The underlying solver to use. + Solver *createAssignmentValidatingSolver(Solver *s); + /// createCachingSolver - Create a solver which will cache the queries in /// memory (without eviction). /// diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 5d8aa1ab..55e681de 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -46,6 +46,7 @@ namespace klee { ref<Expr> evaluate(const Array *mo, unsigned index) const; ref<Expr> evaluate(ref<Expr> e); + void createConstraintsFromAssignment(std::vector<ref<Expr> > &out) const; template<typename InputIterator> bool satisfies(InputIterator begin, InputIterator end); diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index e55c4550..82cb01b2 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -82,6 +82,10 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( llvm::cl::CommaSeparated ); +llvm::cl::opt<bool> + UseAssignmentValidatingSolver("debug-assignment-validating-solver", + llvm::cl::init(false)); + #ifdef ENABLE_METASMT #ifdef METASMT_DEFAULT_BACKEND_IS_BTOR diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 68e1b08b..d00fcec1 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -37,6 +37,9 @@ Solver *constructSolverChain(Solver *coreSolver, baseSolverQuerySMT2LogPath.c_str()); } + if (UseAssignmentValidatingSolver) + solver = createAssignmentValidatingSolver(solver); + if (UseFastCexSolver) solver = createFastCexSolver(solver); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8a445aa3..5af31125 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -81,6 +81,7 @@ #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ErrorHandling.h" +#include "llvm/Support/FileSystem.h" #include "llvm/Support/Process.h" #include "llvm/Support/raw_ostream.h" @@ -383,7 +384,13 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, if (!DebugCompressInstructions) { #endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + std::error_code ec; + debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ec, + llvm::sys::fs::OpenFlags::F_Text); + if (ec) + ErrorInfo = ec.message(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text); #else @@ -976,14 +983,18 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { falseState->ptreeNode = res.first; trueState->ptreeNode = res.second; - if (!isInternal) { - if (pathWriter) { - falseState->pathOS = pathWriter->open(current.pathOS); + if (pathWriter) { + // Need to update the pathOS.id field of falseState, otherwise the same id + // is used for both falseState and trueState. + falseState->pathOS = pathWriter->open(current.pathOS); + if (!isInternal) { trueState->pathOS << "1"; falseState->pathOS << "0"; - } - if (symPathWriter) { - falseState->symPathOS = symPathWriter->open(current.symPathOS); + } + } + if (symPathWriter) { + falseState->symPathOS = symPathWriter->open(current.symPathOS); + if (!isInternal) { trueState->symPathOS << "1"; falseState->symPathOS << "0"; } @@ -1235,8 +1246,11 @@ void Executor::printDebugInstructions(ExecutionState &state) { stream = &debugLogBuffer; if (!optionIsSet(DebugPrintInstructions, STDERR_COMPACT) && - !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) - printFileLine(state, state.pc, *stream); + !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) { + (*stream) << " "; + state.pc->printFileLine(*stream); + (*stream) << ":"; + } (*stream) << state.pc->info->id; @@ -1461,15 +1475,6 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src, } } -void Executor::printFileLine(ExecutionState &state, KInstruction *ki, - llvm::raw_ostream &debugFile) { - const InstructionInfo &ii = *ki->info; - if (ii.file != "") - debugFile << " " << ii.file << ":" << ii.line << ":"; - else - debugFile << " [no debug info]:"; -} - /// Compute the true target of a function call, resolving LLVM and KLEE aliases /// and bitcasts. Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { @@ -1481,9 +1486,13 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { while (true) { if (GlobalValue *gv = dyn_cast<GlobalValue>(c)) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (!Visited.insert(gv).second) + return 0; +#else if (!Visited.insert(gv)) return 0; - +#endif std::string alias = state.getFnAlias(gv->getName()); if (alias != "") { llvm::Module* currModule = kmodule->module; @@ -3082,7 +3091,6 @@ void Executor::callExternalFunction(ExecutionState &state, else klee_warning_once(function, "%s", os.str().c_str()); } - bool success = externalDispatcher->executeCall(function, target->inst, args); if (!success) { terminateStateOnError(state, "failed external call: " + function->getName(), @@ -3837,6 +3845,13 @@ size_t Executor::getAllocationAlignment(const llvm::Value *allocSite) const { "Returned alignment must be a power of two"); return alignment; } + +void Executor::prepareForEarlyExit() { + if (statsTracker) { + // Make sure stats get flushed out + statsTracker->done(); + } +} /// Interpreter *Interpreter::create(LLVMContext &ctx, const InterpreterOptions &opts, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 7c18ae1f..c3f6e705 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -487,6 +487,8 @@ public: inhibitForking = value; } + void prepareForEarlyExit(); + /*** State accessor methods ***/ virtual unsigned getPathStreamID(const ExecutionState &state); diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 01c5f935..df0dd9a9 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -11,19 +11,24 @@ #include "klee/Config/Version.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) -#include "llvm/IR/Module.h" #include "llvm/IR/Constants.h" #include "llvm/IR/DerivedTypes.h" #include "llvm/IR/Instructions.h" #include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" #else -#include "llvm/Module.h" #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Instructions.h" #include "llvm/LLVMContext.h" +#include "llvm/Module.h" #endif +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) +#include "llvm/ExecutionEngine/MCJIT.h" +#else #include "llvm/ExecutionEngine/JIT.h" +#endif + #include "llvm/ExecutionEngine/GenericValue.h" #include "llvm/Support/DynamicLibrary.h" #include "llvm/Support/raw_ostream.h" @@ -55,12 +60,48 @@ extern "C" { static void sigsegv_handler(int signal, siginfo_t *info, void *context) { longjmp(escapeCallJmpBuf, 1); } +} +namespace klee { + +class ExternalDispatcherImpl { +private: + typedef std::map<const llvm::Instruction *, llvm::Function *> dispatchers_ty; + dispatchers_ty dispatchers; + llvm::Function *createDispatcher(llvm::Function *f, llvm::Instruction *i, + llvm::Module *module); + llvm::ExecutionEngine *executionEngine; + LLVMContext &ctx; + std::map<std::string, void *> preboundFunctions; + bool runProtectedCall(llvm::Function *f, uint64_t *args); + llvm::Module *singleDispatchModule; + std::vector<std::string> moduleIDs; + std::string &getFreshModuleID(); + +public: + ExternalDispatcherImpl(llvm::LLVMContext &ctx); + ~ExternalDispatcherImpl(); + bool executeCall(llvm::Function *function, llvm::Instruction *i, + uint64_t *args); + void *resolveSymbol(const std::string &name); +}; + +std::string &ExternalDispatcherImpl::getFreshModuleID() { + // We store the module IDs because `llvm::Module` constructor takes the + // module ID as a StringRef so it doesn't own the ID. Therefore we need to + // own the ID. + static uint64_t counter = 0; + std::string underlyingString; + llvm::raw_string_ostream ss(underlyingString); + ss << "ExternalDispatcherModule_" << counter; + moduleIDs.push_back(ss.str()); // moduleIDs now has a copy + ++counter; // Increment for next call + return moduleIDs.back(); } -void *ExternalDispatcher::resolveSymbol(const std::string &name) { +void *ExternalDispatcherImpl::resolveSymbol(const std::string &name) { assert(executionEngine); - + const char *str = name.c_str(); // We use this to validate that function names can be resolved so we @@ -74,10 +115,10 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) { void *addr = sys::DynamicLibrary::SearchForAddressOfSymbol(str); if (addr) return addr; - + // If it has an asm specifier and starts with an underscore we retry // without the underscore. I (DWD) don't know why. - if (name[0] == 1 && str[0]=='_') { + if (name[0] == 1 && str[0] == '_') { ++str; addr = sys::DynamicLibrary::SearchForAddressOfSymbol(str); } @@ -85,11 +126,24 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) { return addr; } -ExternalDispatcher::ExternalDispatcher(LLVMContext &ctx) { - dispatchModule = new Module("ExternalDispatcher", ctx); - +ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx) : ctx(ctx) { std::string error; - executionEngine = ExecutionEngine::createJIT(dispatchModule, &error); + singleDispatchModule = new Module(getFreshModuleID(), ctx); +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 6) + // Use old JIT + executionEngine = ExecutionEngine::createJIT(singleDispatchModule, &error); +#else + // Use MCJIT. + // The MCJIT JITs whole modules at a time rather than individual functions + // so we will let it manage the modules. + // Note that we don't do anything with `singleDispatchModule`. This is just + // so we can use the EngineBuilder API. + auto dispatchModuleUniq = std::unique_ptr<Module>(singleDispatchModule); + executionEngine = EngineBuilder(std::move(dispatchModuleUniq)) + .setEngineKind(EngineKind::JIT) + .create(); +#endif + if (!executionEngine) { llvm::errs() << "unable to make jit: " << error << "\n"; abort(); @@ -98,6 +152,10 @@ ExternalDispatcher::ExternalDispatcher(LLVMContext &ctx) { // If we have a native target, initialize it to ensure it is linked in and // usable by the JIT. llvm::InitializeNativeTarget(); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + llvm::InitializeNativeTargetAsmParser(); + llvm::InitializeNativeTargetAsmPrinter(); +#endif // from ExecutionEngine::create if (executionEngine) { @@ -107,61 +165,90 @@ ExternalDispatcher::ExternalDispatcher(LLVMContext &ctx) { } #ifdef WINDOWS - preboundFunctions["getpid"] = (void*) (long) getpid; - preboundFunctions["putchar"] = (void*) (long) putchar; - preboundFunctions["printf"] = (void*) (long) printf; - preboundFunctions["fprintf"] = (void*) (long) fprintf; - preboundFunctions["sprintf"] = (void*) (long) sprintf; + preboundFunctions["getpid"] = (void *)(long)getpid; + preboundFunctions["putchar"] = (void *)(long)putchar; + preboundFunctions["printf"] = (void *)(long)printf; + preboundFunctions["fprintf"] = (void *)(long)fprintf; + preboundFunctions["sprintf"] = (void *)(long)sprintf; #endif } -ExternalDispatcher::~ExternalDispatcher() { +ExternalDispatcherImpl::~ExternalDispatcherImpl() { delete executionEngine; + // NOTE: the `executionEngine` owns all modules so + // we don't need to delete any of them. } -bool ExternalDispatcher::executeCall(Function *f, Instruction *i, uint64_t *args) { +bool ExternalDispatcherImpl::executeCall(Function *f, Instruction *i, + uint64_t *args) { dispatchers_ty::iterator it = dispatchers.find(i); - Function *dispatcher; + if (it != dispatchers.end()) { + // Code already JIT'ed for this + return runProtectedCall(it->second, args); + } - if (it == dispatchers.end()) { + // Code for this not JIT'ed. Do this now. + Function *dispatcher; #ifdef WINDOWS - std::map<std::string, void*>::iterator it2 = - preboundFunctions.find(f->getName())); - - if (it2 != preboundFunctions.end()) { - // only bind once - if (it2->second) { - executionEngine->addGlobalMapping(f, it2->second); - it2->second = 0; - } + std::map<std::string, void *>::iterator it2 = + preboundFunctions.find(f->getName()); + + if (it2 != preboundFunctions.end()) { + // only bind once + if (it2->second) { + executionEngine->addGlobalMapping(f, it2->second); + it2->second = 0; } + } #endif - dispatcher = createDispatcher(f,i); - - dispatchers.insert(std::make_pair(i, dispatcher)); - - if (dispatcher) { - // Force the JIT execution engine to go ahead and build the function. This - // ensures that any errors or assertions in the compilation process will - // trigger crashes instead of being caught as aborts in the external - // function. - executionEngine->recompileAndRelinkFunction(dispatcher); - } + Module *dispatchModule = NULL; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + // The MCJIT generates whole modules at a time so for every call that we + // haven't made before we need to create a new Module. + dispatchModule = new Module(getFreshModuleID(), ctx); +#else + dispatchModule = this->singleDispatchModule; +#endif + dispatcher = createDispatcher(f, i, dispatchModule); + dispatchers.insert(std::make_pair(i, dispatcher)); + +// Force the JIT execution engine to go ahead and build the function. This +// ensures that any errors or assertions in the compilation process will +// trigger crashes instead of being caught as aborts in the external +// function. +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (dispatcher) { + // The dispatchModule is now ready so tell MCJIT to generate the code for + // it. + auto dispatchModuleUniq = std::unique_ptr<Module>(dispatchModule); + executionEngine->addModule( + std::move(dispatchModuleUniq)); // MCJIT takes ownership + // Force code generation + uint64_t fnAddr = + executionEngine->getFunctionAddress(dispatcher->getName()); + executionEngine->finalizeObject(); + assert(fnAddr && "failed to get function address"); + (void)fnAddr; } else { - dispatcher = it->second; + // MCJIT didn't take ownership of the module so delete it. + delete dispatchModule; } - +#else + if (dispatcher) { + // Old JIT works on a function at a time so compile the function. + executionEngine->recompileAndRelinkFunction(dispatcher); + } +#endif return runProtectedCall(dispatcher, args); } // FIXME: This is not reentrant. static uint64_t *gTheArgsP; - -bool ExternalDispatcher::runProtectedCall(Function *f, uint64_t *args) { +bool ExternalDispatcherImpl::runProtectedCall(Function *f, uint64_t *args) { struct sigaction segvAction, segvActionOld; bool res; - + if (!f) return false; @@ -185,85 +272,87 @@ bool ExternalDispatcher::runProtectedCall(Function *f, uint64_t *args) { return res; } +// FIXME: This might have been relevant for the old JIT but the MCJIT +// has a completly different implementation so this comment below is +// likely irrelevant and misleading. +// // For performance purposes we construct the stub in such a way that the // arguments pointer is passed through the static global variable gTheArgsP in // this file. This is done so that the stub function prototype trivially matches // the special cases that the JIT knows how to directly call. If this is not // done, then the jit will end up generating a nullary stub just to call our // stub, for every single function call. -Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *inst) { +Function *ExternalDispatcherImpl::createDispatcher(Function *target, + Instruction *inst, + Module *module) { if (!resolveSymbol(target->getName())) return 0; - LLVMContext &ctx = target->getContext(); CallSite cs; - if (inst->getOpcode()==Instruction::Call) { + if (inst->getOpcode() == Instruction::Call) { cs = CallSite(cast<CallInst>(inst)); } else { cs = CallSite(cast<InvokeInst>(inst)); } - Value **args = new Value*[cs.arg_size()]; + Value **args = new Value *[cs.arg_size()]; - std::vector<LLVM_TYPE_Q Type*> nullary; - - Function *dispatcher = Function::Create(FunctionType::get(Type::getVoidTy(ctx), - nullary, false), - GlobalVariable::ExternalLinkage, - "", - dispatchModule); + std::vector<LLVM_TYPE_Q Type *> nullary; + // MCJIT functions need unique names, or wrong function can be called. + // The module identifier is included because for the MCJIT we need + // unique function names across all `llvm::Modules`s. + std::string fnName = + "dispatcher_" + target->getName().str() + module->getModuleIdentifier(); + Function *dispatcher = + Function::Create(FunctionType::get(Type::getVoidTy(ctx), nullary, false), + GlobalVariable::ExternalLinkage, fnName, module); BasicBlock *dBB = BasicBlock::Create(ctx, "entry", dispatcher); // Get a Value* for &gTheArgsP, as an i64**. - Instruction *argI64sp = - new IntToPtrInst(ConstantInt::get(Type::getInt64Ty(ctx), - (uintptr_t) (void*) &gTheArgsP), - PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))), - "argsp", dBB); - Instruction *argI64s = new LoadInst(argI64sp, "args", dBB); - + Instruction *argI64sp = new IntToPtrInst( + ConstantInt::get(Type::getInt64Ty(ctx), (uintptr_t)(void *)&gTheArgsP), + PointerType::getUnqual(PointerType::getUnqual(Type::getInt64Ty(ctx))), + "argsp", dBB); + Instruction *argI64s = new LoadInst(argI64sp, "args", dBB); + // Get the target function type. - LLVM_TYPE_Q FunctionType *FTy = - cast<FunctionType>(cast<PointerType>(target->getType())->getElementType()); + LLVM_TYPE_Q FunctionType *FTy = cast<FunctionType>( + cast<PointerType>(target->getType())->getElementType()); // Each argument will be passed by writing it into gTheArgsP[i]. unsigned i = 0, idx = 2; - for (CallSite::arg_iterator ai = cs.arg_begin(), ae = cs.arg_end(); - ai!=ae; ++ai, ++i) { + for (CallSite::arg_iterator ai = cs.arg_begin(), ae = cs.arg_end(); ai != ae; + ++ai, ++i) { // Determine the type the argument will be passed as. This accomodates for // the corresponding code in Executor.cpp for handling calls to bitcasted // functions. - LLVM_TYPE_Q Type *argTy = (i < FTy->getNumParams() ? FTy->getParamType(i) : - (*ai)->getType()); - Instruction *argI64p = - GetElementPtrInst::Create(argI64s, - ConstantInt::get(Type::getInt32Ty(ctx), idx), - "", dBB); - - Instruction *argp = new BitCastInst(argI64p, PointerType::getUnqual(argTy), - "", dBB); + LLVM_TYPE_Q Type *argTy = + (i < FTy->getNumParams() ? FTy->getParamType(i) : (*ai)->getType()); + Instruction *argI64p = GetElementPtrInst::Create( + argI64s, ConstantInt::get(Type::getInt32Ty(ctx), idx), "", dBB); + + Instruction *argp = + new BitCastInst(argI64p, PointerType::getUnqual(argTy), "", dBB); args[i] = new LoadInst(argp, "", dBB); unsigned argSize = argTy->getPrimitiveSizeInBits(); - idx += ((!!argSize ? argSize : 64) + 63)/64; + idx += ((!!argSize ? argSize : 64) + 63) / 64; } - Constant *dispatchTarget = - dispatchModule->getOrInsertFunction(target->getName(), FTy, - target->getAttributes()); + Constant *dispatchTarget = module->getOrInsertFunction( + target->getName(), FTy, target->getAttributes()); #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) - Instruction *result = CallInst::Create(dispatchTarget, - llvm::ArrayRef<Value *>(args, args+i), - "", dBB); + Instruction *result = CallInst::Create( + dispatchTarget, llvm::ArrayRef<Value *>(args, args + i), "", dBB); #else - Instruction *result = CallInst::Create(dispatchTarget, args, args+i, "", dBB); + Instruction *result = + CallInst::Create(dispatchTarget, args, args + i, "", dBB); #endif if (result->getType() != Type::getVoidTy(ctx)) { - Instruction *resp = - new BitCastInst(argI64s, PointerType::getUnqual(result->getType()), - "", dBB); + Instruction *resp = new BitCastInst( + argI64s, PointerType::getUnqual(result->getType()), "", dBB); new StoreInst(result, resp, dBB); } @@ -273,3 +362,18 @@ Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *in return dispatcher; } + +ExternalDispatcher::ExternalDispatcher(llvm::LLVMContext &ctx) + : impl(new ExternalDispatcherImpl(ctx)) {} + +ExternalDispatcher::~ExternalDispatcher() { delete impl; } + +bool ExternalDispatcher::executeCall(llvm::Function *function, + llvm::Instruction *i, uint64_t *args) { + return impl->executeCall(function, i, args); +} + +void *ExternalDispatcher::resolveSymbol(const std::string &name) { + return impl->resolveSymbol(name); +} +} diff --git a/lib/Core/ExternalDispatcher.h b/lib/Core/ExternalDispatcher.h index 94363bab..c64dc7d8 100644 --- a/lib/Core/ExternalDispatcher.h +++ b/lib/Core/ExternalDispatcher.h @@ -10,42 +10,37 @@ #ifndef KLEE_EXTERNALDISPATCHER_H #define KLEE_EXTERNALDISPATCHER_H +#include "klee/Config/Version.h" + #include <map> -#include <string> +#include <memory> #include <stdint.h> +#include <string> namespace llvm { - class ExecutionEngine; - class Instruction; - class LLVMContext; - class Function; - class FunctionType; - class Module; +class Instruction; +class LLVMContext; +class Function; } namespace klee { - class ExternalDispatcher { - private: - typedef std::map<const llvm::Instruction*,llvm::Function*> dispatchers_ty; - dispatchers_ty dispatchers; - llvm::Module *dispatchModule; - llvm::ExecutionEngine *executionEngine; - std::map<std::string, void*> preboundFunctions; - - llvm::Function *createDispatcher(llvm::Function *f, llvm::Instruction *i); - bool runProtectedCall(llvm::Function *f, uint64_t *args); - - public: - ExternalDispatcher(llvm::LLVMContext &ctx); - ~ExternalDispatcher(); - - /* Call the given function using the parameter passing convention of - * ci with arguments in args[1], args[2], ... and writing the result - * into args[0]. - */ - bool executeCall(llvm::Function *function, llvm::Instruction *i, uint64_t *args); - void *resolveSymbol(const std::string &name); - }; +class ExternalDispatcherImpl; +class ExternalDispatcher { +private: + ExternalDispatcherImpl *impl; + +public: + ExternalDispatcher(llvm::LLVMContext &ctx); + ~ExternalDispatcher(); + + /* Call the given function using the parameter passing convention of + * ci with arguments in args[1], args[2], ... and writing the result + * into args[0]. + */ + bool executeCall(llvm::Function *function, llvm::Instruction *i, + uint64_t *args); + void *resolveSymbol(const std::string &name); +}; } #endif diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index d08bfb0c..4e5c8734 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -50,8 +50,6 @@ public: mutable bool isGlobal; bool isFixed; - /// true if created by us. - bool fake_object; bool isUserSpecified; MemoryManager *parent; @@ -96,7 +94,6 @@ public: isLocal(_isLocal), isGlobal(_isGlobal), isFixed(_isFixed), - fake_object(false), isUserSpecified(false), parent(_parent), allocSite(_allocSite) { diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index c787382f..d15226b3 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -539,7 +539,7 @@ ExecutionState &BatchingSearcher::selectState() { if (lastState) { double delta = util::getWallTime()-lastStartTime; if (delta>timeBudget*1.1) { - klee_message("KLEE: increased time budget from %f to %f\n", timeBudget, + klee_message("increased time budget from %f to %f\n", timeBudget, delta); timeBudget = delta; } @@ -613,7 +613,7 @@ void IterativeDeepeningTimeSearcher::update( if (baseSearcher->empty()) { time *= 2; - klee_message("KLEE: increased time budget to %f\n", time); + klee_message("increased time budget to %f\n", time); std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end()); baseSearcher->update(0, ps, std::vector<ExecutionState *>()); pausedStates.clear(); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index ccf6e04d..b93796ec 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -168,7 +168,7 @@ static bool instructionIsCoverable(Instruction *i) { Instruction *prev = static_cast<Instruction *>(--it); if (isa<CallInst>(prev) || isa<InvokeInst>(prev)) { Function *target = - getDirectCallTarget(prev, /*moduleIsFullyLinked=*/true); + getDirectCallTarget(CallSite(prev), /*moduleIsFullyLinked=*/true); if (target && target->doesNotReturn()) return false; } @@ -206,13 +206,16 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, if (!sys::path::is_absolute(objectFilename)) { SmallString<128> current(objectFilename); if(sys::fs::make_absolute(current)) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + Twine current_twine(current.str()); // requires a twine for this + if (!sys::fs::exists(current_twine)) { +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + bool exists = false; + if (!sys::fs::exists(current.str(), exists)) { +#else bool exists = false; - -#if LLVM_VERSION_CODE < LLVM_VERSION(3, 5) error_code ec = sys::fs::exists(current.str(), exists); if (ec == errc::success && exists) { -#else - if (!sys::fs::exists(current.str(), exists)) { #endif objectFilename = current.c_str(); } diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp index 635362d4..d788785a 100644 --- a/lib/Expr/Assigment.cpp +++ b/lib/Expr/Assigment.cpp @@ -22,4 +22,21 @@ void Assignment::dump() { llvm::errs() << "]\n"; } } + +void Assignment::createConstraintsFromAssignment( + std::vector<ref<Expr> > &out) const { + assert(out.size() == 0 && "out should be empty"); + for (bindings_ty::const_iterator it = bindings.begin(), ie = bindings.end(); + it != ie; ++it) { + const Array *array = it->first; + const std::vector<unsigned char> &values = it->second; + for (unsigned arrayIndex = 0; arrayIndex < array->size; ++arrayIndex) { + unsigned char value = values[arrayIndex]; + out.push_back(EqExpr::create( + ReadExpr::create(UpdateList(array, 0), + ConstantExpr::alloc(arrayIndex, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); + } + } +} } diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp index 799620c6..a32745b8 100644 --- a/lib/Module/KInstruction.cpp +++ b/lib/Module/KInstruction.cpp @@ -17,3 +17,10 @@ using namespace klee; KInstruction::~KInstruction() { delete[] operands; } + +void KInstruction::printFileLine(llvm::raw_ostream &debugFile) { + if (info->file != "") + debugFile << info->file << ":" << info->line; + else + debugFile << "[no debug info]"; +} diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 08ec28ef..45dc34bf 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -158,8 +158,14 @@ static Function *getStubFunctionForCtorList(Module *m, if (arr) { for (unsigned i=0; i<arr->getNumOperands(); i++) { ConstantStruct *cs = cast<ConstantStruct>(arr->getOperand(i)); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + // There is a third *optional* element in global_ctor elements (``i8 + // @data``). + assert((cs->getNumOperands() == 2 || cs->getNumOperands() == 3) && + "unexpected element in ctor initializer list"); +#else assert(cs->getNumOperands()==2 && "unexpected element in ctor initializer list"); - +#endif Constant *fp = cs->getOperand(1); if (!fp->isNullValue()) { if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(fp)) @@ -513,8 +519,13 @@ static int getOperandNum(Value *v, return registerMap[inst]; } else if (Argument *a = dyn_cast<Argument>(v)) { return a->getArgNo(); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + // Metadata is no longer a Value + } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v)) { +#else } else if (isa<BasicBlock>(v) || isa<InlineAsm>(v) || isa<MDNode>(v)) { +#endif return -1; } else { assert(isa<Constant>(v)); diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 94a37e08..c7f1c6d9 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -212,15 +212,27 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading modules\n"); // Load all bitcode files in to memory so we can examine their symbols +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + for (object::Archive::child_iterator AI = archive->child_begin(), + AE = archive->child_end(); AI != AE; ++AI) +#else for (object::Archive::child_iterator AI = archive->begin_children(), AE = archive->end_children(); AI != AE; ++AI) +#endif { StringRef memberName; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<StringRef> memberNameErr = AI->getName(); + std::error_code ec = memberNameErr.getError(); + if (!ec) { + memberName = memberNameErr.get(); +#else error_code ec = AI->getName(memberName); if ( ec == errc::success ) { +#endif KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading archive member " << memberName << "\n"); } else @@ -229,17 +241,29 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er return false; } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<std::unique_ptr<llvm::object::Binary> > child = AI->getAsBinary(); + ec = child.getError(); +#else OwningPtr<object::Binary> child; ec = AI->getAsBinary(child); - if (ec != object::object_error::success) - { +#endif + if (ec) { // If we can't open as a binary object file its hopefully a bitcode file - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + ErrorOr<MemoryBufferRef> buff = AI->getMemoryBufferRef(); + ec = buff.getError(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<std::unique_ptr<MemoryBuffer> > buffErr = AI->getMemoryBuffer(); + std::unique_ptr<MemoryBuffer> buff = nullptr; + ec = buffErr.getError(); + if (!ec) + buff = std::move(buffErr.get()); +#else OwningPtr<MemoryBuffer> buff; // Once this is destroyed will Module still be valid?? - Module *Result = 0; - - if (error_code ec = AI->getMemoryBuffer(buff)) - { + ec = AI->getMemoryBuffer(buff); +#endif + if (ec) { SS << "Failed to get MemoryBuffer: " <<ec.message(); SS.flush(); return false; @@ -247,10 +271,20 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er if (buff) { + Module *Result = 0; // FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<Module *> resultErr = parseBitcodeFile(buff.get(), + composite->getContext()); + ec = resultErr.getError(); + if (ec) + errorMessage = ec.message(); + else + Result = resultErr.get(); +#else Result = ParseBitcodeFile(buff.get(), composite->getContext(), &errorMessage); - +#endif if(!Result) { SS << "Loading module failed : " << errorMessage << "\n"; @@ -266,9 +300,9 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er } } - else if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(child.get())) + else if (child.get()->isObject()) { - SS << "Object file " << o->getFileName().data() << + SS << "Object file " << child.get()->getFileName().data() << " in archive is not supported"; SS.flush(); return false; @@ -317,8 +351,11 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Found " << GV->getName() << " in " << M->getModuleIdentifier() << "\n"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (Linker::LinkModules(composite, M)) +#else if (Linker::LinkModules(composite, M, Linker::DestroySource, &errorMessage)) +#endif { // Linking failed SS << "Linking archive module with composite failed:" << errorMessage; @@ -371,36 +408,86 @@ Module *klee::linkWithLibrary(Module *module, libraryName.c_str()); } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<std::unique_ptr<MemoryBuffer> > bufferErr = + MemoryBuffer::getFile(libraryName); + std::error_code ec = bufferErr.getError(); +#else OwningPtr<MemoryBuffer> Buffer; - if (error_code ec = MemoryBuffer::getFile(libraryName,Buffer)) { + error_code ec = MemoryBuffer::getFile(libraryName,Buffer); +#endif + if (ec) { klee_error("Link with library %s failed: %s", libraryName.c_str(), ec.message().c_str()); } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + MemoryBufferRef Buffer = bufferErr.get()->getMemBufferRef(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + MemoryBuffer *Buffer = bufferErr->get(); +#endif + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + sys::fs::file_magic magic = sys::fs::identify_magic(Buffer.getBuffer()); +#else sys::fs::file_magic magic = sys::fs::identify_magic(Buffer->getBuffer()); +#endif LLVMContext &Context = module->getContext(); std::string ErrorMessage; if (magic == sys::fs::file_magic::bitcode) { Module *Result = 0; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<Module *> ResultErr = parseBitcodeFile(Buffer, Context); + if ((ec = ResultErr.getError())) { + ErrorMessage = ec.message(); +#else Result = ParseBitcodeFile(Buffer.get(), Context, &ErrorMessage); + if (!Result) { +#endif + klee_error("Link with library %s failed: %s", libraryName.c_str(), + ErrorMessage.c_str()); + } +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + Result = ResultErr.get(); +#endif - if (!Result || Linker::LinkModules(module, Result, Linker::DestroySource, - &ErrorMessage)) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (Linker::LinkModules(module, Result)) { + ErrorMessage = "linking error"; +#else + if (Linker::LinkModules(module, Result, Linker::DestroySource, &ErrorMessage)) { +#endif klee_error("Link with library %s failed: %s", libraryName.c_str(), ErrorMessage.c_str()); + } delete Result; } else if (magic == sys::fs::file_magic::archive) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + ErrorOr<std::unique_ptr<object::Binary> > arch = + object::createBinary(Buffer, &Context); + ec = arch.getError(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + ErrorOr<object::Binary *> arch = + object::createBinary(std::move(bufferErr.get()), &Context); + ec = arch.getError(); +#else OwningPtr<object::Binary> arch; - if (error_code ec = object::createBinary(Buffer.take(), arch)) + ec = object::createBinary(Buffer.take(), arch); +#endif + if (ec) klee_error("Link with library %s failed: %s", libraryName.c_str(), ec.message().c_str()); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + if (object::Archive *a = dyn_cast<object::Archive>(arch->get())) { +#else if (object::Archive *a = dyn_cast<object::Archive>(arch.get())) { +#endif // Handle in helper if (!linkBCA(a, module, ErrorMessage)) klee_error("Link with library %s failed: %s", libraryName.c_str(), @@ -411,11 +498,15 @@ Module *klee::linkWithLibrary(Module *module, } } else if (magic.is_object()) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + std::unique_ptr<object::Binary> obj; +#else OwningPtr<object::Binary> obj; - if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(obj.get())) { +#endif + if (obj.get()->isObject()) { klee_warning("Link with library: Object file %s in archive %s found. " "Currently not supported.", - o->getFileName().data(), libraryName.c_str()); + obj.get()->getFileName().data(), libraryName.c_str()); } } else { klee_error("Link with library %s failed: Unrecognized file type.", diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 3d9c8cc1..c0f3f34c 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -172,15 +172,17 @@ void Optimize(Module *M, const std::string &EntryPoint) { if (VerifyEach) Passes.add(createVerifierPass()); -#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) - // Add an appropriate TargetData instance for this module... - addPass(Passes, new TargetData(M)); -#elif LLVM_VERSION_CODE < LLVM_VERSION(3, 5) // Add an appropriate DataLayout instance for this module... +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + DataLayoutPass *dlpass = new DataLayoutPass(); + dlpass->doInitialization(*M); + addPass(Passes, dlpass); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + addPass(Passes, new DataLayoutPass(M)); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) addPass(Passes, new DataLayout(M)); #else - // Add an appropriate DataLayout instance for this module... - addPass(Passes, new DataLayoutPass(M)); + addPass(Passes, new TargetData(M)); #endif // DWD - Run the opt standard pass list as well. diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp index af92b74b..5fc54ef1 100644 --- a/lib/Module/RaiseAsm.cpp +++ b/lib/Module/RaiseAsm.cpp @@ -24,6 +24,10 @@ #include "llvm/Support/raw_ostream.h" #include "llvm/Support/Host.h" #include "llvm/Target/TargetLowering.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) +#include "llvm/Target/TargetMachine.h" +#include "llvm/Target/TargetSubtargetInfo.h" +#endif #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0) #include "llvm/Target/TargetRegistry.h" #else @@ -99,15 +103,20 @@ bool RaiseAsmPass::runOnModule(Module &M) { klee_warning("Warning: unable to select native target: %s", Err.c_str()); TLI = 0; } else { -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + TM = NativeTarget->createTargetMachine(HostTriple, "", "", TargetOptions()); + TLI = TM->getSubtargetImpl()->getTargetLowering(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) TM = NativeTarget->createTargetMachine(HostTriple, "", "", TargetOptions()); + TLI = TM->getTargetLowering(); #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) TM = NativeTarget->createTargetMachine(HostTriple, "", ""); + TLI = TM->getTargetLowering(); #else TM = NativeTarget->createTargetMachine(HostTriple, ""); -#endif TLI = TM->getTargetLowering(); +#endif triple = llvm::Triple(HostTriple); } diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp new file mode 100644 index 00000000..a4d97f54 --- /dev/null +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -0,0 +1,158 @@ +//===-- AssignmentValidatingSolver.cpp ------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/util/Assignment.h" +#include "klee/Constraints.h" +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include <vector> + +namespace klee { + +class AssignmentValidatingSolver : public SolverImpl { +private: + Solver *solver; + void dumpAssignmentQuery(const Query &query, const Assignment &assignment); + +public: + AssignmentValidatingSolver(Solver *_solver) : solver(_solver) {} + ~AssignmentValidatingSolver() { delete solver; } + + bool computeValidity(const Query &, Solver::Validity &result); + bool computeTruth(const Query &, bool &isValid); + bool computeValue(const Query &, ref<Expr> &result); + bool computeInitialValues(const Query &, + const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; + +// TODO: use computeInitialValues for all queries for more stress testing +bool AssignmentValidatingSolver::computeValidity(const Query &query, + Solver::Validity &result) { + return solver->impl->computeValidity(query, result); +} +bool AssignmentValidatingSolver::computeTruth(const Query &query, + bool &isValid) { + return solver->impl->computeTruth(query, isValid); +} +bool AssignmentValidatingSolver::computeValue(const Query &query, + ref<Expr> &result) { + return solver->impl->computeValue(query, result); +} + +bool AssignmentValidatingSolver::computeInitialValues( + const Query &query, const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, bool &hasSolution) { + bool success = + solver->impl->computeInitialValues(query, objects, values, hasSolution); + if (!hasSolution) + return success; + + // Use `_allowFreeValues` so that if we are missing an assignment + // we can't compute a constant and flag this as a problem. + Assignment assignment(objects, values, /*_allowFreeValues=*/true); + // Check computed assignment satisfies query + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + ref<Expr> constraint = *it; + ref<Expr> constraintEvaluated = assignment.evaluate(constraint); + ConstantExpr *CE = dyn_cast<ConstantExpr>(constraintEvaluated); + if (CE == NULL) { + llvm::errs() << "Constraint did not evalaute to a constant:\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Evaluated Constraint:\n" << constraintEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + if (CE->isFalse()) { + llvm::errs() << "Constraint evaluated to false when using assignment\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + } + + ref<Expr> queryExprEvaluated = assignment.evaluate(query.expr); + ConstantExpr *CE = dyn_cast<ConstantExpr>(queryExprEvaluated); + if (CE == NULL) { + llvm::errs() << "Query expression did not evalaute to a constant:\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Evaluated expression:\n" << queryExprEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + // KLEE queries are validity queries. A counter example to + // ∀ x constraints(x) → query(x) + // exists therefore + // ¬∀ x constraints(x) → query(x) + // Which is equivalent to + // ∃ x constraints(x) ∧ ¬ query(x) + // This means for the assignment we get back query expression should evaluate + // to false. + if (CE->isTrue()) { + llvm::errs() + << "Query Expression evaluated to true when using assignment\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + + return success; +} + +void AssignmentValidatingSolver::dumpAssignmentQuery( + const Query &query, const Assignment &assignment) { + // Create a Query that is augmented with constraints that + // enforce the given assignment. + std::vector<ref<Expr> > constraints; + assignment.createConstraintsFromAssignment(constraints); + // Add Constraints from `query` + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + constraints.push_back(*it); + } + ConstraintManager augmentedConstraints(constraints); + Query augmentedQuery(augmentedConstraints, query.expr); + + // Ask the solver for the log for this query. + char *logText = solver->getConstraintLog(augmentedQuery); + llvm::errs() << "Query with assignment as constraints:\n" << logText << "\n"; + free(logText); +} + +SolverImpl::SolverRunStatus +AssignmentValidatingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); +} + +char *AssignmentValidatingSolver::getConstraintLog(const Query &query) { + return solver->impl->getConstraintLog(query); +} + +void AssignmentValidatingSolver::setCoreSolverTimeout(double timeout) { + return solver->impl->setCoreSolverTimeout(timeout); +} + +Solver *createAssignmentValidatingSolver(Solver *s) { + return new Solver(new AssignmentValidatingSolver(s)); +} +} diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 1302db38..d9c393fb 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -7,6 +7,7 @@ # #===------------------------------------------------------------------------===# klee_add_component(kleaverSolver + AssignmentValidatingSolver.cpp CachingSolver.cpp CexCachingSolver.cpp ConstantDivision.cpp diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 783047f8..438f38f6 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -7,90 +7,48 @@ // //===----------------------------------------------------------------------===// +#include "STPSolver.h" +#include "Z3Solver.h" +#include "MetaSMTSolver.h" #include "klee/CommandLine.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" #include <string> -#ifdef ENABLE_METASMT - -#include <metaSMT/DirectSolver_Context.hpp> -#include <metaSMT/backend/Z3_Backend.hpp> -#include <metaSMT/backend/Boolector.hpp> - -#define Expr VCExpr -#define Type VCType -#define STP STP_Backend -#include <metaSMT/backend/STP.hpp> -#undef Expr -#undef Type -#undef STP - -using namespace klee; -using namespace metaSMT; -using namespace metaSMT::solver; - -static klee::Solver *handleMetaSMT() { - Solver *coreSolver = NULL; - std::string backend; - switch (MetaSMTBackend) { - case METASMT_BACKEND_STP: - backend = "STP"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_Z3: - backend = "Z3"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_BOOLECTOR: - backend = "Boolector"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - default: - llvm_unreachable("Unrecognised metasmt backend"); - break; - }; - llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; - return coreSolver; -} -#endif /* ENABLE_METASMT */ - namespace klee { Solver *createCoreSolver(CoreSolverType cst) { switch (cst) { case STP_SOLVER: #ifdef ENABLE_STP - llvm::errs() << "Using STP solver backend\n"; + klee_message("Using STP solver backend"); return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); #else - llvm::errs() << "Not compiled with STP support\n"; + klee_message("Not compiled with STP support"); return NULL; #endif case METASMT_SOLVER: #ifdef ENABLE_METASMT - llvm::errs() << "Using MetaSMT solver backend\n"; - return handleMetaSMT(); + klee_message("Using MetaSMT solver backend"); + return createMetaSMTSolver(); #else - llvm::errs() << "Not compiled with MetaSMT support\n"; + klee_message("Not compiled with MetaSMT support"); return NULL; #endif case DUMMY_SOLVER: return createDummySolver(); case Z3_SOLVER: #ifdef ENABLE_Z3 - llvm::errs() << "Using Z3 solver backend\n"; + klee_message("Using Z3 solver backend"); return new Z3Solver(); #else - llvm::errs() << "Not compiled with Z3 support\n"; + klee_message("Not compiled with Z3 support"); return NULL; #endif case NO_SOLVER: - llvm::errs() << "Invalid solver\n"; + klee_message("Invalid solver"); return NULL; default: llvm_unreachable("Unsupported CoreSolverType"); diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index a453de40..9b49f995 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -9,6 +9,7 @@ #include "klee/Config/config.h" #ifdef ENABLE_METASMT +#include "MetaSMTSolver.h" #include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Internal/Support/ErrorHandling.h" @@ -17,6 +18,8 @@ #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/ErrorHandling.h" + #include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> @@ -405,5 +408,36 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >; + +Solver *createMetaSMTSolver() { + using metaSMT::DirectSolver_Context; + using namespace metaSMT::solver; + + Solver *coreSolver = NULL; + std::string backend; + switch (MetaSMTBackend) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + llvm_unreachable("Unrecognised MetaSMT backend"); + break; + }; + klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); + return coreSolver; +} + } #endif // ENABLE_METASMT diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h new file mode 100644 index 00000000..60d72383 --- /dev/null +++ b/lib/Solver/MetaSMTSolver.h @@ -0,0 +1,32 @@ +//===-- MetaSMTSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_METASMTSOLVER_H +#define KLEE_METASMTSOLVER_H + +#include "klee/Solver.h" + +namespace klee { + +template <typename SolverContext> class MetaSMTSolver : public Solver { +public: + MetaSMTSolver(bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolver(); + + virtual char *getConstraintLog(const Query &); + virtual void setCoreSolverTimeout(double timeout); +}; + +/// createMetaSMTSolver - Create a solver using the metaSMT backend set by +/// the option MetaSMTBackend. +Solver *createMetaSMTSolver(); +} + +#endif /* KLEE_METASMTSOLVER_H */ diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index a858a7d7..cf4966cd 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -42,7 +42,13 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, #ifdef HAVE_ZLIB_H if (!CreateCompressedQueryLog) { #endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + std::error_code ec; + os = new llvm::raw_fd_ostream(path.c_str(), ec, + llvm::sys::fs::OpenFlags::F_Text); + if (ec) + ErrorInfo = ec.message(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text); #else diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 5893c28e..d1b8cbdc 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" #ifdef ENABLE_STP +#include "STPSolver.h" #include "STPBuilder.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h new file mode 100644 index 00000000..cb68ed91 --- /dev/null +++ b/lib/Solver/STPSolver.h @@ -0,0 +1,39 @@ +//===-- STPSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_STPSOLVER_H +#define KLEE_STPSOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// STPSolver - A complete solver based on STP. +class STPSolver : public Solver { +public: + /// STPSolver - Construct a new STPSolver. + /// + /// \param useForkedSTP - Whether STP should be run in a separate process + /// (required for using timeouts). + /// \param optimizeDivides - Whether constant division operations should + /// be optimized into add/shift/multiply operations. + STPSolver(bool useForkedSTP, bool optimizeDivides = true); + + /// getConstraintLog - Return the constraint log for the given state in CVC + /// format. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_STPSOLVER_H */ diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index fc826c07..6c0653e8 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -11,10 +11,10 @@ #include "Z3Builder.h" #include "klee/Expr.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" -#include "klee/util/Bits.h" -#include "ConstantDivision.h" #include "klee/SolverStats.h" +#include "klee/util/Bits.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" @@ -26,6 +26,21 @@ llvm::cl::opt<bool> UseConstructHashZ3( "use-construct-hash-z3", llvm::cl::desc("Use hash-consing during Z3 query construction."), llvm::cl::init(true)); + +// FIXME: This should be std::atomic<bool>. Need C++11 for that. +bool Z3InterationLogOpen = false; +} + +namespace klee { + +// Declared here rather than `Z3Builder.h` so they can be called in gdb. +template <> void Z3NodeHandle<Z3_sort>::dump() { + llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) + << "\n"; +} +template <> void Z3NodeHandle<Z3_ast>::dump() { + llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) + << "\n"; } void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { @@ -45,6 +60,9 @@ void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { } llvm::errs() << "Error: Incorrect use of Z3. [" << ec << "] " << errorMsg << "\n"; + // NOTE: The current implementation of `Z3_close_log()` can be safely + // called even if the log isn't open. + Z3_close_log(); abort(); } @@ -55,8 +73,17 @@ void Z3ArrayExprHash::clear() { _array_hash.clear(); } -Z3Builder::Z3Builder(bool autoClearConstructCache) - : autoClearConstructCache(autoClearConstructCache) { +Z3Builder::Z3Builder(bool autoClearConstructCache, const char* z3LogInteractionFileArg) + : autoClearConstructCache(autoClearConstructCache), z3LogInteractionFile("") { + if (z3LogInteractionFileArg) + this->z3LogInteractionFile = std::string(z3LogInteractionFileArg); + if (z3LogInteractionFile.length() > 0) { + klee_message("Logging Z3 API interaction to \"%s\"", + z3LogInteractionFile.c_str()); + assert(!Z3InterationLogOpen && "interaction log should not already be open"); + Z3_open_log(z3LogInteractionFile.c_str()); + Z3InterationLogOpen = true; + } // FIXME: Should probably let the client pass in a Z3_config instead Z3_config cfg = Z3_mk_config(); // It is very important that we ask Z3 to let us manage memory so that @@ -75,6 +102,10 @@ Z3Builder::~Z3Builder() { clearConstructCache(); _arr_hash.clear(); Z3_del_context(ctx); + if (z3LogInteractionFile.length() > 0) { + Z3_close_log(); + Z3InterationLogOpen = false; + } } Z3SortHandle Z3Builder::getBvSort(unsigned width) { @@ -529,6 +560,7 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { if (srcWidth == 1) { return iteExpr(src, bvOne(*width_out), bvZero(*width_out)); } else { + assert(*width_out > srcWidth && "Invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - srcWidth), src), ctx); } @@ -621,12 +653,15 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { uint64_t divisor = CE->getZExtValue(); if (bits64::isPowerOfTwo(divisor)) { - unsigned bits = bits64::indexOfSingleBit(divisor); + // FIXME: This should be unsigned but currently needs to be signed to + // avoid signed-unsigned comparison in assert. + int bits = bits64::indexOfSingleBit(divisor); // special case for modding by 1 or else we bvExtract -1:0 if (bits == 0) { return bvZero(*width_out); } else { + assert(*width_out > bits && "invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - bits), bvExtract(left, bits - 1, 0)), ctx); @@ -816,4 +851,5 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { return getTrue(); } } +} #endif // ENABLE_Z3 diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index f3b2732b..a3473f82 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -81,19 +81,13 @@ template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() { // instead to simplify our implementation but this seems cleaner. return ::Z3_sort_to_ast(context, node); } -template <> inline void Z3NodeHandle<Z3_sort>::dump() { - llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) - << "\n"; -} typedef Z3NodeHandle<Z3_sort> Z3SortHandle; +template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used)); // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; } -template <> inline void Z3NodeHandle<Z3_ast>::dump() { - llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) - << "\n"; -} typedef Z3NodeHandle<Z3_ast> Z3ASTHandle; +template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used)); class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> { @@ -171,11 +165,11 @@ private: Z3SortHandle getBvSort(unsigned width); Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort); bool autoClearConstructCache; + std::string z3LogInteractionFile; public: Z3_context ctx; - - Z3Builder(bool autoClearConstructCache = true); + Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile); ~Z3Builder(); Z3ASTHandle getTrue(); diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 1cbca566..985c143d 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -8,13 +8,37 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Internal/Support/FileHandling.h" #ifdef ENABLE_Z3 +#include "Z3Solver.h" #include "Z3Builder.h" #include "klee/Constraints.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" + +namespace { +// NOTE: Very useful for debugging Z3 behaviour. These files can be given to +// the z3 binary to replay all Z3 API calls using its `-log` option. +llvm::cl::opt<std::string> Z3LogInteractionFile( + "debug-z3-log-api-interaction", llvm::cl::init(""), + llvm::cl::desc("Log API interaction with Z3 to the specified path")); + +llvm::cl::opt<std::string> Z3QueryDumpFile( + "debug-z3-dump-queries", llvm::cl::init(""), + llvm::cl::desc("Dump Z3's representation of the query to the specified path")); + +llvm::cl::opt<bool> Z3ValidateModels( + "debug-z3-validate-models", llvm::cl::init(false), + llvm::cl::desc("When generating Z3 models validate these against the query")); + +llvm::cl::opt<unsigned> + Z3VerbosityLevel("debug-z3-verbosity", llvm::cl::init(0), + llvm::cl::desc("Z3 verbosity level (default=0)")); +} #include "llvm/Support/ErrorHandling.h" @@ -25,6 +49,7 @@ private: Z3Builder *builder; double timeout; SolverRunStatus runStatusCode; + llvm::raw_fd_ostream* dumpedQueriesFile; ::Z3_params solverParameters; // Parameter symbols ::Z3_symbol timeoutParamStrSymbol; @@ -33,6 +58,7 @@ private: const std::vector<const Array *> *objects, std::vector<std::vector<unsigned char> > *values, bool &hasSolution); +bool validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel); public: Z3SolverImpl(); @@ -65,18 +91,47 @@ public: }; Z3SolverImpl::Z3SolverImpl() - : builder(new Z3Builder(/*autoClearConstructCache=*/false)), timeout(0.0), - runStatusCode(SOLVER_RUN_STATUS_FAILURE) { + : builder(new Z3Builder( + /*autoClearConstructCache=*/false, + /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0 + ? Z3LogInteractionFile.c_str() + : NULL)), + timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE), + dumpedQueriesFile(0) { assert(builder && "unable to create Z3Builder"); solverParameters = Z3_mk_params(builder->ctx); Z3_params_inc_ref(builder->ctx, solverParameters); timeoutParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "timeout"); setCoreSolverTimeout(timeout); + + if (!Z3QueryDumpFile.empty()) { + std::string error; + dumpedQueriesFile = klee_open_output_file(Z3QueryDumpFile, error); + if (!error.empty()) { + klee_error("Error creating file for dumping Z3 queries: %s", + error.c_str()); + } + klee_message("Dumping Z3 queries to \"%s\"", Z3QueryDumpFile.c_str()); + } + + // Set verbosity + if (Z3VerbosityLevel > 0) { + std::string underlyingString; + llvm::raw_string_ostream ss(underlyingString); + ss << Z3VerbosityLevel; + ss.flush(); + Z3_global_param_set("verbose", underlyingString.c_str()); + } } Z3SolverImpl::~Z3SolverImpl() { Z3_params_dec_ref(builder->ctx, solverParameters); delete builder; + + if (dumpedQueriesFile) { + dumpedQueriesFile->close(); + delete dumpedQueriesFile; + } } Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {} @@ -91,10 +146,18 @@ void Z3Solver::setCoreSolverTimeout(double timeout) { char *Z3SolverImpl::getConstraintLog(const Query &query) { std::vector<Z3ASTHandle> assumptions; + // We use a different builder here because we don't want to interfere + // with the solver's builder because it may change the solver builder's + // cache. + // NOTE: The builder does not set `z3LogInteractionFile` to avoid conflicting + // with whatever the solver's builder is set to do. + Z3Builder temp_builder(/*autoClearConstructCache=*/false, + /*z3LogInteractionFile=*/NULL); + for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { - assumptions.push_back(builder->construct(*it)); + assumptions.push_back(temp_builder.construct(*it)); } ::Z3_ast *assumptionsArray = NULL; int numAssumptions = query.constraints.size(); @@ -111,10 +174,11 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { // the negation of the equivalent i.e. // ∃ X Constraints(X) ∧ ¬ query(X) Z3ASTHandle formula = Z3ASTHandle( - Z3_mk_not(builder->ctx, builder->construct(query.expr)), builder->ctx); + Z3_mk_not(temp_builder.ctx, temp_builder.construct(query.expr)), + temp_builder.ctx); ::Z3_string result = Z3_benchmark_to_smtlib_string( - builder->ctx, + temp_builder.ctx, /*name=*/"Emited by klee::Z3SolverImpl::getConstraintLog()", /*logic=*/"", /*status=*/"unknown", @@ -125,6 +189,12 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { if (numAssumptions) free(assumptionsArray); + + // We need to trigger a dereference before the `temp_builder` gets destroyed. + // We do this indirectly by emptying `assumptions` and assigning to + // `formula`. + assumptions.clear(); + formula = Z3ASTHandle(NULL, temp_builder.ctx); // Client is responsible for freeing the returned C-string return strdup(result); } @@ -165,12 +235,15 @@ bool Z3SolverImpl::computeInitialValues( bool Z3SolverImpl::internalRunSolver( const Query &query, const std::vector<const Array *> *objects, std::vector<std::vector<unsigned char> > *values, bool &hasSolution) { + TimerStatIncrementer t(stats::queryTime); - // TODO: Does making a new solver for each query have a performance - // impact vs making one global solver and using push and pop? - // TODO: is the "simple_solver" the right solver to use for - // best performance? - Z3_solver theSolver = Z3_mk_simple_solver(builder->ctx); + // NOTE: Z3 will switch to using a slower solver internally if push/pop are + // used so for now it is likely that creating a new solver each time is the + // right way to go until Z3 changes its behaviour. + // + // TODO: Investigate using a custom tactic as described in + // https://github.com/klee/klee/issues/653 + Z3_solver theSolver = Z3_mk_solver(builder->ctx); Z3_solver_inc_ref(builder->ctx, theSolver); Z3_solver_set_params(builder->ctx, theSolver, solverParameters); @@ -197,6 +270,15 @@ bool Z3SolverImpl::internalRunSolver( builder->ctx, theSolver, Z3ASTHandle(Z3_mk_not(builder->ctx, z3QueryExpr), builder->ctx)); + if (dumpedQueriesFile) { + *dumpedQueriesFile << "; start Z3 query\n"; + *dumpedQueriesFile << Z3_solver_to_string(builder->ctx, theSolver); + *dumpedQueriesFile << "(check-sat)\n"; + *dumpedQueriesFile << "(reset)\n"; + *dumpedQueriesFile << "; end Z3 query\n\n"; + dumpedQueriesFile->flush(); + } + ::Z3_lbool satisfiable = Z3_solver_check(builder->ctx, theSolver); runStatusCode = handleSolverResponse(theSolver, satisfiable, objects, values, hasSolution); @@ -271,6 +353,13 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( values->push_back(data); } + // Validate the model if requested + if (Z3ValidateModels) { + bool success = validateZ3Model(theSolver, theModel); + if (!success) + abort(); + } + Z3_model_dec_ref(builder->ctx, theModel); return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; } @@ -280,7 +369,8 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( case Z3_L_UNDEF: { ::Z3_string reason = ::Z3_solver_get_reason_unknown(builder->ctx, theSolver); - if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0) { + if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0 || + strcmp(reason, "(resource limits reached)") == 0) { return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } if (strcmp(reason, "unknown") == 0) { @@ -294,6 +384,54 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( } } +bool Z3SolverImpl::validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel) { + bool success = true; + ::Z3_ast_vector constraints = + Z3_solver_get_assertions(builder->ctx, theSolver); + Z3_ast_vector_inc_ref(builder->ctx, constraints); + + unsigned size = Z3_ast_vector_size(builder->ctx, constraints); + + for (unsigned index = 0; index < size; ++index) { + Z3ASTHandle constraint = Z3ASTHandle( + Z3_ast_vector_get(builder->ctx, constraints, index), builder->ctx); + + ::Z3_ast rawEvaluatedExpr; + bool successfulEval = + Z3_model_eval(builder->ctx, theModel, constraint, + /*model_completion=*/Z3_TRUE, &rawEvaluatedExpr); + assert(successfulEval && "Failed to evaluate model"); + + // Use handle to do ref-counting. + Z3ASTHandle evaluatedExpr(rawEvaluatedExpr, builder->ctx); + + Z3SortHandle sort = + Z3SortHandle(Z3_get_sort(builder->ctx, evaluatedExpr), builder->ctx); + assert(Z3_get_sort_kind(builder->ctx, sort) == Z3_BOOL_SORT && + "Evaluated expression has wrong sort"); + + Z3_lbool evaluatedValue = + Z3_get_bool_value(builder->ctx, evaluatedExpr); + if (evaluatedValue != Z3_L_TRUE) { + llvm::errs() << "Validating model failed:\n" + << "The expression:\n"; + constraint.dump(); + llvm::errs() << "evaluated to \n"; + evaluatedExpr.dump(); + llvm::errs() << "But should be true\n"; + success = false; + } + } + + if (!success) { + llvm::errs() << "Solver state:\n" << Z3_solver_to_string(builder->ctx, theSolver) << "\n"; + llvm::errs() << "Model:\n" << Z3_model_to_string(builder->ctx, theModel) << "\n"; + } + + Z3_ast_vector_dec_ref(builder->ctx, constraints); + return success; +} + SolverImpl::SolverRunStatus Z3SolverImpl::getOperationStatusCode() { return runStatusCode; } diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h new file mode 100644 index 00000000..8dc97e06 --- /dev/null +++ b/lib/Solver/Z3Solver.h @@ -0,0 +1,34 @@ +//===-- Z3Solver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_Z3SOLVER_H +#define KLEE_Z3SOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// Z3Solver - A solver complete solver based on Z3 +class Z3Solver : public Solver { +public: + /// Z3Solver - Construct a new Z3Solver. + Z3Solver(); + + /// Get the query in SMT-LIBv2 format. + /// \return A C-style string. The caller is responsible for freeing this. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_Z3SOLVER_H */ diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt index 4e44fbc6..7145930f 100644 --- a/lib/Support/CMakeLists.txt +++ b/lib/Support/CMakeLists.txt @@ -9,6 +9,7 @@ klee_add_component(kleeSupport CompressionStream.cpp ErrorHandling.cpp + FileHandling.cpp MemoryUsage.cpp PrintVersion.cpp RNG.cpp diff --git a/lib/Support/CompressionStream.cpp b/lib/Support/CompressionStream.cpp index eb208edf..36303878 100644 --- a/lib/Support/CompressionStream.cpp +++ b/lib/Support/CompressionStream.cpp @@ -10,9 +10,11 @@ #include "klee/Config/Version.h" #ifdef HAVE_ZLIB_H #include "klee/Internal/Support/CompressionStream.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#if (LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) \ + && LLVM_VERSION_CODE <= LLVM_VERSION(3, 4)) #include "llvm/Support/system_error.h" #else +#include "llvm/Support/FileSystem.h" #include <fcntl.h> #include <errno.h> #include <sys/types.h> @@ -27,9 +29,13 @@ compressed_fd_ostream::compressed_fd_ostream(const char *Filename, ErrorInfo = ""; #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) // Open file in binary mode +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + std::error_code EC = + llvm::sys::fs::openFileForWrite(Filename, FD, llvm::sys::fs::F_None); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) llvm::error_code EC = llvm::sys::fs::openFileForWrite(Filename, FD, llvm::sys::fs::F_Binary); - +#endif if (EC) { ErrorInfo = EC.message(); FD = -1; diff --git a/lib/Support/ErrorHandling.cpp b/lib/Support/ErrorHandling.cpp index 7ca223e5..00647701 100644 --- a/lib/Support/ErrorHandling.cpp +++ b/lib/Support/ErrorHandling.cpp @@ -10,6 +10,7 @@ #include "klee/Internal/Support/ErrorHandling.h" #include "llvm/ADT/StringRef.h" #include "llvm/Support/raw_ostream.h" +#include "llvm/Support/CommandLine.h" #include <stdlib.h> #include <stdio.h> @@ -20,6 +21,7 @@ #include <set> using namespace klee; +using namespace llvm; FILE *klee::klee_warning_file = NULL; FILE *klee::klee_message_file = NULL; @@ -29,6 +31,13 @@ static const char *warningOncePrefix = "WARNING ONCE"; static const char *errorPrefix = "ERROR"; static const char *notePrefix = "NOTE"; +namespace { +cl::opt<bool> WarningsOnlyToFile( + "warnings-only-to-file", cl::init(false), + cl::desc("All warnings will be written to warnings.txt only. If disabled, " + "they are also written on screen.")); +} + static bool shouldSetColor(const char *pfx, const char *msg, const char *prefixToSearchFor) { if (pfx && strcmp(pfx, prefixToSearchFor) == 0) @@ -139,7 +148,7 @@ void klee::klee_error(const char *msg, ...) { void klee::klee_warning(const char *msg, ...) { va_list ap; va_start(ap, msg); - klee_vmessage(warningPrefix, false, msg, ap); + klee_vmessage(warningPrefix, WarningsOnlyToFile, msg, ap); va_end(ap); } @@ -160,7 +169,7 @@ void klee::klee_warning_once(const void *id, const char *msg, ...) { keys.insert(key); va_list ap; va_start(ap, msg); - klee_vmessage(warningOncePrefix, false, msg, ap); + klee_vmessage(warningOncePrefix, WarningsOnlyToFile, msg, ap); va_end(ap); } } diff --git a/lib/Support/FileHandling.cpp b/lib/Support/FileHandling.cpp new file mode 100644 index 00000000..092a1af0 --- /dev/null +++ b/lib/Support/FileHandling.cpp @@ -0,0 +1,43 @@ +//===-- FileHandling.cpp --------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/Internal/Support/FileHandling.h" +#include "klee/Config/Version.h" +#include "klee/Config/config.h" +#include "klee/Internal/Support/ErrorHandling.h" + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#include "llvm/Support/FileSystem.h" +#endif + +namespace klee { + +llvm::raw_fd_ostream *klee_open_output_file(std::string &path, + std::string &error) { + llvm::raw_fd_ostream *f; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + std::error_code ec; + f = new llvm::raw_fd_ostream(path.c_str(), ec, llvm::sys::fs::F_None); + if (ec) + error = ec.message(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) + f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_None); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 4) + f = new llvm::raw_fd_ostream(path.c_str(), error, llvm::sys::fs::F_Binary); +#else + f = new llvm::raw_fd_ostream(path.c_str(), error, + llvm::raw_fd_ostream::F_Binary); +#endif + if (!error.empty()) { + if (f) + delete f; + f = NULL; + } + return f; +} +} diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt index 1e680e5d..c90cbda0 100644 --- a/runtime/CMakeLists.txt +++ b/runtime/CMakeLists.txt @@ -111,10 +111,17 @@ ExternalProject_Add_Step(BuildKLEERuntimes RuntimeBuild COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all ALWAYS ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" + ${EXTERNAL_PROJECT_ADD_STEP_USES_TERMINAL_ARG} ) -# FIXME: Invoke `make clean` in the bitcode build system -# when the `clean` target is invoked. +# Target for cleaning the bitcode build system +# FIXME: Invoke `make clean` does not invoke this target. It's also weird +# that `ExternalProject` provides no way to do a clean. +add_custom_target(clean_runtime + COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode clean + WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) ############################################################################### # Runtime install diff --git a/runtime/Makefile.cmake.bitcode.rules b/runtime/Makefile.cmake.bitcode.rules index 8261ce99..2737eb80 100644 --- a/runtime/Makefile.cmake.bitcode.rules +++ b/runtime/Makefile.cmake.bitcode.rules @@ -70,8 +70,15 @@ else all:: build_at_level # Compute the directory to find sources -DIR_SUFFIX := $(subst $(RUNTIME_CMAKE_BINARY_DIR),,$(CURRENT_DIR)) +# Note: Use of $(realpath) is to resolve any symlinks +DIR_SUFFIX := $(subst $(realpath $(RUNTIME_CMAKE_BINARY_DIR)),,$(realpath $(CURRENT_DIR))) SRC_DIR := $(abspath $(ROOT_SRC)/$(DIR_SUFFIX)) +# Sanity check +ifeq ($(realpath $(SRC_DIR)),) +$(error SRC_DIR "$(SRC_DIR)" does not exist) +endif + +# Compute the directory to put build files LOCAL_BUILD_DIR := $(abspath $(ROOT_OBJ)/$(DIR_SUFFIX)) C_SRCS := $(shell echo $(SRC_DIR)/*.c) diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c index 24b248e3..6f78c747 100644 --- a/runtime/POSIX/fd.c +++ b/runtime/POSIX/fd.c @@ -37,6 +37,9 @@ int klee_get_errno(void); /* Returns pointer to the symbolic file structure fs the pathname is symbolic */ static exe_disk_file_t *__get_sym_file(const char *pathname) { + if (!pathname) + return NULL; + char c = pathname[0]; unsigned i; diff --git a/runtime/POSIX/stubs.c b/runtime/POSIX/stubs.c index b4f31bf7..bb528ad4 100644 --- a/runtime/POSIX/stubs.c +++ b/runtime/POSIX/stubs.c @@ -240,21 +240,27 @@ int strverscmp (__const char *__s1, __const char *__s2) { return strcmp(__s1, __s2); /* XXX no doubt this is bad */ } -unsigned int gnu_dev_major(unsigned long long int __dev) __attribute__((weak)); -unsigned int gnu_dev_major(unsigned long long int __dev) { +#if __GLIBC_PREREQ(2, 25) +#define gnu_dev_type dev_t +#else +#define gnu_dev_type unsigned long long int +#endif + +unsigned int gnu_dev_major(gnu_dev_type __dev) __attribute__((weak)); +unsigned int gnu_dev_major(gnu_dev_type __dev) { return ((__dev >> 8) & 0xfff) | ((unsigned int) (__dev >> 32) & ~0xfff); } -unsigned int gnu_dev_minor(unsigned long long int __dev) __attribute__((weak)); -unsigned int gnu_dev_minor(unsigned long long int __dev) { +unsigned int gnu_dev_minor(gnu_dev_type __dev) __attribute__((weak)); +unsigned int gnu_dev_minor(gnu_dev_type __dev) { return (__dev & 0xff) | ((unsigned int) (__dev >> 12) & ~0xff); } -unsigned long long int gnu_dev_makedev(unsigned int __major, unsigned int __minor) __attribute__((weak)); -unsigned long long int gnu_dev_makedev(unsigned int __major, unsigned int __minor) { +gnu_dev_type gnu_dev_makedev(unsigned int __major, unsigned int __minor) __attribute__((weak)); +gnu_dev_type gnu_dev_makedev(unsigned int __major, unsigned int __minor) { return ((__minor & 0xff) | ((__major & 0xfff) << 8) - | (((unsigned long long int) (__minor & ~0xff)) << 12) - | (((unsigned long long int) (__major & ~0xfff)) << 32)); + | (((gnu_dev_type) (__minor & ~0xff)) << 12) + | (((gnu_dev_type) (__major & ~0xfff)) << 32)); } char *canonicalize_file_name (const char *name) __attribute__((weak)); diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index a2a46e2a..2e97f38a 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -68,7 +68,7 @@ endif() if (DOWNLOAD_FILECHECK_SOURCE) set(FILECHECK_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/utils/FileCheck/FileCheck.cpp") set(FILECHECK_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/FileCheck.cpp") - if (NOT EXISTS "${FILECHECK_SRC_URL}") + if (NOT EXISTS "${FILECHECK_SRC_FILE}") message(STATUS "Downloading LLVM FileCheck source") file(DOWNLOAD "${FILECHECK_SRC_URL}" "${FILECHECK_SRC_FILE}" SHOW_PROGRESS) endif() @@ -96,7 +96,7 @@ if (DOWNLOAD_NOT_SOURCE) target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) - target_link_libraries("not" PRIVATE ${FILECHECK_NEEDED_LIBS}) + target_link_libraries("not" PRIVATE ${NOT_NEEDED_LIBS}) endif() ############################################################################### diff --git a/test/Concrete/ConstantExpr.ll b/test/Concrete/ConstantExpr.ll index 351223e7..d00c59a6 100644 --- a/test/Concrete/ConstantExpr.ll +++ b/test/Concrete/ConstantExpr.ll @@ -45,13 +45,14 @@ define void @"test_logical_ops"() { call void @print_i32(i32 %t1) call void @print_i32(i32 %t2) call void @print_i32(i32 %t3) + + ; or the address with 1 to ensure the addresses will differ in 'ne' below + %t4 = shl i64 lshr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8 + %t5 = shl i64 ashr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8 + %t6 = lshr i64 shl(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8 - %t4 = shl i32 lshr(i32 ptrtoint(i32* @gInt to i32), i32 8), 8 - %t5 = shl i32 ashr(i32 ptrtoint(i32* @gInt to i32), i32 8), 8 - %t6 = lshr i32 shl(i32 ptrtoint(i32* @gInt to i32), i32 8), 8 - - %t7 = icmp eq i32 %t4, %t5 - %t8 = icmp ne i32 %t4, %t6 + %t7 = icmp eq i64 %t4, %t5 + %t8 = icmp ne i64 %t4, %t6 %t9 = zext i1 %t7 to i8 %t10 = zext i1 %t8 to i8 diff --git a/test/Feature/Alias.c b/test/Feature/Alias.c index 381bcc2a..09abb3e0 100644 --- a/test/Feature/Alias.c +++ b/test/Feature/Alias.c @@ -1,10 +1,9 @@ +// Darwin does not have strong aliases. +// REQUIRES: not-darwin // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc -// Darwin does not have strong aliases. -// XFAIL: darwin - #include <assert.h> // alias for global @@ -17,10 +16,10 @@ extern int foo() __attribute__((alias("__foo"))); int *c = &a; -int main() { +int main() { assert(a == 52); assert(foo() == 52); assert(*c == 52); - + return 0; } diff --git a/test/Feature/LargeReturnTypes.cpp b/test/Feature/LargeReturnTypes.cpp index 937b0758..84119624 100644 --- a/test/Feature/LargeReturnTypes.cpp +++ b/test/Feature/LargeReturnTypes.cpp @@ -1,3 +1,4 @@ +// REQUIRES: not-darwin // RUN: %llvmgxx -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log @@ -9,8 +10,6 @@ // This test currently doesn't work on darwin because this isn't how things work // in libc++. This test should be rewritten to not depend on an external // dependency. -// -// XFAIL: darwin #include <fstream> diff --git a/test/Feature/LinkLLVMLib.c b/test/Feature/LinkLLVMLib.c index 95437094..34931409 100644 --- a/test/Feature/LinkLLVMLib.c +++ b/test/Feature/LinkLLVMLib.c @@ -3,7 +3,7 @@ // // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC // RUN: rm -rf %t.klee-out -// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s +// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors --warnings-only-to-file=false %t2.bc 2>&1 | FileCheck %s #ifdef LINK_LLVM_LIB_TEST_EXEC extern void printint(int d); diff --git a/test/Feature/LongDouble.cpp b/test/Feature/LongDouble.c index 08924293..ad4c1a79 100644 --- a/test/Feature/LongDouble.cpp +++ b/test/Feature/LongDouble.c @@ -1,6 +1,7 @@ -// RUN: %llvmgxx -I../../../include -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s +// RUN: %llvmgcc -g -emit-llvm -O0 -c -o %t.bc %s // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log +// FIXME: When we remove LLVM 2.9 support just use FileCheck and remove these `grep`s. // RUN: grep -q powl\(-11\\.0,0\)=1\\.0\\+ %t.log // RUN: grep -q powl\(-11\\.0,1\)=-11\\.0\\+ %t.log // RUN: grep -q powl\(-11\\.0,2\)=121\\.0\\+ %t.log @@ -8,28 +9,26 @@ // RUN: grep -q 1/-1=-1\\.0\\+ %t.log // RUN: grep -q 1/-2=-0\\.50\\+ %t.log -#include <cstdio> -#include <cstdlib> -#include <cmath> -#include <cassert> - #include "klee/klee.h" +#include <assert.h> +#include <math.h> +#include <stdio.h> +#include <stdlib.h> unsigned klee_urange(unsigned start, unsigned end) { unsigned x; klee_make_symbolic(&x, sizeof x, "x"); - if (x-start>=end-start) klee_silent_exit(0); + if (x - start >= end - start) + klee_silent_exit(0); return x; } -int main(int argc, char ** argv) -{ - - int a = klee_urange(0,3); +int main(int argc, char **argv) { + int a = klee_urange(0, 3); int b; // fork states - switch(a) { + switch (a) { case 0: b = -0; break; @@ -40,7 +39,7 @@ int main(int argc, char ** argv) b = -2; break; default: - assert(false && "Impossible switch target"); + assert(0 && "Impossible switch target"); } // test 80-bit external dispatch @@ -52,7 +51,7 @@ int main(int argc, char ** argv) printf("powl(-11.0,%d)=%Lf\n", a, d); // test 80-bit fdiv - long double e = (long double) 1 / (long double) b; + long double e = (long double)1 / (long double)b; // CHECK-DAG: 1/0=inf // CHECK-DAG: 1/1-1=-1.0 // CHECK-DAG: 1/-2=-0.50 @@ -60,5 +59,3 @@ int main(int argc, char ** argv) return 0; } - - diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index fb9f2c86..ce4bc00f 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -4,17 +4,17 @@ // RUN: %llvmgcc -emit-llvm -DLITTLE_ALLOC -g -c %s -o %t.little.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log 2> %t.little.err +// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log // RUN: not grep -q "MALLOC FAILED" %t.little.log // RUN: not grep -q "DONE" %t.little.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.little.err +// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.big.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log 2> %t.big.err // RUN: not grep -q "MALLOC FAILED" %t.big.log // RUN: not grep -q "DONE" %t.big.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.big.err +// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt #include <stdlib.h> #include <stdio.h> diff --git a/test/Feature/Realloc.c b/test/Feature/Realloc.c index 76016fb7..d0c85b21 100644 --- a/test/Feature/Realloc.c +++ b/test/Feature/Realloc.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --warnings-only-to-file=false %t1.bc 2>&1 | FileCheck %s #include <assert.h> #include <stdlib.h> @@ -13,7 +13,7 @@ int main() { // CHECK: KLEE: WARNING ONCE: Large alloc int *p2 = realloc(p, 1<<30); - assert(p2[1] == 52); + assert(!p2 || p2[1] == 52); return 0; } diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c index 82fbe4f1..a78b784e 100644 --- a/test/Feature/Vararg.c +++ b/test/Feature/Vararg.c @@ -1,3 +1,4 @@ +// REQUIRES: not-darwin // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc > %t2.out diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c index e017b98d..3908b4e2 100644 --- a/test/Runtime/POSIX/DirSeek.c +++ b/test/Runtime/POSIX/DirSeek.c @@ -23,15 +23,13 @@ #include <string.h> int main(int argc, char **argv) { - struct stat s; - char first[256], second[256]; DIR *d = opendir("."); struct dirent *de = readdir(d); assert(de); strcpy(first, de->d_name); off_t pos = telldir(d); - printf("pos: %d\n", telldir(d)); + printf("pos: %ld\n", telldir(d)); de = readdir(d); assert(de); strcpy(second, de->d_name); diff --git a/test/Runtime/POSIX/FD_Fail.c b/test/Runtime/POSIX/FD_Fail.c index 186ada51..2ee1a1a2 100644 --- a/test/Runtime/POSIX/FD_Fail.c +++ b/test/Runtime/POSIX/FD_Fail.c @@ -11,7 +11,7 @@ int main(int argc, char** argv) { char buf[1024]; - FILE* f = fopen("/etc/fstab", "r"); + FILE* f = fopen("/etc/mtab", "r"); assert(f); int r = fread(buf, 1, 100, f); diff --git a/test/lit.cfg b/test/lit.cfg index 31552882..9c557a78 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -1,4 +1,6 @@ # -*- Python -*- +# vim: set filetype=python: +# vim: ts=2:sts=2:sw=2:et:tw=80: # Configuration file for the 'lit' test runner. @@ -8,10 +10,10 @@ import re import platform try: - import lit.util - import lit.formats + import lit.util + import lit.formats except ImportError: - pass + pass # name: The name of this test suite. config.name = 'KLEE' @@ -31,27 +33,33 @@ klee_obj_root = getattr(config, 'klee_obj_root', None) klee_src_root = getattr(config, 'klee_src_root', None) if klee_obj_root is not None: - config.test_exec_root = os.path.join(klee_obj_root, 'test') + config.test_exec_root = os.path.join(klee_obj_root, 'test') # Tweak the PATH to include the tool dir. if klee_obj_root is not None: - klee_tools_dir = getattr(config, 'klee_tools_dir', None) - if not klee_tools_dir: - lit.fatal('No KLEE tools dir set!') + klee_tools_dir = getattr(config, 'klee_tools_dir', None) + if not klee_tools_dir: + lit.fatal('No KLEE tools dir set!') - # Check LLVM tool directory - llvm_tools_dir = getattr(config, 'llvm_tools_dir', None) - if not llvm_tools_dir: - lit.fatal('No LLVM tool directory set!') + # Check LLVM tool directory + llvm_tools_dir = getattr(config, 'llvm_tools_dir', None) + if not llvm_tools_dir: + lit.fatal('No LLVM tool directory set!') - path = os.path.pathsep.join((llvm_tools_dir, klee_tools_dir, config.environment['PATH'] )) - config.environment['PATH'] = path + path = os.path.pathsep.join( + ( + llvm_tools_dir, + klee_tools_dir, + config.environment['PATH'] + ) + ) + config.environment['PATH'] = path # Propogate some environment variable to test environment. def addEnv(name): - if name in os.environ: - config.environment[name] = os.environ[name] + if name in os.environ: + config.environment[name] = os.environ[name] addEnv('HOME') addEnv('PWD') @@ -72,27 +80,37 @@ addEnv('CPLUS_INCLUDE_PATH') # Check that the object root is known. if config.test_exec_root is None: - lit.fatal('test execution root not set!') + lit.fatal('test execution root not set!') # Add substitutions from lit.site.cfg subs = [ 'llvmgcc', 'llvmgxx', 'cc', 'cxx'] for name in subs: - value = getattr(config, name, None) - if value == None: - lit.fatal('{0} is not set'.format(name)) - config.substitutions.append( ('%' + name, value)) + value = getattr(config, name, None) + if value == None: + lit.fatal('{0} is not set'.format(name)) + config.substitutions.append( ('%' + name, value)) # Add a substitution for lli. -config.substitutions.append( ('%lli', os.path.join(llvm_tools_dir, 'lli')) ) +config.substitutions.append( + ('%lli', os.path.join(llvm_tools_dir, 'lli')) +) # Add a substitution for llvm-as -config.substitutions.append( ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as')) ) +config.substitutions.append( + ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as')) +) # Add a substitution for llvm-ar -config.substitutions.append( ('%llvmar', os.path.join(llvm_tools_dir, 'llvm-ar')) ) +config.substitutions.append( + ('%llvmar', os.path.join(llvm_tools_dir, 'llvm-ar')) +) # Add a substition for libkleeruntest -config.substitutions.append( ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) ) -config.substitutions.append( ('%libkleeruntest', config.libkleeruntest) ) +config.substitutions.append( + ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) +) +config.substitutions.append( + ('%libkleeruntest', config.libkleeruntest) +) # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line # e.g. llvm-lit --param klee_opts=--help @@ -106,9 +124,13 @@ else: kleaver_extra_params = lit.params.get('kleaver_opts',"") if len(klee_extra_params) != 0: - print("Passing extra KLEE command line args: {0}".format(klee_extra_params)) + print("Passing extra KLEE command line args: {0}".format( + klee_extra_params) + ) if len(kleaver_extra_params) != 0: - print("Passing extra Kleaver command line args: {0}".format(kleaver_extra_params)) + print("Passing extra Kleaver command line args: {0}".format( + kleaver_extra_params) + ) # Set absolute paths and extra cmdline args for KLEE's tools subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), @@ -116,27 +138,37 @@ subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), ('%ktest-tool', 'ktest-tool', '') ] for s,basename,extra_args in subs: - config.substitutions.append( ( s, - "{0} {1}".format( os.path.join(klee_tools_dir, basename), extra_args ).strip() - ) - ) - -config.substitutions.append( ('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh')) ) + config.substitutions.append( + ( s, + "{0} {1}".format( + os.path.join(klee_tools_dir, basename), + extra_args + ).strip() + ) + ) + +config.substitutions.append( + ('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh')) +) # LLVM < 3.0 doesn't Support %T directive if int(config.llvm_version_major) == 2: - # This is a hack - config.substitutions.append(('%T','Output')) + # This is a hack + config.substitutions.append(('%T','Output')) # Add feature for the LLVM version in use, so it can be tested in REQUIRES and # XFAIL checks. We also add "not-XXX" variants, for the same reason. -known_llvm_versions = set(["2.9", "3.4", "3.5"]) +known_llvm_versions = set(["2.9", "3.4", "3.5", "3.6"]) current_llvm_version = "%s.%s" % (config.llvm_version_major, config.llvm_version_minor) config.available_features.add("llvm-" + current_llvm_version) for version in known_llvm_versions: - if version != current_llvm_version: - config.available_features.add("not-llvm-" + version) + if version != current_llvm_version: + config.available_features.add("not-llvm-" + version) + if current_llvm_version >= version: + config.available_features.add("geq-llvm-" + version) + else: + config.available_features.add("lt-llvm-" + version) # Solver features if config.enable_stp: @@ -151,3 +183,11 @@ else: # POSIX runtime feature if config.enable_posix_runtime: config.available_features.add('posix-runtime') + +# Target operating system features +supported_targets = ['linux', 'darwin'] +for target in supported_targets: + if config.target_triple.find(target) != -1: + config.available_features.add(target) + else: + config.available_features.add('not-{}'.format(target)) diff --git a/test/regression/2016-11-24-bitcast-weak-alias.c b/test/regression/2016-11-24-bitcast-weak-alias.c index f115731b..3e4ebe64 100644 --- a/test/regression/2016-11-24-bitcast-weak-alias.c +++ b/test/regression/2016-11-24-bitcast-weak-alias.c @@ -1,3 +1,4 @@ +// REQUIRES: not-darwin // RUN: %llvmgcc %s -Wall -emit-llvm -g -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: klee --output-dir=%t.klee-out -exit-on-error -search=nurs:covnew %t.bc DUMMY_ARG >%t1.log 2>&1 diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c new file mode 100644 index 00000000..d3bffbe0 --- /dev/null +++ b/test/regression/2017-02-21-pathOS-id.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -write-paths %t.bc 2> %t.log +// RUN: cat %t.klee-out/test000001.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1 +int main(){ + int a, b; + klee_make_symbolic (&a, sizeof(int), "a"); + klee_make_symbolic (&b, sizeof(int), "b"); + klee_assume(a<2); + klee_assume(a>=0); + malloc(a); + if(b){ + b++;//do something + } + return b; +} diff --git a/test/regression/2017-03-23-early-exit-log-stats.c b/test/regression/2017-03-23-early-exit-log-stats.c new file mode 100644 index 00000000..96d3c30f --- /dev/null +++ b/test/regression/2017-03-23-early-exit-log-stats.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// Delay writing instructions so that we ensure on exit that flush happens +// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 %t.bc 2> %t.log +// RUN: FileCheck -check-prefix=CHECK-KLEE -input-file=%t.log %s +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.klee-out/run.stats %s +#include "klee/klee.h" +#include <stdlib.h> +int main(){ + int a; + klee_make_symbolic (&a, sizeof(int), "a"); + if (a) { + // CHECK-KLEE: EXITING ON ERROR + // CHECK-KLEE-NEXT: Error: abort failure + abort(); + } + return 0; +} +// First check we find a line with the expected format +// CHECK-STATS:{{^\('Instructions'}} +// Now check that we eventually get a line where a non zero amount of instructions were executed +// CHECK-STATS:{{^\([ ]*([1-9]|([1-9]+)[0-9])}} diff --git a/tools/klee/Makefile b/tools/klee/Makefile index 8d50403f..2930427c 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -13,7 +13,13 @@ TOOLNAME = klee include $(LEVEL)/Makefile.config USEDLIBS = kleeCore.a kleeBasic.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a -LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine +LINK_COMPONENTS = bitreader bitwriter ipo linker engine + +ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.6)"), True) +LINK_COMPONENTS += mcjit +else +LINK_COMPONENTS += jit +endif ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True) LINK_COMPONENTS += irreader @@ -36,4 +42,4 @@ endif ifeq ($(HAVE_ZLIB),1) LIBS += -lz -endif \ No newline at end of file +endif diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index c65953d1..b74789fa 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -9,18 +9,19 @@ // //===----------------------------------------------------------------------===// +#include "klee/Config/Version.h" #include "klee/ExecutionState.h" #include "klee/Expr.h" -#include "klee/Interpreter.h" -#include "klee/Statistics.h" -#include "klee/Config/Version.h" #include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/TreeStream.h" #include "klee/Internal/Support/Debug.h" +#include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Internal/Support/FileHandling.h" #include "klee/Internal/Support/ModuleUtil.h" -#include "klee/Internal/System/Time.h" #include "klee/Internal/Support/PrintVersion.h" -#include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Internal/System/Time.h" +#include "klee/Interpreter.h" +#include "klee/Statistics.h" #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) #include "llvm/IR/Constants.h" @@ -131,7 +132,7 @@ namespace { cl::desc("Write .sym.path files for each test case")); cl::opt<bool> - ExitOnError("exit-on-error", + OptExitOnError("exit-on-error", cl::desc("Exit if errors occur")); @@ -385,22 +386,14 @@ llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string &filename) { llvm::raw_fd_ostream *f; std::string Error; std::string path = getOutputFilename(filename); -#if LLVM_VERSION_CODE >= LLVM_VERSION(3,5) - f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_None); -#elif LLVM_VERSION_CODE >= LLVM_VERSION(3,4) - f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_Binary); -#else - f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::raw_fd_ostream::F_Binary); -#endif + f = klee_open_output_file(path, Error); if (!Error.empty()) { klee_warning("error opening file \"%s\". KLEE may have run out of file " - "descriptors: try to increase the maximum number of open file " - "descriptors by using ulimit (%s).", - filename.c_str(), Error.c_str()); - delete f; - f = NULL; + "descriptors: try to increase the maximum number of open file " + "descriptors by using ulimit (%s).", + path.c_str(), Error.c_str()); + return NULL; } - return f; } @@ -420,9 +413,9 @@ llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix, void KleeHandler::processTestCase(const ExecutionState &state, const char *errorMessage, const char *errorSuffix) { - if (errorMessage && ExitOnError) { - llvm::errs() << "EXITING ON ERROR:\n" << errorMessage << "\n"; - exit(1); + if (errorMessage && OptExitOnError) { + m_interpreter->prepareForEarlyExit(); + klee_error("EXITING ON ERROR:\n%s\n", errorMessage); } if (!NoOutput) { @@ -1038,9 +1031,14 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) SmallString<128> uclibcBCA(libDir); llvm::sys::path::append(uclibcBCA, KLEE_UCLIBC_BCA_NAME); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + Twine uclibcBCA_twine(uclibcBCA.c_str()); + if (!llvm::sys::fs::exists(uclibcBCA_twine)) +#else bool uclibcExists=false; llvm::sys::fs::exists(uclibcBCA.c_str(), uclibcExists); if (!uclibcExists) +#endif klee_error("Cannot find klee-uclibc : %s", uclibcBCA.c_str()); Function *f; @@ -1265,7 +1263,11 @@ int main(int argc, char **argv, char **envp) { klee_error("error loading program '%s': %s", InputFile.c_str(), Buffer.getError().message().c_str()); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + auto mainModuleOrError = getLazyBitcodeModule(std::move(Buffer.get()), ctx); +#else auto mainModuleOrError = getLazyBitcodeModule(Buffer->get(), ctx); +#endif if (!mainModuleOrError) { klee_error("error loading program '%s': %s", InputFile.c_str(), |