Enable subsets for RandomPathSearcher

3 files changed, 216 insertions, 0 deletions

diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt
index ef052f9b..75c4d892 100644
--- a/unittests/CMakeLists.txt
+++ b/unittests/CMakeLists.txt
@@ -166,6 +166,7 @@ add_subdirectory(Assignment)
 add_subdirectory(Expr)
 add_subdirectory(Ref)
 add_subdirectory(Solver)
+add_subdirectory(Searcher)
 add_subdirectory(TreeStream)
 add_subdirectory(DiscretePDF)
 add_subdirectory(Time)
diff --git a/unittests/Searcher/CMakeLists.txt b/unittests/Searcher/CMakeLists.txt
new file mode 100644
index 00000000..29358470
--- /dev/null
+++ b/unittests/Searcher/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_klee_unit_test(SearcherTest
+  SearcherTest.cpp)
+target_link_libraries(SearcherTest PRIVATE kleeCore)
+target_include_directories(SearcherTest BEFORE PUBLIC "../../lib")
diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp
new file mode 100644
index 00000000..e9e7c043
--- /dev/null
+++ b/unittests/Searcher/SearcherTest.cpp
@@ -0,0 +1,211 @@
+//===-- SearcherTest.cpp ----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#define KLEE_UNITTEST
+
+#include "gtest/gtest.h"
+
+#include "Core/ExecutionState.h"
+#include "Core/PTree.h"
+#include "Core/Searcher.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace klee;
+
+namespace {
+
+TEST(SearcherTest, RandomPath) {
+  // First state
+  ExecutionState es;
+  PTree processTree(&es);
+  es.ptreeNode = processTree.root.getPointer();
+
+  RandomPathSearcher rp(processTree);
+  EXPECT_TRUE(rp.empty());
+
+  rp.update(nullptr, {&es}, {});
+  EXPECT_FALSE(rp.empty());
+  EXPECT_EQ(&rp.selectState(), &es);
+
+  // Two states
+  ExecutionState es1(es);
+  processTree.attach(es.ptreeNode, &es1, &es);
+  rp.update(&es, {&es1}, {});
+
+  // Random path seed dependant
+  EXPECT_EQ(&rp.selectState(), &es1);
+  EXPECT_EQ(&rp.selectState(), &es);
+  EXPECT_EQ(&rp.selectState(), &es1);
+
+  rp.update(&es, {}, {&es1});
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp.selectState(), &es);
+  }
+
+  rp.update(&es, {&es1}, {&es});
+  processTree.remove(es.ptreeNode);
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp.selectState(), &es1);
+  }
+
+  rp.update(&es1, {}, {&es1});
+  processTree.remove(es1.ptreeNode);
+  EXPECT_TRUE(rp.empty());
+}
+
+TEST(SearcherTest, TwoRandomPath) {
+  // Root state
+  ExecutionState root;
+  PTree processTree(&root);
+  root.ptreeNode = processTree.root.getPointer();
+
+  ExecutionState es(root);
+  processTree.attach(root.ptreeNode, &es, &root);
+
+  RandomPathSearcher rp(processTree);
+  RandomPathSearcher rp1(processTree);
+  EXPECT_TRUE(rp.empty());
+  EXPECT_TRUE(rp1.empty());
+
+  rp.update(nullptr, {&es}, {});
+  EXPECT_FALSE(rp.empty());
+  EXPECT_TRUE(rp1.empty());
+  EXPECT_EQ(&rp.selectState(), &es);
+
+  // Two states
+  ExecutionState es1(es);
+  processTree.attach(es.ptreeNode, &es1, &es);
+
+  rp.update(&es, {}, {});
+  rp1.update(nullptr, {&es1}, {});
+  EXPECT_FALSE(rp1.empty());
+
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp.selectState(), &es);
+    EXPECT_EQ(&rp1.selectState(), &es1);
+  }
+
+  rp.update(&es, {&es1}, {&es});
+  rp1.update(nullptr, {&es}, {&es1});
+
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp1.selectState(), &es);
+    EXPECT_EQ(&rp.selectState(), &es1);
+  }
+
+  rp1.update(&es, {}, {&es});
+  processTree.remove(es.ptreeNode);
+  EXPECT_TRUE(rp1.empty());
+  EXPECT_EQ(&rp.selectState(), &es1);
+
+  rp.update(&es1, {}, {&es1});
+  processTree.remove(es1.ptreeNode);
+  EXPECT_TRUE(rp.empty());
+  EXPECT_TRUE(rp1.empty());
+
+  processTree.remove(root.ptreeNode);
+}
+
+TEST(SearcherTest, TwoRandomPathDot) {
+  std::stringstream modelPTreeDot;
+  PTreeNode *rootPNode, *rightLeafPNode, *esParentPNode, *es1LeafPNode,
+      *esLeafPNode;
+
+  // Root state
+  ExecutionState root;
+  PTree processTree(&root);
+  root.ptreeNode = processTree.root.getPointer();
+  rootPNode = root.ptreeNode;
+
+  ExecutionState es(root);
+  processTree.attach(root.ptreeNode, &es, &root);
+  rightLeafPNode = root.ptreeNode;
+  esParentPNode = es.ptreeNode;
+
+  RandomPathSearcher rp(processTree);
+  RandomPathSearcher rp1(processTree);
+
+  rp.update(nullptr, {&es}, {});
+
+  ExecutionState es1(es);
+  processTree.attach(es.ptreeNode, &es1, &es);
+  esLeafPNode = es.ptreeNode;
+  es1LeafPNode = es1.ptreeNode;
+
+  rp.update(&es, {}, {});
+  rp1.update(nullptr, {&es1}, {});
+
+  // Compare PTree to model PTree
+  modelPTreeDot
+      << "digraph G {\n"
+      << "\tsize=\"10,7.5\";\n"
+      << "\tratio=fill;\n"
+      << "\trotate=90;\n"
+      << "\tcenter = \"true\";\n"
+      << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
+      << "\tedge [arrowsize=.3]\n"
+      << "\tn" << rootPNode << " [shape=diamond];\n"
+      << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b011];\n"
+      << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n"
+      << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << esParentPNode << " [shape=diamond];\n"
+      << "\tn" << esParentPNode << " -> n" << es1LeafPNode
+      << " [label=0b010];\n"
+      << "\tn" << esParentPNode << " -> n" << esLeafPNode << " [label=0b001];\n"
+      << "\tn" << esLeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "}\n";
+  std::string pTreeDot;
+  llvm::raw_string_ostream pTreeDotStream(pTreeDot);
+  processTree.dump(pTreeDotStream);
+  EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str());
+
+  rp.update(&es, {&es1}, {&es});
+  rp1.update(nullptr, {&es}, {&es1});
+
+  rp1.update(&es, {}, {&es});
+  processTree.remove(es.ptreeNode);
+
+  modelPTreeDot.str("");
+  modelPTreeDot
+      << "digraph G {\n"
+      << "\tsize=\"10,7.5\";\n"
+      << "\tratio=fill;\n"
+      << "\trotate=90;\n"
+      << "\tcenter = \"true\";\n"
+      << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
+      << "\tedge [arrowsize=.3]\n"
+      << "\tn" << rootPNode << " [shape=diamond];\n"
+      << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b001];\n"
+      << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n"
+      << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << esParentPNode << " [shape=diamond];\n"
+      << "\tn" << esParentPNode << " -> n" << es1LeafPNode
+      << " [label=0b001];\n"
+      << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "}\n";
+
+  pTreeDot = "";
+  processTree.dump(pTreeDotStream);
+  EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str());
+  processTree.remove(es1.ptreeNode);
+  processTree.remove(root.ptreeNode);
+}
+TEST(SearcherDeathTest, TooManyRandomPaths) {
+  // First state
+  ExecutionState es;
+  PTree processTree(&es);
+  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); }, "");
+}
+}