diff options
| -rw-r--r-- | include/klee/ExecutionState.h | 115 | ||||
| -rw-r--r-- | include/klee/Internal/Module/KInstruction.h | 2 | ||||
| -rw-r--r-- | lib/Core/ExecutionState.cpp | 38 |
3 files changed, 100 insertions, 55 deletions
diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 97b700c1..eddf3d4a 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -23,14 +23,14 @@ #include <vector> namespace klee { - class Array; - class CallPathNode; - struct Cell; - struct KFunction; - struct KInstruction; - class MemoryObject; - class PTreeNode; - struct InstructionInfo; +class Array; +class CallPathNode; +struct Cell; +struct KFunction; +struct KInstruction; +class MemoryObject; +class PTreeNode; +struct InstructionInfo; llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); @@ -39,7 +39,7 @@ struct StackFrame { KFunction *kf; CallPathNode *callPathNode; - std::vector<const MemoryObject*> allocas; + std::vector<const MemoryObject *> allocas; Cell *locals; /// Minimum distance to an uncovered instruction once the function @@ -61,56 +61,100 @@ struct StackFrame { ~StackFrame(); }; +/// @brief ExecutionState representing the one state of execution class ExecutionState { public: typedef std::vector<StackFrame> stack_ty; private: // unsupported, use copy constructor - ExecutionState &operator=(const ExecutionState&); - std::map< std::string, std::string > fnAliases; + ExecutionState &operator=(const ExecutionState &); + + std::map<std::string, std::string> fnAliases; public: - bool fakeState; - unsigned depth; - - // pc - pointer to current instruction stream - KInstIterator pc, prevPC; + // Are we currently underconstrained? Hack: value is size to make fake + // objects. + unsigned underConstrained; + + /// Execution - Control Flow specific + + /// @brief pointer to instruction to be executed next after the current + /// instruction (prevPc) + KInstIterator pc; + + /// @brief Pointer to instruction which is currently executed + KInstIterator prevPC; + + /// @brief Stack representing the current instruction stream stack_ty stack; + + /// @brief Remember from which Basic Block control flow arrived (i.e. to + /// select the right phi values) + unsigned incomingBBIndex; + + /// Overall state of the state - Data specific + + /// @brief Address space used by this state (e.g. Global and Heap). + AddressSpace addressSpace; + + /// @brief Constraints collected so far ConstraintManager constraints; + + /// Statistics and information + + /// @brief Costs for all queries in seconds for this state mutable double queryCost; + + /// @brief Weight assigned for importance of this state. Can be used for + /// searchers to decide double weight; - AddressSpace addressSpace; - TreeOStream pathOS, symPathOS; + + /// @brief Counter how often KLEE branched for this state + unsigned depth; + + /// @brief History of complete path: Represents branches taken to reach/create + /// this state + /// Includes symbolic-based branches as well. + TreeOStream pathOS; + + /// @brief History of symbolic path: Represents branches taken but only + /// symbolic ones. + TreeOStream symPathOS; + + /// @brief Does not represent a real state just for patching purposes + bool fakeState; + + /// @brief Counts how many instructions were executed since the last new + /// instruction was covered. unsigned instsSinceCovNew; + + /// @brief Flag if new instruction was covered or not in this state bool coveredNew; - /// Disables forking, set by user code. + /// @brief Disables forking for this state. Set by user code. bool forkDisabled; - std::map<const std::string*, std::set<unsigned> > coveredLines; + /// @brief Set containing which lines in which files are covered by this state + std::map<const std::string *, std::set<unsigned> > coveredLines; + + /// @brief Representing pointer to process tree of current state PTreeNode *ptreeNode; - /// ordered list of symbolics: used to generate test cases. + /// ordered list of symbolics: used to generate test cases. // // FIXME: Move to a shared list structure (not critical). - std::vector< std::pair<const MemoryObject*, const Array*> > symbolics; + std::vector<std::pair<const MemoryObject *, const Array *> > symbolics; - /// Set of used array names. Used to avoid collisions. + /// @brief Set of used array names for this state. Used to avoid collisions. std::set<std::string> arrayNames; - // Used by the checkpoint/rollback methods for fake objects. - // FIXME: not freeing things on branch deletion. - MemoryMap shadowObjects; - - unsigned incomingBBIndex; - std::string getFnAlias(std::string fn); void addFnAlias(std::string old_fn, std::string new_fn); void removeFnAlias(std::string fn); - + private: - ExecutionState() : fakeState(false), ptreeNode(0) {} + ExecutionState() : underConstrained(0), fakeState(false), ptreeNode(0) {} public: ExecutionState(KFunction *kf); @@ -119,24 +163,21 @@ public: // use on structure ExecutionState(const std::vector<ref<Expr> > &assumptions); - ExecutionState(const ExecutionState& state); + ExecutionState(const ExecutionState &state); ~ExecutionState(); - + ExecutionState *branch(); void pushFrame(KInstIterator caller, KFunction *kf); void popFrame(); void addSymbolic(const MemoryObject *mo, const Array *array); - void addConstraint(ref<Expr> e) { - constraints.addConstraint(e); - } + void addConstraint(ref<Expr> e) { constraints.addConstraint(e); } bool merge(const ExecutionState &b); void dumpStack(llvm::raw_ostream &out) const; }; - } #endif diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h index fc86070b..62f514ff 100644 --- a/include/klee/Internal/Module/KInstruction.h +++ b/include/klee/Internal/Module/KInstruction.h @@ -50,7 +50,7 @@ namespace klee { std::vector< std::pair<unsigned, uint64_t> > indices; /// offset - A constant offset to add to the pointer operand to execute the - /// insturction. + /// instruction. uint64_t offset; }; } diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 5d32c936..1dc08624 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -66,13 +66,16 @@ StackFrame::~StackFrame() { /***/ -ExecutionState::ExecutionState(KFunction *kf) - : fakeState(false), - depth(0), +ExecutionState::ExecutionState(KFunction *kf) : + underConstrained(0), pc(kf->instructions), prevPC(pc), + queryCost(0.), weight(1), + depth(0), + + fakeState(false), instsSinceCovNew(0), coveredNew(false), forkDisabled(false), @@ -80,12 +83,9 @@ ExecutionState::ExecutionState(KFunction *kf) pushFrame(0, kf); } -ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) - : fakeState(true), - constraints(assumptions), - queryCost(0.), - ptreeNode(0) { -} +ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) + : underConstrained(0), constraints(assumptions), queryCost(0.), + fakeState(true), ptreeNode(0) {} ExecutionState::~ExecutionState() { for (unsigned int i=0; i<symbolics.size(); i++) @@ -100,28 +100,32 @@ ExecutionState::~ExecutionState() { while (!stack.empty()) popFrame(); } -ExecutionState::ExecutionState(const ExecutionState& state) - : fnAliases(state.fnAliases), - fakeState(state.fakeState), - depth(state.depth), +ExecutionState::ExecutionState(const ExecutionState& state): + fnAliases(state.fnAliases), + underConstrained(state.underConstrained), pc(state.pc), prevPC(state.prevPC), stack(state.stack), + incomingBBIndex(state.incomingBBIndex), + + addressSpace(state.addressSpace), constraints(state.constraints), + queryCost(state.queryCost), weight(state.weight), - addressSpace(state.addressSpace), + depth(state.depth), + pathOS(state.pathOS), symPathOS(state.symPathOS), + + fakeState(state.fakeState), instsSinceCovNew(state.instsSinceCovNew), coveredNew(state.coveredNew), forkDisabled(state.forkDisabled), coveredLines(state.coveredLines), ptreeNode(state.ptreeNode), symbolics(state.symbolics), - arrayNames(state.arrayNames), - shadowObjects(state.shadowObjects), - incomingBBIndex(state.incomingBBIndex) + arrayNames(state.arrayNames) { for (unsigned int i=0; i<symbolics.size(); i++) symbolics[i].first->refCount++; |