diff --git a/build.sh b/build.sh index 71df1df169..24f537596b 100755 --- a/build.sh +++ b/build.sh @@ -31,7 +31,7 @@ LLVM_VERSION=14 ENABLE_OPTIMIZED=1 ENABLE_DEBUG=0 DISABLE_ASSERTIONS=1 -REQUIRES_RTTI=0 +REQUIRES_RTTI=1 ## Solvers Required options # SOLVERS=STP diff --git a/include/klee/ADT/DisjointSetUnion.h b/include/klee/ADT/DisjointSetUnion.h index 41c1a0296b..9a3673af64 100644 --- a/include/klee/ADT/DisjointSetUnion.h +++ b/include/klee/ADT/DisjointSetUnion.h @@ -21,7 +21,7 @@ DISABLE_WARNING_POP #include namespace klee { -using ExprEitherSymcrete = either; +using ExprOrSymcrete = either; template , diff --git a/include/klee/ADT/Either.h b/include/klee/ADT/Either.h index 81b2d8e51c..c941d33103 100644 --- a/include/klee/ADT/Either.h +++ b/include/klee/ADT/Either.h @@ -46,7 +46,6 @@ template class either { virtual EitherKind getKind() const = 0; static bool classof(const either *) { return true; } - // virtual unsigned hash() = 0; virtual int compare(const either &b) = 0; virtual bool equals(const either &b) = 0; @@ -83,7 +82,6 @@ template class either_left : public either { } static bool classof(const either_left *) { return true; } - // virtual unsigned hash() override { return value_->hash(); }; virtual int compare(const either &b) override { if (b.getKind() != getKind()) { return b.getKind() < getKind() ? -1 : 1; @@ -134,7 +132,6 @@ template class either_right : public either { } static bool classof(const either_right *) { return true; } - // virtual unsigned hash() override { return value_->hash(); }; virtual int compare(const either &b) override { if (b.getKind() != getKind()) { return b.getKind() < getKind() ? -1 : 1; diff --git a/include/klee/ADT/SparseStorage.h b/include/klee/ADT/SparseStorage.h index a06f63391f..a78df85770 100644 --- a/include/klee/ADT/SparseStorage.h +++ b/include/klee/ADT/SparseStorage.h @@ -75,7 +75,7 @@ class SparseStorage { for (auto i : internalStorage) { sizeOfRange = std::max(i.first, sizeOfRange); } - return sizeOfRange; + return internalStorage.empty() ? 0 : sizeOfRange + 1; } bool operator==(const SparseStorage &another) const { diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 766380b486..43280ff28f 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -177,6 +177,8 @@ class Interpreter { virtual void setHaltExecution(HaltExecution::Reason value) = 0; + virtual HaltExecution::Reason getHaltExecution() = 0; + virtual void setInhibitForking(bool value) = 0; virtual void prepareForEarlyExit() = 0; diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 786cf610d6..a08b3585e7 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -97,6 +97,7 @@ enum Reason { CovCheck, NoMoreStates, ReachedTarget, + UnreachedTarget, ErrorOnWhichShouldExit, Interrupt, MaxDepth, diff --git a/include/klee/Expr/AlphaBuilder.h b/include/klee/Expr/AlphaBuilder.h index 7012411908..6a965c3962 100644 --- a/include/klee/Expr/AlphaBuilder.h +++ b/include/klee/Expr/AlphaBuilder.h @@ -25,6 +25,7 @@ class AlphaBuilder final : public ExprVisitor { private: ArrayCache &arrayCache; unsigned index = 0; + bool reverse = false; const Array *visitArray(const Array *arr); UpdateList visitUpdateList(UpdateList u); @@ -36,6 +37,7 @@ class AlphaBuilder final : public ExprVisitor { constraints_ty visitConstraints(constraints_ty cs); ref build(ref v); const Array *buildArray(const Array *arr) { return visitArray(arr); } + ref reverseBuild(ref v); }; } // namespace klee diff --git a/include/klee/Expr/IndependentConstraintSetUnion.h b/include/klee/Expr/IndependentConstraintSetUnion.h index 783dadc256..c4ce9a4559 100644 --- a/include/klee/Expr/IndependentConstraintSetUnion.h +++ b/include/klee/Expr/IndependentConstraintSetUnion.h @@ -8,11 +8,11 @@ namespace klee { class IndependentConstraintSetUnion - : public DisjointSetUnion, IndependentConstraintSet, - ExprEitherSymcreteHash, ExprEitherSymcreteCmp> { + : public DisjointSetUnion, IndependentConstraintSet, + ExprOrSymcreteHash, ExprOrSymcreteCmp> { public: Assignment concretization; - std::vector> constraintQueue; + std::vector> constraintQueue; Assignment updateQueue; Assignment removeQueue; diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index c1c69f2f72..cbcf9ec752 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -22,17 +22,15 @@ DISABLE_WARNING_POP #include namespace klee { -using ExprEitherSymcrete = either; +using ExprOrSymcrete = either; -struct ExprEitherSymcreteHash { - unsigned operator()(const ref &e) const { - return e->hash(); - } +struct ExprOrSymcreteHash { + unsigned operator()(const ref &e) const { return e->hash(); } }; -struct ExprEitherSymcreteCmp { - bool operator()(const ref &a, - const ref &b) const { +struct ExprOrSymcreteCmp { + bool operator()(const ref &a, + const ref &b) const { return a == b; } }; @@ -100,8 +98,8 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, class IndependentConstraintSet { private: using InnerSetUnion = - DisjointSetUnion, IndependentConstraintSet, - ExprEitherSymcreteHash, ExprEitherSymcreteCmp>; + DisjointSetUnion, IndependentConstraintSet, + ExprOrSymcreteHash, ExprOrSymcreteCmp>; void initIndependentConstraintSet(ref e); void initIndependentConstraintSet(ref s); @@ -137,7 +135,7 @@ class IndependentConstraintSet { Assignment &assign) const; IndependentConstraintSet(); - explicit IndependentConstraintSet(ref v); + explicit IndependentConstraintSet(ref v); IndependentConstraintSet(const IndependentConstraintSet &ics); void print(llvm::raw_ostream &os) const; diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h index 83cef2cce5..dfd00c101f 100644 --- a/include/klee/Module/KModule.h +++ b/include/klee/Module/KModule.h @@ -197,6 +197,12 @@ struct KBlockCompare { } }; +struct KFunctionCompare { + bool operator()(const KFunction *a, const KFunction *b) const { + return a->id < b->id; + } +}; + class KConstant { public: /// Actual LLVM constant this represents. diff --git a/lib/ADT/SparseStorage.cpp b/lib/ADT/SparseStorage.cpp index dc24e7d993..1cfe3319b4 100644 --- a/lib/ADT/SparseStorage.cpp +++ b/lib/ADT/SparseStorage.cpp @@ -18,7 +18,7 @@ void SparseStorage::print(llvm::raw_ostream &os, if (firstPrinted) { os << ", "; } - os << element.first << ": " << element.second; + os << element.first << ": " << llvm::utostr(element.second); firstPrinted = true; } os << "} default: "; @@ -35,7 +35,7 @@ void SparseStorage::print(llvm::raw_ostream &os, } os << "] default: "; } - os << defaultValue; + os << llvm::utostr(defaultValue); } template <> diff --git a/lib/Core/AddressManager.cpp b/lib/Core/AddressManager.cpp index f763e0d3e0..b0219fb9ea 100644 --- a/lib/Core/AddressManager.cpp +++ b/lib/Core/AddressManager.cpp @@ -25,9 +25,15 @@ void *AddressManager::allocate(ref address, uint64_t size) { } } else { if (sizeLocation == objects.end() || !sizeLocation->second) { - uint64_t newSize = (uint64_t)1 - << (sizeof(size) * CHAR_BIT - - __builtin_clzll(std::max((uint64_t)1, size))); + uint64_t newSize = std::max((uint64_t)1, size); + int clz = __builtin_clzll(std::max((uint64_t)1, newSize)); + int popcount = __builtin_popcountll(std::max((uint64_t)1, newSize)); + if (popcount > 1) { + newSize = (uint64_t)1 << (sizeof(newSize) * CHAR_BIT - clz); + } + if (newSize > maxSize) { + newSize = std::max((uint64_t)1, size); + } assert(!objects.empty()); MemoryObject *mo = objects.begin()->second; newMO = memory->allocate(newSize, mo->isLocal, mo->isGlobal, diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 8227e81436..6c5d4f9128 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -75,6 +75,7 @@ void ExecutionStack::pushFrame(KInstIterator caller, KFunction *kf) { ++stackBalance; assert(valueStack_.size() == callStack_.size()); assert(valueStack_.size() == infoStack_.size()); + stackSize += kf->getNumRegisters(); } void ExecutionStack::popFrame() { @@ -94,6 +95,7 @@ void ExecutionStack::popFrame() { --stackBalance; assert(valueStack_.size() == callStack_.size()); assert(valueStack_.size() == infoStack_.size()); + stackSize -= kf->getNumRegisters(); } bool CallStackFrame::equals(const CallStackFrame &other) const { diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 9e74c4ef37..74ba2c67d4 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -37,6 +37,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" DISABLE_WARNING_POP +#include #include #include #include @@ -119,6 +120,7 @@ struct ExecutionStack { call_stack_ty callStack_; info_stack_ty infoStack_; call_stack_ty uniqueFrames_; + size_t stackSize = 0; unsigned stackBalance = 0; public: @@ -133,6 +135,7 @@ struct ExecutionStack { inline const call_stack_ty &uniqueFrames() const { return uniqueFrames_; } inline unsigned size() const { return callStack_.size(); } + inline size_t stackRegisterSize() const { return stackSize; } inline bool empty() const { return callStack_.empty(); } }; @@ -377,7 +380,7 @@ class ExecutionState { ExprHashMap, llvm::Type *>> gepExprBases; - ReachWithError error = ReachWithError::None; + mutable ReachWithError error = ReachWithError::None; std::atomic terminationReasonType{ HaltExecution::NotHalt}; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 48a2b4ae09..8fab82715d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -162,7 +162,7 @@ cl::opt AlignSymbolicPointers("align-symbolic-pointers", cl::desc("Makes symbolic pointers aligned according" "to the used type system (default=true)"), - cl::init(true), cl::cat(ExecCat)); + cl::init(false), cl::cat(ExecCat)); cl::opt ExternCallsCanReturnNull("extern-calls-can-return-null", cl::init(false), @@ -170,6 +170,17 @@ cl::opt "and return null (default=false)"), cl::cat(ExecCat)); +cl::opt OSCopySizeMemoryCheckThreshold( + "os-copy-size-mem-check-threshold", cl::init(10000), + cl::desc("Check memory usage when this amount of bytes dense OS is copied"), + cl::cat(ExecCat)); + +cl::opt StackCopySizeMemoryCheckThreshold( + "stack-copy-size-mem-check-threshold", cl::init(10000), + cl::desc("Check memory usage when state with stack this big (in bytes) is " + "copied"), + cl::cat(ExecCat)); + enum class MockMutableGlobalsPolicy { None, PrimitiveFields, @@ -227,17 +238,24 @@ llvm::cl::opt X86FPAsX87FP80( cl::desc("Convert X86 fp values to X87FP80 during computation according to " "GCC behavior (default=false)"), cl::cat(ExecCat)); + +cl::opt DumpStatesOnHalt( + "dump-states-on-halt", cl::init(HaltExecution::Reason::Unspecified), + cl::values( + clEnumValN(HaltExecution::Reason::NotHalt, "none", + "Do not dump test cases for all active states on exit."), + clEnumValN(HaltExecution::Reason::UnreachedTarget, "unreached", + "Dump test cases for all active states on exit if error not " + "reached."), + clEnumValN(HaltExecution::Reason::Unspecified, "all", + "Dump test cases for all active states on exit (default)")), + cl::cat(TestGenCat)); } // namespace klee namespace { /*** Test generation options ***/ -cl::opt DumpStatesOnHalt( - "dump-states-on-halt", cl::init(true), - cl::desc("Dump test cases for all active states on exit (default=true)"), - cl::cat(TestGenCat)); - cl::opt OnlyOutputStatesCoveringNew( "only-output-states-covering-new", cl::init(false), cl::desc("Only output test cases covering new code (default=false)"), @@ -609,6 +627,10 @@ llvm::Module *Executor::setModule( preservedFunctions.push_back("memcmp"); preservedFunctions.push_back("memmove"); + for (const auto &p : klee::floatReplacements) { + preservedFunctions.push_back(p.second.c_str()); + } + if (FunctionCallReproduce != "") { preservedFunctions.push_back(FunctionCallReproduce.c_str()); } @@ -663,6 +685,39 @@ Executor::~Executor() { /***/ +ref X87FP80ToFPTrunc(ref arg, Expr::Width type, + llvm::APFloat::roundingMode rm) { + ref result = arg; +#ifdef ENABLE_FP + Expr::Width resultType = type; + if (Context::get().getPointerWidth() == 32 && arg->getWidth() == Expr::Fl80) { + result = FPTruncExpr::create(arg, resultType, rm); + } +#else + klee_message( + "You may enable x86-as-x87FP80 behaviour by passing the following options" + " to cmake:\n" + "\"-DENABLE_FLOATING_POINT=ON\"\n"); +#endif + return result; +} + +ref FPToX87FP80Ext(ref arg) { + ref result = arg; +#ifdef ENABLE_FP + Expr::Width resultType = Expr::Fl80; + if (Context::get().getPointerWidth() == 32) { + result = FPExtExpr::create(arg, resultType); + } +#else + klee_message( + "You may enable x86-as-x87FP80 behaviour by passing the following options" + " to cmake:\n" + "\"-DENABLE_FLOATING_POINT=ON\"\n"); +#endif + return result; +} + void Executor::initializeGlobalObject(ExecutionState &state, ObjectState *os, const Constant *c, unsigned offset) { const auto targetData = kmodule->targetData.get(); @@ -698,6 +753,12 @@ void Executor::initializeGlobalObject(ExecutionState &state, ObjectState *os, unsigned StoreBits = targetData->getTypeStoreSizeInBits(c->getType()); ref C = evalConstant(c, state.roundingMode); + if (c->getType()->isFloatingPointTy() && + Context::get().getPointerWidth() == 32) { + C = X87FP80ToFPTrunc(C, getWidthForLLVMType(c->getType()), + state.roundingMode); + } + // Extend the constant if necessary; assert(StoreBits >= C->getWidth() && "Invalid store size!"); if (StoreBits > C->getWidth()) @@ -2463,40 +2524,6 @@ void Executor::checkNullCheckAfterDeref(ref cond, ExecutionState &state, } } -ref X87FP80ToFPTrunc(ref arg, Expr::Width type, - llvm::APFloat::roundingMode rm) { - ref result = arg; -#ifdef ENABLE_FP - Expr::Width resultType = type; - if (Context::get().getPointerWidth() == 32 && arg->getWidth() == Expr::Fl80) { - result = FPTruncExpr::create(arg, resultType, rm); - } -#else - klee_message( - "You may enable x86-as-x87FP80 behaviour by passing the following options" - " to cmake:\n" - "\"-DENABLE_FLOATING_POINT=ON\"\n"); -#endif - return result; -} - -ref FPToX87FP80Ext(ref arg) { - ref result = arg; -#ifdef ENABLE_FP - Expr::Width resultType = Expr::Fl80; - if (Context::get().getPointerWidth() == 32 && - arg->getWidth() == Expr::Int64) { - result = FPExtExpr::create(arg, resultType); - } -#else - klee_message( - "You may enable x86-as-x87FP80 behaviour by passing the following options" - " to cmake:\n" - "\"-DENABLE_FLOATING_POINT=ON\"\n"); -#endif - return result; -} - void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Instruction *i = ki->inst; @@ -2642,6 +2669,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Executor::StatePair branches = fork(state, cond, ifTrueBlock, ifFalseBlock, BranchType::Conditional); + if (branches.first && branches.second) { + maxNewStateStackSize = + std::max(maxNewStateStackSize, + branches.first->stack.stackRegisterSize() * 8); + } + // NOTE: There is a hidden dependency here, markBranchVisited // requires that we still be in the context of the branch // instruction (it reuses its statistic id). Should be cleaned @@ -3338,6 +3371,20 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { BitCastInst *bc = cast(ki->inst); llvm::Type *castToType = bc->getType(); + + if (X86FPAsX87FP80 && result->getWidth() == Expr::Fl80 && + !castToType->isFloatingPointTy() && + Context::get().getPointerWidth() == 32) { + result = X87FP80ToFPTrunc( + result, getWidthForLLVMType(bc->getOperand(0)->getType()), + state.roundingMode); + } + + if (X86FPAsX87FP80 && castToType->isFloatingPointTy() && + Context::get().getPointerWidth() == 32) { + result = FPToX87FP80Ext(result); + } + if (castToType->isPointerTy()) { castToType = castToType->getPointerElementType(); } @@ -3715,9 +3762,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref arg = eval(ki, 0, state).value; if (!fpWidthToSemantics(arg->getWidth()) || !fpWidthToSemantics(resultType)) return terminateStateOnExecError(state, "Unsupported FPTrunc operation"); - if (arg->getWidth() < resultType) - return terminateStateOnExecError(state, "Invalid FPTrunc"); - ref result = FPTruncExpr::create(arg, resultType, state.roundingMode); + ref result = arg; + if (arg->getWidth() > resultType) + result = FPTruncExpr::create(arg, resultType, state.roundingMode); + if (X86FPAsX87FP80 && Context::get().getPointerWidth() == 32) { + result = FPToX87FP80Ext(result); + } bindLocal(ki, state, result); break; } @@ -3728,9 +3778,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref arg = eval(ki, 0, state).value; if (!fpWidthToSemantics(arg->getWidth()) || !fpWidthToSemantics(resultType)) return terminateStateOnExecError(state, "Unsupported FPExt operation"); - if (arg->getWidth() > resultType) - return terminateStateOnExecError(state, "Invalid FPExt"); - ref result = FPExtExpr::create(arg, resultType); + ref result = arg; + if (arg->getWidth() < resultType) { + // return terminateStateOnExecError(state, "Invalid FPExt"); + result = FPExtExpr::create(arg, resultType); + } + if (X86FPAsX87FP80 && Context::get().getPointerWidth() == 32) { + result = FPToX87FP80Ext(result); + } bindLocal(ki, state, result); break; } @@ -4142,7 +4197,10 @@ bool Executor::checkMemoryUsage() { // We need to avoid calling GetTotalMallocUsage() often because it // is O(elts on freelist). This is really bad since we start // to pummel the freelist once we hit the memory cap. - if ((stats::instructions & 0xFFFFU) != 0) // every 65536 instructions + // every 65536 instructions + if ((stats::instructions & 0xFFFFU) != 0 && + maxNewWriteableOSSize < OSCopySizeMemoryCheckThreshold && + maxNewStateStackSize < StackCopySizeMemoryCheckThreshold) return true; // check memory limit @@ -4208,11 +4266,19 @@ void Executor::decreaseConfidenceFromStoppedStates( } void Executor::doDumpStates() { - if (!DumpStatesOnHalt || states.empty()) { + if (DumpStatesOnHalt == HaltExecution::Reason::NotHalt || + (DumpStatesOnHalt == HaltExecution::Reason::UnreachedTarget && + haltExecution == HaltExecution::Reason::ReachedTarget) || + states.empty()) { interpreterHandler->incPathsExplored(states.size()); return; } + if (FunctionCallReproduce != "" && + haltExecution != HaltExecution::Reason::ReachedTarget) { + haltExecution = HaltExecution::UnreachedTarget; + } + klee_message("halting execution, dumping remaining states"); for (const auto &state : pausedStates) terminateStateEarly(*state, "Execution halting (paused state).", @@ -4480,6 +4546,8 @@ void Executor::executeStep(ExecutionState &state) { terminateStateEarly(state, "max-cycles exceeded.", StateTerminationType::MaxCycles); } else { + maxNewWriteableOSSize = 0; + maxNewStateStackSize = 0; KInstruction *ki = state.pc; stepInstruction(state); executeInstruction(state, ki); @@ -5988,6 +6056,8 @@ void Executor::collectReads( !targetType->getRawType()->isPointerTy()) { result = makeMockValue(state, "mockGlobalValue", result->getWidth()); ObjectState *wos = state.addressSpace.getWriteable(mo, os); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->write(mo->getOffsetExpr(address), result); } @@ -6137,6 +6207,8 @@ void Executor::executeMemoryOperation( state->addPointerResolution(address, mo); if (isWrite) { ObjectState *wos = state->addressSpace.getWriteable(mo, os); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->getDynamicType()->handleMemoryAccess( targetType, mo->getOffsetExpr(address), ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); @@ -6162,6 +6234,8 @@ void Executor::executeMemoryOperation( !targetType->getRawType()->isPointerTy()) { result = makeMockValue(*state, "mockGlobalValue", result->getWidth()); ObjectState *wos = state->addressSpace.getWriteable(mo, os); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->write(mo->getOffsetExpr(address), result); } @@ -6257,6 +6331,8 @@ void Executor::executeMemoryOperation( const ObjectState *os = op.second; ObjectState *wos = state->addressSpace.getWriteable(mo, os); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); if (wos->readOnly) { branches = forkInternal(*state, Expr::createIsZero(unboundConditions[i]), @@ -6326,6 +6402,8 @@ void Executor::executeMemoryOperation( if (isWrite) { ObjectState *wos = bound->addressSpace.getWriteable(mo, os); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->getDynamicType()->handleMemoryAccess( targetType, mo->getOffsetExpr(address), ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); @@ -6348,6 +6426,8 @@ void Executor::executeMemoryOperation( !targetType->getRawType()->isPointerTy()) { result = makeMockValue(*bound, "mockGlobalValue", result->getWidth()); ObjectState *wos = bound->addressSpace.getWriteable(mo, os); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->write(mo->getOffsetExpr(address), result); } @@ -6537,6 +6617,8 @@ void Executor::updateStateWithSymcretes(ExecutionState &state, auto wos = new ObjectState( *(state.addressSpace.getWriteable(op.first, op.second))); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->swapObjectHack(newMO); state.addressSpace.unbindObject(op.first); state.addressSpace.bindObject(newMO, wos); @@ -6763,7 +6845,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, if (guidanceKind == GuidanceKind::ErrorGuidance) { std::map, - klee::TargetedExecutionManager::KFunctionLess> + klee::KFunctionCompare> prepTargets; if (FunctionCallReproduce == "") { auto &paths = interpreterOpts.Paths.value(); @@ -7223,6 +7305,13 @@ Assignment Executor::computeConcretization(const ConstraintSet &constraints, bool isReproducible(const klee::Symbolic &symb) { auto arr = symb.array; bool bad = IrreproducibleSource::classof(arr->source.get()); + if (auto liSource = dyn_cast(arr->source.get())) { + std::vector arrays; + findObjects(liSource->pointer, arrays); + for (auto innerArr : arrays) { + bad |= IrreproducibleSource::classof(innerArr->source.get()); + } + } if (bad) klee_warning_once(arr->source.get(), "A irreproducible symbolic %s reaches a test", @@ -7292,6 +7381,15 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { std::copy_if(state.symbolics.begin(), state.symbolics.end(), std::back_inserter(symbolics), isReproducible); + // we cannot be sure that an irreproducible state proves the presence of an + // error + if (uninitObjects.size() > 0 || state.symbolics.size() != symbolics.size()) { + state.error = ReachWithError::None; + } else if (FunctionCallReproduce != "" && + state.error == ReachWithError::Reachable) { + setHaltExecution(HaltExecution::ReachedTarget); + } + std::vector> values; std::vector objects; for (auto &symbolic : symbolics) { @@ -7377,6 +7475,8 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, ref e, assert(!os->readOnly && "not possible? read only object with static read?"); ObjectState *wos = state.addressSpace.getWriteable(mo, os); + maxNewWriteableOSSize = + std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->write(CE, it->second); } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index a1a1e3c380..0f8d8eaf69 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -123,6 +123,9 @@ class Executor : public Interpreter { private: int *errno_addr; + size_t maxNewWriteableOSSize = 0; + size_t maxNewStateStackSize = 0; + using SetOfStates = std::set; /* Set of Intrinsic::ID. Plain type is used here to avoid including llvm in * the header */ @@ -779,6 +782,8 @@ class Executor : public Interpreter { haltExecution = value; } + HaltExecution::Reason getHaltExecution() override { return haltExecution; } + void setInhibitForking(bool value) override { inhibitForking = value; } void prepareForEarlyExit() override; diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index ef3a100f0e..ce19fa74bf 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -36,13 +36,28 @@ using namespace llvm; namespace klee { extern llvm::cl::opt X86FPAsX87FP80; +ref X87FP80ToFPTrunc(ref arg, Expr::Width type, + llvm::APFloat::roundingMode rm) { + ref result = arg; +#ifdef ENABLE_FP + Expr::Width resultType = type; + if (Context::get().getPointerWidth() == 32 && arg->getWidth() == Expr::Fl80) { + result = FPTruncExpr::create(arg, resultType, rm); + } +#else + klee_message( + "You may enable x86-as-x87FP80 behaviour by passing the following options" + " to cmake:\n" + "\"-DENABLE_FLOATING_POINT=ON\"\n"); +#endif // ENABLE_FP + return result; +} ref FPToX87FP80Ext(ref arg) { ref result = arg; #ifdef ENABLE_FP Expr::Width resultType = Expr::Fl80; - if (Context::get().getPointerWidth() == 32 && - arg->getWidth() == Expr::Int64) { + if (Context::get().getPointerWidth() == 32) { result = FPExtExpr::create(arg, resultType); } #else @@ -340,8 +355,22 @@ ref Executor::evalConstantExpr(const llvm::ConstantExpr *ce, return op1->LShr(op2); case Instruction::AShr: return op1->AShr(op2); - case Instruction::BitCast: - return op1; + case Instruction::BitCast: { + ref result = op1; + + if (X86FPAsX87FP80 && result->getWidth() == Expr::Fl80 && + !ce->getType()->isFloatingPointTy() && + Context::get().getPointerWidth() == 32) { + result = cast( + X87FP80ToFPTrunc(result, getWidthForLLVMType(type), rm)); + } + + if (X86FPAsX87FP80 && ce->getType()->isFloatingPointTy() && + Context::get().getPointerWidth() == 32) { + result = cast(FPToX87FP80Ext(result)); + } + return result; + } case Instruction::IntToPtr: return op1->ZExt(getWidthForLLVMType(type)); diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 7b072ddcf1..6d3bb3b987 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -246,6 +246,10 @@ class ObjectState { void setReadOnly(bool ro) { readOnly = ro; } + size_t getSparseStorageEntries() { + return knownSymbolics.storage().size() + unflushedMask.storage().size(); + } + void swapObjectHack(MemoryObject *mo) { object = mo; } ref read(ref offset, Expr::Width width) const; diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index f2d91cfd79..f42f798141 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -193,12 +193,12 @@ weight_type TargetedSearcher::getWeight(ExecutionState *es) { ExecutionState &GuidedSearcher::selectState() { unsigned size = historiesAndTargets.size(); - index = theRNG.getInt32() % (size + 1); + interleave ^= 1; ExecutionState *state = nullptr; - if (index == size) { + if (interleave || !size) { state = &baseSearcher->selectState(); } else { - index = index % size; + index = theRNG.getInt32() % size; auto &historyTargetPair = historiesAndTargets[index]; ref history = historyTargetPair.first; ref target = historyTargetPair.second; @@ -657,7 +657,7 @@ class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric { return state.isCycled(maxCycles); } void increaseLimit() final { - maxCycles *= 2ULL; + maxCycles *= 4ULL; klee_message("increased max-cycles to %llu", maxCycles); } }; diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 8b8224f85c..f0b7e8d2b5 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -169,6 +169,7 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber { DistanceCalculator &distanceCalculator; RNG &theRNG; unsigned index{1}; + bool interleave = true; TargetForestHistoryTargetSet localHistoryTargets; std::vector baseAddedStates; diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index d323180908..ab4b67f3df 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -493,13 +493,12 @@ KFunction *TargetedExecutionManager::tryResolveEntryFunction( return resKf; } -std::map, - TargetedExecutionManager::KFunctionLess> +std::map, KFunctionCompare> TargetedExecutionManager::prepareTargets(KModule *kmodule, SarifReport paths) { Locations locations = collectAllLocations(paths); LocationToBlocks locToBlocks = prepareAllLocations(kmodule, locations); - std::map, KFunctionLess> whitelists; + std::map, KFunctionCompare> whitelists; for (auto &result : paths.results) { bool isFullyResolved = tryResolveLocations(result, locToBlocks); diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h index 93ea108a07..e5f72e935b 100644 --- a/lib/Core/TargetedExecutionManager.h +++ b/lib/Core/TargetedExecutionManager.h @@ -115,17 +115,11 @@ class TargetedExecutionManager { StatesSet localStates; public: - struct KFunctionLess { - bool operator()(const KFunction *a, const KFunction *b) const { - return a->id < b->id; - } - }; - explicit TargetedExecutionManager(CodeGraphInfo &codeGraphInfo_, TargetManager &targetManager_) : codeGraphInfo(codeGraphInfo_), targetManager(targetManager_) {} ~TargetedExecutionManager() = default; - std::map, KFunctionLess> + std::map, KFunctionCompare> prepareTargets(KModule *kmodule, SarifReport paths); void reportFalseNegative(ExecutionState &state, ReachWithError error); diff --git a/lib/Expr/AlphaBuilder.cpp b/lib/Expr/AlphaBuilder.cpp index b3b98723c9..13fb00073f 100644 --- a/lib/Expr/AlphaBuilder.cpp +++ b/lib/Expr/AlphaBuilder.cpp @@ -16,7 +16,7 @@ namespace klee { const Array *AlphaBuilder::visitArray(const Array *arr) { - if (alphaArrayMap.find(arr) == alphaArrayMap.end()) { + if (!reverse && alphaArrayMap.find(arr) == alphaArrayMap.end()) { ref source = arr->source; ref size = visit(arr->getSize()); @@ -35,7 +35,11 @@ const Array *AlphaBuilder::visitArray(const Array *arr) { reverseAlphaArrayMap[arr] = arr; } } - return alphaArrayMap[arr]; + if (reverse) { + return reverseAlphaArrayMap[arr]; + } else { + return alphaArrayMap[arr]; + } } UpdateList AlphaBuilder::visitUpdateList(UpdateList u) { @@ -81,5 +85,11 @@ ref AlphaBuilder::build(ref v) { reverseExprMap[Expr::createIsZero(e)] = Expr::createIsZero(v); return e; } +ref AlphaBuilder::reverseBuild(ref v) { + reverse = true; + ref e = visit(v); + reverse = false; + return e; +} } // namespace klee diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index aa963d6cbc..b88c204555 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -265,8 +265,8 @@ ConstraintSet ConstraintSet::getConcretizedVersion() const { _independentElements->getConcretizedVersion()); for (auto &e : cs._independentElements->is()) { - if (isa(e)) { - cs._constraints.insert(cast(e)->value()); + if (isa(e)) { + cs._constraints.insert(cast(e)->value()); } } return cs; @@ -278,7 +278,7 @@ ConstraintSet ConstraintSet::getConcretizedVersion( cs._independentElements = std::make_shared( _independentElements->getConcretizedVersion(newConcretization)); for (auto &e : cs._independentElements->is()) { - cs._constraints.insert(cast(e)->value()); + cs._constraints.insert(cast(e)->value()); } return cs; } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index ec1ecd9235..90f2380709 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -1821,9 +1821,13 @@ ref FPTruncExpr::create(const ref &e, Width w, return e; } else if (ConstantExpr *CE = dyn_cast(e)) { return CE->FPTrunc(w, rm); - } else { - return FPTruncExpr::alloc(e, w, rm); + } else if (FPExtExpr *ExtE = dyn_cast(e)) { + if (ExtE->src->getWidth() == w) { + return ExtE->src; + } } + + return FPTruncExpr::alloc(e, w, rm); } ref FPToUIExpr::create(const ref &e, Width w, diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp index 74fa369b14..b2c67e5a14 100644 --- a/lib/Expr/IndependentConstraintSetUnion.cpp +++ b/lib/Expr/IndependentConstraintSetUnion.cpp @@ -20,13 +20,13 @@ IndependentConstraintSetUnion::IndependentConstraintSetUnion( ref ics) { auto exprs = ics->exprs; for (ref e : exprs) { - auto v = ref(new ExprEitherSymcrete::left(e)); + auto v = ref(new ExprOrSymcrete::left(e)); rank.insert_or_assign(v, 0); internalStorage.insert(v); } for (ref s : ics->symcretes) { - auto v = ref(new ExprEitherSymcrete::right(s)); + auto v = ref(new ExprOrSymcrete::right(s)); rank.insert_or_assign(v, 0); internalStorage.insert(v); } @@ -114,7 +114,7 @@ void IndependentConstraintSetUnion::getAllIndependentConstraintSets( ref e, std::vector> &result) { calculateQueue(); ref compare = - new IndependentConstraintSet(new ExprEitherSymcrete::left(e)); + new IndependentConstraintSet(new ExprOrSymcrete::left(e)); for (auto &r : roots) { ref ics = disjointSets.at(r); if (!IndependentConstraintSet::intersects(ics, compare)) { @@ -127,7 +127,7 @@ void IndependentConstraintSetUnion::getAllDependentConstraintSets( ref e, std::vector> &result) { calculateQueue(); ref compare = - new IndependentConstraintSet(new ExprEitherSymcrete::left(e)); + new IndependentConstraintSet(new ExprOrSymcrete::left(e)); for (auto &r : roots) { ref ics = disjointSets.at(r); if (IndependentConstraintSet::intersects(ics, compare)) { @@ -137,11 +137,11 @@ void IndependentConstraintSetUnion::getAllDependentConstraintSets( } void IndependentConstraintSetUnion::addExpr(ref e) { - constraintQueue.push_back(new ExprEitherSymcrete::left(e)); + constraintQueue.push_back(new ExprOrSymcrete::left(e)); } void IndependentConstraintSetUnion::addSymcrete(ref s) { - constraintQueue.push_back(new ExprEitherSymcrete::right(s)); + constraintQueue.push_back(new ExprOrSymcrete::right(s)); } IndependentConstraintSetUnion @@ -152,7 +152,7 @@ IndependentConstraintSetUnion::getConcretizedVersion() { ref root = disjointSets.at(i); if (root->concretization.bindings.empty()) { for (ref expr : root->exprs) { - icsu.addValue(new ExprEitherSymcrete::left(expr)); + icsu.addValue(new ExprOrSymcrete::left(expr)); } } else { icsu.add(root->concretizedSets); diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index d01b234f17..888dc52fdd 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -34,7 +34,7 @@ IndependentConstraintSet::updateConcretization( continue; } concretizedExprs[i] = e; - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } for (ref s : symcretes) { ref e = EqExpr::create(ics->concretization.evaluate(s->symcretized), @@ -43,7 +43,7 @@ IndependentConstraintSet::updateConcretization( assert(ce->isTrue() && "Attempt to add invalid constraint"); continue; } - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } auto concretizationConstraints = ics->concretization.createConstraintsFromAssignment(); @@ -52,7 +52,7 @@ IndependentConstraintSet::updateConcretization( assert(ce->isTrue() && "Attempt to add invalid constraint"); continue; } - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } ics->concretizedSets = DSU; return ics; @@ -76,7 +76,7 @@ IndependentConstraintSet::removeConcretization( continue; } concretizedExprs[i] = e; - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } for (ref s : symcretes) { ref e = EqExpr::create(ics->concretization.evaluate(s->symcretized), @@ -85,7 +85,7 @@ IndependentConstraintSet::removeConcretization( assert(ce->isTrue() && "Attempt to add invalid constraint"); continue; } - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } auto concretizationConstraints = ics->concretization.createConstraintsFromAssignment(); @@ -94,7 +94,7 @@ IndependentConstraintSet::removeConcretization( assert(ce->isTrue() && "Attempt to add invalid constraint"); continue; } - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } ics->concretizedSets = DSU; @@ -123,11 +123,11 @@ void IndependentConstraintSet::addValuesToAssignment( IndependentConstraintSet::IndependentConstraintSet() {} -IndependentConstraintSet::IndependentConstraintSet(ref v) { - if (isa(v)) { - initIndependentConstraintSet(cast(v)->value()); +IndependentConstraintSet::IndependentConstraintSet(ref v) { + if (isa(v)) { + initIndependentConstraintSet(cast(v)->value()); } else { - initIndependentConstraintSet(cast(v)->value()); + initIndependentConstraintSet(cast(v)->value()); } } @@ -350,7 +350,7 @@ IndependentConstraintSet::merge(ref A, assert(ce->isTrue() && "Attempt to add invalid constraint"); continue; } - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } for (ref s : a->symcretes) { ref e = EqExpr::create(a->concretization.evaluate(s->symcretized), @@ -359,7 +359,7 @@ IndependentConstraintSet::merge(ref A, assert(ce->isTrue() && "Attempt to add invalid constraint"); continue; } - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } auto concretizationConstraints = a->concretization.createConstraintsFromAssignment(); @@ -368,7 +368,7 @@ IndependentConstraintSet::merge(ref A, assert(ce->isTrue() && "Attempt to add invalid constraint"); continue; } - DSU.addValue(new ExprEitherSymcrete::left(e)); + DSU.addValue(new ExprOrSymcrete::left(e)); } a->concretizedSets = DSU; @@ -405,7 +405,7 @@ void calculateArraysInFactors( } std::vector result; ref queryExprSet = - new IndependentConstraintSet(new ExprEitherSymcrete::left(queryExpr)); + new IndependentConstraintSet(new ExprOrSymcrete::left(queryExpr)); queryExprSet->calculateArrayReferences(result); returnSet.insert(result.begin(), result.end()); returnVector.insert(returnVector.begin(), returnSet.begin(), returnSet.end()); diff --git a/lib/Solver/AlphaEquivalenceSolver.cpp b/lib/Solver/AlphaEquivalenceSolver.cpp index 4c0cc81fa3..d8b6011c78 100644 --- a/lib/Solver/AlphaEquivalenceSolver.cpp +++ b/lib/Solver/AlphaEquivalenceSolver.cpp @@ -54,7 +54,7 @@ class AlphaEquivalenceSolver : public SolverImpl { void setCoreSolverTimeout(time::Span timeout); void notifyStateTermination(std::uint32_t id); ValidityCore changeVersion(const ValidityCore &validityCore, - const ExprHashMap> &reverse); + AlphaBuilder &builder); std::vector changeVersion(const std::vector &objects, AlphaBuilder &builder); @@ -66,24 +66,20 @@ class AlphaEquivalenceSolver : public SolverImpl { changeVersion(const Assignment &a, const ArrayCache::ArrayHashMap &reverse); ref changeVersion(ref res, - const AlphaBuilder &builder); - ref createAlphaVersion(ref res, - const AlphaBuilder &builder); + AlphaBuilder &builder); }; ValidityCore AlphaEquivalenceSolver::changeVersion(const ValidityCore &validityCore, - const ExprHashMap> &reverse) { + AlphaBuilder &builder) { ValidityCore reverseValidityCore; if (isa(validityCore.expr)) { reverseValidityCore.expr = validityCore.expr; } else { - assert(reverse.find(validityCore.expr) != reverse.end()); - reverseValidityCore.expr = reverse.at(validityCore.expr); + reverseValidityCore.expr = builder.reverseBuild(validityCore.expr); } for (auto e : validityCore.constraints) { - assert(reverse.find(e) != reverse.end()); - reverseValidityCore.constraints.insert(reverse.at(e)); + reverseValidityCore.constraints.insert(builder.reverseBuild(e)); } return reverseValidityCore; } @@ -123,7 +119,7 @@ Assignment AlphaEquivalenceSolver::changeVersion( ref AlphaEquivalenceSolver::changeVersion(ref res, - const AlphaBuilder &builder) { + AlphaBuilder &builder) { ref reverseRes; if (!isa(res) && !isa(res)) { return res; @@ -136,24 +132,12 @@ AlphaEquivalenceSolver::changeVersion(ref res, } else { ValidityCore validityCore; res->tryGetValidityCore(validityCore); - validityCore = changeVersion(validityCore, builder.reverseExprMap); + validityCore = changeVersion(validityCore, builder); reverseRes = new ValidResponse(validityCore); } return reverseRes; } -ref -AlphaEquivalenceSolver::createAlphaVersion(ref res, - const AlphaBuilder &builder) { - if (!res || !isa(res)) { - return res; - } - - Assignment a = cast(res)->initialValues(); - changeVersion(a, builder.alphaArrayMap); - return new InvalidResponse(a.bindings); -} - bool AlphaEquivalenceSolver::computeValidity(const Query &query, PartialValidity &result) { AlphaBuilder builder(arrayCache); @@ -205,7 +189,6 @@ bool AlphaEquivalenceSolver::check(const Query &query, constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs()); ref alphaQueryExpr = builder.build(query.expr); - result = createAlphaVersion(result, builder); if (!solver->impl->check( Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id), result)) { @@ -228,7 +211,7 @@ bool AlphaEquivalenceSolver::computeValidityCore(const Query &query, validityCore, isValid)) { return false; } - validityCore = changeVersion(validityCore, builder.reverseExprMap); + validityCore = changeVersion(validityCore, builder); return true; } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 3cd4947c9f..038af68e2e 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -93,6 +93,7 @@ class CexCachingSolver : public SolverImpl { } bool getResponse(const Query &query, ref &result); + void setResponse(const Query &query, ref &result); public: CexCachingSolver(std::unique_ptr solver) @@ -132,8 +133,9 @@ struct isValidOrSatisfyingResponse { isValidOrSatisfyingResponse(KeyType &_key) : key(_key) {} bool operator()(ref a) const { - return isa(a) || (isa(a) && - cast(a)->satisfies(key)); + return isa(a) || + (isa(a) && + cast(a)->satisfiesOrConstant(key)); } }; @@ -208,6 +210,17 @@ bool CexCachingSolver::searchForResponse(KeyType &key, return false; } +KeyType makeKey(const Query &query) { + KeyType key = + KeyType(query.constraints.cs().begin(), query.constraints.cs().end()); + for (ref s : query.constraints.symcretes()) { + key.insert(s->symcretized); + } + ref neg = Expr::createIsZero(query.expr); + key.insert(neg); + return key; +} + /// lookupResponse - Lookup a cached result for the given \arg query. /// /// \param query - The query to lookup. @@ -217,10 +230,7 @@ bool CexCachingSolver::searchForResponse(KeyType &key, /// an unsatisfiable query). \return True if a cached result was found. bool CexCachingSolver::lookupResponse(const Query &query, KeyType &key, ref &result) { - key = KeyType(query.constraints.cs().begin(), query.constraints.cs().end()); - for (ref s : query.constraints.symcretes()) { - key.insert(s->symcretized); - } + key = makeKey(query); ref neg = Expr::createIsZero(query.expr); if (ConstantExpr *CE = dyn_cast(neg)) { if (CE->isFalse()) { @@ -228,8 +238,6 @@ bool CexCachingSolver::lookupResponse(const Query &query, KeyType &key, ++stats::queryCexCacheHits; return true; } - } else { - key.insert(neg); } bool found = searchForResponse(key, result); @@ -243,8 +251,7 @@ bool CexCachingSolver::lookupResponse(const Query &query, KeyType &key, bool CexCachingSolver::getResponse(const Query &query, ref &result) { - KeyType key; - if (lookupResponse(query, key, result)) { + if (lookupResponse(query, result)) { return true; } @@ -252,6 +259,14 @@ bool CexCachingSolver::getResponse(const Query &query, return false; } + setResponse(query, result); + return true; +} + +void CexCachingSolver::setResponse(const Query &query, + ref &result) { + KeyType key = makeKey(query); + if (isa(result)) { // Memorize the result. std::pair res = @@ -261,7 +276,7 @@ bool CexCachingSolver::getResponse(const Query &query, } if (DebugCexCacheCheckBinding) { - if (!cast(result)->satisfiesOrConstant(key)) { + if (!cast(result)->satisfiesOrConstant(key, false)) { query.dump(); result->dump(); klee_error("Generated assignment doesn't match query"); @@ -281,8 +296,6 @@ bool CexCachingSolver::getResponse(const Query &query, if (isa(result) || isa(result)) { cache.insert(key, result); } - - return true; } /// @@ -364,6 +377,12 @@ bool CexCachingSolver::computeValue(const Query &query, ref &result) { assert(isa(result) && "assignment evaluation did not result in constant"); + + if (cast(result)->isTrue()) { + setResponse(query.negateExpr(), a); + } else if (cast(result)->isFalse()) { + setResponse(query, a); + } return true; } diff --git a/scripts/build/p-bitwuzla-linux-ubuntu.inc b/scripts/build/p-bitwuzla-linux-ubuntu.inc index cd585c7e31..f36ab25d5e 100644 --- a/scripts/build/p-bitwuzla-linux-ubuntu.inc +++ b/scripts/build/p-bitwuzla-linux-ubuntu.inc @@ -19,7 +19,7 @@ install_build_dependencies_bitwuzla() { with_sudo apt-get update -y with_sudo apt-get -y --no-install-recommends install pkg-config cmake-data m4 - with_sudo pip3 install --user meson + pip3 install --user meson base_path="$(python3 -m site --user-base)" export PATH="$PATH:${base_path}/bin" } diff --git a/scripts/build/p-bitwuzla-osx.inc b/scripts/build/p-bitwuzla-osx.inc index af4cc8f651..27df98058e 100644 --- a/scripts/build/p-bitwuzla-osx.inc +++ b/scripts/build/p-bitwuzla-osx.inc @@ -7,8 +7,8 @@ install_build_dependencies_bitwuzla() { git pkg-config ) - brew install "${dependencies[@]}" - with_sudo pip3 install --user meson + brew install "${dependencies[@]}" + pip3 install --user meson base_path="$(python3 -m site --user-base)" export PATH="$PATH:${base_path}/bin" } diff --git a/scripts/kleef b/scripts/kleef index 35f0e4ac65..2dd0bd016d 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -22,9 +22,9 @@ def klee_options( write_ktests, ): if max_time and int(max_time) > 30: - MAX_SOLVER_TIME = 10 + MAX_SOLVER_TIME = 15 else: - MAX_SOLVER_TIME = 5 + MAX_SOLVER_TIME = 10 cmd = [ "--strip-unwanted-calls", # removes llvm.dbg.* instructions, exponentially reduces time on some benchmarks "--delete-dead-loops=false", # without this optimizer removes some code, which decreases coverage @@ -33,10 +33,11 @@ def klee_options( "--external-calls=all", "--use-forked-solver=false", # "--solver-backend=stp", - "--solver-backend=z3-tree", + # "--solver-backend=z3-tree", + "--solver-backend=bitwuzla-tree", "--max-solvers-approx-tree-inc=16", f"--max-memory={int(max_memory * 0.9)}", # Just use half of the memory in case we have to fork - "--optimize", + "--libc=klee", "--skip-not-lazy-initialized", f"--output-dir={test_output_dir}", # Output files into specific directory "--output-source=false", # Do not output assembly.ll - it can be too large @@ -53,7 +54,6 @@ def klee_options( # "--libc=uclibc", # "--posix-runtime", "--fp-runtime", - "--x86FP-as-x87FP80=false", # "--max-sym-array-size=4096", "--symbolic-allocation-threshold=8192", "--uninit-memory-test-multiplier=10", @@ -68,38 +68,48 @@ def klee_options( "--allocate-determ", f"--allocate-determ-size={min(int(max_memory * 0.6), 3 * 1024)}", "--allocate-determ-start-address=0x00030000000", + "--x86FP-as-x87FP80", ] if f_err: cmd += [ - "--use-alpha-equivalence=false", + "--optimize=true", + "--use-alpha-equivalence=true", "--function-call-reproduce=reach_error", # "--max-cycles=0", # "--tc-type=bug", - "--dump-states-on-halt=false", # Explicitly do not dump states + "--dump-states-on-halt=unreached", # Explicitly do not dump states "--exit-on-error-type=Assert", # Only generate test cases of type assert # "--dump-test-case-type=Assert", # Only dump test cases of type assert "--search=dfs", + "--search=bfs", # "--search=nurs:covnew", "--search=random-path","--search=dfs", "--use-batching-search", # "--search=distance","--search=random-path","--use-batching-search", # "--target-assert", # Target ] if max_time: + max_time = float(max_time) + if max_time and int(max_time) > 30: + max_time = int(max_time * 0.99) + else: + max_time = int(max_time * 0.9) cmd += [ - f"--max-time={int(max_time)}", # Use the whole time + f"--max-time={max_time}", ] if f_cov: cmd += [ + "--optimize=false", "--mem-trigger-cof", # Start on the fly tests generation after approaching memory cup "--use-alpha-equivalence=true", + "--optimize-aggressive=false", "--track-coverage=all", # Only branches and only instructions are wrong in real life. E.g., ternary operators are sometimes counted as different branches, while we stick to look at them as a single instruction from a single branch "--use-iterative-deepening-search=max-cycles", f"--max-solver-time={MAX_SOLVER_TIME}s", "--max-cycles-before-stuck=15", # "--tc-type=cov", "--only-output-states-covering-new", # Don't generate all test cases - "--dump-states-on-halt=true", # Check in case we missed some oncovered instructions + "--dump-states-on-halt=all", # Check in case we missed some oncovered instructions "--search=dfs", "--search=random-state", ] @@ -267,6 +277,7 @@ class KLEEF(object): def run(self): test_output_dir = self.test_results_path / self.source.name + test_output_dir = self.test_results_path # Clean-up from previous runs if needed shutil.rmtree(test_output_dir, ignore_errors=True) diff --git a/test/Feature/CoverOnTheFly.c b/test/Feature/CoverOnTheFly.c index 37e4381614..73bd550f2c 100644 --- a/test/Feature/CoverOnTheFly.c +++ b/test/Feature/CoverOnTheFly.c @@ -1,8 +1,8 @@ -// ASAN fails because KLEE does not cleanup states with -dump-states-on-halt=false +// ASAN fails because KLEE does not cleanup states with -dump-states-on-halt=none // 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 --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 +// RUN: %klee --only-output-states-covering-new --max-instructions=2000 --timer-interval=1ms --delay-cover-on-the-fly=1ms --dump-states-on-halt=none --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" diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c index aca8d7c810..9bda0cb83a 100644 --- a/test/Feature/DumpStatesOnHalt.c +++ b/test/Feature/DumpStatesOnHalt.c @@ -1,6 +1,6 @@ // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-instructions=1 --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --max-instructions=1 --dump-states-on-halt=all %t1.bc 2>&1 | FileCheck %s // RUN: test -f %t.klee-out/test000001.ktest int main(int argc, char **argv) { diff --git a/test/Floats/cast_union_loose.c b/test/Floats/cast_union_loose.c new file mode 100644 index 0000000000..6dbf5c77a9 --- /dev/null +++ b/test/Floats/cast_union_loose.c @@ -0,0 +1,53 @@ +// It requires bitwuzla because the script currently runs with bitwuzla solver backend +// REQUIRES: bitwuzla +// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --32 %s + +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__((__nothrow__, __leaf__)) __attribute__((__noreturn__)); +void reach_error() { __assert_fail("0", "cast_union_loose.c", 3, "reach_error"); } +/* Example from "Abstract Domains for Bit-Level Machine Integer and + Floating-point Operations" by Miné, published in WING 12. +*/ + +extern int __VERIFIER_nondet_int(void); +extern void abort(void); +void assume_abort_if_not(int cond) { + if (!cond) { + abort(); + } +} +void __VERIFIER_assert(int cond) { + if (!(cond)) { + ERROR : { + reach_error(); + abort(); + } + } + return; +} + +union u { + int i[2]; + double d; +}; + +double cast(int i) { + union u x, y; + x.i[0] = 0x43300000; + y.i[0] = x.i[0]; + x.i[1] = 0x80000000; + y.i[1] = i ^ x.i[1]; + return y.d - x.d; +} + +int main() { + int a; + double r; + + a = __VERIFIER_nondet_int(); + assume_abort_if_not(a >= -10000 && a <= 10000); + + r = cast(a); + __VERIFIER_assert(r >= -10000. && r <= 10000.); + return 0; +} diff --git a/test/Floats/cast_union_loose.yml b/test/Floats/cast_union_loose.yml new file mode 100644 index 0000000000..27094e3abe --- /dev/null +++ b/test/Floats/cast_union_loose.yml @@ -0,0 +1,18 @@ +format_version: '2.0' + +# old file name: cast_union_loose_false-unreach-call_true-termination.c +input_files: 'cast_union_loose.c' + +properties: + - property_file: ../properties/termination.prp + expected_verdict: true + - property_file: ../properties/unreach-call.prp + expected_verdict: false + - property_file: ../properties/coverage-error-call.prp + - property_file: ../properties/coverage-branches.prp + - property_file: ../properties/coverage-conditions.prp + - property_file: ../properties/coverage-statements.prp + +options: + language: C + data_model: ILP32 diff --git a/test/Floats/cast_union_tight.c b/test/Floats/cast_union_tight.c new file mode 100644 index 0000000000..a5f5e5fe44 --- /dev/null +++ b/test/Floats/cast_union_tight.c @@ -0,0 +1,46 @@ +// It requires bitwuzla because the script currently runs with bitwuzla solver backend +// REQUIRES: bitwuzla +// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --32 %s + +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__((__nothrow__, __leaf__)) __attribute__((__noreturn__)); +void reach_error() { __assert_fail("0", "cast_union_tight.c", 3, "reach_error"); } +/* Example from "Abstract Domains for Bit-Level Machine Integer and + Floating-point Operations" by Miné, published in WING 12. +*/ + +extern int __VERIFIER_nondet_int(void); +void __VERIFIER_assert(int cond) { + if (!(cond)) { + ERROR : { + reach_error(); + abort(); + } + } + return; +} + +union u { + int i[2]; + double d; +}; + +double cast(int i) { + union u x, y; + x.i[0] = 0x43300000; + y.i[0] = x.i[0]; + x.i[1] = 0x80000000; + y.i[1] = i ^ x.i[1]; + return y.d - x.d; +} + +int main() { + int a; + double r; + + a = __VERIFIER_nondet_int(); + + r = cast(a); + __VERIFIER_assert(r == a); + return 0; +} diff --git a/test/Floats/cast_union_tight.yml b/test/Floats/cast_union_tight.yml new file mode 100644 index 0000000000..7bea04b7f8 --- /dev/null +++ b/test/Floats/cast_union_tight.yml @@ -0,0 +1,18 @@ +format_version: '2.0' + +# old file name: cast_union_tight_false-unreach-call_true-termination.c +input_files: 'cast_union_tight.c' + +properties: + - property_file: ../properties/termination.prp + expected_verdict: true + - property_file: ../properties/unreach-call.prp + expected_verdict: false + - property_file: ../properties/coverage-error-call.prp + - property_file: ../properties/coverage-branches.prp + - property_file: ../properties/coverage-conditions.prp + - property_file: ../properties/coverage-statements.prp + +options: + language: C + data_model: ILP32 diff --git a/test/Floats/copysign.c b/test/Floats/copysign.c index 03f3cb4851..80a5921322 100644 --- a/test/Floats/copysign.c +++ b/test/Floats/copysign.c @@ -16,4 +16,4 @@ int main() { return 2; } } -// CHECK: KLEE: done: completed paths = 4 +// CHECK: KLEE: done: completed paths = {{4|6}} diff --git a/test/Floats/coverage-error-call.prp b/test/Floats/coverage-error-call.prp new file mode 100644 index 0000000000..496ed998fa --- /dev/null +++ b/test/Floats/coverage-error-call.prp @@ -0,0 +1,2 @@ +COVER( init(main()), FQL(COVER EDGES(@CALL(reach_error))) ) + diff --git a/test/Floats/double_req_bl_0670.c b/test/Floats/double_req_bl_0670.c new file mode 100644 index 0000000000..0ecac476be --- /dev/null +++ b/test/Floats/double_req_bl_0670.c @@ -0,0 +1,279 @@ +// It requires bitwuzla because the script currently runs with bitwuzla solver backend +// REQUIRES: bitwuzla +// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --32 %s + +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__((__nothrow__, __leaf__)) __attribute__((__noreturn__)); +void reach_error() { __assert_fail("0", "double_req_bl_0670.c", 3, "reach_error"); } +extern double __VERIFIER_nondet_double(); + +typedef int __int32_t; +typedef unsigned int __uint32_t; + +/* A union which permits us to convert between a double and two 32 bit + ints. */ +typedef union { + double value; + struct { + __uint32_t lsw; + __uint32_t msw; + } parts; +} ieee_double_shape_type; + +double fabs_double(double x) { + __uint32_t high; + do { + ieee_double_shape_type gh_u; + gh_u.value = (x); + (high) = gh_u.parts.msw; + } while (0); + do { + ieee_double_shape_type sh_u; + sh_u.value = (x); + sh_u.parts.msw = (high & 0x7fffffff); + (x) = sh_u.value; + } while (0); + return x; +} + +/* + * Preprocessed code for the function libs/newlib/math/s_atan.c + */ + +static const double atanhi_atan[] = { + 4.63647609000806093515e-01, + 7.85398163397448278999e-01, + 9.82793723247329054082e-01, + 1.57079632679489655800e+00, +}; + +static const double atanlo_atan[] = { + 2.26987774529616870924e-17, + 3.06161699786838301793e-17, + 1.39033110312309984516e-17, + 6.12323399573676603587e-17, +}; + +static const double aT_atan[] = { + 3.33333333333329318027e-01, + -1.99999999998764832476e-01, + 1.42857142725034663711e-01, + -1.11111104054623557880e-01, + 9.09088713343650656196e-02, + -7.69187620504482999495e-02, + 6.66107313738753120669e-02, + -5.83357013379057348645e-02, + 4.97687799461593236017e-02, + -3.65315727442169155270e-02, + 1.62858201153657823623e-02, +}; + +static const double one_atan = 1.0, pi_o_4 = 7.8539816339744827900E-01, + pi_o_2 = 1.5707963267948965580E+00, + pi = 3.1415926535897931160E+00, huge_atan = 1.0e300; + +double atan_double(double x) { + double w, s1, s2, z; + __int32_t ix, hx, id; + + do { + ieee_double_shape_type gh_u; + gh_u.value = (x); + (hx) = gh_u.parts.msw; + } while (0); + ix = hx & 0x7fffffff; + if (ix >= 0x44100000) { + __uint32_t low; + do { + ieee_double_shape_type gl_u; + gl_u.value = (x); + (low) = gl_u.parts.lsw; + } while (0); + if (ix > 0x7ff00000 || (ix == 0x7ff00000 && (low != 0))) + return x + x; + if (hx > 0) + return atanhi_atan[3] + atanlo_atan[3]; + else + return -atanhi_atan[3] - atanlo_atan[3]; + } + if (ix < 0x3fdc0000) { + if (ix < 0x3e200000) { + if (huge_atan + x > one_atan) + return x; + } + id = -1; + } else { + x = fabs_double(x); + if (ix < 0x3ff30000) { + if (ix < 0x3fe60000) { + id = 0; + x = (2.0 * x - one_atan) / (2.0 + x); + } else { + id = 1; + x = (x - one_atan) / (x + one_atan); + } + } else { + if (ix < 0x40038000) { + id = 2; + x = (x - 1.5) / (one_atan + 1.5 * x); + } else { + id = 3; + x = -1.0 / x; + } + } + } + + z = x * x; + w = z * z; + + s1 = z * (aT_atan[0] + + w * (aT_atan[2] + + w * (aT_atan[4] + + w * (aT_atan[6] + w * (aT_atan[8] + w * aT_atan[10]))))); + s2 = + w * + (aT_atan[1] + + w * (aT_atan[3] + w * (aT_atan[5] + w * (aT_atan[7] + w * aT_atan[9])))); + if (id < 0) + return x - x * (s1 + s2); + else { + z = atanhi_atan[id] - ((x * (s1 + s2) - atanlo_atan[id]) - x); + return (hx < 0) ? -z : z; + } +} + +/* + * Preprocessed code for the function libs/newlib/math/e_atan2.c (Constants are + * defined in requrements/includes/math_constants_double.h) + */ + +static const double tiny_atan2 = 1.0e-300, zero_atan2 = 0.0, + pi_lo_atan2 = 1.2246467991473531772E-16; + +double __ieee754_atan2(double y, double x) { + double z; + __int32_t k, m, hx, hy, ix, iy; + __uint32_t lx, ly; + + do { + ieee_double_shape_type ew_u; + ew_u.value = (x); + (hx) = ew_u.parts.msw; + (lx) = ew_u.parts.lsw; + } while (0); + ix = hx & 0x7fffffff; + do { + ieee_double_shape_type ew_u; + ew_u.value = (y); + (hy) = ew_u.parts.msw; + (ly) = ew_u.parts.lsw; + } while (0); + iy = hy & 0x7fffffff; + if (((ix | ((lx | -lx) >> 31)) > 0x7ff00000) || + ((iy | ((ly | -ly) >> 31)) > 0x7ff00000)) + return x + y; + if (((hx - 0x3ff00000) | lx) == 0) + return atan_double(y); + m = ((hy >> 31) & 1) | ((hx >> 30) & 2); + + if ((iy | ly) == 0) { + switch (m) { + case 0: + case 1: + return y; + case 2: + return pi + tiny_atan2; + case 3: + return -pi - tiny_atan2; + } + } + + if ((ix | lx) == 0) + return (hy < 0) ? -pi_o_2 - tiny_atan2 : pi_o_2 + tiny_atan2; + + if (ix == 0x7ff00000) { + if (iy == 0x7ff00000) { + switch (m) { + case 0: + return pi_o_4 + tiny_atan2; + case 1: + return -pi_o_4 - tiny_atan2; + case 2: + return 3.0 * pi_o_4 + tiny_atan2; + case 3: + return -3.0 * pi_o_4 - tiny_atan2; + } + } else { + switch (m) { + case 0: + return zero_atan2; + case 1: + return -zero_atan2; + case 2: + return pi + tiny_atan2; + case 3: + return -pi - tiny_atan2; + } + } + } + + if (iy == 0x7ff00000) + return (hy < 0) ? -pi_o_2 - tiny_atan2 : pi_o_2 + tiny_atan2; + + k = (iy - ix) >> 20; + if (k > 60) + z = pi_o_2 + 0.5 * pi_lo_atan2; + else if (hx < 0 && k < -60) + z = 0.0; + else + z = atan_double(fabs_double(y / x)); + switch (m) { + case 0: + return z; + case 1: { + __uint32_t zh; + do { + ieee_double_shape_type gh_u; + gh_u.value = (z); + (zh) = gh_u.parts.msw; + } while (0); + do { + ieee_double_shape_type sh_u; + sh_u.value = (z); + sh_u.parts.msw = (zh ^ 0x80000000); + (z) = sh_u.value; + } while (0); + } + return z; + case 2: + return pi - (z - pi_lo_atan2); + default: + return (z - pi_lo_atan2) - pi; + } +} + +// nan check for doubles +int isnan_double(double x) { return x != x; } + +int main() { + + /* REQ-BL-0670: + * The atan2 and atan2f procedures shall return NaN if any argument is NaN. + */ + + double x = __VERIFIER_nondet_double(); + double y = __VERIFIER_nondet_double(); + + if (isnan_double(x) || isnan_double(y)) { + + double res = __ieee754_atan2(y, x); + + // x is NAN, y is any or vice versa, the result shall be NAN + if (!isnan_double(res)) { + { reach_error(); } + return 1; + } + } + + return 0; +} diff --git a/test/Floats/double_req_bl_0670.yml b/test/Floats/double_req_bl_0670.yml new file mode 100644 index 0000000000..dfe3bebd6a --- /dev/null +++ b/test/Floats/double_req_bl_0670.yml @@ -0,0 +1,15 @@ +format_version: '2.0' + +# old file name: double_req_bl_0670_true-unreach-call.c +input_files: 'double_req_bl_0670.c' + +properties: + - property_file: ../properties/unreach-call.prp + expected_verdict: true + - property_file: ../properties/coverage-branches.prp + - property_file: ../properties/coverage-conditions.prp + - property_file: ../properties/coverage-statements.prp + +options: + language: C + data_model: ILP32 diff --git a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c index 99f638327a..fff21e4d2b 100644 --- a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c +++ b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c @@ -1,6 +1,6 @@ // 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-aggressive=false --track-coverage=branches --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 +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --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=all %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s // RUN: rm -f %t*.gcda %t*.gcno %t*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/CoverageBranches/CostasArray-17.c b/test/Industry/CoverageBranches/CostasArray-17.c index 088a33fbb0..6f2bcea325 100644 --- a/test/Industry/CoverageBranches/CostasArray-17.c +++ b/test/Industry/CoverageBranches/CostasArray-17.c @@ -1,6 +1,6 @@ // 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-aggressive --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs %t1.bc // RUN: rm -f %t*.gcda %t*.gcno %t*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage @@ -10,7 +10,7 @@ // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs %t1.bc // RUN: rm -f %t*.gcda %t*.gcno %t*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c index d5405512d8..9d433194b3 100644 --- a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c +++ b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state %t1.bc +// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc // RUN: rm -f %t*.gcda %t*.gcno %t*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/CoverageBranches/matrix-2-2.c b/test/Industry/CoverageBranches/matrix-2-2.c index d25bd92255..6170da72fe 100644 --- a/test/Industry/CoverageBranches/matrix-2-2.c +++ b/test/Industry/CoverageBranches/matrix-2-2.c @@ -1,6 +1,6 @@ // 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-aggressive=false --track-coverage=all --max-cycles=2 --optimize=true --emit-all-errors --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 --use-sym-size-alloc=true --symbolic-allocation-threshold=8192 %t1.bc 2>&1 +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=all --max-cycles=2 --optimize=true --emit-all-errors --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=all --use-sym-size-alloc=true --symbolic-allocation-threshold=8192 %t1.bc 2>&1 // RUN: rm -f %t*.gcda %t*.gcno %t*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c index 2b7a4dd7e1..c1fc602469 100644 --- a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c +++ b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc // RUN: rm -f %t*.gcda %t*.gcno %t*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c index f11474a141..f0261d2008 100644 --- a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c +++ b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c @@ -1,5 +1,5 @@ -// It requires Z3 because the script currently runs with Z3 solver backend -// REQUIRES: z3 +// It requires bitwuzla because the script currently runs with bitwuzla solver backend +// REQUIRES: bitwuzla // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 --write-ktests %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable diff --git a/test/Industry/egcd3-ll_valuebound10.c b/test/Industry/egcd3-ll_valuebound10.c index cf89ea4af7..5811f1f44d 100644 --- a/test/Industry/egcd3-ll_valuebound10.c +++ b/test/Industry/egcd3-ll_valuebound10.c @@ -1,7 +1,7 @@ // REQUIRES: not-darwin, not-san // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state %t1.bc +// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc // RUN: rm -f %t*.gcda %t*.gcno %t*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/if2.c b/test/Industry/if2.c index e41a4a0a0e..b35cb487bf 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -14,4 +14,4 @@ int main(int x) { // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-DISTANCE -// CHECK-DISTANCE: KLEE: (0, 1, 1) for Target 1: error in function main (lines 8 to 8) +// CHECK-DISTANCE: KLEE: (0, 1, 0) for Target 1: error in function main (lines 8 to 8) diff --git a/test/Industry/ll_create_rec-alloca-2.c b/test/Industry/ll_create_rec-alloca-2.c index a91b65235c..27b037bf35 100644 --- a/test/Industry/ll_create_rec-alloca-2.c +++ b/test/Industry/ll_create_rec-alloca-2.c @@ -1,6 +1,6 @@ // 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 --track-coverage=branches --delete-dead-loops=false --cex-cache-validity-cores --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs --search=random-path %t1.bc +// RUN: %klee --output-dir=%t.klee-out --track-coverage=branches --delete-dead-loops=false --cex-cache-validity-cores --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs --search=random-path %t1.bc // RUN: %klee-stats --print-columns 'ICov(%),BCov(%)' --table-format=csv %t.klee-out > %t.stats // RUN: FileCheck -check-prefix=CHECK-BRANCH -input-file=%t.stats %s @@ -9,7 +9,7 @@ // CHECK-BRANCH-NEXT: {{([1-9][0-9]\.[0-9][0-9])}},100.00 // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --track-coverage=blocks --delete-dead-loops=false --cex-cache-validity-cores --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs --search=random-path %t1.bc +// RUN: %klee --output-dir=%t.klee-out --track-coverage=blocks --delete-dead-loops=false --cex-cache-validity-cores --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs --search=random-path %t1.bc // RUN: %klee-stats --print-columns 'ICov(%),BCov(%)' --table-format=csv %t.klee-out > %t.stats // RUN: FileCheck -check-prefix=CHECK-BLOCK -input-file=%t.stats %s diff --git a/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c index 6048923249..8314734367 100644 --- a/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c +++ b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c @@ -2,7 +2,7 @@ // Disabling msan because it times out on CI // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false -max-memory=6008 --optimize=true --skip-not-lazy-initialized -output-source=true --output-stats=false --output-istats=false --write-xml-tests --write-ktests=false --xml-metadata-programfile=wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c --xml-metadata-programhash=a18daeacf63b42ad6e1cb490555b7cdecd71ad6e58b167ed0f5626c03bc3d772 --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error --dump-states-on-halt=false -exit-on-error-type=Assert --search=dfs --search=random-path -max-time=20 %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false -max-memory=6008 --optimize=true --skip-not-lazy-initialized -output-source=true --output-stats=false --output-istats=false --write-xml-tests --write-ktests=false --xml-metadata-programfile=wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c --xml-metadata-programhash=a18daeacf63b42ad6e1cb490555b7cdecd71ad6e58b167ed0f5626c03bc3d772 --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error --dump-states-on-halt=all -exit-on-error-type=Assert --search=dfs --search=random-path -max-time=20 %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s // RUN: test -f %t.klee-out/test000001.xml // RUN: not test -f %t.klee-out/test000001.ktest diff --git a/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c b/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c index 4341173c1d..fb8ace55c5 100644 --- a/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c +++ b/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3-tree --max-solvers-approx-tree-inc=16 --optimize-aggressive=false --track-coverage=branches -max-memory=6008 --optimize --skip-not-lazy-initialized -output-source=false --output-stats=false --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error -dump-states-on-halt=true -exit-on-error-type=Assert --search=dfs -max-instructions=6000 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3-tree --max-solvers-approx-tree-inc=16 --optimize-aggressive=false --track-coverage=branches -max-memory=6008 --optimize --skip-not-lazy-initialized -output-source=false --output-stats=false --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error -dump-states-on-halt=all -exit-on-error-type=Assert --search=dfs -max-instructions=6000 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s // CHECK-VERDICT: KLEE: done: total instructions = 6000 #include "klee-test-comp.c" diff --git a/test/Solver/sina2f.c b/test/Solver/sina2f.c index fb7179d785..628a8e0e8b 100644 --- a/test/Solver/sina2f.c +++ b/test/Solver/sina2f.c @@ -3,7 +3,7 @@ // REQUIRES: not-msan // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --strip-unwanted-calls --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=16 --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=false --output-istats=false --use-sym-size-alloc=true --cex-cache-validity-cores --fp-runtime --x86FP-as-x87FP80 --symbolic-allocation-threshold=8192 --allocate-determ --allocate-determ-size=3072 --allocate-determ-start-address=0x00030000000 --mem-trigger-cof --use-alpha-equivalence=true --track-coverage=all --use-iterative-deepening-search=max-cycles --max-solver-time=5s --max-cycles-before-stuck=15 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --cover-on-the-fly=true --delay-cover-on-the-fly=27 --max-time=29 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --strip-unwanted-calls --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=16 --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=false --output-istats=false --use-sym-size-alloc=true --cex-cache-validity-cores --fp-runtime --x86FP-as-x87FP80 --symbolic-allocation-threshold=8192 --allocate-determ --allocate-determ-size=3072 --allocate-determ-start-address=0x00030000000 --mem-trigger-cof --use-alpha-equivalence=true --track-coverage=all --use-iterative-deepening-search=max-cycles --max-solver-time=5s --max-cycles-before-stuck=15 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --cover-on-the-fly=true --delay-cover-on-the-fly=27 --max-time=29 %t1.bc 2>&1 | FileCheck %s #include "klee-test-comp.c" /* diff --git a/test/regression/2020-02-24-count-paths-nodump.c b/test/regression/2020-02-24-count-paths-nodump.c index c066886c20..83af8e919b 100644 --- a/test/regression/2020-02-24-count-paths-nodump.c +++ b/test/regression/2020-02-24-count-paths-nodump.c @@ -1,8 +1,8 @@ -// ASAN fails because KLEE does not cleanup states with -dump-states-on-halt=false +// ASAN fails because KLEE does not cleanup states with -dump-states-on-halt=none // REQUIRES: not-asan // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee -dump-states-on-halt=false -max-instructions=1 -output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s +// RUN: %klee -dump-states-on-halt=none -max-instructions=1 -output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s int main(int argc, char **argv) { // just do something diff --git a/test/regression/2023-10-06-Dubois-015.c b/test/regression/2023-10-06-Dubois-015.c index c782d694b5..a7917dc82d 100644 --- a/test/regression/2023-10-06-Dubois-015.c +++ b/test/regression/2023-10-06-Dubois-015.c @@ -1,6 +1,6 @@ // 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-aggressive=false --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s #include "klee-test-comp.c" diff --git a/test/regression/2023-10-13-kbfiltr.i.cil-2.c b/test/regression/2023-10-13-kbfiltr.i.cil-2.c index 57a75af0b9..f65ab2393b 100644 --- a/test/regression/2023-10-13-kbfiltr.i.cil-2.c +++ b/test/regression/2023-10-13-kbfiltr.i.cil-2.c @@ -1,6 +1,6 @@ // 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-aggressive=false --track-coverage=branches --optimize=true --mock-all-externals --external-calls=all --use-forked-solver=false --max-memory=6008 --skip-not-lazy-initialized --istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --write-kqueries --write-xml-tests --only-output-states-covering-new=true --dump-states-on-halt=true --emit-all-errors=true --search=bfs %t1.bc +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --mock-all-externals --external-calls=all --use-forked-solver=false --max-memory=6008 --skip-not-lazy-initialized --istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --write-kqueries --write-xml-tests --only-output-states-covering-new=true --dump-states-on-halt=all --emit-all-errors=true --search=bfs %t1.bc // RUN: ls %t.klee-out | grep _1.xml | wc -l | grep 8 #include "klee-test-comp.c" diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 766013544b..e0ec4b2092 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -369,6 +369,7 @@ cl::opt XMLMetadataProgramHash( namespace klee { extern cl::opt MaxTime; extern cl::opt FunctionCallReproduce; +extern cl::opt DumpStatesOnHalt; class ExecutionState; } // namespace klee @@ -586,7 +587,10 @@ void KleeHandler::processTestCase(const ExecutionState &state, unsigned id = ++m_numTotalTests; if (!WriteNone && (FunctionCallReproduce == "" || strcmp(suffix, "assert.err") == 0 || - strcmp(suffix, "reachable.err") == 0)) { + strcmp(suffix, "reachable.err") == 0 || + (DumpStatesOnHalt == HaltExecution::Reason::UnreachedTarget && + m_interpreter->getHaltExecution() == + HaltExecution::Reason::UnreachedTarget))) { KTest ktest; ktest.numArgs = m_argc; ktest.args = m_argv;