introduce --rng-initial-seed=<unsigned>

* move global theRNG into Executor
* pass theRNG via ctor to searchers
* remove some type warnings from RNG.cpp

Fixes #1023.

7 files changed, 72 insertions, 52 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 041a4e6a..3dbb5a66 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -414,10 +414,6 @@ cl::opt<bool> DebugCheckForImpliedValues(
 
 } // namespace
 
-namespace klee {
-  RNG theRNG;
-}
-
 // XXX hack
 extern "C" unsigned dumpStates, dumpPTree;
 unsigned dumpStates = 0, dumpPTree = 0;
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 31882cd4..25a874cd 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -18,6 +18,7 @@
 #include "ExecutionState.h"
 #include "UserSearcher.h"
 
+#include "klee/ADT/RNG.h"
 #include "klee/Core/Interpreter.h"
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/ArrayExprOptimizer.h"
@@ -111,6 +112,9 @@ public:
     Unhandled
   };
 
+  /// The random number generator.
+  RNG theRNG;
+
 private:
   static const char *TerminateReasonNames[];
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 765784c5..d6cf8dfd 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -41,10 +41,6 @@ using namespace klee;
 using namespace llvm;
 
 
-namespace klee {
-  extern RNG theRNG;
-}
-
 Searcher::~Searcher() {
 }
 
@@ -166,9 +162,10 @@ RandomSearcher::update(ExecutionState *current,
 
 ///
 
-WeightedRandomSearcher::WeightedRandomSearcher(WeightType _type)
+WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng)
   : states(new DiscretePDF<ExecutionState*>()),
-    type(_type) {
+    theRNG{rng},
+    type(type) {
   switch(type) {
   case Depth:
   case RP:
@@ -261,8 +258,10 @@ bool WeightedRandomSearcher::empty() {
   return states->empty(); 
 }
 
-RandomPathSearcher::RandomPathSearcher(PTree &_processTree)
-    : processTree(_processTree), idBitMask(_processTree.getNextId()) {}
+///
+RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng)
+  : processTree{processTree}, theRNG{rng}, idBitMask{processTree.getNextId()} {
+}
 
 RandomPathSearcher::~RandomPathSearcher() {
 }
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index baeafd84..fa0440b8 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -11,6 +11,7 @@
 #define KLEE_SEARCHER_H
 
 #include "PTree.h"
+#include "klee/ADT/RNG.h"
 #include "klee/System/Time.h"
 
 #include "llvm/Support/CommandLine.h"
@@ -116,8 +117,10 @@ namespace klee {
 
   class RandomSearcher : public Searcher {
     std::vector<ExecutionState*> states;
+    RNG &theRNG;
 
   public:
+    explicit RandomSearcher(RNG &rng) : theRNG{rng} {}
     ExecutionState &selectState();
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
@@ -142,13 +145,14 @@ namespace klee {
 
   private:
     DiscretePDF<ExecutionState*> *states;
+    RNG &theRNG;
     WeightType type;
     bool updateWeights;
     
     double getWeight(ExecutionState*);
 
   public:
-    WeightedRandomSearcher(WeightType type);
+    WeightedRandomSearcher(WeightType type, RNG &rng);
     ~WeightedRandomSearcher();
 
     ExecutionState &selectState();
@@ -191,12 +195,13 @@ namespace klee {
   */
   class RandomPathSearcher : public Searcher {
     PTree &processTree;
+    RNG &theRNG;
 
     // Unique bitmask of this searcher
     const uint8_t idBitMask;
 
   public:
-    RandomPathSearcher(PTree &processTree);
+    RandomPathSearcher(PTree &processTree, RNG &rng);
     ~RandomPathSearcher();
 
     ExecutionState &selectState();
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 42d6b334..7acca58e 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -104,22 +104,21 @@ bool klee::userSearcherRequiresMD2U() {
 	  std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end());
 }
 
-Searcher *getNewSearcher(Searcher::CoreSearchType type, PTree &processTree) {
-  Searcher *searcher = NULL;
+
+Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &processTree) {
+  Searcher *searcher = nullptr;
   switch (type) {
-  case Searcher::DFS: searcher = new DFSSearcher(); break;
-  case Searcher::BFS: searcher = new BFSSearcher(); break;
-  case Searcher::RandomState: searcher = new RandomSearcher(); break;
-  case Searcher::RandomPath:
-    searcher = new RandomPathSearcher(processTree);
-    break;
-  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;
+    case Searcher::DFS: searcher = new DFSSearcher(); break;
+    case Searcher::BFS: searcher = new BFSSearcher(); break;
+    case Searcher::RandomState: searcher = new RandomSearcher(rng); break;
+    case Searcher::RandomPath: searcher = new RandomPathSearcher(processTree, rng); break;
+    case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew, rng); break;
+    case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered, rng); break;
+    case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth, rng); break;
+    case Searcher::NURS_RP: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::RP, rng); break;
+    case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::InstCount, rng); break;
+    case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CPInstCount, rng); break;
+    case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::QueryCost, rng); break;
   }
 
   return searcher;
@@ -127,13 +126,14 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, PTree &processTree) {
 
 Searcher *klee::constructUserSearcher(Executor &executor) {
 
-  Searcher *searcher = getNewSearcher(CoreSearch[0], *executor.processTree);
+  Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, *executor.processTree);
+
   if (CoreSearch.size() > 1) {
     std::vector<Searcher *> s;
     s.push_back(searcher);
 
     for (unsigned i = 1; i < CoreSearch.size(); i++)
-      s.push_back(getNewSearcher(CoreSearch[i], *executor.processTree));
+      s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, *executor.processTree));
 
     searcher = new InterleavedSearcher(s);
   }
diff --git a/lib/Support/ErrorHandling.cpp b/lib/Support/ErrorHandling.cpp
index 5c7b69dd..2f4bc5cc 100644
--- a/lib/Support/ErrorHandling.cpp
+++ b/lib/Support/ErrorHandling.cpp
@@ -31,8 +31,11 @@ static const char *warningOncePrefix = "WARNING ONCE";
 static const char *errorPrefix = "ERROR";
 static const char *notePrefix = "NOTE";
 
-namespace {
+namespace klee {
 cl::OptionCategory MiscCat("Miscellaneous options", "");
+}
+
+namespace {
 cl::opt<bool> WarningsOnlyToFile(
     "warnings-only-to-file", cl::init(false),
     cl::desc("All warnings will be written to warnings.txt only.  If disabled, "
diff --git a/lib/Support/RNG.cpp b/lib/Support/RNG.cpp
index 9f0824ad..a6841c5c 100644
--- a/lib/Support/RNG.cpp
+++ b/lib/Support/RNG.cpp
@@ -43,9 +43,22 @@
 */
 
 #include "klee/ADT/RNG.h"
+#include "klee/Support/OptionCategories.h"
 
 using namespace klee;
 
+namespace {
+llvm::cl::opt<unsigned> RNGInitialSeed(
+    "rng-initial-seed", llvm::cl::init(5489U),
+    llvm::cl::desc("seed value for random number generator (default=5489)"),
+    llvm::cl::cat(klee::MiscCat));
+
+}
+
+RNG::RNG() {
+  seed(RNGInitialSeed);
+}
+
 /* initializes mt[N] with a seed */
 RNG::RNG(unsigned int s) {
   seed(s);
@@ -55,7 +68,7 @@ void RNG::seed(unsigned int s) {
   mt[0]= s & 0xffffffffUL;
   for (mti=1; mti<N; mti++) {
     mt[mti] = 
-      (1812433253UL * (mt[mti-1] ^ (mt[mti-1] >> 30)) + mti); 
+      (1812433253UL * (mt[mti-1] ^ (mt[mti-1] >> 30U)) + mti);
     /* See Knuth TAOCP Vol2. 3rd Ed. P.106 for multiplier. */
     /* In the previous versions, MSBs of the seed affect   */
     /* only MSBs of the array mt[].                        */
@@ -70,38 +83,38 @@ unsigned int RNG::getInt32() {
   unsigned int y;
   static unsigned int mag01[2]={0x0UL, MATRIX_A};
   /* mag01[x] = x * MATRIX_A  for x=0,1 */
-  
+
   if (mti >= N) { /* generate N words at one time */
     int kk;
-    
+
     for (kk=0;kk<N-M;kk++) {
       y = (mt[kk]&UPPER_MASK)|(mt[kk+1]&LOWER_MASK);
-      mt[kk] = mt[kk+M] ^ (y >> 1) ^ mag01[y & 0x1UL];
+      mt[kk] = mt[kk+M] ^ (y >> 1U) ^ mag01[y & 0x1UL];
     }
     for (;kk<N-1;kk++) {
       y = (mt[kk]&UPPER_MASK)|(mt[kk+1]&LOWER_MASK);
-      mt[kk] = mt[kk+(M-N)] ^ (y >> 1) ^ mag01[y & 0x1UL];
+      mt[kk] = mt[kk+(M-N)] ^ (y >> 1U) ^ mag01[y & 0x1UL];
     }
     y = (mt[N-1]&UPPER_MASK)|(mt[0]&LOWER_MASK);
-    mt[N-1] = mt[M-1] ^ (y >> 1) ^ mag01[y & 0x1UL];
-    
+    mt[N-1] = mt[M-1] ^ (y >> 1U) ^ mag01[y & 0x1UL];
+
     mti = 0;
   }
-  
+
   y = mt[mti++];
 
   /* Tempering */
-  y ^= (y >> 11);
-  y ^= (y << 7) & 0x9d2c5680UL;
-  y ^= (y << 15) & 0xefc60000UL;
-  y ^= (y >> 18);
-  
+  y ^= (y >> 11U);
+  y ^= (y << 7U) & 0x9d2c5680UL;
+  y ^= (y << 15U) & 0xefc60000UL;
+  y ^= (y >> 18U);
+
   return y;
 }
 
 /* generates a random number on [0,0x7fffffff]-interval */
 int RNG::getInt31() {
-  return (int)(getInt32()>>1);
+  return (int)(getInt32() >> 1U);
 }
 
 /* generates a random number on [0,1]-real-interval */
@@ -137,10 +150,10 @@ float RNG::getFloat() {
 
 bool RNG::getBool() {
   unsigned bits = getInt32();
-  bits ^= bits >> 16;
-  bits ^= bits >> 8;
-  bits ^= bits >> 4;
-  bits ^= bits >> 2;
-  bits ^= bits >> 1;
-  return bits&1;
+  bits ^= bits >> 16U;
+  bits ^= bits >> 8U;
+  bits ^= bits >> 4U;
+  bits ^= bits >> 2U;
+  bits ^= bits >> 1U;
+  return bits & 1U;
 }