klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Executor.h
Go to the documentation of this file.
1 //===-- Executor.h ----------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 //
10 // Class to perform actual execution, hides implementation details from external
11 // interpreter.
12 //
13 //===----------------------------------------------------------------------===//
14 
15 #ifndef KLEE_EXECUTOR_H
16 #define KLEE_EXECUTOR_H
17 
18 #include "klee/ExecutionState.h"
19 #include "klee/Interpreter.h"
23 #include "llvm/Support/CallSite.h"
24 #include <vector>
25 #include <string>
26 #include <map>
27 #include <set>
28 
29 struct KTest;
30 
31 namespace llvm {
32  class BasicBlock;
33  class BranchInst;
34  class CallInst;
35  class Constant;
36  class ConstantExpr;
37  class Function;
38  class GlobalValue;
39  class Instruction;
40 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
41  class TargetData;
42 #else
43  class DataLayout;
44 #endif
45  class Twine;
46  class Value;
47 }
48 
49 namespace klee {
50  class Array;
51  struct Cell;
52  class ExecutionState;
53  class ExternalDispatcher;
54  class Expr;
55  class InstructionInfoTable;
56  struct KFunction;
57  struct KInstruction;
58  class KInstIterator;
59  class KModule;
60  class MemoryManager;
61  class MemoryObject;
62  class ObjectState;
63  class PTree;
64  class Searcher;
65  class SeedInfo;
66  class SpecialFunctionHandler;
67  struct StackFrame;
68  class StatsTracker;
69  class TimingSolver;
70  class TreeStreamWriter;
71  template<class T> class ref;
72 
73 
74 
78 
79 class Executor : public Interpreter {
80  friend class BumpMergingSearcher;
81  friend class MergingSearcher;
82  friend class RandomPathSearcher;
83  friend class OwningSearcher;
84  friend class WeightedRandomSearcher;
85  friend class SpecialFunctionHandler;
86  friend class StatsTracker;
87 
88 public:
89  class Timer {
90  public:
91  Timer();
92  virtual ~Timer();
93 
95  virtual void run() = 0;
96  };
97 
98  typedef std::pair<ExecutionState*,ExecutionState*> StatePair;
99 
100 private:
101  class TimerInfo;
102 
103  KModule *kmodule;
106 
110  std::set<ExecutionState*> states;
114  std::vector<TimerInfo*> timers;
116 
121  std::set<ExecutionState*> addedStates;
126  std::set<ExecutionState*> removedStates;
127 
135  std::map<ExecutionState*, std::vector<SeedInfo> > seedMap;
136 
138  std::map<const llvm::GlobalValue*, MemoryObject*> globalObjects;
139 
142  std::map<const llvm::GlobalValue*, ref<ConstantExpr> > globalAddresses;
143 
146  std::set<uint64_t> legalFunctions;
147 
150  const struct KTest *replayOut;
152  const std::vector<bool> *replayPath;
155  unsigned replayPosition;
156 
159  const std::vector<struct KTest *> *usingSeeds;
160 
164 
167 
171 
175 
179 
180  llvm::Function* getTargetFunction(llvm::Value *calledVal,
181  ExecutionState &state);
182 
184 
185  void printFileLine(ExecutionState &state, KInstruction *ki);
186 
187  void run(ExecutionState &initialState);
188 
189  // Given a concrete object in our [klee's] address space, add it to
190  // objects checked code can reference.
191  MemoryObject *addExternalObject(ExecutionState &state, void *addr,
192  unsigned size, bool isReadOnly);
193 
195  const llvm::Constant *c,
196  unsigned offset);
197  void initializeGlobals(ExecutionState &state);
198 
199  void stepInstruction(ExecutionState &state);
200  void updateStates(ExecutionState *current);
201  void transferToBasicBlock(llvm::BasicBlock *dst,
202  llvm::BasicBlock *src,
203  ExecutionState &state);
204 
206  KInstruction *target,
207  llvm::Function *function,
208  std::vector< ref<Expr> > &arguments);
209 
211  bool isLocal, const Array *array = 0);
212 
221  typedef std::vector< std::pair<std::pair<const MemoryObject*, const ObjectState*>,
223  void resolveExact(ExecutionState &state,
224  ref<Expr> p,
225  ExactResolutionList &results,
226  const std::string &name);
227 
243  void executeAlloc(ExecutionState &state,
244  ref<Expr> size,
245  bool isLocal,
246  KInstruction *target,
247  bool zeroMemory=false,
248  const ObjectState *reallocFrom=0);
249 
255  void executeFree(ExecutionState &state,
256  ref<Expr> address,
257  KInstruction *target = 0);
258 
259  void executeCall(ExecutionState &state,
260  KInstruction *ki,
261  llvm::Function *f,
262  std::vector< ref<Expr> > &arguments);
263 
264  // do address resolution / object binding / out of bounds checking
265  // and perform the operation
267  bool isWrite,
268  ref<Expr> address,
269  ref<Expr> value /* undef if read */,
270  KInstruction *target /* undef if write */);
271 
272  void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo,
273  const std::string &name);
274 
279  void branch(ExecutionState &state,
280  const std::vector< ref<Expr> > &conditions,
281  std::vector<ExecutionState*> &result);
282 
283  // Fork current and return states in which condition holds / does
284  // not hold, respectively. One of the states is necessarily the
285  // current state, and one of the states may be null.
286  StatePair fork(ExecutionState &current, ref<Expr> condition, bool isInternal);
287 
292  void addConstraint(ExecutionState &state, ref<Expr> condition);
293 
294  // Called on [for now] concrete reads, replaces constant with a symbolic
295  // Used for testing.
297 
298  const Cell& eval(KInstruction *ki, unsigned index,
299  ExecutionState &state) const;
300 
302  KFunction *kf,
303  unsigned index) {
304  return state.stack.back().locals[kf->getArgRegister(index)];
305  }
306 
308  KInstruction *target) {
309  return state.stack.back().locals[target->dest];
310  }
311 
312  void bindLocal(KInstruction *target,
313  ExecutionState &state,
314  ref<Expr> value);
315  void bindArgument(KFunction *kf,
316  unsigned index,
317  ExecutionState &state,
318  ref<Expr> value);
319 
320  ref<klee::ConstantExpr> evalConstantExpr(const llvm::ConstantExpr *ce);
321 
325  ref<Expr> toUnique(const ExecutionState &state, ref<Expr> &e);
326 
334  const char *purpose);
335 
338  void executeGetValue(ExecutionState &state, ref<Expr> e, KInstruction *target);
339 
341  std::string getAddressInfo(ExecutionState &state, ref<Expr> address) const;
342 
343  // Determines the \param lastInstruction of the \param state which is not KLEE
344  // internal and returns its InstructionInfo
346  llvm::Instruction** lastInstruction);
347 
348  // remove state from queue and delete
349  void terminateState(ExecutionState &state);
350  // call exit handler and terminate state
351  void terminateStateEarly(ExecutionState &state, const llvm::Twine &message);
352  // call exit handler and terminate state
354  // call error handler and terminate state
356  const llvm::Twine &message,
357  const char *suffix,
358  const llvm::Twine &longMessage="");
359 
360  // call error handler and terminate state, for execution errors
361  // (things that should not be possible, like illegal instruction or
362  // unlowered instrinsic, or are unsupported, like inline assembly)
364  const llvm::Twine &message,
365  const llvm::Twine &info="") {
366  terminateStateOnError(state, message, "exec.err", info);
367  }
368 
370  void bindModuleConstants();
371 
372  template <typename TypeIt>
373  void computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie);
374 
378 
379  void handlePointsToObj(ExecutionState &state,
380  KInstruction *target,
381  const std::vector<ref<Expr> > &arguments);
382 
384  ref<Expr> e,
385  ref<ConstantExpr> value);
386 
391  void addTimer(Timer *timer, double rate);
392 
393  void initTimers();
394  void processTimers(ExecutionState *current,
395  double maxInstTime);
396 
397 public:
398  Executor(const InterpreterOptions &opts, InterpreterHandler *ie);
399  virtual ~Executor();
400 
402  return *interpreterHandler;
403  }
404 
405  // XXX should just be moved out to utility module
406  ref<klee::ConstantExpr> evalConstant(const llvm::Constant *c);
407 
408  virtual void setPathWriter(TreeStreamWriter *tsw) {
409  pathWriter = tsw;
410  }
412  symPathWriter = tsw;
413  }
414 
415  virtual void setReplayOut(const struct KTest *out) {
416  assert(!replayPath && "cannot replay both buffer and path");
417  replayOut = out;
418  replayPosition = 0;
419  }
420 
421  virtual void setReplayPath(const std::vector<bool> *path) {
422  assert(!replayOut && "cannot replay both buffer and path");
423  replayPath = path;
424  replayPosition = 0;
425  }
426 
427  virtual const llvm::Module *
428  setModule(llvm::Module *module, const ModuleOptions &opts);
429 
430  virtual void useSeeds(const std::vector<struct KTest *> *seeds) {
431  usingSeeds = seeds;
432  }
433 
434  virtual void runFunctionAsMain(llvm::Function *f,
435  int argc,
436  char **argv,
437  char **envp);
438 
439  /*** Runtime options ***/
440 
441  virtual void setHaltExecution(bool value) {
442  haltExecution = value;
443  }
444 
445  virtual void setInhibitForking(bool value) {
446  inhibitForking = value;
447  }
448 
449  /*** State accessor methods ***/
450 
451  virtual unsigned getPathStreamID(const ExecutionState &state);
452 
453  virtual unsigned getSymbolicPathStreamID(const ExecutionState &state);
454 
455  virtual void getConstraintLog(const ExecutionState &state,
456  std::string &res,
458 
459  virtual bool getSymbolicSolution(const ExecutionState &state,
460  std::vector<
461  std::pair<std::string,
462  std::vector<unsigned char> > >
463  &res);
464 
465  virtual void getCoveredLines(const ExecutionState &state,
466  std::map<const std::string*, std::set<unsigned> > &res);
467 
468  Expr::Width getWidthForLLVMType(LLVM_TYPE_Q llvm::Type *type) const;
469 };
470 
471 } // End klee namespace
472 
473 #endif
Definition: KTest.h:26
virtual void setPathWriter(TreeStreamWriter *tsw)
Definition: Executor.h:408
void executeCall(ExecutionState &state, KInstruction *ki, llvm::Function *f, std::vector< ref< Expr > > &arguments)
Definition: Executor.cpp:1191
void transferToBasicBlock(llvm::BasicBlock *dst, llvm::BasicBlock *src, ExecutionState &state)
Definition: Executor.cpp:1334
std::pair< ExecutionState *, ExecutionState * > StatePair
Definition: Executor.h:98
void computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie)
Definition: Executor.cpp:2443
virtual void setInhibitForking(bool value)
Definition: Executor.h:445
void executeFree(ExecutionState &state, ref< Expr > address, KInstruction *target=0)
Definition: Executor.cpp:3069
int const char const char * suffix
Definition: klee.h:68
#define Expr
Definition: STPBuilder.h:19
std::map< ExecutionState *, std::vector< SeedInfo > > seedMap
Definition: Executor.h:135
void run(ExecutionState &initialState)
Definition: Executor.cpp:2504
std::set< ExecutionState * > states
Definition: Executor.h:110
ObjectState * bindObjectInState(ExecutionState &state, const MemoryObject *mo, bool isLocal, const Array *array=0)
Definition: Executor.cpp:2942
Expr::Width getWidthForLLVMType(LLVM_TYPE_Q llvm::Type *type) const
Definition: Executor.cpp:3567
void handlePointsToObj(ExecutionState &state, KInstruction *target, const std::vector< ref< Expr > > &arguments)
unsigned getArgRegister(unsigned index)
Definition: KModule.h:65
std::set< uint64_t > legalFunctions
Definition: Executor.h:146
void initializeGlobalObject(ExecutionState &state, ObjectState *os, const llvm::Constant *c, unsigned offset)
Definition: Executor.cpp:397
double coreSolverTimeout
Definition: Executor.h:178
void bindArgument(KFunction *kf, unsigned index, ExecutionState &state, ref< Expr > value)
Definition: Executor.cpp:1074
void printFileLine(ExecutionState &state, KInstruction *ki)
Definition: Executor.cpp:1358
MemoryObject * addExternalObject(ExecutionState &state, void *addr, unsigned size, bool isReadOnly)
Definition: Executor.cpp:449
int const char * message
Definition: klee.h:68
const Cell & eval(KInstruction *ki, unsigned index, ExecutionState &state) const
Definition: Executor.cpp:1050
void addTimer(Timer *timer, double rate)
unsigned dest
Destination register index.
Definition: KInstruction.h:39
void terminateState(ExecutionState &state)
Definition: Executor.cpp:2695
std::string getAddressInfo(ExecutionState &state, ref< Expr > address) const
Get textual information regarding a memory address.
Definition: Executor.cpp:2645
virtual void setSymbolicPathWriter(TreeStreamWriter *tsw)
Definition: Executor.h:411
void callExternalFunction(ExecutionState &state, KInstruction *target, llvm::Function *function, std::vector< ref< Expr > > &arguments)
Definition: Executor.cpp:2827
StatePair fork(ExecutionState &current, ref< Expr > condition, bool isInternal)
Definition: Executor.cpp:729
MemoryManager * memory
Definition: Executor.h:109
bool haltExecution
Definition: Executor.h:170
void executeGetValue(ExecutionState &state, ref< Expr > e, KInstruction *target)
Definition: Executor.cpp:1130
StatsTracker * statsTracker
Definition: Executor.h:111
void terminateStateOnExit(ExecutionState &state)
Definition: Executor.cpp:2729
void addConstraint(ExecutionState &state, ref< Expr > condition)
Definition: Executor.cpp:956
ref< klee::ConstantExpr > toConstant(ExecutionState &state, ref< Expr > e, const char *purpose)
Definition: Executor.cpp:1102
void processTimers(ExecutionState *current, double maxInstTime)
virtual void getConstraintLog(const ExecutionState &state, std::string &res, Interpreter::LogType logFormat=Interpreter::STP)
Definition: Executor.cpp:3449
Cell & getDestCell(ExecutionState &state, KInstruction *target)
Definition: Executor.h:307
std::map< const llvm::GlobalValue *, MemoryObject * > globalObjects
Map of globals to their representative memory object.
Definition: Executor.h:138
const struct KTest * replayOut
Definition: Executor.h:150
PTree * processTree
Definition: Executor.h:115
void executeMemoryOperation(ExecutionState &state, bool isWrite, ref< Expr > address, ref< Expr > value, KInstruction *target)
Definition: Executor.cpp:3134
virtual unsigned getSymbolicPathStreamID(const ExecutionState &state)
Definition: Executor.cpp:3444
virtual void setReplayPath(const std::vector< bool > *path)
Definition: Executor.h:421
std::map< const llvm::GlobalValue *, ref< ConstantExpr > > globalAddresses
Definition: Executor.h:142
TreeStreamWriter * pathWriter
Definition: Executor.h:112
const std::vector< struct KTest * > * usingSeeds
Definition: Executor.h:159
SpecialFunctionHandler * specialFunctionHandler
Definition: Executor.h:113
#define LLVM_TYPE_Q
Definition: Version.h:21
void doImpliedValueConcretization(ExecutionState &state, ref< Expr > e, ref< ConstantExpr > value)
Definition: Executor.cpp:3533
void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, const char *suffix, const llvm::Twine &longMessage="")
Definition: Executor.cpp:2778
virtual void useSeeds(const std::vector< struct KTest * > *seeds)
Definition: Executor.h:430
InterpreterHandler * interpreterHandler
Definition: Executor.h:104
std::vector< TimerInfo * > timers
Definition: Executor.h:114
ref< Expr > toUnique(const ExecutionState &state, ref< Expr > &e)
Definition: Executor.cpp:1079
void bindModuleConstants()
bindModuleConstants - Initialize the module constant table.
Definition: Executor.cpp:2489
unsigned replayPosition
Definition: Executor.h:155
TreeStreamWriter * symPathWriter
Definition: Executor.h:112
Executor(const InterpreterOptions &opts, InterpreterHandler *ie)
Definition: Executor.cpp:275
std::set< ExecutionState * > addedStates
Definition: Executor.h:121
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
friend class OwningSearcher
Definition: Executor.h:83
void terminateStateOnExecError(ExecutionState &state, const llvm::Twine &message, const llvm::Twine &info="")
Definition: Executor.h:363
void executeAlloc(ExecutionState &state, ref< Expr > size, bool isLocal, KInstruction *target, bool zeroMemory=false, const ObjectState *reallocFrom=0)
Definition: Executor.cpp:2959
Cell & getArgumentCell(ExecutionState &state, KFunction *kf, unsigned index)
Definition: Executor.h:301
void stepInstruction(ExecutionState &state)
Definition: Executor.cpp:1173
virtual ~Executor()
Definition: Executor.cpp:378
virtual void getCoveredLines(const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res)
Definition: Executor.cpp:3528
virtual unsigned getPathStreamID(const ExecutionState &state)
Definition: Executor.cpp:3439
void terminateStateEarly(ExecutionState &state, const llvm::Twine &message)
Definition: Executor.cpp:2720
TimingSolver * solver
Definition: Executor.h:108
ExternalDispatcher * externalDispatcher
Definition: Executor.h:107
KModule * kmodule
Definition: Executor.h:101
ref< klee::ConstantExpr > evalConstantExpr(const llvm::ConstantExpr *ce)
std::vector< std::pair< std::pair< const MemoryObject *, const ObjectState * >, ExecutionState * > > ExactResolutionList
Definition: Executor.h:222
virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv, char **envp)
Definition: Executor.cpp:3340
virtual void setReplayOut(const struct KTest *out)
Definition: Executor.h:415
const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, llvm::Instruction **lastInstruction)
Definition: Executor.cpp:2736
bool inhibitForking
Disables forking, set by client.
Definition: Executor.h:166
const std::vector< bool > * replayPath
When non-null a list of branch decisions to be used for replay.
Definition: Executor.h:152
llvm::Function * getTargetFunction(llvm::Value *calledVal, ExecutionState &state)
Definition: Executor.cpp:1368
bool atMemoryLimit
Definition: Executor.h:163
void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, const std::string &name)
Definition: Executor.cpp:3260
virtual bool getSymbolicSolution(const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res)
Definition: Executor.cpp:3486
const InterpreterHandler & getHandler()
Definition: Executor.h:401
bool ivcEnabled
Definition: Executor.h:174
ref< klee::ConstantExpr > evalConstant(const llvm::Constant *c)
Definition: Executor.cpp:989
void branch(ExecutionState &state, const std::vector< ref< Expr > > &conditions, std::vector< ExecutionState * > &result)
Definition: Executor.cpp:642
void initializeGlobals(ExecutionState &state)
Definition: Executor.cpp:465
Searcher * searcher
Definition: Executor.h:105
ref< Expr > replaceReadWithSymbolic(ExecutionState &state, ref< Expr > e)
Definition: Executor.cpp:2916
void executeInstruction(ExecutionState &state, KInstruction *ki)
Definition: Executor.cpp:1426
virtual const llvm::Module * setModule(llvm::Module *module, const ModuleOptions &opts)
Definition: Executor.cpp:347
virtual void run()=0
The event callback.
virtual void setHaltExecution(bool value)
Definition: Executor.h:441
void bindInstructionConstants(KInstruction *KI)
Definition: Executor.cpp:2475
void updateStates(ExecutionState *current)
Definition: Executor.cpp:2417
void bindLocal(KInstruction *target, ExecutionState &state, ref< Expr > value)
Definition: Executor.cpp:1069
std::set< ExecutionState * > removedStates
Definition: Executor.h:126
void resolveExact(ExecutionState &state, ref< Expr > p, ExactResolutionList &results, const std::string &name)
Definition: Executor.cpp:3103