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.

4 files changed, 68 insertions, 9 deletions

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); }, "");
 }
 }