[feat] Added error classification on 'confident' and 'possible'.

S1eGa · S1eGa · commit 2d82e285ff36 · 2024-02-19T18:13:18.000+01:00
diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h
@@ -85,6 +85,8 @@ enum class StateTerminationType : std::uint8_t {
   /// \endcond
 };
 
+enum StateTerminationConfidenceCategory { CONFIDENT, PROBABLY };
+
 namespace HaltExecution {
 enum Reason {
   NotHalt = 0,
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
@@ -317,6 +317,9 @@ class ExecutionState {
 
   // Overall state of the state - Data specific
 
+  /// @brief: TODO:
+  bool lastBrConfidently = true;
+
   /// @brief Exploration depth, i.e., number of times KLEE branched for this
   /// state
   std::uint32_t depth = 0;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -40,6 +40,7 @@
 #include "klee/Config/Version.h"
 #include "klee/Config/config.h"
 #include "klee/Core/Interpreter.h"
+#include "klee/Core/TerminationTypes.h"
 #include "klee/Expr/ArrayExprOptimizer.h"
 #include "klee/Expr/ArrayExprVisitor.h"
 #include "klee/Expr/Assignment.h"
@@ -519,9 +520,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                    InterpreterHandler *ih)
     : Interpreter(opts), interpreterHandler(ih), searcher(nullptr),
       externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
-      pathWriter(0), symPathWriter(0),
-      specialFunctionHandler(0), timers{time::Span(TimerInterval)},
-      guidanceKind(opts.Guidance), codeGraphInfo(new CodeGraphInfo()),
+      pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
+      timers{time::Span(TimerInterval)}, guidanceKind(opts.Guidance),
+      codeGraphInfo(new CodeGraphInfo()),
       distanceCalculator(new DistanceCalculator(*codeGraphInfo)),
       targetCalculator(new TargetCalculator(*codeGraphInfo)),
       targetManager(new TargetManager(guidanceKind, *distanceCalculator,
@@ -2728,6 +2729,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       if (bi->getMetadata("md.ret")) {
         state.stack.forceReturnLocation(locationOf(state));
       }
+      state.lastBrConfidently = true;
 
       transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state);
     } else {
@@ -2747,6 +2749,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         maxNewStateStackSize =
             std::max(maxNewStateStackSize,
                      branches.first->stack.stackRegisterSize() * 8);
+        branches.first->lastBrConfidently = false;
+        branches.second->lastBrConfidently = false;
+      } else {
+        (branches.first ? branches.first : branches.second)->lastBrConfidently =
+            true;
       }
 
       // NOTE: There is a hidden dependency here, markBranchVisited
@@ -4018,9 +4025,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (iIdx >= vt->getNumElements()) {
       // Out of bounds write
       terminateStateOnProgramError(
-          state, new ErrorEvent(locationOf(state),
-                                StateTerminationType::BadVectorAccess,
-                                "Out of bounds write when inserting element"));
+          state,
+          new ErrorEvent(locationOf(state),
+                         StateTerminationType::BadVectorAccess,
+                         "Out of bounds write when inserting element"),
+          StateTerminationConfidenceCategory::CONFIDENT);
       return;
     }
 
@@ -4061,9 +4070,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (iIdx >= vt->getNumElements()) {
       // Out of bounds read
       terminateStateOnProgramError(
-          state, new ErrorEvent(locationOf(state),
-                                StateTerminationType::BadVectorAccess,
-                                "Out of bounds read when extracting element"));
+          state,
+          new ErrorEvent(locationOf(state),
+                         StateTerminationType::BadVectorAccess,
+                         "Out of bounds read when extracting element"),
+          StateTerminationConfidenceCategory::CONFIDENT);
       return;
     }
 
@@ -4967,28 +4978,41 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
     terminationType = StateTerminationType::User;
   }
   terminateStateOnProgramError(
-      state, new ErrorEvent(locationOf(state), terminationType, messaget));
+      state, new ErrorEvent(locationOf(state), terminationType, messaget),
+      StateTerminationConfidenceCategory::CONFIDENT);
 }
 
-void Executor::terminateStateOnError(ExecutionState &state,
-                                     const llvm::Twine &messaget,
-                                     StateTerminationType terminationType,
-                                     const llvm::Twine &info,
-                                     const char *suffix) {
+void Executor::terminateStateOnError(
+    ExecutionState &state, const llvm::Twine &messaget,
+    StateTerminationType terminationType,
+    StateTerminationConfidenceCategory confidence, const llvm::Twine &info,
+    const char *suffix) {
   std::string message = messaget.str();
-  static std::set<std::pair<Instruction *, std::string>> emittedErrors;
+  static std::set<
+      std::pair<Instruction *,
+                std::pair<StateTerminationConfidenceCategory, std::string>>>
+      emittedErrors;
   const KInstruction *ki = getLastNonKleeInternalInstruction(state);
   Instruction *lastInst = ki->inst();
 
-  if ((EmitAllErrors ||
-       emittedErrors.insert(std::make_pair(lastInst, message)).second) &&
+  if ((EmitAllErrors || emittedErrors
+                            .insert(std::make_pair(
+                                lastInst, std::make_pair(confidence, message)))
+                            .second) &&
       shouldWriteTest(state, true)) {
     std::string filepath = ki->getSourceFilepath();
+
+    std::string prefix =
+        (confidence == StateTerminationConfidenceCategory::CONFIDENT
+             ? "ERROR"
+             : "POSSIBLE ERROR");
+
     if (!filepath.empty()) {
-      klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
-                   message.c_str());
+      klee_message((prefix + ": %s:%zu: %s").c_str(), filepath.c_str(),
+                   ki->getLine(), message.c_str());
     } else {
-      klee_message("ERROR: (location information missing) %s", message.c_str());
+      klee_message((prefix + ": (location information missing) %s").c_str(),
+                   message.c_str());
     }
     if (!EmitAllErrors)
       klee_message("NOTE: now ignoring this error at this location");
@@ -5034,13 +5058,14 @@ void Executor::terminateStateOnExecError(ExecutionState &state,
   assert(reason > StateTerminationType::USERERR &&
          reason <= StateTerminationType::EXECERR);
   ++stats::terminationExecutionError;
-  terminateStateOnError(state, message, reason, "");
+  terminateStateOnError(state, message, reason,
+                        StateTerminationConfidenceCategory::CONFIDENT, "");
 }
 
-void Executor::terminateStateOnProgramError(ExecutionState &state,
-                                            const ref<ErrorEvent> &reason,
-                                            const llvm::Twine &info,
-                                            const char *suffix) {
+void Executor::terminateStateOnProgramError(
+    ExecutionState &state, const ref<ErrorEvent> &reason,
+    StateTerminationConfidenceCategory confidence, const llvm::Twine &info,
+    const char *suffix) {
   assert(reason->ruleID > StateTerminationType::SOLVERERR &&
          reason->ruleID <= StateTerminationType::PROGERR);
   ++stats::terminationProgramError;
@@ -5059,19 +5084,22 @@ void Executor::terminateStateOnProgramError(ExecutionState &state,
   }
   state.eventsRecorder.record(reason);
 
-  terminateStateOnError(state, reason->message, reason->ruleID, info, suffix);
+  terminateStateOnError(state, reason->message, reason->ruleID, confidence,
+                        info, suffix);
 }
 
 void Executor::terminateStateOnSolverError(ExecutionState &state,
                                            const llvm::Twine &message) {
   ++stats::terminationSolverError;
-  terminateStateOnError(state, message, StateTerminationType::Solver, "");
+  terminateStateOnError(state, message, StateTerminationType::Solver,
+                        StateTerminationConfidenceCategory::CONFIDENT, "");
 }
 
 void Executor::terminateStateOnUserError(ExecutionState &state,
                                          const llvm::Twine &message) {
   ++stats::terminationUserError;
-  terminateStateOnError(state, message, StateTerminationType::User, "");
+  terminateStateOnError(state, message, StateTerminationType::User,
+                        StateTerminationConfidenceCategory::CONFIDENT, "");
 }
 
 // XXX shoot me
@@ -5442,13 +5470,20 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
             new ErrorEvent(new AllocEvent(mo->allocSite),
                            locationOf(*it->second), StateTerminationType::Free,
                            "free of alloca"),
+            rl.size() != 1 ? StateTerminationConfidenceCategory::PROBABLY
+                           : StateTerminationConfidenceCategory::CONFIDENT,
             getAddressInfo(*it->second, address));
       } else if (mo->isGlobal) {
+        if (rl.size() != 1) {
+          klee_warning("Following error if likely false positive");
+        }
         terminateStateOnProgramError(
             *it->second,
             new ErrorEvent(new AllocEvent(mo->allocSite),
                            locationOf(*it->second), StateTerminationType::Free,
                            "free of global"),
+            rl.size() != 1 ? StateTerminationConfidenceCategory::PROBABLY
+                           : StateTerminationConfidenceCategory::CONFIDENT,
             getAddressInfo(*it->second, address));
       } else {
         it->second->removePointerResolutions(mo);
@@ -5544,6 +5579,8 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
           *unbound,
           new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr,
                          "memory error: invalid pointer: " + name),
+          !results.empty() ? StateTerminationConfidenceCategory::PROBABLY
+                           : StateTerminationConfidenceCategory::CONFIDENT,
           getAddressInfo(*unbound, address));
     }
   }
@@ -5633,7 +5670,7 @@ void Executor::concretizeSize(ExecutionState &state, ref<Expr> size,
             new ErrorEvent(locationOf(*hugeSize.second),
                            StateTerminationType::Model,
                            "concretized symbolic size"),
-            info.str());
+            StateTerminationConfidenceCategory::CONFIDENT, info.str());
       }
     }
   }
@@ -6359,7 +6396,8 @@ void Executor::executeMemoryOperation(
               *state,
               new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*state),
                              StateTerminationType::ReadOnly,
-                             "memory error: object read only"));
+                             "memory error: object read only"),
+              StateTerminationConfidenceCategory::CONFIDENT);
         } else {
           wos->write(mo->getOffsetExpr(address), value);
         }
@@ -6431,6 +6469,10 @@ void Executor::executeMemoryOperation(
     return;
   }
 
+  bool mayBeFalsePositive =
+      resolvedMemoryObjects.size() > 1 ||
+      (resolvedMemoryObjects.size() == 1 && mayBeOutOfBound);
+
   ExecutionState *unbound = nullptr;
   if (MergedPointerDereference) {
     ref<Expr> guard;
@@ -6488,7 +6530,10 @@ void Executor::executeMemoryOperation(
                 new ErrorEvent(new AllocEvent(mo->allocSite),
                                locationOf(*branches.first),
                                StateTerminationType::ReadOnly,
-                               "memory error: object read only"));
+                               "memory error: object read only"),
+                mayBeFalsePositive
+                    ? StateTerminationConfidenceCategory::PROBABLY
+                    : StateTerminationConfidenceCategory::CONFIDENT);
             state = branches.second;
           } else {
             ref<Expr> result = SelectExpr::create(
@@ -6560,7 +6605,10 @@ void Executor::executeMemoryOperation(
               *bound,
               new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*bound),
                              StateTerminationType::ReadOnly,
-                             "memory error: object read only"));
+                             "memory error: object read only"),
+              mayBeFalsePositive
+                  ? StateTerminationConfidenceCategory::PROBABLY
+                  : StateTerminationConfidenceCategory::CONFIDENT);
         } else {
           wos->write(mo->getOffsetExpr(address), value);
         }
@@ -6622,6 +6670,8 @@ void Executor::executeMemoryOperation(
             new ErrorEvent(new AllocEvent(baseObjectPair.first->allocSite),
                            locationOf(*unbound), StateTerminationType::Ptr,
                            "memory error: out of bound pointer"),
+            mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
+                               : StateTerminationConfidenceCategory::CONFIDENT,
             getAddressInfo(*unbound, address));
         return;
       }
@@ -6631,6 +6681,8 @@ void Executor::executeMemoryOperation(
         *unbound,
         new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr,
                        "memory error: out of bound pointer"),
+        mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
+                           : StateTerminationConfidenceCategory::CONFIDENT,
         getAddressInfo(*unbound, address));
   }
 }
@@ -6864,8 +6916,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
                (!AllowSeedTruncation && obj->numBytes > mo->size))) {
             std::stringstream msg;
             msg << "replace size mismatch: " << mo->name << "[" << mo->size
-                << "]"
-                << " vs " << obj->name << "[" << obj->numBytes << "]"
+                << "]" << " vs " << obj->name << "[" << obj->numBytes << "]"
                 << " in test\n";
 
             terminateStateOnUserError(state, msg.str());
@@ -7309,8 +7360,7 @@ void Executor::logState(const ExecutionState &state, int id,
     *f << "Address memory object: " << object.first->address << "\n";
     *f << "Memory object size: " << object.first->size << "\n";
   }
-  *f << state.symbolics.size() << " symbolics total. "
-     << "Symbolics:\n";
+  *f << state.symbolics.size() << " symbolics total. " << "Symbolics:\n";
   size_t sc = 0;
   for (const auto &symbolic : state.symbolics) {
     *f << "Symbolic number " << sc++ << "\n";
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
@@ -618,6 +618,7 @@ class Executor : public Interpreter {
   /// below.
   void terminateStateOnError(ExecutionState &state, const llvm::Twine &message,
                              StateTerminationType reason,
+                             StateTerminationConfidenceCategory confidence,
                              const llvm::Twine &longMessage = "",
                              const char *suffix = nullptr);
 
@@ -629,10 +630,10 @@ class Executor : public Interpreter {
 
   /// Call error handler and terminate state in case of program errors
   /// (e.g. free()ing globals, out-of-bound accesses)
-  void terminateStateOnProgramError(ExecutionState &state,
-                                    const ref<ErrorEvent> &reason,
-                                    const llvm::Twine &longMessage = "",
-                                    const char *suffix = nullptr);
+  void terminateStateOnProgramError(
+      ExecutionState &state, const ref<ErrorEvent> &reason,
+      StateTerminationConfidenceCategory confidence,
+      const llvm::Twine &longMessage = "", const char *suffix = nullptr);
 
   void terminateStateOnTerminator(ExecutionState &state);
 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
diff --git a/lib/Support/ErrorHandling.cpp b/lib/Support/ErrorHandling.cpp
