From 661fba88fff0205ea258a1149907f2822458cd83 Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Thu, 25 Jun 2020 21:35:25 +0100
Subject: 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.
---
 unittests/CMakeLists.txt            |  1 +
 unittests/RNG/CMakeLists.txt        |  3 +++
 unittests/RNG/RNGTest.cpp           | 49 +++++++++++++++++++++++++++++++++++++
 unittests/Searcher/SearcherTest.cpp | 24 +++++++++++-------
 4 files changed, 68 insertions(+), 9 deletions(-)
 create mode 100644 unittests/RNG/CMakeLists.txt
 create mode 100644 unittests/RNG/RNGTest.cpp

(limited to 'unittests')

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