 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
50.0% |
2 / 4 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
100.0% |
4 / 4 |
| |
|
Line Coverage: |
46.4% |
13 / 28 |
| |
 |
|
 |
1 : //===- Executor.h - --*- C++ -*-===//
2 : //
3 : // Klee
4 : //
5 : //===---------------------------===//
6 : //
7 : // Class to perform actual execution, hides implementation details
8 : // from external interpreter.
9 : //
10 : //===--------------------------===//
11 :
12 : #ifndef KLEE_EXECUTOR_H
13 : #define KLEE_EXECUTOR_H
14 :
15 : #include "klee/Interpreter.h"
16 : #include "llvm/Support/CallSite.h"
17 : #include <vector>
18 : #include <string>
19 : #include <map>
20 : #include <set>
21 :
22 : struct BOut;
23 :
24 : namespace llvm {
25 : class BasicBlock;
26 : class BranchInst;
27 : class CallInst;
28 : class Constant;
29 : class ConstantExpr;
30 : class Function;
31 : class GlobalValue;
32 : class Instruction;
33 : class TargetData;
34 : class Value;
35 : }
36 :
37 : namespace klee {
38 : class ExecutionState;
39 : class ExternalDispatcher;
40 : class Expr;
41 : class InstructionInfoTable;
42 : class KFunction;
43 : class KInstruction;
44 : class KInstIterator;
45 : class KModule;
46 : class MemoryManager;
47 : class MemoryObject;
48 : class ObjectState;
49 : class PTree;
50 : class Searcher;
51 : class SeedInfo;
52 : class SpecialFunctionHandler;
53 : class StackFrame;
54 : class StatsTracker;
55 : class TimingSolver;
56 : class TreeStreamWriter;
57 : template<class T> class ref;
58 :
59 : /// \todo Add a context object to keep track of data only live
60 : /// during an instruction step. Should contain addedStates,
61 : /// removedStates, and haltExecution, among others.
62 :
63 : class Executor : public Interpreter {
64 : friend class BumpMergingSearcher;
65 : friend class MergingSearcher;
66 : friend class RandomPathSearcher;
67 : friend class OwningSearcher;
68 : friend class WeightedRandomSearcher;
69 : friend class SpecialFunctionHandler;
70 : friend class StatsTracker;
71 :
72 : public:
73 : class Timer {
74 : public:
75 : Timer();
76 : virtual ~Timer();
77 :
78 : /// The event callback.
79 : virtual void run() = 0;
80 : };
81 :
82 : typedef std::pair<ExecutionState*,ExecutionState*> StatePair;
83 :
84 : private:
85 : class TimerInfo;
86 :
87 : KModule *kmodule;
88 : InterpreterHandler *interpreterHandler;
89 : Searcher *searcher;
90 :
91 : ExternalDispatcher *externalDispatcher;
92 : TimingSolver *solver;
93 : MemoryManager *memory;
94 : std::set<ExecutionState*> states;
95 : StatsTracker *statsTracker;
96 : TreeStreamWriter *pathWriter, *symPathWriter;
97 : SpecialFunctionHandler *specialFunctionHandler;
98 : std::vector<TimerInfo*> timers;
99 : PTree *processTree;
100 :
101 : /// Used to track states that have been added during the current
102 : /// instructions step.
103 : /// \invariant \ref addedStates is a subset of \ref states.
104 : /// \invariant \ref addedStates and \ref removedStates are disjoint.
105 : std::set<ExecutionState*> addedStates;
106 : /// Used to track states that have been removed during the current
107 : /// instructions step.
108 : /// \invariant \ref removedStates is a subset of \ref states.
109 : /// \invariant \ref addedStates and \ref removedStates are disjoint.
110 : std::set<ExecutionState*> removedStates;
111 :
112 : /// When non-empty the Executor is running in "seed" mode. The
113 : /// states in this map will be executed in an arbitrary order
114 : /// (outside the normal search interface) until they terminate. When
115 : /// the states reach a symbolic branch then either direction that
116 : /// satisfies one or more seeds will be added to this map. What
117 : /// happens with other states (that don't satisfy the seeds) depends
118 : /// on as-yet-to-be-determined flags.
119 : std::map<ExecutionState*, std::vector<SeedInfo> > seedMap;
120 :
121 : /// Map of globals to their representative memory object.
122 : std::map<const llvm::GlobalValue*, MemoryObject*> globalObjects;
123 :
124 : /// Map of globals to their bound address. This also includes
125 : /// globals that have no representative object (i.e. functions).
126 : std::map<const llvm::GlobalValue*, ref<Expr> > globalAddresses;
127 :
128 : /// The set of legal function addresses, used to validate function
129 : /// pointers.
130 : std::set<void*> legalFunctions;
131 :
132 : /// When non-null the bindings that will be used for calls to
133 : /// klee_make_symbolic in order replay.
134 : const struct BOut *replayOut;
135 : /// When non-null a list of branch decisions to be used for replay.
136 : const std::vector<bool> *replayPath;
137 : /// The index into the current \ref replayOut or \ref replayPath
138 : /// object.
139 : unsigned replayPosition;
140 :
141 : /// When non-null a list of "seed" inputs which will be used to
142 : /// drive execution.
143 : const std::vector<struct BOut *> *usingSeeds;
144 :
145 : /// Disables forking, instead a random path is chosen. Enabled as
146 : /// needed to control memory usage. \see fork()
147 : bool atMemoryLimit;
148 :
149 : /// Disables forking, set by client. \see setInhibitForking()
150 : bool inhibitForking;
151 :
152 : /// Signals the executor to halt execution at the next instruction
153 : /// step.
154 : bool haltExecution;
155 :
156 : /// Whether implied-value concretization is enabled. Currently
157 : /// false, it is buggy (it needs to validate its writes).
158 : bool ivcEnabled;
159 :
160 : /// The maximum time to allow for a single stp query.
161 : double stpTimeout;
162 :
163 : llvm::Function* getCalledFunction(llvm::CallSite &cs, ExecutionState &state);
164 :
165 : void executeInstruction(ExecutionState &state, KInstruction *ki);
166 :
167 : void printFileLine(ExecutionState &state, KInstruction *ki);
168 :
169 : void run(ExecutionState &initialState);
170 :
171 : // Given a concrete object in our [klee's] address space, add it to
172 : // objects checked code can reference.
173 : MemoryObject *addExternalObject(ExecutionState &state, void *addr, unsigned size, MemoryObject *referent, bool isReadOnly);
174 :
175 : MemoryObject *lazyAllocate(ExecutionState &state, ref<Expr> base, llvm::Value *ptr);
176 : MemoryObject *recoverReferent(ExecutionState &state, ref<Expr> base, llvm::Value *ptr);
177 :
178 : void initializeGlobalObject(ExecutionState &state, ObjectState *os,
179 : llvm::Constant *c,
180 : unsigned offset);
181 : void initializeGlobals(ExecutionState &state);
182 :
183 : void stepInstruction(ExecutionState &state);
184 : void updateStates(ExecutionState *current);
185 : void transferToBasicBlock(llvm::BasicBlock *dst,
186 : llvm::BasicBlock *src,
187 : ExecutionState &state);
188 :
189 : void callExternalFunction(ExecutionState &state,
190 : KInstruction *target,
191 : llvm::Function *function,
192 : std::vector< ref<Expr> > &arguments);
193 :
194 : ObjectState *bindObjectInState(ExecutionState &state, const MemoryObject *mo,
195 : bool isLocal);
196 :
197 : /// Resolve a pointer to the memory objects it could point to the
198 : /// start of, forking execution when necessary and generating errors
199 : /// for pointers to invalid locations (either out of bounds or
200 : /// address inside the middle of objects).
201 : ///
202 : /// \param results[out] A list of ((MemoryObject,ObjectState),
203 : /// state) pairs for each object the given address can point to the
204 : /// beginning of.
205 : typedef std::vector< std::pair<std::pair<const MemoryObject*, const ObjectState*>,
206 : ExecutionState*> > ExactResolutionList;
207 : void resolveExact(ExecutionState &state,
208 : ref<Expr> p,
209 : ExactResolutionList &results,
210 : const std::string &name);
211 :
212 : /// Allocate and bind a new object in a particular state. NOTE: This
213 : /// function may fork.
214 : ///
215 : /// \param isLocal Flag to indicate if the object should be
216 : /// automatically deallocated on function return (this also makes it
217 : /// illegal to free directly).
218 : ///
219 : /// \param target Value at which to bind the base address of the new
220 : /// object.
221 : ///
222 : /// \param reallocFrom If non-zero and the allocation succeeds,
223 : /// initialize the new object from the given one and unbind it when
224 : /// done (realloc semantics). The initialized bytes will be the
225 : /// minimum of the size of the old and new objects, with remaining
226 : /// bytes initialized as specified by zeroMemory.
227 : void executeAlloc(ExecutionState &state,
228 : ref<Expr> size,
229 : bool isLocal,
230 : KInstruction *target,
231 : bool zeroMemory=false,
232 : const ObjectState *reallocFrom=0);
233 :
234 : /// XXX not for public use (this is for histar, it allocations a
235 : /// contiguous set of objects, while guaranteeing page alignment)
236 : void executeAllocN(ExecutionState &state,
237 : uint64_t nelems,
238 : uint64_t size,
239 : uint64_t alignment,
240 : bool isLocal,
241 : KInstruction *target);
242 :
243 : /// Free the given address with checking for errors. If target is
244 : /// given it will be bound to 0 in the resulting states (this is a
245 : /// convenience for realloc). Note that this function can cause the
246 : /// state to fork and that \ref state cannot be safely accessed
247 : /// afterwards.
248 : void executeFree(ExecutionState &state,
249 : ref<Expr> address,
250 : KInstruction *target = 0);
251 :
252 : void executeCall(ExecutionState &state,
253 : KInstruction *ki,
254 : llvm::Function *f,
255 : std::vector< ref<Expr> > &arguments,
256 : const std::vector<MemoryObject*> &argReferents);
257 :
258 : // do address resolution / object binding / out of bounds checking
259 : // and perform the operation
260 : void executeMemoryOperation(ExecutionState &state,
261 : bool isWrite,
262 : ref<Expr> address,
263 : MemoryObject *addressReferent,
264 : ref<Expr> value /* undef if read */,
265 : MemoryObject *valueReferent,
266 : KInstruction *target /* undef if write */);
267 :
268 : void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo);
269 :
270 : #ifdef KLEE_TRACK_REFERENTS
271 : void writeReferent(ExecutionState &state, ObjectState *os, ref<Expr> address, MemoryObject *mo);
272 :
273 : #else
274 : # define writeReferent(_state, _os, _addr, _mo) do { } while(0)
275 : #endif
276 :
277 : /// Create a new state where each input condition has been added as
278 : /// a constraint and return the results. The input state is included
279 : /// as one of the results. Note that the output vector may included
280 : /// NULL pointers for states which were unable to be created.
281 : void branch(ExecutionState &state,
282 : const std::vector< ref<Expr> > &conditions,
283 : std::vector<ExecutionState*> &result);
284 :
285 : // Fork current and return states in which condition holds / does
286 : // not hold, respectively. One of the states is necessarily the
287 : // current state, and one of the states may be null.
288 : StatePair fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal);
289 :
290 : /// Add the given (boolean) condition as a constraint on state. This
291 : /// function is a wrapper around the state's addConstraint function
292 : /// which also manages manages propogation of implied values,
293 : /// validity checks, and seed patching.
294 : void addConstraint(ExecutionState &state, ref<Expr> condition);
295 :
296 : // Called on [for now] concrete reads, replaces constant with a symbolic
297 : // Used for testing.
298 : ref<Expr> replaceReadWithSymbolic(ExecutionState &state, ref<Expr> e);
299 :
300 : ref<Expr> eval(KInstruction *ki,
301 : unsigned index,
302 : ExecutionState &state,
303 : MemoryObject **referent=0);
304 :
305 : void bindLocal(KInstruction *target,
306 : ExecutionState &state,
307 : ref<Expr> value,
308 : MemoryObject *referent=0);
309 : void bindArgument(KFunction *kf,
310 : unsigned index,
311 : ExecutionState &state,
312 : ref<Expr> value,
313 : MemoryObject *referent=0);
314 :
315 : ref<Expr> evalConstantExpr(llvm::ConstantExpr *ce, MemoryObject **referent = 0);
316 :
317 : /// Return a unique constant value for the given expression in the
318 : /// given state, if it has one (i.e. it provably only has a single
319 : /// value). Otherwise return the original expression.
320 : ref<Expr> toUnique(const ExecutionState &state, ref<Expr> &e);
321 :
322 : /// Return a constant value for the given expression, forcing it to
323 : /// be constant in the given state by adding a constraint if
324 : /// necessary. Note that this function breaks completeness and
325 : /// should generally be avoided.
326 : ///
327 : /// \param purpose An identify string to printed in case of concretization.
328 : ref<Expr> toConstant(ExecutionState &state, ref<Expr> e, const char *purpose);
329 :
330 : /// Bind a constant value for e to the given target. NOTE: This
331 : /// function may fork state if the state has multiple seeds.
332 : void executeGetValue(ExecutionState &state, ref<Expr> e, KInstruction *target);
333 :
334 : /// Get textual information regarding a memory address.
335 : std::string getAddressInfo(ExecutionState &state, ref<Expr> address) const;
336 :
337 : // remove state from queue and delete
338 : void terminateState(ExecutionState &state);
339 : // call exit handler and terminate state
340 : void terminateStateEarly(ExecutionState &state, std::string message);
341 : // call exit handler and terminate state
342 : void terminateStateOnExit(ExecutionState &state);
343 : // call error handler and terminate state
344 : void terminateStateOnError(ExecutionState &state,
345 : const std::string &message,
346 : const std::string &suffix,
347 : const std::string &longMessage="");
348 :
349 : // call error handler and terminate state, for execution errors
350 : // (things that should not be possible, like illegal instruction or
351 : // unlowered instrinsic, or are unsupported, like inline assembly)
352 : void terminateStateOnExecError(ExecutionState &state,
353 : const std::string &message,
354 0: const std::string &info="") {
355 0: terminateStateOnError(state, message, "exec.err", info);
356 0: }
357 :
358 : /// bindModuleConstants - Initialize the module constant table.
359 : void bindModuleConstants();
360 :
361 : /// bindInstructionConstants - Initialize any necessary per instruction
362 : /// constant values.
363 : void bindInstructionConstants(KInstruction *KI);
364 :
365 : void handlePointsToObj(ExecutionState &state,
366 : KInstruction *target,
367 : const std::vector<ref<Expr> > &arguments,
368 : const std::vector< MemoryObject * > &argReferent);
369 :
370 : void doImpliedValueConcretization(ExecutionState &state,
371 : ref<Expr> e,
372 : ref<Expr> value);
373 :
374 : /// Add a timer to be executed periodically.
375 : ///
376 : /// \param timer The timer object to run on firings.
377 : /// \param rate The approximate delay (in seconds) between firings.
378 : void addTimer(Timer *timer, double rate);
379 :
380 : void initTimers();
381 : void processTimers(ExecutionState *current,
382 : double maxInstTime);
383 :
384 : public:
385 : Executor(const InterpreterOptions &opts, InterpreterHandler *ie);
386 : virtual ~Executor();
387 :
388 : // XXX should just be moved out to utility module
389 : ref<Expr> evalConstant(llvm::Constant *c, MemoryObject **referent=0);
390 :
391 0: virtual void setPathWriter(TreeStreamWriter *tsw) {
392 0: pathWriter = tsw;
393 0: }
394 0: virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) {
395 0: symPathWriter = tsw;
396 0: }
397 :
398 2: virtual void setReplayOut(const struct BOut *out) {
0: branch 0 not taken
2: branch 1 taken
399 2: assert(!replayPath && "cannot replay both buffer and path");
400 2: replayOut = out;
401 2: replayPosition = 0;
402 2: }
403 :
404 1: virtual void setReplayPath(const std::vector<bool> *path) {
0: branch 0 not taken
1: branch 1 taken
405 1: assert(!replayOut && "cannot replay both buffer and path");
406 1: replayPath = path;
407 1: replayPosition = 0;
408 1: }
409 :
410 : virtual const llvm::Module *
411 : setModule(llvm::Module *module,
412 : const ModuleOptions &opts,
413 : const std::vector<std::string> &excludeCovFiles);
414 :
415 1: virtual void useSeeds(const std::vector<struct BOut *> *seeds) {
416 1: usingSeeds = seeds;
417 1: }
418 :
419 : virtual void runFunctionAsMain(llvm::Function *f,
420 : int argc,
421 : char **argv,
422 : char **envp);
423 :
424 : /*** Runtime options ***/
425 :
426 0: virtual void setHaltExecution(bool value) {
427 0: haltExecution = value;
428 0: }
429 :
430 0: virtual void setInhibitForking(bool value) {
431 0: inhibitForking = value;
432 0: }
433 :
434 : /*** State accessor methods ***/
435 :
436 : virtual unsigned getPathStreamID(const ExecutionState &state);
437 :
438 : virtual unsigned getSymbolicPathStreamID(const ExecutionState &state);
439 :
440 : virtual void getConstraintLog(const ExecutionState &state,
441 : std::string &res,
442 : bool asCVC = false);
443 :
444 : virtual bool getSymbolicSolution(const ExecutionState &state,
445 : std::vector<
446 : std::pair<std::string,
447 : std::vector<unsigned char> > >
448 : &res);
449 :
450 : virtual void getCoveredLines(const ExecutionState &state,
451 : std::map<const std::string*, std::set<unsigned> > &res);
452 : };
453 :
454 : // utility function.
455 : MemoryObject *selectReferent(MemoryObject *r1, MemoryObject *r2);
456 :
457 : } // End klee namespace
458 :
459 : #endif
Generated: 2009-05-17 22:47 by zcov