Skip to content

Commit d8ff87b

Browse files
Columpiomisonijnik
authored andcommitted
[feat] Cover on the fly based on time
1 parent 0583657 commit d8ff87b

3 files changed

Lines changed: 21 additions & 12 deletions

File tree

lib/Core/Executor.cpp

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -249,10 +249,10 @@ cl::opt<bool> CoverOnTheFly(
249249
"(default=false, i.e. one per (error,instruction) pair)"),
250250
cl::cat(TestGenCat));
251251

252-
cl::opt<unsigned> DelayCoverOnTheFly(
253-
"delay-cover-on-the-fly", cl::init(10000),
254-
cl::desc("Start on the fly tests generation after this many instructions "
255-
"(default=10000)"),
252+
cl::opt<std::string> DelayCoverOnTheFly(
253+
"delay-cover-on-the-fly", cl::init("0s"),
254+
cl::desc("Start on the fly tests generation after the specified duration. "
255+
"Set to 0s to disable (default=0s)"),
256256
cl::cat(TestGenCat));
257257

258258
cl::opt<unsigned> UninitMemoryTestMultiplier(
@@ -487,15 +487,23 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
487487
targetedExecutionManager(
488488
new TargetedExecutionManager(*codeGraphInfo, *targetManager)),
489489
replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false),
490-
inhibitForking(false), haltExecution(HaltExecution::NotHalt),
491-
ivcEnabled(false), debugLogBuffer(debugBufferString) {
490+
inhibitForking(false), coverOnTheFly(false),
491+
haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
492+
debugLogBuffer(debugBufferString) {
492493
const time::Span maxTime{MaxTime};
493494
if (maxTime)
494495
timers.add(std::make_unique<Timer>(maxTime, [&] {
495496
klee_message("HaltTimer invoked");
496497
setHaltExecution(HaltExecution::MaxTime);
497498
}));
498499

500+
if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance) {
501+
const time::Span delayTime{DelayCoverOnTheFly};
502+
if (delayTime)
503+
timers.add(
504+
std::make_unique<Timer>(delayTime, [&] { coverOnTheFly = true; }));
505+
}
506+
499507
coreSolverTimeout = time::Span{MaxCoreSolverTime};
500508
if (coreSolverTimeout)
501509
UseForkedCoreSolver = true;
@@ -4381,8 +4389,8 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {
43814389

43824390
void Executor::executeStep(ExecutionState &state) {
43834391
KFunction *initKF = state.initPC->parent->parent;
4384-
if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance &&
4385-
stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) {
4392+
4393+
if (coverOnTheFly && shouldWriteTest(state)) {
43864394
state.clearCoveredNew();
43874395
interpreterHandler->processTestCase(
43884396
state, nullptr,

lib/Core/Executor.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -208,6 +208,9 @@ class Executor : public Interpreter {
208208
/// Disables forking, set by client. \see setInhibitForking()
209209
bool inhibitForking;
210210

211+
/// Should it generate test cases for each new covered block or branch
212+
bool coverOnTheFly;
213+
211214
/// Signals the executor to halt execution at the next instruction
212215
/// step.
213216
HaltExecution::Reason haltExecution = HaltExecution::NotHalt;

test/Feature/CoverOnTheFly.c

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,10 @@
22
// REQUIRES: not-asan
33
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
44
// RUN: rm -rf %t.klee-out
5-
// RUN: %klee --only-output-states-covering-new --max-instructions=2000 --delay-cover-on-the-fly=500 --dump-states-on-halt=false --cover-on-the-fly --search=bfs --use-guided-search=none --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
5+
// RUN: %klee --only-output-states-covering-new --max-instructions=2000 --timer-interval=1ms --delay-cover-on-the-fly=1ms --dump-states-on-halt=false --cover-on-the-fly --search=bfs --use-guided-search=none --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
66

77
#include "klee/klee.h"
88

9-
#define a (2)
109
int main() {
1110
int res = 0;
1211
for (;;) {
@@ -31,5 +30,4 @@ int main() {
3130
}
3231
}
3332

34-
// CHECK: KLEE: done: completed paths = 0
35-
// CHECK: KLEE: done: generated tests = 5
33+
// CHECK-NOT: KLEE: done: generated tests = 0

0 commit comments

Comments
 (0)