Skip to content

Commit

Permalink
[feat] Cover on the fly based on time
Browse files Browse the repository at this point in the history
  • Loading branch information
Columpio committed Oct 24, 2023
1 parent 3a69ec3 commit 89b5568
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 12 deletions.
24 changes: 16 additions & 8 deletions lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -249,10 +249,10 @@ cl::opt<bool> CoverOnTheFly(
"(default=false, i.e. one per (error,instruction) pair)"),
cl::cat(TestGenCat));

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

cl::opt<unsigned> UninitMemoryTestMultiplier(
Expand Down Expand Up @@ -487,15 +487,23 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
targetedExecutionManager(
new TargetedExecutionManager(*codeGraphInfo, *targetManager)),
replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false),
inhibitForking(false), haltExecution(HaltExecution::NotHalt),
ivcEnabled(false), debugLogBuffer(debugBufferString) {
inhibitForking(false), coverOnTheFly(false),
haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
debugLogBuffer(debugBufferString) {
const time::Span maxTime{MaxTime};
if (maxTime)
timers.add(std::make_unique<Timer>(maxTime, [&] {
klee_message("HaltTimer invoked");
setHaltExecution(HaltExecution::MaxTime);
}));

if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance) {
const time::Span delayTime{DelayCoverOnTheFly};
if (delayTime)
timers.add(
std::make_unique<Timer>(delayTime, [&] { coverOnTheFly = true; }));
}

coreSolverTimeout = time::Span{MaxCoreSolverTime};
if (coreSolverTimeout)
UseForkedCoreSolver = true;
Expand Down Expand Up @@ -4381,8 +4389,8 @@ static std::string terminationTypeFileExtension(StateTerminationType type) {

void Executor::executeStep(ExecutionState &state) {
KFunction *initKF = state.initPC->parent->parent;
if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance &&
stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) {

if (coverOnTheFly && shouldWriteTest(state)) {
state.clearCoveredNew();
interpreterHandler->processTestCase(
state, nullptr,
Expand Down
3 changes: 3 additions & 0 deletions lib/Core/Executor.h
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,9 @@ class Executor : public Interpreter {
/// Disables forking, set by client. \see setInhibitForking()
bool inhibitForking;

/// Should it generate test cases for each new covered block or branch
bool coverOnTheFly;

/// Signals the executor to halt execution at the next instruction
/// step.
HaltExecution::Reason haltExecution = HaltExecution::NotHalt;
Expand Down
6 changes: 2 additions & 4 deletions test/Feature/CoverOnTheFly.c
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,10 @@
// REQUIRES: not-asan
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// 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
// 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

#include "klee/klee.h"

#define a (2)
int main() {
int res = 0;
for (;;) {
Expand All @@ -31,5 +30,4 @@ int main() {
}
}

// CHECK: KLEE: done: completed paths = 0
// CHECK: KLEE: done: generated tests = 5
// CHECK-NOT: KLEE: done: generated tests = 0

0 comments on commit 89b5568

Please sign in to comment.