about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/AddressSpace.cpp2
-rw-r--r--lib/Core/ExecutionState.cpp4
-rw-r--r--lib/Core/Executor.cpp291
-rw-r--r--lib/Core/Executor.h5
-rw-r--r--lib/Core/ExecutorTimers.cpp4
-rw-r--r--lib/Core/MemoryManager.cpp143
-rw-r--r--lib/Core/MemoryManager.h57
-rw-r--r--lib/Core/Searcher.cpp124
-rw-r--r--lib/Core/Searcher.h56
-rw-r--r--lib/Core/StatsTracker.cpp76
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp42
-rw-r--r--lib/Solver/QueryLoggingSolver.h2
-rw-r--r--lib/Solver/STPBuilder.cpp92
-rw-r--r--lib/Solver/STPBuilder.h2
-rw-r--r--lib/Support/CompressionStream.cpp119
15 files changed, 728 insertions, 291 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 25418c13..811e52c3 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -58,6 +58,8 @@ bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr,
 
   if (const MemoryMap::value_type *res = objects.lookup_previous(&hack)) {
     const MemoryObject *mo = res->first;
+    // Check if the provided address is between start and end of the object
+    // [mo->address, mo->address + mo->size) or the object is a 0-sized object.
     if ((mo->size==0 && address==mo->address) ||
         (address - mo->address < mo->size)) {
       result = *res;
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 6aeaa833..30d20266 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -370,8 +370,8 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
 
       out << ai->getName().str();
       // XXX should go through function
-      ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; 
-      if (isa<ConstantExpr>(value))
+      ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value;
+      if (value.get() && isa<ConstantExpr>(value))
         out << "=" << value;
     }
     out << ")";
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 49b022f8..acd02c67 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -89,6 +89,10 @@
 #include "llvm/IR/CallSite.h"
 #endif
 
+#ifdef HAVE_ZLIB_H
+#include "klee/Internal/Support/CompressionStream.h"
+#endif
+
 #include <cassert>
 #include <algorithm>
 #include <iomanip>
@@ -158,6 +162,11 @@ namespace {
                      "[inst_id]"),
           clEnumValEnd),
       llvm::cl::CommaSeparated);
+#ifdef HAVE_ZLIB_H
+  cl::opt<bool> DebugCompressInstructions(
+      "debug-compress-instructions", cl::init(false),
+      cl::desc("Compress the logged instructions in gzip format."));
+#endif
 
   cl::opt<bool>
   DebugCheckForImpliedValues("debug-check-for-implied-values");
@@ -332,6 +341,10 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih)
     std::string debug_file_name =
         interpreterHandler->getOutputFilename("instructions.txt");
     std::string ErrorInfo;
+#ifdef HAVE_ZLIB_H
+    if (!DebugCompressInstructions) {
+#endif
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
     debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo,
                                              llvm::sys::fs::OpenFlags::F_Text),
@@ -339,6 +352,16 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih)
     debugInstFile =
         new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo);
 #endif
+#ifdef HAVE_ZLIB_H
+    } else {
+      debugInstFile = new compressed_fd_ostream(
+          (debug_file_name + ".gz").c_str(), ErrorInfo);
+    }
+#endif
+    if (ErrorInfo != "") {
+      klee_error("Could not open file %s : %s", debug_file_name.c_str(),
+                 ErrorInfo.c_str());
+    }
   }
 }
 
@@ -364,7 +387,7 @@ const Module *Executor::setModule(llvm::Module *module,
   kmodule->prepare(opts, interpreterHandler);
   specialFunctionHandler->bind();
 
-  if (StatsTracker::useStatistics()) {
+  if (StatsTracker::useStatistics() || userSearcherRequiresMD2U()) {
     statsTracker = 
       new StatsTracker(*this,
                        interpreterHandler->getOutputFilename("assembly.ll"),
@@ -539,7 +562,13 @@ void Executor::initializeGlobals(ExecutionState &state) {
       // hack where we check the object file information.
 
       LLVM_TYPE_Q Type *ty = i->getType()->getElementType();
-      uint64_t size = kmodule->targetData->getTypeStoreSize(ty);
+      uint64_t size = 0;
+      if (ty->isSized()) {
+	size = kmodule->targetData->getTypeStoreSize(ty);
+      } else {
+        klee_warning("Type for %.*s is not sized", (int)i->getName().size(),
+			i->getName().data());
+      }
 
       // XXX - DWD - hardcode some things until we decide how to fix.
 #ifndef WINDOWS
@@ -553,9 +582,8 @@ void Executor::initializeGlobals(ExecutionState &state) {
 #endif
 
       if (size == 0) {
-        llvm::errs() << "Unable to find size for global variable: " 
-                     << i->getName() 
-                     << " (use will result in out of bounds access)\n";
+        klee_warning("Unable to find size for global variable: %.*s (use will result in out of bounds access)",
+			(int)i->getName().size(), i->getName().data());
       }
 
       MemoryObject *mo = memory->allocate(size, false, true, i);
@@ -642,7 +670,7 @@ void Executor::branch(ExecutionState &state,
     for (unsigned i=1; i<N; ++i) {
       ExecutionState *es = result[theRNG.getInt32() % i];
       ExecutionState *ns = es->branch();
-      addedStates.insert(ns);
+      addedStates.push_back(ns);
       result.push_back(ns);
       es->ptreeNode->data = 0;
       std::pair<PTree::Node*,PTree::Node*> res = 
@@ -860,7 +888,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     ++stats::forks;
 
     falseState = trueState->branch();
-    addedStates.insert(falseState);
+    addedStates.push_back(falseState);
 
     if (RandomizeFork && theRNG.getBool())
       std::swap(trueState, falseState);
@@ -1212,8 +1240,10 @@ void Executor::executeCall(ExecutionState &state,
       // ExecutionState::varargs
     case Intrinsic::vastart:  {
       StackFrame &sf = state.stack.back();
-      assert(sf.varargs && 
-             "vastart called in function with no vararg object");
+
+      // varargs can be zero if no varargs were provided
+      if (!sf.varargs)
+        return;
 
       // FIXME: This is really specific to the architecture, not the pointer
       // size. This happens to work fir x86-32 and x86-64, however.
@@ -1270,13 +1300,13 @@ void Executor::executeCall(ExecutionState &state,
     KFunction *kf = kmodule->functionMap[f];
     state.pushFrame(state.prevPC, kf);
     state.pc = kf->instructions;
-        
+
     if (statsTracker)
       statsTracker->framePushed(state, &state.stack[state.stack.size()-2]);
- 
+
      // TODO: support "byval" parameter attribute
      // TODO: support zeroext, signext, sret attributes
-        
+
     unsigned callingArgs = arguments.size();
     unsigned funcArgs = f->arg_size();
     if (!f->isVarArg()) {
@@ -1296,56 +1326,64 @@ void Executor::executeCall(ExecutionState &state,
                               "user.err");
         return;
       }
-            
+
       StackFrame &sf = state.stack.back();
       unsigned size = 0;
+      bool requires16ByteAlignment = false;
       for (unsigned i = funcArgs; i < callingArgs; i++) {
         // FIXME: This is really specific to the architecture, not the pointer
-        // size. This happens to work fir x86-32 and x86-64, however.
+        // size. This happens to work for x86-32 and x86-64, however.
         if (WordSize == Expr::Int32) {
           size += Expr::getMinBytesForWidth(arguments[i]->getWidth());
         } else {
           Expr::Width argWidth = arguments[i]->getWidth();
-          // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a 16
-          // byte boundary if alignment needed by type exceeds 8 byte boundary.
+          // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a
+          // 16 byte boundary if alignment needed by type exceeds 8 byte
+          // boundary.
           //
           // Alignment requirements for scalar types is the same as their size
           if (argWidth > Expr::Int64) {
              size = llvm::RoundUpToAlignment(size, 16);
+             requires16ByteAlignment = true;
           }
           size += llvm::RoundUpToAlignment(argWidth, WordSize) / 8;
         }
       }
 
-      MemoryObject *mo = sf.varargs = memory->allocate(size, true, false, 
-                                                       state.prevPC->inst);
-      if (!mo) {
+      MemoryObject *mo = sf.varargs =
+          memory->allocate(size, true, false, state.prevPC->inst,
+                           (requires16ByteAlignment ? 16 : 8));
+      if (!mo && size) {
         terminateStateOnExecError(state, "out of memory (varargs)");
         return;
       }
 
-      if ((WordSize == Expr::Int64) && (mo->address & 15)) {
-        // Both 64bit Linux/Glibc and 64bit MacOSX should align to 16 bytes.
-        klee_warning_once(0, "While allocating varargs: malloc did not align to 16 bytes.");
-      }
+      if (mo) {
+        if ((WordSize == Expr::Int64) && (mo->address & 15) &&
+            requires16ByteAlignment) {
+          // Both 64bit Linux/Glibc and 64bit MacOSX should align to 16 bytes.
+          klee_warning_once(
+              0, "While allocating varargs: malloc did not align to 16 bytes.");
+        }
 
-      ObjectState *os = bindObjectInState(state, mo, true);
-      unsigned offset = 0;
-      for (unsigned i = funcArgs; i < callingArgs; i++) {
-        // FIXME: This is really specific to the architecture, not the pointer
-        // size. This happens to work fir x86-32 and x86-64, however.
-        if (WordSize == Expr::Int32) {
-          os->write(offset, arguments[i]);
-          offset += Expr::getMinBytesForWidth(arguments[i]->getWidth());
-        } else {
-          assert(WordSize == Expr::Int64 && "Unknown word size!");
+        ObjectState *os = bindObjectInState(state, mo, true);
+        unsigned offset = 0;
+        for (unsigned i = funcArgs; i < callingArgs; i++) {
+          // FIXME: This is really specific to the architecture, not the pointer
+          // size. This happens to work for x86-32 and x86-64, however.
+          if (WordSize == Expr::Int32) {
+            os->write(offset, arguments[i]);
+            offset += Expr::getMinBytesForWidth(arguments[i]->getWidth());
+          } else {
+            assert(WordSize == Expr::Int64 && "Unknown word size!");
 
-          Expr::Width argWidth = arguments[i]->getWidth();
-          if (argWidth > Expr::Int64) {
-             offset = llvm::RoundUpToAlignment(offset, 16);
+            Expr::Width argWidth = arguments[i]->getWidth();
+            if (argWidth > Expr::Int64) {
+              offset = llvm::RoundUpToAlignment(offset, 16);
+            }
+            os->write(offset, arguments[i]);
+            offset += llvm::RoundUpToAlignment(argWidth, WordSize) / 8;
           }
-          os->write(offset, arguments[i]);
-          offset += llvm::RoundUpToAlignment(argWidth, WordSize) / 8;
         }
       }
     }
@@ -1586,58 +1624,108 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 #endif
       transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
     } else {
-      std::map<BasicBlock*, ref<Expr> > targets;
-      ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool);
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)      
-      for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end();
-           i != e; ++i) {
+      // Handle possible different branch targets
+
+      // We have the following assumptions:
+      // - each case value is mutual exclusive to all other values including the
+      //   default value
+      // - order of case branches is based on the order of the expressions of
+      //   the scase values, still default is handled last
+      std::vector<BasicBlock *> bbOrder;
+      std::map<BasicBlock *, ref<Expr> > branchTargets;
+
+      std::map<ref<Expr>, BasicBlock *> expressionOrder;
+
+      // Iterate through all non-default cases and order them by expressions
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
+      for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); i != e;
+           ++i) {
         ref<Expr> value = evalConstant(i.getCaseValue());
 #else
-      for (unsigned i=1, cases = si->getNumCases(); i<cases; ++i) {
+      for (unsigned i = 1, cases = si->getNumCases(); i < cases; ++i) {
         ref<Expr> value = evalConstant(si->getCaseValue(i));
 #endif
-        ref<Expr> match = EqExpr::create(cond, value);
-        isDefault = AndExpr::create(isDefault, Expr::createIsZero(match));
+
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
+        BasicBlock *caseSuccessor = i.getCaseSuccessor();
+#else
+        BasicBlock *caseSuccessor = si->getSuccessor(i);
+#endif
+        expressionOrder.insert(std::make_pair(value, caseSuccessor));
+      }
+
+      // Track default branch values
+      ref<Expr> defaultValue = ConstantExpr::alloc(1, Expr::Bool);
+
+      // iterate through all non-default cases but in order of the expressions
+      for (std::map<ref<Expr>, BasicBlock *>::iterator
+               it = expressionOrder.begin(),
+               itE = expressionOrder.end();
+           it != itE; ++it) {
+        ref<Expr> match = EqExpr::create(cond, it->first);
+
+        // Make sure that the default value does not contain this target's value
+        defaultValue = AndExpr::create(defaultValue, Expr::createIsZero(match));
+
+        // Check if control flow could take this case
         bool result;
         bool success = solver->mayBeTrue(state, match, result);
         assert(success && "FIXME: Unhandled solver failure");
         (void) success;
         if (result) {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
-          BasicBlock *caseSuccessor = i.getCaseSuccessor();
-#else
-          BasicBlock *caseSuccessor = si->getSuccessor(i);
-#endif
-          std::map<BasicBlock*, ref<Expr> >::iterator it =
-            targets.insert(std::make_pair(caseSuccessor,
-                           ConstantExpr::alloc(0, Expr::Bool))).first;
-
-          it->second = OrExpr::create(match, it->second);
+          BasicBlock *caseSuccessor = it->second;
+
+          // Handle the case that a basic block might be the target of multiple
+          // switch cases.
+          // Currently we generate an expression containing all switch-case
+          // values for the same target basic block. We spare us forking too
+          // many times but we generate more complex condition expressions
+          // TODO Add option to allow to choose between those behaviors
+          std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> res =
+              branchTargets.insert(std::make_pair(
+                  caseSuccessor, ConstantExpr::alloc(0, Expr::Bool)));
+
+          res.first->second = OrExpr::create(match, res.first->second);
+
+          // Only add basic blocks which have not been target of a branch yet
+          if (res.second) {
+            bbOrder.push_back(caseSuccessor);
+          }
         }
       }
+
+      // Check if control could take the default case
       bool res;
-      bool success = solver->mayBeTrue(state, isDefault, res);
+      bool success = solver->mayBeTrue(state, defaultValue, res);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
-      if (res)
-        targets.insert(std::make_pair(si->getDefaultDest(), isDefault));
-      
+      if (res) {
+        std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> ret =
+            branchTargets.insert(
+                std::make_pair(si->getDefaultDest(), defaultValue));
+        if (ret.second) {
+          bbOrder.push_back(si->getDefaultDest());
+        }
+      }
+
+      // Fork the current state with each state having one of the possible
+      // successors of this switch
       std::vector< ref<Expr> > conditions;
-      for (std::map<BasicBlock*, ref<Expr> >::iterator it = 
-             targets.begin(), ie = targets.end();
-           it != ie; ++it)
-        conditions.push_back(it->second);
-      
+      for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(),
+                                               ie = bbOrder.end();
+           it != ie; ++it) {
+        conditions.push_back(branchTargets[*it]);
+      }
       std::vector<ExecutionState*> branches;
       branch(state, conditions, branches);
-        
+
       std::vector<ExecutionState*>::iterator bit = branches.begin();
-      for (std::map<BasicBlock*, ref<Expr> >::iterator it = 
-             targets.begin(), ie = targets.end();
+      for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(),
+                                               ie = bbOrder.end();
            it != ie; ++it) {
         ExecutionState *es = *bit;
         if (es)
-          transferToBasicBlock(it->first, bb, *es);
+          transferToBasicBlock(*it, bb, *es);
         ++bit;
       }
     }
@@ -2444,9 +2532,9 @@ void Executor::updateStates(ExecutionState *current) {
   
   states.insert(addedStates.begin(), addedStates.end());
   addedStates.clear();
-  
-  for (std::set<ExecutionState*>::iterator
-         it = removedStates.begin(), ie = removedStates.end();
+
+  for (std::vector<ExecutionState *>::iterator it = removedStates.begin(),
+                                               ie = removedStates.end();
        it != ie; ++it) {
     ExecutionState *es = *it;
     std::set<ExecutionState*>::iterator it2 = states.find(es);
@@ -2531,7 +2619,9 @@ void Executor::checkMemoryUsage() {
     // We need to avoid calling GetTotalMallocUsage() often because it
     // is O(elts on freelist). This is really bad since we start
     // to pummel the freelist once we hit the memory cap.
-    unsigned mbs = util::GetTotalMallocUsage() >> 20;
+    unsigned mbs = (util::GetTotalMallocUsage() >> 20) +
+                   (memory->getUsedDeterministicSize() >> 20);
+
     if (mbs > MaxMemory) {
       if (mbs > MaxMemory + 100) {
         // just guess at how many to kill
@@ -2557,6 +2647,20 @@ void Executor::checkMemoryUsage() {
   }
 }
 
+void Executor::doDumpStates() {
+  if (!DumpStatesOnHalt || states.empty())
+    return;
+  klee_message("halting execution, dumping remaining states");
+  for (std::set<ExecutionState *>::iterator it = states.begin(),
+                                            ie = states.end();
+       it != ie; ++it) {
+    ExecutionState &state = **it;
+    stepInstruction(state); // keep stats rolling
+    terminateStateEarly(state, "Execution halting.");
+  }
+  updateStates(0);
+}
+
 void Executor::run(ExecutionState &initialState) {
   bindModuleConstants();
 
@@ -2577,7 +2681,10 @@ void Executor::run(ExecutionState &initialState) {
     double lastTime, startTime = lastTime = util::getWallTime();
     ExecutionState *lastState = 0;
     while (!seedMap.empty()) {
-      if (haltExecution) goto dump;
+      if (haltExecution) {
+        doDumpStates();
+        return;
+      }
 
       std::map<ExecutionState*, std::vector<SeedInfo> >::iterator it = 
         seedMap.upper_bound(lastState);
@@ -2626,13 +2733,16 @@ void Executor::run(ExecutionState &initialState) {
       (*it)->weight = 1.;
     }
 
-    if (OnlySeed)
-      goto dump;
+    if (OnlySeed) {
+      doDumpStates();
+      return;
+    }
   }
 
   searcher = constructUserSearcher(*this);
 
-  searcher->update(0, states, std::set<ExecutionState*>());
+  std::vector<ExecutionState *> newStates(states.begin(), states.end());
+  searcher->update(0, newStates, std::vector<ExecutionState *>());
 
   while (!states.empty() && !haltExecution) {
     ExecutionState &state = searcher->selectState();
@@ -2649,19 +2759,8 @@ void Executor::run(ExecutionState &initialState) {
 
   delete searcher;
   searcher = 0;
-  
- dump:
-  if (DumpStatesOnHalt && !states.empty()) {
-    klee_message("halting execution, dumping remaining states");
-    for (std::set<ExecutionState*>::iterator
-           it = states.begin(), ie = states.end();
-         it != ie; ++it) {
-      ExecutionState &state = **it;
-      stepInstruction(state); // keep stats rolling
-      terminateStateEarly(state, "Execution halting.");
-    }
-    updateStates(0);
-  }
+
+  doDumpStates();
 }
 
 std::string Executor::getAddressInfo(ExecutionState &state, 
@@ -2722,11 +2821,12 @@ void Executor::terminateState(ExecutionState &state) {
 
   interpreterHandler->incPathsExplored();
 
-  std::set<ExecutionState*>::iterator it = addedStates.find(&state);
+  std::vector<ExecutionState *>::iterator it =
+      std::find(addedStates.begin(), addedStates.end(), &state);
   if (it==addedStates.end()) {
     state.pc = state.prevPC;
 
-    removedStates.insert(&state);
+    removedStates.push_back(&state);
   } else {
     // never reached searcher, just delete immediately
     std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 = 
@@ -3390,7 +3490,10 @@ void Executor::runFunctionAsMain(Function *f,
     if (++ai!=ae) {
       argvMO = memory->allocate((argc+1+envc+1+1) * NumPtrBytes, false, true,
                                 f->begin()->begin());
-      
+
+      if (!argvMO)
+        klee_error("Could not allocate memory for function arguments");
+
       arguments.push_back(argvMO->getBaseExpr());
 
       if (++ai!=ae) {
@@ -3430,6 +3533,8 @@ void Executor::runFunctionAsMain(Function *f,
         int j, len = strlen(s);
         
         MemoryObject *arg = memory->allocate(len+1, false, true, state->pc->inst);
+        if (!arg)
+          klee_error("Could not allocate memory for function arguments");
         ObjectState *os = bindObjectInState(*state, arg, false);
         for (j=0; j<len+1; j++)
           os->write8(j, s[j]);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 600c7b90..92edc364 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -122,12 +122,12 @@ private:
   /// instructions step. 
   /// \invariant \ref addedStates is a subset of \ref states. 
   /// \invariant \ref addedStates and \ref removedStates are disjoint.
-  std::set<ExecutionState*> addedStates;
+  std::vector<ExecutionState *> addedStates;
   /// Used to track states that have been removed during the current
   /// instructions step. 
   /// \invariant \ref removedStates is a subset of \ref states. 
   /// \invariant \ref addedStates and \ref removedStates are disjoint.
-  std::set<ExecutionState*> removedStates;
+  std::vector<ExecutionState *> removedStates;
 
   /// When non-empty the Executor is running in "seed" mode. The
   /// states in this map will be executed in an arbitrary order
@@ -412,6 +412,7 @@ private:
                      double maxInstTime);
   void checkMemoryUsage();
   void printDebugInstructions(ExecutionState &state);
+  void doDumpStates();
 
 public:
   Executor(const InterpreterOptions &opts, InterpreterHandler *ie);
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 480f1cde..f1c45105 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -179,7 +179,9 @@ void Executor::processTimers(ExecutionState *current,
       dumpStates = 0;
     }
 
-    if (maxInstTime>0 && current && !removedStates.count(current)) {
+    if (maxInstTime > 0 && current &&
+        std::find(removedStates.begin(), removedStates.end(), current) ==
+            removedStates.end()) {
       if (timerTicks*kSecondsPerTick > maxInstTime) {
         klee_warning("max-instruction-time exceeded: %.2fs",
                      timerTicks*kSecondsPerTick);
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index 7c76d480..f9f4b105 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -11,37 +11,135 @@
 #include "Memory.h"
 #include "MemoryManager.h"
 
-#include "klee/ExecutionState.h"
 #include "klee/Expr.h"
-#include "klee/Solver.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/MathExtras.h"
 
+#include <sys/mman.h>
 using namespace klee;
 
+namespace {
+llvm::cl::opt<bool> DeterministicAllocation(
+    "allocate-determ",
+    llvm::cl::desc("Allocate memory deterministically(default=off)"),
+    llvm::cl::init(false));
+
+llvm::cl::opt<unsigned> DeterministicAllocationSize(
+    "allocate-determ-size",
+    llvm::cl::desc(
+        "Preallocated memory for deterministic allocation in MB (default=100)"),
+    llvm::cl::init(100));
+
+llvm::cl::opt<bool>
+    NullOnZeroMalloc("return-null-on-zero-malloc",
+                     llvm::cl::desc("Returns NULL in case malloc(size) was "
+                                    "called with size 0 (default=off)."),
+                     llvm::cl::init(false));
+
+llvm::cl::opt<unsigned> RedZoneSpace(
+    "red-zone-space",
+    llvm::cl::desc("Set the amount of free space between allocations. This is "
+                   "important to detect out-of-bound accesses (default=10)."),
+    llvm::cl::init(10));
+
+llvm::cl::opt<unsigned long long> DeterministicStartAddress(
+    "allocate-determ-start-address",
+    llvm::cl::desc("Start address for deterministic allocation. Has to be page "
+                   "aligned (default=0x7ff30000000)."),
+    llvm::cl::init(0x7ff30000000));
+}
+
 /***/
+MemoryManager::MemoryManager(ArrayCache *_arrayCache)
+    : arrayCache(_arrayCache), deterministicSpace(0), nextFreeSlot(0),
+      spaceSize(DeterministicAllocationSize.getValue() * 1024 * 1024) {
+  if (DeterministicAllocation) {
+    // Page boundary
+    void *expectedAddress = (void *)DeterministicStartAddress.getValue();
+
+    char *newSpace =
+        (char *)mmap(expectedAddress, spaceSize, PROT_READ | PROT_WRITE,
+                     MAP_ANONYMOUS | MAP_PRIVATE, -1, 0);
 
-MemoryManager::~MemoryManager() { 
+    if (newSpace == MAP_FAILED) {
+      klee_error("Couldn't mmap() memory for deterministic allocations");
+    }
+    if (expectedAddress != newSpace && expectedAddress != 0) {
+      klee_error("Could not allocate memory deterministically");
+    }
+
+    klee_message("Deterministic memory allocation starting from %p", newSpace);
+    deterministicSpace = newSpace;
+    nextFreeSlot = newSpace;
+  }
+}
+
+MemoryManager::~MemoryManager() {
   while (!objects.empty()) {
     MemoryObject *mo = *objects.begin();
-    if (!mo->isFixed)
+    if (!mo->isFixed && !DeterministicAllocation)
       free((void *)mo->address);
     objects.erase(mo);
     delete mo;
   }
+
+  if (DeterministicAllocation)
+    munmap(deterministicSpace, spaceSize);
 }
 
-MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, 
+MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal,
                                       bool isGlobal,
-                                      const llvm::Value *allocSite) {
-  if (size>10*1024*1024)
-    klee_warning_once(0, "Large alloc: %u bytes.  KLEE may run out of memory.", (unsigned) size);
-  
-  uint64_t address = (uint64_t) (unsigned long) malloc((unsigned) size);
+                                      const llvm::Value *allocSite,
+                                      size_t alignment) {
+  if (size > 10 * 1024 * 1024)
+    klee_warning_once(0, "Large alloc: %lu bytes.  KLEE may run out of memory.",
+                      size);
+
+  // Return NULL if size is zero, this is equal to error during allocation
+  if (NullOnZeroMalloc && size == 0)
+    return 0;
+
+  if (!llvm::isPowerOf2_64(alignment)) {
+    klee_warning("Only alignment of power of two is supported");
+    return 0;
+  }
+
+  uint64_t address = 0;
+  if (DeterministicAllocation) {
+
+    address = llvm::RoundUpToAlignment((uint64_t)nextFreeSlot + alignment - 1,
+                                       alignment);
+
+    // Handle the case of 0-sized allocations as 1-byte allocations.
+    // This way, we make sure we have this allocation between its own red zones
+    size_t alloc_size = std::max(size, (uint64_t)1);
+    if ((char *)address + alloc_size < deterministicSpace + spaceSize) {
+      nextFreeSlot = (char *)address + alloc_size + RedZoneSpace;
+    } else {
+      klee_warning_once(
+          0,
+          "Couldn't allocate %lu bytes. Not enough deterministic space left.",
+          size);
+      address = 0;
+    }
+  } else {
+    // Use malloc for the standard case
+    if (alignment <= 8)
+      address = (uint64_t)malloc(size);
+    else {
+      int res = posix_memalign((void **)&address, alignment, size);
+      if (res < 0) {
+        klee_warning("Allocating aligned memory failed.");
+        address = 0;
+      }
+    }
+  }
+
   if (!address)
     return 0;
-  
+
   ++stats::allocations;
   MemoryObject *res = new MemoryObject(address, size, isLocal, isGlobal, false,
                                        allocSite, this);
@@ -52,30 +150,31 @@ MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal,
 MemoryObject *MemoryManager::allocateFixed(uint64_t address, uint64_t size,
                                            const llvm::Value *allocSite) {
 #ifndef NDEBUG
-  for (objects_ty::iterator it = objects.begin(), ie = objects.end();
-       it != ie; ++it) {
+  for (objects_ty::iterator it = objects.begin(), ie = objects.end(); it != ie;
+       ++it) {
     MemoryObject *mo = *it;
-    if (address+size > mo->address && address < mo->address+mo->size)
+    if (address + size > mo->address && address < mo->address + mo->size)
       klee_error("Trying to allocate an overlapping object");
   }
 #endif
 
   ++stats::allocations;
-  MemoryObject *res = new MemoryObject(address, size, false, true, true,
-                                       allocSite, this);
+  MemoryObject *res =
+      new MemoryObject(address, size, false, true, true, allocSite, this);
   objects.insert(res);
   return res;
 }
 
-void MemoryManager::deallocate(const MemoryObject *mo) {
-  assert(0);
-}
+void MemoryManager::deallocate(const MemoryObject *mo) { assert(0); }
 
 void MemoryManager::markFreed(MemoryObject *mo) {
-  if (objects.find(mo) != objects.end())
-  {
-    if (!mo->isFixed)
+  if (objects.find(mo) != objects.end()) {
+    if (!mo->isFixed && !DeterministicAllocation)
       free((void *)mo->address);
     objects.erase(mo);
   }
 }
+
+size_t MemoryManager::getUsedDeterministicSize() {
+  return nextFreeSlot - deterministicSpace;
+}
diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h
index 01683443..fc77b476 100644
--- a/lib/Core/MemoryManager.h
+++ b/lib/Core/MemoryManager.h
@@ -14,31 +14,44 @@
 #include <stdint.h>
 
 namespace llvm {
-  class Value;
+class Value;
 }
 
 namespace klee {
-  class MemoryObject;
-  class ArrayCache;
-
-  class MemoryManager {
-  private:
-    typedef std::set<MemoryObject*> objects_ty;
-    objects_ty objects;
-    ArrayCache *const arrayCache;
-
-  public:
-    MemoryManager(ArrayCache *arrayCache) : arrayCache(arrayCache) {}
-    ~MemoryManager();
-
-    MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal,
-                           const llvm::Value *allocSite);
-    MemoryObject *allocateFixed(uint64_t address, uint64_t size,
-                                const llvm::Value *allocSite);
-    void deallocate(const MemoryObject *mo);
-    void markFreed(MemoryObject *mo);
-    ArrayCache *getArrayCache() const { return arrayCache; }
-  };
+class MemoryObject;
+class ArrayCache;
+
+class MemoryManager {
+private:
+  typedef std::set<MemoryObject *> objects_ty;
+  objects_ty objects;
+  ArrayCache *const arrayCache;
+
+  char *deterministicSpace;
+  char *nextFreeSlot;
+  size_t spaceSize;
+
+public:
+  MemoryManager(ArrayCache *arrayCache);
+  ~MemoryManager();
+
+  /**
+   * Returns memory object which contains a handle to real virtual process
+   * memory.
+   */
+  MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal,
+                         const llvm::Value *allocSite, size_t alignment = 8);
+  MemoryObject *allocateFixed(uint64_t address, uint64_t size,
+                              const llvm::Value *allocSite);
+  void deallocate(const MemoryObject *mo);
+  void markFreed(MemoryObject *mo);
+  ArrayCache *getArrayCache() const { return arrayCache; }
+
+  /*
+   * Returns the size used by deterministic allocation in bytes
+   */
+  size_t getUsedDeterministicSize();
+};
 
 } // End klee namespace
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index cbb88727..973057c3 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -67,13 +67,14 @@ ExecutionState &DFSSearcher::selectState() {
 }
 
 void DFSSearcher::update(ExecutionState *current,
-                         const std::set<ExecutionState*> &addedStates,
-                         const std::set<ExecutionState*> &removedStates) {
+                         const std::vector<ExecutionState *> &addedStates,
+                         const std::vector<ExecutionState *> &removedStates) {
   states.insert(states.end(),
                 addedStates.begin(),
                 addedStates.end());
-  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
-         ie = removedStates.end(); it != ie; ++it) {
+  for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+                                                     ie = removedStates.end();
+       it != ie; ++it) {
     ExecutionState *es = *it;
     if (es == states.back()) {
       states.pop_back();
@@ -101,13 +102,14 @@ ExecutionState &BFSSearcher::selectState() {
 }
 
 void BFSSearcher::update(ExecutionState *current,
-                         const std::set<ExecutionState*> &addedStates,
-                         const std::set<ExecutionState*> &removedStates) {
+                         const std::vector<ExecutionState *> &addedStates,
+                         const std::vector<ExecutionState *> &removedStates) {
   states.insert(states.end(),
                 addedStates.begin(),
                 addedStates.end());
-  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
-         ie = removedStates.end(); it != ie; ++it) {
+  for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+                                                     ie = removedStates.end();
+       it != ie; ++it) {
     ExecutionState *es = *it;
     if (es == states.front()) {
       states.pop_front();
@@ -134,14 +136,16 @@ ExecutionState &RandomSearcher::selectState() {
   return *states[theRNG.getInt32()%states.size()];
 }
 
-void RandomSearcher::update(ExecutionState *current,
-                            const std::set<ExecutionState*> &addedStates,
-                            const std::set<ExecutionState*> &removedStates) {
+void
+RandomSearcher::update(ExecutionState *current,
+                       const std::vector<ExecutionState *> &addedStates,
+                       const std::vector<ExecutionState *> &removedStates) {
   states.insert(states.end(),
                 addedStates.begin(),
                 addedStates.end());
-  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
-         ie = removedStates.end(); it != ie; ++it) {
+  for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+                                                     ie = removedStates.end();
+       it != ie; ++it) {
     ExecutionState *es = *it;
     bool ok = false;
 
@@ -224,20 +228,24 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
   }
 }
 
-void WeightedRandomSearcher::update(ExecutionState *current,
-                                    const std::set<ExecutionState*> &addedStates,
-                                    const std::set<ExecutionState*> &removedStates) {
-  if (current && updateWeights && !removedStates.count(current))
+void WeightedRandomSearcher::update(
+    ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+    const std::vector<ExecutionState *> &removedStates) {
+  if (current && updateWeights &&
+      std::find(removedStates.begin(), removedStates.end(), current) ==
+          removedStates.end())
     states->update(current, getWeight(current));
-  
-  for (std::set<ExecutionState*>::const_iterator it = addedStates.begin(),
-         ie = addedStates.end(); it != ie; ++it) {
+
+  for (std::vector<ExecutionState *>::const_iterator it = addedStates.begin(),
+                                                     ie = addedStates.end();
+       it != ie; ++it) {
     ExecutionState *es = *it;
     states->insert(es, getWeight(es));
   }
 
-  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
-         ie = removedStates.end(); it != ie; ++it) {
+  for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
+                                                     ie = removedStates.end();
+       it != ie; ++it) {
     states->remove(*it);
   }
 }
@@ -277,9 +285,10 @@ ExecutionState &RandomPathSearcher::selectState() {
   return *n->data;
 }
 
-void RandomPathSearcher::update(ExecutionState *current,
-                                const std::set<ExecutionState*> &addedStates,
-                                const std::set<ExecutionState*> &removedStates) {
+void
+RandomPathSearcher::update(ExecutionState *current,
+                           const std::vector<ExecutionState *> &addedStates,
+                           const std::vector<ExecutionState *> &removedStates) {
 }
 
 bool RandomPathSearcher::empty() { 
@@ -358,9 +367,9 @@ entry:
   }
 }
 
-void BumpMergingSearcher::update(ExecutionState *current,
-                                 const std::set<ExecutionState*> &addedStates,
-                                 const std::set<ExecutionState*> &removedStates) {
+void BumpMergingSearcher::update(
+    ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+    const std::vector<ExecutionState *> &removedStates) {
   baseSearcher->update(current, addedStates, removedStates);
 }
 
@@ -472,18 +481,21 @@ ExecutionState &MergingSearcher::selectState() {
   return selectState();
 }
 
-void MergingSearcher::update(ExecutionState *current,
-                             const std::set<ExecutionState*> &addedStates,
-                             const std::set<ExecutionState*> &removedStates) {
+void
+MergingSearcher::update(ExecutionState *current,
+                        const std::vector<ExecutionState *> &addedStates,
+                        const std::vector<ExecutionState *> &removedStates) {
   if (!removedStates.empty()) {
-    std::set<ExecutionState *> alt = removedStates;
-    for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
-           ie = removedStates.end(); it != ie; ++it) {
+    std::vector<ExecutionState *> alt = removedStates;
+    for (std::vector<ExecutionState *>::const_iterator
+             it = removedStates.begin(),
+             ie = removedStates.end();
+         it != ie; ++it) {
       ExecutionState *es = *it;
       std::set<ExecutionState*>::const_iterator it2 = statesAtMerge.find(es);
       if (it2 != statesAtMerge.end()) {
         statesAtMerge.erase(it2);
-        alt.erase(alt.find(es));
+        alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end());
       }
     }    
     baseSearcher->update(current, addedStates, alt);
@@ -529,10 +541,12 @@ ExecutionState &BatchingSearcher::selectState() {
   }
 }
 
-void BatchingSearcher::update(ExecutionState *current,
-                              const std::set<ExecutionState*> &addedStates,
-                              const std::set<ExecutionState*> &removedStates) {
-  if (removedStates.count(lastState))
+void
+BatchingSearcher::update(ExecutionState *current,
+                         const std::vector<ExecutionState *> &addedStates,
+                         const std::vector<ExecutionState *> &removedStates) {
+  if (std::find(removedStates.begin(), removedStates.end(), lastState) !=
+      removedStates.end())
     lastState = 0;
   baseSearcher->update(current, addedStates, removedStates);
 }
@@ -554,20 +568,22 @@ ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
   return res;
 }
 
-void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
-                                            const std::set<ExecutionState*> &addedStates,
-                                            const std::set<ExecutionState*> &removedStates) {
+void IterativeDeepeningTimeSearcher::update(
+    ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+    const std::vector<ExecutionState *> &removedStates) {
   double elapsed = util::getWallTime() - startTime;
 
   if (!removedStates.empty()) {
-    std::set<ExecutionState *> alt = removedStates;
-    for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
-           ie = removedStates.end(); it != ie; ++it) {
+    std::vector<ExecutionState *> alt = removedStates;
+    for (std::vector<ExecutionState *>::const_iterator
+             it = removedStates.begin(),
+             ie = removedStates.end();
+         it != ie; ++it) {
       ExecutionState *es = *it;
       std::set<ExecutionState*>::const_iterator it2 = pausedStates.find(es);
       if (it2 != pausedStates.end()) {
-        pausedStates.erase(it);
-        alt.erase(alt.find(es));
+        pausedStates.erase(it2);
+        alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end());
       }
     }    
     baseSearcher->update(current, addedStates, alt);
@@ -575,7 +591,10 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
     baseSearcher->update(current, addedStates, removedStates);
   }
 
-  if (current && !removedStates.count(current) && elapsed>time) {
+  if (current &&
+      std::find(removedStates.begin(), removedStates.end(), current) ==
+          removedStates.end() &&
+      elapsed > time) {
     pausedStates.insert(current);
     baseSearcher->removeState(current);
   }
@@ -583,7 +602,8 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
   if (baseSearcher->empty()) {
     time *= 2;
     llvm::errs() << "KLEE: increasing time budget to: " << time << "\n";
-    baseSearcher->update(0, pausedStates, std::set<ExecutionState*>());
+    std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
+    baseSearcher->update(0, ps, std::vector<ExecutionState *>());
     pausedStates.clear();
   }
 }
@@ -607,9 +627,9 @@ ExecutionState &InterleavedSearcher::selectState() {
   return s->selectState();
 }
 
-void InterleavedSearcher::update(ExecutionState *current,
-                                 const std::set<ExecutionState*> &addedStates,
-                                 const std::set<ExecutionState*> &removedStates) {
+void InterleavedSearcher::update(
+    ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+    const std::vector<ExecutionState *> &removedStates) {
   for (std::vector<Searcher*>::const_iterator it = searchers.begin(),
          ie = searchers.end(); it != ie; ++it)
     (*it)->update(current, addedStates, removedStates);
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index d866f521..4ede3640 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -35,8 +35,8 @@ namespace klee {
     virtual ExecutionState &selectState() = 0;
 
     virtual void update(ExecutionState *current,
-                        const std::set<ExecutionState*> &addedStates,
-                        const std::set<ExecutionState*> &removedStates) = 0;
+                        const std::vector<ExecutionState *> &addedStates,
+                        const std::vector<ExecutionState *> &removedStates) = 0;
 
     virtual bool empty() = 0;
 
@@ -55,15 +55,15 @@ namespace klee {
     // utility functions
 
     void addState(ExecutionState *es, ExecutionState *current = 0) {
-      std::set<ExecutionState*> tmp;
-      tmp.insert(es);
-      update(current, tmp, std::set<ExecutionState*>());
+      std::vector<ExecutionState *> tmp;
+      tmp.push_back(es);
+      update(current, tmp, std::vector<ExecutionState *>());
     }
 
     void removeState(ExecutionState *es, ExecutionState *current = 0) {
-      std::set<ExecutionState*> tmp;
-      tmp.insert(es);
-      update(current, std::set<ExecutionState*>(), tmp);
+      std::vector<ExecutionState *> tmp;
+      tmp.push_back(es);
+      update(current, std::vector<ExecutionState *>(), tmp);
     }
 
     enum CoreSearchType {
@@ -86,8 +86,8 @@ namespace klee {
   public:
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return states.empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "DFSSearcher\n";
@@ -100,8 +100,8 @@ namespace klee {
   public:
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return states.empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "BFSSearcher\n";
@@ -114,8 +114,8 @@ namespace klee {
   public:
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return states.empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "RandomSearcher\n";
@@ -146,8 +146,8 @@ namespace klee {
 
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty();
     void printName(llvm::raw_ostream &os) {
       os << "WeightedRandomSearcher::";
@@ -172,8 +172,8 @@ namespace klee {
 
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty();
     void printName(llvm::raw_ostream &os) {
       os << "RandomPathSearcher\n";
@@ -195,8 +195,8 @@ namespace klee {
 
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "MergingSearcher\n";
@@ -218,8 +218,8 @@ namespace klee {
 
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "BumpMergingSearcher\n";
@@ -243,8 +243,8 @@ namespace klee {
 
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return baseSearcher->empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "<BatchingSearcher> timeBudget: " << timeBudget
@@ -266,8 +266,8 @@ namespace klee {
 
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return baseSearcher->empty() && pausedStates.empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "IterativeDeepeningTimeSearcher\n";
@@ -286,8 +286,8 @@ namespace klee {
 
     ExecutionState &selectState();
     void update(ExecutionState *current,
-                const std::set<ExecutionState*> &addedStates,
-                const std::set<ExecutionState*> &removedStates);
+                const std::vector<ExecutionState *> &addedStates,
+                const std::vector<ExecutionState *> &removedStates);
     bool empty() { return searchers[0]->empty(); }
     void printName(llvm::raw_ostream &os) {
       os << "<InterleavedSearcher> containing "
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 5e77172e..97ed26ea 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -86,17 +86,20 @@ namespace {
                      cl::init(1.),
 		     cl::desc("Approximate number of seconds between stats writes (default=1.0s)"));
 
+  cl::opt<unsigned> StatsWriteAfterInstructions(
+      "stats-write-after-instructions", cl::init(0),
+      cl::desc("Write statistics after each n instructions, 0 to disable "
+               "(default=0)"));
+
   cl::opt<double>
   IStatsWriteInterval("istats-write-interval",
 		      cl::init(10.),
                       cl::desc("Approximate number of seconds between istats writes (default: 10.0s)"));
 
-  /*
-  cl::opt<double>
-  BranchCovCountsWriteInterval("branch-cov-counts-write-interval",
-                     cl::desc("Approximate number of seconds between run.branches writes (default: 5.0s)"),
-                     cl::init(5.));
-  */
+  cl::opt<unsigned> IStatsWriteAfterInstructions(
+      "istats-write-after-instructions", cl::init(0),
+      cl::desc("Write istats after each n instructions, 0 to disable "
+               "(default=0)"));
 
   // XXX I really would like to have dynamic rate control for something like this.
   cl::opt<double>
@@ -185,6 +188,18 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
     fullBranches(0),
     partialBranches(0),
     updateMinDistToUncovered(_updateMinDistToUncovered) {
+
+  if (StatsWriteAfterInstructions > 0 && StatsWriteInterval > 0)
+    klee_error("Both options --stats-write-interval and "
+               "--stats-write-after-instructions cannot be enabled at the same "
+               "time.");
+
+  if (IStatsWriteAfterInstructions > 0 && IStatsWriteInterval > 0)
+    klee_error(
+        "Both options --istats-write-interval and "
+        "--istats-write-after-instructions cannot be enabled at the same "
+        "time.");
+
   KModule *km = executor.kmodule;
 
   if (!sys::path::is_absolute(objectFilename)) {
@@ -235,19 +250,22 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
     writeStatsHeader();
     writeStatsLine();
 
-    executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+    if (StatsWriteInterval > 0)
+      executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+  }
 
-    if (updateMinDistToUncovered) {
-      computeReachableUncovered();
-      executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval);
-    }
+  // Add timer to calculate uncovered instructions if needed by the solver
+  if (updateMinDistToUncovered) {
+    computeReachableUncovered();
+    executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval);
   }
 
   if (OutputIStats) {
     istatsFile = executor.interpreterHandler->openOutputFile("run.istats");
     assert(istatsFile && "unable to open istats file");
 
-    executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
+    if (IStatsWriteInterval > 0)
+      executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
   }
 }
 
@@ -261,8 +279,12 @@ StatsTracker::~StatsTracker() {
 void StatsTracker::done() {
   if (statsFile)
     writeStatsLine();
-  if (OutputIStats)
+
+  if (OutputIStats) {
+    if (updateMinDistToUncovered)
+      computeReachableUncovered();
     writeIStats();
+  }
 }
 
 void StatsTracker::stepInstruction(ExecutionState &es) {
@@ -310,6 +332,14 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
       }
     }
   }
+
+  if (statsFile && StatsWriteAfterInstructions &&
+      stats::instructions % StatsWriteAfterInstructions.getValue() == 0)
+    writeStatsLine();
+
+  if (istatsFile && IStatsWriteAfterInstructions &&
+      stats::instructions % IStatsWriteAfterInstructions.getValue() == 0)
+    writeIStats();
 }
 
 ///
@@ -327,15 +357,17 @@ void StatsTracker::framePushed(ExecutionState &es, StackFrame *parentFrame) {
       sf.callPathNode = cp;
       cp->count++;
     }
+  }
 
-    if (updateMinDistToUncovered) {
-      uint64_t minDistAtRA = 0;
-      if (parentFrame)
-        minDistAtRA = parentFrame->minDistToUncoveredOnReturn;
-      
-      sf.minDistToUncoveredOnReturn = sf.caller ?
-        computeMinDistToUncovered(sf.caller, minDistAtRA) : 0;
-    }
+  if (updateMinDistToUncovered) {
+    StackFrame &sf = es.stack.back();
+
+    uint64_t minDistAtRA = 0;
+    if (parentFrame)
+      minDistAtRA = parentFrame->minDistToUncoveredOnReturn;
+
+    sf.minDistToUncoveredOnReturn =
+        sf.caller ? computeMinDistToUncovered(sf.caller, minDistAtRA) : 0;
   }
 }
 
@@ -406,7 +438,7 @@ void StatsTracker::writeStatsLine() {
              << "," << numBranches
              << "," << util::getUserTime()
              << "," << executor.states.size()
-             << "," << util::GetTotalMallocUsage()
+             << "," << util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize()
              << "," << stats::queries
              << "," << stats::queryConstructs
              << "," << 0 // was numObjects
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index f93bec3c..fb957b65 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -7,8 +7,13 @@
 //
 //===----------------------------------------------------------------------===//
 #include "QueryLoggingSolver.h"
+#include "klee/Config/config.h"
 #include "klee/Internal/System/Time.h"
 #include "klee/Statistics.h"
+#ifdef HAVE_ZLIB_H
+#include "klee/Internal/Support/CompressionStream.h"
+#include "klee/Internal/Support/ErrorHandling.h"
+#endif
 
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
 #include "llvm/Support/FileSystem.h"
@@ -20,30 +25,49 @@ 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)"));
+
+#ifdef HAVE_ZLIB_H
+llvm::cl::opt<bool> CreateCompressedQueryLog(
+    "compress-query-log", llvm::cl::init(false),
+    llvm::cl::desc("Compress query log files (default=off)"));
+#endif
 }
 
 QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
                                        const std::string &commentSign,
                                        int queryTimeToLog)
-    : solver(_solver),
+    : solver(_solver), os(0), BufferString(""), logBuffer(BufferString),
+      queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f),
+      lastQueryTime(0.0f), queryCommentSign(commentSign) {
+  if (!CreateCompressedQueryLog) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-      os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text),
+    os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo,
+                                  llvm::sys::fs::OpenFlags::F_Text);
 #else
-      os(path.c_str(), ErrorInfo),
+    os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo);
+#endif
+  }
+#ifdef HAVE_ZLIB_H
+  else {
+    os = new compressed_fd_ostream((path + ".gz").c_str(), ErrorInfo);
+  }
+  if (ErrorInfo != "") {
+    klee_error("Could not open file %s : %s", path.c_str(), ErrorInfo.c_str());
+  }
 #endif
-      BufferString(""), logBuffer(BufferString), queryCount(0),
-      minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f),
-      queryCommentSign(commentSign) {
   assert(0 != solver);
 }
 
-QueryLoggingSolver::~QueryLoggingSolver() { delete solver; }
+QueryLoggingSolver::~QueryLoggingSolver() {
+  delete solver;
+  delete os;
+}
 
 void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) {
   logBuffer.flush();
   if (writeToFile) {
-    os << logBuffer.str();
-    os.flush();
+    *os << logBuffer.str();
+    os->flush();
   }
   // prepare the buffer for reuse
   BufferString = "";
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index bb266c67..7ac783d1 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -26,7 +26,7 @@ class QueryLoggingSolver : public SolverImpl {
 protected:
   Solver *solver;
   std::string ErrorInfo;
-  llvm::raw_fd_ostream os;
+  llvm::raw_ostream *os;
   // @brief Buffer used by logBuffer
   std::string BufferString;
   // @brief buffer to store logs before flushing to file
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 307ae0fb..8ec35762 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -152,6 +152,7 @@ ExprHandle STPBuilder::bvExtract(ExprHandle expr, unsigned top, unsigned bottom)
   return vc_bvExtract(vc, expr, top, bottom);
 }
 ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) {
+  assert((vc_getBVLength(vc, a) == vc_getBVLength(vc, b)) && "a and b should be same type");
   return vc_eqExpr(vc, a, b);
 }
 
@@ -187,76 +188,93 @@ ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned shift) {
   }
 }
 
+ExprHandle STPBuilder::extractPartialShiftValue(ExprHandle shift,
+                                                unsigned width,
+                                                unsigned &shiftBits) {
+  // Assuming width is power of 2
+  llvm::APInt sw(32, width);
+  shiftBits = sw.getActiveBits();
+
+  // get the shift amount (looking only at the bits appropriate for the given
+  // width)
+  return vc_bvExtract(vc, shift, shiftBits - 1, 0);
+}
+
 // left shift by a variable amount on an expression of the specified width
 ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
   unsigned width = vc_getBVLength(vc, expr);
   ExprHandle res = bvZero(width);
 
-  //construct a big if-then-elif-elif-... with one case per possible shift amount
-  for( int i=width-1; i>=0; i-- ) {
-    res = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(width, i)),
-                     bvLeftShift(expr, i),
-                     res);
+  unsigned shiftBits = 0;
+  ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res = vc_iteExpr(vc, eqExpr(shift_ext, bvConst32(shiftBits, i)),
+                     bvLeftShift(expr, i), res);
   }
 
   // If overshifting, shift to zero
-  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
+  ExprHandle ex =
+      vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width));
 
   res = vc_iteExpr(vc, ex, res, bvZero(width));
   return res;
 }
 
-// logical right shift by a variable amount on an expression of the specified width
+// logical right shift by a variable amount on an expression of the specified
+// width
 ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
   unsigned width = vc_getBVLength(vc, expr);
   ExprHandle res = bvZero(width);
 
-  //construct a big if-then-elif-elif-... with one case per possible shift amount
-  for( int i=width-1; i>=0; i-- ) {
-    res = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(width, i)),
-                     bvRightShift(expr, i),
-                     res);
+  unsigned shiftBits = 0;
+  ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res = vc_iteExpr(vc, eqExpr(shift_ext, bvConst32(shiftBits, i)),
+                     bvRightShift(expr, i), res);
   }
 
   // If overshifting, shift to zero
-  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
-  res = vc_iteExpr(vc,
-                   ex,
-                   res,
-                   bvZero(width));
+  // If overshifting, shift to zero
+  ExprHandle ex =
+      vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width));
+  res = vc_iteExpr(vc, ex, res, bvZero(width));
+
   return res;
 }
 
-// arithmetic right shift by a variable amount on an expression of the specified width
+// arithmetic right shift by a variable amount on an expression of the specified
+// width
 ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
   unsigned width = vc_getBVLength(vc, expr);
 
-  //get the sign bit to fill with
-  ExprHandle signedBool = bvBoolExtract(expr, width-1);
+  unsigned shiftBits = 0;
+  ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits);
 
-  //start with the result if shifting by width-1
-  ExprHandle res = constructAShrByConstant(expr, width-1, signedBool);
+  // get the sign bit to fill with
+  ExprHandle signedBool = bvBoolExtract(expr, width - 1);
 
-  //construct a big if-then-elif-elif-... with one case per possible shift amount
+  // start with the result if shifting by width-1
+  ExprHandle res = constructAShrByConstant(expr, width - 1, signedBool);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
   // XXX more efficient to move the ite on the sign outside all exprs?
   // XXX more efficient to sign extend, right shift, then extract lower bits?
-  for( int i=width-2; i>=0; i-- ) {
-    res = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(width,i)),
-                     constructAShrByConstant(expr, 
-                                             i, 
-                                             signedBool),
-                     res);
+  for (int i = width - 2; i >= 0; i--) {
+    res = vc_iteExpr(vc, eqExpr(shift_ext, bvConst32(shiftBits, i)),
+                     constructAShrByConstant(expr, i, signedBool), res);
   }
 
   // If overshifting, shift to zero
-  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
-  res = vc_iteExpr(vc,
-                   ex,
-                   res,
-                   bvZero(width));
+  ExprHandle ex =
+      vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width));
+  res = vc_iteExpr(vc, ex, res, bvZero(width));
   return res;
 }
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 3b17ccf1..5be34029 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -93,6 +93,8 @@ private:
   ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift);
+  ExprHandle extractPartialShiftValue(ExprHandle shift, unsigned width,
+                                      unsigned &shiftBits);
 
   ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, 
                                      ExprHandle isSigned);
diff --git a/lib/Support/CompressionStream.cpp b/lib/Support/CompressionStream.cpp
new file mode 100644
index 00000000..eb208edf
--- /dev/null
+++ b/lib/Support/CompressionStream.cpp
@@ -0,0 +1,119 @@
+//===-- CompressionStream.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/Config/config.h"
+#include "klee/Config/Version.h"
+#ifdef HAVE_ZLIB_H
+#include "klee/Internal/Support/CompressionStream.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/Support/system_error.h"
+#else
+#include <fcntl.h>
+#include <errno.h>
+#include <sys/types.h>
+#include <sys/stat.h>
+#endif
+
+namespace klee {
+
+compressed_fd_ostream::compressed_fd_ostream(const char *Filename,
+                                             std::string &ErrorInfo)
+    : llvm::raw_ostream(), pos(0) {
+  ErrorInfo = "";
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+  // Open file in binary mode
+  llvm::error_code EC =
+      llvm::sys::fs::openFileForWrite(Filename, FD, llvm::sys::fs::F_Binary);
+
+  if (EC) {
+    ErrorInfo = EC.message();
+    FD = -1;
+  }
+#else
+  FD = ::open(Filename, O_WRONLY | O_CREAT | O_TRUNC, 0666);
+  if (FD < 0) {
+    ErrorInfo = "Could not open file.";
+    FD = -1;
+  }
+#endif
+  // Initialize the compression library
+  strm.zalloc = 0;
+  strm.zfree = 0;
+  strm.next_out = buffer;
+  strm.avail_out = BUFSIZE;
+
+  deflateInit2(&strm, Z_BEST_COMPRESSION, Z_DEFLATED, 15 | 16,
+               8 /* memory usage default, 0 smalles, 9 highest*/,
+               Z_DEFAULT_STRATEGY);
+}
+
+void compressed_fd_ostream::writeFullCompressedData() {
+  // Check if no space available and write the buffer
+  if (strm.avail_out == 0) {
+    write_file(reinterpret_cast<const char *>(buffer), BUFSIZE);
+    strm.next_out = buffer;
+    strm.avail_out = BUFSIZE;
+  }
+}
+
+void compressed_fd_ostream::flush_compressed_data() {
+  // flush data from the raw buffer
+  flush();
+
+  // write the remaining data
+  int deflate_res = Z_OK;
+  while (deflate_res == Z_OK) {
+    // Check if no space available and write the buffer
+    writeFullCompressedData();
+    deflate_res = deflate(&strm, Z_FINISH);
+  }
+  assert(deflate_res == Z_STREAM_END);
+  write_file(reinterpret_cast<const char *>(buffer), BUFSIZE - strm.avail_out);
+}
+
+compressed_fd_ostream::~compressed_fd_ostream() {
+  if (FD >= 0) {
+    // write the remaining data
+    flush_compressed_data();
+    close(FD);
+  }
+  deflateEnd(&strm);
+}
+
+void compressed_fd_ostream::write_impl(const char *Ptr, size_t Size) {
+  strm.next_in =
+      const_cast<unsigned char *>(reinterpret_cast<const unsigned char *>(Ptr));
+  strm.avail_in = Size;
+
+  // Check if there is still data to compress
+  while (strm.avail_in != 0) {
+    // compress data
+    int res = deflate(&strm, Z_NO_FLUSH);
+    assert(res == Z_OK);
+    writeFullCompressedData();
+  }
+}
+
+void compressed_fd_ostream::write_file(const char *Ptr, size_t Size) {
+  pos += Size;
+  assert(FD >= 0 && "File already closed");
+  do {
+    ssize_t ret = ::write(FD, Ptr, Size);
+    if (ret < 0) {
+      if (errno == EINTR || errno == EAGAIN)
+        continue;
+      assert(0 && "Could not write to file");
+      break;
+    }
+
+    Ptr += ret;
+    Size -= ret;
+  } while (Size > 0);
+}
+}
+#endif
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-04-02 13:32:23 +0000