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/ExecutionState.h b/lib/Core/ExecutionState.h index 3dc0b3bff7..c3191d5ca8 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -317,6 +317,9 @@ class ExecutionState { // Overall state of the state - Data specific + /// @brief: TODO: + bool lastBrConfidently = true; + /// @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..778998681e 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" @@ -2724,6 +2725,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 +2745,11 @@ 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 { + (branches.first ? branches.first : branches.second)->lastBrConfidently = + true; } // NOTE: There is a hidden dependency here, markBranchVisited @@ -4014,9 +4021,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (iIdx >= vt->getNumElements()) { // Out of bounds write terminateStateOnProgramError( - state, new ErrorEvent(locationOf(state), - StateTerminationType::BadVectorAccess, - "Out of bounds write when inserting element")); + state, + new ErrorEvent(locationOf(state), + StateTerminationType::BadVectorAccess, + "Out of bounds write when inserting element"), + StateTerminationConfidenceCategory::CONFIDENT); return; } @@ -4057,9 +4066,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (iIdx >= vt->getNumElements()) { // Out of bounds read terminateStateOnProgramError( - state, new ErrorEvent(locationOf(state), - StateTerminationType::BadVectorAccess, - "Out of bounds read when extracting element")); + state, + new ErrorEvent(locationOf(state), + StateTerminationType::BadVectorAccess, + "Out of bounds read when extracting element"), + StateTerminationConfidenceCategory::CONFIDENT); return; } @@ -4963,28 +4974,41 @@ void Executor::terminateStateOnTargetError(ExecutionState &state, terminationType = StateTerminationType::User; } terminateStateOnProgramError( - state, new ErrorEvent(locationOf(state), terminationType, messaget)); + state, new ErrorEvent(locationOf(state), terminationType, messaget), + StateTerminationConfidenceCategory::CONFIDENT); } -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,13 +5054,14 @@ 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, - const ref &reason, - const llvm::Twine &info, - const char *suffix) { +void Executor::terminateStateOnProgramError( + ExecutionState &state, const ref &reason, + StateTerminationConfidenceCategory confidence, const llvm::Twine &info, + const char *suffix) { assert(reason->ruleID > StateTerminationType::SOLVERERR && reason->ruleID <= StateTerminationType::PROGERR); ++stats::terminationProgramError; @@ -5055,19 +5080,22 @@ void Executor::terminateStateOnProgramError(ExecutionState &state, } state.eventsRecorder.record(reason); - terminateStateOnError(state, reason->message, reason->ruleID, info, suffix); + terminateStateOnError(state, reason->message, reason->ruleID, 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 @@ -5416,13 +5444,20 @@ void Executor::executeFree(ExecutionState &state, ref address, new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*it->second), StateTerminationType::Free, "free of alloca"), + rl.size() != 1 ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, 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, "free of global"), + rl.size() != 1 ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, getAddressInfo(*it->second, address)); } else { it->second->removePointerResolutions(mo); @@ -5518,6 +5553,8 @@ bool Executor::resolveExact(ExecutionState &estate, ref address, *unbound, new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr, "memory error: invalid pointer: " + name), + !results.empty() ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, getAddressInfo(*unbound, address)); } } @@ -5607,7 +5644,7 @@ void Executor::concretizeSize(ExecutionState &state, ref size, new ErrorEvent(locationOf(*hugeSize.second), StateTerminationType::Model, "concretized symbolic size"), - info.str()); + StateTerminationConfidenceCategory::CONFIDENT, info.str()); } } } @@ -6309,7 +6346,8 @@ void Executor::executeMemoryOperation( *state, new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*state), StateTerminationType::ReadOnly, - "memory error: object read only")); + "memory error: object read only"), + StateTerminationConfidenceCategory::CONFIDENT); } else { wos->write(mo->getOffsetExpr(address), value); } @@ -6371,6 +6409,10 @@ void Executor::executeMemoryOperation( return; } + bool mayBeFalsePositive = + resolvedMemoryObjects.size() > 1 || + (resolvedMemoryObjects.size() == 1 && mayBeOutOfBound); + ExecutionState *unbound = nullptr; if (MergedPointerDereference) { ref guard; @@ -6428,7 +6470,10 @@ void Executor::executeMemoryOperation( new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*branches.first), StateTerminationType::ReadOnly, - "memory error: object read only")); + "memory error: object read only"), + mayBeFalsePositive + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT); state = branches.second; } else { ref result = SelectExpr::create( @@ -6500,7 +6545,10 @@ void Executor::executeMemoryOperation( *bound, new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*bound), StateTerminationType::ReadOnly, - "memory error: object read only")); + "memory error: object read only"), + mayBeFalsePositive + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT); } else { wos->write(mo->getOffsetExpr(address), value); } @@ -6552,6 +6600,8 @@ void Executor::executeMemoryOperation( new ErrorEvent(new AllocEvent(baseObjectPair.first->allocSite), locationOf(*unbound), StateTerminationType::Ptr, "memory error: out of bound pointer"), + mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, getAddressInfo(*unbound, address)); return; } @@ -6561,6 +6611,8 @@ void Executor::executeMemoryOperation( *unbound, new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr, "memory error: out of bound pointer"), + mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT, getAddressInfo(*unbound, address)); } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index a0a645eba3..b6a1b01c0e 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -618,6 +618,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); @@ -629,10 +630,10 @@ class Executor : public Interpreter { /// Call error handler and terminate state in case of program errors /// (e.g. free()ing globals, out-of-bound accesses) - void terminateStateOnProgramError(ExecutionState &state, - const ref &reason, - const llvm::Twine &longMessage = "", - const char *suffix = nullptr); + void terminateStateOnProgramError( + ExecutionState &state, const ref &reason, + StateTerminationConfidenceCategory confidence, + const llvm::Twine &longMessage = "", const char *suffix = nullptr); void terminateStateOnTerminator(ExecutionState &state); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index ba762edd0b..a46345fad8 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, + "abort failure"), + StateTerminationConfidenceCategory::CONFIDENT); } void SpecialFunctionHandler::handleExit(ExecutionState &state, @@ -361,15 +366,23 @@ 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, "ASSERTION FAIL: " + - readStringAtAddress(state, arguments[0]))); + readStringAtAddress(state, arguments[0])), + isAssertFailsConfidently(state) + ? StateTerminationConfidenceCategory::CONFIDENT + : StateTerminationConfidenceCategory::PROBABLY); } void SpecialFunctionHandler::handleAssertFail( @@ -381,7 +394,10 @@ void SpecialFunctionHandler::handleAssertFail( state, new ErrorEvent(executor.locationOf(state), StateTerminationType::Assert, "ASSERTION FAIL: " + - readStringAtAddress(state, arguments[0]))); + readStringAtAddress(state, arguments[0])), + isAssertFailsConfidently(state) + ? StateTerminationConfidenceCategory::CONFIDENT + : StateTerminationConfidenceCategory::PROBABLY); } void SpecialFunctionHandler::handleReportError( @@ -396,7 +412,8 @@ void SpecialFunctionHandler::handleReportError( new ErrorEvent(executor.locationOf(state), StateTerminationType::ReportError, readStringAtAddress(state, arguments[2])), - "", readStringAtAddress(state, arguments[3]).c_str()); + StateTerminationConfidenceCategory::CONFIDENT, "", + readStringAtAddress(state, arguments[3]).c_str()); } void SpecialFunctionHandler::handleNew(ExecutionState &state, @@ -840,6 +857,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess( state, new ErrorEvent(executor.locationOf(state), StateTerminationType::Ptr, "check_memory_access: memory error"), + StateTerminationConfidenceCategory::CONFIDENT, executor.getAddressInfo(state, address)); } else { const MemoryObject *mo = state.addressSpace.findObject(idObject).first; @@ -851,6 +869,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess( new ErrorEvent( new AllocEvent(mo->allocSite), executor.locationOf(state), StateTerminationType::Ptr, "check_memory_access: memory error"), + StateTerminationConfidenceCategory::CONFIDENT, executor.getAddressInfo(state, address)); } } @@ -1122,8 +1141,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 +1164,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/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,