From 2af34dc2f0a9e282c29ba28c774c8218b0c5ddd2 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sat, 16 Sep 2023 13:24:32 +0400 Subject: [PATCH] [feat] Add `cover-on-the-fly` option --- include/klee/Core/TerminationTypes.h | 3 +- lib/Core/Executor.cpp | 59 +++++++++++++++++++--------- test/Feature/CoverOnTheFly.c | 33 ++++++++++++++++ test/Feature/CoverageCheck.c | 2 +- 4 files changed, 76 insertions(+), 21 deletions(-) create mode 100644 test/Feature/CoverOnTheFly.c diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 06d1522923c..786cf610d6e 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -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") \ diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 761f832c479..65a6dcdedbb 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -239,6 +239,18 @@ cl::opt EmitAllErrors( "(default=false, i.e. one per (error,instruction) pair)"), cl::cat(TestGenCat)); +cl::opt 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 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 MaxSymArraySize( @@ -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); @@ -4511,25 +4551,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; diff --git a/test/Feature/CoverOnTheFly.c b/test/Feature/CoverOnTheFly.c new file mode 100644 index 00000000000..48a21b31f63 --- /dev/null +++ b/test/Feature/CoverOnTheFly.c @@ -0,0 +1,33 @@ +// 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 \ No newline at end of file diff --git a/test/Feature/CoverageCheck.c b/test/Feature/CoverageCheck.c index 48000103506..a9c9eb2b630 100644 --- a/test/Feature/CoverageCheck.c +++ b/test/Feature/CoverageCheck.c @@ -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)