diff options
| -rw-r--r-- | include/klee/Core/TerminationTypes.h | 110 | ||||
| -rw-r--r-- | lib/Core/CoreStats.cpp | 8 | ||||
| -rw-r--r-- | lib/Core/CoreStats.h | 6 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 139 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 41 | ||||
| -rw-r--r-- | lib/Core/MergeHandler.cpp | 2 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 26 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 13 | ||||
| -rwxr-xr-x | tools/klee-stats/klee-stats | 9 |
9 files changed, 243 insertions, 111 deletions
diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 4fe5583a..25e5ef4a 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -12,51 +12,85 @@ #include <cstdint> + +#define TERMINATION_CLASSES \ + TCLASS(Exit, 1U) \ + TCLASS(Early, 2U) \ + TCLASS(SolverError, 3U) \ + TCLASS(ProgramError, 4U) \ + TCLASS(UserError, 5U) \ + TCLASS(ExecutionError, 6U) \ + TCLASS(EarlyAlgorithm, 7U) \ + TCLASS(EarlyUser, 8U) + +///@brief Termination classes categorize termination types +enum class StateTerminationClass : std::uint8_t { + /// \cond DO_NOT_DOCUMENT + #define TCLASS(N,I) N = (I), + TERMINATION_CLASSES + /// \endcond +}; + + +// (Name, ID, file suffix) #define TERMINATION_TYPES \ TTYPE(RUNNING, 0U, "") \ TTYPE(Exit, 1U, "") \ - MARK(NORMAL, 1U) \ - TTYPE(Interrupted, 2U, "early") \ - TTYPE(MaxDepth, 3U, "early") \ - TTYPE(OutOfMemory, 4U, "early") \ - TTYPE(OutOfStackMemory, 5U, "early") \ - MARK(EARLY, 5U) \ - TTYPE(Solver, 8U, "solver.err") \ - MARK(SOLVERERR, 8U) \ - TTYPE(Abort, 10U, "abort.err") \ - TTYPE(Assert, 11U, "assert.err") \ - TTYPE(BadVectorAccess, 12U, "bad_vector_access.err") \ - TTYPE(Free, 13U, "free.err") \ - TTYPE(Model, 14U, "model.err") \ - TTYPE(Overflow, 15U, "overflow.err") \ - TTYPE(Ptr, 16U, "ptr.err") \ - TTYPE(ReadOnly, 17U, "read_only.err") \ - TTYPE(ReportError, 18U, "report_error.err") \ - TTYPE(InvalidBuiltin, 19U, "invalid_builtin_use.err") \ - TTYPE(ImplicitTruncation, 20U, "implicit_truncation.err") \ - TTYPE(ImplicitConversion, 21U, "implicit_conversion.err") \ - TTYPE(UnreachableCall, 22U, "unreachable_call.err") \ - TTYPE(MissingReturn, 23U, "missing_return.err") \ - TTYPE(InvalidLoad, 24U, "invalid_load.err") \ - TTYPE(NullableAttribute, 25U, "nullable_attribute.err") \ - MARK(PROGERR, 25U) \ - TTYPE(User, 33U, "user.err") \ - MARK(USERERR, 33U) \ - TTYPE(Execution, 35U, "exec.err") \ - TTYPE(External, 36U, "external.err") \ - MARK(EXECERR, 36U) \ - TTYPE(Replay, 37U, "") \ - TTYPE(Merge, 38U, "") \ - TTYPE(SilentExit, 39U, "") \ - MARK(END, 39U) + TTMARK(EXIT, 1U) \ + TTYPE(Interrupted, 10U, "early") \ + TTYPE(MaxDepth, 11U, "early") \ + TTYPE(OutOfMemory, 12U, "early") \ + TTYPE(OutOfStackMemory, 13U, "early") \ + TTMARK(EARLY, 13U) \ + TTYPE(Solver, 20U, "solver.err") \ + TTMARK(SOLVERERR, 20U) \ + TTYPE(Abort, 30U, "abort.err") \ + TTYPE(Assert, 31U, "assert.err") \ + TTYPE(BadVectorAccess, 32U, "bad_vector_access.err") \ + TTYPE(Free, 33U, "free.err") \ + TTYPE(Model, 34U, "model.err") \ + TTYPE(Overflow, 35U, "overflow.err") \ + TTYPE(Ptr, 36U, "ptr.err") \ + TTYPE(ReadOnly, 37U, "read_only.err") \ + TTYPE(ReportError, 38U, "report_error.err") \ + TTYPE(InvalidBuiltin, 39U, "invalid_builtin_use.err") \ + TTYPE(ImplicitTruncation, 40U, "implicit_truncation.err") \ + TTYPE(ImplicitConversion, 41U, "implicit_conversion.err") \ + TTYPE(UnreachableCall, 42U, "unreachable_call.err") \ + TTYPE(MissingReturn, 43U, "missing_return.err") \ + TTYPE(InvalidLoad, 44U, "invalid_load.err") \ + TTYPE(NullableAttribute, 45U, "nullable_attribute.err") \ + TTMARK(PROGERR, 45U) \ + TTYPE(User, 50U, "user.err") \ + TTMARK(USERERR, 50U) \ + TTYPE(Execution, 60U, "exec.err") \ + TTYPE(External, 61U, "external.err") \ + TTMARK(EXECERR, 61U) \ + TTYPE(Replay, 70U, "") \ + TTYPE(Merge, 71U, "") \ + TTMARK(EARLYALGORITHM, 71U) \ + TTYPE(SilentExit, 80U, "") \ + TTMARK(EARLYUSER, 80U) \ + TTMARK(END, 80U) + ///@brief Reason an ExecutionState got terminated. enum class StateTerminationType : std::uint8_t { -#define TTYPE(N,I,S) N = (I), -#define MARK(N,I) N = (I), + /// \cond DO_NOT_DOCUMENT + #define TTYPE(N,I,S) N = (I), + #define TTMARK(N,I) N = (I), TERMINATION_TYPES -#undef TTYPE -#undef MARK + /// \endcond }; + +// reset definitions + +#undef TCLASS +#undef TTYPE +#undef TTMARK +#define TCLASS(N,I) +#define TTYPE(N,I,S) +#define TTMARK(N,I) + #endif diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp index 54a9a697..48eb1e85 100644 --- a/lib/Core/CoreStats.cpp +++ b/lib/Core/CoreStats.cpp @@ -8,7 +8,6 @@ //===----------------------------------------------------------------------===// #include "CoreStats.h" - #include "klee/Support/ErrorHandling.h" @@ -49,3 +48,10 @@ void stats::incBranchStat(BranchType reason, std::uint32_t value) { static_cast<std::uint8_t>(reason)); } } + + +// termination types + +#undef TCLASS +#define TCLASS(Name,I) Statistic stats::termination ## Name("Termination"#Name, "Trm"#Name); +TERMINATION_CLASSES diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h index 15850354..609e976a 100644 --- a/lib/Core/CoreStats.h +++ b/lib/Core/CoreStats.h @@ -11,6 +11,7 @@ #define KLEE_CORESTATS_H #include "klee/Core/BranchTypes.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Statistics/Statistic.h" namespace klee { @@ -55,6 +56,11 @@ namespace stats { #define BTYPE(Name,I) extern Statistic branches ## Name; BRANCH_TYPES + /// Count termination types. + #undef TCLASS + #define TCLASS(Name,I) extern Statistic termination ## Name; + TERMINATION_CLASSES + /// Increase a branch statistic for the given reason by value. void incBranchStat(BranchType reason, std::uint32_t value); } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e3af7348..a3f91f20 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -436,6 +436,7 @@ llvm::cl::bits<PrintDebugInstructionsType> DebugPrintInstructions( "Log all instructions to file " "instructions.txt in format [src, " "inst_id]"), + clEnumValN(FILE_COMPACT, "compact:file", "Log all instructions to file instructions.txt in format " "[inst_id]")), @@ -953,7 +954,7 @@ void Executor::branch(ExecutionState &state, if (OnlyReplaySeeds) { for (unsigned i=0; i<N; ++i) { if (result[i] && !seedMap.count(result[i])) { - terminateStateEarly(*result[i], "Unseeded path during replay", StateTerminationType::Replay); + terminateStateEarlyAlgorithm(*result[i], "Unseeded path during replay", StateTerminationType::Replay); result[i] = nullptr; } } @@ -3167,8 +3168,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (iIdx >= vt->getNumElements()) { // Out of bounds write - terminateStateOnError(state, "Out of bounds write when inserting element", - StateTerminationType::BadVectorAccess); + terminateStateOnProgramError(state, + "Out of bounds write when inserting element", + StateTerminationType::BadVectorAccess); return; } @@ -3208,8 +3210,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (iIdx >= vt->getNumElements()) { // Out of bounds read - terminateStateOnError(state, "Out of bounds read when extracting element", - StateTerminationType::BadVectorAccess); + terminateStateOnProgramError(state, + "Out of bounds read when extracting element", + StateTerminationType::BadVectorAccess); return; } @@ -3658,17 +3661,18 @@ static bool shouldWriteTest(const ExecutionState &state) { static std::string terminationTypeFileExtension(StateTerminationType type) { std::string ret; -#define TTYPE(N,I,S) case StateTerminationType::N: ret = (S); break; -#define MARK(N,I) + #undef TTYPE + #undef TTMARK + #define TTYPE(N,I,S) case StateTerminationType::N: ret = (S); break; + #define TTMARK(N,I) switch (type) { - TERMINATION_TYPES + TERMINATION_TYPES } -#undef TTYPE -#undef MARK return ret; }; void Executor::terminateStateOnExit(ExecutionState &state) { + ++stats::terminationExit; if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state))) interpreterHandler->processTestCase( state, nullptr, @@ -3679,20 +3683,35 @@ void Executor::terminateStateOnExit(ExecutionState &state) { } void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, - StateTerminationType terminationType) { - if ((terminationType <= StateTerminationType::EXECERR && - shouldWriteTest(state)) || + StateTerminationType reason) { + if (reason <= StateTerminationType::EARLY) { + assert(reason > StateTerminationType::EXIT); + ++stats::terminationEarly; + } + + if ((reason <= StateTerminationType::EARLY && shouldWriteTest(state)) || (AlwaysOutputSeeds && seedMap.count(&state))) { interpreterHandler->processTestCase( state, (message + "\n").str().c_str(), - terminationTypeFileExtension(terminationType).c_str()); + terminationTypeFileExtension(reason).c_str()); } terminateState(state); } -void Executor::terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message) { - terminateStateOnError(state, message, StateTerminationType::User, ""); +void Executor::terminateStateEarlyAlgorithm(ExecutionState &state, + const llvm::Twine &message, + StateTerminationType reason) { + assert(reason > StateTerminationType::EXECERR && + reason <= StateTerminationType::EARLYALGORITHM); + ++stats::terminationEarlyAlgorithm; + terminateStateEarly(state, message, reason); +} + +void Executor::terminateStateEarlyUser(ExecutionState &state, + const llvm::Twine &message) { + ++stats::terminationEarlyUser; + terminateStateEarly(state, message, StateTerminationType::SilentExit); } const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state, @@ -3793,15 +3812,36 @@ void Executor::terminateStateOnError(ExecutionState &state, void Executor::terminateStateOnExecError(ExecutionState &state, const llvm::Twine &message, - const llvm::Twine &info) { - terminateStateOnError(state, message, StateTerminationType::Execution, info); + StateTerminationType reason) { + assert(reason > StateTerminationType::USERERR && + reason <= StateTerminationType::EXECERR); + ++stats::terminationExecutionError; + terminateStateOnError(state, message, reason, ""); +} + +void Executor::terminateStateOnProgramError(ExecutionState &state, + const llvm::Twine &message, + StateTerminationType reason, + const llvm::Twine &info, + const char *suffix) { + assert(reason > StateTerminationType::SOLVERERR && + reason <= StateTerminationType::PROGERR); + ++stats::terminationProgramError; + terminateStateOnError(state, message, reason, info, suffix); } void Executor::terminateStateOnSolverError(ExecutionState &state, const llvm::Twine &message) { + ++stats::terminationSolverError; terminateStateOnError(state, message, StateTerminationType::Solver, ""); } +void Executor::terminateStateOnUserError(ExecutionState &state, + const llvm::Twine &message) { + ++stats::terminationUserError; + terminateStateOnError(state, message, StateTerminationType::User, ""); +} + // XXX shoot me static const char *okExternalsList[] = { "printf", "fprintf", @@ -3945,14 +3985,15 @@ void Executor::callExternalFunction(ExecutionState &state, bool success = externalDispatcher->executeCall(callable, target->inst, args); if (!success) { - terminateStateOnError(state, "failed external call: " + callable->getName(), - StateTerminationType::External); + terminateStateOnExecError(state, + "failed external call: " + callable->getName(), + StateTerminationType::External); return; } if (!state.addressSpace.copyInConcretes()) { - terminateStateOnError(state, "external modified read-only object", - StateTerminationType::External); + terminateStateOnExecError(state, "external modified read-only object", + StateTerminationType::External); return; } @@ -4135,8 +4176,9 @@ void Executor::executeAlloc(ExecutionState &state, ExprPPrinter::printOne(info, " size expr", size); info << " concretization : " << example << "\n"; info << " unbound example: " << tmp << "\n"; - terminateStateOnError(*hugeSize.second, "concretized symbolic size", - StateTerminationType::Model, info.str()); + terminateStateOnProgramError(*hugeSize.second, + "concretized symbolic size", + StateTerminationType::Model, info.str()); } } } @@ -4165,13 +4207,13 @@ void Executor::executeFree(ExecutionState &state, ie = rl.end(); it != ie; ++it) { const MemoryObject *mo = it->first.first; if (mo->isLocal) { - terminateStateOnError(*it->second, "free of alloca", - StateTerminationType::Free, - getAddressInfo(*it->second, address)); + terminateStateOnProgramError(*it->second, "free of alloca", + StateTerminationType::Free, + getAddressInfo(*it->second, address)); } else if (mo->isGlobal) { - terminateStateOnError(*it->second, "free of global", - StateTerminationType::Free, - getAddressInfo(*it->second, address)); + terminateStateOnProgramError(*it->second, "free of global", + StateTerminationType::Free, + getAddressInfo(*it->second, address)); } else { it->second->deallocate(mo); it->second->addressSpace.unbindObject(mo); @@ -4215,14 +4257,15 @@ void Executor::resolveExact(ExecutionState &state, auto locinfo = unbound->heapAllocator.location_info(ptr, 1); if (locinfo == LocationInfo::LI_AllocatedOrQuarantined && locinfo.getBaseAddress() == ptr && name == "free") { - terminateStateOnError(*unbound, "memory error: double free", - StateTerminationType::Ptr, - getAddressInfo(*unbound, p)); + terminateStateOnProgramError(*unbound, "memory error: double free", + StateTerminationType::Ptr, + getAddressInfo(*unbound, p)); return; } } - terminateStateOnError(*unbound, "memory error: invalid pointer: " + name, - StateTerminationType::Ptr, getAddressInfo(*unbound, p)); + terminateStateOnProgramError( + *unbound, "memory error: invalid pointer: " + name, + StateTerminationType::Ptr, getAddressInfo(*unbound, p)); } } @@ -4280,8 +4323,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, const ObjectState *os = op.second; if (isWrite) { if (os->readOnly) { - terminateStateOnError(state, "memory error: object read only", - StateTerminationType::ReadOnly); + terminateStateOnProgramError(state, "memory error: object read only", + StateTerminationType::ReadOnly); } else { ObjectState *wos = state.addressSpace.getWriteable(mo, os); wos->write(offset, value); @@ -4324,8 +4367,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (bound) { if (isWrite) { if (os->readOnly) { - terminateStateOnError(*bound, "memory error: object read only", - StateTerminationType::ReadOnly); + terminateStateOnProgramError(*bound, "memory error: object read only", + StateTerminationType::ReadOnly); } else { ObjectState *wos = bound->addressSpace.getWriteable(mo, os); wos->write(mo->getOffsetExpr(address), value); @@ -4350,9 +4393,9 @@ void Executor::executeMemoryOperation(ExecutionState &state, std::uintptr_t ptrval = CE->getZExtValue(); auto ptr = reinterpret_cast<void *>(ptrval); if (ptrval < MemoryManager::pageSize) { - terminateStateOnError(*unbound, "memory error: null page access", - StateTerminationType::Ptr, - getAddressInfo(*unbound, address)); + terminateStateOnProgramError( + *unbound, "memory error: null page access", + StateTerminationType::Ptr, getAddressInfo(*unbound, address)); return; } else if (MemoryManager::isDeterministic) { using kdalloc::LocationInfo; @@ -4364,17 +4407,17 @@ void Executor::executeMemoryOperation(ExecutionState &state, auto baseExpr = Expr::createPointer(base); ObjectPair op; if (!unbound->addressSpace.resolveOne(baseExpr, op)) { - terminateStateOnError(*unbound, "memory error: use after free", - StateTerminationType::Ptr, - getAddressInfo(*unbound, address)); + terminateStateOnProgramError( + *unbound, "memory error: use after free", + StateTerminationType::Ptr, getAddressInfo(*unbound, address)); return; } } } } - terminateStateOnError(*unbound, "memory error: out of bound pointer", - StateTerminationType::Ptr, - getAddressInfo(*unbound, address)); + terminateStateOnProgramError( + *unbound, "memory error: out of bound pointer", + StateTerminationType::Ptr, getAddressInfo(*unbound, address)); } } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c821b987..28a7d56d 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -410,7 +410,8 @@ private: const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, llvm::Instruction** lastInstruction); - /// Remove state from queue and delete state + /// Remove state from queue and delete state. This function should only be + /// used in the termination functions below. void terminateState(ExecutionState &state); /// Call exit handler and terminate state normally @@ -420,21 +421,43 @@ private: /// Call exit handler and terminate state early /// (e.g. due to state merging or memory pressure) void terminateStateEarly(ExecutionState &state, const llvm::Twine &message, - StateTerminationType terminationType); + StateTerminationType reason); + + /// Call exit handler and terminate state early + /// (e.g. caused by the applied algorithm as in state merging or replaying) + void terminateStateEarlyAlgorithm(ExecutionState &state, + const llvm::Twine &message, + StateTerminationType reason); + + /// Call exit handler and terminate state early + /// (e.g. due to klee_silent_exit issued by user) + void terminateStateEarlyUser(ExecutionState &state, + const llvm::Twine &message); + + /// Call error handler and terminate state in case of errors. + /// The underlying function of all error-handling termination functions + /// below. This function should only be used in the termination functions + /// below. + void terminateStateOnError(ExecutionState &state, + const llvm::Twine &message, + StateTerminationType reason, + const llvm::Twine &longMessage = "", + const char *suffix = nullptr); /// Call error handler and terminate state in case of program errors /// (e.g. free()ing globals, out-of-bound accesses) - void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, - StateTerminationType terminationType, - const llvm::Twine &longMessage = "", - const char *suffix = nullptr); + void terminateStateOnProgramError(ExecutionState &state, + const llvm::Twine &message, + StateTerminationType reason, + const llvm::Twine &longMessage = "", + const char *suffix = nullptr); /// Call error handler and terminate state in case of execution errors /// (things that should not be possible, like illegal instruction or /// unlowered intrinsic, or unsupported intrinsics, like inline assembly) - void terminateStateOnExecError(ExecutionState &state, - const llvm::Twine &message, - const llvm::Twine &info = ""); + void terminateStateOnExecError( + ExecutionState &state, const llvm::Twine &message, + StateTerminationType = StateTerminationType::Execution); /// Call error handler and terminate state in case of solver errors /// (solver error or timeout) diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp index 00677541..3034dd74 100644 --- a/lib/Core/MergeHandler.cpp +++ b/lib/Core/MergeHandler.cpp @@ -106,7 +106,7 @@ void MergeHandler::addClosedState(ExecutionState *es, for (auto& mState: cpv) { if (mState->merge(*es)) { - executor->terminateStateEarly(*es, "merged state.", StateTerminationType::Merge); + executor->terminateStateEarlyAlgorithm(*es, "merged state.", StateTerminationType::Merge); executor->mergingSearcher->inCloseMerge.erase(es); mergedSuccessful = true; break; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index f4b09f36..7996499c 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -286,8 +286,8 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, KInstruction *target, std::vector<ref<Expr>> &arguments) { assert(arguments.size() == 0 && "invalid number of arguments to abort"); - executor.terminateStateOnError(state, "abort failure", - StateTerminationType::Abort); + executor.terminateStateOnProgramError(state, "abort failure", + StateTerminationType::Abort); } void SpecialFunctionHandler::handleExit(ExecutionState &state, @@ -301,14 +301,14 @@ void SpecialFunctionHandler::handleSilentExit( ExecutionState &state, KInstruction *target, std::vector<ref<Expr>> &arguments) { assert(arguments.size() == 1 && "invalid number of arguments to exit"); - executor.terminateStateEarly(state, "", StateTerminationType::SilentExit); + executor.terminateStateEarlyUser(state, ""); } void SpecialFunctionHandler::handleAssert(ExecutionState &state, KInstruction *target, std::vector<ref<Expr>> &arguments) { assert(arguments.size() == 3 && "invalid number of arguments to _assert"); - executor.terminateStateOnError( + executor.terminateStateOnProgramError( state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), StateTerminationType::Assert); } @@ -318,7 +318,7 @@ void SpecialFunctionHandler::handleAssertFail( std::vector<ref<Expr>> &arguments) { assert(arguments.size() == 4 && "invalid number of arguments to __assert_fail"); - executor.terminateStateOnError( + executor.terminateStateOnProgramError( state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), StateTerminationType::Assert); } @@ -330,7 +330,7 @@ void SpecialFunctionHandler::handleReportError( "invalid number of arguments to klee_report_error"); // arguments[0,1,2,3] are file, line, message, suffix - executor.terminateStateOnError( + executor.terminateStateOnProgramError( state, readStringAtAddress(state, arguments[2]), StateTerminationType::ReportError, "", readStringAtAddress(state, arguments[3]).c_str()); @@ -759,19 +759,17 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, ObjectPair op; if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) { - executor.terminateStateOnError(state, - "check_memory_access: memory error", - StateTerminationType::Ptr, - executor.getAddressInfo(state, address)); + executor.terminateStateOnProgramError( + state, "check_memory_access: memory error", StateTerminationType::Ptr, + executor.getAddressInfo(state, address)); } else { ref<Expr> chk = op.first->getBoundsCheckPointer(address, cast<ConstantExpr>(size)->getZExtValue()); if (!chk->isTrue()) { - executor.terminateStateOnError(state, - "check_memory_access: memory error", - StateTerminationType::Ptr, - executor.getAddressInfo(state, address)); + executor.terminateStateOnProgramError( + state, "check_memory_access: memory error", + StateTerminationType::Ptr, executor.getAddressInfo(state, address)); } } } diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 80723f8a..9f92a127 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -12,6 +12,7 @@ #include "ExecutionState.h" #include "klee/Config/Version.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Module/InstructionInfoTable.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" @@ -432,6 +433,8 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue, void StatsTracker::writeStatsHeader() { #undef BTYPE #define BTYPE(Name,I) << "Branches" #Name " INTEGER," + #undef TCLASS + #define TCLASS(Name,I) << "Termination" #Name " INTEGER," std::ostringstream create, insert; create << "CREATE TABLE stats (" << "Instructions INTEGER," @@ -461,6 +464,7 @@ void StatsTracker::writeStatsHeader() { << "Allocations INTEGER," << "States INTEGER," BRANCH_TYPES + TERMINATION_CLASSES << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; @@ -476,6 +480,8 @@ void StatsTracker::writeStatsHeader() { */ #undef BTYPE #define BTYPE(Name, I) << "Branches" #Name "," + #undef TCLASS + #define TCLASS(Name, I) << "Termination" #Name "," insert << "INSERT OR FAIL INTO stats (" << "Instructions," << "FullBranches," @@ -504,10 +510,13 @@ void StatsTracker::writeStatsHeader() { << "Allocations," << "States," BRANCH_TYPES + TERMINATION_CLASSES << "ArrayHashTime" << ')'; #undef BTYPE #define BTYPE(Name, I) << "?," + #undef TCLASS + #define TCLASS(Name, I) << "?," insert << " VALUES (" << "?," << "?," @@ -536,6 +545,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," BRANCH_TYPES + TERMINATION_CLASSES << "? " << ')'; @@ -551,6 +561,8 @@ time::Span StatsTracker::elapsed() { void StatsTracker::writeStatsLine() { #undef BTYPE #define BTYPE(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::branches ## Name); + #undef TCLASS + #define TCLASS(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::termination ## Name); int arg = 1; sqlite3_bind_int64(insertStmt, arg++, stats::instructions); sqlite3_bind_int64(insertStmt, arg++, fullBranches); @@ -579,6 +591,7 @@ void StatsTracker::writeStatsLine() { sqlite3_bind_int64(insertStmt, arg++, stats::allocations); sqlite3_bind_int64(insertStmt, arg++, ExecutionState::getLastID()); BRANCH_TYPES + TERMINATION_CLASSES #ifdef KLEE_ARRAY_DEBUG sqlite3_bind_int64(insertStmt, arg++, stats::arrayHashTime); #else diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index 20d75adb..f681a06f 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -75,6 +75,15 @@ Legend = [ ('BrRealloc', 'number of forks caused by symbolic reallocation size', "BranchesRealloc"), ('BrFree', 'number of forks caused by freeing a symbolic pointer', "BranchesFree"), ('BrGetVal', 'number of forks caused by user-invoked concretization while seeding', "BranchesGetVal"), + # - termination classes + ('TermExit', 'number of states that reached end of execution path', "TerminationExit"), + ('TermEarly', 'number of early terminated states (e.g. due to memory pressure, state limt)', "TerminationEarly"), + ('TermSolverErr', 'number of states terminated due to solver errors', "TerminationSolverError"), + ('TermProgrErr', 'number of states terminated due to program errors (e.g. division by zero)', "TerminationProgramError"), + ('TermUserErr', 'number of states terminated due to user errors (e.g. misuse of KLEE API)', "TerminationUserError"), + ('TermExecErr', 'number of states terminated due to execution errors (e.g. unsupported intrinsics)', "TerminationExecutionError"), + ('TermEarlyAlgo', 'number of state terminations required by algorithm (e.g. state merging or replaying)', "TerminationEarlyAlgorithm"), + ('TermEarlyUser', 'number of states terminated via klee_silent_exit()', "TerminationEarlyUser"), # - debugging ('TArrayHash(s)', 'time spent hashing arrays (if KLEE_ARRAY_DEBUG enabled, otherwise -1)', "ArrayHashTime"), ('TFork(s)', 'time spent forking states', "ForkTime"), |