MergeHandler.h File Reference

Implementation of the region based merging. More...

#include "klee/ADT/Ref.h"
#include "llvm/Support/CommandLine.h"
#include <map>
#include <stdint.h>
#include <vector>

Include dependency graph for MergeHandler.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	klee::MergeHandler
	Represents one klee_open_merge() call. Handles merging of states that branched from it. More...

Namespaces
namespace	llvm
namespace	klee

Variables
llvm::cl::opt< bool >	klee::UseMerge
llvm::cl::opt< bool >	klee::DebugLogMerge
llvm::cl::opt< bool >	klee::DebugLogIncompleteMerge

Detailed Description

Implementation of the region based merging.

Basic usage:

klee_open_merge();
 
code containing branches etc. 
 
klee_close_merge();

Will lead to all states that forked from the state that executed the klee_open_merge() being merged in the klee_close_merge(). This allows for fine-grained regions to be specified for merging.

Implementation Structure

The main part of the new functionality is implemented in the class klee::MergeHandler. The Special Function Handler generates an instance of this class every time a state runs into a klee_open_merge() call.

This instance is appended to a std::vector<klee::ref<klee::MergeHandler>> in the ExecutionState that passed the merge open point. This stack is also copied during forks. We use a stack instead of a single instance to support nested merge regions.

Once a state runs into a klee_close_merge(), the Special Function Handler notifies the top klee::MergeHandler in the state's stack, pauses the state from scheduling, and tries to merge it with all other states that already arrived at the same close merge point. This top instance is then popped from the stack, resulting in a decrease of the ref count of the klee::MergeHandler.

Since the only references to this MergeHandler are in the stacks of the ExecutionStates currently in the merging region, once the ref count 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.

Definition in file MergeHandler.h.