searchers: clean up, add documentation

2 files changed, 215 insertions, 246 deletions

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 37c40897..e2f11a87 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -23,7 +23,6 @@
 #include "klee/Module/KInstruction.h"
 #include "klee/Module/KModule.h"
 #include "klee/Support/ErrorHandling.h"
-#include "klee/Support/ModuleUtil.h"
 #include "klee/System/Time.h"
 
 #include "llvm/IR/Constants.h"
@@ -32,17 +31,12 @@
 #include "llvm/Support/CommandLine.h"
 
 #include <cassert>
-#include <climits>
 #include <cmath>
-#include <fstream>
 
 using namespace klee;
 using namespace llvm;
 
 
-Searcher::~Searcher() {
-}
-
 ///
 
 ExecutionState &DFSSearcher::selectState() {
@@ -52,28 +46,25 @@ ExecutionState &DFSSearcher::selectState() {
 void DFSSearcher::update(ExecutionState *current,
                          const std::vector<ExecutionState *> &addedStates,
                          const std::vector<ExecutionState *> &removedStates) {
-  states.insert(states.end(),
-                addedStates.begin(),
-                addedStates.end());
-  for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
-                                                     ie = removedStates.end();
-       it != ie; ++it) {
-    ExecutionState *es = *it;
-    if (es == states.back()) {
+  // insert states
+  states.insert(states.end(), addedStates.begin(), addedStates.end());
+
+  // remove states
+  for (const auto state : removedStates) {
+    if (state == states.back()) {
       states.pop_back();
     } else {
+      __attribute__((unused))
       bool ok = false;
 
-      for (std::vector<ExecutionState*>::iterator it = states.begin(),
-             ie = states.end(); it != ie; ++it) {
-        if (es==*it) {
+      for (auto it = states.begin(), ie = states.end(); it != ie; ++it) {
+        if (state == *it) {
           states.erase(it);
           ok = true;
           break;
         }
       }
 
-      (void) ok;
       assert(ok && "invalid state removed");
     }
   }
@@ -88,6 +79,7 @@ ExecutionState &BFSSearcher::selectState() {
 void BFSSearcher::update(ExecutionState *current,
                          const std::vector<ExecutionState *> &addedStates,
                          const std::vector<ExecutionState *> &removedStates) {
+  // update current state
   // Assumption: If new states were added KLEE forked, therefore states evolved.
   // constraints were added to the current state, it evolved.
   if (!addedStates.empty() && current &&
@@ -99,28 +91,25 @@ void BFSSearcher::update(ExecutionState *current,
     states.push_back(current);
   }
 
-  states.insert(states.end(),
-                addedStates.begin(),
-                addedStates.end());
-  for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
-                                                     ie = removedStates.end();
-       it != ie; ++it) {
-    ExecutionState *es = *it;
-    if (es == states.front()) {
+  // insert states
+  states.insert(states.end(), addedStates.begin(), addedStates.end());
+
+  // remove states
+  for (const auto state : removedStates) {
+    if (state == states.front()) {
       states.pop_front();
     } else {
+      __attribute__((unused))
       bool ok = false;
 
-      for (std::deque<ExecutionState*>::iterator it = states.begin(),
-             ie = states.end(); it != ie; ++it) {
-        if (es==*it) {
+      for (auto it = states.begin(), ie = states.end(); it != ie; ++it) {
+        if (state == *it) {
           states.erase(it);
           ok = true;
           break;
         }
       }
 
-      (void) ok;
       assert(ok && "invalid state removed");
     }
   }
@@ -129,32 +118,28 @@ void BFSSearcher::update(ExecutionState *current,
 ///
 
 ExecutionState &RandomSearcher::selectState() {
-  return *states[theRNG.getInt32()%states.size()];
+  return *states[theRNG.getInt32() % states.size()];
 }
 
-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::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
-                                                     ie = removedStates.end();
-       it != ie; ++it) {
-    ExecutionState *es = *it;
+void RandomSearcher::update(ExecutionState *current,
+                            const std::vector<ExecutionState *> &addedStates,
+                            const std::vector<ExecutionState *> &removedStates) {
+  // insert states
+  states.insert(states.end(), addedStates.begin(), addedStates.end());
+
+  // remove states
+  for (const auto state : removedStates) {
     __attribute__((unused))
     bool ok = false;
 
-    for (std::vector<ExecutionState*>::iterator it = states.begin(),
-           ie = states.end(); it != ie; ++it) {
-      if (es==*it) {
+    for (auto it = states.begin(), ie = states.end(); it != ie; ++it) {
+      if (state == *it) {
         states.erase(it);
         ok = true;
         break;
       }
     }
-    
+
     assert(ok && "invalid state removed");
   }
 }
@@ -162,9 +147,10 @@ RandomSearcher::update(ExecutionState *current,
 ///
 
 WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng)
-  : states(new DiscretePDF<ExecutionState*, ExecutionStateIDCompare>()),
+  : states(std::make_unique<DiscretePDF<ExecutionState*, ExecutionStateIDCompare>>()),
     theRNG{rng},
     type(type) {
+
   switch(type) {
   case Depth:
   case RP:
@@ -182,10 +168,6 @@ WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng)
   }
 }
 
-WeightedRandomSearcher::~WeightedRandomSearcher() {
-  delete states;
-}
-
 ExecutionState &WeightedRandomSearcher::selectState() {
   return *states->choose(theRNG.getDoubleL());
 }
@@ -234,36 +216,28 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
 void WeightedRandomSearcher::update(
     ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
     const std::vector<ExecutionState *> &removedStates) {
+
+  // update current
   if (current && updateWeights &&
       std::find(removedStates.begin(), removedStates.end(), current) ==
           removedStates.end())
     states->update(current, getWeight(current));
 
-  for (std::vector<ExecutionState *>::const_iterator it = addedStates.begin(),
-                                                     ie = addedStates.end();
-       it != ie; ++it) {
-    ExecutionState *es = *it;
-    states->insert(es, getWeight(es));
-  }
+  // insert states
+  for (const auto state : addedStates)
+    states->insert(state, getWeight(state));
 
-  for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(),
-                                                     ie = removedStates.end();
-       it != ie; ++it) {
-    states->remove(*it);
-  }
+  // remove states
+  for (const auto state : removedStates)
+    states->remove(state);
 }
 
-bool WeightedRandomSearcher::empty() { 
-  return states->empty(); 
+bool WeightedRandomSearcher::empty() {
+  return states->empty();
 }
 
 ///
-RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng)
-  : processTree{processTree}, theRNG{rng}, idBitMask{processTree.getNextId()} {
-}
 
-RandomPathSearcher::~RandomPathSearcher() {
-}
 // Check if n is a valid pointer and a node belonging to us
 #define IS_OUR_NODE_VALID(n)                                                   \
   (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
@@ -289,17 +263,17 @@ ExecutionState &RandomPathSearcher::selectState() {
         bits = 32;
       }
       --bits;
-      n = ((flips & (1 << bits)) ? n->left : n->right).getPointer();
+      n = ((flips & (1U << bits)) ? n->left : n->right).getPointer();
     }
   }
 
   return *n->state;
 }
 
-void
-RandomPathSearcher::update(ExecutionState *current,
-                           const std::vector<ExecutionState *> &addedStates,
-                           const std::vector<ExecutionState *> &removedStates) {
+void RandomPathSearcher::update(ExecutionState *current,
+                                const std::vector<ExecutionState *> &addedStates,
+                                const std::vector<ExecutionState *> &removedStates) {
+  // insert states
   for (auto es : addedStates) {
     PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
     PTreeNodePtr *childPtr;
@@ -320,6 +294,7 @@ RandomPathSearcher::update(ExecutionState *current,
     }
   }
 
+  // remove states
   for (auto es : removedStates) {
     PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
 
@@ -344,13 +319,6 @@ bool RandomPathSearcher::empty() {
 
 ///
 
-MergingSearcher::MergingSearcher(Searcher *_baseSearcher)
-  : baseSearcher(_baseSearcher){}
-
-MergingSearcher::~MergingSearcher() {
-  delete baseSearcher;
-}
-
 ExecutionState& MergingSearcher::selectState() {
   assert(!baseSearcher->empty() && "base searcher is empty");
 
@@ -382,20 +350,6 @@ ExecutionState& MergingSearcher::selectState() {
 
 ///
 
-BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher,
-                                   time::Span _timeBudget,
-                                   unsigned _instructionBudget) 
-  : baseSearcher(_baseSearcher),
-    timeBudget(_timeBudget),
-    instructionBudget(_instructionBudget),
-    lastState(0) {
-  
-}
-
-BatchingSearcher::~BatchingSearcher() {
-  delete baseSearcher;
-}
-
 ExecutionState &BatchingSearcher::selectState() {
   if (!lastState ||
       (((timeBudget.toSeconds() > 0) &&
@@ -420,26 +374,18 @@ ExecutionState &BatchingSearcher::selectState() {
   }
 }
 
-void
-BatchingSearcher::update(ExecutionState *current,
-                         const std::vector<ExecutionState *> &addedStates,
-                         const std::vector<ExecutionState *> &removedStates) {
+void BatchingSearcher::update(ExecutionState *current,
+                              const std::vector<ExecutionState *> &addedStates,
+                              const std::vector<ExecutionState *> &removedStates) {
+  // drop memoized state if it is marked for deletion
   if (std::find(removedStates.begin(), removedStates.end(), lastState) !=
       removedStates.end())
-    lastState = 0;
+    lastState = nullptr;
+  // update underlying searcher
   baseSearcher->update(current, addedStates, removedStates);
 }
 
-/***/
-
-IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(Searcher *_baseSearcher)
-  : baseSearcher(_baseSearcher),
-    time(time::seconds(1)) {
-}
-
-IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() {
-  delete baseSearcher;
-}
+///
 
 ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
   ExecutionState &res = baseSearcher->selectState();
@@ -453,17 +399,14 @@ void IterativeDeepeningTimeSearcher::update(
 
   const auto elapsed = time::getWallTime() - startTime;
 
+  // update underlying searcher (filter paused states unknown to underlying searcher)
   if (!removedStates.empty()) {
     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(it2);
-        alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end());
+    for (const auto state : removedStates) {
+      auto it = pausedStates.find(state);
+      if (it != pausedStates.end()) {
+        pausedStates.erase(it);
+        alt.erase(std::remove(alt.begin(), alt.end(), state), alt.end());
       }
     }    
     baseSearcher->update(current, addedStates, alt);
@@ -471,6 +414,7 @@ void IterativeDeepeningTimeSearcher::update(
     baseSearcher->update(current, addedStates, removedStates);
   }
 
+  // update current: pause if time exceeded
   if (current &&
       std::find(removedStates.begin(), removedStates.end(), current) ==
           removedStates.end() &&
@@ -479,38 +423,35 @@ void IterativeDeepeningTimeSearcher::update(
     baseSearcher->removeState(current);
   }
 
+  // no states left in underlying searcher: fill with paused states
   if (baseSearcher->empty()) {
     time *= 2U;
     klee_message("increased time budget to %f\n", time.toSeconds());
     std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
-    baseSearcher->update(0, ps, std::vector<ExecutionState *>());
+    baseSearcher->update(nullptr, ps, std::vector<ExecutionState *>());
     pausedStates.clear();
   }
 }
 
-/***/
-
-InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers)
-  : searchers(_searchers),
-    index(1) {
-}
+///
 
-InterleavedSearcher::~InterleavedSearcher() {
-  for (std::vector<Searcher*>::const_iterator it = searchers.begin(),
-         ie = searchers.end(); it != ie; ++it)
-    delete *it;
+InterleavedSearcher::InterleavedSearcher(const std::vector<Searcher*> &_searchers) {
+  searchers.reserve(_searchers.size());
+  for (auto searcher : _searchers)
+    searchers.emplace_back(searcher);
 }
 
 ExecutionState &InterleavedSearcher::selectState() {
-  Searcher *s = searchers[--index];
-  if (index==0) index = searchers.size();
+  Searcher *s = searchers[--index].get();
+  if (index == 0) index = searchers.size();
   return s->selectState();
 }
 
 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);
+
+  // update underlying searchers
+  for (auto &searcher : searchers)
+    searcher->update(current, addedStates, removedStates);
 }
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 437cf01f..9243b69a 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -35,45 +35,44 @@ namespace klee {
   class ExecutionState;
   class Executor;
 
+  /// A Searcher implements an exploration strategy for the Executor by selecting
+  /// states for further exploration using different strategies or heuristics.
   class Searcher {
   public:
-    virtual ~Searcher();
+    virtual ~Searcher() = default;
 
+    /// Selects a state for further exploration.
+    /// \return The selected state.
     virtual ExecutionState &selectState() = 0;
 
+    /// Notifies searcher about new or deleted states.
+    /// \param current The currently selected state for exploration.
+    /// \param addedStates The newly branched states with `current` as common ancestor.
+    /// \param removedStates The states that will be terminated.
     virtual void update(ExecutionState *current,
                         const std::vector<ExecutionState *> &addedStates,
                         const std::vector<ExecutionState *> &removedStates) = 0;
 
+    /// \return True if no state left for exploration, False otherwise
     virtual bool empty() = 0;
 
-    // prints name of searcher as a klee_message()
-    // TODO: could probably make prettier or more flexible
+    /// Prints name of searcher as a `klee_message()`.
+    // TODO: could probably made prettier or more flexible
     virtual void printName(llvm::raw_ostream &os) {
       os << "<unnamed searcher>\n";
     }
 
-    // pgbovine - to be called when a searcher gets activated and
-    // deactivated, say, by a higher-level searcher; most searchers
-    // don't need this functionality, so don't have to override.
-    virtual void activate() {}
-    virtual void deactivate() {}
-
     // utility functions
 
-    void addState(ExecutionState *es, ExecutionState *current = 0) {
-      std::vector<ExecutionState *> tmp;
-      tmp.push_back(es);
-      update(current, tmp, std::vector<ExecutionState *>());
+    void addState(ExecutionState *es, ExecutionState *current = nullptr) {
+      update(current, {es}, std::vector<ExecutionState *>());
     }
 
-    void removeState(ExecutionState *es, ExecutionState *current = 0) {
-      std::vector<ExecutionState *> tmp;
-      tmp.push_back(es);
-      update(current, std::vector<ExecutionState *>(), tmp);
+    void removeState(ExecutionState *es, ExecutionState *current = nullptr) {
+      update(current, std::vector<ExecutionState *>(), {es});
     }
 
-    enum CoreSearchType {
+    enum CoreSearchType : std::uint8_t {
       DFS,
       BFS,
       RandomState,
@@ -88,53 +87,62 @@ namespace klee {
     };
   };
 
-  class DFSSearcher : public Searcher {
+  /// DFSSearcher implements depth-first exploration. All states are kept in
+  /// insertion order. The last state is selected for further exploration.
+  class DFSSearcher final : public Searcher {
     std::vector<ExecutionState*> states;
 
   public:
-    ExecutionState &selectState();
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return states.empty(); }
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override { return states.empty(); }
+    void printName(llvm::raw_ostream &os) override {
       os << "DFSSearcher\n";
     }
   };
 
-  class BFSSearcher : public Searcher {
+  /// BFSSearcher implements breadth-first exploration. When KLEE branches multiple
+  /// times for a single instruction, all new states have the same depth. Keep in
+  /// mind that the process tree (PTree) is a binary tree and hence the depth of
+  /// a state in that tree and its branch depth during BFS are different.
+  class BFSSearcher final : public Searcher {
     std::deque<ExecutionState*> states;
 
   public:
-    ExecutionState &selectState();
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return states.empty(); }
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override { return states.empty(); }
+    void printName(llvm::raw_ostream &os) override {
       os << "BFSSearcher\n";
     }
   };
 
-  class RandomSearcher : public Searcher {
+  /// RandomSearcher picks a state randomly.
+  class RandomSearcher final : public Searcher {
     std::vector<ExecutionState*> states;
     RNG &theRNG;
 
   public:
     explicit RandomSearcher(RNG &rng) : theRNG{rng} {}
-    ExecutionState &selectState();
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return states.empty(); }
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override { return states.empty(); }
+    void printName(llvm::raw_ostream &os) override {
       os << "RandomSearcher\n";
     }
   };
 
-  class WeightedRandomSearcher : public Searcher {
+  /// The base class for all weighted searchers. Uses DiscretePDF as underlying
+  /// data structure.
+  class WeightedRandomSearcher final : public Searcher {
   public:
-    enum WeightType {
+    enum WeightType : std::uint8_t {
       Depth,
       RP,
       QueryCost,
@@ -145,7 +153,7 @@ namespace klee {
     };
 
   private:
-    DiscretePDF<ExecutionState*, ExecutionStateIDCompare> *states;
+    std::unique_ptr<DiscretePDF<ExecutionState*, ExecutionStateIDCompare>> states;
     RNG &theRNG;
     WeightType type;
     bool updateWeights;
@@ -153,15 +161,17 @@ namespace klee {
     double getWeight(ExecutionState*);
 
   public:
+    /// \param type The WeightType that determines the underlying heuristic.
+    /// \param RNG A random number generator.
     WeightedRandomSearcher(WeightType type, RNG &rng);
-    ~WeightedRandomSearcher();
+    ~WeightedRandomSearcher() override = default;
 
-    ExecutionState &selectState();
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty();
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override;
+    void printName(llvm::raw_ostream &os) override {
       os << "WeightedRandomSearcher::";
       switch(type) {
       case Depth              : os << "Depth\n"; return;
@@ -176,25 +186,22 @@ namespace klee {
     }
   };
 
-  /* RandomPathSearcher performs a random walk of the PTree to
-     select a state. PTree is a global data structure, however
-     a searcher can sometimes only select from a subset of all states
-     (depending on the update calls).
-
-     To support this RandomPathSearcher has a subgraph view of PTree, in that it
-     only
-     walks the PTreeNodes that it "owns". Ownership is stored in the
-     getInt method of PTreeNodePtr class (which hides it in the pointer itself).
-
-     The current implementation of PTreeNodePtr supports only 3 instances of the
-     RandomPathSearcher. This is because current PTreeNodePtr implementation
-     conforms to C++ and only steals the last 3 alligment bits. This restriction
-     could be relaxed  slightly by an architecture specific implementation of
-     PTreeNodePtr, that also steals the top bits of the pointer.
-
-     The ownership bits are maintained in the update method.
-  */
-  class RandomPathSearcher : public Searcher {
+  /// RandomPathSearcher performs a random walk of the PTree to select a state.
+  /// PTree is a global data structure, however, a searcher can sometimes only
+  /// select from a subset of all states (depending on the update calls).
+  ///
+  /// To support this, RandomPathSearcher has a subgraph view of PTree, in that it
+  /// only walks the PTreeNodes that it "owns". Ownership is stored in the
+  /// getInt method of the PTreeNodePtr class (which hides it in the pointer itself).
+  ///
+  /// The current implementation of PTreeNodePtr supports only 3 instances of the
+  /// RandomPathSearcher. This is because the current PTreeNodePtr implementation
+  /// conforms to C++ and only steals the last 3 alignment bits. This restriction
+  /// could be relaxed slightly by an architecture-specific implementation of
+  /// PTreeNodePtr that also steals the top bits of the pointer.
+  ///
+  /// The ownership bits are maintained in the update method.
+  class RandomPathSearcher final : public Searcher {
     PTree &processTree;
     RNG &theRNG;
 
@@ -202,15 +209,20 @@ namespace klee {
     const uint8_t idBitMask;
 
   public:
-    RandomPathSearcher(PTree &processTree, RNG &rng);
-    ~RandomPathSearcher();
-
-    ExecutionState &selectState();
+    /// \param processTree The process tree.
+    /// \param RNG A random number generator.
+    RandomPathSearcher(PTree &processTree, RNG &rng) :
+                         processTree{processTree},
+                         theRNG{rng},
+                         idBitMask{processTree.getNextId()} {};
+    ~RandomPathSearcher() override = default;
+
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty();
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override;
+    void printName(llvm::raw_ostream &os) override {
       os << "RandomPathSearcher\n";
     }
   };
@@ -218,19 +230,20 @@ namespace klee {
 
   extern llvm::cl::opt<bool> UseIncompleteMerge;
   class MergeHandler;
-  class MergingSearcher : public Searcher {
+  class MergingSearcher final : public Searcher {
     friend class MergeHandler;
 
     private:
 
-    Searcher *baseSearcher;
+    std::unique_ptr<Searcher> baseSearcher;
 
     /// States that have been paused by the 'pauseState' function
     std::vector<ExecutionState*> pausedStates;
 
     public:
-    MergingSearcher(Searcher *baseSearcher);
-    ~MergingSearcher();
+    /// \param baseSearcher The underlying searcher (takes ownership).
+    explicit MergingSearcher(Searcher *baseSearcher) : baseSearcher{baseSearcher} {};
+    ~MergingSearcher() override = default;
 
     /// ExecutionStates currently paused from scheduling because they are
     /// waiting to be merged in a klee_close_merge instruction
@@ -260,11 +273,11 @@ namespace klee {
       baseSearcher->addState(&state);
     }
 
-    ExecutionState &selectState();
+    ExecutionState &selectState() override;
 
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates) {
+                const std::vector<ExecutionState *> &removedStates) override {
       // We have to check if the current execution state was just deleted, as to
       // not confuse the nurs searchers
       if (std::find(pausedStates.begin(), pausedStates.end(), current) ==
@@ -273,33 +286,40 @@ namespace klee {
       }
     }
 
-    bool empty() { return baseSearcher->empty(); }
-    void printName(llvm::raw_ostream &os) {
+    bool empty() override { return baseSearcher->empty(); }
+    void printName(llvm::raw_ostream &os) override {
       os << "MergingSearcher\n";
     }
   };
 
-  class BatchingSearcher : public Searcher {
-    Searcher *baseSearcher;
+  /// BatchingSearcher selects a state from an underlying searcher and returns
+  /// that state for further exploration for a given time or a given number
+  /// of instructions.
+  class BatchingSearcher final : public Searcher {
+    std::unique_ptr<Searcher> baseSearcher;
     time::Span timeBudget;
     unsigned instructionBudget;
 
-    ExecutionState *lastState;
+    ExecutionState *lastState {nullptr};
     time::Point lastStartTime;
     unsigned lastStartInstructions;
 
   public:
-    BatchingSearcher(Searcher *baseSearcher, 
-                     time::Span _timeBudget,
-                     unsigned _instructionBudget);
-    ~BatchingSearcher();
-
-    ExecutionState &selectState();
+    /// \param baseSearcher The underlying searcher (takes ownership).
+    /// \param timeBudget Time span a state gets selected before choosing a different one.
+    /// \param instructionBudget Number of instructions to re-select a state for.
+    BatchingSearcher(Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget) :
+                       baseSearcher{baseSearcher},
+                       timeBudget{timeBudget},
+                       instructionBudget{instructionBudget} {};
+    ~BatchingSearcher() override = default;
+
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return baseSearcher->empty(); }
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override { return baseSearcher->empty(); }
+    void printName(llvm::raw_ostream &os) override {
       os << "<BatchingSearcher> timeBudget: " << timeBudget
          << ", instructionBudget: " << instructionBudget
          << ", baseSearcher:\n";
@@ -308,51 +328,59 @@ namespace klee {
     }
   };
 
-  class IterativeDeepeningTimeSearcher : public Searcher {
-    Searcher *baseSearcher;
+  /// IterativeDeepeningTimeSearcher implements time-based deepening. States
+  /// are selected from an underlying searcher. When a state reaches its time
+  /// limit it is paused (removed from underlying searcher). When the underlying
+  /// searcher runs out of states, the time budget is increased and all paused
+  /// states are revived (added to underlying searcher).
+  class IterativeDeepeningTimeSearcher final : public Searcher {
+    std::unique_ptr<Searcher> baseSearcher;
     time::Point startTime;
-    time::Span time;
+    time::Span time {time::seconds(1)};
     std::set<ExecutionState*> pausedStates;
 
   public:
-    IterativeDeepeningTimeSearcher(Searcher *baseSearcher);
-    ~IterativeDeepeningTimeSearcher();
+    /// \param baseSearcher The underlying searcher (takes ownership).
+    explicit IterativeDeepeningTimeSearcher(Searcher *baseSearcher) :
+                                              baseSearcher{baseSearcher} {};
+    ~IterativeDeepeningTimeSearcher() override = default;
 
-    ExecutionState &selectState();
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return baseSearcher->empty() && pausedStates.empty(); }
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override { return baseSearcher->empty() && pausedStates.empty(); }
+    void printName(llvm::raw_ostream &os) override {
       os << "IterativeDeepeningTimeSearcher\n";
     }
   };
 
-  class InterleavedSearcher : public Searcher {
-    typedef std::vector<Searcher*> searchers_ty;
-
-    searchers_ty searchers;
-    unsigned index;
+  /// InterleavedSearcher selects states from a set of searchers in round-robin
+  /// manner. It is used for KLEE's default strategy where it switches between
+  /// RandomPathSearcher and WeightedRandomSearcher with CoveringNew metric.
+  class InterleavedSearcher final : public Searcher {
+    std::vector<std::unique_ptr<Searcher>> searchers;
+    unsigned index {1};
 
   public:
-    explicit InterleavedSearcher(const searchers_ty &_searchers);
-    ~InterleavedSearcher();
+    /// \param searchers The underlying searchers (takes ownership).
+    explicit InterleavedSearcher(const std::vector<Searcher *> &searchers);
+    ~InterleavedSearcher() override = default;
 
-    ExecutionState &selectState();
+    ExecutionState &selectState() override;
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
-                const std::vector<ExecutionState *> &removedStates);
-    bool empty() { return searchers[0]->empty(); }
-    void printName(llvm::raw_ostream &os) {
+                const std::vector<ExecutionState *> &removedStates) override;
+    bool empty() override { return searchers[0]->empty(); }
+    void printName(llvm::raw_ostream &os) override {
       os << "<InterleavedSearcher> containing "
          << searchers.size() << " searchers:\n";
-      for (searchers_ty::iterator it = searchers.begin(), ie = searchers.end();
-           it != ie; ++it)
-        (*it)->printName(os);
+      for (const auto &searcher : searchers)
+        searcher->printName(os);
       os << "</InterleavedSearcher>\n";
     }
   };
 
-}
+} // klee namespace
 
 #endif /* KLEE_SEARCHER_H */