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.

1 files changed, 33 insertions, 20 deletions

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;
 }