[Searchers] Remove weight from es, add nurs_depth

Having both weight and depth in execution state is wasteful,
therefore this patch removes weight.

The nurs:depth searcher is replaced by nurs:rp, which uses pow to compute
the weight

A new nurs:depth searcher is introduced that biases the search with depth,
making it the only other searcher that prefers to go deep (similar to dfs).

5 files changed, 14 insertions, 19 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 15003b0e..60715b33 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -69,7 +69,6 @@ ExecutionState::ExecutionState(KFunction *kf) :
     pc(kf->instructions),
     prevPC(pc),
 
-    weight(1),
     depth(0),
 
     instsSinceCovNew(0),
@@ -111,7 +110,6 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     constraints(state.constraints),
 
     queryCost(state.queryCost),
-    weight(state.weight),
     depth(state.depth),
 
     pathOS(state.pathOS),
@@ -141,9 +139,6 @@ ExecutionState *ExecutionState::branch() {
   falseState->coveredNew = false;
   falseState->coveredLines.clear();
 
-  weight *= .5;
-  falseState->weight -= weight;
-
   return falseState;
 }
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f90a8909..934fa43e 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2940,14 +2940,6 @@ void Executor::run(ExecutionState &initialState) {
 
     klee_message("seeding done (%d states remain)", (int) states.size());
 
-    // XXX total hack, just because I like non uniform better but want
-    // seed results to be equally weighted.
-    for (std::set<ExecutionState*>::iterator
-           it = states.begin(), ie = states.end();
-         it != ie; ++it) {
-      (*it)->weight = 1.;
-    }
-
     if (OnlySeed) {
       doDumpStates();
       return;
@@ -4113,7 +4105,6 @@ void Executor::dumpStates() {
 
       *os << "{";
       *os << "'depth' : " << es->depth << ", ";
-      *os << "'weight' : " << es->weight << ", ";
       *os << "'queryCost' : " << es->queryCost << ", ";
       *os << "'coveredNew' : " << es->coveredNew << ", ";
       *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index e576e8bc..1e9e5b9b 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -32,8 +32,9 @@
 #include "llvm/Support/CommandLine.h"
 
 #include <cassert>
-#include <fstream>
 #include <climits>
+#include <cmath>
+#include <fstream>
 
 using namespace klee;
 using namespace llvm;
@@ -168,7 +169,8 @@ WeightedRandomSearcher::WeightedRandomSearcher(WeightType _type)
   : states(new DiscretePDF<ExecutionState*>()),
     type(_type) {
   switch(type) {
-  case Depth: 
+  case Depth:
+  case RP:
     updateWeights = false;
     break;
   case InstCount:
@@ -194,8 +196,10 @@ ExecutionState &WeightedRandomSearcher::selectState() {
 double WeightedRandomSearcher::getWeight(ExecutionState *es) {
   switch(type) {
   default:
-  case Depth: 
-    return es->weight;
+  case Depth:
+    return es->depth;
+  case RP:
+    return std::pow(0.5, es->depth);
   case InstCount: {
     uint64_t count = theStatisticManager->getIndexedValue(stats::instructions,
                                                           es->pc->info->id);
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 13941af7..f1e093db 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -78,6 +78,7 @@ namespace klee {
       NURS_CovNew,
       NURS_MD2U,
       NURS_Depth,
+      NURS_RP,
       NURS_ICnt,
       NURS_CPICnt,
       NURS_QC
@@ -130,6 +131,7 @@ namespace klee {
   public:
     enum WeightType {
       Depth,
+      RP,
       QueryCost,
       InstCount,
       CPInstCount,
@@ -157,6 +159,7 @@ namespace klee {
       os << "WeightedRandomSearcher::";
       switch(type) {
       case Depth              : os << "Depth\n"; return;
+      case RP                 : os << "RandomPath\n"; return;
       case QueryCost          : os << "QueryCost\n"; return;
       case InstCount          : os << "InstCount\n"; return;
       case CPInstCount        : os << "CPInstCount\n"; return;
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 3aa07e73..22098231 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -42,7 +42,8 @@ cl::list<Searcher::CoreSearchType> CoreSearch(
                    "use Non Uniform Random Search (NURS) with Coverage-New"),
         clEnumValN(Searcher::NURS_MD2U, "nurs:md2u",
                    "use NURS with Min-Dist-to-Uncovered"),
-        clEnumValN(Searcher::NURS_Depth, "nurs:depth", "use NURS with 2^depth"),
+        clEnumValN(Searcher::NURS_Depth, "nurs:depth", "use NURS with depth"),
+        clEnumValN(Searcher::NURS_RP, "nurs:rp", "use NURS with 1/2^depth"),
         clEnumValN(Searcher::NURS_ICnt, "nurs:icnt",
                    "use NURS with Instr-Count"),
         clEnumValN(Searcher::NURS_CPICnt, "nurs:cpicnt",
@@ -114,6 +115,7 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
   case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew); break;
   case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered); break;
   case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth); break;
+  case Searcher::NURS_RP: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::RP); break;
   case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::InstCount); break;
   case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CPInstCount); break;
   case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::QueryCost); break;