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
|
//===-- 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 "klee/Constraints.h"
#include "klee/Expr.h"
#include "klee/Internal/ADT/TreeStream.h"
// FIXME: We do not want to be exposing these? :(
#include "../../lib/Core/AddressSpace.h"
#include "klee/Internal/Module/KInstIterator.h"
#include <map>
#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();
};
/// @brief ExecutionState representing a path under exploration
class ExecutionState {
public:
typedef std::vector<StackFrame> stack_ty;
private:
// unsupported, use copy constructor
ExecutionState &operator=(const ExecutionState &);
std::map<std::string, std::string> fnAliases;
public:
// 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)
unsigned incomingBBIndex;
// Overall state of the state - Data specific
/// @brief Address space used by this state (e.g. Global and Heap)
AddressSpace addressSpace;
/// @brief Constraints collected so far
ConstraintManager constraints;
/// Statistics and information
/// @brief Costs for all queries issued for this state, in seconds
mutable double queryCost;
/// @brief Weight assigned for importance of this state. Can be
/// used for searchers to decide what paths to explore
double weight;
/// @brief Exploration depth, i.e., number of times KLEE branched for this state
unsigned depth;
/// @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 Counts how many instructions were executed since the last new
/// instruction was covered.
unsigned instsSinceCovNew;
/// @brief Whether a new instruction was covered in this state
bool coveredNew;
/// @brief Disables forking for this state. Set by user code
bool forkDisabled;
/// @brief Set containing which lines in which files are covered by this state
std::map<const std::string *, std::set<unsigned> > coveredLines;
/// @brief Pointer to the process tree of the current state
PTreeNode *ptreeNode;
/// @brief Ordered list of symbolics: used to generate test cases.
//
// FIXME: Move to a shared list structure (not critical).
std::vector<std::pair<const MemoryObject *, const Array *> > symbolics;
/// @brief Set of used array names for this state. Used to avoid collisions.
std::set<std::string> arrayNames;
std::string getFnAlias(std::string fn);
void addFnAlias(std::string old_fn, std::string new_fn);
void removeFnAlias(std::string fn);
private:
ExecutionState() : ptreeNode(0) {}
public:
ExecutionState(KFunction *kf);
// XXX total hack, just used to make a state so solver can
// use on structure
ExecutionState(const std::vector<ref<Expr> > &assumptions);
ExecutionState(const ExecutionState &state);
~ExecutionState();
ExecutionState *branch();
void pushFrame(KInstIterator caller, KFunction *kf);
void popFrame();
void addSymbolic(const MemoryObject *mo, const Array *array);
void addConstraint(ref<Expr> e) { constraints.addConstraint(e); }
bool merge(const ExecutionState &b);
void dumpStack(llvm::raw_ostream &out) const;
};
}
#endif
|
