From db655af90427e7c102108b14479130e07524f60e Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Fri, 14 Mar 2014 23:21:48 +0100 Subject: [Core] Documentation and cleanup * Removed unused member ShadowObjects in ExecutionState * Added documentation of members and reorder according to categories --- include/klee/ExecutionState.h | 115 +++++++++++++++++++--------- include/klee/Internal/Module/KInstruction.h | 2 +- 2 files changed, 79 insertions(+), 38 deletions(-) (limited to 'include') 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 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 allocas; + std::vector 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 stack_ty; private: // unsupported, use copy constructor - ExecutionState &operator=(const ExecutionState&); - std::map< std::string, std::string > fnAliases; + ExecutionState &operator=(const ExecutionState &); + + std::map 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 > coveredLines; + /// @brief Set containing which lines in which files are covered by this state + std::map > 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 > symbolics; + std::vector > 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 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 > &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 e) { - constraints.addConstraint(e); - } + void addConstraint(ref 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 > indices; /// offset - A constant offset to add to the pointer operand to execute the - /// insturction. + /// instruction. uint64_t offset; }; } -- cgit 1.4.1