klee
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 "ExecutionState.h"
19#include "UserSearcher.h"
20
21#include "klee/ADT/RNG.h"
27#include "klee/Module/Cell.h"
29#include "klee/Module/KModule.h"
30#include "klee/System/Time.h"
31
32#include "llvm/ADT/Twine.h"
33#include "llvm/Support/raw_ostream.h"
34
35#include <map>
36#include <memory>
37#include <set>
38#include <string>
39#include <unordered_map>
40#include <vector>
41
42struct KTest;
43
44namespace llvm {
45 class BasicBlock;
46 class BranchInst;
47 class CallInst;
48 class LandingPadInst;
49 class Constant;
50 class ConstantExpr;
51 class Function;
52 class GlobalValue;
53 class Instruction;
54 class LLVMContext;
55 class DataLayout;
56 class Twine;
57 class Value;
58}
59
60namespace klee {
61 class Array;
62 struct Cell;
63 class ExecutionState;
64 class ExternalDispatcher;
65 class Expr;
66 class InstructionInfoTable;
67 struct KFunction;
68 struct KInstruction;
69 class KInstIterator;
70 class KModule;
71 class MemoryManager;
72 class MemoryObject;
73 class ObjectState;
74 class PTree;
75 class Searcher;
76 class SeedInfo;
77 class SpecialFunctionHandler;
78 struct StackFrame;
79 class StatsTracker;
80 class TimingSolver;
81 class TreeStreamWriter;
82 class MergeHandler;
83 class MergingSearcher;
84 template<class T> class ref;
85
86
87
91
92class Executor : public Interpreter {
93 friend class OwningSearcher;
96 friend class StatsTracker;
97 friend class MergeHandler;
99
100public:
101 typedef std::pair<ExecutionState*,ExecutionState*> StatePair;
102
105
106private:
107 std::unique_ptr<KModule> kmodule;
110
114 std::set<ExecutionState*, ExecutionStateIDCompare> states;
119 std::unique_ptr<PTree> processTree;
120
125 std::vector<ExecutionState *> addedStates;
130 std::vector<ExecutionState *> removedStates;
131
139 std::map<ExecutionState*, std::vector<SeedInfo> > seedMap;
140
142 std::map<const llvm::GlobalValue*, MemoryObject*> globalObjects;
143
146 std::map<const llvm::GlobalValue*, ref<ConstantExpr> > globalAddresses;
147
150 std::unordered_map<std::uint64_t, llvm::Function*> legalFunctions;
151
154 const struct KTest *replayKTest;
155
157 const std::vector<bool> *replayPath;
158
162
165 const std::vector<struct KTest *> *usingSeeds;
166
170
173
177
181
185
188
191
193 std::unique_ptr<llvm::raw_ostream> debugInstFile;
194
195 // @brief Buffer used by logBuffer
196 std::string debugBufferString;
197
198 // @brief buffer to store logs before flushing to file
199 llvm::raw_string_ostream debugLogBuffer;
200
203
207
209 std::vector<ref<Expr>> eh_typeids;
210
213
214 llvm::Function* getTargetFunction(llvm::Value *calledVal,
215 ExecutionState &state);
216
218
219 void run(ExecutionState &initialState);
220
221 // Given a concrete object in our [klee's] address space, add it to
222 // objects checked code can reference.
223 MemoryObject *addExternalObject(ExecutionState &state, void *addr,
224 unsigned size, bool isReadOnly);
225
226 void initializeGlobalAlias(const llvm::Constant *c);
228 const llvm::Constant *c,
229 unsigned offset);
234
235 void stepInstruction(ExecutionState &state);
236 void updateStates(ExecutionState *current);
237 void transferToBasicBlock(llvm::BasicBlock *dst,
238 llvm::BasicBlock *src,
239 ExecutionState &state);
240
242 KInstruction *target,
243 llvm::Function *function,
244 std::vector< ref<Expr> > &arguments);
245
247 bool isLocal, const Array *array = 0);
248
257 typedef std::vector< std::pair<std::pair<const MemoryObject*, const ObjectState*>,
259 void resolveExact(ExecutionState &state,
260 ref<Expr> p,
261 ExactResolutionList &results,
262 const std::string &name);
263
283 void executeAlloc(ExecutionState &state,
284 ref<Expr> size,
285 bool isLocal,
286 KInstruction *target,
287 bool zeroMemory=false,
288 const ObjectState *reallocFrom=0,
289 size_t allocationAlignment=0);
290
296 void executeFree(ExecutionState &state,
297 ref<Expr> address,
298 KInstruction *target = 0);
299
303 const llvm::LandingPadInst &lpi,
304 bool &stateTerminated);
305
309
310 void executeCall(ExecutionState &state,
311 KInstruction *ki,
312 llvm::Function *f,
313 std::vector< ref<Expr> > &arguments);
314
315 // do address resolution / object binding / out of bounds checking
316 // and perform the operation
318 bool isWrite,
319 ref<Expr> address,
320 ref<Expr> value /* undef if read */,
321 KInstruction *target /* undef if write */);
322
323 void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo,
324 const std::string &name);
325
330 void branch(ExecutionState &state, const std::vector<ref<Expr>> &conditions,
331 std::vector<ExecutionState *> &result, BranchType reason);
332
336 StatePair fork(ExecutionState &current, ref<Expr> condition, bool isInternal,
337 BranchType reason);
338
339 // If the MaxStatic*Pct limits have been reached, concretize the condition and
340 // return it. Otherwise, return the unmodified condition.
342
347 void addConstraint(ExecutionState &state, ref<Expr> condition);
348
349 // Called on [for now] concrete reads, replaces constant with a symbolic
350 // Used for testing.
352
353 const Cell& eval(KInstruction *ki, unsigned index,
354 ExecutionState &state) const;
355
357 KFunction *kf,
358 unsigned index) {
359 return state.stack.back().locals[kf->getArgRegister(index)];
360 }
361
363 KInstruction *target) {
364 return state.stack.back().locals[target->dest];
365 }
366
367 void bindLocal(KInstruction *target,
368 ExecutionState &state,
369 ref<Expr> value);
370 void bindArgument(KFunction *kf,
371 unsigned index,
372 ExecutionState &state,
373 ref<Expr> value);
374
378 ref<klee::ConstantExpr> evalConstantExpr(const llvm::ConstantExpr *c,
379 const KInstruction *ki = NULL);
380
384 ref<klee::ConstantExpr> evalConstant(const llvm::Constant *c,
385 const KInstruction *ki = NULL);
386
390 ref<Expr> toUnique(const ExecutionState &state, ref<Expr> &e);
391
399 const char *purpose);
400
403 void executeGetValue(ExecutionState &state, ref<Expr> e, KInstruction *target);
404
406 std::string getAddressInfo(ExecutionState &state, ref<Expr> address) const;
407
408 // Determines the \param lastInstruction of the \param state which is not KLEE
409 // internal and returns its InstructionInfo
411 llvm::Instruction** lastInstruction);
412
414 void terminateState(ExecutionState &state);
415
419
422 void terminateStateEarly(ExecutionState &state, const llvm::Twine &message,
423 StateTerminationType terminationType);
424
427 void terminateStateOnError(ExecutionState &state, const llvm::Twine &message,
428 StateTerminationType terminationType,
429 const llvm::Twine &longMessage = "",
430 const char *suffix = nullptr);
431
436 const llvm::Twine &message,
437 const llvm::Twine &info = "");
438
442 const llvm::Twine &message);
443
447 const llvm::Twine &message);
448
450 void bindModuleConstants();
451
452 template <typename SqType, typename TypeIt>
454 ref<ConstantExpr> &constantOffset, uint64_t index,
455 const TypeIt it);
456
457 template <typename TypeIt>
458 void computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie);
459
463
465 ref<Expr> e,
466 ref<ConstantExpr> value);
467
470 bool checkMemoryUsage();
471
473 bool branchingPermitted(const ExecutionState &state) const;
474
476 void doDumpStates();
477
479 void dumpStates();
480 void dumpPTree();
481
482public:
483 Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts,
485 virtual ~Executor();
486
488 return *interpreterHandler;
489 }
490
491 void setPathWriter(TreeStreamWriter *tsw) override { pathWriter = tsw; }
492
494 symPathWriter = tsw;
495 }
496
497 void setReplayKTest(const struct KTest *out) override {
498 assert(!replayPath && "cannot replay both buffer and path");
499 replayKTest = out;
500 replayPosition = 0;
501 }
502
503 void setReplayPath(const std::vector<bool> *path) override {
504 assert(!replayKTest && "cannot replay both buffer and path");
505 replayPath = path;
506 replayPosition = 0;
507 }
508
509 llvm::Module *setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
510 const ModuleOptions &opts) override;
511
512 void useSeeds(const std::vector<struct KTest *> *seeds) override {
513 usingSeeds = seeds;
514 }
515
516 void runFunctionAsMain(llvm::Function *f, int argc, char **argv,
517 char **envp) override;
518
519 /*** Runtime options ***/
520
521 void setHaltExecution(bool value) override { haltExecution = value; }
522
523 void setInhibitForking(bool value) override { inhibitForking = value; }
524
525 void prepareForEarlyExit() override;
526
527 /*** State accessor methods ***/
528
529 unsigned getPathStreamID(const ExecutionState &state) override;
530
531 unsigned getSymbolicPathStreamID(const ExecutionState &state) override;
532
533 void getConstraintLog(const ExecutionState &state, std::string &res,
534 Interpreter::LogType logFormat =
535 Interpreter::STP) override;
536
538 const ExecutionState &state,
539 std::vector<std::pair<std::string, std::vector<unsigned char>>> &res)
540 override;
541
542 void getCoveredLines(const ExecutionState &state,
543 std::map<const std::string *, std::set<unsigned>> &res)
544 override;
545
546 Expr::Width getWidthForLLVMType(llvm::Type *type) const;
547 size_t getAllocationAlignment(const llvm::Value *allocSite) const;
548
550 int *getErrnoLocation(const ExecutionState &state) const;
551
554};
555
556} // End klee namespace
557
558#endif /* KLEE_EXECUTOR_H */
BranchType
Reason an ExecutionState forked.
Definition: BranchTypes.h:48
#define Expr
Definition: STPBuilder.h:19
StateTerminationType
Reason an ExecutionState got terminated.
Provides an interface for creating and destroying Array objects.
Definition: ArrayCache.h:31
ExecutionState representing a path under exploration.
stack_ty stack
Stack representing the current instruction stream.
std::unique_ptr< llvm::raw_ostream > debugInstFile
File to print executed instructions to.
Definition: Executor.h:193
void callExternalFunction(ExecutionState &state, KInstruction *target, llvm::Function *function, std::vector< ref< Expr > > &arguments)
Definition: Executor.cpp:3781
bool ivcEnabled
Definition: Executor.h:180
MemoryManager * memory
Definition: Executor.h:113
void terminateStateOnExit(ExecutionState &state)
Definition: Executor.cpp:3638
void addConstraint(ExecutionState &state, ref< Expr > condition)
Definition: Executor.cpp:1194
ArrayCache arrayCache
Assumes ownership of the created array objects.
Definition: Executor.h:190
Cell & getArgumentCell(ExecutionState &state, KFunction *kf, unsigned index)
Definition: Executor.h:356
bool checkMemoryUsage()
Definition: Executor.cpp:3388
const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, llvm::Instruction **lastInstruction)
Definition: Executor.cpp:3665
TreeStreamWriter * symPathWriter
Definition: Executor.h:116
unsigned replayPosition
Definition: Executor.h:161
std::string getAddressInfo(ExecutionState &state, ref< Expr > address) const
Get textual information regarding a memory address.
Definition: Executor.cpp:3543
ObjectState * bindObjectInState(ExecutionState &state, const MemoryObject *mo, bool isLocal, const Array *array=0)
Definition: Executor.cpp:3938
virtual ~Executor()
Definition: Executor.cpp:562
void initializeGlobalAlias(const llvm::Constant *c)
Definition: Executor.cpp:758
std::map< ExecutionState *, std::vector< SeedInfo > > seedMap
Definition: Executor.h:139
std::map< const llvm::GlobalValue *, ref< ConstantExpr > > globalAddresses
Definition: Executor.h:146
TimerGroup timers
Definition: Executor.h:118
ref< klee::ConstantExpr > toConstant(ExecutionState &state, ref< Expr > e, const char *purpose)
Definition: Executor.cpp:1285
ref< ConstantExpr > getEhTypeidFor(ref< Expr > type_info)
Return the typeid corresponding to a certain type_info
Definition: Executor.cpp:1641
TimingSolver * solver
Definition: Executor.h:112
const InterpreterHandler & getHandler()
Definition: Executor.h:487
void printDebugInstructions(ExecutionState &state)
Definition: Executor.cpp:1361
void branch(ExecutionState &state, const std::vector< ref< Expr > > &conditions, std::vector< ExecutionState * > &result, BranchType reason)
Definition: Executor.cpp:864
void bindArgument(KFunction *kf, unsigned index, ExecutionState &state, ref< Expr > value)
Definition: Executor.cpp:1253
llvm::Function * getTargetFunction(llvm::Value *calledVal, ExecutionState &state)
Definition: Executor.cpp:2017
std::vector< std::pair< std::pair< const MemoryObject *, const ObjectState * >, ExecutionState * > > ExactResolutionList
Definition: Executor.h:258
StatePair fork(ExecutionState &current, ref< Expr > condition, bool isInternal, BranchType reason)
Definition: Executor.cpp:1003
size_t getAllocationAlignment(const llvm::Value *allocSite) const
Definition: Executor.cpp:4588
std::unique_ptr< PTree > processTree
Definition: Executor.h:119
void initializeGlobalAliases()
Definition: Executor.cpp:789
void dumpPTree()
Definition: Executor.cpp:4677
RNG theRNG
The random number generator.
Definition: Executor.h:104
const struct KTest * replayKTest
Definition: Executor.h:154
TreeStreamWriter * pathWriter
Definition: Executor.h:116
void doDumpStates()
Definition: Executor.cpp:3430
ref< Expr > toUnique(const ExecutionState &state, ref< Expr > &e)
Definition: Executor.cpp:1258
std::vector< ExecutionState * > addedStates
Definition: Executor.h:125
void terminateState(ExecutionState &state)
Remove state from queue and delete state.
Definition: Executor.cpp:3596
void computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie)
Definition: Executor.cpp:3334
std::unordered_map< std::uint64_t, llvm::Function * > legalFunctions
Definition: Executor.h:150
void computeOffsetsSeqTy(KGEPInstruction *kgepi, ref< ConstantExpr > &constantOffset, uint64_t index, const TypeIt it)
Definition: Executor.cpp:3315
bool inhibitForking
Disables forking, set by client.
Definition: Executor.h:172
void runFunctionAsMain(llvm::Function *f, int argc, char **argv, char **envp) override
Definition: Executor.cpp:4344
llvm::raw_string_ostream debugLogBuffer
Definition: Executor.h:199
std::vector< ref< Expr > > eh_typeids
Typeids used during exception handling.
Definition: Executor.h:209
void executeAlloc(ExecutionState &state, ref< Expr > size, bool isLocal, KInstruction *target, bool zeroMemory=false, const ObjectState *reallocFrom=0, size_t allocationAlignment=0)
Definition: Executor.cpp:3955
void executeInstruction(ExecutionState &state, KInstruction *ki)
Definition: Executor.cpp:2045
void setReplayKTest(const struct KTest *out) override
Definition: Executor.h:497
void executeMemoryOperation(ExecutionState &state, bool isWrite, ref< Expr > address, ref< Expr > value, KInstruction *target)
Definition: Executor.cpp:4141
void initializeGlobals(ExecutionState &state)
Definition: Executor.cpp:634
std::set< ExecutionState *, ExecutionStateIDCompare > states
Definition: Executor.h:114
ref< Expr > maxStaticPctChecks(ExecutionState &current, ref< Expr > condition)
Definition: Executor.cpp:947
Expr::Width getWidthForLLVMType(llvm::Type *type) const
Definition: Executor.cpp:4584
void setReplayPath(const std::vector< bool > *path) override
Definition: Executor.h:503
Cell & getDestCell(ExecutionState &state, KInstruction *target)
Definition: Executor.h:362
ref< klee::ConstantExpr > evalConstantExpr(const llvm::ConstantExpr *c, const KInstruction *ki=NULL)
bool atMemoryLimit
Definition: Executor.h:169
void bindLocal(KInstruction *target, ExecutionState &state, ref< Expr > value)
Definition: Executor.cpp:1248
void setInhibitForking(bool value) override
Definition: Executor.h:523
Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ie)
Definition: Executor.cpp:436
void doImpliedValueConcretization(ExecutionState &state, ref< Expr > e, ref< ConstantExpr > value)
Definition: Executor.cpp:4550
void getConstraintLog(const ExecutionState &state, std::string &res, Interpreter::LogType logFormat=Interpreter::STP) override
Definition: Executor.cpp:4460
time::Span maxInstructionTime
Maximum time to allow for a single instruction.
Definition: Executor.h:187
void terminateStateEarly(ExecutionState &state, const llvm::Twine &message, StateTerminationType terminationType)
Definition: Executor.cpp:3648
time::Span coreSolverTimeout
Definition: Executor.h:184
void setMergingSearcher(MergingSearcher *ms)
Definition: Executor.h:553
void bindInstructionConstants(KInstruction *KI)
Definition: Executor.cpp:3358
MemoryObject * serializeLandingpad(ExecutionState &state, const llvm::LandingPadInst &lpi, bool &stateTerminated)
Definition: Executor.cpp:1429
std::map< const llvm::GlobalValue *, MemoryObject * > globalObjects
Map of globals to their representative memory object.
Definition: Executor.h:142
void getCoveredLines(const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res) override
Definition: Executor.cpp:4545
void bindModuleConstants()
bindModuleConstants - Initialize the module constant table.
Definition: Executor.cpp:3373
std::pair< ExecutionState *, ExecutionState * > StatePair
Definition: Executor.h:101
ref< Expr > replaceReadWithSymbolic(ExecutionState &state, ref< Expr > e)
Definition: Executor.cpp:3911
MergingSearcher * getMergingSearcher() const
Definition: Executor.h:552
const Cell & eval(KInstruction *ki, unsigned index, ExecutionState &state) const
Definition: Executor.cpp:1229
void terminateStateOnExecError(ExecutionState &state, const llvm::Twine &message, const llvm::Twine &info="")
Definition: Executor.cpp:3761
bool haltExecution
Definition: Executor.h:176
void allocateGlobalObjects(ExecutionState &state)
Definition: Executor.cpp:648
void useSeeds(const std::vector< struct KTest * > *seeds) override
Definition: Executor.h:512
void stepInstruction(ExecutionState &state)
Definition: Executor.cpp:1402
std::string debugBufferString
Definition: Executor.h:196
SpecialFunctionHandler * specialFunctionHandler
Definition: Executor.h:117
llvm::Module * setModule(std::vector< std::unique_ptr< llvm::Module > > &modules, const ModuleOptions &opts) override
Definition: Executor.cpp:499
bool getSymbolicSolution(const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res) override
Definition: Executor.cpp:4494
void prepareForEarlyExit() override
Definition: Executor.cpp:4659
void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, const std::string &name)
Definition: Executor.cpp:4268
void setPathWriter(TreeStreamWriter *tsw) override
Definition: Executor.h:491
void run(ExecutionState &initialState)
Definition: Executor.cpp:3442
InterpreterHandler * interpreterHandler
Definition: Executor.h:108
const std::vector< bool > * replayPath
When non-null a list of branch decisions to be used for replay.
Definition: Executor.h:157
bool branchingPermitted(const ExecutionState &state) const
check if branching/forking is allowed
Definition: Executor.cpp:843
void terminateStateOnSolverError(ExecutionState &state, const llvm::Twine &message)
Definition: Executor.cpp:3767
void transferToBasicBlock(llvm::BasicBlock *dst, llvm::BasicBlock *src, ExecutionState &state)
Definition: Executor.cpp:1991
std::unique_ptr< KModule > kmodule
Definition: Executor.h:107
unsigned getSymbolicPathStreamID(const ExecutionState &state) override
Definition: Executor.cpp:4455
void terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message)
Definition: Executor.cpp:3661
void resolveExact(ExecutionState &state, ref< Expr > p, ExactResolutionList &results, const std::string &name)
Definition: Executor.cpp:4110
friend class OwningSearcher
Definition: Executor.h:93
MergingSearcher * mergingSearcher
Definition: Executor.h:206
void setHaltExecution(bool value) override
Definition: Executor.h:521
ExternalDispatcher * externalDispatcher
Definition: Executor.h:111
ExprOptimizer optimizer
Optimizes expressions.
Definition: Executor.h:202
void executeGetValue(ExecutionState &state, ref< Expr > e, KInstruction *target)
Definition: Executor.cpp:1314
void unwindToNextLandingpad(ExecutionState &state)
Definition: Executor.cpp:1532
void executeCall(ExecutionState &state, KInstruction *ki, llvm::Function *f, std::vector< ref< Expr > > &arguments)
Definition: Executor.cpp:1657
void executeFree(ExecutionState &state, ref< Expr > address, KInstruction *target=0)
Definition: Executor.cpp:4076
MemoryObject * addExternalObject(ExecutionState &state, void *addr, unsigned size, bool isReadOnly)
Definition: Executor.cpp:618
StatsTracker * statsTracker
Definition: Executor.h:115
void initializeGlobalObjects(ExecutionState &state)
Definition: Executor.cpp:796
void initializeGlobalObject(ExecutionState &state, ObjectState *os, const llvm::Constant *c, unsigned offset)
Definition: Executor.cpp:572
unsigned getPathStreamID(const ExecutionState &state) override
Definition: Executor.cpp:4450
void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, StateTerminationType terminationType, const llvm::Twine &longMessage="", const char *suffix=nullptr)
Definition: Executor.cpp:3713
void updateStates(ExecutionState *current)
Definition: Executor.cpp:3289
Searcher * searcher
Definition: Executor.h:109
std::vector< ExecutionState * > removedStates
Definition: Executor.h:130
ref< klee::ConstantExpr > evalConstant(const llvm::Constant *c, const KInstruction *ki=NULL)
const std::vector< struct KTest * > * usingSeeds
Definition: Executor.h:165
void dumpStates()
Only for debug purposes; enable via debugger or klee-control.
Definition: Executor.cpp:4690
int * getErrnoLocation(const ExecutionState &state) const
Returns the errno location in memory of the state.
Definition: Executor.cpp:4667
void setSymbolicPathWriter(TreeStreamWriter *tsw) override
Definition: Executor.h:493
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:97
Represents one klee_open_merge() call. Handles merging of states that branched from it.
Definition: MergeHandler.h:96
Definition: RNG.h:14
Definition: Ref.h:82
int const char * message
Definition: klee.h:75
int const char const char * suffix
Definition: klee.h:76
Definition: main.cpp:291
Searcher * constructUserSearcher(Executor &executor)
Definition: KTest.h:25
InstructionInfo stores debug information for a KInstruction.
unsigned getArgRegister(unsigned index)
Definition: KModule.h:63
unsigned dest
Destination register index.
Definition: KInstruction.h:43