diff options
author | Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | 2017-06-24 19:59:48 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2017-11-30 12:18:15 +0000 |
commit | 60b5c574ea565b3132cc60d946d87a4d1243801b (patch) | |
tree | c7b781fe9aa8c1fdf5b4753ddaa2c694d8878b99 /lib/Core | |
parent | bc84fb1f642cbd15064c86d3839e278be536b254 (diff) | |
download | klee-60b5c574ea565b3132cc60d946d87a4d1243801b.tar.gz |
Implemented bounded merging functionality
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/CMakeLists.txt | 1 | ||||
-rw-r--r-- | lib/Core/ExecutionState.cpp | 3 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 7 | ||||
-rw-r--r-- | lib/Core/Executor.h | 4 | ||||
-rw-r--r-- | lib/Core/MergeHandler.cpp | 76 | ||||
-rw-r--r-- | lib/Core/Searcher.cpp | 5 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 41 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.h | 2 | ||||
-rw-r--r-- | lib/Core/UserSearcher.cpp | 17 |
9 files changed, 142 insertions, 14 deletions
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 86ce3cfc..4b14df36 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -8,6 +8,7 @@ #===------------------------------------------------------------------------===# klee_add_component(kleeCore AddressSpace.cpp + MergeHandler.cpp CallPathManager.cpp Context.cpp CoreStats.cpp diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 20b1a162..522bdd15 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -116,7 +116,8 @@ ExecutionState::ExecutionState(const ExecutionState& state): coveredLines(state.coveredLines), ptreeNode(state.ptreeNode), symbolics(state.symbolics), - arrayNames(state.arrayNames) + arrayNames(state.arrayNames), + openMergeStack(state.openMergeStack) { for (unsigned int i=0; i<symbolics.size(); i++) symbolics[i].first->refCount++; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e79d6a2c..be92b16a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2456,7 +2456,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { void Executor::updateStates(ExecutionState *current) { if (searcher) { searcher->update(current, addedStates, removedStates); - searcher->update(0, continuedStates, pausedStates); + searcher->update(nullptr, continuedStates, pausedStates); pausedStates.clear(); continuedStates.clear(); } @@ -2745,7 +2745,7 @@ std::string Executor::getAddressInfo(ExecutionState &state, } void Executor::pauseState(ExecutionState &state){ - std::vector<ExecutionState *>::iterator it = std::find(continuedStates.begin(), continuedStates.end(), &state); + auto it = std::find(continuedStates.begin(), continuedStates.end(), &state); // If the state was to be continued, but now gets paused again if (it != continuedStates.end()){ // ...just don't continue it @@ -2757,7 +2757,7 @@ void Executor::pauseState(ExecutionState &state){ } void Executor::continueState(ExecutionState &state){ - std::vector<ExecutionState *>::iterator it = std::find(pausedStates.begin(), pausedStates.end(), &state); + auto it = std::find(pausedStates.begin(), pausedStates.end(), &state); // If the state was to be paused, but now gets continued again if (it != pausedStates.end()){ // ...don't pause it @@ -2768,7 +2768,6 @@ void Executor::continueState(ExecutionState &state){ } } - void Executor::terminateState(ExecutionState &state) { if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c6f01179..71b1f5f7 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -69,6 +69,7 @@ namespace klee { class StatsTracker; class TimingSolver; class TreeStreamWriter; + class MergeHandler; template<class T> class ref; @@ -78,13 +79,12 @@ namespace klee { /// removedStates, and haltExecution, among others. class Executor : public Interpreter { - friend class BumpMergingSearcher; - friend class MergingSearcher; friend class RandomPathSearcher; friend class OwningSearcher; friend class WeightedRandomSearcher; friend class SpecialFunctionHandler; friend class StatsTracker; + friend class MergeHandler; public: class Timer { diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp new file mode 100644 index 00000000..ad8ffd62 --- /dev/null +++ b/lib/Core/MergeHandler.cpp @@ -0,0 +1,76 @@ +//===-- MergeHandler.cpp --------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/MergeHandler.h" + +#include "CoreStats.h" +#include "Executor.h" +#include "klee/ExecutionState.h" + +namespace klee { +llvm::cl::opt<bool> + UseMerge("use-merge", + llvm::cl::init(false), + llvm::cl::desc("Enable support for klee_open_merge() and klee_close_merge() (experimental)")); + +llvm::cl::opt<bool> + DebugLogMerge("debug-log-merge", + llvm::cl::init(false), + llvm::cl::desc("Enhanced verbosity for region based merge operations")); + +void MergeHandler::addClosedState(ExecutionState *es, + llvm::Instruction *mp) { + auto closePoint = reachedMergeClose.find(mp); + + // If no other state has yet encountered this klee_close_merge instruction, + // add a new element to the map + if (closePoint == reachedMergeClose.end()) { + reachedMergeClose[mp].push_back(es); + executor->pauseState(*es); + } else { + // Otherwise try to merge with any state in the map element for this + // instruction + auto &cpv = closePoint->second; + bool mergedSuccessful = false; + + for (auto& mState: cpv) { + if (mState->merge(*es)) { + executor->terminateState(*es); + mergedSuccessful = true; + break; + } + } + if (!mergedSuccessful) { + cpv.push_back(es); + executor->pauseState(*es); + } + } +} + +void MergeHandler::releaseStates() { + for (auto& curMergeGroup: reachedMergeClose) { + for (auto curState: curMergeGroup.second) { + executor->continueState(*curState); + } + } + reachedMergeClose.clear(); +} + +bool MergeHandler::hasMergedStates() { + return (!reachedMergeClose.empty()); +} + +MergeHandler::MergeHandler(Executor *_executor) + : executor(_executor), refCount(0) { +} + +MergeHandler::~MergeHandler() { + releaseStates(); +} +} diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index d5d35e8f..05ebe6a6 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -42,11 +42,6 @@ using namespace klee; using namespace llvm; -namespace { - cl::opt<bool> - DebugLogMerge("debug-log-merge"); -} - namespace klee { extern RNG theRNG; } diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 1c2b245c..a8d6edec 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -10,6 +10,7 @@ #include "Memory.h" #include "SpecialFunctionHandler.h" #include "TimingSolver.h" +#include "klee/MergeHandler.h" #include "klee/ExecutionState.h" @@ -28,6 +29,7 @@ #include "llvm/IR/DataLayout.h" #include <errno.h> +#include <sstream> using namespace llvm; using namespace klee; @@ -92,6 +94,8 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), add("klee_mark_global", handleMarkGlobal, false), + add("klee_open_merge", handleOpenMerge, false), + add("klee_close_merge", handleCloseMerge, false), add("klee_prefer_cex", handlePreferCex, false), add("klee_posix_prefer_cex", handlePosixPreferCex, false), add("klee_print_expr", handlePrintExpr, false), @@ -324,6 +328,43 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state, readStringAtAddress(state, arguments[3]).c_str()); } +void SpecialFunctionHandler::handleOpenMerge(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + if (!UseMerge) { + klee_warning_once(0, "klee_open_merge ignored, use '-use-merge'"); + return; + } + + state.openMergeStack.push_back( + ref<MergeHandler>(new MergeHandler(&executor))); + + if (DebugLogMerge) + llvm::errs() << "open merge: " << &state << "\n"; +} + +void SpecialFunctionHandler::handleCloseMerge(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + if (!UseMerge) { + klee_warning_once(0, "klee_close_merge ignored, use '-use-merge'"); + return; + } + Instruction *i = target->inst; + + if (DebugLogMerge) + llvm::errs() << "close merge: " << &state << " at " << i << '\n'; + + if (state.openMergeStack.empty()) { + std::ostringstream warning; + warning << &state << " ran into a close at " << i << " without a preceding open\n"; + klee_warning(warning.str().c_str()); + } else { + state.openMergeStack.back()->addClosedState(&state, i); + state.openMergeStack.pop_back(); + } +} + void SpecialFunctionHandler::handleNew(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 394b649a..7e58018f 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -116,6 +116,8 @@ namespace klee { HANDLER(handleMakeSymbolic); HANDLER(handleMalloc); HANDLER(handleMarkGlobal); + HANDLER(handleOpenMerge); + HANDLER(handleCloseMerge); HANDLER(handleNew); HANDLER(handleNewArray); HANDLER(handlePreferCex); diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 6158f722..f0b2f85a 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -13,6 +13,8 @@ #include "Executor.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/CommandLine.h" + #include "llvm/Support/CommandLine.h" using namespace llvm; @@ -58,8 +60,13 @@ namespace { void klee::initializeSearchOptions() { // default values if (CoreSearch.empty()) { - CoreSearch.push_back(Searcher::RandomPath); - CoreSearch.push_back(Searcher::NURS_CovNew); + if (UseMerge){ + CoreSearch.push_back(Searcher::NURS_CovNew); + klee_warning("--use-merge enabled. Using NURS_CovNew as default searcher."); + } else { + CoreSearch.push_back(Searcher::RandomPath); + CoreSearch.push_back(Searcher::NURS_CovNew); + } } } @@ -104,6 +111,12 @@ Searcher *klee::constructUserSearcher(Executor &executor) { searcher = new InterleavedSearcher(s); } + if (UseMerge) { + if (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end()){ + klee_error("use-merge currently does not support random-path, please use another search strategy"); + } + } + if (UseBatchingSearch) { searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions); } |