Skip to content

Commit

Permalink
[feat] Add cover-on-the-fly option
Browse files Browse the repository at this point in the history
  • Loading branch information
misonijnik committed Sep 18, 2023
1 parent 4486529 commit d3344b5
Show file tree
Hide file tree
Showing 4 changed files with 78 additions and 21 deletions.
3 changes: 2 additions & 1 deletion include/klee/Core/TerminationTypes.h
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,8 @@ enum class StateTerminationClass : std::uint8_t {
TTYPE(OutOfMemory, 12U, "early") \
TTYPE(OutOfStackMemory, 13U, "early") \
TTYPE(MaxCycles, 14U, "early") \
TTMARK(EARLY, 14U) \
TTYPE(CoverOnTheFly, 15U, "early") \
TTMARK(EARLY, 15U) \
TTYPE(Solver, 20U, "solver.err") \
TTMARK(SOLVERERR, 20U) \
TTYPE(Abort, 30U, "abort.err") \
Expand Down
59 changes: 40 additions & 19 deletions lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -239,6 +239,18 @@ cl::opt<bool> EmitAllErrors(
"(default=false, i.e. one per (error,instruction) pair)"),
cl::cat(TestGenCat));

cl::opt<bool> CoverOnTheFly(
"cover-on-the-fly", cl::init(false),
cl::desc("Generate tests cases for each new covered block or branch "
"(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::cat(TestGenCat));

/* Constraint solving options */

cl::opt<unsigned> MaxSymArraySize(
Expand Down Expand Up @@ -4325,8 +4337,36 @@ void Executor::initializeTypeManager() {
typeSystemManager->initModule();
}

static bool shouldWriteTest(const ExecutionState &state) {
bool coveredNew = state.coveredNew->value;
state.coveredNew->value = false;
return !OnlyOutputStatesCoveringNew || coveredNew;
}

static std::string terminationTypeFileExtension(StateTerminationType type) {
std::string ret;
#undef TTYPE
#undef TTMARK
#define TTYPE(N, I, S) \
case StateTerminationType::N: \
ret = (S); \
break;
#define TTMARK(N, I)
switch (type) { TERMINATION_TYPES }
return ret;
};

void Executor::executeStep(ExecutionState &state) {
KInstruction *prevKI = state.prevPC;

if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance &&
stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) {
interpreterHandler->processTestCase(
state, nullptr,
terminationTypeFileExtension(StateTerminationType::CoverOnTheFly)
.c_str());
}

if (targetManager->isTargeted(state) && state.targets().empty()) {
terminateStateEarlyAlgorithm(state, "State missed all it's targets.",
StateTerminationType::MissedAllTargets);
Expand Down Expand Up @@ -4512,25 +4552,6 @@ void Executor::terminateState(ExecutionState &state,
removedStates.push_back(&state);
}

static bool shouldWriteTest(const ExecutionState &state) {
bool coveredNew = state.coveredNew->value;
state.coveredNew->value = false;
return !OnlyOutputStatesCoveringNew || coveredNew;
}

static std::string terminationTypeFileExtension(StateTerminationType type) {
std::string ret;
#undef TTYPE
#undef TTMARK
#define TTYPE(N, I, S) \
case StateTerminationType::N: \
ret = (S); \
break;
#define TTMARK(N, I)
switch (type) { TERMINATION_TYPES }
return ret;
};

void Executor::terminateStateOnExit(ExecutionState &state) {
auto terminationType = StateTerminationType::Exit;
++stats::terminationExit;
Expand Down
35 changes: 35 additions & 0 deletions test/Feature/CoverOnTheFly.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
// ASAN fails because KLEE does not cleanup states with -dump-states-on-halt=false
// 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

#include "klee/klee.h"

#define a (2)
int main() {
int res = 0;
for (;;) {
int n = klee_int("n");
switch (n) {
case 1:
res += 1;
break;
case 2:
res += 2;
break;
case 3:
res += 3;
break;
case 4:
res += 4;
break;

default:
break;
}
}
}

// CHECK: KLEE: done: completed paths = 0
// CHECK: KLEE: done: generated tests = 5
2 changes: 1 addition & 1 deletion test/Feature/CoverageCheck.c
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --use-cov-check=instruction-based --output-dir=%t.klee-out %t.bc > %t.log
// RUN: %klee --use-guided-search=none --use-cov-check=instruction-based --output-dir=%t.klee-out %t.bc > %t.log
#include "klee/klee.h"

#define a (2)
Expand Down

0 comments on commit d3344b5

Please sign in to comment.