about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-03-15 20:47:47 +0000
committerMartinNowack <martin.nowack@gmail.com>2019-03-16 21:23:24 +0000
commitc1d3977f07ddbf840ca3cdbd580239921a9c5f91 (patch)
tree92774b4a261228f4ae5523850a2efce122b00e6c
parentd44d507631c345edf33ee7f6ecf7fd942af7760b (diff)
downloadklee-c1d3977f07ddbf840ca3cdbd580239921a9c5f91.tar.gz
Added support for disabling --batch-instructions and --batch-time by setting them to 0
-rw-r--r--lib/Core/Searcher.cpp8
-rw-r--r--lib/Core/UserSearcher.cpp31
2 files changed, 23 insertions, 16 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index db295468..47457a91 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -351,9 +351,11 @@ BatchingSearcher::~BatchingSearcher() {
 }
 
 ExecutionState &BatchingSearcher::selectState() {
-  if (!lastState || 
-      (time::getWallTime() - lastStartTime) > timeBudget ||
-      (stats::instructions - lastStartInstructions) > instructionBudget) {
+  if (!lastState ||
+      (((timeBudget.toSeconds() > 0) &&
+        (time::getWallTime() - lastStartTime) > timeBudget)) ||
+      ((instructionBudget > 0) &&
+       (stats::instructions - lastStartInstructions) > instructionBudget)) {
     if (lastState) {
       time::Span delta = time::getWallTime() - lastStartTime;
       auto t = timeBudget;
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 754b3796..7efdb30d 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -56,25 +56,30 @@ 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::init(false),
+    cl::cat(SearchCat));
 
 cl::opt<bool> UseBatchingSearch(
     "use-batching-search",
     cl::desc("Use batching searcher (keep running selected state for N "
              "instructions/time, see --batch-instructions and --batch-time) "
              "(default=false)"),
-    cl::init(false), cl::cat(SearchCat));
-
-cl::opt<unsigned>
-    BatchInstructions("batch-instructions",
-                      cl::desc("Number of instructions to batch when using "
-                               "--use-batching-search (default=10000)"),
-                      cl::init(10000), cl::cat(SearchCat));
-
-cl::opt<std::string> BatchTime("batch-time",
-                               cl::desc("Amount of time to batch when using "
-                                        "--use-batching-search (default=5s)"),
-                               cl::init("5s"), cl::cat(SearchCat));
+    cl::init(false),
+    cl::cat(SearchCat));
+
+cl::opt<unsigned> BatchInstructions(
+    "batch-instructions",
+    cl::desc("Number of instructions to batch when using "
+             "--use-batching-search.  Set to 0 to disable (default=10000)"),
+    cl::init(10000),
+    cl::cat(SearchCat));
+
+cl::opt<std::string> BatchTime(
+    "batch-time",
+    cl::desc("Amount of time to batch when using "
+             "--use-batching-search.  Set to 0s to disable (default=5s)"),
+    cl::init("5s"),
+    cl::cat(SearchCat));
 
 } // namespace