diff --git a/configs/options.json b/configs/options.json index 736bb70193..03a3849384 100644 --- a/configs/options.json +++ b/configs/options.json @@ -7,7 +7,11 @@ "maxSolverTime" : "5", "maxForks" : "200", "maxSymAlloc" : "32", - "symbolicAllocationThreshhold" : "2048" + "SymbolicAllocationThreshold" : "2048", + "minNumberElements" : "4", + "maxCycles" : 10, + "useSymbolicSizeLI" : false, + "writeKpaths": false }, "configurations": [ { @@ -33,10 +37,13 @@ "--extern-calls-can-return-null", "--align-symbolic-pointers=false", "--write-no-tests", - "--write-kpaths", + "--write-kpaths=${writeKpaths}", "--use-lazy-initialization=only", + "--min-number-elements-li=${minNumberElements}", + "--use-sym-size-li=${useSymbolicSizeLI}", + "--max-cycles=${maxCycles}", "--rewrite-equalities=simple", - "--symbolic-allocation-threshhold=${symbolicAllocationThreshhold}", + "--symbolic-allocation-threshold=${SymbolicAllocationThreshold}", "--analysis-reproduce=${sarifTracesFilePath}", "${bytecodeFilePath}" ] diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index e865de6a31..72132b109d 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -33,8 +33,9 @@ TTYPE(ReadOnly, 17U, "read_only.err") \ TTYPE(ReportError, 18U, "report_error.err") \ TTYPE(UndefinedBehavior, 19U, "undefined_behavior.err") \ - TTYPE(InternalOutOfMemory, 20U, "out_of_memory.er") \ - MARK(PROGERR, 20U) \ + TTYPE(InternalOutOfMemory, 20U, "out_of_memory.err") \ + TTYPE(MissedAllTargets, 21U, "miss_all_targets.err") \ + MARK(PROGERR, 21U) \ TTYPE(User, 23U, "user.err") \ MARK(USERERR, 23U) \ TTYPE(Execution, 25U, "exec.err") \ @@ -42,8 +43,7 @@ MARK(EXECERR, 26U) \ TTYPE(Replay, 27U, "") \ TTYPE(SilentExit, 28U, "") \ - TTYPE(MissedAllTargets, 29U, "") \ - MARK(END, 29U) + MARK(END, 28U) ///@brief Reason an ExecutionState got terminated. enum class StateTerminationType : std::uint8_t { @@ -61,6 +61,7 @@ enum Reason { MaxInstructions, MaxSteppedInstructions, MaxTime, + MaxCycles, CovCheck, NoMoreStates, ReachedTarget, diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h index f57e908d79..8ce01335f5 100644 --- a/include/klee/Expr/Expr.h +++ b/include/klee/Expr/Expr.h @@ -321,6 +321,9 @@ class Expr { /// isZero - Is this a constant zero. bool isZero() const; + /// isZero - Is this a constant one. + bool isOne() const; + /// isTrue - Is this the true expression. bool isTrue() const; @@ -1553,6 +1556,12 @@ inline bool Expr::isZero() const { return false; } +inline bool Expr::isOne() const { + if (const ConstantExpr *CE = dyn_cast(this)) + return CE->isOne(); + return false; +} + inline bool Expr::isTrue() const { assert(getWidth() == Expr::Bool && "Invalid isTrue() call!"); if (const ConstantExpr *CE = dyn_cast(this)) diff --git a/include/klee/Expr/ExprVisitor.h b/include/klee/Expr/ExprVisitor.h index 8808f63add..15c9741272 100644 --- a/include/klee/Expr/ExprVisitor.h +++ b/include/klee/Expr/ExprVisitor.h @@ -137,10 +137,9 @@ class ExprVisitor { virtual Action visitFNeg(const FNegExpr &); virtual Action visitFRint(const FRintExpr &); -protected: - VisitorHash visited; - private: + typedef ExprHashMap> visited_ty; + visited_ty visited; bool recursive; ref visitActual(const ref &e); diff --git a/include/klee/Module/TargetForest.h b/include/klee/Module/TargetForest.h index eac93e8ef4..8476e5aa61 100644 --- a/include/klee/Module/TargetForest.h +++ b/include/klee/Module/TargetForest.h @@ -218,12 +218,35 @@ class TargetForest { static EquivTargetsHistoryHashSet cachedHistories; static TargetsHistoryHashSet histories; unsigned hashValue; + unsigned sizeValue; explicit History(ref _target, ref _visitedTargets) : target(_target), visitedTargets(_visitedTargets) { computeHash(); } + void computeHash() { + unsigned res = 0; + if (target) { + res = target->hash() * Expr::MAGIC_HASH_CONSTANT; + } + if (visitedTargets) { + res ^= visitedTargets->hash() * Expr::MAGIC_HASH_CONSTANT; + } + hashValue = res; + } + + void computeSize() { + unsigned res = 0; + if (target) { + ++res; + } + if (visitedTargets) { + res += visitedTargets->size(); + } + sizeValue = res; + } + public: const ref target; const ref visitedTargets; @@ -238,21 +261,11 @@ class TargetForest { } unsigned hash() const { return hashValue; } + unsigned size() const { return sizeValue; } int compare(const History &h) const; bool equals(const History &h) const; - void computeHash() { - unsigned res = 0; - if (target) { - res = target->hash() * Expr::MAGIC_HASH_CONSTANT; - } - if (visitedTargets) { - res ^= visitedTargets->hash() * Expr::MAGIC_HASH_CONSTANT; - } - hashValue = res; - } - void dump() const; ~History(); diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h index b22aab4e93..7b8889dfd4 100644 --- a/include/klee/Solver/SolverCmdLine.h +++ b/include/klee/Solver/SolverCmdLine.h @@ -70,7 +70,7 @@ extern llvm::cl::opt DebugCrossCheckCoreSolverWith; extern llvm::cl::opt ProduceUnsatCore; -extern llvm::cl::opt SymbolicAllocationThreshhold; +extern llvm::cl::opt SymbolicAllocationThreshold; #ifdef ENABLE_METASMT diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 7612ead8f9..40820835fa 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -274,12 +274,8 @@ int AddressSpace::checkPointerInObject(ExecutionState &state, // mustBeTrue before mayBeTrue for the first result. easy // to add I just want to have a nice symbolic test case first. const MemoryObject *mo = op.first; - ref base = state.isGEPExpr(p) ? state.gepExprBases.at(p).first : p; ref inBounds = mo->getBoundsCheckPointer(p); - inBounds = AndExpr::create( - inBounds, - mo->getBoundsCheckPointer(base)); // FIXME: remove when segmented memory - // model will be implemented + bool mayBeTrue; if (!solver->mayBeTrue(state.constraints.cs(), inBounds, mayBeTrue, state.queryMetaData)) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2fd22d3e67..c2780d603d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -136,6 +136,9 @@ cl::OptionCategory SeedingCat( cl::OptionCategory TestGenCat("Test generation options", "These options impact test generation."); +cl::OptionCategory LazyInitCat("Lazy initialization option", + "These options configure lazy initialization."); + cl::opt TypeSystem("type-system", cl::desc("Use information about type system from specified " @@ -202,7 +205,20 @@ cl::opt LazyInitialization( "Only lazy initilization without resolving."), clEnumValN(LazyInitializationPolicy::All, "all", "Enable lazy initialization (default).")), - cl::init(LazyInitializationPolicy::All), cl::cat(ExecCat)); + cl::init(LazyInitializationPolicy::All), cl::cat(LazyInitCat)); + +llvm::cl::opt UseSymbolicSizeLazyInit( + "use-sym-size-li", + llvm::cl::desc( + "Allows lazy initialize symbolic size objects (default false)"), + llvm::cl::init(false), llvm::cl::cat(LazyInitCat)); + +llvm::cl::opt MinNumberElementsLazyInit( + "min-number-elements-li", + llvm::cl::desc("Minimum number of array elements for one lazy " + "initialization (default 4)"), + llvm::cl::init(4), llvm::cl::cat(LazyInitCat)); + } // namespace klee namespace { @@ -235,9 +251,9 @@ cl::opt MaxSymArraySize( cl::init(0), cl::cat(SolvingCat)); cl::opt - SimplifySymIndices("simplify-sym-indices", cl::init(false), + SimplifySymIndices("simplify-sym-indices", cl::init(true), cl::desc("Simplify symbolic accesses using equalities " - "from other constraints (default=false)"), + "from other constraints (default=true)"), cl::cat(SolvingCat)); cl::opt @@ -415,6 +431,7 @@ bool allLeafsAreConstant(const ref &expr) { extern llvm::cl::opt MaxConstantAllocationSize; extern llvm::cl::opt MaxSymbolicAllocationSize; +extern llvm::cl::opt UseSymbolicSizeAllocation; // XXX hack extern "C" unsigned dumpStates, dumpPForest; @@ -3127,7 +3144,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { offset = AddExpr::create(offset, Expr::createPointer(kgepi->offset)); ref address = AddExpr::create(base, offset); - if (!isa(address) || base->isZero()) { + if (!isa(address) || base->isZero() || + state.isGEPExpr(base)) { if (state.isGEPExpr(base)) { state.gepExprBases[address] = state.gepExprBases[base]; } else { @@ -4155,8 +4173,10 @@ void Executor::reportProgressTowardsTargets(std::string prefix, for (auto &p : distancesTowardsTargets) { auto target = p.first; auto distance = p.second; - klee_message("%s for %s", distance.toString().c_str(), - target->toString().c_str()); + klee_message("%s for %s (lines %d to %d)", distance.toString().c_str(), + target->toString().c_str(), + target->getBlock()->getFirstInstruction()->info->line, + target->getBlock()->getLastInstruction()->info->line); } } @@ -4203,10 +4223,16 @@ void Executor::run(std::vector initialStates) { } if (guidanceKind == GuidanceKind::ErrorGuidance) { + SetOfStates leftState = states; + for (auto state : pausedStates) { + leftState.erase(state); + } + reportProgressTowardsTargets(); - bool canReachNew1 = decreaseConfidenceFromStoppedStates(pausedStates); + bool canReachNew1 = decreaseConfidenceFromStoppedStates( + pausedStates, HaltExecution::MaxCycles); bool canReachNew2 = - decreaseConfidenceFromStoppedStates(states, haltExecution); + decreaseConfidenceFromStoppedStates(leftState, haltExecution); for (auto &startBlockAndWhiteList : targets) { startBlockAndWhiteList.second.reportFalsePositives(canReachNew1 || @@ -4319,14 +4345,20 @@ void Executor::targetedRun(ExecutionState &initialState, KBlock *target, } std::string Executor::getAddressInfo(ExecutionState &state, ref address, + unsigned size, const MemoryObject *mo) const { std::string Str; llvm::raw_string_ostream info(Str); + address = + Simplificator::simplifyExpr(state.constraints.cs(), address).simplified; info << "\taddress: " << address << "\n"; if (state.isGEPExpr(address)) { ref base = state.gepExprBases[address].first; info << "\tbase: " << base << "\n"; } + if (size) { + info << "\tsize: " << size << "\n"; + } uint64_t example; if (ConstantExpr *CE = dyn_cast(address)) { @@ -4906,6 +4938,11 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, if (allocationAlignment == 0) { allocationAlignment = getAllocationAlignment(allocSite); } + + if (!isa(size) && !UseSymbolicSizeAllocation) { + size = toConstant(state, size, "symbolic size allocation"); + } + ref upperBoundSizeConstraint = Expr::createTrue(); if (!isa(size)) { upperBoundSizeConstraint = UleExpr::create( @@ -5115,7 +5152,7 @@ bool Executor::computeSizes(ExecutionState &state, ref size, bool success = solver->getResponse( state.constraints.cs(), UgtExpr::create(symbolicSizesSum, - ConstantExpr::create(SymbolicAllocationThreshhold, + ConstantExpr::create(SymbolicAllocationThreshold, symbolicSizesSum->getWidth())), response, state.queryMetaData); solver->setTimeout(time::Span()); @@ -5300,14 +5337,11 @@ bool Executor::resolveMemoryObjects( // we are on an error path (no resolution, multiple resolution, one // resolution with out of bounds) - bool baseWasNotResolved = state.resolvedPointers.count(base) == 0; address = optimizer.optimizeExpr(address, true); ref checkOutOfBounds = Expr::createTrue(); - ref baseUniqueExpr = toUnique(state, base); - - bool checkAddress = isa(address) || isa(address) || - state.isGEPExpr(address); + bool checkAddress = + isa(address) || isa(address) || base != address; if (!checkAddress && isa(address)) { checkAddress = true; std::vector> alternatives; @@ -5320,8 +5354,7 @@ bool Executor::resolveMemoryObjects( } mayLazyInitialize = LazyInitialization != LazyInitializationPolicy::None && - !isa(baseUniqueExpr) && - baseWasNotResolved && checkAddress; + !isa(base); if (!onlyLazyInitialize || !mayLazyInitialize) { ResolutionList rl; @@ -5352,8 +5385,11 @@ bool Executor::resolveMemoryObjects( return false; } else if (mayLazyInitialize) { IDType idLazyInitialization; - if (!lazyInitializeObject(state, base, target, baseTargetType, size, - idLazyInitialization)) { + uint64_t minObjectSize = MinNumberElementsLazyInit * size; + if (!lazyInitializeObject(state, base, target, baseTargetType, + minObjectSize, false, idLazyInitialization, + /*state.isolated || UseSymbolicSizeLazyInit*/ + UseSymbolicSizeLazyInit)) { return false; } // Lazy initialization might fail if we've got unappropriate address @@ -5400,7 +5436,7 @@ bool Executor::checkResolvedMemoryObjects( ref baseInBounds = Expr::createTrue(); ref notInBounds = Expr::createIsZero(inBounds); - if (state.isGEPExpr(address)) { + if (base != address || size != bytes) { baseInBounds = AndExpr::create(baseInBounds, mo->getBoundsCheckPointer(base, size)); } @@ -5447,12 +5483,20 @@ bool Executor::checkResolvedMemoryObjects( } else { resolveConditions.push_back(inBounds); unboundConditions.push_back(notInBounds); + if (hasLazyInitialized /*&& !state.isolated*/) { + notInBounds = AndExpr::create( + notInBounds, Expr::createIsZero(mo->getOffsetExpr(base))); + } checkOutOfBounds = notInBounds; } } else if (mayBeOutOfBound) { if (mustBeOutOfBound) { checkOutOfBounds = Expr::createTrue(); } else { + if (hasLazyInitialized /*&& !state.isolated*/) { + notInBounds = AndExpr::create( + notInBounds, Expr::createIsZero(mo->getOffsetExpr(base))); + } checkOutOfBounds = notInBounds; } } @@ -5468,9 +5512,11 @@ bool Executor::checkResolvedMemoryObjects( ref baseInBounds = Expr::createTrue(); ref notInBounds = Expr::createIsZero(inBounds); - if (state.isGEPExpr(address)) { + if (base != address || size != bytes) { baseInBounds = AndExpr::create(baseInBounds, mo->getBoundsCheckPointer(base, size)); + baseInBounds = AndExpr::create( + baseInBounds, Expr::createIsZero(mo->getOffsetExpr(base))); } if (hasLazyInitialized && i == mayBeResolvedMemoryObjects.size() - 1) { @@ -5503,6 +5549,13 @@ bool Executor::checkResolvedMemoryObjects( resolveConditions.push_back(inBounds); resolvedMemoryObjects.push_back(mo->id); unboundConditions.push_back(notInBounds); + + if (hasLazyInitialized && + i == mayBeResolvedMemoryObjects.size() - 1 /*&& !state.isolated*/) { + notInBounds = AndExpr::create( + notInBounds, Expr::createIsZero(mo->getOffsetExpr(base))); + } + if (mayBeOutOfBound) { checkOutOfBounds = AndExpr::create(checkOutOfBounds, notInBounds); } @@ -5541,7 +5594,7 @@ bool Executor::makeGuard(ExecutionState &state, selectGuard = OrExpr::create(selectGuard, resolveConditions.at(i)); } if (hasLazyInitialized) { - ref head = resolveConditions.back(); + ref head = Expr::createIsZero(unboundConditions.back()); ref body = Expr::createTrue(); for (unsigned int j = 0; j < resolveConditions.size(); ++j) { if (resolveConditions.size() - 1 != j) { @@ -5613,18 +5666,14 @@ void Executor::collectReads( const MemoryObject *mo = op.first; const ObjectState *os = op.second; - ObjectState *wos = state.addressSpace.getWriteable(mo, os); - - wos->getDynamicType()->handleMemoryAccess( - targetType, mo->getOffsetExpr(address), - ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); - ref result = wos->read(mo->getOffsetExpr(address), type); + ref result = os->read(mo->getOffsetExpr(address), type); if (MockMutableGlobals != MockMutableGlobalsPolicy::None && mo->isGlobal && - !wos->readOnly && isa(result) && + !os->readOnly && isa(result) && (MockMutableGlobals != MockMutableGlobalsPolicy::PrimitiveFields || !targetType->getRawType()->isPointerTy())) { result = makeMockValue(state, "mockGlobalValue", result->getWidth()); + ObjectState *wos = state.addressSpace.getWriteable(mo, os); wos->write(mo->getOffsetExpr(address), result); } @@ -5654,12 +5703,24 @@ void Executor::executeMemoryOperation( } if (SimplifySymIndices) { - if (!isa(address)) + ref oldAddress = address; + ref oldbase = base; + if (!isa(address)) { address = Simplificator::simplifyExpr(estate.constraints.cs(), address) .simplified; - if (!isa(base)) + } + if (!isa(base)) { base = Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified; + } + if (!isa(address) || base->isZero()) { + if (estate.isGEPExpr(oldAddress)) { + estate.gepExprBases[address] = { + base, + estate.gepExprBases[oldAddress].second, + }; + } + } if (isWrite && !isa(value)) value = Simplificator::simplifyExpr(estate.constraints.cs(), value) .simplified; @@ -5668,9 +5729,7 @@ void Executor::executeMemoryOperation( address = optimizer.optimizeExpr(address, true); base = optimizer.optimizeExpr(base, true); - ref uniqueBase = - Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified; - uniqueBase = toUnique(estate, uniqueBase); + ref uniqueBase = toUnique(estate, base); StatePair branches = forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp); @@ -5695,7 +5754,7 @@ void Executor::executeMemoryOperation( state->resolvedPointers.at(base).size() == 1) { success = true; idFastResult = *state->resolvedPointers[base].begin(); - } else if (allLeafsAreConstant(address)) { + } else { solver->setTimeout(coreSolverTimeout); if (!state->addressSpace.resolveOne(*state, solver, address, targetType, @@ -5717,6 +5776,16 @@ void Executor::executeMemoryOperation( } ref inBounds = mo->getBoundsCheckPointer(address, bytes); + ref baseInBounds = Expr::createTrue(); + + if (base != address || size != bytes) { + baseInBounds = + AndExpr::create(baseInBounds, mo->getBoundsCheckPointer(base, size)); + baseInBounds = AndExpr::create( + baseInBounds, Expr::createIsZero(mo->getOffsetExpr(base))); + } + + inBounds = AndExpr::create(inBounds, baseInBounds); inBounds = optimizer.optimizeExpr(inBounds, true); inBounds = Simplificator::simplifyExpr(state->constraints.cs(), inBounds) @@ -5743,8 +5812,8 @@ void Executor::executeMemoryOperation( const ObjectState *os = op.second; state->addPointerResolution(base, mo); state->addPointerResolution(address, mo); - ObjectState *wos = state->addressSpace.getWriteable(mo, os); if (isWrite) { + ObjectState *wos = state->addressSpace.getWriteable(mo, os); wos->getDynamicType()->handleMemoryAccess( targetType, mo->getOffsetExpr(address), ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); @@ -5755,19 +5824,17 @@ void Executor::executeMemoryOperation( wos->write(mo->getOffsetExpr(address), value); } } else { - wos->getDynamicType()->handleMemoryAccess( - targetType, mo->getOffsetExpr(address), - ConstantExpr::alloc(size, Context::get().getPointerWidth()), false); - result = wos->read(mo->getOffsetExpr(address), type); + result = os->read(mo->getOffsetExpr(address), type); if (interpreterOpts.MakeConcreteSymbolic) result = replaceReadWithSymbolic(*state, result); if (MockMutableGlobals != MockMutableGlobalsPolicy::None && - mo->isGlobal && !wos->readOnly && isa(result) && + mo->isGlobal && !os->readOnly && isa(result) && (MockMutableGlobals != MockMutableGlobalsPolicy::PrimitiveFields || !targetType->getRawType()->isPointerTy())) { result = makeMockValue(*state, "mockGlobalValue", result->getWidth()); + ObjectState *wos = state->addressSpace.getWriteable(mo, os); wos->write(mo->getOffsetExpr(address), result); } @@ -5911,6 +5978,16 @@ void Executor::executeMemoryOperation( const MemoryObject *mo = op.first; const ObjectState *os = op.second; + if (hasLazyInitialized && i + 1 != resolvedMemoryObjects.size()) { + const MemoryObject *liMO = + bound->addressSpace + .findObject( + resolvedMemoryObjects[resolvedMemoryObjects.size() - 1]) + .first; + bound->removePointerResolutions(liMO); + bound->addressSpace.unbindObject(liMO); + } + bound->addUniquePointerResolution(address, mo); bound->addUniquePointerResolution(base, mo); @@ -5919,9 +5996,9 @@ void Executor::executeMemoryOperation( waste too much memory as we do now always modify something. To fix this we can ask memory if we will make anything, and create a copy if required. */ - ObjectState *wos = bound->addressSpace.getWriteable(mo, os); if (isWrite) { + ObjectState *wos = bound->addressSpace.getWriteable(mo, os); wos->getDynamicType()->handleMemoryAccess( targetType, mo->getOffsetExpr(address), ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); @@ -5932,16 +6009,14 @@ void Executor::executeMemoryOperation( wos->write(mo->getOffsetExpr(address), value); } } else { - wos->getDynamicType()->handleMemoryAccess( - targetType, mo->getOffsetExpr(address), - ConstantExpr::alloc(size, Context::get().getPointerWidth()), false); - ref result = wos->read(mo->getOffsetExpr(address), type); + ref result = os->read(mo->getOffsetExpr(address), type); if (MockMutableGlobals != MockMutableGlobalsPolicy::None && - mo->isGlobal && !wos->readOnly && isa(result) && + mo->isGlobal && !os->readOnly && isa(result) && (MockMutableGlobals != MockMutableGlobalsPolicy::PrimitiveFields || !targetType->getRawType()->isPointerTy())) { result = makeMockValue(*bound, "mockGlobalValue", result->getWidth()); + ObjectState *wos = bound->addressSpace.getWriteable(mo, os); wos->write(mo->getOffsetExpr(address), result); } @@ -5963,15 +6038,14 @@ void Executor::executeMemoryOperation( assert(mayBeOutOfBound && "must be true since unbound is not null"); terminateStateOnError(*unbound, "memory error: out of bound pointer", StateTerminationType::Ptr, - getAddressInfo(*unbound, address)); + getAddressInfo(*unbound, address, bytes)); } } bool Executor::lazyInitializeObject(ExecutionState &state, ref address, const KInstruction *target, KType *targetType, uint64_t size, - IDType &id, bool isConstantSize, - bool isLocal) { + bool isLocal, IDType &id, bool isSymbolic) { assert(!isa(address)); const llvm::Value *allocSite = target ? target->inst : nullptr; std::pair, ref> moBasePair; @@ -5981,7 +6055,7 @@ bool Executor::lazyInitializeObject(ExecutionState &state, ref address, } ref sizeExpr; - if (size <= MaxSymbolicAllocationSize && !isConstantSize) { + if (size < MaxSymbolicAllocationSize && !isLocal && isSymbolic) { const Array *lazyInstantiationSize = makeArray( Expr::createPointer(Context::get().getPointerWidth() / CHAR_BIT), SourceBuilder::lazyInitializationSize(address)); @@ -6007,9 +6081,11 @@ bool Executor::lazyInitializeObject(ExecutionState &state, ref address, sizeExpr = Expr::createPointer(size); } - MemoryObject *mo = allocate(state, sizeExpr, isLocal, - /*isGlobal=*/false, allocSite, - /*allocationAlignment=*/8, address, timestamp); + ref addressExpr = isSymbolic ? address : nullptr; + MemoryObject *mo = + allocate(state, sizeExpr, isLocal, + /*isGlobal=*/false, allocSite, + /*allocationAlignment=*/8, addressExpr, timestamp); if (!mo) { return false; } @@ -6032,6 +6108,8 @@ bool Executor::lazyInitializeObject(ExecutionState &state, ref address, if (!mayBeLazyInitialized) { id = 0; } else { + address = + Simplificator::simplifyExpr(state.constraints.cs(), address).simplified; executeMakeSymbolic(state, mo, targetType, SourceBuilder::lazyInitializationContent(address), isLocal); @@ -6059,7 +6137,8 @@ IDType Executor::lazyInitializeLocalObject(ExecutionState &state, IDType id; bool success = lazyInitializeObject( state, address, target, typeSystemManager->getWrappedType(ai->getType()), - elementSize, id, isa(size), true); + elementSize, true, id, + /*state.isolated || UseSymbolicSizeLazyInit*/ UseSymbolicSizeLazyInit); assert(success); assert(id); auto op = state.addressSpace.findObject(id); @@ -6597,18 +6676,24 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res, void Executor::logState(const ExecutionState &state, int id, std::unique_ptr &f) { *f << "State number " << state.id << ". Test number: " << id << "\n\n"; + for (auto &object : state.addressSpace.objects) { + *f << "ID memory object: " << object.first->id << "\n"; + *f << "Address memory object: " << object.first->address << "\n"; + *f << "Memory object size: " << object.first->size << "\n"; + } *f << state.symbolics.size() << " symbolics total. " << "Symbolics:\n"; size_t sc = 0; - for (auto &i : state.symbolics) { + for (auto &symbolic : state.symbolics) { *f << "Symbolic number " << sc++ << "\n"; - *f << "Associated memory object: " << i.memoryObject.get()->id << "\n"; - *f << "Memory object size: " << i.memoryObject.get()->size << "\n"; + *f << "Associated memory object: " << symbolic.memoryObject.get()->id + << "\n"; + *f << "Memory object size: " << symbolic.memoryObject.get()->size << "\n"; } *f << "\n"; *f << "State constraints:\n"; - for (auto i : state.constraints.cs().cs()) { - i->print(*f); + for (auto constraint : state.constraints.cs().cs()) { + constraint->print(*f); *f << "\n"; } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 0fe7a1f0d7..ac9165f9f4 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -397,8 +397,8 @@ class Executor : public Interpreter { bool lazyInitializeObject(ExecutionState &state, ref address, const KInstruction *target, KType *targetType, - uint64_t size, IDType &id, - bool isConstantSize = false, bool isLocal = false); + uint64_t size, bool isLocal, IDType &id, + bool isConstant = true); IDType lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf, ref address, @@ -547,6 +547,7 @@ class Executor : public Interpreter { /// Get textual information regarding a memory address. std::string getAddressInfo(ExecutionState &state, ref address, + unsigned size = 0, const MemoryObject *mo = nullptr) const; // Determines the \param lastInstruction of the \param state which is not KLEE diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index bbc314e982..8a1997dc9a 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -155,17 +155,18 @@ class MemoryObject { ref isZeroSizeExpr = EqExpr::create(Expr::createPointer(0), getSizeExpr()); ref isZeroOffsetExpr = EqExpr::create(Expr::createPointer(0), offset); - /* Check for zero size with zero offset. Useful for free of malloc(0) */ - ref andZeroExpr = AndExpr::create(isZeroSizeExpr, isZeroOffsetExpr); - return OrExpr::create(UltExpr::create(offset, getSizeExpr()), andZeroExpr); + return SelectExpr::create(isZeroSizeExpr, isZeroOffsetExpr, + UltExpr::create(offset, getSizeExpr())); } ref getBoundsCheckOffset(ref offset, unsigned bytes) const { ref offsetSizeCheck = UleExpr::create(Expr::createPointer(bytes), getSizeExpr()); - ref writeInSizeCheck = UleExpr::create( - offset, SubExpr::create(getSizeExpr(), Expr::createPointer(bytes))); - return AndExpr::create(offsetSizeCheck, writeInSizeCheck); + ref trueExpr = UltExpr::create( + offset, AddExpr::create( + SubExpr::create(getSizeExpr(), Expr::createPointer(bytes)), + Expr::createPointer(1))); + return SelectExpr::create(offsetSizeCheck, trueExpr, Expr::createFalse()); } /// Compare this object with memory object b. diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp index 6d601ce3e2..f0dc22287c 100644 --- a/lib/Core/MemoryManager.cpp +++ b/lib/Core/MemoryManager.cpp @@ -72,6 +72,11 @@ llvm::cl::opt MaxSymbolicAllocationSize( "Maximum available size for single allocation (default 10Mb)"), llvm::cl::init(10ll << 20), llvm::cl::cat(MemoryCat)); +llvm::cl::opt UseSymbolicSizeAllocation( + "use-sym-size-alloc", + llvm::cl::desc("Allows symbolic size allocation (default false)"), + llvm::cl::init(false), llvm::cl::cat(MemoryCat)); + /***/ MemoryManager::MemoryManager(ArrayCache *_arrayCache) : arrayCache(_arrayCache), deterministicSpace(0), nextFreeSlot(0), diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 4302977607..2951b62dd8 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -161,7 +161,6 @@ class GuidedSearcher final : public Searcher { using TargetToStateUnorderedSetMap = TargetHashMap>; -private: using TargetToSearcherMap = TargetHashMap>; using TargetToStateSetMap = TargetHashMap>; @@ -189,6 +188,7 @@ class GuidedSearcher final : public Searcher { using TargetForestHisoryTargetVector = std::vector, ref>>; +private: enum Guidance { CoverageGuidance, ErrorGuidance }; Guidance guidance; diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index 3cf9cd1810..2aa1d615ee 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -248,6 +248,9 @@ getAdviseWhatToIncreaseConfidenceRate(HaltExecution::Reason reason) { case HaltExecution::MaxSteppedInstructions: what = MaxSteppedInstructions.ArgStr.str(); break; + case HaltExecution::MaxCycles: + what = "max-cycles"; // TODO: taken from UserSearcher.cpp + break; case HaltExecution::CovCheck: what = "cov-check"; // TODO: taken from StatsTracker.cpp break; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 88f0e137a8..a52db8dd2d 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -104,44 +104,6 @@ class ExprReplaceVisitor2 : public ExprVisitor { return Action::doChildren(); } - std::pair processUpdateList(const UpdateList &updates) { - UpdateList newUpdates = UpdateList(updates.root, 0); - std::stack> forward; - - for (auto it = updates.head; !it.isNull(); it = it->next) { - forward.push(it); - } - - bool changed = false; - while (!forward.empty()) { - ref UNode = forward.top(); - forward.pop(); - ref newIndex = visit(UNode->index); - ref newValue = visit(UNode->value); - if (newIndex != UNode->index || newValue != UNode->value) { - changed = true; - } - newUpdates.extend(newIndex, newValue); - } - return {newUpdates, changed}; - } - - Action visitRead(const ReadExpr &re) override { - auto updates = processUpdateList(re.updates); - - ref index = visit(re.index); - if (!updates.second && index == re.index) { - return Action::skipChildren(); - } else { - ref reres = ReadExpr::create(updates.first, index); - Action res = visitExprPost(*reres.get()); - if (res.kind == Action::ChangeTo) { - reres = res.argument; - } - return Action::changeTo(reres); - } - } - Action visitSelect(const SelectExpr &sexpr) override { auto cond = visit(sexpr.cond); if (auto CE = dyn_cast(cond)) { diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 5b8bed1008..348034153d 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -1605,6 +1605,8 @@ ref SelectExpr::create(ref c, ref t, ref f) { AndExpr::create(Expr::createIsZero(c), se->cond), se->trueExpr, t); } } + } else if (!isa(t) && isa(f)) { + return SelectExpr::alloc(Expr::createIsZero(c), f, t); } return SelectExpr::alloc(c, t, f); @@ -1622,6 +1624,21 @@ ref ConcatExpr::create(const ref &l, const ref &r) { if (ConstantExpr *rCE = dyn_cast(r)) return lCE->Concat(rCE); + if (isa(l) || isa(r)) { + if (SelectExpr *se = dyn_cast(l)) { + if (isa(se->trueExpr)) { + return SelectExpr::create(se->cond, ConcatExpr::create(se->trueExpr, r), + ConcatExpr::create(se->falseExpr, r)); + } + } + if (SelectExpr *se = dyn_cast(r)) { + if (isa(se->trueExpr)) { + return SelectExpr::create(se->cond, ConcatExpr::create(l, se->trueExpr), + ConcatExpr::create(l, se->falseExpr)); + } + } + } + // Merge contiguous Extracts if (ExtractExpr *ee_left = dyn_cast(l)) { if (ExtractExpr *ee_right = dyn_cast(r)) { @@ -1678,6 +1695,12 @@ ref ExtractExpr::create(ref expr, unsigned off, Width w) { return expr; } else if (ConstantExpr *CE = dyn_cast(expr)) { return CE->Extract(off, w); + } else if (SelectExpr *se = dyn_cast(expr)) { + if (isa(se->trueExpr)) { + return SelectExpr::create(se->cond, + ExtractExpr::create(se->trueExpr, off, w), + ExtractExpr::create(se->falseExpr, off, w)); + } } else { // Extract(Concat) if (ConcatExpr *ce = dyn_cast(expr)) { @@ -1722,6 +1745,11 @@ ref NotExpr::create(const ref &e) { NotExpr::create(OE->right)); } + if (SelectExpr *SE = dyn_cast(e)) { + return SelectExpr::create(SE->cond, NotExpr::create(SE->trueExpr), + NotExpr::create(SE->falseExpr)); + } + return NotExpr::alloc(e); } @@ -1735,9 +1763,14 @@ ref ZExtExpr::create(const ref &e, Width w) { return ExtractExpr::create(e, 0, w); } else if (ConstantExpr *CE = dyn_cast(e)) { return CE->ZExt(w); - } else { - return ZExtExpr::alloc(e, w); + } else if (SelectExpr *se = dyn_cast(e)) { + if (isa(se->trueExpr)) { + return SelectExpr::create(se->cond, ZExtExpr::create(se->trueExpr, w), + ZExtExpr::create(se->falseExpr, w)); + } } + + return ZExtExpr::alloc(e, w); } ref SExtExpr::create(const ref &e, Width w) { @@ -1748,9 +1781,14 @@ ref SExtExpr::create(const ref &e, Width w) { return ExtractExpr::create(e, 0, w); } else if (ConstantExpr *CE = dyn_cast(e)) { return CE->SExt(w); - } else { - return SExtExpr::alloc(e, w); + } else if (SelectExpr *se = dyn_cast(e)) { + if (isa(se->trueExpr)) { + return SelectExpr::create(se->cond, SExtExpr::create(se->trueExpr, w), + SExtExpr::create(se->falseExpr, w)); + } } + + return SExtExpr::alloc(e, w); } /***/ @@ -1839,10 +1877,6 @@ static ref AddExpr_createPartialR(const ref &cl, Expr *r) { } else if (rk == Expr::Sub && isa(r->getKid(0))) { // A + (B-c) == (A+B) - c return SubExpr::create(AddExpr::create(cl, r->getKid(0)), r->getKid(1)); - } else if (rk == Expr::Select) { - SelectExpr *se = cast(r); - return SelectExpr::create(se->cond, AddExpr::create(cl, se->trueExpr), - AddExpr::create(cl, se->falseExpr)); } else { return AddExpr::alloc(cl, r); } @@ -2058,6 +2092,18 @@ static ref AShrExpr_create(const ref &l, const ref &r) { #define BCREATE_R(_e_op, _op, partialL, partialR) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth() == r->getWidth() && "type mismatch"); \ + if (SelectExpr *sel = dyn_cast(l)) { \ + if (isa(sel->trueExpr)) { \ + return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r), \ + _e_op::create(sel->falseExpr, r)); \ + } \ + } \ + if (SelectExpr *ser = dyn_cast(r)) { \ + if (isa(ser->trueExpr)) { \ + return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr), \ + _e_op::create(l, ser->falseExpr)); \ + } \ + } \ if (ConstantExpr *cl = dyn_cast(l)) { \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ @@ -2071,6 +2117,18 @@ static ref AShrExpr_create(const ref &l, const ref &r) { #define BCREATE(_e_op, _op) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth() == r->getWidth() && "type mismatch"); \ + if (SelectExpr *sel = dyn_cast(l)) { \ + if (isa(sel->trueExpr)) { \ + return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r), \ + _e_op::create(sel->falseExpr, r)); \ + } \ + } \ + if (SelectExpr *ser = dyn_cast(r)) { \ + if (isa(ser->trueExpr)) { \ + return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr), \ + _e_op::create(l, ser->falseExpr)); \ + } \ + } \ if (ConstantExpr *cl = dyn_cast(l)) \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ @@ -2094,6 +2152,18 @@ BCREATE(AShrExpr, AShr) #define CMPCREATE(_e_op, _op) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth() == r->getWidth() && "type mismatch"); \ + if (SelectExpr *sel = dyn_cast(l)) { \ + if (isa(sel->trueExpr)) { \ + return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r), \ + _e_op::create(sel->falseExpr, r)); \ + } \ + } \ + if (SelectExpr *ser = dyn_cast(r)) { \ + if (isa(ser->trueExpr)) { \ + return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr), \ + _e_op::create(l, ser->falseExpr)); \ + } \ + } \ if (ConstantExpr *cl = dyn_cast(l)) \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ @@ -2103,15 +2173,26 @@ BCREATE(AShrExpr, AShr) #define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth() == r->getWidth() && "type mismatch"); \ + if (SelectExpr *sel = dyn_cast(l)) { \ + if (isa(sel->trueExpr)) { \ + return SelectExpr::create(sel->cond, _e_op::create(sel->trueExpr, r), \ + _e_op::create(sel->falseExpr, r)); \ + } \ + } \ + if (SelectExpr *ser = dyn_cast(r)) { \ + if (isa(ser->trueExpr)) { \ + return SelectExpr::create(ser->cond, _e_op::create(l, ser->trueExpr), \ + _e_op::create(l, ser->falseExpr)); \ + } \ + } \ if (ConstantExpr *cl = dyn_cast(l)) { \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ return partialR(cl, r.get()); \ } else if (ConstantExpr *cr = dyn_cast(r)) { \ return partialL(l.get(), cr); \ - } else { \ - return _e_op##_create(l.get(), r.get()); \ } \ + return _e_op##_create(l.get(), r.get()); \ } static ref EqExpr_create(const ref &l, const ref &r) { @@ -2150,12 +2231,16 @@ static ref EqExpr_create(const ref &l, const ref &r) { } } else if (isa(l) || isa(r)) { if (SelectExpr *se = dyn_cast(l)) { - return SelectExpr::create(se->cond, EqExpr::create(se->trueExpr, r), - EqExpr::create(se->falseExpr, r)); + if (isa(se->trueExpr)) { + return SelectExpr::create(se->cond, EqExpr::create(se->trueExpr, r), + EqExpr::create(se->falseExpr, r)); + } } if (SelectExpr *se = dyn_cast(r)) { - return SelectExpr::create(se->cond, EqExpr::create(se->trueExpr, l), - EqExpr::create(se->falseExpr, l)); + if (isa(se->trueExpr)) { + return SelectExpr::create(se->cond, EqExpr::create(l, se->trueExpr), + EqExpr::create(l, se->falseExpr)); + } } } @@ -2299,6 +2384,10 @@ static ref UltExpr_create(const ref &l, const ref &r) { Expr::Width t = l->getWidth(); if (t == Expr::Bool) { // !l && r return AndExpr::create(Expr::createIsZero(l), r); + } else if (r->isOne()) { + return EqExpr::create(l, ConstantExpr::create(0, t)); + } else if (r->isZero()) { + return Expr::createFalse(); } else { return UltExpr::alloc(l, r); } @@ -2309,9 +2398,9 @@ static ref UleExpr_create(const ref &l, const ref &r) { return OrExpr::create(Expr::createIsZero(l), r); } else if (r->isZero()) { return EqExpr::create(l, r); + } else { + return UleExpr::alloc(l, r); } - - return UleExpr::alloc(l, r); } static ref SltExpr_create(const ref &l, const ref &r) { diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index bf222af763..b8fc326ef1 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -595,10 +595,11 @@ void ExprPPrinter::printQuery( } } + PC.breakLine(); PC << "(query ["; // Ident at constraint list; - unsigned indent = PC.pos; + unsigned indent = PC.pos - 1; for (auto it = constraints.cs().begin(), ie = constraints.cs().end(); it != ie;) { p.print(*it, PC); @@ -608,12 +609,12 @@ void ExprPPrinter::printQuery( } PC << ']'; - p.printSeparator(PC, constraints.cs().empty(), indent - 1); + p.printSeparator(PC, constraints.cs().empty(), indent); p.print(q, PC); // Print expressions to obtain values for, if any. if (evalExprsBegin != evalExprsEnd) { - p.printSeparator(PC, q->isFalse(), indent - 1); + p.printSeparator(PC, q->isFalse(), indent); PC << '['; for (const ref *it = evalExprsBegin; it != evalExprsEnd; ++it) { p.print(*it, PC, /*printConstWidth*/ true); @@ -628,7 +629,7 @@ void ExprPPrinter::printQuery( if (evalExprsBegin == evalExprsEnd) PC << " []"; - PC.breakLine(indent - 1); + PC.breakLine(indent); PC << '['; for (const Array *const *it = evalArraysBegin; it != evalArraysEnd; ++it) { PC << (*it)->getIdentifier(); diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp index 0cc373e668..6d2e509f33 100644 --- a/lib/Expr/ExprVisitor.cpp +++ b/lib/Expr/ExprVisitor.cpp @@ -27,12 +27,13 @@ ref ExprVisitor::visit(const ref &e) { if (!UseVisitorHash || isa(e)) { return visitActual(e); } else { - auto cached = visited.get(e); - if (cached.second) { - return cached.first; + visited_ty::iterator it = visited.find(e); + + if (it != visited.end()) { + return it->second; } else { - auto res = visitActual(cached.first); - visited.add({e, res}); + ref res = visitActual(e); + visited.insert(std::make_pair(e, res)); return res; } } diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index b87e3e0ec2..03549daea7 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -728,8 +728,6 @@ std::string KBlock::getLabel() const { std::string _label; llvm::raw_string_ostream label_stream(_label); basicBlock->printAsOperand(label_stream, false); - label_stream << " (lines " << getFirstInstruction()->info->line << " to " - << getLastInstruction()->info->line << ")"; std::string label = label_stream.str(); return label; } diff --git a/lib/Runner/run_klee.cpp b/lib/Runner/run_klee.cpp index 6637bc2512..f5bfd1a9ea 100644 --- a/lib/Runner/run_klee.cpp +++ b/lib/Runner/run_klee.cpp @@ -542,6 +542,7 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id) { void KleeHandler::processTestCase(const ExecutionState &state, const char *errorMessage, const char *errorSuffix) { + unsigned id = ++m_numTotalTests; if (!WriteNone) { KTest ktest; ktest.numArgs = m_argc; @@ -556,8 +557,6 @@ void KleeHandler::processTestCase(const ExecutionState &state, const auto start_time = time::getWallTime(); - unsigned id = ++m_numTotalTests; - if (success) { if (!kTest_toFile( &ktest, @@ -597,32 +596,6 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } - if (errorMessage || WriteKQueries) { - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::KQUERY); - auto f = openTestFile("kquery", id); - if (f) - *f << constraints; - } - - if (WriteCVCs) { - // FIXME: If using Z3 as the core solver the emitted file is actually - // SMT-LIBv2 not CVC which is a bit confusing - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); - auto f = openTestFile("cvc", id); - if (f) - *f << constraints; - } - - if (WriteSMT2s) { - std::string constraints; - m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); - auto f = openTestFile("smt2", id); - if (f) - *f << constraints; - } - if (m_symPathWriter) { std::vector symbolicBranches; m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state), @@ -635,27 +608,6 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } - if (WriteKPaths) { - std::string blockPath; - m_interpreter->getBlockPath(state, blockPath); - auto f = openTestFile("kpath", id); - if (f) - *f << blockPath; - } - - if (WriteCov) { - std::map> cov; - m_interpreter->getCoveredLines(state, cov); - auto f = openTestFile("cov", id); - if (f) { - for (const auto &entry : cov) { - for (const auto &line : entry.second) { - *f << *entry.first << ':' << line << '\n'; - } - } - } - } - if (m_numGeneratedTests == MaxTests) m_interpreter->setHaltExecution(HaltExecution::MaxTests); @@ -667,6 +619,53 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } // if (!WriteNone) + if (WriteKQueries) { + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::KQUERY); + auto f = openTestFile("kquery", id); + if (f) + *f << constraints; + } + + if (WriteCVCs) { + // FIXME: If using Z3 as the core solver the emitted file is actually + // SMT-LIBv2 not CVC which is a bit confusing + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); + auto f = openTestFile("cvc", id); + if (f) + *f << constraints; + } + + if (WriteSMT2s) { + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); + auto f = openTestFile("smt2", id); + if (f) + *f << constraints; + } + + if (WriteKPaths) { + std::string blockPath; + m_interpreter->getBlockPath(state, blockPath); + auto f = openTestFile("kpath", id); + if (f) + *f << blockPath; + } + + if (WriteCov) { + std::map> cov; + m_interpreter->getCoveredLines(state, cov); + auto f = openTestFile("cov", id); + if (f) { + for (const auto &entry : cov) { + for (const auto &line : entry.second) { + *f << *entry.first << ':' << line << '\n'; + } + } + } + } + if (errorMessage && OptExitOnError) { m_interpreter->prepareForEarlyExit(); klee_error("EXITING ON ERROR:\n%s\n", errorMessage); diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index b7f2b93404..f48cb2c1f7 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -253,7 +253,7 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, Query(queryConstraints, UgtExpr::create( symbolicSizesSum, - ConstantExpr::create(SymbolicAllocationThreshhold, + ConstantExpr::create(SymbolicAllocationThreshold, symbolicSizesSum->getWidth()))), response)) { return false; diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index fad32223ae..f1a66b20be 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -220,8 +220,8 @@ llvm::cl::opt llvm::cl::desc("Produce unsat core (default=true)."), llvm::cl::cat(klee::SolvingCat)); -llvm::cl::opt SymbolicAllocationThreshhold( - "symbolic-allocation-threshhold", +llvm::cl::opt SymbolicAllocationThreshold( + "symbolic-allocation-threshold", llvm::cl::desc("Maximum possible sum of sizes for all symbolic allocation " "before minimazation (default 1Kb)"), llvm::cl::init(1024), llvm::cl::cat(klee::SolvingCat)); diff --git a/runtime/klee-libc/strcmp.c b/runtime/klee-libc/strcmp.c index cdb002c739..2a81fe9f21 100644 --- a/runtime/klee-libc/strcmp.c +++ b/runtime/klee-libc/strcmp.c @@ -10,5 +10,5 @@ int strcmp(const char *a, const char *b) { while (*a && *a == *b) ++a, ++b; - return *a - *b; + return *(const unsigned char *)a - *(const unsigned char *)b; } diff --git a/test/Feature/BlockPath.ll b/test/Feature/BlockPath.ll new file mode 100644 index 0000000000..b46b04e96f --- /dev/null +++ b/test/Feature/BlockPath.ll @@ -0,0 +1,82 @@ +; REQUIRES: geq-llvm-12.0 +; RUN: %llvmas %s -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out --libc=klee --write-kpaths %t1.bc +; RUN: grep "(path: 0 (main: %0 %5 %6 %8 (abs: %1 %8 %11 %13) %8 %10 %16 %17 %19" %t.klee-out/test000001.kpath +; RUN: grep "(path: 0 (main: %0 %5 %6 %8 (abs: %1 %6 %11 %13) %8 %10 %16 %17 %19" %t.klee-out/test000002.kpath + +@.str = private unnamed_addr constant [2 x i8] c"x\00", align 1 + +define i32 @abs(i32 %0) { + %2 = alloca i32, align 4 + %3 = alloca i32, align 4 + store i32 %0, i32* %3, align 4 + %4 = load i32, i32* %3, align 4 + %5 = icmp sge i32 %4, 0 + br i1 %5, label %6, label %8 + +6: ; preds = %1 + %7 = load i32, i32* %3, align 4 + store i32 %7, i32* %2, align 4 + br label %11 + +8: ; preds = %1 + %9 = load i32, i32* %3, align 4 + %10 = sub nsw i32 0, %9 + store i32 %10, i32* %2, align 4 + br label %11 + +11: ; preds = %8, %6 + %12 = load i32, i32* %2, align 4 + br label %13 + +13: ; preds = %11 + ret i32 %12 +} + +define i32 @main() { + %1 = alloca i32, align 4 + %2 = alloca i32, align 4 + %3 = alloca i32, align 4 + store i32 0, i32* %1, align 4 + %4 = bitcast i32* %2 to i8* + br label %5 + +5: ; preds = %0 + call void @klee_make_symbolic(i8* %4, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0)) + br label %6 + +6: ; preds = %5 + %7 = load i32, i32* %2, align 4 + br label %8 + +8: ; preds = %6 + %9 = call i32 @abs(i32 %7) #4 + br label %10 + +10: ; preds = %8 + store i32 %9, i32* %3, align 4 + %11 = load i32, i32* %3, align 4 + %12 = icmp ne i32 %11, -2147483648 + %13 = load i32, i32* %3, align 4 + %14 = icmp slt i32 %13, 0 + %or.cond = select i1 %12, i1 %14, i1 false + br i1 %or.cond, label %15, label %16 + +15: ; preds = %10 + store i32 1, i32* %1, align 4 + br label %17 + +16: ; preds = %10 + store i32 0, i32* %1, align 4 + br label %17 + +17: ; preds = %16, %15 + %18 = load i32, i32* %1, align 4 + br label %19 + +19: ; preds = %17 + ret i32 %18 +} + +declare void @klee_make_symbolic(i8*, i64, i8*) diff --git a/test/Feature/LazyInitialization/ImpossibleAddressForLI.c b/test/Feature/LazyInitialization/ImpossibleAddressForLI.c index 9dd2a4b80a..abc643eb05 100644 --- a/test/Feature/LazyInitialization/ImpossibleAddressForLI.c +++ b/test/Feature/LazyInitialization/ImpossibleAddressForLI.c @@ -17,4 +17,4 @@ int main() { } // CHECK: KLEE: done: completed paths = 1 -// CHECK: KLEE: done: generated tests = 4 +// CHECK: KLEE: done: generated tests = 3 diff --git a/test/Feature/LazyInitialization/SingleInitializationAndAccess.c b/test/Feature/LazyInitialization/SingleInitializationAndAccess.c index 172e9850b9..1def3a9876 100644 --- a/test/Feature/LazyInitialization/SingleInitializationAndAccess.c +++ b/test/Feature/LazyInitialization/SingleInitializationAndAccess.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --skip-local=false %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --skip-local=false --use-sym-size-li --min-number-elements-li=1 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include @@ -9,11 +9,9 @@ int main() { int *x; klee_make_symbolic(&x, sizeof(x), "*x"); - // CHECK: SingleInitializationAndAccess.c:[[@LINE+2]]: memory error: null pointer exception - // CHECK: SingleInitializationAndAccess.c:[[@LINE+1]]: memory error: out of bound pointer + // CHECK: SingleInitializationAndAccess.c:[[@LINE+1]]: memory error: null pointer exception *x = 10; - // CHECK-NOT: SingleInitializationAndAccess.c:[[@LINE+2]]: memory error: null pointer exception - // CHECK: SingleInitializationAndAccess.c:[[@LINE+1]]: memory error: out of bound pointer + // CHECK-NOT: SingleInitializationAndAccess.c:[[@LINE+1]]: memory error: null pointer exception if (*x == 10) { // CHECK-NOT: SingleInitializationAndAccess.c:[[@LINE+2]]: memory error: null pointer exception // CHECK-NOT: SingleInitializationAndAccess.c:[[@LINE+1]]: memory error: out of bound pointer @@ -28,4 +26,4 @@ int main() { } // CHECK: KLEE: done: completed paths = 1 -// CHECK: KLEE: done: generated tests = 5 +// CHECK: KLEE: done: generated tests = 4 diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index 640850d2aa..f0522c4da8 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -7,13 +7,13 @@ // RUN: %clang -emit-llvm -DLITTLE_ALLOC -g -c %s -o %t.little.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log +// RUN: %klee --output-dir=%t.klee-out --max-memory=20 --max-cycles=0 %t.little.bc > %t.little.log // RUN: FileCheck -check-prefix=CHECK-LITTLE -input-file=%t.little.log %s // RUN: FileCheck -check-prefix=CHECK-WRN -input-file=%t.klee-out/warnings.txt %s // RUN: %clang -emit-llvm -g -c %s -o %t.big.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log 2> %t.big.err +// RUN: %klee --output-dir=%t.klee-out --max-memory=20 --max-cycles=0 %t.big.bc > %t.big.log 2> %t.big.err // RUN: FileCheck -check-prefix=CHECK-BIG -input-file=%t.big.log %s // RUN: FileCheck -check-prefix=CHECK-WRN -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Feature/SymbolicSizes/FirstAndLastElements.c b/test/Feature/SymbolicSizes/FirstAndLastElements.c index 800af271e4..da74d0569b 100644 --- a/test/Feature/SymbolicSizes/FirstAndLastElements.c +++ b/test/Feature/SymbolicSizes/FirstAndLastElements.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-sym-size-alloc --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c index 56ff1843e5..604d137360 100644 --- a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c +++ b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c b/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c index 974623d058..0ca567204c 100644 --- a/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c +++ b/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --check-out-of-memory --output-dir=%t.klee-out --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/IntArray.c b/test/Feature/SymbolicSizes/IntArray.c index c709975480..e820df0a04 100644 --- a/test/Feature/SymbolicSizes/IntArray.c +++ b/test/Feature/SymbolicSizes/IntArray.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --use-sym-size-alloc --use-sym-size-li --min-number-elements-li=1 --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/LazyInstantiationOfSymbolicSize.c b/test/Feature/SymbolicSizes/LazyInstantiationOfSymbolicSize.c index d027d2adf6..51ad20892e 100644 --- a/test/Feature/SymbolicSizes/LazyInstantiationOfSymbolicSize.c +++ b/test/Feature/SymbolicSizes/LazyInstantiationOfSymbolicSize.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --use-sym-size-alloc --use-sym-size-li --min-number-elements-li=1 --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include @@ -21,4 +21,4 @@ int main() { } // CHECK: KLEE: done: completed paths = 1 -// CHECK: KLEE: done: generated tests = 5 +// CHECK: KLEE: done: generated tests = 4 diff --git a/test/Feature/SymbolicSizes/LowerOutOfBound.c b/test/Feature/SymbolicSizes/LowerOutOfBound.c index 80634e364f..0a97e5c63a 100644 --- a/test/Feature/SymbolicSizes/LowerOutOfBound.c +++ b/test/Feature/SymbolicSizes/LowerOutOfBound.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --use-sym-size-alloc %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/MinimizeSize.c b/test/Feature/SymbolicSizes/MinimizeSize.c index a67bca1cb6..5da9f65c0f 100644 --- a/test/Feature/SymbolicSizes/MinimizeSize.c +++ b/test/Feature/SymbolicSizes/MinimizeSize.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-sym-size-alloc --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/MultipleAllocations.c b/test/Feature/SymbolicSizes/MultipleAllocations.c index 69d9633abf..4ef3193a47 100644 --- a/test/Feature/SymbolicSizes/MultipleAllocations.c +++ b/test/Feature/SymbolicSizes/MultipleAllocations.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/NegativeIndexArray.c b/test/Feature/SymbolicSizes/NegativeIndexArray.c index 37c413bd51..2d4e0a6368 100644 --- a/test/Feature/SymbolicSizes/NegativeIndexArray.c +++ b/test/Feature/SymbolicSizes/NegativeIndexArray.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-sym-size-alloc --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include "stdlib.h" diff --git a/test/Feature/SymbolicSizes/NegativeSize.c b/test/Feature/SymbolicSizes/NegativeSize.c index ea8ab6d955..72c0b9c4c7 100644 --- a/test/Feature/SymbolicSizes/NegativeSize.c +++ b/test/Feature/SymbolicSizes/NegativeSize.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c b/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c index 83c52cab06..7d3bab5940 100644 --- a/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c +++ b/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --use-sym-size-alloc --solver-backend=z3 --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/SegmentComparator.c b/test/Feature/SymbolicSizes/SegmentComparator.c index f2cc574c23..3a7f16db76 100644 --- a/test/Feature/SymbolicSizes/SegmentComparator.c +++ b/test/Feature/SymbolicSizes/SegmentComparator.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --use-sym-size-alloc --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c b/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c index 26a0e18fff..acf086a65f 100644 --- a/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c +++ b/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-sym-size-alloc --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" diff --git a/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c b/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c index af5a4df6dd..dbb2331aac 100644 --- a/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c +++ b/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --skip-not-symbolic-objects --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-sym-size-alloc --skip-not-symbolic-objects --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" diff --git a/test/Feature/SymbolicSizes/VoidStar.c b/test/Feature/SymbolicSizes/VoidStar.c index cd64f3d10a..48924f7b69 100644 --- a/test/Feature/SymbolicSizes/VoidStar.c +++ b/test/Feature/SymbolicSizes/VoidStar.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --skip-not-lazy-initialized --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-sym-size-alloc --skip-not-lazy-initialized --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include @@ -19,7 +19,7 @@ void foo(void *s) { ((char *)s)[1] = 'a'; // CHECK: VoidStar.c:[[@LINE+1]]: memory error: out of bound pointer struct Node *node = ((struct Node *)s)->next; - // CHECK: VoidStar.c:[[@LINE+1]]: memory error: out of bound pointer + // CHECK: VoidStar.c:[[@LINE+1]]: memory error: null pointer exception node->x = 20; } @@ -32,5 +32,5 @@ int main() { } // CHECK: KLEE: done: completed paths = 1 -// CHECK: KLEE: done: partially completed paths = 5 -// CHECK: KLEE: done: generated tests = 6 +// CHECK: KLEE: done: partially completed paths = 4 +// CHECK: KLEE: done: generated tests = 5 diff --git a/test/Industry/if2.c b/test/Industry/if2.c index 6ab4ec7ae0..3e4990abbe 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -15,4 +15,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 %13 (lines 8 to 8) in function main +// CHECK-DISTANCE: KLEE: (0, 1, 1) for Target 1: error in %13 in function main (lines 8 to 8) diff --git a/test/Industry/while_true.c b/test/Industry/while_true.c index 11ef6bba59..4b6cc204dc 100644 --- a/test/Industry/while_true.c +++ b/test/Industry/while_true.c @@ -15,11 +15,11 @@ int main() { // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 0.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-REACH-1 -// CHECK-REACH-1: (0, 1, 4) for Target 1: error in %17 (lines 8 to 8) in function main +// CHECK-REACH-1: (0, 1, 4) for Target 1: error in %17 in function main (lines 8 to 8) // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=5000 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-ALL // CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-REACH-2 -// CHECK-REACH-2: (0, 1, 1) for Target 1: error in %17 (lines 8 to 8) in function main +// CHECK-REACH-2: (0, 1, 1) for Target 1: error in %17 in function main (lines 8 to 8) diff --git a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c index 4f789d9aeb..1cac47fe6f 100644 --- a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c +++ b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c @@ -3,10 +3,10 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --solver-backend=z3 --skip-not-lazy-initialized --skip-not-symbolic-objects %t.bc > %t.log -// RUN: test -f %t.klee-out/test000008.ktest +// RUN: test -f %t.klee-out/test000006.ktest // RUN: %cc %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner -// RUN: env KTEST_FILE=%t.klee-out/test000008.ktest %t_runner | FileCheck %s +// RUN: env KTEST_FILE=%t.klee-out/test000006.ktest %t_runner | FileCheck %s #include