 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
0.0% |
0 / 15 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
0.0% |
0 / 15 |
| |
|
Line Coverage: |
33.3% |
7 / 21 |
| |
 |
|
 |
1 : //===- ExecutionState.h - --*- C++ -*-===//
2 :
3 : #ifndef KLEE_EXECUTIONSTATE_H
4 : #define KLEE_EXECUTIONSTATE_H
5 :
6 : #include "klee/Constraints.h"
7 : #include "klee/Expr.h"
8 : #include "klee/Internal/ADT/TreeStream.h"
9 :
10 : // FIXME: We do not want to be exposing these? :(
11 : #include "../../lib/Core/AddressSpace.h"
12 : #include "klee/Internal/Module/KInstIterator.h"
13 :
14 : #include <map>
15 : #include <set>
16 : #include <vector>
17 :
18 : namespace klee {
19 : class CallPathNode;
20 : class Cell;
21 : class KFunction;
22 : class KInstruction;
23 : class MemoryObject;
24 : class PTreeNode;
25 : class InstructionInfo;
26 : class ExecutionTraceEvent;
27 :
28 : std::ostream &operator<<(std::ostream &os, const MemoryMap &mm);
29 :
30 0: struct StackFrame {
31 : KInstIterator caller;
32 : KFunction *kf;
33 : CallPathNode *callPathNode;
34 :
35 : std::vector<const MemoryObject*> allocas;
36 : Cell *locals;
37 :
38 : /// Minimum distance to an uncovered instruction once the function
39 : /// returns. This is not a good place for this but is used to
40 : /// quickly compute the context sensitive minimum distance to an
41 : /// uncovered instruction. This value is updated by the StatsTracker
42 : /// periodically.
43 : unsigned minDistToUncoveredOnReturn;
44 :
45 : // For vararg functions: arguments not passed via parameter are
46 : // stored (packed tightly) in a local (alloca) memory object. This
47 : // is setup to match the way the front-end generates vaarg code (it
48 : // does not pass vaarg through as expected). VACopy is lowered inside
49 : // of intrinsic lowering.
50 : MemoryObject *varargs;
51 :
52 : StackFrame(KInstIterator caller, KFunction *kf);
53 : StackFrame(const StackFrame &s);
54 : ~StackFrame();
55 : };
56 :
57 : // for use in ExecutionState::branchInfoSequence
58 : struct BranchInfo {
59 : bool isTwoWay; // TRUE iff both sides of branch are feasible
60 : bool alreadyCoveredNew; // has this state already covered new
61 : // code by the time this branch occurs?
62 : };
63 :
64 : // FIXME: Redo execution trace stuff to use a TreeStream, there is no
65 : // need to keep this stuff in memory as far as I can tell.
66 :
67 : // each state should have only one of these guys ...
68 2803: class ExecutionTraceManager {
69 : public:
70 103: ExecutionTraceManager() : hasSeenUserMain(false) {}
71 :
72 : void addEvent(ExecutionTraceEvent* evt);
73 : void printAllEvents(std::ostream &os) const;
74 :
75 : private:
76 : // have we seen a call to __user_main() yet?
77 : // don't bother tracing anything until we see this,
78 : // or else we'll get junky prologue shit
79 : bool hasSeenUserMain;
80 :
81 : // ugh C++ only supports polymorphic calls thru pointers
82 : //
83 : // WARNING: these are NEVER FREED, because they are shared
84 : // across different states (when states fork), so we have
85 : // an *intentional* memory leak, but oh wellz ;)
86 : std::vector<ExecutionTraceEvent*> events;
87 : };
88 :
89 :
90 18213: class ExecutionState {
91 : private:
92 : // unsupported, use copy constructor
93 : ExecutionState &operator=(const ExecutionState&);
94 : std::map< std::string, std::string > fnAliases;
95 :
96 : public:
97 : bool fakeState;
98 : // Are we currently underconstrained? Hack: value is size to make fake
99 : // objects.
100 : unsigned underConstrained;
101 : unsigned depth;
102 :
103 : // pc - pointer to current instruction stream
104 : KInstIterator pc, prevPC;
105 : std::vector<StackFrame> stack;
106 : ConstraintManager constraints;
107 : mutable double queryCost;
108 : double weight;
109 : AddressSpace addressSpace;
110 : TreeOStream pathOS, symPathOS;
111 : unsigned instsSinceCovNew;
112 : bool coveredNew;
113 :
114 : // FIXME: These next three data structures are incredibly
115 : // heavyweight for what they are used for, this makes branching
116 : // O(branch-depth) instead of O(1). :(
117 : //
118 : // At the minimum, these can largely be highly-shared structures
119 : // like an ImmutableSet or an ImmutableList.
120 : //
121 : // If PG's searcher really needs this much information, we should
122 : // provide an interface so that it can manage the information itself
123 : // instead of forcing all clients to.
124 :
125 : // An ordered sequence of branches that this state took
126 : // during execution thus far:
127 : // Each element is a pair consisting of an instruction ID
128 : // corresponding to a branch and a bool corresponding to
129 : // whether the TRUE side was taken
130 : std::vector<std::pair<unsigned, bool> > branchDecisionsSequence;
131 :
132 : // Metadata about each branch taken in branchDecisionsSequence
133 : // TODO: should probably combine with branchDecisionsSequence
134 : // but too lazy to change other code for now
135 : std::vector<BranchInfo> branchInfoSequence;
136 :
137 : // contains consecutive pairs of elements of
138 : // this->branchDecisionsSequence,
139 : // implemented as an optimization for PGSearcher
140 : std::set< std::pair< std::pair<unsigned, bool>,
141 : std::pair<unsigned, bool> > > mySeenBranchPairs;
142 :
143 : // returns true iff the FINAL branch pair is in
144 : // theStatisticManager->seenBranchPairs
145 : bool isLastBranchPairSeen();
146 :
147 : // called whenever a state branches
148 : // only relevant if klee::userSearcherRequiresBranchSequences()
149 : void branchSeqHandleStateBranch(unsigned branchID, bool trueTaken,
150 : bool isTwoWay);
151 :
152 : // refer to theStatisticManager->termStatesBranchPairTally:
153 : int getBranchPairsTally();
154 :
155 : // for printing execution traces when this state terminates
156 : ExecutionTraceManager exeTraceMgr;
157 :
158 : std::pair< std::pair<unsigned, bool>,
159 : std::pair<unsigned, bool> > getLastBranchPair();
160 :
161 : /// Disables forking, set by user code.
162 : bool forkDisabled;
163 :
164 : std::map<const std::string*, std::set<unsigned> > coveredLines;
165 : PTreeNode *ptreeNode;
166 :
167 : /// ordered list of symbolics: used to generate test cases.
168 : //
169 : // FIXME: Move to a shared list structure (not critical).
170 : std::vector<const MemoryObject*> symbolics;
171 :
172 : // Used by the checkpoint/rollback methods for fake objects.
173 : // FIXME: not freeing things on branch deletion.
174 : MemoryMap shadowObjects;
175 :
176 : unsigned incomingBBIndex;
177 :
178 : std::string getFnAlias(std::string fn);
179 : void addFnAlias(std::string old_fn, std::string new_fn);
180 : void removeFnAlias(std::string fn);
181 :
182 : private:
183 : ExecutionState() : fakeState(false), underConstrained(0), ptreeNode(0) {};
184 :
185 : public:
186 : ExecutionState(KFunction *kf);
187 :
188 : // XXX total hack, just used to make a state so solver can
189 : // use on structure
190 : ExecutionState(const std::vector<ref<Expr> > &assumptions);
191 :
192 : ~ExecutionState();
193 :
194 : ExecutionState *branch();
195 :
196 : void pushFrame(KInstIterator caller, KFunction *kf);
197 : void popFrame();
198 :
199 : void addSymbolic(const MemoryObject *mo) {
200 90: symbolics.push_back(mo);
201 : }
202 1360: void addConstraint(ref<Expr> e) {
203 1360: constraints.addConstraint(e);
204 1360: }
205 :
206 : // Used for checkpoint/rollback of fake objects created during tainting.
207 : ObjectState *cloneObject(ObjectState *os, MemoryObject *mo);
208 :
209 : // revirt mo to os.
210 : void revirtClonedObject(const MemoryObject *mo, ObjectState *os);
211 :
212 : void revirtClonedObjects(void);
213 :
214 : //
215 :
216 : bool merge(const ExecutionState &b);
217 : };
218 :
219 :
220 : // for producing abbreviated execution traces to help visualize
221 : // paths and diagnose bugs
222 :
223 : class ExecutionTraceEvent {
224 : public:
225 : // the location of the instruction:
226 : std::string file;
227 : unsigned line;
228 : std::string funcName;
229 : unsigned stackDepth;
230 :
231 : unsigned consecutiveCount; // init to 1, increase for CONSECUTIVE
232 : // repetitions of the SAME event
233 :
234 : ExecutionTraceEvent()
235 : : file("global"), line(0), funcName("global_def"),
236 : consecutiveCount(1) {}
237 :
238 : ExecutionTraceEvent(ExecutionState& state, KInstruction* ki);
239 :
0: branch 2 not taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 12 not taken
0: branch 13 not taken
240 0: virtual ~ExecutionTraceEvent() {}
241 :
242 : void print(std::ostream &os) const;
243 :
244 : // return true if it shouldn't be added to ExecutionTraceManager
245 : //
246 : virtual bool ignoreMe() const;
247 :
248 : private:
249 : virtual void printDetails(std::ostream &os) const = 0;
250 : };
251 :
252 :
0: branch 2 not taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
253 0: class FunctionCallTraceEvent : public ExecutionTraceEvent {
254 : public:
255 : std::string calleeFuncName;
256 :
257 : FunctionCallTraceEvent(ExecutionState& state, KInstruction* ki,
258 : const std::string& _calleeFuncName)
259 0: : ExecutionTraceEvent(state, ki), calleeFuncName(_calleeFuncName) {}
260 :
261 : private:
262 0: virtual void printDetails(std::ostream &os) const {
263 0: os << "CALL " << calleeFuncName;
264 0: }
265 :
266 : };
267 :
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
268 0: class FunctionReturnTraceEvent : public ExecutionTraceEvent {
269 : public:
270 : FunctionReturnTraceEvent(ExecutionState& state, KInstruction* ki)
271 0: : ExecutionTraceEvent(state, ki) {}
272 :
273 : private:
274 0: virtual void printDetails(std::ostream &os) const {
275 0: os << "RETURN";
276 0: }
277 : };
278 :
0: branch 1 not taken
279 0: class BranchTraceEvent : public ExecutionTraceEvent {
280 : public:
281 : bool trueTaken; // which side taken?
282 : bool canForkGoBothWays;
283 :
284 : BranchTraceEvent(ExecutionState& state, KInstruction* ki,
285 : bool _trueTaken, bool _isTwoWay)
286 : : ExecutionTraceEvent(state, ki),
287 : trueTaken(_trueTaken),
288 0: canForkGoBothWays(_isTwoWay) {}
289 :
290 : private:
291 : virtual void printDetails(std::ostream &os) const;
292 : };
293 :
294 : }
295 :
296 : #endif
Generated: 2009-05-17 22:47 by zcov