diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 05142dd2c4..e1b4cde6f8 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -120,9 +120,8 @@ ExecutionState::ExecutionState() : initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1), depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), - roundingMode(llvm::APFloat::rmNearestTiesToEven), - coveredNew(new box(false)), forkDisabled(false), - prevHistory_(TargetsHistory::create()), + roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}), + forkDisabled(false), prevHistory_(TargetsHistory::create()), history_(TargetsHistory::create()) { setID(); } @@ -131,9 +130,8 @@ ExecutionState::ExecutionState(KFunction *kf) : initPC(kf->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1), depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), - roundingMode(llvm::APFloat::rmNearestTiesToEven), - coveredNew(new box(false)), forkDisabled(false), - prevHistory_(TargetsHistory::create()), + roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}), + forkDisabled(false), prevHistory_(TargetsHistory::create()), history_(TargetsHistory::create()) { pushFrame(nullptr, kf); setID(); @@ -143,9 +141,8 @@ ExecutionState::ExecutionState(KFunction *kf, KBlock *kb) : initPC(kb->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1), depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), - roundingMode(llvm::APFloat::rmNearestTiesToEven), - coveredNew(new box(false)), forkDisabled(false), - prevHistory_(TargetsHistory::create()), + roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}), + forkDisabled(false), prevHistory_(TargetsHistory::create()), history_(TargetsHistory::create()) { pushFrame(nullptr, kf); setID(); diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index a0aa46619a..f8cc093489 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -36,6 +36,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" DISABLE_WARNING_POP +#include #include #include #include @@ -364,7 +365,7 @@ class ExecutionState { std::uint32_t id = 0; /// @brief Whether a new instruction was covered in this state - mutable ref> coveredNew; + mutable std::deque>> coveredNew; /// @brief Disables forking for this state. Set by user code bool forkDisabled = false; @@ -502,6 +503,22 @@ class ExecutionState { } return false; } + + bool isCoveredNew() const { + return !coveredNew.empty() && coveredNew.back()->value; + } + void coverNew() const { coveredNew.push_back(new box(true)); } + void updateCoveredNew() const { + while (!coveredNew.empty() && !coveredNew.front()->value) { + coveredNew.pop_front(); + } + } + void clearCoveredNew() const { + for (auto signal : coveredNew) { + signal->value = false; + } + coveredNew.clear(); + } }; struct ExecutionStateIDCompare { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c58e1a51ac..e3c8cce344 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3953,6 +3953,10 @@ void Executor::updateStates(ExecutionState *current) { targetedExecutionManager->update(current, addedStates, removedStates); } + if (targetCalculator) { + targetCalculator->update(current, addedStates, removedStates); + } + if (searcher) { searcher->update(current, addedStates, removedStates); } @@ -4084,7 +4088,7 @@ bool Executor::checkMemoryUsage() { unsigned idx = theRNG.getInt32() % N; // Make two pulls to try and not hit a state that // covered new code. - if (arr[idx]->coveredNew->value) + if (arr[idx]->isCoveredNew()) idx = theRNG.getInt32() % N; std::swap(arr[idx], arr[N - 1]); @@ -4294,11 +4298,6 @@ void Executor::run(std::vector initialStates) { KInstruction *prevKI = state.prevPC; KFunction *kf = prevKI->parent->parent; - if (prevKI->inst->isTerminator() && - kmodule->inMainModule(*kf->function)) { - targetCalculator->update(state); - } - executeStep(state); } @@ -4357,8 +4356,8 @@ void Executor::initializeTypeManager() { } static bool shouldWriteTest(const ExecutionState &state) { - bool coveredNew = state.coveredNew->value; - state.coveredNew->value = false; + state.updateCoveredNew(); + bool coveredNew = state.isCoveredNew(); return !OnlyOutputStatesCoveringNew || coveredNew; } @@ -4380,6 +4379,7 @@ void Executor::executeStep(ExecutionState &state) { if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance && stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) { + state.clearCoveredNew(); interpreterHandler->processTestCase( state, nullptr, terminationTypeFileExtension(StateTerminationType::CoverOnTheFly) @@ -4565,7 +4565,6 @@ void Executor::terminateState(ExecutionState &state, interpreterHandler->incPathsExplored(); state.pc = state.prevPC; - targetCalculator->update(state); solver->notifyStateTermination(state.id); removedStates.push_back(&state); @@ -4574,9 +4573,11 @@ void Executor::terminateState(ExecutionState &state, void Executor::terminateStateOnExit(ExecutionState &state) { auto terminationType = StateTerminationType::Exit; ++stats::terminationExit; - if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state))) + if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state))) { + state.clearCoveredNew(); interpreterHandler->processTestCase( state, nullptr, terminationTypeFileExtension(terminationType).c_str()); + } interpreterHandler->incPathsCompleted(); terminateState(state, terminationType); @@ -4593,6 +4594,7 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, reason == StateTerminationType::MissedAllTargets) && shouldWriteTest(state)) || (AlwaysOutputSeeds && seedMap.count(&state))) { + state.clearCoveredNew(); interpreterHandler->processTestCase( state, (message + "\n").str().c_str(), terminationTypeFileExtension(reason).c_str(), @@ -4717,8 +4719,9 @@ void Executor::terminateStateOnError(ExecutionState &state, const KInstruction *ki = getLastNonKleeInternalInstruction(state); Instruction *lastInst = ki->inst; - if (EmitAllErrors || - emittedErrors.insert(std::make_pair(lastInst, message)).second) { + if ((EmitAllErrors || + emittedErrors.insert(std::make_pair(lastInst, message)).second) && + shouldWriteTest(state)) { std::string filepath = ki->getSourceFilepath(); if (!filepath.empty()) { klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(), @@ -7375,7 +7378,7 @@ void Executor::dumpStates() { *os << "{"; *os << "'depth' : " << es->depth << ", "; *os << "'queryCost' : " << es->queryMetaData.queryCost << ", "; - *os << "'coveredNew' : " << es->coveredNew->value << ", "; + *os << "'coveredNew' : " << es->isCoveredNew() << ", "; *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", "; *os << "'md2u' : " << md2u << ", "; *os << "'icnt' : " << icnt << ", "; diff --git a/lib/Core/TargetCalculator.cpp b/lib/Core/TargetCalculator.cpp index 0c5d72fedb..e6a8f8834c 100644 --- a/lib/Core/TargetCalculator.cpp +++ b/lib/Core/TargetCalculator.cpp @@ -51,8 +51,7 @@ void TargetCalculator::update(const ExecutionState &state) { unsigned index = 0; if (!coveredBranches[state.prevPC->parent->parent].count( state.prevPC->parent)) { - state.coveredNew->value = false; - state.coveredNew = new box(true); + state.coverNew(); coveredBranches[state.prevPC->parent->parent][state.prevPC->parent]; } for (auto succ : successors(state.getPrevPCBlock())) { @@ -60,8 +59,7 @@ void TargetCalculator::update(const ExecutionState &state) { if (!coveredBranches[state.prevPC->parent->parent] [state.prevPC->parent] .count(index)) { - state.coveredNew->value = false; - state.coveredNew = new box(true); + state.coverNew(); coveredBranches[state.prevPC->parent->parent][state.prevPC->parent] .insert(index); } @@ -129,6 +127,30 @@ void TargetCalculator::update(const ExecutionState &state) { } } +void TargetCalculator::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { + if (current && (std::find(removedStates.begin(), removedStates.end(), + current) == removedStates.end())) { + localStates.insert(current); + } + for (const auto state : addedStates) { + localStates.insert(state); + } + for (const auto state : removedStates) { + localStates.insert(state); + } + for (auto state : localStates) { + KFunction *kf = state->prevPC->parent->parent; + KModule *km = kf->parent; + if (state->prevPC->inst->isTerminator() && + km->inMainModule(*kf->function)) { + update(*state); + } + } + localStates.clear(); +} + bool TargetCalculator::differenceIsEmpty( const ExecutionState &state, const std::unordered_map &history, diff --git a/lib/Core/TargetCalculator.h b/lib/Core/TargetCalculator.h index ba78a89f20..75bd8413d8 100644 --- a/lib/Core/TargetCalculator.h +++ b/lib/Core/TargetCalculator.h @@ -42,6 +42,8 @@ typedef std::pair Transition; typedef std::pair Branch; class TargetCalculator { + using StatesSet = std::unordered_set; + typedef std::unordered_set VisitedBlocks; typedef std::unordered_set VisitedTransitions; typedef std::unordered_set VisitedBranches; @@ -63,12 +65,15 @@ class TargetCalculator { typedef std::unordered_set CoveredFunctionsBranches; typedef std::unordered_map CoveredBlocks; + void update(const ExecutionState &state); public: TargetCalculator(CodeGraphInfo &codeGraphInfo) : codeGraphInfo(codeGraphInfo) {} - void update(const ExecutionState &state); + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates); TargetHashSet calculate(ExecutionState &state); @@ -80,6 +85,7 @@ class TargetCalculator { CoveredFunctionsBranches coveredFunctionsInBranches; CoveredFunctionsBranches fullyCoveredFunctions; CoveredBlocks coveredBlocks; + StatesSet localStates; bool differenceIsEmpty( const ExecutionState &state, diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index dd97353391..cda430bd96 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -75,6 +75,10 @@ static cl::opt static cl::alias A1("S", cl::desc("Alias for --strip-debug"), cl::aliasopt(StripDebug)); +static cl::opt DeleteDeadLoops("delete-dead-loops", + cl::desc("Use LoopDeletionPass"), + cl::init(true), cl::cat(klee::ModuleCat)); + // A utility function that adds a pass to the pass manager but will also add // a verifier pass after if we're supposed to verify. static inline void addPass(legacy::PassManager &PM, Pass *P) { @@ -131,8 +135,9 @@ static void AddStandardCompilePasses(legacy::PassManager &PM) { addPass(PM, createLoopUnswitchPass()); // Unswitch loops. // FIXME : Removing instcombine causes nestedloop regression. addPass(PM, createInstructionCombiningPass()); - addPass(PM, createIndVarSimplifyPass()); // Canonicalize indvars - addPass(PM, createLoopDeletionPass()); // Delete dead loops + addPass(PM, createIndVarSimplifyPass()); // Canonicalize indvars + if (DeleteDeadLoops) + addPass(PM, createLoopDeletionPass()); // Delete dead loops addPass(PM, createLoopUnrollPass()); // Unroll small loops addPass(PM, createInstructionCombiningPass()); // Clean up after the unroller addPass(PM, createGVNPass()); // Remove redundancies diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 0bf904a60a..75dbe1dfec 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -187,30 +187,36 @@ bool CachingSolver::computeValidity(const Query &query, return true; case PValidity::MayBeTrue: { ++stats::queryCacheMisses; - if (!solver->impl->computeTruth(query, tmp)) - return false; - if (tmp) { + bool success = solver->impl->computeTruth(query, tmp); + if (success && tmp) { cacheInsert(query, PValidity::MustBeTrue); result = PValidity::MustBeTrue; return true; - } else { + } else if (success && !tmp) { cacheInsert(query, PValidity::TrueOrFalse); result = PValidity::TrueOrFalse; return true; + } else { + cacheInsert(query, PValidity::MayBeTrue); + result = PValidity::MayBeTrue; + return true; } } case PValidity::MayBeFalse: { ++stats::queryCacheMisses; - if (!solver->impl->computeTruth(query.negateExpr(), tmp)) - return false; - if (tmp) { + bool success = solver->impl->computeTruth(query.negateExpr(), tmp); + if (success && tmp) { cacheInsert(query, PValidity::MustBeFalse); result = PValidity::MustBeFalse; return true; - } else { + } else if (success && !tmp) { cacheInsert(query, PValidity::TrueOrFalse); result = PValidity::TrueOrFalse; return true; + } else { + cacheInsert(query, PValidity::MayBeFalse); + result = PValidity::MayBeFalse; + return true; } } default: @@ -267,50 +273,8 @@ bool CachingSolver::computeTruth(const Query &query, bool &isValid) { bool CachingSolver::computeValidityCore(const Query &query, ValidityCore &validityCore, bool &isValid) { - PartialValidity cachedResult; - bool tmp, cacheHit = cacheLookup(query, cachedResult); - - // a cached result of MayBeTrue forces us to check whether - // a False assignment exists. - if (cacheHit && cachedResult != PValidity::MayBeTrue) { - ValidityCore cachedValidityCore; - cacheHit = validityCoreCacheLookup(query, cachedValidityCore); - if (cacheHit && cachedResult == PValidity::MustBeTrue) { - ++stats::queryCacheHits; - validityCore = cachedValidityCore; - } else if (cachedResult == PValidity::MustBeTrue) { - ++stats::queryCacheMisses; - if (!solver->impl->computeValidityCore(query, validityCore, tmp)) - return false; - assert(tmp && "Query must be true!"); - validityCoreCacheInsert(query, validityCore); - } else { - ++stats::queryCacheHits; - } - isValid = (cachedResult == PValidity::MustBeTrue); - return true; - } - ++stats::queryCacheMisses; - - // cache miss: query solver - if (!solver->impl->computeValidityCore(query, validityCore, isValid)) - return false; - - if (isValid) { - cachedResult = PValidity::MustBeTrue; - validityCoreCacheInsert(query, validityCore); - } else if (cacheHit) { - // We know a true assignment exists, and query isn't valid, so - // must be TrueOrFalse. - assert(cachedResult == PValidity::MayBeTrue); - cachedResult = PValidity::TrueOrFalse; - } else { - cachedResult = PValidity::MayBeFalse; - } - - cacheInsert(query, cachedResult); - return true; + return solver->impl->computeValidityCore(query, validityCore, isValid); } bool CachingSolver::computeInitialValues( @@ -322,50 +286,8 @@ bool CachingSolver::computeInitialValues( } bool CachingSolver::check(const Query &query, ref &result) { - PartialValidity cachedResult; - bool tmp, cacheHit = cacheLookup(query, cachedResult); - - // a cached result of MayBeTrue forces us to check whether - // a False assignment exists. - if (cacheHit && cachedResult != PValidity::MayBeTrue) { - ValidityCore cachedValidityCore; - cacheHit = validityCoreCacheLookup(query, cachedValidityCore); - if (cacheHit && cachedResult == PValidity::MustBeTrue) { - ++stats::queryCacheHits; - result = new ValidResponse(cachedValidityCore); - } else if (cachedResult == PValidity::MustBeTrue) { - ++stats::queryCacheMisses; - if (!solver->impl->computeValidityCore(query, cachedValidityCore, tmp)) - return false; - result = new ValidResponse(cachedValidityCore); - assert(tmp && "Query must be true!"); - } else { - ++stats::queryCacheMisses; - if (!solver->impl->check(query, result)) - return false; - } - return true; - } - ++stats::queryCacheMisses; - - // cache miss: query solver - if (!solver->impl->check(query, result)) - return false; - - if (isa(result)) { - cachedResult = PValidity::MustBeTrue; - } else if (cacheHit) { - // We know a true assignment exists, and query isn't valid, so - // must be TrueOrFalse. - assert(cachedResult == PValidity::MayBeTrue); - cachedResult = PValidity::TrueOrFalse; - } else { - cachedResult = PValidity::MayBeFalse; - } - - cacheInsert(query, cachedResult); - return true; + return solver->impl->check(query, result); } SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() { diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 92a209e4f9..98a9f58149 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -180,13 +180,25 @@ bool CexCachingSolver::searchForResponse(KeyType &key, return true; } + KeyType booleanKey; + KeyType nonBooleanKey; + for (auto i : key) { + if (i->getWidth() == Expr::Bool) { + booleanKey.insert(i); + } else { + nonBooleanKey.insert(i); + } + } + // Otherwise, iterate through the set of current solver responses to see if // one of them satisfies the query. for (responseTable_ty::iterator it = responseTable.begin(), ie = responseTable.end(); it != ie; ++it) { ref a = *it; - if (isa(a) && cast(a)->satisfies(key)) { + if (isa(a) && + cast(a)->satisfies(booleanKey) && + cast(a)->satisfiesNonBoolean(nonBooleanKey)) { result = a; return true; } @@ -270,12 +282,23 @@ bool CexCachingSolver::getResponse(const Query &query, result = *res.first; } - if (DebugCexCacheCheckBinding) - if (!cast(result)->satisfies(key)) { + if (DebugCexCacheCheckBinding) { + KeyType booleanKey; + KeyType nonBooleanKey; + for (auto i : key) { + if (i->getWidth() == Expr::Bool) { + booleanKey.insert(i); + } else { + nonBooleanKey.insert(i); + } + } + if (!cast(result)->satisfies(booleanKey) || + !cast(result)->satisfiesNonBoolean(nonBooleanKey)) { query.dump(); result->dump(); klee_error("Generated assignment doesn't match query"); } + } } ValidityCore resultCore; @@ -307,21 +330,19 @@ bool CexCachingSolver::computeValidity(const Query &query, return false; if (cast(q)->isTrue()) { - if (!getResponse(query, a)) - return false; - if (isa(a)) { + bool success = getResponse(query, a); + if (success && isa(a)) { result = PValidity::MustBeTrue; - } else if (isa(a)) { + } else if (success && isa(a)) { result = PValidity::TrueOrFalse; } else { result = PValidity::MayBeTrue; } } else { - if (!getResponse(query.negateExpr(), a)) - return false; - if (isa(a)) { + bool success = getResponse(query.negateExpr(), a); + if (success && isa(a)) { result = PValidity::MustBeFalse; - } else if (isa(a)) { + } else if (success && isa(a)) { result = PValidity::TrueOrFalse; } else { result = PValidity::MayBeFalse; diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp index 2768ce3ce9..e1d3ab3513 100644 --- a/lib/Solver/SolverImpl.cpp +++ b/lib/Solver/SolverImpl.cpp @@ -18,27 +18,41 @@ using namespace klee; SolverImpl::~SolverImpl() {} bool SolverImpl::computeValidity(const Query &query, PartialValidity &result) { + bool trueSuccess, falseSuccess; bool isTrue, isFalse; - if (!computeTruth(query, isTrue)) - return false; - if (isTrue) { + trueSuccess = computeTruth(query, isTrue); + if (trueSuccess && isTrue) { result = PValidity::MustBeTrue; } else { - if (!computeTruth(query.negateExpr(), isFalse)) - return false; - result = isFalse ? PValidity::MustBeFalse : PValidity::TrueOrFalse; + falseSuccess = computeTruth(query.negateExpr(), isFalse); + if (falseSuccess && isFalse) { + result = PValidity::MustBeFalse; + } else { + if (trueSuccess && falseSuccess) { + result = PValidity::TrueOrFalse; + } else if (!trueSuccess) { + result = PValidity::MayBeTrue; + } else if (!falseSuccess) { + result = PValidity::MayBeFalse; + } else { + result = PValidity::None; + } + } } - return true; + return result != PValidity::None; } bool SolverImpl::computeValidity(const Query &query, ref &queryResult, ref &negatedQueryResult) { - if (!check(query, queryResult)) - return false; - if (!check(query.negateExpr(), negatedQueryResult)) - return false; - return true; + if (!check(query, queryResult)) { + queryResult = new UnknownResponse(); + } + if (!check(query.negateExpr(), negatedQueryResult)) { + negatedQueryResult = new UnknownResponse(); + } + return !isa(queryResult) || + !isa(negatedQueryResult); } bool SolverImpl::check(const Query &query, ref &result) { diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c index af449cebd0..41049f5b34 100644 --- a/test/Feature/SolverTimeout.c +++ b/test/Feature/SolverTimeout.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t.bc +// RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t.bc 2>&1 | FileCheck %s // // Note: This test occasionally fails when using Z3 4.4.1 @@ -11,6 +11,8 @@ int main() { klee_make_symbolic(&x, sizeof(x), "x"); + // CHECK-NOT: Yes + // CHECK: No if (x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x + (x * x % (x + 12)) == y * y * y * y * y * y * y * y * y * y * y * y * y * y * y * y % i) printf("Yes\n"); else diff --git a/test/InteractiveMode/interactive_mode.c b/test/InteractiveMode/interactive_mode.c index 1adb5e01f2..8ae3cb75c1 100644 --- a/test/InteractiveMode/interactive_mode.c +++ b/test/InteractiveMode/interactive_mode.c @@ -1,4 +1,5 @@ -// REQUIRES: not-ubsan +/* The test is flaky and the feature isn't importatnt now */ +// REQUIRES: not-ubsan, not-darwin // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out %t.entrypoints // RUN: echo sign_sum >> %t.entrypoints diff --git a/test/Solver/CexCacheCheckBinding.c b/test/Solver/CexCacheCheckBinding.c new file mode 100644 index 0000000000..4743ef1027 --- /dev/null +++ b/test/Solver/CexCacheCheckBinding.c @@ -0,0 +1,8 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --debug-cex-cache-check-binding --search=bfs --use-guided-search=none --use-cex-cache=false %t1.bc 2>&1 | FileCheck %s + +#include "ExerciseSolver.c.inc" + +// CHECK: KLEE: done: completed paths = 18 +// CHECK: KLEE: done: partially completed paths = 0 diff --git a/test/Solver/DummySolver.c b/test/Solver/DummySolver.c index 9242396854..54d94b5b2c 100644 --- a/test/Solver/DummySolver.c +++ b/test/Solver/DummySolver.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=dummy --use-guided-search=none %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=dummy --use-guided-search=none --use-cex-cache=false %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" diff --git a/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c new file mode 100644 index 0000000000..9b27688a42 --- /dev/null +++ b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c @@ -0,0 +1,25 @@ +// REQUIRES: z3 +// RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --optimize=true --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s + +#include "klee-test-comp.c" + +extern int __VERIFIER_nondet_int(void); + +int main() { + int *x = alloca(sizeof(int)); + int *y = alloca(sizeof(int)); + int *z = alloca(sizeof(int)); + *x = __VERIFIER_nondet_int(); + *y = __VERIFIER_nondet_int(); + *z = __VERIFIER_nondet_int(); + + while (*x > 0) { + *x = *x + *y; + *y = *z; + *z = -(*z) - 1; + } +} + +// CHECK: generated tests = 3 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 364254f278..e9bb118371 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -593,6 +593,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, klee_warning("unable to get symbolic solution, losing test case"); const auto start_time = time::getWallTime(); + bool atLeastOneGenerated = false; if (WriteKTests) { @@ -602,7 +603,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, getOutputFilename(getTestFilename("ktest", id)).c_str())) { klee_warning("unable to write output test case, losing it"); } else { - ++m_numGeneratedTests; + atLeastOneGenerated = true; } if (WriteStates) { @@ -691,6 +692,10 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (WriteXMLTests) { writeTestCaseXML(message != nullptr, ktest, id); + atLeastOneGenerated = true; + } + + if (atLeastOneGenerated) { ++m_numGeneratedTests; }