about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorJulian Büning <julian.buening@comsys.rwth-aachen.de>2020-04-11 16:43:01 +0200
committerCristian Cadar <c.cadar@imperial.ac.uk>2023-06-05 17:13:21 +0100
commitd3aee9c0e619fa097e296de81de93a09aaab82f2 (patch)
tree01bd41526ea0cbcb05f5092870fac47be9b409f4
parent3c42e214fb2ec4a101dd1e91e2d8c1ce4983a569 (diff)
downloadklee-d3aee9c0e619fa097e296de81de93a09aaab82f2.tar.gz
fix BatchingSearcher's disabled time budget
The functionality of the batching searcher that increases the time
budget if it is shorter than the time between two calls to
`selectState()` ignored the disabled time budget. Effectively, the
batching searcher thus picks a very arbitrary time budget on its own.
-rw-r--r--lib/Core/Searcher.cpp2
-rw-r--r--test/regression/2020-04-11-batching-search-zero-time-budget.c16
2 files changed, 17 insertions, 1 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 080c31aa..f5d6543f 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -423,7 +423,7 @@ ExecutionState &BatchingSearcher::selectState() {
         (time::getWallTime() - lastStartTime) > timeBudget)) ||
       ((instructionBudget > 0) &&
        (stats::instructions - lastStartInstructions) > instructionBudget)) {
-    if (lastState) {
+    if (lastState && timeBudget.toSeconds() > 0) {
       time::Span delta = time::getWallTime() - lastStartTime;
       auto t = timeBudget;
       t *= 1.1;
diff --git a/test/regression/2020-04-11-batching-search-zero-time-budget.c b/test/regression/2020-04-11-batching-search-zero-time-budget.c
new file mode 100644
index 00000000..46043f31
--- /dev/null
+++ b/test/regression/2020-04-11-batching-search-zero-time-budget.c
@@ -0,0 +1,16 @@
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-batching-search --batch-time=0 --batch-instructions=1 %t.bc 2>&1 | FileCheck %s
+
+#include <time.h>
+
+#include "klee/klee.h"
+
+int main(void) {
+  for (int i = 0; i < 10; ++i) {
+    struct timespec ts = {.tv_sec = 0, .tv_nsec = 10000000}; // 10 ms
+    nanosleep(&ts, NULL);
+  }
+  // CHECK-NOT: increased time budget
+  return 0;
+}