aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2020-06-16 18:33:26 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-06-24 13:48:18 +0100
commita36f7a20afaf6e477846cf72814ebe2c346d87ec (patch)
tree3ce7eeef77ce7b31f077cce68ec178775bd6e18c /lib/Core
parent623d7149dc629af9c8a85fe5d3f841d9deed2192 (diff)
downloadklee-a36f7a20afaf6e477846cf72814ebe2c346d87ec.tar.gz
slightly update ExecutionState, remove holes in struct
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutionState.cpp45
-rw-r--r--lib/Core/ExecutionState.h62
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;