From 2b2b2b0e46ae260e7974f0d2738f2d23ca255874 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 9 Nov 2016 22:51:48 +0100 Subject: Fix BFS searcher For performance reasons, if KLEE branches, one state is reused and it is progressed by adding new constraints. Make sure both new states end up at the end of the BFS searcher queue. --- lib/Core/Searcher.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'lib/Core') diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 3bfcd6b3..f61ae6ec 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -104,6 +104,16 @@ ExecutionState &BFSSearcher::selectState() { void BFSSearcher::update(ExecutionState *current, const std::vector &addedStates, const std::vector &removedStates) { + // Assumption: If new states were added KLEE forked, therefore states evolved. + // constraints were added to the current state, it evolved. + if (!addedStates.empty() && current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) { + assert(states.front() == current); + states.pop_front(); + states.push_back(current); + } + states.insert(states.end(), addedStates.begin(), addedStates.end()); -- cgit 1.4.1 From d85f81ce5cf60817550f200a69923e47a8e0792c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 19 Nov 2016 20:34:23 +0000 Subject: Documented the level at which BFS operates in KLEE, as part of --help --- lib/Core/UserSearcher.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/Core') diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 0aa4a4b0..725836e8 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -22,7 +22,7 @@ namespace { cl::list CoreSearch("search", cl::desc("Specify the search heuristic (default=random-path interleaved with nurs:covnew)"), cl::values(clEnumValN(Searcher::DFS, "dfs", "use Depth First Search (DFS)"), - clEnumValN(Searcher::BFS, "bfs", "use Breadth First Search (BFS)"), + clEnumValN(Searcher::BFS, "bfs", "use Breadth First Search (BFS), where scheduling decisions are taken at the level of (2-way) forks"), clEnumValN(Searcher::RandomState, "random-state", "randomly select a state to explore"), clEnumValN(Searcher::RandomPath, "random-path", "use Random Path Selection (see OSDI'08 paper)"), clEnumValN(Searcher::NURS_CovNew, "nurs:covnew", "use Non Uniform Random Search (NURS) with Coverage-New"), -- cgit 1.4.1