[feat] Improve only-output-states-covering-new option

UnitTestBot · Sep 17, 2023 · d0d4033 · d0d4033
1 parent e2a864e
commit d0d4033
Show file tree

Hide file tree

Showing 6 changed files with 41 additions and 17 deletions.
diff --git 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<T> &e) {
   return os;
 }
 
+template <class T> class box {
+  friend class ref<box<T>>;
+
+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
@@ -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<bool>(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<bool>(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<bool>(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
@@ -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<box<bool>> 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
@@ -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
@@ -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
@@ -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<bool>(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<bool>(true);
+            coveredBranches[state.prevPC->parent->parent][state.prevPC->parent]
+                .insert(index);
+          }
           break;
         }
         ++index;