diff --git a/include/klee/ADT/Ref.h b/include/klee/ADT/Ref.h index 45e9632ca2..008580cc7e 100644 --- a/include/klee/ADT/Ref.h +++ b/include/klee/ADT/Ref.h @@ -227,6 +227,18 @@ inline std::stringstream &operator<<(std::stringstream &os, const ref &e) { return os; } +template class box { + friend class ref>; + +private: + /// @brief Required by klee::ref-managed objects + class ReferenceCounter _refCount; + +public: + box(T value_) : value(value_) {} + ReferenceCounter count() { return _refCount; } + T value; +}; } // end namespace klee namespace llvm { diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 5cc0a1dd1e..2b37c844ce 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -128,8 +128,9 @@ ExecutionState::ExecutionState() : initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1), depth(0), ptreeNode(nullptr), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), - roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false), - forkDisabled(false), prevHistory_(TargetsHistory::create()), + roundingMode(llvm::APFloat::rmNearestTiesToEven), + coveredNew(new box(false)), forkDisabled(false), + prevHistory_(TargetsHistory::create()), history_(TargetsHistory::create()) { setID(); } @@ -138,8 +139,9 @@ ExecutionState::ExecutionState(KFunction *kf) : initPC(kf->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1), depth(0), ptreeNode(nullptr), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), - roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false), - forkDisabled(false), prevHistory_(TargetsHistory::create()), + roundingMode(llvm::APFloat::rmNearestTiesToEven), + coveredNew(new box(false)), forkDisabled(false), + prevHistory_(TargetsHistory::create()), history_(TargetsHistory::create()) { pushFrame(nullptr, kf); setID(); @@ -149,8 +151,9 @@ ExecutionState::ExecutionState(KFunction *kf, KBlock *kb) : initPC(kb->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1), depth(0), ptreeNode(nullptr), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), - roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false), - forkDisabled(false), prevHistory_(TargetsHistory::create()), + roundingMode(llvm::APFloat::rmNearestTiesToEven), + coveredNew(new box(false)), forkDisabled(false), + prevHistory_(TargetsHistory::create()), history_(TargetsHistory::create()) { pushFrame(nullptr, kf); setID(); @@ -189,7 +192,6 @@ ExecutionState *ExecutionState::branch() { auto *falseState = new ExecutionState(*this); falseState->setID(); - falseState->coveredNew = false; falseState->coveredLines.clear(); return falseState; diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 93d24d5d34..8853cb2536 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -369,7 +369,7 @@ class ExecutionState { std::uint32_t id = 0; /// @brief Whether a new instruction was covered in this state - bool coveredNew = false; + mutable ref> coveredNew; /// @brief Disables forking for this state. Set by user code bool forkDisabled = false; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ff355b0b9f..761f832c47 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4053,7 +4053,7 @@ bool Executor::checkMemoryUsage() { unsigned idx = theRNG.getInt32() % N; // Make two pulls to try and not hit a state that // covered new code. - if (arr[idx]->coveredNew) + if (arr[idx]->coveredNew->value) idx = theRNG.getInt32() % N; std::swap(arr[idx], arr[N - 1]); @@ -4512,7 +4512,9 @@ void Executor::terminateState(ExecutionState &state, } static bool shouldWriteTest(const ExecutionState &state) { - return !OnlyOutputStatesCoveringNew || state.coveredNew; + bool coveredNew = state.coveredNew->value; + state.coveredNew->value = false; + return !OnlyOutputStatesCoveringNew || coveredNew; } static std::string terminationTypeFileExtension(StateTerminationType type) { @@ -7273,7 +7275,7 @@ void Executor::dumpStates() { *os << "{"; *os << "'depth' : " << es->depth << ", "; *os << "'queryCost' : " << es->queryMetaData.queryCost << ", "; - *os << "'coveredNew' : " << es->coveredNew << ", "; + *os << "'coveredNew' : " << es->coveredNew->value << ", "; *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", "; *os << "'md2u' : " << md2u << ", "; *os << "'icnt' : " << icnt << ", "; diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 372c6fc61b..e662644be3 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -411,7 +411,6 @@ void StatsTracker::stepInstruction(ExecutionState &es) { // FIXME: This trick no longer works, we should fix this in the line // number propogation. es.coveredLines[&ii.file].insert(ii.line); - es.coveredNew = true; es.instsSinceCovNew = 1; ++stats::coveredInstructions; stats::uncoveredInstructions += (uint64_t)-1; @@ -480,7 +479,6 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue, uint64_t hasFalse = theStatisticManager->getIndexedValue(stats::falseBranches, id); if (visitedTrue && !hasTrue) { - visitedTrue->coveredNew = true; visitedTrue->instsSinceCovNew = 1; ++stats::trueBranches; if (hasFalse) { @@ -491,7 +489,6 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue, hasTrue = 1; } if (visitedFalse && !hasFalse) { - visitedFalse->coveredNew = true; visitedFalse->instsSinceCovNew = 1; ++stats::falseBranches; if (hasTrue) { diff --git a/lib/Core/TargetCalculator.cpp b/lib/Core/TargetCalculator.cpp index 6b6a2f7d3e..0c5d72fedb 100644 --- a/lib/Core/TargetCalculator.cpp +++ b/lib/Core/TargetCalculator.cpp @@ -49,11 +49,22 @@ void TargetCalculator::update(const ExecutionState &state) { if (!coveredFunctionsInBranches.count(state.prevPC->parent->parent)) { unsigned index = 0; - coveredBranches[state.prevPC->parent->parent][state.prevPC->parent]; + if (!coveredBranches[state.prevPC->parent->parent].count( + state.prevPC->parent)) { + state.coveredNew->value = false; + state.coveredNew = new box(true); + coveredBranches[state.prevPC->parent->parent][state.prevPC->parent]; + } for (auto succ : successors(state.getPrevPCBlock())) { if (succ == state.getPCBlock()) { - coveredBranches[state.prevPC->parent->parent][state.prevPC->parent] - .insert(index); + if (!coveredBranches[state.prevPC->parent->parent] + [state.prevPC->parent] + .count(index)) { + state.coveredNew->value = false; + state.coveredNew = new box(true); + coveredBranches[state.prevPC->parent->parent][state.prevPC->parent] + .insert(index); + } break; } ++index;