chore: Add max-sym-cycles case in iterative deepening searcher

Author: misonijnik

include/klee/Core/TerminationTypes.h

@@ -94,6 +94,7 @@ enum Reason {
   MaxSteppedInstructions,
   MaxTime,
   MaxCycles,
+  MaxSymCycles,
   MaxForks,
   CovCheck,
   NoMoreStates,

lib/Core/Searcher.cpp

@@ -669,6 +669,26 @@ class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric {
   }
 };
 
+class MaxSymCyclesMetric final : public IterativeDeepeningSearcher::Metric {
+public:
+  using ty = unsigned long long;
+
+private:
+  ty maxCycles;
+
+public:
+  explicit MaxSymCyclesMetric(ty maxCycles) : maxCycles(maxCycles){};
+  explicit MaxSymCyclesMetric() : MaxSymCyclesMetric(1ULL){};
+
+  bool exceeds(const ExecutionState &state) const final {
+    return state.isSymbolicCycled(maxCycles);
+  }
+  void increaseLimit() final {
+    maxCycles *= 4ULL;
+    klee_message("increased max-sym-cycles to %llu", maxCycles);
+  }
+};
+
 IterativeDeepeningSearcher::IterativeDeepeningSearcher(Searcher *baseSearcher,
                                                        HaltExecution::Reason m)
     : baseSearcher{baseSearcher} {
@@ -679,6 +699,9 @@ IterativeDeepeningSearcher::IterativeDeepeningSearcher(Searcher *baseSearcher,
   case HaltExecution::Reason::MaxCycles:
     metric = std::make_unique<MaxCyclesMetric>();
     return;
+  case HaltExecution::Reason::MaxSymCycles:
+    metric = std::make_unique<MaxSymCyclesMetric>();
+    return;
   default:
     klee_error("Illegal metric for iterative deepening searcher: %d", m);
   }

lib/Core/UserSearcher.cpp

@@ -58,7 +58,9 @@ cl::opt<HaltExecution::Reason> UseIterativeDeepeningSearch(
                clEnumValN(HaltExecution::Reason::MaxTime, "max-time",
                           "metric is maximum time"),
                clEnumValN(HaltExecution::Reason::MaxCycles, "max-cycles",
-                          "metric is maximum cycles")),
+                          "metric is maximum cycles"),
+               clEnumValN(HaltExecution::Reason::MaxSymCycles, "max-sym-cycles",
+                          "metric is maximum symbolic cycles")),
     cl::init(HaltExecution::Reason::Unspecified), cl::cat(SearchCat));
 
 cl::opt<bool> UseBatchingSearch(

scripts/kleef

@@ -80,7 +80,7 @@ def klee_options(
         "--memory-backend=mixed",
         "--max-fixed-size-structures-size=64",
         "--use-intermittent-equalities-rewriter",
-        "--use-iterative-deepening-search=max-cycles",
+        "--use-iterative-deepening-search=max-sym-cycles",
         "--optimize=true",
     ]
     if run_forever: