diff options
author | Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | 2017-06-24 19:31:04 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-05-15 15:18:36 +0100 |
commit | e5a18f47a8cdd37a5c2721e89df68ea7aafed8a0 (patch) | |
tree | 620bd0ab0ce7f737db5ab7f8f656d32ea0849f4a /lib/Core/MergeHandler.cpp | |
parent | 0cf0150da0f674c85f9eaccee8b487ed004c3edc (diff) | |
download | klee-e5a18f47a8cdd37a5c2721e89df68ea7aafed8a0.tar.gz |
Implemented incomplete merging
Diffstat (limited to 'lib/Core/MergeHandler.cpp')
-rw-r--r-- | lib/Core/MergeHandler.cpp | 69 |
1 files changed, 67 insertions, 2 deletions
diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp index ad8ffd62..45373002 100644 --- a/lib/Core/MergeHandler.cpp +++ b/lib/Core/MergeHandler.cpp @@ -24,8 +24,65 @@ llvm::cl::opt<bool> llvm::cl::init(false), llvm::cl::desc("Enhanced verbosity for region based merge operations")); +llvm::cl::opt<bool> + UseIncompleteMerge("use-incomplete-merge", + llvm::cl::init(false), + llvm::cl::desc("Heuristic based merging")); + +llvm::cl::opt<bool> + DebugLogIncompleteMerge("debug-log-incomplete-merge", + llvm::cl::init(false), + llvm::cl::desc("Debug info about incomplete merging")); + +double MergeHandler::getMean() { + if (closedStateCount == 0) + return 0; + + return closeMean; +} + +unsigned MergeHandler::getInstrDistance(ExecutionState *es){ + return es->steppedInstructions - openInstruction; +} + +ExecutionState *MergeHandler::getPrioritizeState(){ + for (ExecutionState *cur_state : openStates) { + bool stateIsClosed = (executor->inCloseMerge.find(cur_state) != + executor->inCloseMerge.end()); + + if (!stateIsClosed && (getInstrDistance(cur_state) < 2 * getMean())) { + return cur_state; + } + } + return 0; +} + + +void MergeHandler::addOpenState(ExecutionState *es){ + openStates.push_back(es); +} + +void MergeHandler::removeOpenState(ExecutionState *es){ + auto it = std::find(openStates.begin(), openStates.end(), es); + assert(it != openStates.end()); + std::swap(*it, openStates.back()); + openStates.pop_back(); +} + +void MergeHandler::removeFromCloseMergeSet(ExecutionState *es){ + executor->inCloseMerge.erase(es); +} + void MergeHandler::addClosedState(ExecutionState *es, llvm::Instruction *mp) { + // Update stats + ++closedStateCount; + closeMean += (static_cast<double>(getInstrDistance(es)) - closeMean) / + closedStateCount; + + // Remove from openStates + removeOpenState(es); + auto closePoint = reachedMergeClose.find(mp); // If no other state has yet encountered this klee_close_merge instruction, @@ -66,11 +123,19 @@ bool MergeHandler::hasMergedStates() { return (!reachedMergeClose.empty()); } -MergeHandler::MergeHandler(Executor *_executor) - : executor(_executor), refCount(0) { +MergeHandler::MergeHandler(Executor *_executor, ExecutionState *es) + : executor(_executor), openInstruction(es->steppedInstructions), + closedStateCount(0), refCount(0) { + executor->mergeGroups.push_back(this); + addOpenState(es); } MergeHandler::~MergeHandler() { + auto it = std::find(executor->mergeGroups.begin(), + executor->mergeGroups.end(), this); + std::swap(*it, executor->mergeGroups.back()); + executor->mergeGroups.pop_back(); + releaseStates(); } } |