From 8f2bc3a7188d93edd9a131bfd2101c2ec5adab9e Mon Sep 17 00:00:00 2001 From: Lukas Wölfer Date: Thu, 5 Apr 2018 15:56:05 +0200 Subject: Improved code quality --- include/klee/MergeHandler.h | 22 +++++++++++++++++++--- lib/Core/Executor.h | 8 ++++++-- lib/Core/MergeHandler.cpp | 23 +++++++++++++---------- test/Merging/incomplete_merge.c | 20 +++++++++++++++++--- 4 files changed, 55 insertions(+), 18 deletions(-) diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h index 79357d7c..75f4a3d1 100644 --- a/include/klee/MergeHandler.h +++ b/include/klee/MergeHandler.h @@ -48,6 +48,22 @@ * reaches zero, every state which ran into the same `klee_open_merge()` is now * paused and waiting to be merged. The destructor of the MergeHandler * then continues the scheduling of the corresponding paused states. + * + * # Non-blocking State Merging + * + * This feature adds functionality to the BoundedMergingSearcher that will + * prioritize (e.g., immediately schedule) states running inside a bounded-merge + * region once a state has reached a corresponding klee_close_merge() call. The + * goal is to quickly gather all states inside the merging region in order to + * release the waiting states. However, states that are running for more than + * twice the mean number of instructions compared to the states that are already + * waiting, will not be prioritized anymore. + * + * Once no more states are available for prioritizing, but there are states + * waiting to be released, these states (which have already been merged as good as + * possible) will be continued without waiting for the remaining states. When a + * remaining state now enters a close-merge point, it will again wait for the + * other states, or until the 'timeout' is reached. */ #ifndef KLEE_MERGEHANDLER_H @@ -85,14 +101,14 @@ private: /// @brief The average number of instructions between the open and close merge of each /// state that has finished so far - double closeMean; + double closedMean; /// @brief Number of states that are tracked by this MergeHandler, that ran /// into a relevant klee_close_merge unsigned closedStateCount; /// @brief Get distance of state from the openInstruction - unsigned getInstrDistance(ExecutionState *es); + unsigned getInstructionDistance(ExecutionState *es); /// @brief States that ran through the klee_open_merge, but not yet into a /// corresponding klee_close_merge @@ -101,7 +117,7 @@ private: /// @brief Mapping the different 'klee_close_merge' calls to the states that ran into /// them std::map > - reachedMergeClose; + reachedCloseMerge; public: diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 852aaf3c..a0174ab7 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -134,10 +134,14 @@ private: std::vector timers; PTree *processTree; + /// Keeps track of all currently ongoing merges. + /// An ongoing merge is a set of states which branched from a single state + /// which ran into a klee_open_merge(), and not all states in the set have + /// reached the corresponding klee_close_merge() yet. std::vector mergeGroups; - // Set of vectors that are currently paused from scheduling because they are - // waiting to be merged in a klee_close_merge instruction + /// ExecutionStates currently paused from scheduling because they are + /// waiting to be merged in a klee_close_merge instruction std::set inCloseMerge; /// Used to track states that have been added during the current diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp index 45373002..67c24912 100644 --- a/lib/Core/MergeHandler.cpp +++ b/lib/Core/MergeHandler.cpp @@ -38,10 +38,10 @@ double MergeHandler::getMean() { if (closedStateCount == 0) return 0; - return closeMean; + return closedMean; } -unsigned MergeHandler::getInstrDistance(ExecutionState *es){ +unsigned MergeHandler::getInstructionDistance(ExecutionState *es){ return es->steppedInstructions - openInstruction; } @@ -50,7 +50,7 @@ ExecutionState *MergeHandler::getPrioritizeState(){ bool stateIsClosed = (executor->inCloseMerge.find(cur_state) != executor->inCloseMerge.end()); - if (!stateIsClosed && (getInstrDistance(cur_state) < 2 * getMean())) { + if (!stateIsClosed && (getInstructionDistance(cur_state) < 2 * getMean())) { return cur_state; } } @@ -77,18 +77,21 @@ void MergeHandler::addClosedState(ExecutionState *es, llvm::Instruction *mp) { // Update stats ++closedStateCount; - closeMean += (static_cast(getInstrDistance(es)) - closeMean) / + + // Incremental update of mean (travelling mean) + // https://math.stackexchange.com/a/1836447 + closedMean += (static_cast(getInstructionDistance(es)) - closedMean) / closedStateCount; // Remove from openStates removeOpenState(es); - auto closePoint = reachedMergeClose.find(mp); + auto closePoint = reachedCloseMerge.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); + if (closePoint == reachedCloseMerge.end()) { + reachedCloseMerge[mp].push_back(es); executor->pauseState(*es); } else { // Otherwise try to merge with any state in the map element for this @@ -111,16 +114,16 @@ void MergeHandler::addClosedState(ExecutionState *es, } void MergeHandler::releaseStates() { - for (auto& curMergeGroup: reachedMergeClose) { + for (auto& curMergeGroup: reachedCloseMerge) { for (auto curState: curMergeGroup.second) { executor->continueState(*curState); } } - reachedMergeClose.clear(); + reachedCloseMerge.clear(); } bool MergeHandler::hasMergedStates() { - return (!reachedMergeClose.empty()); + return (!reachedCloseMerge.empty()); } MergeHandler::MergeHandler(Executor *_executor, ExecutionState *es) diff --git a/test/Merging/incomplete_merge.c b/test/Merging/incomplete_merge.c index 1962cfaa..bb5e4f37 100644 --- a/test/Merging/incomplete_merge.c +++ b/test/Merging/incomplete_merge.c @@ -16,6 +16,11 @@ // CHECK: close merge: // CHECK: close merge: +// This test merges branches with vastly different instruction counts. +// The incomplete merging heuristic merges preemptively if a branch takes too long. +// It might occur that the random branch selection completes the heavy branch first, +// which results in the branches being merged completely. + #include int main(int argc, char **args) { @@ -31,15 +36,24 @@ int main(int argc, char **args) { if (a == 0) { klee_open_merge(); + for (int i = 0; i < 5; ++i){ + foo += 2; + } if (x == 1) { - foo = 5; + foo += 5; } else if (x == 2) { - foo = 6; + for (int i = 0; i < 10; ++i) { + foo += foo; + } } else { - foo = 7; + foo += 7; } klee_close_merge(); + } else if (a == 1) { + foo = 4; + } else { + foo = 3; } klee_close_merge(); -- cgit 1.4.1