UnitTestBot · misonijnik · Oct 12, 2023 · Oct 10, 2023
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
@@ -127,6 +127,7 @@ struct ExecutionStack {
   inline value_stack_ty &valueStack() { return valueStack_; }
   inline const value_stack_ty &valueStack() const { return valueStack_; }
   inline const call_stack_ty &callStack() const { return callStack_; }
+  inline const info_stack_ty &infoStack() const { return infoStack_; }
   inline info_stack_ty &infoStack() { return infoStack_; }
   inline const call_stack_ty &uniqueFrames() const { return uniqueFrames_; }
 
@@ -491,16 +492,18 @@ class ExecutionState {
   bool reachedTarget(ref<ReachBlockTarget> target) const;
   static std::uint32_t getLastID() { return nextID - 1; };
 
-  inline bool isStuck(unsigned long long bound) {
-    KInstruction *prevKI = prevPC;
-    if (prevKI->inst->isTerminator() && stack.size() > 0) {
-      auto level = stack.infoStack().back().multilevel[getPCBlock()].second;
-      return bound && level > bound;
+  inline bool isStuck(unsigned long long bound) const {
+    if (bound == 0)
+      return false;
+    if (prevPC->inst->isTerminator() && stack.size() > 0) {
+      auto &ml = stack.infoStack().back().multilevel;
+      auto level = ml.find(getPCBlock());
+      return level != ml.end() && level->second > bound;
     }
     if (pc == pc->parent->getFirstInstruction() &&
         pc->parent == pc->parent->parent->entryKBlock) {
-      auto level = stack.multilevel[stack.callStack().back().kf].second;
-      return bound && level > bound;
+      auto level = stack.multilevel.at(stack.callStack().back().kf);
+      return level > bound;
     }
     return false;
   }

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -4295,8 +4295,6 @@ void Executor::run(std::vector<ExecutionState *> initialStates) {
   while (!states.empty() && !haltExecution) {
     while (!searcher->empty() && !haltExecution) {
       ExecutionState &state = searcher->selectState();
-      KInstruction *prevKI = state.prevPC;
-      KFunction *kf = prevKI->parent->parent;
 
       executeStep(state);
     }
@@ -4375,8 +4373,6 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
 };
 
 void Executor::executeStep(ExecutionState &state) {
-  KInstruction *prevKI = state.prevPC;
-
   if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance &&
       stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) {
     state.clearCoveredNew();
@@ -4389,13 +4385,7 @@ void Executor::executeStep(ExecutionState &state) {
   if (targetManager->isTargeted(state) && state.targets().empty()) {
     terminateStateEarlyAlgorithm(state, "State missed all it's targets.",
                                  StateTerminationType::MissedAllTargets);
-  } else if (prevKI->inst->isTerminator() && MaxCycles &&
-             (state.stack.infoStack()
-                      .back()
-                      .multilevel[state.getPCBlock()]
-                      .second > MaxCycles ||
-              state.stack.multilevel[state.stack.callStack().back().kf].second >
-                  MaxCycles)) {
+  } else if (state.isStuck(MaxCycles)) {
     terminateStateEarly(state, "max-cycles exceeded.",
                         StateTerminationType::MaxCycles);
   } else {

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
@@ -640,33 +640,94 @@ void BatchingSearcher::printName(llvm::raw_ostream &os) {
 
 ///
 
-IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(
-    Searcher *baseSearcher)
-    : baseSearcher{baseSearcher} {};
+class TimeMetric final : public IterativeDeepeningSearcher::Metric {
+  time::Point startTime;
+  time::Span time{time::seconds(1)};
 
-ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
+public:
+  void selectState() final { startTime = time::getWallTime(); }
+  bool exceeds(const ExecutionState &state) const final {
+    return time::getWallTime() - startTime > time;
+  }
+  void increaseLimit() final {
+    time *= 2U;
+    klee_message("increased time budget to %f seconds", time.toSeconds());
+  }
+};
+
+class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric {
+public:
+  using ty = unsigned long long;
+
+private:
+  ty maxCycles;
+
+public:
+  explicit MaxCyclesMetric(ty maxCycles) : maxCycles(maxCycles){};
+  explicit MaxCyclesMetric() : MaxCyclesMetric(1ULL){};
+
+  bool exceeds(const ExecutionState &state) const final {
+    return state.isStuck(maxCycles);
+  }
+  void increaseLimit() final {
+    maxCycles *= 2ULL;
+    klee_message("increased max-cycles to %llu", maxCycles);
+  }
+};
+
+IterativeDeepeningSearcher::IterativeDeepeningSearcher(
+    Searcher *baseSearcher, TargetManagerSubscriber *tms,
+    HaltExecution::Reason m)
+    : baseSearcher{baseSearcher}, tms{tms} {
+  switch (m) {
+  case HaltExecution::Reason::MaxTime:
+    metric = std::make_unique<TimeMetric>();
+    return;
+  case HaltExecution::Reason::MaxCycles:
+    metric = std::make_unique<MaxCyclesMetric>();
+    return;
+  default:
+    klee_error("Illegal metric for iterative deepening searcher: %d", m);
+  }
+}
+
+ExecutionState &IterativeDeepeningSearcher::selectState() {
   ExecutionState &res = baseSearcher->selectState();
-  startTime = time::getWallTime();
+  metric->selectState();
   return res;
 }
 
-void IterativeDeepeningTimeSearcher::update(
-    ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
-    const std::vector<ExecutionState *> &removedStates) {
+void IterativeDeepeningSearcher::filter(const StatesVector &states,
+                                        StatesVector &result) const {
+  StatesVector states1(states);
+  std::sort(states1.begin(), states1.end());
+  std::set_difference(states1.begin(), states1.end(), pausedStates.begin(),
+                      pausedStates.end(), std::back_inserter(result));
+}
 
-  const auto elapsed = time::getWallTime() - startTime;
+void IterativeDeepeningSearcher::update(
+    const TargetHistoryTargetPairToStatesMap &added,
+    const TargetHistoryTargetPairToStatesMap &removed) {
+  if (!tms)
+    return;
+  TargetHistoryTargetPairToStatesMap removedRefined(removed.size());
+  for (const auto &pair : removed) {
+    StatesVector refined;
+    IterativeDeepeningSearcher::filter(pair.second, refined);
+    removedRefined.emplace(pair.first, std::move(refined));
+  }
+  tms->update(added, removedRefined);
+}
+
+void IterativeDeepeningSearcher::update(ExecutionState *current,
+                                        const StatesVector &addedStates,
+                                        const StatesVector &removedStates) {
 
   // update underlying searcher (filter paused states unknown to underlying
   // searcher)
   if (!removedStates.empty()) {
-    std::vector<ExecutionState *> alt = removedStates;
-    for (const auto state : removedStates) {
-      auto it = pausedStates.find(state);
-      if (it != pausedStates.end()) {
-        pausedStates.erase(it);
-        alt.erase(std::remove(alt.begin(), alt.end(), state), alt.end());
-      }
-    }
+    StatesVector alt;
+    IterativeDeepeningSearcher::filter(removedStates, alt);
     baseSearcher->update(current, addedStates, alt);
   } else {
     baseSearcher->update(current, addedStates, removedStates);
@@ -676,27 +737,26 @@ void IterativeDeepeningTimeSearcher::update(
   if (current &&
       std::find(removedStates.begin(), removedStates.end(), current) ==
           removedStates.end() &&
-      elapsed > time) {
+      metric->exceeds(*current)) {
     pausedStates.insert(current);
     baseSearcher->update(nullptr, {}, {current});
   }
 
   // no states left in underlying searcher: fill with paused states
   if (baseSearcher->empty()) {
-    time *= 2U;
-    klee_message("increased time budget to %f\n", time.toSeconds());
-    std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
-    baseSearcher->update(nullptr, ps, std::vector<ExecutionState *>());
+    metric->increaseLimit();
+    StatesVector ps(pausedStates.begin(), pausedStates.end());
+    baseSearcher->update(nullptr, ps, {});
     pausedStates.clear();
   }
 }
 
-bool IterativeDeepeningTimeSearcher::empty() {
+bool IterativeDeepeningSearcher::empty() {
   return baseSearcher->empty() && pausedStates.empty();
 }
 
-void IterativeDeepeningTimeSearcher::printName(llvm::raw_ostream &os) {
-  os << "IterativeDeepeningTimeSearcher\n";
+void IterativeDeepeningSearcher::printName(llvm::raw_ostream &os) {
+  os << "IterativeDeepeningSearcher\n";
 }
 
 ///

diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
@@ -160,17 +160,10 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber {
   using TargetHistoryTargetPairHashMap =
       std::unordered_map<TargetHistoryTargetPair, T, TargetHistoryTargetHash,
                          TargetHistoryTargetCmp>;
-
-  using TargetHistoryTargetPair =
-      std::pair<ref<const TargetsHistory>, ref<Target>>;
   using TargetHistoryTargetPairToSearcherMap =
       std::unordered_map<TargetHistoryTargetPair,
                          std::unique_ptr<TargetedSearcher>,
                          TargetHistoryTargetHash, TargetHistoryTargetCmp>;
-  using StatesVector = std::vector<ExecutionState *>;
-  using TargetHistoryTargetPairToStatesMap =
-      std::unordered_map<TargetHistoryTargetPair, StatesVector,
-                         TargetHistoryTargetHash, TargetHistoryTargetCmp>;
   using TargetForestHisoryTargetVector = std::vector<TargetHistoryTargetPair>;
   using TargetForestHistoryTargetSet =
       std::unordered_set<TargetHistoryTargetPair, TargetHistoryTargetHash,
@@ -323,26 +316,43 @@ class BatchingSearcher final : public Searcher {
   void printName(llvm::raw_ostream &os) override;
 };
 
-/// IterativeDeepeningTimeSearcher implements time-based deepening. States
-/// are selected from an underlying searcher. When a state reaches its time
-/// limit it is paused (removed from underlying searcher). When the underlying
-/// searcher runs out of states, the time budget is increased and all paused
+/// IterativeDeepeningSearcher implements a metric-based deepening. States
+/// are selected from an underlying searcher. When a state exceeds its metric
+/// limit, it is paused (removed from underlying searcher). When the underlying
+/// searcher runs out of states, the metric limit is increased and all paused
 /// states are revived (added to underlying searcher).
-class IterativeDeepeningTimeSearcher final : public Searcher {
+class IterativeDeepeningSearcher final : public Searcher,
+                                         public TargetManagerSubscriber {
+public:
+  struct Metric {
+    virtual ~Metric() = default;
+    virtual void selectState(){};
+    virtual bool exceeds(const ExecutionState &state) const = 0;
+    virtual void increaseLimit() = 0;
+  };
+
+private:
   std::unique_ptr<Searcher> baseSearcher;
-  time::Point startTime;
-  time::Span time{time::seconds(1)};
+  TargetManagerSubscriber *tms;
+  std::unique_ptr<Metric> metric;
   std::set<ExecutionState *> pausedStates;
 
+  void filter(const std::vector<ExecutionState *> &states,
+              std::vector<ExecutionState *> &result) const;
+
 public:
   /// \param baseSearcher The underlying searcher (takes ownership).
-  explicit IterativeDeepeningTimeSearcher(Searcher *baseSearcher);
-  ~IterativeDeepeningTimeSearcher() override = default;
+  explicit IterativeDeepeningSearcher(Searcher *baseSearcher,
+                                      TargetManagerSubscriber *tms,
+                                      HaltExecution::Reason metric);
+  ~IterativeDeepeningSearcher() override = default;
 
   ExecutionState &selectState() override;
   void update(ExecutionState *current,
               const std::vector<ExecutionState *> &addedStates,
               const std::vector<ExecutionState *> &removedStates) override;
+  void update(const TargetHistoryTargetPairToStatesMap &added,
+              const TargetHistoryTargetPairToStatesMap &removed) override;
   bool empty() override;
   void printName(llvm::raw_ostream &os) override;
 };

diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
@@ -392,7 +392,7 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
 
     Instruction *inst = es.pc->inst;
     const KInstruction *ki = es.pc;
-    InfoStackFrame &sf = es.stack.infoStack().back();
+    auto &sf = es.stack.infoStack().back();
     theStatisticManager->setIndex(ki->getGlobalIndex());
     if (UseCallPaths)
       theStatisticManager->setContext(&sf.callPathNode->statistics);

diff --git a/lib/Core/TargetManager.h b/lib/Core/TargetManager.h
@@ -25,15 +25,15 @@
 namespace klee {
 class TargetCalculator;
 
+using TargetHistoryTargetPair =
+    std::pair<ref<const TargetsHistory>, ref<Target>>;
+using StatesVector = std::vector<ExecutionState *>;
+using TargetHistoryTargetPairToStatesMap =
+    std::unordered_map<TargetHistoryTargetPair, StatesVector,
+                       TargetHistoryTargetHash, TargetHistoryTargetCmp>;
+
 class TargetManagerSubscriber {
 public:
-  using TargetHistoryTargetPair =
-      std::pair<ref<const TargetsHistory>, ref<Target>>;
-  using StatesVector = std::vector<ExecutionState *>;
-  using TargetHistoryTargetPairToStatesMap =
-      std::unordered_map<TargetHistoryTargetPair, StatesVector,
-                         TargetHistoryTargetHash, TargetHistoryTargetCmp>;
-
   virtual ~TargetManagerSubscriber() = default;
 
   /// Selects a state for further exploration.
@@ -47,12 +47,6 @@ class TargetManager {
   using StatesSet = std::unordered_set<ExecutionState *>;
   using StateToDistanceMap =
       std::unordered_map<const ExecutionState *, TargetHashMap<DistanceResult>>;
-  using TargetHistoryTargetPair =
-      std::pair<ref<const TargetsHistory>, ref<Target>>;
-  using StatesVector = std::vector<ExecutionState *>;
-  using TargetHistoryTargetPairToStatesMap =
-      std::unordered_map<TargetHistoryTargetPair, StatesVector,
-                         TargetHistoryTargetHash, TargetHistoryTargetCmp>;
   using TargetForestHistoryTargetSet =
       std::unordered_set<TargetHistoryTargetPair, TargetHistoryTargetHash,
                          TargetHistoryTargetCmp>;

diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
@@ -55,11 +55,17 @@ cl::list<Searcher::CoreSearchType> CoreSearch(
         clEnumValN(Searcher::NURS_QC, "nurs:qc", "use NURS with Query-Cost")),
     cl::cat(SearchCat));
 
-cl::opt<bool> UseIterativeDeepeningTimeSearch(
-    "use-iterative-deepening-time-search",
-    cl::desc(
-        "Use iterative deepening time search (experimental) (default=false)"),
-    cl::init(false), cl::cat(SearchCat));
+cl::opt<HaltExecution::Reason> UseIterativeDeepeningSearch(
+    "use-iterative-deepening-search",
+    cl::desc("Use iterative deepening search based on metric (experimental) "
+             "(default=unspecified)"),
+    cl::values(clEnumValN(HaltExecution::Reason::Unspecified, "unspecified",
+                          "Do not use iterative deepening search (default)"),
+               clEnumValN(HaltExecution::Reason::MaxTime, "max-time",
+                          "metric is maximum time"),
+               clEnumValN(HaltExecution::Reason::MaxCycles, "max-cycles",
+                          "metric is maximum cycles")),
+    cl::init(HaltExecution::Reason::Unspecified), cl::cat(SearchCat));
 
 cl::opt<bool> UseBatchingSearch(
     "use-batching-search",
@@ -172,16 +178,22 @@ Searcher *klee::constructUserSearcher(Executor &executor,
                                     BatchInstructions);
   }
 
-  if (UseIterativeDeepeningTimeSearch) {
-    searcher = new IterativeDeepeningTimeSearcher(searcher);
-  }
-
+  TargetManagerSubscriber *tms = nullptr;
   if (executor.guidanceKind != Interpreter::GuidanceKind::NoGuidance) {
     searcher = new GuidedSearcher(searcher, *executor.distanceCalculator,
                                   executor.theRNG);
-    executor.targetManager->subscribe(*static_cast<GuidedSearcher *>(searcher));
+    tms = static_cast<GuidedSearcher *>(searcher);
   }
 
+  if (UseIterativeDeepeningSearch != HaltExecution::Reason::Unspecified) {
+    searcher = new IterativeDeepeningSearcher(searcher, tms,
+                                              UseIterativeDeepeningSearch);
+    tms = static_cast<IterativeDeepeningSearcher *>(searcher);
+  }
+
+  if (tms)
+    executor.targetManager->subscribe(*tms);
+
   llvm::raw_ostream &os = executor.getHandler().getInfoStream();
 
   os << "BEGIN searcher description\n";

diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c
@@ -18,13 +18,13 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --search=random-path --search=nurs:qc %t2.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search %t2.bc
+// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --use-batching-search %t2.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --use-batching-search --search=random-state %t2.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --use-batching-search --search=nurs:depth %t2.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-time-search --use-batching-search --search=nurs:qc %t2.bc
+// RUN: %klee --output-dir=%t.klee-out --use-iterative-deepening-search=max-time --use-batching-search --search=nurs:qc %t2.bc
 
 /* this test is basically just for coverage and doesn't really do any
    correctness check (aside from testing that the various combinations