From d591cba305cb86ee8c520b7ff427651d8f9e0f31 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Thu, 17 Oct 2019 15:58:26 +0100 Subject: Enable subsets for RandomPathSearcher --- unittests/CMakeLists.txt | 1 + unittests/Searcher/CMakeLists.txt | 4 + unittests/Searcher/SearcherTest.cpp | 211 ++++++++++++++++++++++++++++++++++++ 3 files changed, 216 insertions(+) create mode 100644 unittests/Searcher/CMakeLists.txt create mode 100644 unittests/Searcher/SearcherTest.cpp (limited to 'unittests') 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); }, ""); +} +} -- cgit 1.4.1