diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index a08b3585e7..8f8ca41c2f 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -85,6 +85,8 @@ enum class StateTerminationType : std::uint8_t { /// \endcond }; +enum StateTerminationConfidenceCategory { CONFIDENT, PROBABLY }; + namespace HaltExecution { enum Reason { NotHalt = 0, diff --git a/lib/Core/CodeEvent.h b/lib/Core/CodeEvent.h index f266208629..31962875df 100644 --- a/lib/Core/CodeEvent.h +++ b/lib/Core/CodeEvent.h @@ -152,6 +152,10 @@ struct ErrorEvent : public CodeEvent { /// @brief ID for this error. const StateTerminationType ruleID; + /// @brief Confidence of this error: may be considered + /// as a flag of `true positive` error for instance. + const StateTerminationConfidenceCategory confidence; + /// @brief Message describing this error. const std::string message; @@ -161,14 +165,17 @@ struct ErrorEvent : public CodeEvent { const std::optional> source; ErrorEvent(const ref &source, const ref &sink, - StateTerminationType ruleID, const std::string &message) - : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), message(message), - source(source) {} + StateTerminationType ruleID, + StateTerminationConfidenceCategory confidence, + const std::string &message) + : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), confidence(confidence), + message(message), source(source) {} ErrorEvent(const ref &sink, StateTerminationType ruleID, + StateTerminationConfidenceCategory confidence, const std::string &message) - : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), message(message), - source(std::nullopt) {} + : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), confidence(confidence), + message(message), source(std::nullopt) {} std::string description() const override { return message; } diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index fa14493607..352058f707 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -160,7 +160,9 @@ ExecutionState::~ExecutionState() { ExecutionState::ExecutionState(const ExecutionState &state) : initPC(state.initPC), pc(state.pc), prevPC(state.prevPC), stack(state.stack), stackBalance(state.stackBalance), - incomingBBIndex(state.incomingBBIndex), depth(state.depth), + incomingBBIndex(state.incomingBBIndex), + lastBrConfidently(state.lastBrConfidently), + nullPointerMarkers(state.nullPointerMarkers), depth(state.depth), level(state.level), addressSpace(state.addressSpace), constraints(state.constraints), eventsRecorder(state.eventsRecorder), targetForest(state.targetForest), pathOS(state.pathOS), diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 3dc0b3bff7..76107ca2f2 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -317,6 +317,12 @@ class ExecutionState { // Overall state of the state - Data specific + /// @brief: TODO: + bool lastBrConfidently = true; + + /// @brief: TODO: + ImmutableList> nullPointerMarkers; + /// @brief Exploration depth, i.e., number of times KLEE branched for this /// state std::uint32_t depth = 0; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index eca2e57d1e..a439c14d59 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -40,6 +40,7 @@ #include "klee/Config/config.h" #include "klee/Core/Interpreter.h" #include "klee/Core/MockBuilder.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/ArrayExprVisitor.h" #include "klee/Expr/Assignment.h" @@ -61,6 +62,7 @@ #include "klee/Solver/Common.h" #include "klee/Solver/Solver.h" #include "klee/Solver/SolverCmdLine.h" +#include "klee/Solver/SolverUtil.h" #include "klee/Statistics/TimerStatIncrementer.h" #include "klee/Support/Casting.h" #include "klee/Support/ErrorHandling.h" @@ -2724,6 +2726,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (bi->getMetadata("md.ret")) { state.stack.forceReturnLocation(locationOf(state)); } + state.lastBrConfidently = true; transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state); } else { @@ -2743,6 +2746,15 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { maxNewStateStackSize = std::max(maxNewStateStackSize, branches.first->stack.stackRegisterSize() * 8); + branches.first->lastBrConfidently = false; + branches.second->lastBrConfidently = false; + } else { + if (branches.first) { + branches.first->lastBrConfidently = true; + } + if (branches.second) { + branches.second->lastBrConfidently = true; + } } // NOTE: There is a hidden dependency here, markBranchVisited @@ -4016,6 +4028,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { terminateStateOnProgramError( state, new ErrorEvent(locationOf(state), StateTerminationType::BadVectorAccess, + StateTerminationConfidenceCategory::CONFIDENT, "Out of bounds write when inserting element")); return; } @@ -4059,6 +4072,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { terminateStateOnProgramError( state, new ErrorEvent(locationOf(state), StateTerminationType::BadVectorAccess, + StateTerminationConfidenceCategory::CONFIDENT, "Out of bounds read when extracting element")); return; } @@ -4963,28 +4977,42 @@ void Executor::terminateStateOnTargetError(ExecutionState &state, terminationType = StateTerminationType::User; } terminateStateOnProgramError( - state, new ErrorEvent(locationOf(state), terminationType, messaget)); + state, + new ErrorEvent(locationOf(state), terminationType, + StateTerminationConfidenceCategory::CONFIDENT, messaget)); } -void Executor::terminateStateOnError(ExecutionState &state, - const llvm::Twine &messaget, - StateTerminationType terminationType, - const llvm::Twine &info, - const char *suffix) { +void Executor::terminateStateOnError( + ExecutionState &state, const llvm::Twine &messaget, + StateTerminationType terminationType, + StateTerminationConfidenceCategory confidence, const llvm::Twine &info, + const char *suffix) { std::string message = messaget.str(); - static std::set> emittedErrors; + static std::set< + std::pair>> + emittedErrors; const KInstruction *ki = getLastNonKleeInternalInstruction(state); Instruction *lastInst = ki->inst(); - if ((EmitAllErrors || - emittedErrors.insert(std::make_pair(lastInst, message)).second) && + if ((EmitAllErrors || emittedErrors + .insert(std::make_pair( + lastInst, std::make_pair(confidence, message))) + .second) && shouldWriteTest(state, true)) { std::string filepath = ki->getSourceFilepath(); + + std::string prefix = + (confidence == StateTerminationConfidenceCategory::CONFIDENT + ? "ERROR" + : "POSSIBLE ERROR"); + if (!filepath.empty()) { - klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(), - message.c_str()); + klee_message((prefix + ": %s:%zu: %s").c_str(), filepath.c_str(), + ki->getLine(), message.c_str()); } else { - klee_message("ERROR: (location information missing) %s", message.c_str()); + klee_message((prefix + ": (location information missing) %s").c_str(), + message.c_str()); } if (!EmitAllErrors) klee_message("NOTE: now ignoring this error at this location"); @@ -5030,7 +5058,8 @@ void Executor::terminateStateOnExecError(ExecutionState &state, assert(reason > StateTerminationType::USERERR && reason <= StateTerminationType::EXECERR); ++stats::terminationExecutionError; - terminateStateOnError(state, message, reason, ""); + terminateStateOnError(state, message, reason, + StateTerminationConfidenceCategory::CONFIDENT, ""); } void Executor::terminateStateOnProgramError(ExecutionState &state, @@ -5055,19 +5084,22 @@ void Executor::terminateStateOnProgramError(ExecutionState &state, } state.eventsRecorder.record(reason); - terminateStateOnError(state, reason->message, reason->ruleID, info, suffix); + terminateStateOnError(state, reason->message, reason->ruleID, + reason->confidence, info, suffix); } void Executor::terminateStateOnSolverError(ExecutionState &state, const llvm::Twine &message) { ++stats::terminationSolverError; - terminateStateOnError(state, message, StateTerminationType::Solver, ""); + terminateStateOnError(state, message, StateTerminationType::Solver, + StateTerminationConfidenceCategory::CONFIDENT, ""); } void Executor::terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message) { ++stats::terminationUserError; - terminateStateOnError(state, message, StateTerminationType::User, ""); + terminateStateOnError(state, message, StateTerminationType::User, + StateTerminationConfidenceCategory::CONFIDENT, ""); } // XXX shoot me @@ -5245,6 +5277,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, e->getWidth() == Context::get().getPointerWidth()) { ref symExternCallsCanReturnNullExpr = makeMockValue(state, "symExternCallsCanReturnNull", Expr::Bool); + state.nullPointerMarkers.push_back(symExternCallsCanReturnNullExpr); e = SelectExpr::create( symExternCallsCanReturnNullExpr, ConstantExpr::alloc(0, Context::get().getPointerWidth()), e); @@ -5370,6 +5403,7 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, makeMockValue(state, "symCheckOutOfMemory", Expr::Bool); address = SelectExpr::create(symCheckOutOfMemoryExpr, Expr::createPointer(0), address); + state.nullPointerMarkers.push_back(symCheckOutOfMemoryExpr); } // state.addPointerResolution(address, mo); @@ -5415,13 +5449,22 @@ void Executor::executeFree(ExecutionState &state, ref address, *it->second, new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*it->second), StateTerminationType::Free, + rl.size() != 1 + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, "free of alloca"), getAddressInfo(*it->second, address)); } else if (mo->isGlobal) { + if (rl.size() != 1) { + klee_warning("Following error if likely false positive"); + } terminateStateOnProgramError( *it->second, new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*it->second), StateTerminationType::Free, + rl.size() != 1 + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, "free of global"), getAddressInfo(*it->second, address)); } else { @@ -5434,6 +5477,99 @@ void Executor::executeFree(ExecutionState &state, ref address, } } +ExecutionState *Executor::handleNullPointerException(ExecutionState &state, + ref base) { + StatePair branches = + forkInternal(state, Expr::createIsZero(base), BranchType::MemOp); + ExecutionState *bound = branches.first; + if (!bound) { + return branches.second; + } + + // If there are no markers on `malloc` returning nullptr, + // then `confidence` depends on presence of `unbound` state. + if (!bound->nullPointerMarkers.empty()) { + // bound constraints already contain `Expr::createIsZero()` + std::vector markersArrays; + markersArrays.reserve(bound->nullPointerMarkers.size()); + findSymbolicObjects(bound->nullPointerMarkers.begin(), + bound->nullPointerMarkers.end(), markersArrays); + + // Do some iterations (2-3) to figure out if error is confident. + ref allExcludedVectorsOfMarkers = Expr::createTrue(); + + bool convinced = false; + for (int tpCheckIteration = 0; tpCheckIteration < 2; ++tpCheckIteration) { + ref isConfidentResponse; + if (!solver->getResponse(bound->constraints.cs(), + allExcludedVectorsOfMarkers, isConfidentResponse, + bound->queryMetaData)) { + terminateStateOnSolverError(*bound, "Query timeout"); + } + + if (isa(isConfidentResponse)) { + reportStateOnTargetError(*bound, + ReachWithError::MustBeNullPointerException); + + terminateStateOnProgramError( + *bound, + new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr, + StateTerminationConfidenceCategory::CONFIDENT, + "memory error: null pointer exception")); + convinced = true; + break; + } + + // Receive current values of markers + std::vector> boundSetSolution; + isConfidentResponse->tryGetInitialValuesFor(markersArrays, + boundSetSolution); + Assignment nonConfidentResponseAssignment(markersArrays, + boundSetSolution); + + // Exclude this combinations of markers + + ref conjExcludedVectorOfMarkers = Expr::createTrue(); + for (ref marker : bound->nullPointerMarkers) { + conjExcludedVectorOfMarkers = AndExpr::create( + conjExcludedVectorOfMarkers, + EqExpr::create(marker, + nonConfidentResponseAssignment.evaluate(marker))); + } + + allExcludedVectorsOfMarkers = + OrExpr::create(allExcludedVectorsOfMarkers, + NotExpr::create(conjExcludedVectorOfMarkers)); + } + + if (!convinced) { + reportStateOnTargetError(*bound, + ReachWithError::MayBeNullPointerException); + + terminateStateOnProgramError( + *bound, new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr, + StateTerminationConfidenceCategory::PROBABLY, + "memory error: null pointer exception")); + } + + } else { + auto error = branches.second != nullptr + ? ReachWithError::MayBeNullPointerException + : ReachWithError::MustBeNullPointerException; + reportStateOnTargetError(*bound, error); + + terminateStateOnProgramError( + *bound, + new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr, + branches.second != nullptr + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, + "memory error: null pointer exception")); + } + + return branches.second; +} + bool Executor::resolveExact(ExecutionState &estate, ref address, KType *type, ExactResolutionList &results, const std::string &name) { @@ -5459,20 +5595,12 @@ bool Executor::resolveExact(ExecutionState &estate, ref address, Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified; uniqueBase = toUnique(estate, uniqueBase); - StatePair branches = - forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp); - ExecutionState *bound = branches.first; - if (bound) { - auto error = isReadFromSymbolicArray(uniqueBase) - ? ReachWithError::MayBeNullPointerException - : ReachWithError::MustBeNullPointerException; - terminateStateOnTargetError(*bound, error); - } - if (!branches.second) { - address = Expr::createPointer(0); + ExecutionState *handledNPEState = handleNullPointerException(estate, base); + if (!handledNPEState) { + return false; } - ExecutionState &state = *branches.second; + ExecutionState &state = *handledNPEState; ResolutionList rl; bool mayBeOutOfBound = true; @@ -5517,6 +5645,9 @@ bool Executor::resolveExact(ExecutionState &estate, ref address, terminateStateOnProgramError( *unbound, new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr, + !results.empty() + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, "memory error: invalid pointer: " + name), getAddressInfo(*unbound, address)); } @@ -5606,6 +5737,7 @@ void Executor::concretizeSize(ExecutionState &state, ref size, *hugeSize.second, new ErrorEvent(locationOf(*hugeSize.second), StateTerminationType::Model, + StateTerminationConfidenceCategory::CONFIDENT, "concretized symbolic size"), info.str()); } @@ -6227,18 +6359,9 @@ void Executor::executeMemoryOperation( ref uniqueBase = toUnique(estate, base); - StatePair branches = - forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp); - ExecutionState *bound = branches.first; - if (bound) { - auto error = isReadFromSymbolicArray(uniqueBase) - ? ReachWithError::MayBeNullPointerException - : ReachWithError::MustBeNullPointerException; - terminateStateOnTargetError(*bound, error); - } - if (!branches.second) + ExecutionState *state = handleNullPointerException(estate, base); + if (!state) return; - ExecutionState *state = branches.second; // fast path: single in-bounds resolution IDType idFastResult; @@ -6309,6 +6432,7 @@ void Executor::executeMemoryOperation( *state, new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*state), StateTerminationType::ReadOnly, + StateTerminationConfidenceCategory::CONFIDENT, "memory error: object read only")); } else { wos->write(mo->getOffsetExpr(address), value); @@ -6371,6 +6495,10 @@ void Executor::executeMemoryOperation( return; } + bool mayBeFalsePositive = + resolvedMemoryObjects.size() > 1 || + (resolvedMemoryObjects.size() == 1 && mayBeOutOfBound); + ExecutionState *unbound = nullptr; if (MergedPointerDereference) { ref guard; @@ -6419,16 +6547,19 @@ void Executor::executeMemoryOperation( maxNewWriteableOSSize = std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); if (wos->readOnly) { - branches = + StatePair branches = forkInternal(*state, Expr::createIsZero(unboundConditions[i]), BranchType::MemOp); assert(branches.first); terminateStateOnProgramError( *branches.first, - new ErrorEvent(new AllocEvent(mo->allocSite), - locationOf(*branches.first), - StateTerminationType::ReadOnly, - "memory error: object read only")); + new ErrorEvent( + new AllocEvent(mo->allocSite), locationOf(*branches.first), + StateTerminationType::ReadOnly, + mayBeFalsePositive + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, + "memory error: object read only")); state = branches.second; } else { ref result = SelectExpr::create( @@ -6497,10 +6628,13 @@ void Executor::executeMemoryOperation( ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); if (wos->readOnly) { terminateStateOnProgramError( - *bound, - new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*bound), - StateTerminationType::ReadOnly, - "memory error: object read only")); + *bound, new ErrorEvent( + new AllocEvent(mo->allocSite), locationOf(*bound), + StateTerminationType::ReadOnly, + mayBeFalsePositive + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, + "memory error: object read only")); } else { wos->write(mo->getOffsetExpr(address), value); } @@ -6551,6 +6685,9 @@ void Executor::executeMemoryOperation( *unbound, new ErrorEvent(new AllocEvent(baseObjectPair.first->allocSite), locationOf(*unbound), StateTerminationType::Ptr, + mayBeFalsePositive + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, "memory error: out of bound pointer"), getAddressInfo(*unbound, address)); return; @@ -6560,6 +6697,9 @@ void Executor::executeMemoryOperation( terminateStateOnProgramError( *unbound, new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr, + mayBeFalsePositive + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, "memory error: out of bound pointer"), getAddressInfo(*unbound, address)); } @@ -7212,21 +7352,25 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res, } void Executor::addSARIFReport(const ExecutionState &state) { - ResultJson result{}; - - CodeFlowJson codeFlow = state.eventsRecorder.serialize(); - if (ref lastEvent = llvm::dyn_cast(state.eventsRecorder.last())) { + + ResultJson result{}; + + CodeFlowJson codeFlow = state.eventsRecorder.serialize(); + result.locations.push_back(lastEvent->serialize()); result.message = {Message{lastEvent->message}}; result.ruleId = {terminationTypeName(lastEvent->ruleID)}; - result.level = {"error"}; - } + result.level = {lastEvent->confidence == + StateTerminationConfidenceCategory::CONFIDENT + ? "error" + : "warning"}; - result.codeFlows.push_back(std::move(codeFlow)); + result.codeFlows.push_back(std::move(codeFlow)); - sarifReport.runs.back().results.push_back(std::move(result)); + sarifReport.runs.back().results.push_back(std::move(result)); + } } SarifReportJson Executor::getSARIFReport() const { return sarifReport; } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index a0a645eba3..37d7852488 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -413,6 +413,9 @@ class Executor : public Interpreter { const std::vector &resolveConcretizations, std::vector> &results); + ExecutionState *handleNullPointerException(ExecutionState &state, + ref base); + // do address resolution / object binding / out of bounds checking // and perform the operation void executeMemoryOperation(ExecutionState &state, bool isWrite, @@ -618,6 +621,7 @@ class Executor : public Interpreter { /// below. void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, StateTerminationType reason, + StateTerminationConfidenceCategory confidence, const llvm::Twine &longMessage = "", const char *suffix = nullptr); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index ba762edd0b..104f4fee8a 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -20,6 +20,7 @@ #include "TypeManager.h" #include "klee/Config/config.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" #include "klee/Solver/SolverCmdLine.h" @@ -30,6 +31,8 @@ #include "klee/klee.h" #include "klee/Support/CompilerWarning.h" +#include +#include DISABLE_WARNING_PUSH DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/APFloat.h" @@ -343,8 +346,10 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, std::vector> &arguments) { assert(arguments.size() == 0 && "invalid number of arguments to abort"); executor.terminateStateOnProgramError( - state, new ErrorEvent(executor.locationOf(state), - StateTerminationType::Abort, "abort failure")); + state, + new ErrorEvent(executor.locationOf(state), StateTerminationType::Abort, + StateTerminationConfidenceCategory::CONFIDENT, + "abort failure")); } void SpecialFunctionHandler::handleExit(ExecutionState &state, @@ -361,13 +366,21 @@ void SpecialFunctionHandler::handleSilentExit( executor.terminateStateEarlyUser(state, ""); } +static bool isAssertFailsConfidently(ExecutionState &state) { + return state.lastBrConfidently; +} + void SpecialFunctionHandler::handleAssert(ExecutionState &state, KInstruction *target, std::vector> &arguments) { assert(arguments.size() == 3 && "invalid number of arguments to _assert"); + executor.terminateStateOnProgramError( state, new ErrorEvent(executor.locationOf(state), StateTerminationType::Assert, + isAssertFailsConfidently(state) + ? StateTerminationConfidenceCategory::CONFIDENT + : StateTerminationConfidenceCategory::PROBABLY, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]))); } @@ -380,6 +393,9 @@ void SpecialFunctionHandler::handleAssertFail( executor.terminateStateOnProgramError( state, new ErrorEvent(executor.locationOf(state), StateTerminationType::Assert, + isAssertFailsConfidently(state) + ? StateTerminationConfidenceCategory::CONFIDENT + : StateTerminationConfidenceCategory::PROBABLY, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]))); } @@ -395,6 +411,7 @@ void SpecialFunctionHandler::handleReportError( state, new ErrorEvent(executor.locationOf(state), StateTerminationType::ReportError, + StateTerminationConfidenceCategory::CONFIDENT, readStringAtAddress(state, arguments[2])), "", readStringAtAddress(state, arguments[3]).c_str()); } @@ -839,6 +856,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess( executor.terminateStateOnProgramError( state, new ErrorEvent(executor.locationOf(state), StateTerminationType::Ptr, + StateTerminationConfidenceCategory::CONFIDENT, "check_memory_access: memory error"), executor.getAddressInfo(state, address)); } else { @@ -848,9 +866,11 @@ void SpecialFunctionHandler::handleCheckMemoryAccess( if (!chk->isTrue()) { executor.terminateStateOnProgramError( state, - new ErrorEvent( - new AllocEvent(mo->allocSite), executor.locationOf(state), - StateTerminationType::Ptr, "check_memory_access: memory error"), + new ErrorEvent(new AllocEvent(mo->allocSite), + executor.locationOf(state), + StateTerminationType::Ptr, + StateTerminationConfidenceCategory::CONFIDENT, + "check_memory_access: memory error"), executor.getAddressInfo(state, address)); } } @@ -1122,8 +1142,9 @@ void SpecialFunctionHandler::handleSetConcreteRoundingMode( llvm::APFloat::rmNearestTiesToEven; ref roundingModeArg = arguments[0]; if (!isa(roundingModeArg)) { - executor.terminateStateOnError(state, "argument should be concrete", - StateTerminationType::User); + executor.terminateStateOnError( + state, "argument should be concrete", StateTerminationType::User, + StateTerminationConfidenceCategory::CONFIDENT); return; } const ConstantExpr *CE = dyn_cast(roundingModeArg); @@ -1144,8 +1165,9 @@ void SpecialFunctionHandler::handleSetConcreteRoundingMode( newRoundingMode = llvm::APFloat::rmTowardZero; break; default: - executor.terminateStateOnError(state, "Invalid rounding mode", - StateTerminationType::User); + executor.terminateStateOnError( + state, "Invalid rounding mode", StateTerminationType::User, + StateTerminationConfidenceCategory::CONFIDENT); return; } state.roundingMode = newRoundingMode; diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 518e922dc8..0d94d022b3 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #include "klee/Expr/ExprUtil.h" +#include "klee/ADT/ImmutableList.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprVisitor.h" @@ -186,6 +187,9 @@ template void klee::findSymbolicObjects(B, B, std::vector &); typedef ExprHashSet::iterator C; template void klee::findSymbolicObjects(C, C, std::vector &); +typedef ImmutableList>::iterator D; +template void klee::findSymbolicObjects(D, D, std::vector &); + typedef std::vector>::iterator A; template void klee::findObjects(A, A, std::vector &); diff --git a/lib/Support/ErrorHandling.cpp b/lib/Support/ErrorHandling.cpp index 685ac5c52b..2318a78bc7 100644 --- a/lib/Support/ErrorHandling.cpp +++ b/lib/Support/ErrorHandling.cpp @@ -32,6 +32,7 @@ FILE *klee::klee_message_file = NULL; static const char *warningPrefix = "WARNING"; static const char *warningOncePrefix = "WARNING ONCE"; static const char *errorPrefix = "ERROR"; +static const char *possibleErrorPrefix = "POSSIBLE ERROR"; static const char *notePrefix = "NOTE"; namespace klee { @@ -80,12 +81,18 @@ static void klee_vfmessage(FILE *fp, const char *pfx, const char *msg, /*bold=*/true, /*bg=*/false); - // Errors + // True-Postive Errors if (shouldSetColor(pfx, msg, errorPrefix)) fdos.changeColor(llvm::raw_ostream::RED, /*bold=*/true, /*bg=*/false); + // Non True-Positive Errors + if (shouldSetColor(pfx, msg, possibleErrorPrefix)) + fdos.changeColor(llvm::raw_ostream::YELLOW, + /*bold=*/true, + /*bg=*/false); + // Notes if (shouldSetColor(pfx, msg, notePrefix)) fdos.changeColor(llvm::raw_ostream::WHITE,