diff options
author | Frank Busse <bb0xfb@gmail.com> | 2020-06-16 18:33:26 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2020-06-24 13:48:18 +0100 |
commit | a36f7a20afaf6e477846cf72814ebe2c346d87ec (patch) | |
tree | 3ce7eeef77ce7b31f077cce68ec178775bd6e18c | |
parent | 623d7149dc629af9c8a85fe5d3f841d9deed2192 (diff) | |
download | klee-a36f7a20afaf6e477846cf72814ebe2c346d87ec.tar.gz |
slightly update ExecutionState, remove holes in struct
-rw-r--r-- | lib/Core/ExecutionState.cpp | 45 | ||||
-rw-r--r-- | lib/Core/ExecutionState.h | 62 |
2 files changed, 49 insertions, 58 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 94ac7888..b3719295 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -68,22 +68,20 @@ StackFrame::~StackFrame() { ExecutionState::ExecutionState(KFunction *kf) : pc(kf->instructions), prevPC(pc), - depth(0), - + ptreeNode(nullptr), + steppedInstructions(0), instsSinceCovNew(0), coveredNew(false), - forkDisabled(false), - ptreeNode(0), - steppedInstructions(0){ - pushFrame(0, kf); + forkDisabled(false) { + pushFrame(nullptr, kf); } -ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) - : constraints(assumptions), ptreeNode(0) {} +ExecutionState::ExecutionState(const std::vector<ref<Expr>> &assumptions) + : constraints(assumptions), ptreeNode(nullptr) {} ExecutionState::~ExecutionState() { - for (auto cur_mergehandler: openMergeStack){ + for (const auto &cur_mergehandler: openMergeStack){ cur_mergehandler->removeOpenState(this); } @@ -95,33 +93,29 @@ ExecutionState::ExecutionState(const ExecutionState& state): prevPC(state.prevPC), stack(state.stack), incomingBBIndex(state.incomingBBIndex), - + depth(state.depth), addressSpace(state.addressSpace), constraints(state.constraints), - queryCost(state.queryCost), - depth(state.depth), - pathOS(state.pathOS), symPathOS(state.symPathOS), - - instsSinceCovNew(state.instsSinceCovNew), - coveredNew(state.coveredNew), - forkDisabled(state.forkDisabled), coveredLines(state.coveredLines), ptreeNode(state.ptreeNode), symbolics(state.symbolics), arrayNames(state.arrayNames), openMergeStack(state.openMergeStack), - steppedInstructions(state.steppedInstructions) { - for (auto cur_mergehandler: openMergeStack) + steppedInstructions(state.steppedInstructions), + instsSinceCovNew(state.instsSinceCovNew), + coveredNew(state.coveredNew), + forkDisabled(state.forkDisabled) { + for (const auto &cur_mergehandler: openMergeStack) cur_mergehandler->addOpenState(this); } ExecutionState *ExecutionState::branch() { depth++; - ExecutionState *falseState = new ExecutionState(*this); + auto *falseState = new ExecutionState(*this); falseState->coveredNew = false; falseState->coveredLines.clear(); @@ -129,19 +123,18 @@ ExecutionState *ExecutionState::branch() { } void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) { - stack.push_back(StackFrame(caller,kf)); + stack.emplace_back(StackFrame(caller, kf)); } void ExecutionState::popFrame() { - StackFrame &sf = stack.back(); - for (std::vector<const MemoryObject*>::iterator it = sf.allocas.begin(), - ie = sf.allocas.end(); it != ie; ++it) - addressSpace.unbindObject(*it); + const StackFrame &sf = stack.back(); + for (const auto * memoryObject : sf.allocas) + addressSpace.unbindObject(memoryObject); stack.pop_back(); } void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array) { - symbolics.emplace_back(std::make_pair(ref<const MemoryObject>(mo), array)); + symbolics.emplace_back(ref<const MemoryObject>(mo), array); } /**/ diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index f9051195..176ffef6 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -65,13 +65,8 @@ struct StackFrame { /// @brief ExecutionState representing a path under exploration class ExecutionState { public: - typedef std::vector<StackFrame> stack_ty; + using stack_ty = std::vector<StackFrame>; -private: - // unsupported, use copy constructor - ExecutionState &operator=(const ExecutionState &); - -public: // Execution - Control Flow specific /// @brief Pointer to instruction to be executed after the current @@ -86,10 +81,13 @@ public: /// @brief Remember from which Basic Block control flow arrived /// (i.e. to select the right phi values) - unsigned incomingBBIndex; + std::uint32_t incomingBBIndex; // Overall state of the state - Data specific + /// @brief Exploration depth, i.e., number of times KLEE branched for this state + std::uint32_t depth; + /// @brief Address space used by this state (e.g. Global and Heap) AddressSpace addressSpace; @@ -101,9 +99,6 @@ public: /// @brief Costs for all queries issued for this state, in seconds mutable time::Span queryCost; - /// @brief Exploration depth, i.e., number of times KLEE branched for this state - unsigned depth; - /// @brief History of complete path: represents branches taken to /// reach/create this state (both concrete and symbolic) TreeOStream pathOS; @@ -112,18 +107,8 @@ public: /// taken to reach/create this state TreeOStream symPathOS; - /// @brief Counts how many instructions were executed since the last new - /// instruction was covered. - unsigned instsSinceCovNew; - - /// @brief Whether a new instruction was covered in this state - bool coveredNew; - - /// @brief Disables forking for this state. Set by user code - bool forkDisabled; - /// @brief Set containing which lines in which files are covered by this state - std::map<const std::string *, std::set<unsigned> > coveredLines; + std::map<const std::string *, std::set<std::uint32_t>> coveredLines; /// @brief Pointer to the process tree of the current state PTreeNode *ptreeNode; @@ -136,24 +121,37 @@ public: /// @brief Set of used array names for this state. Used to avoid collisions. std::set<std::string> arrayNames; - // The objects handling the klee_open_merge calls this state ran through - std::vector<ref<MergeHandler> > openMergeStack; + /// @brief The objects handling the klee_open_merge calls this state ran through + std::vector<ref<MergeHandler>> openMergeStack; - // The numbers of times this state has run through Executor::stepInstruction + /// @brief The numbers of times this state has run through Executor::stepInstruction std::uint64_t steppedInstructions; -private: - ExecutionState() : ptreeNode(0) {} + /// @brief Counts how many instructions were executed since the last new + /// instruction was covered. + std::uint32_t instsSinceCovNew; -public: - ExecutionState(KFunction *kf); + /// @brief Whether a new instruction was covered in this state + bool coveredNew; + /// @brief Disables forking for this state. Set by user code + bool forkDisabled; + +public: + // ctors + explicit ExecutionState(KFunction *kf); // XXX total hack, just used to make a state so solver can // use on structure - ExecutionState(const std::vector<ref<Expr> > &assumptions); - + explicit ExecutionState(const std::vector<ref<Expr>> &assumptions); + // copy ctor ExecutionState(const ExecutionState &state); - + // no copy assignment, use copy constructor + ExecutionState &operator=(const ExecutionState &) = delete; + // no move ctor + ExecutionState(ExecutionState &&) noexcept = delete; + // no move assignment + ExecutionState& operator=(ExecutionState &&) noexcept = delete; + // dtor ~ExecutionState(); ExecutionState *branch(); @@ -162,7 +160,7 @@ public: 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(std::move(e)); } bool merge(const ExecutionState &b); void dumpStack(llvm::raw_ostream &out) const; |