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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
|
//===-- ExecutionState.h ----------------------------------------*- C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef KLEE_EXECUTIONSTATE_H
#define KLEE_EXECUTIONSTATE_H
#include "AddressSpace.h"
#include "MemoryManager.h"
#include "MergeHandler.h"
#include "klee/ADT/ImmutableSet.h"
#include "klee/ADT/TreeStream.h"
#include "klee/Expr/Constraints.h"
#include "klee/Expr/Expr.h"
#include "klee/KDAlloc/kdalloc.h"
#include "klee/Module/KInstIterator.h"
#include "klee/Solver/Solver.h"
#include "klee/System/Time.h"
#include <map>
#include <memory>
#include <set>
#include <vector>
namespace klee {
class Array;
class CallPathNode;
struct Cell;
struct KFunction;
struct KInstruction;
class MemoryObject;
class PTreeNode;
struct InstructionInfo;
llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
struct StackFrame {
KInstIterator caller;
KFunction *kf;
CallPathNode *callPathNode;
std::vector<const MemoryObject *> allocas;
Cell *locals;
/// Minimum distance to an uncovered instruction once the function
/// returns. This is not a good place for this but is used to
/// quickly compute the context sensitive minimum distance to an
/// uncovered instruction. This value is updated by the StatsTracker
/// periodically.
unsigned minDistToUncoveredOnReturn;
// For vararg functions: arguments not passed via parameter are
// stored (packed tightly) in a local (alloca) memory object. This
// is set up to match the way the front-end generates vaarg code (it
// does not pass vaarg through as expected). VACopy is lowered inside
// of intrinsic lowering.
MemoryObject *varargs;
StackFrame(KInstIterator caller, KFunction *kf);
StackFrame(const StackFrame &s);
~StackFrame();
};
/// Contains information related to unwinding (Itanium ABI/2-Phase unwinding)
class UnwindingInformation {
public:
enum class Kind {
SearchPhase, // first phase
CleanupPhase // second phase
};
private:
const Kind kind;
public:
// _Unwind_Exception* of the thrown exception, used in both phases
ref<ConstantExpr> exceptionObject;
Kind getKind() const { return kind; }
explicit UnwindingInformation(ref<ConstantExpr> exceptionObject, Kind k)
: kind(k), exceptionObject(exceptionObject) {}
virtual ~UnwindingInformation() = default;
virtual std::unique_ptr<UnwindingInformation> clone() const = 0;
};
struct SearchPhaseUnwindingInformation : public UnwindingInformation {
// Keeps track of the stack index we have so far unwound to.
std::size_t unwindingProgress;
// MemoryObject that contains a serialized version of the last executed
// landingpad, so we can clean it up after the personality fn returns.
MemoryObject *serializedLandingpad = nullptr;
SearchPhaseUnwindingInformation(ref<ConstantExpr> exceptionObject,
std::size_t const unwindingProgress)
: UnwindingInformation(exceptionObject,
UnwindingInformation::Kind::SearchPhase),
unwindingProgress(unwindingProgress) {}
std::unique_ptr<UnwindingInformation> clone() const {
return std::make_unique<SearchPhaseUnwindingInformation>(*this);
}
static bool classof(const UnwindingInformation *u) {
return u->getKind() == UnwindingInformation::Kind::SearchPhase;
}
};
struct CleanupPhaseUnwindingInformation : public UnwindingInformation {
// Phase 1 will try to find a catching landingpad.
// Phase 2 will unwind up to this landingpad or return from
// _Unwind_RaiseException if none was found.
// The selector value of the catching landingpad that was found
// during the search phase.
ref<ConstantExpr> selectorValue;
// Used to know when we have to stop unwinding and to
// ensure that unwinding stops at the frame for which
// we first found a handler in the search phase.
const std::size_t catchingStackIndex;
CleanupPhaseUnwindingInformation(ref<ConstantExpr> exceptionObject,
ref<ConstantExpr> selectorValue,
const std::size_t catchingStackIndex)
: UnwindingInformation(exceptionObject,
UnwindingInformation::Kind::CleanupPhase),
selectorValue(selectorValue),
catchingStackIndex(catchingStackIndex) {}
std::unique_ptr<UnwindingInformation> clone() const {
return std::make_unique<CleanupPhaseUnwindingInformation>(*this);
}
static bool classof(const UnwindingInformation *u) {
return u->getKind() == UnwindingInformation::Kind::CleanupPhase;
}
};
/// @brief ExecutionState representing a path under exploration
class ExecutionState {
#ifdef KLEE_UNITTEST
public:
#else
private:
#endif
// copy ctor
ExecutionState(const ExecutionState &state);
public:
using stack_ty = std::vector<StackFrame>;
// Execution - Control Flow specific
/// @brief Pointer to instruction to be executed after the current
/// instruction
KInstIterator pc;
/// @brief Pointer to instruction which is currently executed
KInstIterator prevPC;
/// @brief Stack representing the current instruction stream
stack_ty stack;
/// @brief Remember from which Basic Block control flow arrived
/// (i.e. to select the right phi values)
std::uint32_t incomingBBIndex;
// Overall state of the state - Data specific
/// @brief Exploration depth, i.e., number of times KLEE branched for this state
std::uint32_t depth = 0;
/// @brief Address space used by this state (e.g. Global and Heap)
AddressSpace addressSpace;
/// @brief Stack allocator (used with deterministic allocation)
kdalloc::StackAllocator stackAllocator;
/// @brief Heap allocator (used with deterministic allocation)
kdalloc::Allocator heapAllocator;
/// @brief Constraints collected so far
ConstraintSet constraints;
/// Statistics and information
/// @brief Metadata utilized and collected by solvers for this state
mutable SolverQueryMetaData queryMetaData;
/// @brief History of complete path: represents branches taken to
/// reach/create this state (both concrete and symbolic)
TreeOStream pathOS;
/// @brief History of symbolic path: represents symbolic branches
/// taken to reach/create this state
TreeOStream symPathOS;
/// @brief Set containing which lines in which files are covered by this state
std::map<const std::string *, std::set<std::uint32_t>> coveredLines;
/// @brief Pointer to the process tree of the current state
/// Copies of ExecutionState should not copy ptreeNode
PTreeNode *ptreeNode = nullptr;
/// @brief Ordered list of symbolics: used to generate test cases.
//
// FIXME: Move to a shared list structure (not critical).
std::vector<std::pair<ref<const MemoryObject>, const Array *>> symbolics;
/// @brief A set of boolean expressions
/// the user has requested be true of a counterexample.
ImmutableSet<ref<Expr>> cexPreferences;
/// @brief Set of used array names for this state. Used to avoid collisions.
std::set<std::string> arrayNames;
/// @brief The objects handling the klee_open_merge calls this state ran through
std::vector<ref<MergeHandler>> openMergeStack;
/// @brief The numbers of times this state has run through Executor::stepInstruction
std::uint64_t steppedInstructions = 0;
/// @brief Counts how many instructions were executed since the last new
/// instruction was covered.
std::uint32_t instsSinceCovNew = 0;
/// @brief Keep track of unwinding state while unwinding, otherwise empty
std::unique_ptr<UnwindingInformation> unwindingInformation;
/// @brief the global state counter
static std::uint32_t nextID;
/// @brief the state id
std::uint32_t id = 0;
/// @brief Whether a new instruction was covered in this state
bool coveredNew = false;
/// @brief Disables forking for this state. Set by user code
bool forkDisabled = false;
public:
#ifdef KLEE_UNITTEST
// provide this function only in the context of unittests
ExecutionState() = default;
#endif
// only to create the initial state
explicit ExecutionState(KFunction *kf, MemoryManager *mm);
// no copy assignment, use copy constructor
ExecutionState &operator=(const ExecutionState &) = delete;
// no move ctor
ExecutionState(ExecutionState &&) noexcept = delete;
// no move assignment
ExecutionState& operator=(ExecutionState &&) noexcept = delete;
// dtor
~ExecutionState();
ExecutionState *branch();
void pushFrame(KInstIterator caller, KFunction *kf);
void popFrame();
void deallocate(const MemoryObject *mo);
void addSymbolic(const MemoryObject *mo, const Array *array);
void addConstraint(ref<Expr> e);
void addCexPreference(const ref<Expr> &cond);
bool merge(const ExecutionState &b);
void dumpStack(llvm::raw_ostream &out) const;
std::uint32_t getID() const { return id; };
void setID() { id = nextID++; };
};
struct ExecutionStateIDCompare {
bool operator()(const ExecutionState *a, const ExecutionState *b) const {
return a->getID() < b->getID();
}
};
}
#endif /* KLEE_EXECUTIONSTATE_H */
|