diff options
| -rw-r--r-- | include/klee/Core/BranchTypes.h | 33 | ||||
| -rw-r--r-- | lib/Core/CoreStats.cpp | 21 | ||||
| -rw-r--r-- | lib/Core/CoreStats.h | 8 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 6 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 234 | ||||
| -rwxr-xr-x | tools/klee-stats/klee-stats | 11 |
6 files changed, 188 insertions, 125 deletions
diff --git a/include/klee/Core/BranchTypes.h b/include/klee/Core/BranchTypes.h index 5c3e5f32..e8b48cd8 100644 --- a/include/klee/Core/BranchTypes.h +++ b/include/klee/Core/BranchTypes.h @@ -14,9 +14,9 @@ /// \cond DO_NOT_DOCUMENT #define BRANCH_TYPES \ - BTYPE(NONE, 0U) \ - BTYPE(ConditionalBranch, 1U) \ - BTYPE(IndirectBranch, 2U) \ + BTYPEDEFAULT(NONE, 0U) \ + BTYPE(Conditional, 1U) \ + BTYPE(Indirect, 2U) \ BTYPE(Switch, 3U) \ BTYPE(Call, 4U) \ BTYPE(MemOp, 5U) \ @@ -25,7 +25,7 @@ BTYPE(Realloc, 8U) \ BTYPE(Free, 9U) \ BTYPE(GetVal, 10U) \ - MARK(END, 10U) + BMARK(END, 10U) /// \endcond /** @enum BranchType @@ -34,8 +34,8 @@ * | Value | Description | * |---------------------------------|----------------------------------------------------------------------------------------------------| * | `BranchType::NONE` | default value (no branch) | - * | `BranchType::ConditionalBranch` | branch caused by `br` instruction with symbolic condition | - * | `BranchType::IndirectBranch` | branch caused by `indirectbr` instruction with symbolic address | + * | `BranchType::Conditional` | branch caused by `br` instruction with symbolic condition | + * | `BranchType::Indirect` | branch caused by `indirectbr` instruction with symbolic address | * | `BranchType::Switch` | branch caused by `switch` instruction with symbolic value | * | `BranchType::Call` | branch caused by `call` with symbolic function pointer | * | `BranchType::MemOp` | branch caused by memory operation with symbolic address (e.g. multiple resolutions, out-of-bounds) | @@ -46,13 +46,20 @@ * | `BranchType::GetVal` | branch caused by user-invoked concretization while seeding | */ enum class BranchType : std::uint8_t { -/// \cond DO_NOT_DOCUMENT -#define BTYPE(N,I) N = (I), -#define MARK(N,I) N = (I), + /// \cond DO_NOT_DOCUMENT + #define BTYPEDEFAULT(N,I) N = (I), + #define BTYPE(N,I) N = (I), + #define BMARK(N,I) N = (I), BRANCH_TYPES -#undef BTYPE -#undef MARK -/// \endcond + /// \endcond }; -#endif \ No newline at end of file + +#undef BTYPEDEFAULT +#undef BTYPE +#undef BMARK +#define BTYPEDEFAULT(N,I) +#define BTYPE(N,I) +#define BMARK(N,I) + +#endif diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp index 06b8b930..54a9a697 100644 --- a/lib/Core/CoreStats.cpp +++ b/lib/Core/CoreStats.cpp @@ -9,6 +9,9 @@ #include "CoreStats.h" +#include "klee/Support/ErrorHandling.h" + + using namespace klee; Statistic stats::allocations("Allocations", "Alloc"); @@ -28,3 +31,21 @@ Statistic stats::solverTime("SolverTime", "Stime"); Statistic stats::states("States", "States"); Statistic stats::trueBranches("TrueBranches", "Bt"); Statistic stats::uncoveredInstructions("UncoveredInstructions", "Iuncov"); + + +// branch stats and setter + +#undef BTYPE +#define BTYPE(Name,I) Statistic stats::branches ## Name("Branches"#Name, "Br"#Name); +BRANCH_TYPES + +void stats::incBranchStat(BranchType reason, std::uint32_t value) { +#undef BTYPE +#define BTYPE(N,I) case BranchType::N : stats::branches ## N += value; break; + switch (reason) { + BRANCH_TYPES + default: + klee_error("Illegal branch type in incBranchStat(): %hhu", + static_cast<std::uint8_t>(reason)); + } +} diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h index c0dcac7d..15850354 100644 --- a/lib/Core/CoreStats.h +++ b/lib/Core/CoreStats.h @@ -10,6 +10,7 @@ #ifndef KLEE_CORESTATS_H #define KLEE_CORESTATS_H +#include "klee/Core/BranchTypes.h" #include "klee/Statistics/Statistic.h" namespace klee { @@ -49,6 +50,13 @@ namespace stats { /// distance to a function return. extern Statistic minDistToReturn; + /// Count branch types in execution tree. Inhibited branches are ignored. + #undef BTYPE + #define BTYPE(Name,I) extern Statistic branches ## Name; + BRANCH_TYPES + + /// 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 c3a10144..e3af7348 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -900,6 +900,7 @@ void Executor::branch(ExecutionState &state, stats::inhibitedForks += N - 1; } else { stats::forks += N-1; + stats::incBranchStat(reason, N-1); // XXX do proper balance or keep random? result.push_back(&state); @@ -1180,6 +1181,7 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref<Expr> condition, } processTree->attach(current.ptreeNode, falseState, trueState, reason); + stats::incBranchStat(reason, 1); if (pathWriter) { // Need to update the pathOS.id field of falseState, otherwise the same id @@ -2196,7 +2198,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref<Expr> cond = eval(ki, 0, state).value; cond = optimizer.optimizeExpr(cond, false); - Executor::StatePair branches = fork(state, cond, false, BranchType::ConditionalBranch); + Executor::StatePair branches = fork(state, cond, false, BranchType::Conditional); // NOTE: There is a hidden dependency here, markBranchVisited // requires that we still be in the context of the branch @@ -2269,7 +2271,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // fork states std::vector<ExecutionState *> branches; - branch(state, expressions, branches, BranchType::IndirectBranch); + branch(state, expressions, branches, BranchType::Indirect); // terminate error state if (result) { diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 51a0b73c..80723f8a 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -430,35 +430,38 @@ void StatsTracker::markBranchVisited(ExecutionState *visitedTrue, } void StatsTracker::writeStatsHeader() { + #undef BTYPE + #define BTYPE(Name,I) << "Branches" #Name " INTEGER," std::ostringstream create, insert; create << "CREATE TABLE stats (" - << "Instructions INTEGER," - << "FullBranches INTEGER," - << "PartialBranches INTEGER," - << "NumBranches INTEGER," - << "UserTime REAL," - << "NumStates INTEGER," - << "MallocUsage INTEGER," - << "Queries INTEGER," - << "SolverQueries INTEGER," - << "NumQueryConstructs INTEGER," - << "WallTime REAL," - << "CoveredInstructions INTEGER," - << "UncoveredInstructions INTEGER," - << "QueryTime INTEGER," - << "SolverTime INTEGER," - << "CexCacheTime INTEGER," - << "ForkTime INTEGER," - << "ResolveTime INTEGER," - << "QueryCacheMisses INTEGER," - << "QueryCacheHits INTEGER," - << "QueryCexCacheMisses INTEGER," - << "QueryCexCacheHits INTEGER," - << "InhibitedForks INTEGER," - << "ExternalCalls INTEGER," - << "Allocations INTEGER," - << "States INTEGER," - << "ArrayHashTime INTEGER" + << "Instructions INTEGER," + << "FullBranches INTEGER," + << "PartialBranches INTEGER," + << "NumBranches INTEGER," + << "UserTime REAL," + << "NumStates INTEGER," + << "MallocUsage INTEGER," + << "Queries INTEGER," + << "SolverQueries INTEGER," + << "NumQueryConstructs INTEGER," + << "WallTime REAL," + << "CoveredInstructions INTEGER," + << "UncoveredInstructions INTEGER," + << "QueryTime INTEGER," + << "SolverTime INTEGER," + << "CexCacheTime INTEGER," + << "ForkTime INTEGER," + << "ResolveTime INTEGER," + << "QueryCacheMisses INTEGER," + << "QueryCacheHits INTEGER," + << "QueryCexCacheMisses INTEGER," + << "QueryCexCacheHits INTEGER," + << "InhibitedForks INTEGER," + << "ExternalCalls INTEGER," + << "Allocations INTEGER," + << "States INTEGER," + BRANCH_TYPES + << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; if(sqlite3_exec(statsFile, create.str().c_str(), nullptr, nullptr, &zErrMsg)) { @@ -471,62 +474,69 @@ void StatsTracker::writeStatsHeader() { * happen, but if it does this statement will fail with SQLITE_CONSTRAINT error. If this happens you should either * remove the constraints or consider using `IGNORE` mode. */ + #undef BTYPE + #define BTYPE(Name, I) << "Branches" #Name "," insert << "INSERT OR FAIL INTO stats (" - << "Instructions," - << "FullBranches," - << "PartialBranches," - << "NumBranches," - << "UserTime," - << "NumStates," - << "MallocUsage," - << "Queries," - << "SolverQueries," - << "NumQueryConstructs," - << "WallTime," - << "CoveredInstructions," - << "UncoveredInstructions," - << "QueryTime," - << "SolverTime," - << "CexCacheTime," - << "ForkTime," - << "ResolveTime," - << "QueryCacheMisses," - << "QueryCacheHits," - << "QueryCexCacheMisses," - << "QueryCexCacheHits," - << "InhibitedForks," - << "ExternalCalls," - << "Allocations," - << "States," - << "ArrayHashTime" - << ") VALUES (" - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "?," - << "? " + << "Instructions," + << "FullBranches," + << "PartialBranches," + << "NumBranches," + << "UserTime," + << "NumStates," + << "MallocUsage," + << "Queries," + << "SolverQueries," + << "NumQueryConstructs," + << "WallTime," + << "CoveredInstructions," + << "UncoveredInstructions," + << "QueryTime," + << "SolverTime," + << "CexCacheTime," + << "ForkTime," + << "ResolveTime," + << "QueryCacheMisses," + << "QueryCacheHits," + << "QueryCexCacheMisses," + << "QueryCexCacheHits," + << "InhibitedForks," + << "ExternalCalls," + << "Allocations," + << "States," + BRANCH_TYPES + << "ArrayHashTime" + << ')'; + #undef BTYPE + #define BTYPE(Name, I) << "?," + insert << " VALUES (" + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + BRANCH_TYPES + << "? " << ')'; if(sqlite3_prepare_v2(statsFile, insert.str().c_str(), -1, &insertStmt, nullptr) != SQLITE_OK) { @@ -539,36 +549,40 @@ time::Span StatsTracker::elapsed() { } void StatsTracker::writeStatsLine() { - sqlite3_bind_int64(insertStmt, 1, stats::instructions); - sqlite3_bind_int64(insertStmt, 2, fullBranches); - sqlite3_bind_int64(insertStmt, 3, partialBranches); - sqlite3_bind_int64(insertStmt, 4, numBranches); - sqlite3_bind_int64(insertStmt, 5, time::getUserTime().toMicroseconds()); - sqlite3_bind_int64(insertStmt, 6, executor.states.size()); - sqlite3_bind_int64(insertStmt, 7, util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize()); - sqlite3_bind_int64(insertStmt, 8, stats::queries); - sqlite3_bind_int64(insertStmt, 9, stats::solverQueries); - sqlite3_bind_int64(insertStmt, 10, stats::queryConstructs); - sqlite3_bind_int64(insertStmt, 11, elapsed().toMicroseconds()); - sqlite3_bind_int64(insertStmt, 12, stats::coveredInstructions); - sqlite3_bind_int64(insertStmt, 13, stats::uncoveredInstructions); - sqlite3_bind_int64(insertStmt, 14, stats::queryTime); - sqlite3_bind_int64(insertStmt, 15, stats::solverTime); - sqlite3_bind_int64(insertStmt, 16, stats::cexCacheTime); - sqlite3_bind_int64(insertStmt, 17, stats::forkTime); - sqlite3_bind_int64(insertStmt, 18, stats::resolveTime); - sqlite3_bind_int64(insertStmt, 19, stats::queryCacheMisses); - sqlite3_bind_int64(insertStmt, 10, stats::queryCacheHits); - sqlite3_bind_int64(insertStmt, 21, stats::queryCexCacheMisses); - sqlite3_bind_int64(insertStmt, 22, stats::queryCexCacheHits); - sqlite3_bind_int64(insertStmt, 23, stats::inhibitedForks); - sqlite3_bind_int64(insertStmt, 24, stats::externalCalls); - sqlite3_bind_int64(insertStmt, 25, stats::allocations); - sqlite3_bind_int64(insertStmt, 26, ExecutionState::getLastID()); + #undef BTYPE + #define BTYPE(Name,I) sqlite3_bind_int64(insertStmt, arg++, stats::branches ## Name); + int arg = 1; + sqlite3_bind_int64(insertStmt, arg++, stats::instructions); + sqlite3_bind_int64(insertStmt, arg++, fullBranches); + sqlite3_bind_int64(insertStmt, arg++, partialBranches); + sqlite3_bind_int64(insertStmt, arg++, numBranches); + sqlite3_bind_int64(insertStmt, arg++, time::getUserTime().toMicroseconds()); + sqlite3_bind_int64(insertStmt, arg++, executor.states.size()); + sqlite3_bind_int64(insertStmt, arg++, util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize()); + sqlite3_bind_int64(insertStmt, arg++, stats::queries); + sqlite3_bind_int64(insertStmt, arg++, stats::solverQueries); + sqlite3_bind_int64(insertStmt, arg++, stats::queryConstructs); + sqlite3_bind_int64(insertStmt, arg++, elapsed().toMicroseconds()); + sqlite3_bind_int64(insertStmt, arg++, stats::coveredInstructions); + sqlite3_bind_int64(insertStmt, arg++, stats::uncoveredInstructions); + sqlite3_bind_int64(insertStmt, arg++, stats::queryTime); + sqlite3_bind_int64(insertStmt, arg++, stats::solverTime); + sqlite3_bind_int64(insertStmt, arg++, stats::cexCacheTime); + sqlite3_bind_int64(insertStmt, arg++, stats::forkTime); + sqlite3_bind_int64(insertStmt, arg++, stats::resolveTime); + sqlite3_bind_int64(insertStmt, arg++, stats::queryCacheMisses); + sqlite3_bind_int64(insertStmt, arg++, stats::queryCacheHits); + sqlite3_bind_int64(insertStmt, arg++, stats::queryCexCacheMisses); + sqlite3_bind_int64(insertStmt, arg++, stats::queryCexCacheHits); + sqlite3_bind_int64(insertStmt, arg++, stats::inhibitedForks); + sqlite3_bind_int64(insertStmt, arg++, stats::externalCalls); + sqlite3_bind_int64(insertStmt, arg++, stats::allocations); + sqlite3_bind_int64(insertStmt, arg++, ExecutionState::getLastID()); + BRANCH_TYPES #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 27, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, arg++, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 27, -1LL); + sqlite3_bind_int64(insertStmt, arg++, -1LL); #endif int errCode = sqlite3_step(insertStmt); if(errCode != SQLITE_DONE) klee_error("Error writing stats data: %s", sqlite3_errmsg(statsFile)); diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index 629095bc..20d75adb 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -64,6 +64,17 @@ Legend = [ ('Mem(MiB)', 'mebibytes of memory currently used', "MallocUsage"), ('MaxMem(MiB)', 'maximum memory usage', "MaxMem"), ('AvgMem(MiB)', 'average memory usage', "AvgMem"), + # - branch types + ('BrConditional', 'number of forks caused by symbolic branch conditions (br)', "BranchesConditional"), + ('BrIndirect', 'number of forks caused by indirect branches (indirectbr) with symbolic address', "BranchesIndirect"), + ('BrSwitch', 'number of forks caused by switch with symbolic value', "BranchesSwitch"), + ('BrCall', 'number of forks caused by symbolic function pointers', "BranchesCall"), + ('BrMemOp', 'number of forks caused by memory operation with symbolic address', "BranchesMemOp"), + ('BrResolvePointer', 'number of forks caused by symbolic pointers', "BranchesResolvePointer"), + ('BrAlloc', 'number of forks caused by symbolic allocation size', "BranchesAlloc"), + ('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"), # - debugging ('TArrayHash(s)', 'time spent hashing arrays (if KLEE_ARRAY_DEBUG enabled, otherwise -1)', "ArrayHashTime"), ('TFork(s)', 'time spent forking states', "ForkTime"), |