[feat] Differentiate isCoveredNew and isCoveredNewError

UnitTestBot · Oct 7, 2023 · d5095be · d5095be
1 parent 8798ea5
commit d5095be
Show file tree

Hide file tree

Showing 4 changed files with 375 additions and 12 deletions.
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
@@ -121,7 +121,8 @@ ExecutionState::ExecutionState()
       depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
-      forkDisabled(false), prevHistory_(TargetsHistory::create()),
+      coveredNewError(new box<bool>(false)), forkDisabled(false),
+      prevHistory_(TargetsHistory::create()),
       history_(TargetsHistory::create()) {
   setID();
 }
@@ -131,7 +132,8 @@ ExecutionState::ExecutionState(KFunction *kf)
       depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
-      forkDisabled(false), prevHistory_(TargetsHistory::create()),
+      coveredNewError(new box<bool>(false)), forkDisabled(false),
+      prevHistory_(TargetsHistory::create()),
       history_(TargetsHistory::create()) {
   pushFrame(nullptr, kf);
   setID();
@@ -142,7 +144,8 @@ ExecutionState::ExecutionState(KFunction *kf, KBlock *kb)
       depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
       steppedMemoryInstructions(0), instsSinceCovNew(0),
       roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
-      forkDisabled(false), prevHistory_(TargetsHistory::create()),
+      coveredNewError(new box<bool>(false)), forkDisabled(false),
+      prevHistory_(TargetsHistory::create()),
       history_(TargetsHistory::create()) {
   pushFrame(nullptr, kf);
   setID();
@@ -170,11 +173,11 @@ ExecutionState::ExecutionState(const ExecutionState &state)
       unwindingInformation(state.unwindingInformation
                                ? state.unwindingInformation->clone()
                                : nullptr),
-      coveredNew(state.coveredNew), forkDisabled(state.forkDisabled),
-      returnValue(state.returnValue), gepExprBases(state.gepExprBases),
-      prevTargets_(state.prevTargets_), targets_(state.targets_),
-      prevHistory_(state.prevHistory_), history_(state.history_),
-      isTargeted_(state.isTargeted_) {
+      coveredNew(state.coveredNew), coveredNewError(state.coveredNewError),
+      forkDisabled(state.forkDisabled), returnValue(state.returnValue),
+      gepExprBases(state.gepExprBases), prevTargets_(state.prevTargets_),
+      targets_(state.targets_), prevHistory_(state.prevHistory_),
+      history_(state.history_), isTargeted_(state.isTargeted_) {
   queryMetaData.id = state.id;
 }
 

diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
@@ -366,6 +366,7 @@ class ExecutionState {
 
   /// @brief Whether a new instruction was covered in this state
   mutable std::deque<ref<box<bool>>> coveredNew;
+  mutable ref<box<bool>> coveredNewError;
 
   /// @brief Disables forking for this state. Set by user code
   bool forkDisabled = false;
@@ -507,7 +508,12 @@ class ExecutionState {
   bool isCoveredNew() const {
     return !coveredNew.empty() && coveredNew.back()->value;
   }
-  void coverNew() const { coveredNew.push_back(new box<bool>(true)); }
+  bool isCoveredNewError() const { return coveredNewError->value; }
+  void coverNew() const {
+    coveredNew.push_back(new box<bool>(true));
+    coveredNewError->value = false;
+    coveredNewError = new box<bool>(true);
+  }
   void updateCoveredNew() const {
     while (!coveredNew.empty() && !coveredNew.front()->value) {
       coveredNew.pop_front();
@@ -519,6 +525,7 @@ class ExecutionState {
     }
     coveredNew.clear();
   }
+  void clearCoveredNewError() const { coveredNewError->value = false; }
 };
 
 struct ExecutionStateIDCompare {

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -4355,9 +4355,9 @@ void Executor::initializeTypeManager() {
   typeSystemManager->initModule();
 }
 
-static bool shouldWriteTest(const ExecutionState &state) {
+static bool shouldWriteTest(const ExecutionState &state, bool isError = false) {
   state.updateCoveredNew();
-  bool coveredNew = state.isCoveredNew();
+  bool coveredNew = isError ? state.isCoveredNewError() : state.isCoveredNew();
   return !OnlyOutputStatesCoveringNew || coveredNew;
 }
 
@@ -4721,7 +4721,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
 
   if ((EmitAllErrors ||
        emittedErrors.insert(std::make_pair(lastInst, message)).second) &&
-      shouldWriteTest(state)) {
+      shouldWriteTest(state, true)) {
     std::string filepath = ki->getSourceFilepath();
     if (!filepath.empty()) {
       klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
@@ -4752,6 +4752,8 @@ void Executor::terminateStateOnError(ExecutionState &state,
     if (!info_str.empty())
       msg << "Info: \n" << info_str;
 
+    state.clearCoveredNewError();
+
     const std::string ext = terminationTypeFileExtension(terminationType);
     // use user provided suffix from klee_report_error()
     const char *file_suffix = suffix ? suffix : ext.c_str();