about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/ADT/RNG.h12
-rw-r--r--include/klee/Support/OptionCategories.h1
-rw-r--r--lib/Core/Executor.cpp4
-rw-r--r--lib/Core/Executor.h4
-rw-r--r--lib/Core/Searcher.cpp15
-rw-r--r--lib/Core/Searcher.h9
-rw-r--r--lib/Core/UserSearcher.cpp34
-rw-r--r--lib/Support/ErrorHandling.cpp5
-rw-r--r--lib/Support/RNG.cpp53
-rw-r--r--unittests/CMakeLists.txt1
-rw-r--r--unittests/RNG/CMakeLists.txt3
-rw-r--r--unittests/RNG/RNGTest.cpp49
-rw-r--r--unittests/Searcher/SearcherTest.cpp24
13 files changed, 148 insertions, 66 deletions
diff --git a/include/klee/ADT/RNG.h b/include/klee/ADT/RNG.h
index 5ea375b5..1c8eed15 100644
--- a/include/klee/ADT/RNG.h
+++ b/include/klee/ADT/RNG.h
@@ -19,16 +19,18 @@ namespace klee {
     static const unsigned int MATRIX_A = 0x9908b0dfUL;   /* constant vector a */
     static const unsigned int UPPER_MASK = 0x80000000UL; /* most significant w-r bits */
     static const unsigned int LOWER_MASK = 0x7fffffffUL; /* least significant r bits */
-      
+
   private:
     unsigned int mt[N]; /* the array for the state vector  */
     int mti;
-    
+
   public:
-    RNG(unsigned int seed=5489UL);
-  
+    RNG();
+    explicit RNG(unsigned int seed);
+
+    /* set seed value */
     void seed(unsigned int seed);
-    
+
     /* generates a random number on [0,0xffffffff]-interval */
     unsigned int getInt32();
     /* generates a random number on [0,0x7fffffff]-interval */
diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h
index 4fb7e5cb..40f3deb8 100644
--- a/include/klee/Support/OptionCategories.h
+++ b/include/klee/Support/OptionCategories.h
@@ -19,6 +19,7 @@
 namespace klee {
   extern llvm::cl::OptionCategory DebugCat;
   extern llvm::cl::OptionCategory MergeCat;
+  extern llvm::cl::OptionCategory MiscCat;
   extern llvm::cl::OptionCategory ModuleCat;
   extern llvm::cl::OptionCategory SeedingCat;
   extern llvm::cl::OptionCategory SolvingCat;
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;
 }
diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt
index 75c4d892..fbc6c256 100644
--- a/unittests/CMakeLists.txt
+++ b/unittests/CMakeLists.txt
@@ -170,6 +170,7 @@ add_subdirectory(Searcher)
 add_subdirectory(TreeStream)
 add_subdirectory(DiscretePDF)
 add_subdirectory(Time)
+add_subdirectory(RNG)
 
 # Set up lit configuration
 set (UNIT_TEST_EXE_SUFFIX "Test")
diff --git a/unittests/RNG/CMakeLists.txt b/unittests/RNG/CMakeLists.txt
new file mode 100644
index 00000000..866f9158
--- /dev/null
+++ b/unittests/RNG/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_klee_unit_test(RNGTest
+  RNGTest.cpp)
+target_link_libraries(RNGTest PRIVATE kleeSupport)
diff --git a/unittests/RNG/RNGTest.cpp b/unittests/RNG/RNGTest.cpp
new file mode 100644
index 00000000..218a15a7
--- /dev/null
+++ b/unittests/RNG/RNGTest.cpp
@@ -0,0 +1,49 @@
+#include "klee/ADT/RNG.h"
+
+#include "gtest/gtest.h"
+
+using namespace klee;
+
+/* test equality with default seed */
+TEST(RNG, InitialSeedEquality) {
+  RNG noseed;
+  RNG seed(5489U);
+
+  ASSERT_EQ(noseed.getBool(), seed.getBool());
+  ASSERT_EQ(noseed.getInt31(), seed.getInt31());
+  ASSERT_EQ(noseed.getInt32(), seed.getInt32());
+  ASSERT_EQ(noseed.getDouble(), seed.getDouble());
+  ASSERT_EQ(noseed.getDoubleL(), seed.getDoubleL());
+  ASSERT_EQ(noseed.getDoubleLR(), seed.getDoubleLR());
+  ASSERT_EQ(noseed.getFloat(), seed.getFloat());
+  ASSERT_EQ(noseed.getFloatL(), seed.getFloatL());
+  ASSERT_EQ(noseed.getFloatLR(), seed.getFloatLR());
+}
+
+
+/* test inequality with default seed */
+TEST(RNG, InitialSeedInEquality) {
+  RNG noseed;
+  RNG seed(42U);
+
+  ASSERT_NE(noseed.getInt32(), seed.getInt32());
+}
+
+
+/* test inequality with zero seed */
+TEST(RNG, InitialSeedZeroInEquality) {
+  RNG noseed;
+  RNG seed(0U);
+
+  ASSERT_NE(noseed.getInt32(), seed.getInt32());
+}
+
+
+/* test equality with seed provided by ctor and seed() */
+TEST(RNG, SeedEquality) {
+  RNG noseed;
+  noseed.seed(42U);
+  RNG seed(42U);
+
+  ASSERT_EQ(noseed.getInt32(), seed.getInt32());
+}
diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp
index e9e7c043..eff5a8af 100644
--- a/unittests/Searcher/SearcherTest.cpp
+++ b/unittests/Searcher/SearcherTest.cpp
@@ -10,9 +10,11 @@
 
 #include "gtest/gtest.h"
 
+#include "klee/ADT/RNG.h"
 #include "Core/ExecutionState.h"
 #include "Core/PTree.h"
 #include "Core/Searcher.h"
+
 #include "llvm/Support/raw_ostream.h"
 
 using namespace klee;
@@ -25,7 +27,8 @@ TEST(SearcherTest, RandomPath) {
   PTree processTree(&es);
   es.ptreeNode = processTree.root.getPointer();
 
-  RandomPathSearcher rp(processTree);
+  RNG rng;
+  RandomPathSearcher rp(processTree, rng);
   EXPECT_TRUE(rp.empty());
 
   rp.update(nullptr, {&es}, {});
@@ -67,8 +70,9 @@ TEST(SearcherTest, TwoRandomPath) {
   ExecutionState es(root);
   processTree.attach(root.ptreeNode, &es, &root);
 
-  RandomPathSearcher rp(processTree);
-  RandomPathSearcher rp1(processTree);
+  RNG rng, rng1;
+  RandomPathSearcher rp(processTree, rng);
+  RandomPathSearcher rp1(processTree, rng1);
   EXPECT_TRUE(rp.empty());
   EXPECT_TRUE(rp1.empty());
 
@@ -127,8 +131,9 @@ TEST(SearcherTest, TwoRandomPathDot) {
   rightLeafPNode = root.ptreeNode;
   esParentPNode = es.ptreeNode;
 
-  RandomPathSearcher rp(processTree);
-  RandomPathSearcher rp1(processTree);
+  RNG rng;
+  RandomPathSearcher rp(processTree, rng);
+  RandomPathSearcher rp1(processTree, rng);
 
   rp.update(nullptr, {&es}, {});
 
@@ -203,9 +208,10 @@ TEST(SearcherDeathTest, TooManyRandomPaths) {
   es.ptreeNode = processTree.root.getPointer();
   processTree.remove(es.ptreeNode); // Need to remove to avoid leaks
 
-  RandomPathSearcher rp(processTree);
-  RandomPathSearcher rp1(processTree);
-  RandomPathSearcher rp2(processTree);
-  ASSERT_DEATH({ RandomPathSearcher rp3(processTree); }, "");
+  RNG rng;
+  RandomPathSearcher rp(processTree, rng);
+  RandomPathSearcher rp1(processTree, rng);
+  RandomPathSearcher rp2(processTree, rng);
+  ASSERT_DEATH({ RandomPathSearcher rp3(processTree, rng); }, "");
 }
 }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-21 22:10:38 +0000