about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--NEWS24
-rw-r--r--autoconf/configure.ac2
-rwxr-xr-xconfigure18
-rw-r--r--include/klee/Expr.h4
-rw-r--r--include/klee/Interpreter.h2
-rw-r--r--lib/Basic/CmdLineOptions.cpp4
-rw-r--r--lib/Core/Executor.cpp19
-rw-r--r--lib/Core/Executor.h12
-rw-r--r--lib/Expr/ExprPPrinter.cpp22
-rw-r--r--lib/Module/PhiCleaner.cpp20
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp310
-rw-r--r--lib/Solver/QueryLoggingSolver.h105
-rw-r--r--runtime/Runtest/Makefile42
-rw-r--r--test/Coverage/ReplayOutDir.c2
-rw-r--r--test/regression/2016-04-14-sdiv-2.c_25
-rw-r--r--tools/klee/main.cpp68
16 files changed, 390 insertions, 289 deletions
diff --git a/NEWS b/NEWS
index 8c1699e5..17d62a3a 100644
--- a/NEWS
+++ b/NEWS
@@ -1,3 +1,27 @@
+KLEE 1.2.0, 31 March 2016
+=========================
+
+* Added native support for Z3 (@delcypher)
+* Made it possible to build KLEE without using STP and only MetaSMT (@delcypher)
+* Added support for tcmalloc, which allows KLEE to better track memory consumption (@MartinNowack)
+* Added support for lowering the ``llvm.objectsize`` intrinsic (@delcypher)
+* Added soname for Runtest dynamic library (@MartinNowack)
+* Added support to load libraries from command line (@omeranson)
+* Added command line flag --silent-klee-assume to suppress errors due to infeasible assumptions (Valentin Wüstholz, @wuestholz)
+* Changed code to print out arrays deterministically (@MartinNowack)
+* Improved klee-clang script (@msoos)
+* Added code to dump queries and assignments (@MartinNowack)
+* Code cleanup and refactorings (@delcypher, @MartinNowack)
+* Improvements to code infrastructure (@delcypher, @domainexpert, @MartinNowack, @mdimjasevic, @msoos)
+* Fixed several memory leaks (@delcypher)
+* Fixed a bug with how non-power of 2 values were written to memory (@kren1)
+* Fixed valueIsOnlyCalled() used by MD2U (@yotann)
+* Fixed SELinux signatures (@lszekeres)
+* Fixed incorrect position of Not in Expr::Kind (@delcypher)
+* Fixed wrong std::vector usage after reserve() call (@pollnossa)
+* Improved documentation (@bananaappletw, @ccadar, @delcypher, @mdimjasevic, @Teemperor, @ward, @wuestholz)
+
+
 KLEE 1.1.0, 13 November 2015
 ============================
 
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 01c2c809..2be02321 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -1,7 +1,7 @@
 dnl **************************************************************************
 dnl * Initialize
 dnl **************************************************************************
-AC_INIT([[KLEE]],[[1.1.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]])
+AC_INIT([[KLEE]],[[1.2.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]])
 
 dnl Identify where LLVM source tree is (this is patched by
 dnl AutoRegen.sh)
diff --git a/configure b/configure
index ee5593d2..33893680 100755
--- a/configure
+++ b/configure
@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for KLEE 1.1.0.
+# Generated by GNU Autoconf 2.69 for KLEE 1.2.0.
 #
 # Report bugs to <klee-dev@imperial.ac.uk>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='KLEE'
 PACKAGE_TARNAME='klee-'
-PACKAGE_VERSION='1.1.0'
-PACKAGE_STRING='KLEE 1.1.0'
+PACKAGE_VERSION='1.2.0'
+PACKAGE_STRING='KLEE 1.2.0'
 PACKAGE_BUGREPORT='klee-dev@imperial.ac.uk'
 PACKAGE_URL='https://klee.github.io'
 
@@ -1293,7 +1293,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures KLEE 1.1.0 to adapt to many kinds of systems.
+\`configure' configures KLEE 1.2.0 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1359,7 +1359,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of KLEE 1.1.0:";;
+     short | recursive ) echo "Configuration of KLEE 1.2.0:";;
    esac
   cat <<\_ACEOF
 
@@ -1474,7 +1474,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-KLEE configure 1.1.0
+KLEE configure 1.2.0
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -2055,7 +2055,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by KLEE $as_me 1.1.0, which was
+It was created by KLEE $as_me 1.2.0, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -5934,7 +5934,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by KLEE $as_me 1.1.0, which was
+This file was extended by KLEE $as_me 1.2.0, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -6001,7 +6001,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-KLEE config.status 1.1.0
+KLEE config.status 1.2.0
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 9ad1b49a..d70cfdc9 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -128,6 +128,9 @@ public:
     ZExt,
     SExt,
 
+    // Bit
+    Not,
+
     // All subsequent kinds are binary.
 
     // Arithmetic
@@ -140,7 +143,6 @@ public:
     SRem,
 
     // Bit
-    Not,
     And,
     Or,
     Xor,
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index abd454b1..b40ad0d5 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -113,7 +113,7 @@ public:
 
   // supply a test case to replay from. this can be used to drive the
   // interpretation down a user specified path. use null to reset.
-  virtual void setReplayOut(const struct KTest *out) = 0;
+  virtual void setReplayKTest(const struct KTest *out) = 0;
 
   // supply a list of branch decisions specifying which direction to
   // take on forks. this can be used to drive the interpretation down
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 1724ea06..a0fbda03 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -61,8 +61,8 @@ UseForkedCoreSolver("use-forked-solver",
 
 llvm::cl::opt<bool>
 CoreSolverOptimizeDivides("solver-optimize-divides", 
-                 llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"),
-                 llvm::cl::init(true));
+                 llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=off)"),
+                 llvm::cl::init(false));
 
 
 /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index dc9edf5f..3b2a860e 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -282,7 +282,7 @@ Executor::Executor(const InterpreterOptions &opts,
     symPathWriter(0),
     specialFunctionHandler(0),
     processTree(0),
-    replayOut(0),
+    replayKTest(0),
     replayPath(0),    
     usingSeeds(0),
     atMemoryLimit(false),
@@ -736,7 +736,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
         }
       }
     } else if (res==Solver::Unknown) {
-      assert(!replayOut && "in replay mode, only one branch can be true.");
+      assert(!replayKTest && "in replay mode, only one branch can be true.");
       
       if ((MaxMemoryInhibit && atMemoryLimit) || 
           current.forkDisabled ||
@@ -1926,8 +1926,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       count = Expr::createZExtToPointerWidth(count);
       size = MulExpr::create(size, count);
     }
-    bool isLocal = i->getOpcode()==Instruction::Alloca;
-    executeAlloc(state, size, isLocal, ki);
+    executeAlloc(state, size, true, ki);
     break;
   }
 
@@ -2652,8 +2651,8 @@ std::string Executor::getAddressInfo(ExecutionState &state,
 }
 
 void Executor::terminateState(ExecutionState &state) {
-  if (replayOut && replayPosition!=replayOut->numObjects) {
-    klee_warning_once(replayOut, 
+  if (replayKTest && replayPosition!=replayKTest->numObjects) {
+    klee_warning_once(replayKTest,
                       "replay did not consume all objects in test input.");
   }
 
@@ -2875,7 +2874,7 @@ void Executor::callExternalFunction(ExecutionState &state,
 ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, 
                                             ref<Expr> e) {
   unsigned n = interpreterOpts.MakeConcreteSymbolic;
-  if (!n || replayOut || replayPath)
+  if (!n || replayKTest || replayPath)
     return e;
 
   // right now, we don't replace symbolics (is there any reason to?)
@@ -3221,7 +3220,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
                                    const MemoryObject *mo,
                                    const std::string &name) {
   // Create a new object state for the memory object (instead of a copy).
-  if (!replayOut) {
+  if (!replayKTest) {
     // Find a unique name for this array.  First try the original name,
     // or if that fails try adding a unique identifier.
     unsigned id = 0;
@@ -3281,10 +3280,10 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     }
   } else {
     ObjectState *os = bindObjectInState(state, mo, false);
-    if (replayPosition >= replayOut->numObjects) {
+    if (replayPosition >= replayKTest->numObjects) {
       terminateStateOnError(state, "replay count mismatch", "user.err");
     } else {
-      KTestObject *obj = &replayOut->objects[replayPosition++];
+      KTestObject *obj = &replayKTest->objects[replayPosition++];
       if (obj->numBytes != mo->size) {
         terminateStateOnError(state, "replay size mismatch", "user.err");
       } else {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 8bfa278a..1997bad2 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -150,10 +150,10 @@ private:
 
   /// When non-null the bindings that will be used for calls to
   /// klee_make_symbolic in order replay.
-  const struct KTest *replayOut;
+  const struct KTest *replayKTest;
   /// When non-null a list of branch decisions to be used for replay.
   const std::vector<bool> *replayPath;
-  /// The index into the current \ref replayOut or \ref replayPath
+  /// The index into the current \ref replayKTest or \ref replayPath
   /// object.
   unsigned replayPosition;
 
@@ -417,16 +417,16 @@ public:
   }
   virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) {
     symPathWriter = tsw;
-  }      
+  }
 
-  virtual void setReplayOut(const struct KTest *out) {
+  virtual void setReplayKTest(const struct KTest *out) {
     assert(!replayPath && "cannot replay both buffer and path");
-    replayOut = out;
+    replayKTest = out;
     replayPosition = 0;
   }
 
   virtual void setReplayPath(const std::vector<bool> *path) {
-    assert(!replayOut && "cannot replay both buffer and path");
+    assert(!replayKTest && "cannot replay both buffer and path");
     replayPath = path;
     replayPosition = 0;
   }
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index ddcc57a1..1682d9b5 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -457,6 +457,14 @@ void ExprPPrinter::printConstraints(llvm::raw_ostream &os,
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
+namespace {
+
+struct ArrayPtrsByName {
+  bool operator()(const Array *a1, const Array *a2) const {
+    return a1->name < a2->name;
+  }
+};
+}
 
 void ExprPPrinter::printQuery(llvm::raw_ostream &os,
                               const ConstraintManager &constraints,
@@ -482,13 +490,15 @@ void ExprPPrinter::printQuery(llvm::raw_ostream &os,
   if (printArrayDecls) {
     for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it)
       p.usedArrays.insert(*it);
-    for (std::set<const Array*>::iterator it = p.usedArrays.begin(), 
-           ie = p.usedArrays.end(); it != ie; ++it) {
+    std::vector<const Array *> sortedArray(p.usedArrays.begin(),
+                                           p.usedArrays.end());
+    std::sort(sortedArray.begin(), sortedArray.end(), ArrayPtrsByName());
+    for (std::vector<const Array *>::iterator it = sortedArray.begin(),
+                                              ie = sortedArray.end();
+         it != ie; ++it) {
       const Array *A = *it;
-      // FIXME: Print correct name, domain, and range.
-      PC << "array " << A->name
-         << "[" << A->size << "]"
-         << " : " << "w32" << " -> " << "w8" << " = ";
+      PC << "array " << A->name << "[" << A->size << "]"
+         << " : w" << A->domain << " -> w" << A->range << " = ";
       if (A->isSymbolicArray()) {
         PC << "symbolic";
       } else {
diff --git a/lib/Module/PhiCleaner.cpp b/lib/Module/PhiCleaner.cpp
index 3d8d7867..2cf3ba4a 100644
--- a/lib/Module/PhiCleaner.cpp
+++ b/lib/Module/PhiCleaner.cpp
@@ -39,16 +39,16 @@ bool klee::PhiCleanerPass::runOnFunction(Function &f) {
           if (pi->getIncomingBlock(i) != reference->getIncomingBlock(i))
             break;
 
-        if (i!=numBlocks) {
-          std::vector<Value*> values;
-          values.reserve(numBlocks);
-          for (unsigned i=0; i<numBlocks; i++)
-            values[i] = pi->getIncomingValueForBlock(reference->getIncomingBlock(i));
-          for (unsigned i=0; i<numBlocks; i++) {
-            pi->setIncomingBlock(i, reference->getIncomingBlock(i));
-            pi->setIncomingValue(i, values[i]);
-          }
-          changed = true;
+        if (i != numBlocks) {
+            std::vector<Value*> values;
+            values.reserve(numBlocks);
+            for (unsigned i = 0; i<numBlocks; i++)
+                values.push_back(pi->getIncomingValueForBlock(reference->getIncomingBlock(i)));
+            for (unsigned i = 0; i<numBlocks; i++) {
+                pi->setIncomingBlock(i, reference->getIncomingBlock(i));
+                pi->setIncomingValue(i, values[i]);
+            }
+            changed = true;
         }
 
         // see if it uses any previously defined phi nodes
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 5484a319..f93bec3c 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -1,13 +1,4 @@
 //===-- QueryLoggingSolver.cpp --------------------------------------------===//
-
-#include "QueryLoggingSolver.h"
-#include "klee/Internal/System/Time.h"
-#include "klee/Statistics.h"
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-#include "llvm/Support/FileSystem.h"
-#endif
-
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -15,188 +6,203 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
+#include "QueryLoggingSolver.h"
+#include "klee/Internal/System/Time.h"
+#include "klee/Statistics.h"
+
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+#include "llvm/Support/FileSystem.h"
+#endif
 
 using namespace klee::util;
 
-QueryLoggingSolver::QueryLoggingSolver(Solver *_solver,
-                                       std::string path,
-                                       const std::string& commentSign,
-                                       int queryTimeToLog)                                  
+namespace {
+llvm::cl::opt<bool> DumpPartialQueryiesEarly(
+    "log-partial-queries-early", llvm::cl::init(false),
+    llvm::cl::desc("Log queries before calling the solver (default=off)"));
+}
+
+QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
+                                       const std::string &commentSign,
+                                       int queryTimeToLog)
     : solver(_solver),
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
       os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text),
 #else
       os(path.c_str(), ErrorInfo),
 #endif
-      BufferString(""),
-      logBuffer(BufferString),
-      queryCount(0),    
-      minQueryTimeToLog(queryTimeToLog),
-      startTime(0.0f),
-      lastQueryTime(0.0f),
+      BufferString(""), logBuffer(BufferString), queryCount(0),
+      minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f),
       queryCommentSign(commentSign) {
-    assert(0 != solver);
+  assert(0 != solver);
 }
 
-QueryLoggingSolver::~QueryLoggingSolver() {
-    delete solver;
+QueryLoggingSolver::~QueryLoggingSolver() { delete solver; }
+
+void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) {
+  logBuffer.flush();
+  if (writeToFile) {
+    os << logBuffer.str();
+    os.flush();
+  }
+  // prepare the buffer for reuse
+  BufferString = "";
 }
 
-void QueryLoggingSolver::startQuery(const Query& query, const char* typeName,
-                                    const Query* falseQuery,
-                                    const std::vector<const Array*> *objects) {
-    Statistic *S = theStatisticManager->getStatisticByName("Instructions");
-    uint64_t instructions = S ? S->getValue() : 0;
-
-    logBuffer << queryCommentSign << " Query " << queryCount++ << " -- "
-              << "Type: " << typeName << ", "
-              << "Instructions: " << instructions << "\n";
-    
-    printQuery(query, falseQuery, objects);
-    
-    startTime = getWallTime();
-    
+void QueryLoggingSolver::startQuery(const Query &query, const char *typeName,
+                                    const Query *falseQuery,
+                                    const std::vector<const Array *> *objects) {
+  Statistic *S = theStatisticManager->getStatisticByName("Instructions");
+  uint64_t instructions = S ? S->getValue() : 0;
+
+  logBuffer << queryCommentSign << " Query " << queryCount++ << " -- "
+            << "Type: " << typeName << ", "
+            << "Instructions: " << instructions << "\n";
+
+  printQuery(query, falseQuery, objects);
+
+  if (DumpPartialQueryiesEarly) {
+    flushBufferConditionally(true);
+  }
+  startTime = getWallTime();
 }
 
 void QueryLoggingSolver::finishQuery(bool success) {
-    lastQueryTime = getWallTime() - startTime;
-    logBuffer << queryCommentSign << "   " << (success ? "OK" : "FAIL") << " -- "
-              << "Elapsed: " << lastQueryTime << "\n";
-    
-    if (false == success) {
-        logBuffer << queryCommentSign << "   Failure reason: "
-                  << SolverImpl::getOperationStatusString(solver->impl->getOperationStatusCode())
-                  << "\n";
-    }
+  lastQueryTime = getWallTime() - startTime;
+  logBuffer << queryCommentSign << "   " << (success ? "OK" : "FAIL") << " -- "
+            << "Elapsed: " << lastQueryTime << "\n";
+
+  if (false == success) {
+    logBuffer << queryCommentSign << "   Failure reason: "
+              << SolverImpl::getOperationStatusString(
+                     solver->impl->getOperationStatusCode()) << "\n";
+  }
 }
 
 void QueryLoggingSolver::flushBuffer() {
-    logBuffer.flush();            
-
-      if ((0 == minQueryTimeToLog) ||
-          (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) {
-          // we either do not limit logging queries or the query time
-          // is larger than threshold (in ms)
-          
-          if ((minQueryTimeToLog >= 0) || 
-              (SOLVER_RUN_STATUS_TIMEOUT == (solver->impl->getOperationStatusCode()))) {
-              // we do additional check here to log only timeouts in case
-              // user specified negative value for minQueryTimeToLog param
-              os << logBuffer.str();              
-              os.flush();
-          }                    
-      }
-      
-      // prepare the buffer for reuse
-      BufferString = "";
+  bool writeToFile = false;
+
+  if ((0 == minQueryTimeToLog) ||
+      (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) {
+    // we either do not limit logging queries or the query time
+    // is larger than threshold (in ms)
+
+    if ((minQueryTimeToLog >= 0) ||
+        (SOLVER_RUN_STATUS_TIMEOUT ==
+         (solver->impl->getOperationStatusCode()))) {
+      // we do additional check here to log only timeouts in case
+      // user specified negative value for minQueryTimeToLog param
+      writeToFile = true;
+    }
+  }
+
+  flushBufferConditionally(writeToFile);
 }
 
-bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) {
-    startQuery(query, "Truth");
-    
-    bool success = solver->impl->computeTruth(query, isValid);
-    
-    finishQuery(success);
-    
-    if (success) {
-        logBuffer << queryCommentSign << "   Is Valid: " 
-                  << (isValid ? "true" : "false") << "\n";
-    }
-    logBuffer << "\n";
-    
-    flushBuffer();
-    
-    return success;    
+bool QueryLoggingSolver::computeTruth(const Query &query, bool &isValid) {
+  startQuery(query, "Truth");
+
+  bool success = solver->impl->computeTruth(query, isValid);
+
+  finishQuery(success);
+
+  if (success) {
+    logBuffer << queryCommentSign
+              << "   Is Valid: " << (isValid ? "true" : "false") << "\n";
+  }
+  logBuffer << "\n";
+
+  flushBuffer();
+
+  return success;
 }
 
-bool QueryLoggingSolver::computeValidity(const Query& query,
-                                         Solver::Validity& result) {
-    startQuery(query, "Validity");
-    
-    bool success = solver->impl->computeValidity(query, result);
-    
-    finishQuery(success);
-    
-    if (success) {
-        logBuffer << queryCommentSign << "   Validity: " 
-                  << result << "\n";
-    }
-    logBuffer << "\n";
-    
-    flushBuffer();
-    
-    return success;
+bool QueryLoggingSolver::computeValidity(const Query &query,
+                                         Solver::Validity &result) {
+  startQuery(query, "Validity");
+
+  bool success = solver->impl->computeValidity(query, result);
+
+  finishQuery(success);
+
+  if (success) {
+    logBuffer << queryCommentSign << "   Validity: " << result << "\n";
+  }
+  logBuffer << "\n";
+
+  flushBuffer();
+
+  return success;
 }
 
-bool QueryLoggingSolver::computeValue(const Query& query, ref<Expr>& result) {
-    Query withFalse = query.withFalse();
-    startQuery(query, "Value", &withFalse);
+bool QueryLoggingSolver::computeValue(const Query &query, ref<Expr> &result) {
+  Query withFalse = query.withFalse();
+  startQuery(query, "Value", &withFalse);
 
-    bool success = solver->impl->computeValue(query, result);
-    
-    finishQuery(success);
-    
-    if (success) {
-        logBuffer << queryCommentSign << "   Result: " << result << "\n";
-    }
-    logBuffer << "\n";
-    
-    flushBuffer();
-    
-    return success;
+  bool success = solver->impl->computeValue(query, result);
+
+  finishQuery(success);
+
+  if (success) {
+    logBuffer << queryCommentSign << "   Result: " << result << "\n";
+  }
+  logBuffer << "\n";
+
+  flushBuffer();
+
+  return success;
 }
 
-bool QueryLoggingSolver::computeInitialValues(const Query& query,
-                                              const std::vector<const Array*>& objects,
-                                              std::vector<std::vector<unsigned char> >& values,
-                                              bool& hasSolution) {
-    startQuery(query, "InitialValues", 0, &objects);
-
-    bool success = solver->impl->computeInitialValues(query, objects, 
-                                                      values, hasSolution);
-    
-    finishQuery(success);
-    
-    if (success) {
-        logBuffer << queryCommentSign << "   Solvable: " 
-                  << (hasSolution ? "true" : "false") << "\n";
-        if (hasSolution) {
-            std::vector< std::vector<unsigned char> >::iterator
-            values_it = values.begin();
-        
-            for (std::vector<const Array*>::const_iterator i = objects.begin(),
-                 e = objects.end(); i != e; ++i, ++values_it) {
-                const Array *array = *i;
-                std::vector<unsigned char> &data = *values_it;
-                logBuffer << queryCommentSign << "     " << array->name << " = [";
-                
-                for (unsigned j = 0; j < array->size; j++) {
-                    logBuffer << (int) data[j];
-            
-                    if (j+1 < array->size) {
-                        logBuffer << ",";
-                    }                    
-              }
-              logBuffer << "]\n";
-            }
+bool QueryLoggingSolver::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+  startQuery(query, "InitialValues", 0, &objects);
+
+  bool success =
+      solver->impl->computeInitialValues(query, objects, values, hasSolution);
+
+  finishQuery(success);
+
+  if (success) {
+    logBuffer << queryCommentSign
+              << "   Solvable: " << (hasSolution ? "true" : "false") << "\n";
+    if (hasSolution) {
+      std::vector<std::vector<unsigned char> >::iterator values_it =
+          values.begin();
+
+      for (std::vector<const Array *>::const_iterator i = objects.begin(),
+                                                      e = objects.end();
+           i != e; ++i, ++values_it) {
+        const Array *array = *i;
+        std::vector<unsigned char> &data = *values_it;
+        logBuffer << queryCommentSign << "     " << array->name << " = [";
+
+        for (unsigned j = 0; j < array->size; j++) {
+          logBuffer << (int)data[j];
+
+          if (j + 1 < array->size) {
+            logBuffer << ",";
+          }
         }
+        logBuffer << "]\n";
+      }
     }
-    logBuffer << "\n";
-    
-    flushBuffer();
-    
-    return success;
+  }
+  logBuffer << "\n";
+
+  flushBuffer();
+
+  return success;
 }
 
 SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() {
-    return solver->impl->getOperationStatusCode();
+  return solver->impl->getOperationStatusCode();
 }
 
-char *QueryLoggingSolver::getConstraintLog(const Query& query) {
+char *QueryLoggingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
 void QueryLoggingSolver::setCoreSolverTimeout(double timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
-
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index ad1722ca..bb266c67 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -1,4 +1,5 @@
-//===-- QueryLoggingSolver.h ---------------------------------------------------===//
+//===-- QueryLoggingSolver.h
+//---------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -8,75 +9,71 @@
 //===----------------------------------------------------------------------===//
 
 #ifndef KLEE_QUERYLOGGINGSOLVER_H
-#define	KLEE_QUERYLOGGINGSOLVER_H
+#define KLEE_QUERYLOGGINGSOLVER_H
 
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
 #include "llvm/Support/raw_ostream.h"
-#include <fstream>
-#include <sstream>
 
 using namespace klee;
 
-/// This abstract class represents a solver that is capable of logging 
+/// This abstract class represents a solver that is capable of logging
 /// queries to a file.
 /// Derived classes might specialize this one by providing different formats
 /// for the query output.
 class QueryLoggingSolver : public SolverImpl {
 
 protected:
-    Solver *solver;
-    std::string ErrorInfo;
-    llvm::raw_fd_ostream os;
-    // @brief Buffer used by logBuffer
-    std::string BufferString;
-    // @brief buffer to store logs before flushing to file
-    llvm::raw_string_ostream logBuffer;
-    unsigned queryCount;
-    int minQueryTimeToLog; // we log to file only those queries
-                           // which take longer than the specified time (ms);
-                           // if this param is negative, log only those queries
-                           // on which the solver has timed out
+  Solver *solver;
+  std::string ErrorInfo;
+  llvm::raw_fd_ostream os;
+  // @brief Buffer used by logBuffer
+  std::string BufferString;
+  // @brief buffer to store logs before flushing to file
+  llvm::raw_string_ostream logBuffer;
+  unsigned queryCount;
+  int minQueryTimeToLog; // we log to file only those queries
+                         // which take longer than the specified time (ms);
+                         // if this param is negative, log only those queries
+                         // on which the solver has timed out
 
-    double startTime;
-    double lastQueryTime;
-    const std::string queryCommentSign; // sign representing commented lines
-                                        // in given a query format
+  double startTime;
+  double lastQueryTime;
+  const std::string queryCommentSign; // sign representing commented lines
+                                      // in given a query format
+
+  virtual void startQuery(const Query &query, const char *typeName,
+                          const Query *falseQuery = 0,
+                          const std::vector<const Array *> *objects = 0);
+
+  virtual void finishQuery(bool success);
+
+  /// flushBuffer - flushes the temporary logs buffer. Depending on threshold
+  /// settings, contents of the buffer are either discarded or written to a
+  /// file.
+  void flushBuffer(void);
+
+  virtual void printQuery(const Query &query, const Query *falseQuery = 0,
+                          const std::vector<const Array *> *objects = 0) = 0;
+  void flushBufferConditionally(bool writeToFile);
 
-    virtual void startQuery(const Query& query, const char* typeName,
-                            const Query* falseQuery = 0,
-                            const std::vector<const Array*>* objects = 0);
-           
-    virtual void finishQuery(bool success);        
-  
-    /// flushBuffer - flushes the temporary logs buffer. Depending on threshold
-    /// settings, contents of the buffer are either discarded or written to a file.  
-    void flushBuffer(void);
-    
-    virtual void printQuery(const Query& query,
-                            const Query* falseQuery = 0,
-                            const std::vector<const Array*>* objects = 0) = 0;
-  
 public:
-    QueryLoggingSolver(Solver *_solver,
-                       std::string path,
-                       const std::string& commentSign,
-                       int queryTimeToLog);
-  
-    virtual ~QueryLoggingSolver();
+  QueryLoggingSolver(Solver *_solver, std::string path,
+                     const std::string &commentSign, int queryTimeToLog);
 
-    /// implementation of the SolverImpl interface
-    bool computeTruth(const Query& query, bool &isValid);
-    bool computeValidity(const Query& query, Solver::Validity &result);
-    bool computeValue(const Query& query, ref<Expr> &result);
-    bool computeInitialValues(const Query& 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);
-};
+  virtual ~QueryLoggingSolver();
 
-#endif	/* KLEE_QUERYLOGGINGSOLVER_H */
+  /// implementation of the SolverImpl interface
+  bool computeTruth(const Query &query, bool &isValid);
+  bool computeValidity(const Query &query, Solver::Validity &result);
+  bool computeValue(const Query &query, ref<Expr> &result);
+  bool computeInitialValues(const Query &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);
+};
 
+#endif /* KLEE_QUERYLOGGINGSOLVER_H */
diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile
index dd21c4a9..666fe06d 100644
--- a/runtime/Runtest/Makefile
+++ b/runtime/Runtest/Makefile
@@ -15,5 +15,47 @@ SHARED_LIBRARY=1
 LINK_LIBS_IN_SHARED = 1
 DONT_BUILD_RELINKED = 1
 NO_PEDANTIC=1
+# Increment version appropriately if ABI/API changes, more details:
+# http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html#AEN135
+SHARED_VERSION=1.0
 
 include $(LEVEL)/Makefile.common
+
+#LDFLAGS += -Wl,-soname,lib$(LIBRARYNAME)$(SHLIBEXT)
+ifeq ($(HOST_OS),Darwin)
+    # set dylib internal version number to llvmCore submission number
+    ifdef LLVM_SUBMIT_VERSION
+        LLVMLibsOptions := $(LLVMLibsOptions) -Wl,-current_version \
+                        -Wl,$(SHARED_VERSION) \
+                        -Wl,-compatibility_version -Wl,1
+    endif
+    # Include everything from the .a's into the shared library.
+    LLVMLibsOptions    := $(LLVMLibsOptions) -all_load
+    # extra options to override libtool defaults
+    LLVMLibsOptions    := $(LLVMLibsOptions)  \
+                         -Wl,-dead_strip
+
+    # Mac OS X 10.4 and earlier tools do not allow a second -install_name on command line
+    DARWIN_VERS := $(shell echo $(TARGET_TRIPLE) | sed 's/.*darwin\([0-9]*\).*/\1/')
+    ifneq ($(DARWIN_VERS),8)
+       LLVMLibsOptions    := $(LLVMLibsOptions)  \
+                            -Wl,-install_name \
+                            -Wl,"@rpath/lib$(LIBRARYNAME)$(SHLIBEXT)"
+    endif
+endif
+
+ifeq ($(HOST_OS), $(filter $(HOST_OS), DragonFly Linux FreeBSD GNU/kFreeBSD OpenBSD GNU Bitrig))
+    # Include everything from the .a's into the shared library.
+    LLVMLibsOptions := -Wl,--whole-archive $(LLVMLibsOptions) \
+                       -Wl,--no-whole-archive
+endif
+
+ifeq ($(HOST_OS), $(filter $(HOST_OS), DragonFly Linux FreeBSD GNU/kFreeBSD GNU))
+    # Add soname to the library.
+    LLVMLibsOptions += -Wl,--soname,lib$(LIBRARYNAME)$(SHLIBEXT).$(SHARED_VERSION)
+endif
+
+ifeq ($(HOST_OS), $(filter $(HOST_OS), Linux GNU GNU/kFreeBSD))
+    # Don't allow unresolved symbols.
+    LLVMLibsOptions += -Wl,--no-undefined
+endif
diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c
index ca7e590a..d9bffea0 100644
--- a/test/Coverage/ReplayOutDir.c
+++ b/test/Coverage/ReplayOutDir.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: rm -rf %t1.out %t1.replay
 // RUN: %klee --output-dir=%t1.out %t1.bc
-// RUN: %klee --output-dir=%t1.replay --replay-out-dir=%t1.out %t1.bc
+// RUN: %klee --output-dir=%t1.replay --replay-ktest-dir=%t1.out %t1.bc
 
 int main() {
   int i;
diff --git a/test/regression/2016-04-14-sdiv-2.c_ b/test/regression/2016-04-14-sdiv-2.c_
new file mode 100644
index 00000000..88a5fca3
--- /dev/null
+++ b/test/regression/2016-04-14-sdiv-2.c_
@@ -0,0 +1,25 @@
+// XFAIL: *
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc >%t1.log
+// RUN: grep "m is 2" %t1.log
+
+#include <assert.h>
+
+int main(void)
+{
+  int n, m;
+  klee_make_symbolic(&n, sizeof n, "n");
+  klee_assume(n < -1);
+
+  if (n/2 > 0)
+    assert(0);
+
+  klee_make_symbolic(&m, sizeof m, "m");
+  klee_assume(m > 0);
+
+  if (m/2 == 2)
+    printf("m is 2\n");
+  
+  return 0;
+} 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 568c70bb..80161caa 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -179,14 +179,14 @@ namespace {
                               "the bytes, not necessarily making them concrete."));
 
   cl::list<std::string>
-  ReplayOutFile("replay-out",
-                cl::desc("Specify an out file to replay"),
-                cl::value_desc("out file"));
+      ReplayKTestFile("replay-ktest-file",
+                      cl::desc("Specify a ktest file to use for replay"),
+                      cl::value_desc("ktest file"));
 
   cl::list<std::string>
-  ReplayOutDir("replay-out-dir",
-	       cl::desc("Specify a directory to replay .out files from"),
-	       cl::value_desc("output directory"));
+      ReplayKTestDir("replay-ktest-dir",
+                   cl::desc("Specify a directory to replay ktest files from"),
+                   cl::value_desc("output directory"));
 
   cl::opt<std::string>
   ReplayPathFile("replay-path",
@@ -261,16 +261,12 @@ public:
   std::string getTestFilename(const std::string &suffix, unsigned id);
   llvm::raw_fd_ostream *openTestFile(const std::string &suffix, unsigned id);
 
-  // load a .out file
-  static void loadOutFile(std::string name,
-                          std::vector<unsigned char> &buffer);
-
   // load a .path file
   static void loadPathFile(std::string name,
                            std::vector<bool> &buffer);
 
-  static void getOutFiles(std::string path,
-			  std::vector<std::string> &results);
+  static void getKTestFilesInDir(std::string directoryPath,
+                                 std::vector<std::string> &results);
 
   static std::string getRunTimeLibraryPath(const char *argv0);
 };
@@ -566,14 +562,15 @@ void KleeHandler::loadPathFile(std::string name,
   }
 }
 
-void KleeHandler::getOutFiles(std::string path,
-			      std::vector<std::string> &results) {
+void KleeHandler::getKTestFilesInDir(std::string directoryPath,
+                                     std::vector<std::string> &results) {
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 5)
   error_code ec;
 #else
   std::error_code ec;
 #endif
-  for (llvm::sys::fs::directory_iterator i(path,ec),e; i!=e && !ec; i.increment(ec)){
+  for (llvm::sys::fs::directory_iterator i(directoryPath, ec), e; i != e && !ec;
+       i.increment(ec)) {
     std::string f = (*i).path();
     if (f.substr(f.size()-6,f.size()) == ".ktest") {
           results.push_back(f);
@@ -581,8 +578,8 @@ void KleeHandler::getOutFiles(std::string path,
   }
 
   if (ec) {
-    llvm::errs() << "ERROR: unable to read output directory: " << path << ": "
-                 << ec.message() << "\n";
+    llvm::errs() << "ERROR: unable to read output directory: " << directoryPath
+                 << ": " << ec.message() << "\n";
     exit(1);
   }
 }
@@ -1385,11 +1382,10 @@ int main(int argc, char **argv, char **envp) {
     theInterpreter = Interpreter::create(IOpts, handler);
   handler->setInterpreter(interpreter);
 
-  llvm::raw_ostream &infoFile = handler->getInfoStream();
   for (int i=0; i<argc; i++) {
-    infoFile << argv[i] << (i+1<argc ? " ":"\n");
+    handler->getInfoStream() << argv[i] << (i+1<argc ? " ":"\n");
   }
-  infoFile << "PID: " << getpid() << "\n";
+  handler->getInfoStream() << "PID: " << getpid() << "\n";
 
   const Module *finalModule =
     interpreter->setModule(mainModule, Opts);
@@ -1403,21 +1399,21 @@ int main(int argc, char **argv, char **envp) {
   time_t t[2];
   t[0] = time(NULL);
   strftime(buf, sizeof(buf), "Started: %Y-%m-%d %H:%M:%S\n", localtime(&t[0]));
-  infoFile << buf;
-  infoFile.flush();
+  handler->getInfoStream() << buf;
+  handler->getInfoStream().flush();
 
-  if (!ReplayOutDir.empty() || !ReplayOutFile.empty()) {
+  if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) {
     assert(SeedOutFile.empty());
     assert(SeedOutDir.empty());
 
-    std::vector<std::string> outFiles = ReplayOutFile;
+    std::vector<std::string> kTestFiles = ReplayKTestFile;
     for (std::vector<std::string>::iterator
-           it = ReplayOutDir.begin(), ie = ReplayOutDir.end();
+           it = ReplayKTestDir.begin(), ie = ReplayKTestDir.end();
          it != ie; ++it)
-      KleeHandler::getOutFiles(*it, outFiles);
+      KleeHandler::getKTestFilesInDir(*it, kTestFiles);
     std::vector<KTest*> kTests;
     for (std::vector<std::string>::iterator
-           it = outFiles.begin(), ie = outFiles.end();
+           it = kTestFiles.begin(), ie = kTestFiles.end();
          it != ie; ++it) {
       KTest *out = kTest_fromFile(it->c_str());
       if (out) {
@@ -1439,15 +1435,15 @@ int main(int argc, char **argv, char **envp) {
            it = kTests.begin(), ie = kTests.end();
          it != ie; ++it) {
       KTest *out = *it;
-      interpreter->setReplayOut(out);
+      interpreter->setReplayKTest(out);
       llvm::errs() << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out)
                    << " bytes)"
-                   << " (" << ++i << "/" << outFiles.size() << ")\n";
+                   << " (" << ++i << "/" << kTestFiles.size() << ")\n";
       // XXX should put envp in .ktest ?
       interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
       if (interrupted) break;
     }
-    interpreter->setReplayOut(0);
+    interpreter->setReplayKTest(0);
     while (!kTests.empty()) {
       kTest_free(kTests.back());
       kTests.pop_back();
@@ -1467,10 +1463,10 @@ int main(int argc, char **argv, char **envp) {
     for (std::vector<std::string>::iterator
            it = SeedOutDir.begin(), ie = SeedOutDir.end();
          it != ie; ++it) {
-      std::vector<std::string> outFiles;
-      KleeHandler::getOutFiles(*it, outFiles);
+      std::vector<std::string> kTestFiles;
+      KleeHandler::getKTestFilesInDir(*it, kTestFiles);
       for (std::vector<std::string>::iterator
-             it2 = outFiles.begin(), ie = outFiles.end();
+             it2 = kTestFiles.begin(), ie = kTestFiles.end();
            it2 != ie; ++it2) {
         KTest *out = kTest_fromFile(it2->c_str());
         if (!out) {
@@ -1479,7 +1475,7 @@ int main(int argc, char **argv, char **envp) {
         }
         seeds.push_back(out);
       }
-      if (outFiles.empty()) {
+      if (kTestFiles.empty()) {
         llvm::errs() << "KLEE: seeds directory is empty: " << *it << "\n";
         exit(1);
       }
@@ -1505,11 +1501,11 @@ int main(int argc, char **argv, char **envp) {
 
   t[1] = time(NULL);
   strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1]));
-  infoFile << buf;
+  handler->getInfoStream() << buf;
 
   strcpy(buf, "Elapsed: ");
   strcpy(format_tdiff(buf, t[1] - t[0]), "\n");
-  infoFile << buf;
+  handler->getInfoStream() << buf;
 
   // Free all the args.
   for (unsigned i=0; i<InputArgv.size()+1; i++)
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-05-12 22:12:12 +0000