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" 22 #include "klee/Core/Interpreter.h" 23 #include "klee/Expr/ArrayCache.h" 24 #include "klee/Expr/ArrayExprOptimizer.h" 25 #include "klee/Module/Cell.h" 26 #include "klee/Module/KInstruction.h" 27 #include "klee/Module/KModule.h" 28 #include "klee/System/Time.h" 29 30 #include "llvm/ADT/Twine.h" 31 #include "llvm/Support/raw_ostream.h" 32 33 #include <map> 34 #include <memory> 35 #include <set> 36 #include <string> 37 #include <vector> 38 39 struct KTest; 40 41 namespace llvm { 42 class BasicBlock; 43 class BranchInst; 44 class CallInst; 45 class LandingPadInst; 46 class Constant; 47 class ConstantExpr; 48 class Function; 49 class GlobalValue; 50 class Instruction; 51 class LLVMContext; 52 class DataLayout; 53 class Twine; 54 class Value; 55 } 56 57 namespace klee { 58 class Array; 59 struct Cell; 60 class ExecutionState; 61 class ExternalDispatcher; 62 class Expr; 63 class InstructionInfoTable; 64 struct KFunction; 65 struct KInstruction; 66 class KInstIterator; 67 class KModule; 68 class MemoryManager; 69 class MemoryObject; 70 class ObjectState; 71 class PTree; 72 class Searcher; 73 class SeedInfo; 74 class SpecialFunctionHandler; 75 struct StackFrame; 76 class StatsTracker; 77 class TimingSolver; 78 class TreeStreamWriter; 79 class MergeHandler; 80 class MergingSearcher; 81 template<class T> class ref; 82 83 84 85 /// \todo Add a context object to keep track of data only live 86 /// during an instruction step. Should contain addedStates, 87 /// removedStates, and haltExecution, among others. 88 89 class Executor : public Interpreter { 90 friend class OwningSearcher; 91 friend class WeightedRandomSearcher; 92 friend class SpecialFunctionHandler; 93 friend class StatsTracker; 94 friend class MergeHandler; 95 friend klee::Searcher *klee::constructUserSearcher(Executor &executor); 96 97 public: 98 typedef std::pair<ExecutionState*,ExecutionState*> StatePair; 99 100 enum TerminateReason { 101 Abort, 102 Assert, 103 BadVectorAccess, 104 Exec, 105 External, 106 Free, 107 Model, 108 Overflow, 109 Ptr, 110 ReadOnly, 111 ReportError, 112 User, 113 UncaughtException, 114 UnexpectedException, 115 Unhandled, 116 }; 117 118 /// The random number generator. 119 RNG theRNG; 120 121 private: 122 static const char *TerminateReasonNames[]; 123 124 std::unique_ptr<KModule> kmodule; 125 InterpreterHandler *interpreterHandler; 126 Searcher *searcher; 127 128 ExternalDispatcher *externalDispatcher; 129 TimingSolver *solver; 130 MemoryManager *memory; 131 std::set<ExecutionState*, ExecutionStateIDCompare> states; 132 StatsTracker *statsTracker; 133 TreeStreamWriter *pathWriter, *symPathWriter; 134 SpecialFunctionHandler *specialFunctionHandler; 135 TimerGroup timers; 136 std::unique_ptr<PTree> processTree; 137 138 /// Used to track states that have been added during the current 139 /// instructions step. 140 /// \invariant \ref addedStates is a subset of \ref states. 141 /// \invariant \ref addedStates and \ref removedStates are disjoint. 142 std::vector<ExecutionState *> addedStates; 143 /// Used to track states that have been removed during the current 144 /// instructions step. 145 /// \invariant \ref removedStates is a subset of \ref states. 146 /// \invariant \ref addedStates and \ref removedStates are disjoint. 147 std::vector<ExecutionState *> removedStates; 148 149 /// When non-empty the Executor is running in "seed" mode. The 150 /// states in this map will be executed in an arbitrary order 151 /// (outside the normal search interface) until they terminate. When 152 /// the states reach a symbolic branch then either direction that 153 /// satisfies one or more seeds will be added to this map. What 154 /// happens with other states (that don't satisfy the seeds) depends 155 /// on as-yet-to-be-determined flags. 156 std::map<ExecutionState*, std::vector<SeedInfo> > seedMap; 157 158 /// Map of globals to their representative memory object. 159 std::map<const llvm::GlobalValue*, MemoryObject*> globalObjects; 160 161 /// Map of globals to their bound address. This also includes 162 /// globals that have no representative object (i.e. functions). 163 std::map<const llvm::GlobalValue*, ref<ConstantExpr> > globalAddresses; 164 165 /// The set of legal function addresses, used to validate function 166 /// pointers. We use the actual Function* address as the function address. 167 std::set<uint64_t> legalFunctions; 168 169 /// When non-null the bindings that will be used for calls to 170 /// klee_make_symbolic in order replay. 171 const struct KTest *replayKTest; 172 173 /// When non-null a list of branch decisions to be used for replay. 174 const std::vector<bool> *replayPath; 175 176 /// The index into the current \ref replayKTest or \ref replayPath 177 /// object. 178 unsigned replayPosition; 179 180 /// When non-null a list of "seed" inputs which will be used to 181 /// drive execution. 182 const std::vector<struct KTest *> *usingSeeds; 183 184 /// Disables forking, instead a random path is chosen. Enabled as 185 /// needed to control memory usage. \see fork() 186 bool atMemoryLimit; 187 188 /// Disables forking, set by client. \see setInhibitForking() 189 bool inhibitForking; 190 191 /// Signals the executor to halt execution at the next instruction 192 /// step. 193 bool haltExecution; 194 195 /// Whether implied-value concretization is enabled. Currently 196 /// false, it is buggy (it needs to validate its writes). 197 bool ivcEnabled; 198 199 /// The maximum time to allow for a single core solver query. 200 /// (e.g. for a single STP query) 201 time::Span coreSolverTimeout; 202 203 /// Maximum time to allow for a single instruction. 204 time::Span maxInstructionTime; 205 206 /// Assumes ownership of the created array objects 207 ArrayCache arrayCache; 208 209 /// File to print executed instructions to 210 std::unique_ptr<llvm::raw_ostream> debugInstFile; 211 212 // @brief Buffer used by logBuffer 213 std::string debugBufferString; 214 215 // @brief buffer to store logs before flushing to file 216 llvm::raw_string_ostream debugLogBuffer; 217 218 /// Optimizes expressions 219 ExprOptimizer optimizer; 220 221 /// Points to the merging searcher of the searcher chain, 222 /// `nullptr` if merging is disabled 223 MergingSearcher *mergingSearcher = nullptr; 224 225 /// Typeids used during exception handling 226 std::vector<ref<Expr>> eh_typeids; 227 228 /// Return the typeid corresponding to a certain `type_info` 229 ref<ConstantExpr> getEhTypeidFor(ref<Expr> type_info); 230 231 llvm::Function* getTargetFunction(llvm::Value *calledVal, 232 ExecutionState &state); 233 234 void executeInstruction(ExecutionState &state, KInstruction *ki); 235 236 void run(ExecutionState &initialState); 237 238 // Given a concrete object in our [klee's] address space, add it to 239 // objects checked code can reference. 240 MemoryObject *addExternalObject(ExecutionState &state, void *addr, 241 unsigned size, bool isReadOnly); 242 243 void initializeGlobalAlias(const llvm::Constant *c); 244 void initializeGlobalObject(ExecutionState &state, ObjectState *os, 245 const llvm::Constant *c, 246 unsigned offset); 247 void initializeGlobals(ExecutionState &state); 248 void allocateGlobalObjects(ExecutionState &state); 249 void initializeGlobalAliases(); 250 void initializeGlobalObjects(ExecutionState &state); 251 252 void stepInstruction(ExecutionState &state); 253 void updateStates(ExecutionState *current); 254 void transferToBasicBlock(llvm::BasicBlock *dst, 255 llvm::BasicBlock *src, 256 ExecutionState &state); 257 258 void callExternalFunction(ExecutionState &state, 259 KInstruction *target, 260 llvm::Function *function, 261 std::vector< ref<Expr> > &arguments); 262 263 ObjectState *bindObjectInState(ExecutionState &state, const MemoryObject *mo, 264 bool isLocal, const Array *array = 0); 265 266 /// Resolve a pointer to the memory objects it could point to the 267 /// start of, forking execution when necessary and generating errors 268 /// for pointers to invalid locations (either out of bounds or 269 /// address inside the middle of objects). 270 /// 271 /// \param results[out] A list of ((MemoryObject,ObjectState), 272 /// state) pairs for each object the given address can point to the 273 /// beginning of. 274 typedef std::vector< std::pair<std::pair<const MemoryObject*, const ObjectState*>, 275 ExecutionState*> > ExactResolutionList; 276 void resolveExact(ExecutionState &state, 277 ref<Expr> p, 278 ExactResolutionList &results, 279 const std::string &name); 280 281 /// Allocate and bind a new object in a particular state. NOTE: This 282 /// function may fork. 283 /// 284 /// \param isLocal Flag to indicate if the object should be 285 /// automatically deallocated on function return (this also makes it 286 /// illegal to free directly). 287 /// 288 /// \param target Value at which to bind the base address of the new 289 /// object. 290 /// 291 /// \param reallocFrom If non-zero and the allocation succeeds, 292 /// initialize the new object from the given one and unbind it when 293 /// done (realloc semantics). The initialized bytes will be the 294 /// minimum of the size of the old and new objects, with remaining 295 /// bytes initialized as specified by zeroMemory. 296 /// 297 /// \param allocationAlignment If non-zero, the given alignment is 298 /// used. Otherwise, the alignment is deduced via 299 /// Executor::getAllocationAlignment 300 void executeAlloc(ExecutionState &state, 301 ref<Expr> size, 302 bool isLocal, 303 KInstruction *target, 304 bool zeroMemory=false, 305 const ObjectState *reallocFrom=0, 306 size_t allocationAlignment=0); 307 308 /// Free the given address with checking for errors. If target is 309 /// given it will be bound to 0 in the resulting states (this is a 310 /// convenience for realloc). Note that this function can cause the 311 /// state to fork and that \ref state cannot be safely accessed 312 /// afterwards. 313 void executeFree(ExecutionState &state, 314 ref<Expr> address, 315 KInstruction *target = 0); 316 317 /// Serialize a landingpad instruction so it can be handled by the 318 /// libcxxabi-runtime 319 MemoryObject *serializeLandingpad(ExecutionState &state, 320 const llvm::LandingPadInst &lpi, 321 bool &stateTerminated); 322 323 /// Unwind the given state until it hits a landingpad. This is used 324 /// for exception handling. 325 void unwindToNextLandingpad(ExecutionState &state); 326 327 void executeCall(ExecutionState &state, 328 KInstruction *ki, 329 llvm::Function *f, 330 std::vector< ref<Expr> > &arguments); 331 332 // do address resolution / object binding / out of bounds checking 333 // and perform the operation 334 void executeMemoryOperation(ExecutionState &state, 335 bool isWrite, 336 ref<Expr> address, 337 ref<Expr> value /* undef if read */, 338 KInstruction *target /* undef if write */); 339 340 void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, 341 const std::string &name); 342 343 /// Create a new state where each input condition has been added as 344 /// a constraint and return the results. The input state is included 345 /// as one of the results. Note that the output vector may included 346 /// NULL pointers for states which were unable to be created. 347 void branch(ExecutionState &state, 348 const std::vector< ref<Expr> > &conditions, 349 std::vector<ExecutionState*> &result); 350 351 // Fork current and return states in which condition holds / does 352 // not hold, respectively. One of the states is necessarily the 353 // current state, and one of the states may be null. 354 StatePair fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal); 355 356 /// Add the given (boolean) condition as a constraint on state. This 357 /// function is a wrapper around the state's addConstraint function 358 /// which also manages propagation of implied values, 359 /// validity checks, and seed patching. 360 void addConstraint(ExecutionState &state, ref<Expr> condition); 361 362 // Called on [for now] concrete reads, replaces constant with a symbolic 363 // Used for testing. 364 ref<Expr> replaceReadWithSymbolic(ExecutionState &state, ref<Expr> e); 365 366 const Cell& eval(KInstruction *ki, unsigned index, 367 ExecutionState &state) const; 368 getArgumentCell(ExecutionState & state,KFunction * kf,unsigned index)369 Cell& getArgumentCell(ExecutionState &state, 370 KFunction *kf, 371 unsigned index) { 372 return state.stack.back().locals[kf->getArgRegister(index)]; 373 } 374 getDestCell(ExecutionState & state,KInstruction * target)375 Cell& getDestCell(ExecutionState &state, 376 KInstruction *target) { 377 return state.stack.back().locals[target->dest]; 378 } 379 380 void bindLocal(KInstruction *target, 381 ExecutionState &state, 382 ref<Expr> value); 383 void bindArgument(KFunction *kf, 384 unsigned index, 385 ExecutionState &state, 386 ref<Expr> value); 387 388 /// Evaluates an LLVM constant expression. The optional argument ki 389 /// is the instruction where this constant was encountered, or NULL 390 /// if not applicable/unavailable. 391 ref<klee::ConstantExpr> evalConstantExpr(const llvm::ConstantExpr *c, 392 const KInstruction *ki = NULL); 393 394 /// Evaluates an LLVM constant. The optional argument ki is the 395 /// instruction where this constant was encountered, or NULL if 396 /// not applicable/unavailable. 397 ref<klee::ConstantExpr> evalConstant(const llvm::Constant *c, 398 const KInstruction *ki = NULL); 399 400 /// Return a unique constant value for the given expression in the 401 /// given state, if it has one (i.e. it provably only has a single 402 /// value). Otherwise return the original expression. 403 ref<Expr> toUnique(const ExecutionState &state, ref<Expr> &e); 404 405 /// Return a constant value for the given expression, forcing it to 406 /// be constant in the given state by adding a constraint if 407 /// necessary. Note that this function breaks completeness and 408 /// should generally be avoided. 409 /// 410 /// \param purpose An identify string to printed in case of concretization. 411 ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e, 412 const char *purpose); 413 414 /// Bind a constant value for e to the given target. NOTE: This 415 /// function may fork state if the state has multiple seeds. 416 void executeGetValue(ExecutionState &state, ref<Expr> e, KInstruction *target); 417 418 /// Get textual information regarding a memory address. 419 std::string getAddressInfo(ExecutionState &state, ref<Expr> address) const; 420 421 // Determines the \param lastInstruction of the \param state which is not KLEE 422 // internal and returns its InstructionInfo 423 const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, 424 llvm::Instruction** lastInstruction); 425 426 bool shouldExitOn(enum TerminateReason termReason); 427 428 // remove state from queue and delete 429 void terminateState(ExecutionState &state); 430 // call exit handler and terminate state 431 void terminateStateEarly(ExecutionState &state, const llvm::Twine &message); 432 // call exit handler and terminate state 433 void terminateStateOnExit(ExecutionState &state); 434 // call error handler and terminate state 435 void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, 436 enum TerminateReason termReason, 437 const char *suffix = NULL, 438 const llvm::Twine &longMessage = ""); 439 440 // call error handler and terminate state, for execution errors 441 // (things that should not be possible, like illegal instruction or 442 // unlowered instrinsic, or are unsupported, like inline assembly) 443 void terminateStateOnExecError(ExecutionState &state, 444 const llvm::Twine &message, 445 const llvm::Twine &info="") { 446 terminateStateOnError(state, message, Exec, NULL, info); 447 } 448 449 /// bindModuleConstants - Initialize the module constant table. 450 void bindModuleConstants(); 451 452 template <typename SqType, typename TypeIt> 453 void computeOffsetsSeqTy(KGEPInstruction *kgepi, 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 460 /// bindInstructionConstants - Initialize any necessary per instruction 461 /// constant values. 462 void bindInstructionConstants(KInstruction *KI); 463 464 void doImpliedValueConcretization(ExecutionState &state, 465 ref<Expr> e, 466 ref<ConstantExpr> value); 467 468 /// check memory usage and terminate states when over threshold of -max-memory + 100MB 469 /// \return true if below threshold, false otherwise (states were terminated) 470 bool checkMemoryUsage(); 471 472 /// check if branching/forking is allowed 473 bool branchingPermitted(const ExecutionState &state) const; 474 475 void printDebugInstructions(ExecutionState &state); 476 void doDumpStates(); 477 478 /// Only for debug purposes; enable via debugger or klee-control 479 void dumpStates(); 480 void dumpPTree(); 481 482 public: 483 Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts, 484 InterpreterHandler *ie); 485 virtual ~Executor(); 486 getHandler()487 const InterpreterHandler& getHandler() { 488 return *interpreterHandler; 489 } 490 setPathWriter(TreeStreamWriter * tsw)491 void setPathWriter(TreeStreamWriter *tsw) override { pathWriter = tsw; } 492 setSymbolicPathWriter(TreeStreamWriter * tsw)493 void setSymbolicPathWriter(TreeStreamWriter *tsw) override { 494 symPathWriter = tsw; 495 } 496 setReplayKTest(const struct KTest * out)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 setReplayPath(const std::vector<bool> * path)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 useSeeds(const std::vector<struct KTest * > * seeds)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 setHaltExecution(bool value)521 void setHaltExecution(bool value) override { haltExecution = value; } 522 setInhibitForking(bool value)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 537 bool getSymbolicSolution( 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 549 /// Returns the errno location in memory of the state 550 int *getErrnoLocation(const ExecutionState &state) const; 551 getMergingSearcher()552 MergingSearcher *getMergingSearcher() const { return mergingSearcher; }; setMergingSearcher(MergingSearcher * ms)553 void setMergingSearcher(MergingSearcher *ms) { mergingSearcher = ms; }; 554 }; 555 556 } // End klee namespace 557 558 #endif /* KLEE_EXECUTOR_H */ 559