blob: ad8ffd623b69880038e0546465ab5c9f8c61bb8e (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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();
}
}
|
