about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml9
-rwxr-xr-x.travis/install-llvm-and-runtime-compiler.sh19
-rwxr-xr-x.travis/install-tcmalloc.sh26
-rwxr-xr-x.travis/klee.sh34
-rwxr-xr-x.travis/solvers.sh9
-rwxr-xr-x.travis/stp.sh63
-rwxr-xr-x.travis/testing-utils.sh15
-rwxr-xr-x.travis/z3.sh20
-rw-r--r--CMakeLists.txt7
-rw-r--r--Dockerfile3
-rw-r--r--README-CMake.md1
-rw-r--r--cmake/find_llvm.cmake2
-rw-r--r--include/klee/CommandLine.h2
-rw-r--r--include/klee/Solver.h6
-rw-r--r--include/klee/util/Assignment.h1
-rw-r--r--lib/Basic/CmdLineOptions.cpp4
-rw-r--r--lib/Basic/ConstructSolverChain.cpp3
-rw-r--r--lib/Expr/Assigment.cpp17
-rw-r--r--lib/Solver/AssignmentValidatingSolver.cpp158
-rw-r--r--lib/Solver/CMakeLists.txt1
-rw-r--r--runtime/CMakeLists.txt11
-rw-r--r--runtime/Makefile.cmake.bitcode.rules9
-rw-r--r--runtime/POSIX/stubs.c22
-rw-r--r--test/lit.cfg106
24 files changed, 442 insertions, 106 deletions
diff --git a/.travis.yml b/.travis.yml
index cd2a9771..3d01b506 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -82,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:
@@ -103,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..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/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..0112ae31 100755
--- a/.travis/stp.sh
+++ b/.travis/stp.sh
@@ -1,46 +1,57 @@
 #!/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
+  # 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
 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..ff55ad23 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.
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/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/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/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/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/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/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/lit.cfg b/test/lit.cfg
index dd2fbc13..8f399642 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,17 +138,23 @@ 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.
@@ -135,8 +163,12 @@ 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:
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-05 21:00:38 +0000