diff options
30 files changed, 381 insertions, 117 deletions
diff --git a/.travis.yml b/.travis.yml index a0b5e7ae..3d01b506 100644 --- a/.travis.yml +++ b/.travis.yml @@ -23,6 +23,7 @@ env: # LLVM : {2.9, 3.4} # SOLVERS : {Z3, STP, STP:Z3, metaSMT} # STP_VERSION : {2.1.2, master} + # METASMT_VERSION : {v4.rc1} # METASMT_DEFAULT : {btor, stp, z3} # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # DISABLE_ASSERTIONS: {0, 1} @@ -43,7 +44,7 @@ env: # Check KLEE CMake build in a few configurations - 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 @@ -64,9 +65,9 @@ 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 + # 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 +82,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: @@ -102,7 +109,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..de6f9bbd 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,13 @@ else export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu llvm-gcc/bin/llvm-gcc test.c -o hello_world ./hello_world + fi +else # OSX + # 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 fi diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh index 5a86380b..a0d825e1 100755 --- a/.travis/install-tcmalloc.sh +++ b/.travis/install-tcmalloc.sh @@ -1,12 +1,19 @@ #!/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 +else # OSX + if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then + echo "Error: Requested to install TCMalloc on macOS, which is not supported" + exit 1 + fi fi diff --git a/.travis/klee.sh b/.travis/klee.sh index 61806df3..a2efc70d 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -10,8 +10,13 @@ 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} + else # OSX + KLEE_CC=/usr/local/bin/clang-${LLVM_VERSION} + KLEE_CXX=/usr/local/bin/clang++-${LLVM_VERSION} + fi else # Just use pre-built llvm-gcc downloaded earlier KLEE_CC=${BUILD_DIR}/llvm-gcc/bin/llvm-gcc @@ -117,6 +122,17 @@ 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" +else # OSX + LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}" + LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)" +fi + +############################################################################### # KLEE ############################################################################### mkdir klee @@ -139,7 +155,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 +176,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 +250,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..9c21d341 100755 --- a/.travis/metaSMT.sh +++ b/.travis/metaSMT.sh @@ -4,14 +4,9 @@ sudo apt-get -y install libboost1.55-dev libz3 libz3-dev libgmp-dev # 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 --depth 1 source ${KLEE_SRC}/.travis/sanitizer_flags.sh if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then @@ -22,7 +17,7 @@ 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 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..412f7613 100755 --- a/.travis/stp.sh +++ b/.travis/stp.sh @@ -1,46 +1,54 @@ #!/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 + else # OSX 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 .. + fi + 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 + CFLAGS="${SANITIZER_C_FLAGS}" \ + CXXFLAGS="${SANITIZER_CXX_FLAGS}" \ + cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF -DNO_BOOST:BOOL=ON ../src - set +e # Do not exit if build fails because we need to display the log - make >> "${STP_LOG}" 2>&1 + 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..29295be2 100755 --- a/.travis/testing-utils.sh +++ b/.travis/testing-utils.sh @@ -18,11 +18,16 @@ 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 + else # OSX + sudo cp lib* /usr/local/lib/ + sudo cp -r include/gtest /usr/local/include + 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 +50,3 @@ else cd "${old_dir}" fi - diff --git a/.travis/z3.sh b/.travis/z3.sh new file mode 100755 index 00000000..f8ae6e0b --- /dev/null +++ b/.travis/z3.sh @@ -0,0 +1,17 @@ +#!/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 +else # OSX + brew install z3 +fi 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/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..32c8cf9e 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -268,6 +268,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 95812dd7..1930cdc3 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3835,6 +3835,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/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/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/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/test/CMakeLists.txt b/test/CMakeLists.txt index a2a46e2a..4b6a63f6 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -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/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/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..dd2fbc13 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -151,3 +151,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-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/main.cpp b/tools/klee/main.cpp index c65953d1..1ac33617 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -421,8 +421,8 @@ 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); + m_interpreter->prepareForEarlyExit(); + klee_error("EXITING ON ERROR:\n%s\n", errorMessage); } if (!NoOutput) { |