From 91468cf16fb158cd6be5eb9d9c5259f7f88bdf9a Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Wed, 22 Mar 2023 22:21:41 +0000 Subject: [PATCH 01/25] Run KDAlloc/rusage unittest a few times to allow for swapfile interference --- unittests/KDAlloc/rusage.cpp | 43 +++++++++++++++++++++--------------- 1 file changed, 25 insertions(+), 18 deletions(-) diff --git a/unittests/KDAlloc/rusage.cpp b/unittests/KDAlloc/rusage.cpp index fa755b736e..453c5e5d74 100644 --- a/unittests/KDAlloc/rusage.cpp +++ b/unittests/KDAlloc/rusage.cpp @@ -11,7 +11,7 @@ #include "gtest/gtest.h" -#include +#include #include @@ -20,7 +20,7 @@ #if !defined(__has_feature) || \ (!__has_feature(memory_sanitizer) && !__has_feature(address_sanitizer)) -std::size_t write_to_allocations(std::deque &allocations) { +std::size_t write_to_allocations(std::vector &allocations) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); auto initial = ru.ru_minflt; @@ -41,26 +41,33 @@ TEST(KDAllocTest, Rusage) { 0); // 1 GB klee::kdalloc::Allocator allocator = factory.makeAllocator(); - std::deque allocations; + std::vector allocations; for (std::size_t i = 0; i < 1000; ++i) { - auto p = allocator.allocate(16); - allocations.emplace_back(p); + allocations.emplace_back(allocator.allocate(16)); } - auto pageFaults = write_to_allocations(allocations); - - ASSERT_GT(pageFaults, static_cast(0)) - << "No page faults happened"; - ASSERT_EQ(pageFaults, allocations.size()) - << "Number of (minor) page faults and objects differs"; - - factory.getMapping().clear(); - - // try again: this should (again) trigger a minor page fault for every object - auto pageFaultsSecondTry = write_to_allocations(allocations); + // When writing to allocations we should have at least one page fault per + // object, but may have more due to unrelated behavior (e.g., swapping). In + // the hopes that such interference is relatively rare, we try a few times to + // encounter a perfect run, where the number of page faults matches the number + // of allocated objects exactly. + constexpr std::size_t tries = 100; + for (std::size_t i = 0; i < tries; ++i) { + auto pageFaults = write_to_allocations(allocations); + if (pageFaults == allocations.size()) { + // we have a perfect match + return; + } + + ASSERT_GE(pageFaults, allocations.size()) + << "There should be at least as many page faults as allocated objects"; + + factory.getMapping().clear(); + } - ASSERT_EQ(pageFaults, pageFaultsSecondTry) - << "Number of minor page faults in second try differs"; + FAIL() + << "No single try out of " << tries + << " yielded a perfect match between page faults and allocated objects"; } #endif From a91be77e800510db50444b3e1f5ef20dbca0260c Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Wed, 22 Mar 2023 23:41:24 +0000 Subject: [PATCH 02/25] remove obsolete header --- include/klee/Support/FloatEvaluation.h | 264 ------------------------- lib/Core/Executor.cpp | 1 - 2 files changed, 265 deletions(-) delete mode 100644 include/klee/Support/FloatEvaluation.h diff --git a/include/klee/Support/FloatEvaluation.h b/include/klee/Support/FloatEvaluation.h deleted file mode 100644 index d6fcc73c66..0000000000 --- a/include/klee/Support/FloatEvaluation.h +++ /dev/null @@ -1,264 +0,0 @@ -//===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -// FIXME: Ditch this and use APFloat. - -#ifndef KLEE_FLOATEVALUATION_H -#define KLEE_FLOATEVALUATION_H - -#include "IntEvaluation.h" // ints::sext - -#include "klee/ADT/Bits.h" // bits64::truncateToNBits - -#include "llvm/Support/ErrorHandling.h" -#include "llvm/Support/MathExtras.h" - -#include - -namespace klee { -namespace floats { - -// ********************************** // -// *** Pack uint64_t into FP types ** // -// ********************************** // - -// interpret the 64 bits as a double instead of a uint64_t -inline double UInt64AsDouble( uint64_t bits ) { - double ret; - assert( sizeof(bits) == sizeof(ret) ); - memcpy( &ret, &bits, sizeof bits ); - return ret; -} - -// interpret the first 32 bits as a float instead of a uint64_t -inline float UInt64AsFloat( uint64_t bits ) { - uint32_t tmp = bits; // ensure that we read correct bytes - float ret; - assert( sizeof(tmp) == sizeof(ret) ); - memcpy( &ret, &tmp, sizeof tmp ); - return ret; -} - - -// ********************************** // -// *** Pack FP types into uint64_t ** // -// ********************************** // - -// interpret the 64 bits as a uint64_t instead of a double -inline uint64_t DoubleAsUInt64( double d ) { - uint64_t ret; - assert( sizeof(d) == sizeof(ret) ); - memcpy( &ret, &d, sizeof d ); - return ret; -} - -// interpret the 32 bits as a uint64_t instead of as a float (add 32 0s) -inline uint64_t FloatAsUInt64( float f ) { - uint32_t tmp; - assert( sizeof(tmp) == sizeof(f) ); - memcpy( &tmp, &f, sizeof f ); - return (uint64_t)tmp; -} - - -// ********************************** // -// ************ Constants *********** // -// ********************************** // - -const unsigned FLT_BITS = 32; -const unsigned DBL_BITS = 64; - - - -// ********************************** // -// ***** LLVM Binary Operations ***** // -// ********************************** // - -// add of l and r -inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) + UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// difference of l and r -inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) - UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// product of l and r -inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) * UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// signed divide of l by r -inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) / UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// signed modulo of l by r -inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l), UInt64AsFloat(r)) ), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - - -// ********************************** // -// *** LLVM Comparison Operations *** // -// ********************************** // - -// determine if l represents NaN -inline bool isNaN(uint64_t l, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: - return std::isnan(UInt64AsFloat(l)); - case DBL_BITS: - return std::isnan(UInt64AsDouble(l)); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) == UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) != UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) < UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) <= UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) > UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) >= UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - - -// ********************************** // -// *** LLVM Conversion Operations *** // -// ********************************** // - -// truncation of l (which must be a double) to float (casts a double to a float) -inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { - // FIXME: Investigate this, should this not happen? Was a quick - // patch for busybox. - if (inWidth==64 && outWidth==64) { - return l; - } else { - assert(inWidth==64 && "can only truncate from a 64-bit double"); - assert(outWidth==32 && "can only truncate to a 32-bit float"); - float trunc = (float)UInt64AsDouble(l); - return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth); - } -} - -// extension of l (which must be a float) to double (casts a float to a double) -inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) { - // FIXME: Investigate this, should this not happen? Was a quick - // patch for busybox. - if (inWidth==64 && outWidth==64) { - return l; - } else { - assert(inWidth==32 && "can only extend from a 32-bit float"); - assert(outWidth==64 && "can only extend to a 64-bit double"); - double ext = (double)UInt64AsFloat(l); - return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth); - } -} - -// conversion of l to an unsigned integer, rounding towards zero -inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l), outWidth ); - case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth ); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// conversion of l to a signed integer, rounding towards zero -inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l), outWidth); - case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// conversion of l, interpreted as an unsigned int, to a floating point number -inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) { - switch( outWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l), outWidth); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// conversion of l, interpreted as a signed int, to a floating point number -inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) { - switch( outWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -} // end namespace ints -} // end namespace klee - -#endif /* KLEE_FLOATEVALUATION_H */ diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d644d647dd..9322f50ab2 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -49,7 +49,6 @@ #include "klee/Support/Casting.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/FileHandling.h" -#include "klee/Support/FloatEvaluation.h" #include "klee/Support/ModuleUtil.h" #include "klee/Support/OptionCategories.h" #include "klee/System/MemoryUsage.h" From fc3c937892998b984a59cfa740244952ff6071b9 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 14:14:38 +0000 Subject: [PATCH 03/25] stats: add InhibitedForks --- lib/Core/CoreStats.cpp | 1 + lib/Core/CoreStats.h | 3 +++ lib/Core/Executor.cpp | 2 ++ lib/Core/StatsTracker.cpp | 8 ++++++-- tools/klee-stats/klee-stats | 1 + 5 files changed, 13 insertions(+), 2 deletions(-) diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp index 2589d7dac4..720fa1b2e6 100644 --- a/lib/Core/CoreStats.cpp +++ b/lib/Core/CoreStats.cpp @@ -16,6 +16,7 @@ Statistic stats::coveredInstructions("CoveredInstructions", "Icov"); Statistic stats::falseBranches("FalseBranches", "Bf"); Statistic stats::forkTime("ForkTime", "Ftime"); Statistic stats::forks("Forks", "Forks"); +Statistic stats::inhibitedForks("InhibitedForks", "InhibForks"); Statistic stats::instructionRealTime("InstructionRealTimes", "Ireal"); Statistic stats::instructionTime("InstructionTimes", "Itime"); Statistic stats::instructions("Instructions", "I"); diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h index 354706f589..b624d1aac7 100644 --- a/lib/Core/CoreStats.h +++ b/lib/Core/CoreStats.h @@ -30,6 +30,9 @@ namespace stats { /// The number of process forks. extern Statistic forks; + /// Number of inhibited forks. + extern Statistic inhibitedForks; + /// Number of states, this is a "fake" statistic used by istats, it /// isn't normally up-to-date. extern Statistic states; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 9322f50ab2..c3a101448f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -897,6 +897,7 @@ void Executor::branch(ExecutionState &state, result.push_back(nullptr); } } + stats::inhibitedForks += N - 1; } else { stats::forks += N-1; @@ -1074,6 +1075,7 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, addConstraint(current, Expr::createIsZero(condition)); res = Solver::False; } + ++stats::inhibitedForks; } } } diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 539b913c42..18c0a6919f 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -451,6 +451,7 @@ void StatsTracker::writeStatsHeader() { << "ResolveTime INTEGER," << "QueryCexCacheMisses INTEGER," << "QueryCexCacheHits INTEGER," + << "InhibitedForks INTEGER," << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; @@ -484,6 +485,7 @@ void StatsTracker::writeStatsHeader() { << "ResolveTime," << "QueryCexCacheMisses," << "QueryCexCacheHits," + << "InhibitedForks," << "ArrayHashTime" << ") VALUES (" << "?," @@ -505,6 +507,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," << "? " << ')'; @@ -537,10 +540,11 @@ void StatsTracker::writeStatsLine() { sqlite3_bind_int64(insertStmt, 17, stats::resolveTime); sqlite3_bind_int64(insertStmt, 18, stats::queryCexCacheMisses); sqlite3_bind_int64(insertStmt, 19, stats::queryCexCacheHits); + sqlite3_bind_int64(insertStmt, 20, stats::inhibitedForks); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 20, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 21, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 20, -1LL); + sqlite3_bind_int64(insertStmt, 21, -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 22cdaf4310..18fbe5950e 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -47,6 +47,7 @@ Legend = [ ('ActiveStates', 'number of currently active states (0 after successful termination)', "NumStates"), ('MaxActiveStates', 'maximum number of active states', "MaxStates"), ('AvgActiveStates', 'average number of active states', "AvgStates"), + ('InhibitedForks', 'number of inhibited state forks due to e.g. memory pressure', "InhibitedForks"), # - constraint caching/solving ('Queries', 'number of queries issued to the constraint solver', "NumQueries"), ('QueryConstructs', 'number of query constructs for all queries send to the constraint solver', "NumQueryConstructs"), From 7b881cd894ce908a4b4e2d2ad89f90e39905905a Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 14:21:00 +0000 Subject: [PATCH 04/25] stats: add QCacheHits/Misses --- lib/Core/StatsTracker.cpp | 18 +++++++++++++----- tools/klee-stats/klee-stats | 6 ++++-- 2 files changed, 17 insertions(+), 7 deletions(-) diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 18c0a6919f..0cec42223b 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -449,6 +449,8 @@ void StatsTracker::writeStatsHeader() { << "CexCacheTime INTEGER," << "ForkTime INTEGER," << "ResolveTime INTEGER," + << "QueryCacheMisses INTEGER," + << "QueryCacheHits INTEGER," << "QueryCexCacheMisses INTEGER," << "QueryCexCacheHits INTEGER," << "InhibitedForks INTEGER," @@ -483,6 +485,8 @@ void StatsTracker::writeStatsHeader() { << "CexCacheTime," << "ForkTime," << "ResolveTime," + << "QueryCacheMisses," + << "QueryCacheHits," << "QueryCexCacheMisses," << "QueryCexCacheHits," << "InhibitedForks," @@ -508,6 +512,8 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," + << "?," << "? " << ')'; @@ -538,13 +544,15 @@ void StatsTracker::writeStatsLine() { sqlite3_bind_int64(insertStmt, 15, stats::cexCacheTime); sqlite3_bind_int64(insertStmt, 16, stats::forkTime); sqlite3_bind_int64(insertStmt, 17, stats::resolveTime); - sqlite3_bind_int64(insertStmt, 18, stats::queryCexCacheMisses); - sqlite3_bind_int64(insertStmt, 19, stats::queryCexCacheHits); - sqlite3_bind_int64(insertStmt, 20, stats::inhibitedForks); + sqlite3_bind_int64(insertStmt, 18, stats::queryCacheMisses); + sqlite3_bind_int64(insertStmt, 19, stats::queryCacheHits); + sqlite3_bind_int64(insertStmt, 20, stats::queryCexCacheMisses); + sqlite3_bind_int64(insertStmt, 21, stats::queryCexCacheHits); + sqlite3_bind_int64(insertStmt, 22, stats::inhibitedForks); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 21, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 23, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 21, -1LL); + sqlite3_bind_int64(insertStmt, 23, -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 18fbe5950e..b819f69b32 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -52,8 +52,10 @@ Legend = [ ('Queries', 'number of queries issued to the constraint solver', "NumQueries"), ('QueryConstructs', 'number of query constructs for all queries send to the constraint solver', "NumQueryConstructs"), ('AvgSolverQuerySize', 'average number of query constructs per query issued to the constraint solver', "AvgQC"), - ('QCexCMisses', 'Counterexample cache misses', "QueryCexCacheMisses"), - ('QCexCHits', 'Counterexample cache hits', "QueryCexCacheHits"), + ('QCacheMisses', 'Query cache misses', "QueryCacheMisses"), + ('QCacheHits', 'Query cache hits', "QueryCacheHits"), + ('QCexCacheMisses', 'Counterexample cache misses', "QueryCexCacheMisses"), + ('QCexCacheHits', 'Counterexample cache hits', "QueryCexCacheHits"), # - memory ('Mem(MiB)', 'mebibytes of memory currently used', "MallocUsage"), ('MaxMem(MiB)', 'maximum memory usage', "MaxMem"), From 895f095d3d16472b9443bda60854a3230fc7e974 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 14:32:22 +0000 Subject: [PATCH 05/25] stats: add ExternalCalls --- lib/Core/CoreStats.cpp | 1 + lib/Core/CoreStats.h | 3 +++ lib/Core/ExternalDispatcher.cpp | 3 +++ lib/Core/StatsTracker.cpp | 8 ++++++-- tools/klee-stats/klee-stats | 1 + 5 files changed, 14 insertions(+), 2 deletions(-) diff --git a/lib/Core/CoreStats.cpp b/lib/Core/CoreStats.cpp index 720fa1b2e6..06b8b93076 100644 --- a/lib/Core/CoreStats.cpp +++ b/lib/Core/CoreStats.cpp @@ -13,6 +13,7 @@ using namespace klee; Statistic stats::allocations("Allocations", "Alloc"); Statistic stats::coveredInstructions("CoveredInstructions", "Icov"); +Statistic stats::externalCalls("ExternalCalls", "ExtC"); Statistic stats::falseBranches("FalseBranches", "Bf"); Statistic stats::forkTime("ForkTime", "Ftime"); Statistic stats::forks("Forks", "Forks"); diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h index b624d1aac7..c0dcac7d7e 100644 --- a/lib/Core/CoreStats.h +++ b/lib/Core/CoreStats.h @@ -27,6 +27,9 @@ namespace stats { extern Statistic forkTime; extern Statistic solverTime; + /// The number of external calls. + extern Statistic externalCalls; + /// The number of process forks. extern Statistic forks; diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index d286bea95a..d155798e0d 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -8,6 +8,8 @@ //===----------------------------------------------------------------------===// #include "ExternalDispatcher.h" + +#include "CoreStats.h" #include "klee/Config/Version.h" #include "klee/Module/KCallable.h" #include "klee/Module/KModule.h" @@ -158,6 +160,7 @@ ExternalDispatcherImpl::~ExternalDispatcherImpl() { bool ExternalDispatcherImpl::executeCall(KCallable *callable, Instruction *i, uint64_t *args) { + ++stats::externalCalls; dispatchers_ty::iterator it = dispatchers.find(i); if (it != dispatchers.end()) { // Code already JIT'ed for this diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 0cec42223b..907aaa7329 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -454,6 +454,7 @@ void StatsTracker::writeStatsHeader() { << "QueryCexCacheMisses INTEGER," << "QueryCexCacheHits INTEGER," << "InhibitedForks INTEGER," + << "ExternalCalls INTEGER," << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; @@ -490,6 +491,7 @@ void StatsTracker::writeStatsHeader() { << "QueryCexCacheMisses," << "QueryCexCacheHits," << "InhibitedForks," + << "ExternalCalls," << "ArrayHashTime" << ") VALUES (" << "?," @@ -514,6 +516,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," << "? " << ')'; @@ -549,10 +552,11 @@ void StatsTracker::writeStatsLine() { sqlite3_bind_int64(insertStmt, 20, stats::queryCexCacheMisses); sqlite3_bind_int64(insertStmt, 21, stats::queryCexCacheHits); sqlite3_bind_int64(insertStmt, 22, stats::inhibitedForks); + sqlite3_bind_int64(insertStmt, 23, stats::externalCalls); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 23, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 24, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 23, -1LL); + sqlite3_bind_int64(insertStmt, 24, -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 b819f69b32..be30a0ca90 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -35,6 +35,7 @@ Legend = [ ('Branches', 'number of conditional branch (br) instructions in the LLVM bitcode', 'NumBranches'), ('FullBranches', 'number of fully-explored conditional branch (br) instructions in the LLVM bitcode', 'FullBranches'), ('PartialBranches', 'number of partially-explored conditional branch (br) instructions in the LLVM bitcode', 'PartialBranches'), + ('ExternalCalls', 'number of external calls', 'ExternalCalls'), # - time ('TUser(s)', 'total user time', "UserTime"), ('TResolve(s)', 'time spent in object resolution', "ResolveTime"), From 855d33173cae9fd43899a6a96a58f79563560cce Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 16:09:10 +0000 Subject: [PATCH 06/25] stats: rename numQueries/Queries -> SolverQueries, add Queries --- include/klee/Solver/SolverStats.h | 1 + lib/Core/StatsTracker.cpp | 42 +++++++++++++++++-------------- lib/Core/TimingSolver.cpp | 6 +++++ lib/Solver/DummySolver.cpp | 8 +++--- lib/Solver/MetaSMTSolver.cpp | 2 +- lib/Solver/STPSolver.cpp | 2 +- lib/Solver/SolverStats.cpp | 1 + lib/Solver/Z3Solver.cpp | 2 +- tools/kleaver/main.cpp | 2 +- tools/klee-stats/klee-stats | 5 ++-- tools/klee/main.cpp | 2 +- 11 files changed, 43 insertions(+), 30 deletions(-) diff --git a/include/klee/Solver/SolverStats.h b/include/klee/Solver/SolverStats.h index fe14d9e555..fd4a3ab6cc 100644 --- a/include/klee/Solver/SolverStats.h +++ b/include/klee/Solver/SolverStats.h @@ -16,6 +16,7 @@ namespace klee { namespace stats { extern Statistic cexCacheTime; + extern Statistic solverQueries; extern Statistic queries; extern Statistic queriesInvalid; extern Statistic queriesValid; diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 907aaa7329..37a52fffb7 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -439,7 +439,8 @@ void StatsTracker::writeStatsHeader() { << "UserTime REAL," << "NumStates INTEGER," << "MallocUsage INTEGER," - << "NumQueries INTEGER," + << "Queries INTEGER," + << "SolverQueries INTEGER," << "NumQueryConstructs INTEGER," << "WallTime REAL," << "CoveredInstructions INTEGER," @@ -476,7 +477,8 @@ void StatsTracker::writeStatsHeader() { << "UserTime," << "NumStates," << "MallocUsage," - << "NumQueries," + << "Queries," + << "SolverQueries," << "NumQueryConstructs," << "WallTime," << "CoveredInstructions," @@ -517,6 +519,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," << "? " << ')'; @@ -538,25 +541,26 @@ void StatsTracker::writeStatsLine() { 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::queryConstructs); - sqlite3_bind_int64(insertStmt, 10, elapsed().toMicroseconds()); - sqlite3_bind_int64(insertStmt, 11, stats::coveredInstructions); - sqlite3_bind_int64(insertStmt, 12, stats::uncoveredInstructions); - sqlite3_bind_int64(insertStmt, 13, stats::queryTime); - sqlite3_bind_int64(insertStmt, 14, stats::solverTime); - sqlite3_bind_int64(insertStmt, 15, stats::cexCacheTime); - sqlite3_bind_int64(insertStmt, 16, stats::forkTime); - sqlite3_bind_int64(insertStmt, 17, stats::resolveTime); - sqlite3_bind_int64(insertStmt, 18, stats::queryCacheMisses); - sqlite3_bind_int64(insertStmt, 19, stats::queryCacheHits); - sqlite3_bind_int64(insertStmt, 20, stats::queryCexCacheMisses); - sqlite3_bind_int64(insertStmt, 21, stats::queryCexCacheHits); - sqlite3_bind_int64(insertStmt, 22, stats::inhibitedForks); - sqlite3_bind_int64(insertStmt, 23, stats::externalCalls); + 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); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 24, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 25, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 24, -1LL); + sqlite3_bind_int64(insertStmt, 25, -1LL); #endif int errCode = sqlite3_step(insertStmt); if(errCode != SQLITE_DONE) klee_error("Error writing stats data: %s", sqlite3_errmsg(statsFile)); diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index fc31e72d8e..812357ce55 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -15,6 +15,7 @@ #include "klee/Statistics/Statistics.h" #include "klee/Statistics/TimerStatIncrementer.h" #include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" #include "CoreStats.h" @@ -26,6 +27,7 @@ using namespace llvm; bool TimingSolver::evaluate(const ConstraintSet &constraints, ref expr, Solver::Validity &result, SolverQueryMetaData &metaData) { + ++stats::queries; // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? Solver::True : Solver::False; @@ -46,6 +48,7 @@ bool TimingSolver::evaluate(const ConstraintSet &constraints, ref expr, bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref expr, bool &result, SolverQueryMetaData &metaData) { + ++stats::queries; // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE->isTrue() ? true : false; @@ -90,6 +93,7 @@ bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref expr, bool TimingSolver::getValue(const ConstraintSet &constraints, ref expr, ref &result, SolverQueryMetaData &metaData) { + ++stats::queries; // Fast path, to avoid timer and OS overhead. if (ConstantExpr *CE = dyn_cast(expr)) { result = CE; @@ -112,6 +116,7 @@ bool TimingSolver::getInitialValues( const ConstraintSet &constraints, const std::vector &objects, std::vector> &result, SolverQueryMetaData &metaData) { + ++stats::queries; if (objects.empty()) return true; @@ -128,6 +133,7 @@ bool TimingSolver::getInitialValues( std::pair, ref> TimingSolver::getRange(const ConstraintSet &constraints, ref expr, SolverQueryMetaData &metaData) { + ++stats::queries; TimerStatIncrementer timer(stats::solverTime); auto result = solver->getRange(Query(constraints, expr)); metaData.queryCost += timer.delta(); diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp index 60a4fb5141..a845f9017c 100644 --- a/lib/Solver/DummySolver.cpp +++ b/lib/Solver/DummySolver.cpp @@ -30,19 +30,19 @@ class DummySolverImpl : public SolverImpl { DummySolverImpl::DummySolverImpl() {} bool DummySolverImpl::computeValidity(const Query &, Solver::Validity &result) { - ++stats::queries; + ++stats::solverQueries; // FIXME: We should have stats::queriesFail; return false; } bool DummySolverImpl::computeTruth(const Query &, bool &isValid) { - ++stats::queries; + ++stats::solverQueries; // FIXME: We should have stats::queriesFail; return false; } bool DummySolverImpl::computeValue(const Query &, ref &result) { - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; return false; } @@ -50,7 +50,7 @@ bool DummySolverImpl::computeValue(const Query &, ref &result) { bool DummySolverImpl::computeInitialValues( const Query &, const std::vector &objects, std::vector > &values, bool &hasSolution) { - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; return false; } diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 0f78bb5b63..37c22f0e1e 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -194,7 +194,7 @@ bool MetaSMTSolverImpl::computeInitialValues( TimerStatIncrementer t(stats::queryTime); assert(_builder); - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; bool success = true; diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 1353691011..6e62b82bed 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -387,7 +387,7 @@ bool STPSolverImpl::computeInitialValues( for (const auto &constraint : query.constraints) vc_assertFormula(vc, builder->construct(constraint)); - ++stats::queries; + ++stats::solverQueries; ++stats::queryCounterexamples; ExprHandle stp_e = builder->construct(query.expr); diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp index 40f0d53f05..97b8902aa6 100644 --- a/lib/Solver/SolverStats.cpp +++ b/lib/Solver/SolverStats.cpp @@ -12,6 +12,7 @@ using namespace klee; Statistic stats::cexCacheTime("CexCacheTime", "CCtime"); +Statistic stats::solverQueries("SolverQueries", "SQ"); Statistic stats::queries("Queries", "Q"); Statistic stats::queriesInvalid("QueriesInvalid", "Qiv"); Statistic stats::queriesValid("QueriesValid", "Qv"); diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index b628b86ba2..8319e5f35e 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -268,7 +268,7 @@ bool Z3SolverImpl::internalRunSolver( Z3_solver_assert(builder->ctx, theSolver, builder->construct(constraint)); constant_arrays_in_query.visit(constraint); } - ++stats::queries; + ++stats::solverQueries; if (objects) ++stats::queryCounterexamples; diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 22c23422e8..eed4e4c9dd 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -296,7 +296,7 @@ static bool EvaluateInputAST(const char *Filename, delete S; - if (uint64_t queries = *theStatisticManager->getStatisticByName("Queries")) { + if (uint64_t queries = *theStatisticManager->getStatisticByName("SolverQueries")) { llvm::outs() << "--\n" << "total queries = " << queries << '\n' diff --git a/tools/klee-stats/klee-stats b/tools/klee-stats/klee-stats index be30a0ca90..5e49587bb9 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -50,8 +50,9 @@ Legend = [ ('AvgActiveStates', 'average number of active states', "AvgStates"), ('InhibitedForks', 'number of inhibited state forks due to e.g. memory pressure', "InhibitedForks"), # - constraint caching/solving - ('Queries', 'number of queries issued to the constraint solver', "NumQueries"), - ('QueryConstructs', 'number of query constructs for all queries send to the constraint solver', "NumQueryConstructs"), + ('Queries', 'number of queries issued to the solver chain', "Queries"), + ('SolverQueries', 'number of queries issued to the constraint solver', "SolverQueries"), + ('SolverQueryConstructs', 'number of query constructs for all queries send to the constraint solver', "NumQueryConstructs"), ('AvgSolverQuerySize', 'average number of query constructs per query issued to the constraint solver', "AvgQC"), ('QCacheMisses', 'Query cache misses', "QueryCacheMisses"), ('QCacheHits', 'Query cache hits', "QueryCacheHits"), diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 0b76e9041a..ddb1faec34 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1547,7 +1547,7 @@ int main(int argc, char **argv, char **envp) { delete interpreter; uint64_t queries = - *theStatisticManager->getStatisticByName("Queries"); + *theStatisticManager->getStatisticByName("SolverQueries"); uint64_t queriesValid = *theStatisticManager->getStatisticByName("QueriesValid"); uint64_t queriesInvalid = From a88a768c3ea9343db746344f2cc6e41d4c598a8c Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 16:12:12 +0000 Subject: [PATCH 07/25] stats: add Allocations --- lib/Core/StatsTracker.cpp | 8 ++++++-- tools/klee-stats/klee-stats | 1 + 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 37a52fffb7..bc40afd9d4 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -456,6 +456,7 @@ void StatsTracker::writeStatsHeader() { << "QueryCexCacheHits INTEGER," << "InhibitedForks INTEGER," << "ExternalCalls INTEGER," + << "Allocations INTEGER," << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; @@ -494,6 +495,7 @@ void StatsTracker::writeStatsHeader() { << "QueryCexCacheHits," << "InhibitedForks," << "ExternalCalls," + << "Allocations," << "ArrayHashTime" << ") VALUES (" << "?," @@ -520,6 +522,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," << "? " << ')'; @@ -557,10 +560,11 @@ void StatsTracker::writeStatsLine() { 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); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 25, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 26, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 25, -1LL); + sqlite3_bind_int64(insertStmt, 26, -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 5e49587bb9..b08022f4db 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -59,6 +59,7 @@ Legend = [ ('QCexCacheMisses', 'Counterexample cache misses', "QueryCexCacheMisses"), ('QCexCacheHits', 'Counterexample cache hits', "QueryCexCacheHits"), # - memory + ('Allocations', 'number of allocated heap objects of the program under test', "Allocations"), ('Mem(MiB)', 'mebibytes of memory currently used', "MallocUsage"), ('MaxMem(MiB)', 'maximum memory usage', "MaxMem"), ('AvgMem(MiB)', 'average memory usage', "AvgMem"), From ba58e4add3bb2e924b0078146fdcd9b4f6158178 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 16:28:17 +0000 Subject: [PATCH 08/25] stats: rename States -> ActiveStates, add States --- lib/Core/ExecutionState.h | 1 + lib/Core/StatsTracker.cpp | 8 ++++++-- tools/klee-stats/klee-stats | 1 + 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 6d6336dd40..dbe02fd9a8 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -281,6 +281,7 @@ class ExecutionState { std::uint32_t getID() const { return id; }; void setID() { id = nextID++; }; + static std::uint32_t getLastID() { return nextID - 1; }; }; struct ExecutionStateIDCompare { diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index bc40afd9d4..51a0b73cc4 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -457,6 +457,7 @@ void StatsTracker::writeStatsHeader() { << "InhibitedForks INTEGER," << "ExternalCalls INTEGER," << "Allocations INTEGER," + << "States INTEGER," << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; @@ -496,6 +497,7 @@ void StatsTracker::writeStatsHeader() { << "InhibitedForks," << "ExternalCalls," << "Allocations," + << "States," << "ArrayHashTime" << ") VALUES (" << "?," @@ -523,6 +525,7 @@ void StatsTracker::writeStatsHeader() { << "?," << "?," << "?," + << "?," << "? " << ')'; @@ -561,10 +564,11 @@ void StatsTracker::writeStatsLine() { 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()); #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 26, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, 27, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 26, -1LL); + sqlite3_bind_int64(insertStmt, 27, -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 b08022f4db..629095bc0a 100755 --- a/tools/klee-stats/klee-stats +++ b/tools/klee-stats/klee-stats @@ -45,6 +45,7 @@ Legend = [ ('TQuery(s)', 'time spent in the constraint solver', "QueryTime"), ('TSolver(s)', 'time spent in the solver chain (incl. caches and constraint solver)', "SolverTime"), # - states + ('States', 'number of created states', "States"), ('ActiveStates', 'number of currently active states (0 after successful termination)', "NumStates"), ('MaxActiveStates', 'maximum number of active states', "MaxStates"), ('AvgActiveStates', 'average number of active states', "AvgStates"), From 4749068700db333a47b034f047eed154de4ad2c8 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 7 Jan 2022 18:58:13 +0000 Subject: [PATCH 09/25] stats: add branch type stats --- include/klee/Core/BranchTypes.h | 33 +++-- lib/Core/CoreStats.cpp | 21 +++ lib/Core/CoreStats.h | 8 ++ lib/Core/Executor.cpp | 6 +- lib/Core/StatsTracker.cpp | 234 +++++++++++++++++--------------- 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 5c3e5f32a0..e8b48cd83b 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 06b8b93076..54a9a69720 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(reason)); + } +} diff --git a/lib/Core/CoreStats.h b/lib/Core/CoreStats.h index c0dcac7d7e..1585035491 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 c3a101448f..e3af734804 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 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 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 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 51a0b73cc4..80723f8a7b 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 629095bc0a..20d75adb10 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"), From a6f0612026cac27a1c997517420bfe5c9d254944 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Mon, 10 Jan 2022 15:19:46 +0000 Subject: [PATCH 10/25] tests: add Feature/KleeStatsBranches.c --- test/Feature/KleeStatsBranches.c | 84 ++++++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) create mode 100644 test/Feature/KleeStatsBranches.c diff --git a/test/Feature/KleeStatsBranches.c b/test/Feature/KleeStatsBranches.c new file mode 100644 index 0000000000..a1bf2721f5 --- /dev/null +++ b/test/Feature/KleeStatsBranches.c @@ -0,0 +1,84 @@ +// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-no-tests --output-dir=%t.klee-out %t.bc 2> %t.log +// RUN: %klee-stats --print-columns 'BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal' --table-format=csv %t.klee-out > %t.stats +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats %s + +#include "klee/klee.h" + +#include + + +void foo(void) {} +void bar(void) {} + +int memop(void) { + int *p; + klee_make_symbolic(&p, sizeof(p), "p"); + return *p; +} + + +int main(void) { + // alloc + size_t size0; + klee_make_symbolic(&size0, sizeof(size_t), "size0"); + klee_assume(size0 < 10); + void *p; + + // realloc + size_t size1; + klee_make_symbolic(&size1, sizeof(size_t), "size1"); + klee_assume(size1 < 20); + + // conditional + int cond; + klee_make_symbolic(&cond, sizeof(cond), "cond"); + + // switch + int sw_cond; + klee_make_symbolic(&sw_cond, sizeof(sw_cond), "sw_cond"); + + // call + void (*fptr)(void); + klee_make_symbolic(&fptr, sizeof(fptr), "fptr"); + klee_assume((fptr == &foo) | (fptr == &bar)); + + // indirectbr + void *lptr; + klee_make_symbolic(&lptr, sizeof(lptr), "lptr"); + klee_assume((lptr == &&one) | (lptr == &&two)); + goto *lptr; + + +one: + p = malloc(size0); + if (p) { + p = realloc(p, size1); + if (p) { + // free + klee_make_symbolic(&p, sizeof(p), "p"); + free(p); + } + } + + return 1; + +two: + switch (sw_cond) { + case 8: memop(); break; // memop + case 15: (*fptr)(); break; + default: { + int c = 42; + // conditional + if (cond) c++; + return c; + } + } + + return 2; +} + +// Check that we create branches +// CHECK-STATS: BrConditional,BrIndirect,BrSwitch,BrCall,BrMemOp,BrResolvePointer,BrAlloc,BrRealloc,BrFree,BrGetVal +// CHECK-STATS: 1,1,2,1,{{[1-9][0-9]*}},{{[1-9][0-9]*}},2,1,1,0 From 3a1965c62540ef3fa3ec857f2b7d055cbbb68939 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Tue, 11 Jan 2022 09:09:44 +0000 Subject: [PATCH 11/25] stats: add termination class stats --- include/klee/Core/TerminationTypes.h | 110 +++++++++++++-------- lib/Core/CoreStats.cpp | 8 +- lib/Core/CoreStats.h | 6 ++ lib/Core/Executor.cpp | 139 ++++++++++++++++++--------- lib/Core/Executor.h | 41 ++++++-- lib/Core/MergeHandler.cpp | 2 +- lib/Core/SpecialFunctionHandler.cpp | 26 +++-- lib/Core/StatsTracker.cpp | 13 +++ 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 4fe5583a99..25e5ef4a5d 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -12,51 +12,85 @@ #include + +#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 54a9a69720..48eb1e85b6 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(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 1585035491..609e976a6a 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 e3af734804..a3f91f20c2 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -436,6 +436,7 @@ llvm::cl::bits 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= 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(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 c821b987bb..28a7d56df9 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -410,7 +410,8 @@ class Executor : public Interpreter { 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 @@ class Executor : public Interpreter { /// 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 0067754137..3034dd7457 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 f4b09f367e..7996499cc8 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -286,8 +286,8 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, KInstruction *target, std::vector> &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> &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> &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> &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(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 chk = op.first->getBoundsCheckPointer(address, cast(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 80723f8a7b..9f92a12775 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 20d75adb10..f681a06f44 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"), From 58d454647ff1465128423fa02896f84e5d3b989a Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Tue, 11 Jan 2022 19:28:24 +0000 Subject: [PATCH 12/25] tests: add Feature/KleeStatsTermClasses.c --- test/Feature/KleeStatsTermClasses.c | 89 +++++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) create mode 100644 test/Feature/KleeStatsTermClasses.c diff --git a/test/Feature/KleeStatsTermClasses.c b/test/Feature/KleeStatsTermClasses.c new file mode 100644 index 0000000000..1606128c05 --- /dev/null +++ b/test/Feature/KleeStatsTermClasses.c @@ -0,0 +1,89 @@ +// RUN: %clang %s -fsanitize=unsigned-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --max-stack-frames=15 --switch-type=simple --search=dfs --use-merge --ubsan-runtime --write-no-tests --output-dir=%t.klee-out %t.bc 2> %t.log +// RUN: %klee-stats --print-columns 'TermExit,TermEarly,TermSolverErr,TermProgrErr,TermUserErr,TermExecErr,TermEarlyAlgo,TermEarlyUser' --table-format=csv %t.klee-out > %t.stats +// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.stats %s + + +#pragma GCC diagnostic ignored "-Wimplicit-function-declaration" +#pragma GCC diagnostic ignored "-Winfinite-recursion" + +// do not #include "klee/klee.h" to misuse API + +#include +#include +#include +#include + +const char *ro_str = "hi"; +int global[3]; + + +void max_depth(int a) { + max_depth(a + 1); // Early (MaxDepth) +} + +unsigned mul(unsigned a, unsigned b) { + uint32_t r = a * b; + return r; +} + +void merge() { + int cond; + int a = 42; + klee_make_symbolic(&cond, sizeof(cond), "merge_cond"); + + klee_open_merge(); + if (cond == 8) a++; + else a--; + klee_close_merge(); // EarlyAlgorithm (Merge) + // (normal) Exit +} + +void bogus_external(); + + +int main(void) { + int cond; + klee_make_symbolic(&cond, sizeof(cond), "cond"); + + switch(cond) { + case __LINE__: + max_depth(17); + case __LINE__: + assert(0); // ProgErr (Assert) + break; + case __LINE__: + abort(); // ProgErr (Abort) + case __LINE__: + free(global); // ProgErr (Free) + case __LINE__: { + unsigned a = UINT_MAX, b = UINT_MAX, c; + c = mul(a, b); // ProgErr (Overflow) + } + case __LINE__: + free((void*)0xdeadbeef); // ProgErr (Ptr) + break; + case __LINE__: { + char *p = (char*)ro_str; + p[0] = '!'; // ProgErr (ReadOnly) + } + case __LINE__: + klee_report_error(__FILE__, __LINE__, "Report Error", "report.err"); // ProgErr (Report) + case __LINE__: + klee_make_symbolic(1); // UserErr + case __LINE__: + bogus_external(); // ExecErr (External) + case __LINE__: + merge(); + break; + case __LINE__: + klee_silent_exit(0); // EarlyUser + default: + return 0; // (normal) Exit + } +} + +// Check termination classes +// CHECK-STATS: TermExit,TermEarly,TermSolverErr,TermProgrErr,TermUserErr,TermExecErr,TermEarlyAlgo,TermEarlyUser +// CHECK-STATS: 2,1,0,7,1,1,1,1 From 0ca2dc8176a08a0d4fcaa90807e770a5809d95cf Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 21 Mar 2023 20:32:09 +0000 Subject: [PATCH 13/25] Remove model_version from the POSIX runtime, as we have never used it. --- runtime/POSIX/fd.h | 1 - runtime/POSIX/fd_init.c | 9 ------- runtime/Runtest/intrinsics.c | 7 ------ .../libkleeruntest/replay_posix_runtime.c | 5 ++-- tools/klee-replay/file-creator.c | 2 +- tools/klee-replay/klee-replay.c | 25 +++++-------------- tools/ktest-gen/ktest-gen.cpp | 2 -- tools/ktest-randgen/ktest-randgen.cpp | 1 - 8 files changed, 9 insertions(+), 43 deletions(-) diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h index 5fa428744c..87d967ee3a 100644 --- a/runtime/POSIX/fd.h +++ b/runtime/POSIX/fd.h @@ -93,7 +93,6 @@ typedef struct { typedef struct { exe_file_t fds[MAX_FDS]; mode_t umask; /* process umask */ - unsigned version; /* If set, writes execute as expected. Otherwise, writes extending the file size only change the contents up to the initial size. The file offset is always incremented correctly. */ diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index a8d557e7f2..a064e42b90 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -36,7 +36,6 @@ exe_sym_env_t __exe_env = { { 1, eOpen | eWriteable, 0, 0}, { 2, eOpen | eWriteable, 0, 0}}, 022, - 0, 0 }; @@ -96,12 +95,6 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, dfile->stat = s; } -static unsigned __sym_uint32(const char *name) { - unsigned x; - klee_make_symbolic(&x, sizeof x, name); - return x; -} - /* n_files: number of symbolic input files, excluding stdin file_length: size in bytes of each symbolic file, including stdin sym_stdout_flag: 1 if stdout should be symbolic, 0 otherwise @@ -168,6 +161,4 @@ void klee_init_fds(unsigned n_files, unsigned file_length, else __exe_fs.sym_stdout = NULL; __exe_env.save_all_writes = save_all_writes_flag; - __exe_env.version = __sym_uint32("model_version"); - klee_assume(__exe_env.version == 1); } diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index 2442db0cb2..18eb3cff1a 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -109,13 +109,6 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) { break; } else { KTestObject *o = &testData->objects[testPosition]; - if (strcmp("model_version", o->name) == 0 && - strcmp("model_version", name) != 0) { - // Skip over this KTestObject because we've hit - // `model_version` which is from the POSIX runtime - // and the caller didn't ask for it. - continue; - } if (strcmp(name, o->name) != 0) { report_internal_error( "object name mismatch. Requesting \"%s\" but returning \"%s\"", diff --git a/test/Replay/libkleeruntest/replay_posix_runtime.c b/test/Replay/libkleeruntest/replay_posix_runtime.c index 570462575c..39b8d18ff8 100644 --- a/test/Replay/libkleeruntest/replay_posix_runtime.c +++ b/test/Replay/libkleeruntest/replay_posix_runtime.c @@ -27,9 +27,8 @@ int main(int argc, char** argv) { return 0; } -// CHECKMODEL: num objects: 2 -// CHECKMODEL: object 0: name: {{b*}}'model_version' -// CHECKMODEL: object 1: name: {{b*}}'x' +// CHECKMODEL: num objects: 1 +// CHECKMODEL: object 0: name: {{b*}}'x' // TESTONE: x is not 0 // TESTTWO: x is 0 diff --git a/tools/klee-replay/file-creator.c b/tools/klee-replay/file-creator.c index a1685a02a4..5e848964c6 100644 --- a/tools/klee-replay/file-creator.c +++ b/tools/klee-replay/file-creator.c @@ -301,7 +301,7 @@ static int create_reg_file(const char *fname, exe_disk_file_t *dfile, fprintf(stderr, "KLEE-REPLAY: NOTE: Creating file %s of length %d\n", fname, flen); // Open in RDWR just in case we have to end up using this fd. - if (__exe_env.version == 0 && mode == 0) + if (mode == 0) mode = 0644; int fd = open(fname, O_CREAT | O_RDWR, mode); diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c index 72eeb17ee6..82c638c25e 100644 --- a/tools/klee-replay/klee-replay.c +++ b/tools/klee-replay/klee-replay.c @@ -466,30 +466,17 @@ void klee_posix_prefer_cex(void *buffer, uintptr_t condition) { } void klee_make_symbolic(void *addr, size_t nbytes, const char *name) { - /* XXX remove model version code once new tests gen'd */ if (obj_index >= input->numObjects) { - if (strcmp("model_version", name) == 0) { - assert(nbytes == 4); - *((int*) addr) = 0; - } else { __emit_error("ran out of appropriate inputs"); - } } else { KTestObject *boo = &input->objects[obj_index]; - - if (strcmp("model_version", name) == 0 && - strcmp("model_version", boo->name) != 0) { - assert(nbytes == 4); - *((int*) addr) = 0; + if (boo->numBytes != nbytes) { + fprintf(stderr, "KLEE-REPLAY: ERROR: make_symbolic mismatch, different sizes: " + "%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes); + exit(1); } else { - if (boo->numBytes != nbytes) { - fprintf(stderr, "KLEE-REPLAY: ERROR: make_symbolic mismatch, different sizes: " - "%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes); - exit(1); - } else { - memcpy(addr, boo->bytes, nbytes); - obj_index++; - } + memcpy(addr, boo->bytes, nbytes); + obj_index++; } } } diff --git a/tools/ktest-gen/ktest-gen.cpp b/tools/ktest-gen/ktest-gen.cpp index 331ff7b1cd..d127c0e5e0 100644 --- a/tools/ktest-gen/ktest-gen.cpp +++ b/tools/ktest-gen/ktest-gen.cpp @@ -303,8 +303,6 @@ int main(int argc, char *argv[]) { b.numArgs = argv_copy_idx; b.args = argv_copy; - push_range(&b, "model_version", 1); - if (!kTest_toFile(&b, bout_file ? bout_file : "file.bout")) assert(0); diff --git a/tools/ktest-randgen/ktest-randgen.cpp b/tools/ktest-randgen/ktest-randgen.cpp index 9b7260eb36..6146d35d6d 100644 --- a/tools/ktest-randgen/ktest-randgen.cpp +++ b/tools/ktest-randgen/ktest-randgen.cpp @@ -281,7 +281,6 @@ int main(int argc, char *argv[]) { push_random_obj(&b, "stdout", 1024, 1024); push_obj(&b, "stdout-stat", sizeof(struct stat), (unsigned char *)&s); } - push_range(&b, "model_version", 1); if (!kTest_toFile(&b, bout_file ? bout_file : "random.bout")) { error_exit("Error in storing data into random.bout\n"); From 76f05738dd0aaedd174af4d12dd37dd42836f47f Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Wed, 22 Mar 2023 23:00:09 +0000 Subject: [PATCH 14/25] fix unused variable warning --- runtime/POSIX/fd.c | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c index 0aba0ade9c..be13a40bca 100644 --- a/runtime/POSIX/fd.c +++ b/runtime/POSIX/fd.c @@ -830,8 +830,6 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) { return bytes; } else { off64_t os_pos = f->off - 4096; - int res; - off64_t s = 0; /* For reasons which I really don't understand, if I don't memset this then sometimes the kernel returns d_ino==0 for @@ -841,9 +839,10 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) { Even more bizarre, interchanging the memset and the seek also case strange behavior. Really should be debugged properly. */ memset(dirp, 0, count); - s = syscall(__NR_lseek, f->fd, os_pos, SEEK_SET); + off64_t s = syscall(__NR_lseek, f->fd, os_pos, SEEK_SET); + (void)s; assert(s != (off64_t) -1); - res = syscall(__NR_getdents64, f->fd, dirp, count); + int res = syscall(__NR_getdents64, f->fd, dirp, count); if (res > -1) { int pos = 0; f->off = syscall(__NR_lseek, f->fd, 0, SEEK_CUR); From c9ce3b462de2372828e65b27acddfe3971813b3c Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 23 Mar 2023 17:20:09 +0000 Subject: [PATCH 15/25] Transition to GitHub Container Registry hosting --- .github/workflows/build.yaml | 2 +- Dockerfile | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index 05fb58c048..96122bcb48 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -10,7 +10,7 @@ on: # Defaults for building KLEE env: BASE_IMAGE: ubuntu:jammy-20230126 - REPOSITORY: klee + REPOSITORY: ghcr.io/klee COVERAGE: 0 DISABLE_ASSERTIONS: 0 ENABLE_DOXYGEN: 0 diff --git a/Dockerfile b/Dockerfile index a10ce3c8d0..d58fd2458a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,11 +1,11 @@ -FROM klee/llvm:110_O_D_A_ubuntu_jammy-20230126 as llvm_base -FROM klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_base -FROM klee/uclibc:klee_uclibc_v1.3_110_ubuntu_jammy-20230126 as uclibc_base -FROM klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 as tcmalloc_base -FROM klee/stp:2.3.3_ubuntu_jammy-20230126 as stp_base -FROM klee/z3:4.8.15_ubuntu_jammy-20230126 as z3_base -FROM klee/libcxx:110_ubuntu_jammy-20230126 as libcxx_base -FROM klee/sqlite:3400100_ubuntu_jammy-20230126 as sqlite3_base +FROM ghcr.io/klee/llvm:110_O_D_A_ubuntu_jammy-20230126 as llvm_base +FROM ghcr.io/klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_base +FROM ghcr.io/klee/uclibc:klee_uclibc_v1.3_110_ubuntu_jammy-20230126 as uclibc_base +FROM ghcr.io/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 as tcmalloc_base +FROM ghcr.io/klee/stp:2.3.3_ubuntu_jammy-20230126 as stp_base +FROM ghcr.io/klee/z3:4.8.15_ubuntu_jammy-20230126 as z3_base +FROM ghcr.io/klee/libcxx:110_ubuntu_jammy-20230126 as libcxx_base +FROM ghcr.io/klee/sqlite:3400100_ubuntu_jammy-20230126 as sqlite3_base FROM llvm_base as intermediate COPY --from=gtest_base /tmp /tmp/ COPY --from=uclibc_base /tmp /tmp/ From 721b2fc39451ecfc4cb84ec32138011f160913f8 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 23 Mar 2023 18:57:57 +0000 Subject: [PATCH 16/25] Fix detection and installation of Ubuntu-provided llvm/clang packages --- scripts/build/p-llvm-linux-ubuntu.inc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/build/p-llvm-linux-ubuntu.inc b/scripts/build/p-llvm-linux-ubuntu.inc index 1af095f985..440afbd4c3 100644 --- a/scripts/build/p-llvm-linux-ubuntu.inc +++ b/scripts/build/p-llvm-linux-ubuntu.inc @@ -56,7 +56,7 @@ install_binary_artifact_llvm() { # Check if package in standard repository otherwise use upstream with_sudo apt-get update -y - if ! apt-cache show "llvm${version}"; then + if ! apt-cache show "llvm-${version}"; then if [[ -z "$(which wget)" ]]; then # Add certificate with_sudo apt-get update -y @@ -82,10 +82,10 @@ install_binary_artifact_llvm() { fi dependencies=( - "llvm${version}" - "llvm${version}-dev" - "llvm${version}-runtime" - "clang${version}" + "llvm-${version}" + "llvm-${version}-dev" + "llvm-${version}-runtime" + "clang-${version}" ) #Install essential dependencies From 7c9ce86abd16624a6d6ee509b3dce86d191568ca Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Fri, 24 Mar 2023 04:45:44 +0000 Subject: [PATCH 17/25] fix unused variables warning --- tools/klee-replay/file-creator.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tools/klee-replay/file-creator.c b/tools/klee-replay/file-creator.c index 5e848964c6..02531ab696 100644 --- a/tools/klee-replay/file-creator.c +++ b/tools/klee-replay/file-creator.c @@ -172,6 +172,7 @@ static int create_char_dev(const char *fname, exe_disk_file_t *dfile, struct termios mode; int res = tcgetattr(aslave, &mode); + (void)res; assert(!res); mode.c_iflag = IGNBRK; #if defined(__APPLE__) || defined(__FreeBSD__) @@ -183,6 +184,7 @@ static int create_char_dev(const char *fname, exe_disk_file_t *dfile, mode.c_cc[VMIN] = 1; mode.c_cc[VTIME] = 0; res = tcsetattr(aslave, TCSANOW, &mode); + (void)res; assert(res == 0); } From 67ec44723e9ce232f067964e7e9fb26090be305d Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 24 Mar 2023 14:27:17 +0000 Subject: [PATCH 18/25] tests: add some missing headers --- test/Coverage/ReplayOutDir.c | 2 ++ test/Feature/AddressOfLabelsSymbolic.c | 2 ++ test/Feature/ExprLogging.c | 2 ++ test/Feature/WithLibc.c | 5 +++++ test/Feature/arithmetic-right-overshift-sym-conc.c | 3 +++ test/Runtime/klee-libc/bcmp.c | 2 ++ test/regression/2016-06-28-div-zero-bug.c | 2 ++ 7 files changed, 18 insertions(+) diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c index 6476f32fb6..d2e34b6ec3 100644 --- a/test/Coverage/ReplayOutDir.c +++ b/test/Coverage/ReplayOutDir.c @@ -3,6 +3,8 @@ // RUN: %klee --output-dir=%t1.out %t1.bc // RUN: %klee --output-dir=%t1.replay --replay-ktest-dir=%t1.out %t1.bc +#include "klee/klee.h" + int main() { int i; klee_make_symbolic(&i, sizeof i, "i"); diff --git a/test/Feature/AddressOfLabelsSymbolic.c b/test/Feature/AddressOfLabelsSymbolic.c index 0b24a42d62..1097a189bc 100644 --- a/test/Feature/AddressOfLabelsSymbolic.c +++ b/test/Feature/AddressOfLabelsSymbolic.c @@ -4,6 +4,8 @@ // RUN: FileCheck %s -check-prefix=CHECK-MSG --input-file=%t.log // RUN: FileCheck %s -check-prefix=CHECK-ERR --input-file=%t.stderr.log +#include "klee/klee.h" + #include int main(void) { diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index 70aaa49be3..d892272a88 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -11,6 +11,8 @@ // RUN: grep "^; Query" %t.klee-out/all-queries.smt2 | wc -l | grep -q 17 // RUN: grep "^; Query" %t.klee-out/solver-queries.smt2 | wc -l | grep -q 17 +#include "klee/klee.h" + #include int constantArr[16 ] = { diff --git a/test/Feature/WithLibc.c b/test/Feature/WithLibc.c index bb1c66c0ca..2babbe629f 100644 --- a/test/Feature/WithLibc.c +++ b/test/Feature/WithLibc.c @@ -4,6 +4,11 @@ // RUN: echo "good" > %t3.good // RUN: diff %t3.log %t3.good +#include "klee/klee.h" + +#include +#include + int main() { char buf[4]; char *s = "foo"; diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c index c58f13a13c..efe946f263 100644 --- a/test/Feature/arithmetic-right-overshift-sym-conc.c +++ b/test/Feature/arithmetic-right-overshift-sym-conc.c @@ -3,6 +3,9 @@ // RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc // RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt // RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info + +#include "klee/klee.h" + #include #include diff --git a/test/Runtime/klee-libc/bcmp.c b/test/Runtime/klee-libc/bcmp.c index d0f5d7e59e..1cc72aa189 100644 --- a/test/Runtime/klee-libc/bcmp.c +++ b/test/Runtime/klee-libc/bcmp.c @@ -4,6 +4,8 @@ // test bcmp for sizes including zero +#include "klee/klee.h" + #include #include #include diff --git a/test/regression/2016-06-28-div-zero-bug.c b/test/regression/2016-06-28-div-zero-bug.c index 6e2e8c5ec5..dfab14d38c 100644 --- a/test/regression/2016-06-28-div-zero-bug.c +++ b/test/regression/2016-06-28-div-zero-bug.c @@ -6,6 +6,8 @@ // See https://github.com/klee/klee/issues/308 // and https://github.com/stp/stp/issues/206 +#include "klee/klee.h" + int b, a, g; int *c = &b, *d = &b, *f = &a; From 89ebbb9de69b4de83e97f068cd2cbcdb7b3d1fb9 Mon Sep 17 00:00:00 2001 From: Jiri Slaby Date: Wed, 22 Mar 2023 09:48:50 +0100 Subject: [PATCH 19/25] (gcc-13) include cstdint for *int*_t Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' --- include/klee/Core/Interpreter.h | 1 + include/klee/Statistics/Statistic.h | 1 + 2 files changed, 2 insertions(+) diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index f14e3d887b..04fdef8803 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -9,6 +9,7 @@ #ifndef KLEE_INTERPRETER_H #define KLEE_INTERPRETER_H +#include #include #include #include diff --git a/include/klee/Statistics/Statistic.h b/include/klee/Statistics/Statistic.h index bbb67116db..e675b06741 100644 --- a/include/klee/Statistics/Statistic.h +++ b/include/klee/Statistics/Statistic.h @@ -10,6 +10,7 @@ #ifndef KLEE_STATISTIC_H #define KLEE_STATISTIC_H +#include #include namespace klee { From dfd2aea9e73c00634f81c6388587713ad737d4b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Luk=C3=A1=C5=A1=20Zaoral?= Date: Sat, 25 Mar 2023 18:33:46 +0100 Subject: [PATCH 20/25] Core/Executor: long double on i686 must be aligned to 4 bytes According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` --- lib/Core/Executor.cpp | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index a3f91f20c2..cdf012a5c5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1960,17 +1960,16 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, argWidth = arguments[k]->getWidth(); } - if (WordSize == Expr::Int32) { - offsets[k] = size; - size += Expr::getMinBytesForWidth(argWidth); - } else { #if LLVM_VERSION_CODE >= LLVM_VERSION(11, 0) - MaybeAlign ma = cb.getParamAlign(k); - unsigned alignment = ma ? ma->value() : 0; + MaybeAlign ma = cb.getParamAlign(k); + unsigned alignment = ma ? ma->value() : 0; #else - unsigned alignment = cb.getParamAlignment(k); + unsigned alignment = cb.getParamAlignment(k); #endif + if (WordSize == Expr::Int32 && !alignment) + alignment = 4; + else { // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a // 16 byte boundary if alignment needed by type exceeds 8 byte // boundary. @@ -1981,10 +1980,14 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, if (!alignment) alignment = 8; + } - size = llvm::alignTo(size, alignment); - offsets[k] = size; + size = llvm::alignTo(size, alignment); + offsets[k] = size; + if (WordSize == Expr::Int32) + size += Expr::getMinBytesForWidth(argWidth); + else { // AMD64-ABI 3.5.7p5: Step 9. Set l->overflow_arg_area to: // l->overflow_arg_area + sizeof(type) // Step 10. Align l->overflow_arg_area upwards to an 8 byte boundary. From 13cfabb17dfb5305cbc8ddc2a2ab94b527f3f30e Mon Sep 17 00:00:00 2001 From: Jan Macku Date: Sun, 11 Sep 2022 17:19:38 +0200 Subject: [PATCH 21/25] ci(lint): add shell linter - Differential ShellCheck It performs differential ShellCheck scans and report results directly in pull request. documentation: https://github.com/redhat-plumbers-in-action/differential-shellcheck Signed-off-by: Jan Macku --- .github/workflows/differential-shellcheck.yml | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 .github/workflows/differential-shellcheck.yml diff --git a/.github/workflows/differential-shellcheck.yml b/.github/workflows/differential-shellcheck.yml new file mode 100644 index 0000000000..2dd92e9b5b --- /dev/null +++ b/.github/workflows/differential-shellcheck.yml @@ -0,0 +1,31 @@ +# Doc: https://github.com/redhat-plumbers-in-action/differential-shellcheck#usage +--- + +name: Differential ShellCheck +on: + push: + branches: [master] + pull_request: + branches: [master] + +permissions: + contents: read + +jobs: + lint: + runs-on: ubuntu-latest + + permissions: + security-events: write + + steps: + - name: Repository checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + + - name: Differential ShellCheck + uses: redhat-plumbers-in-action/differential-shellcheck@v4 + with: + severity: warning + token: ${{ secrets.GITHUB_TOKEN }} From 66e1044824d07697e6745a516451d75a21808938 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Julian=20B=C3=BCning?= Date: Wed, 29 Mar 2023 18:50:43 +0200 Subject: [PATCH 22/25] fix CMake: -UNDEBUG --- CMakeLists.txt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 024d8a5003..e6daa815e6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -90,8 +90,9 @@ list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules") option(ENABLE_KLEE_ASSERTS "Enable KLEE assertions" ON) if (ENABLE_KLEE_ASSERTS) message(STATUS "KLEE assertions enabled") - # We have to add the undefine to the flags, otherwise "-D-UDNDEBUG" will be added - list(APPEND KLEE_COMPONENT_CXX_FLAGS "-UDNDEBUG") + # We have to undefine `NDEBUG` (which CMake adds by default) using `FLAGS` + # and not `DEFINES` since `target_compile_definitions` does not support `-U`. + list(APPEND KLEE_COMPONENT_CXX_FLAGS "-UNDEBUG") else() message(STATUS "KLEE assertions disabled") list(APPEND KLEE_COMPONENT_CXX_DEFINES "-DNDEBUG") From 2aa5b7b83da9d3036c5b90df7be0a1e6a49d058f Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Fri, 24 Mar 2023 04:43:46 +0000 Subject: [PATCH 23/25] Prevent fallthrough warning --- lib/Expr/Parser.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 7ef56849e7..937abdec31 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -21,6 +21,7 @@ #include "llvm/Support/raw_ostream.h" #include +#include #include #include @@ -999,11 +1000,12 @@ ExprResult ParserImpl::ParseParenExpr(TypeResult FIXME_UNUSED) { if (ExprKind == Expr::Select) { return ParseSelectParenExpr(Name, ResTy); } else { - assert(0 && "Invalid ternary expression kind."); + assert(false && "Invalid ternary expression kind."); + std::abort(); } default: - assert(0 && "Invalid argument kind (number of args)."); - return ExprResult(); + assert(false && "Invalid argument kind (number of args)."); + std::abort(); } } From bf55c0bc02a22ca233bfca35586e3c94a6d8bc79 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 24 Mar 2023 21:14:02 +0000 Subject: [PATCH 24/25] new: persistent ptree (-write-ptree) and klee-ptree Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool. --- CMakeLists.txt | 10 + include/klee/Support/OptionCategories.h | 1 + lib/Core/CMakeLists.txt | 1 + lib/Core/Executor.cpp | 23 +- lib/Core/Executor.h | 5 +- lib/Core/PTree.cpp | 186 +++++++++--- lib/Core/PTree.h | 210 +++++++++++--- lib/Core/PTreeWriter.cpp | 184 ++++++++++++ lib/Core/PTreeWriter.h | 47 ++++ lib/Core/Searcher.cpp | 11 +- lib/Core/Searcher.h | 4 +- lib/Core/SpecialFunctionHandler.cpp | 8 +- lib/Core/UserSearcher.cpp | 11 +- lib/Core/UserSearcher.h | 1 + test/Feature/KleePtreeBogus.test | 64 +++++ test/Feature/WritePtree.c | 78 +++++ test/Feature/ptree-dbs/duplicated_node.csv | 5 + test/Feature/ptree-dbs/empty_db.csv | 1 + test/Feature/ptree-dbs/invalid_btype.csv | 4 + test/Feature/ptree-dbs/invalid_ttype.csv | 4 + test/Feature/ptree-dbs/loop.csv | 5 + test/Feature/ptree-dbs/missing_after_max.csv | 5 + test/Feature/ptree-dbs/missing_before_max.csv | 5 + test/Feature/ptree-dbs/node_id0.csv | 6 + test/Feature/ptree-dbs/not_a.db | 1 + test/lit.cfg | 9 + test/lit.site.cfg.in | 3 + tools/CMakeLists.txt | 1 + tools/klee-ptree/CMakeLists.txt | 16 ++ tools/klee-ptree/DFSVisitor.cpp | 46 +++ tools/klee-ptree/DFSVisitor.h | 31 ++ tools/klee-ptree/Printers.cpp | 266 ++++++++++++++++++ tools/klee-ptree/Printers.h | 30 ++ tools/klee-ptree/Tree.cpp | 208 ++++++++++++++ tools/klee-ptree/Tree.h | 53 ++++ tools/klee-ptree/main.cpp | 69 +++++ unittests/Searcher/CMakeLists.txt | 4 +- unittests/Searcher/SearcherTest.cpp | 26 +- 38 files changed, 1519 insertions(+), 123 deletions(-) create mode 100644 lib/Core/PTreeWriter.cpp create mode 100644 lib/Core/PTreeWriter.h create mode 100644 test/Feature/KleePtreeBogus.test create mode 100644 test/Feature/WritePtree.c create mode 100644 test/Feature/ptree-dbs/duplicated_node.csv create mode 100644 test/Feature/ptree-dbs/empty_db.csv create mode 100644 test/Feature/ptree-dbs/invalid_btype.csv create mode 100644 test/Feature/ptree-dbs/invalid_ttype.csv create mode 100644 test/Feature/ptree-dbs/loop.csv create mode 100644 test/Feature/ptree-dbs/missing_after_max.csv create mode 100644 test/Feature/ptree-dbs/missing_before_max.csv create mode 100644 test/Feature/ptree-dbs/node_id0.csv create mode 100644 test/Feature/ptree-dbs/not_a.db create mode 100644 tools/klee-ptree/CMakeLists.txt create mode 100644 tools/klee-ptree/DFSVisitor.cpp create mode 100644 tools/klee-ptree/DFSVisitor.h create mode 100644 tools/klee-ptree/Printers.cpp create mode 100644 tools/klee-ptree/Printers.h create mode 100644 tools/klee-ptree/Tree.cpp create mode 100644 tools/klee-ptree/Tree.h create mode 100644 tools/klee-ptree/main.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index e6daa815e6..cbdb6a71e5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -320,6 +320,16 @@ if (NOT SQLITE3_FOUND) message( FATAL_ERROR "SQLite3 not found, please install" ) endif() +find_program( + SQLITE_CLI + NAMES "sqlite3" + DOC "Path to sqlite3 tool" +) + +if (NOT SQLITE_CLI) + set(SQLITE_CLI "") +endif() + ################################################################################ # Detect libcap ################################################################################ diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h index 40f3deb8be..24e499e7ce 100644 --- a/include/klee/Support/OptionCategories.h +++ b/include/klee/Support/OptionCategories.h @@ -21,6 +21,7 @@ namespace klee { extern llvm::cl::OptionCategory MergeCat; extern llvm::cl::OptionCategory MiscCat; extern llvm::cl::OptionCategory ModuleCat; + extern llvm::cl::OptionCategory PTreeCat; extern llvm::cl::OptionCategory SeedingCat; extern llvm::cl::OptionCategory SolvingCat; extern llvm::cl::OptionCategory TerminationCat; diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index fa5c2b5ae9..ee10742d46 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -20,6 +20,7 @@ add_library(kleeCore Memory.cpp MemoryManager.cpp PTree.cpp + PTreeWriter.cpp Searcher.cpp SeedInfo.cpp SpecialFunctionHandler.cpp diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index cdf012a5c5..e78b45a5fe 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3631,14 +3631,15 @@ std::string Executor::getAddressInfo(ExecutionState &state, return info.str(); } - -void Executor::terminateState(ExecutionState &state) { +void Executor::terminateState(ExecutionState &state, + StateTerminationType reason) { if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, "replay did not consume all objects in test input."); } interpreterHandler->incPathsExplored(); + processTree->setTerminationType(state, reason); std::vector::iterator it = std::find(addedStates.begin(), addedStates.end(), &state); @@ -3682,7 +3683,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) { terminationTypeFileExtension(StateTerminationType::Exit).c_str()); interpreterHandler->incPathsCompleted(); - terminateState(state); + terminateState(state, StateTerminationType::Exit); } void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, @@ -3699,7 +3700,7 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, terminationTypeFileExtension(reason).c_str()); } - terminateState(state); + terminateState(state, reason); } void Executor::terminateStateEarlyAlgorithm(ExecutionState &state, @@ -3807,7 +3808,7 @@ void Executor::terminateStateOnError(ExecutionState &state, interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix); } - terminateState(state); + terminateState(state, terminationType); if (shouldExitOn(terminationType)) haltExecution = true; @@ -3840,9 +3841,14 @@ void Executor::terminateStateOnSolverError(ExecutionState &state, } void Executor::terminateStateOnUserError(ExecutionState &state, - const llvm::Twine &message) { + const llvm::Twine &message, + bool writeErr) { ++stats::terminationUserError; - terminateStateOnError(state, message, StateTerminationType::User, ""); + if (writeErr) { + terminateStateOnError(state, message, StateTerminationType::User, ""); + } else { + terminateState(state, StateTerminationType::User); + } } // XXX shoot me @@ -4593,7 +4599,8 @@ void Executor::runFunctionAsMain(Function *f, initializeGlobals(*state); - processTree = std::make_unique(state); + processTree = + getPTree(*state, userSearcherRequiresInMemoryPTree(), *interpreterHandler); run(*state); processTree = nullptr; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 28a7d56df9..ca311e9168 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -412,7 +412,7 @@ class Executor : public Interpreter { /// Remove state from queue and delete state. This function should only be /// used in the termination functions below. - void terminateState(ExecutionState &state); + void terminateState(ExecutionState &state, StateTerminationType reason); /// Call exit handler and terminate state normally /// (end of execution path) @@ -467,7 +467,8 @@ class Executor : public Interpreter { /// Call error handler and terminate state for user errors /// (e.g. wrong usage of klee.h API) void terminateStateOnUserError(ExecutionState &state, - const llvm::Twine &message); + const llvm::Twine &message, + bool writeErr = true); /// bindModuleConstants - Initialize the module constant table. void bindModuleConstants(); diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index 6c17e29698..67d26842b7 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -11,49 +11,100 @@ #include "ExecutionState.h" -#include "klee/Expr/Expr.h" +#include "klee/Core/Interpreter.h" #include "klee/Expr/ExprPPrinter.h" +#include "klee/Module/KInstruction.h" #include "klee/Support/OptionCategories.h" #include #include using namespace klee; -using namespace llvm; + +namespace klee { +llvm::cl::OptionCategory + PTreeCat("Process tree related options", + "These options affect the process tree handling."); +} namespace { +llvm::cl::opt CompressProcessTree( + "compress-process-tree", + llvm::cl::desc("Remove intermediate nodes in the process " + "tree whenever possible (default=false)"), + llvm::cl::init(false), llvm::cl::cat(PTreeCat)); + +llvm::cl::opt + WritePTree("write-ptree", llvm::cl::init(false), + llvm::cl::desc("Write process tree into ptree.db"), + llvm::cl::cat(PTreeCat)); +} // namespace -cl::opt - CompressProcessTree("compress-process-tree", - cl::desc("Remove intermediate nodes in the process " - "tree whenever possible (default=false)"), - cl::init(false), cl::cat(MiscCat)); +// PTreeNode -} // namespace +PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state, + NodeType nt) noexcept + : parent{parent}, left{nullptr}, right{nullptr}, state{state}, nodeType{ + nt} { + state->ptreeNode = this; +} + +PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept + : PTreeNode(parent, state, NT_Basic) {} + +// AnnotatedPTreeNode + +AnnotatedPTreeNode::AnnotatedPTreeNode(PTreeNode *parent, + ExecutionState *state) noexcept + : PTreeNode(parent, state, NT_Annotated) { + id = nextID++; +} -PTree::PTree(ExecutionState *initialState) - : root(PTreeNodePtr(new PTreeNode(nullptr, initialState))) { - initialState->ptreeNode = root.getPointer(); +// NoopPTree + +NoopPTree::NoopPTree() noexcept : PTree(PT_Noop) {} + +void NoopPTree::dump(llvm::raw_ostream &os) noexcept { + os << "digraph G {\nTreeNotAvailable [shape=box]\n}"; +} + +// InMemoryPTree + +InMemoryPTree::InMemoryPTree(ExecutionState &initialState, + PTreeType pt) noexcept + : PTree{pt} {} + +InMemoryPTree::InMemoryPTree(ExecutionState &initialState) noexcept + : PTree{PT_InMemory} { + root = PTreeNodePtr(createNode(nullptr, &initialState)); + initialState.ptreeNode = root.getPointer(); +} + +PTreeNode *InMemoryPTree::createNode(PTreeNode *parent, ExecutionState *state) { + return new PTreeNode(parent, state); } -void PTree::attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, BranchType reason) { +void InMemoryPTree::attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, + BranchType reason) noexcept { assert(node && !node->left.getPointer() && !node->right.getPointer()); assert(node == rightState->ptreeNode && "Attach assumes the right state is the current state"); - node->state = nullptr; - node->left = PTreeNodePtr(new PTreeNode(node, leftState)); + node->left = PTreeNodePtr(createNode(node, leftState)); // The current node inherits the tag uint8_t currentNodeTag = root.getInt(); if (node->parent) currentNodeTag = node->parent->left.getPointer() == node ? node->parent->left.getInt() : node->parent->right.getInt(); - node->right = PTreeNodePtr(new PTreeNode(node, rightState), currentNodeTag); + node->right = PTreeNodePtr(createNode(node, rightState), currentNodeTag); + updateBranchingNode(*node, reason); + node->state = nullptr; } -void PTree::remove(PTreeNode *n) { +void InMemoryPTree::remove(PTreeNode *n) noexcept { assert(!n->left.getPointer() && !n->right.getPointer()); + updateTerminatingNode(*n); do { PTreeNode *p = n->parent; if (p) { @@ -92,17 +143,17 @@ void PTree::remove(PTreeNode *n) { } } -void PTree::dump(llvm::raw_ostream &os) { - ExprPPrinter *pp = ExprPPrinter::create(os); +void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept { + std::unique_ptr pp(ExprPPrinter::create(os)); pp->setNewline("\\l"); - os << "digraph G {\n"; - os << "\tsize=\"10,7.5\";\n"; - os << "\tratio=fill;\n"; - os << "\trotate=90;\n"; - os << "\tcenter = \"true\";\n"; - os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"; - os << "\tedge [arrowsize=.3]\n"; - std::vector stack; + os << "digraph G {\n" + << "\tsize=\"10,7.5\";\n" + << "\tratio=fill;\n" + << "\trotate=90;\n" + << "\tcenter = \"true\";\n" + << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n" + << "\tedge [arrowsize=.3]\n"; + std::vector stack; stack.push_back(root.getPointer()); while (!stack.empty()) { const PTreeNode *n = stack.back(); @@ -112,24 +163,87 @@ void PTree::dump(llvm::raw_ostream &os) { os << ",fillcolor=green"; os << "];\n"; if (n->left.getPointer()) { - os << "\tn" << n << " -> n" << n->left.getPointer(); - os << " [label=0b" + os << "\tn" << n << " -> n" << n->left.getPointer() << " [label=0b" << std::bitset(n->left.getInt()).to_string() << "];\n"; stack.push_back(n->left.getPointer()); } if (n->right.getPointer()) { - os << "\tn" << n << " -> n" << n->right.getPointer(); - os << " [label=0b" + os << "\tn" << n << " -> n" << n->right.getPointer() << " [label=0b" << std::bitset(n->right.getInt()).to_string() << "];\n"; stack.push_back(n->right.getPointer()); } } os << "}\n"; - delete pp; } -PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) : parent{parent}, state{state} { - state->ptreeNode = this; - left = PTreeNodePtr(nullptr); - right = PTreeNodePtr(nullptr); +std::uint8_t InMemoryPTree::getNextId() noexcept { + std::uint8_t id = 1 << registeredIds++; + if (registeredIds > PtrBitCount) { + klee_error("PTree cannot support more than %d RandomPathSearchers", + PtrBitCount); + } + return id; +} + +// PersistentPTree + +PersistentPTree::PersistentPTree(ExecutionState &initialState, + InterpreterHandler &ih) noexcept + : InMemoryPTree(initialState, PT_Persistent), + writer(ih.getOutputFilename("ptree.db")) { + root = PTreeNodePtr(createNode(nullptr, &initialState)); + initialState.ptreeNode = root.getPointer(); } + +void PersistentPTree::dump(llvm::raw_ostream &os) noexcept { + writer.batchCommit(true); + InMemoryPTree::dump(os); +} + +PTreeNode *PersistentPTree::createNode(PTreeNode *parent, + ExecutionState *state) { + return new AnnotatedPTreeNode(parent, state); +} + +void PersistentPTree::setTerminationType(ExecutionState &state, + StateTerminationType type) { + auto *annotatedNode = llvm::dyn_cast(state.ptreeNode); + assert(annotatedNode); + annotatedNode->kind = type; +} + +void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) { + auto *annotatedNode = llvm::dyn_cast(&node); + assert(annotatedNode); + const auto &state = *node.state; + const auto prevPC = state.prevPC; + annotatedNode->asmLine = + prevPC && prevPC->info ? prevPC->info->assemblyLine : 0; + annotatedNode->kind = reason; + writer.write(*annotatedNode); +} + +void PersistentPTree::updateTerminatingNode(PTreeNode &node) { + assert(node.state); + auto *annotatedNode = llvm::dyn_cast(&node); + assert(annotatedNode); + const auto &state = *node.state; + const auto prevPC = state.prevPC; + annotatedNode->asmLine = + prevPC && prevPC->info ? prevPC->info->assemblyLine : 0; + annotatedNode->stateID = state.getID(); + writer.write(*annotatedNode); +} + +// Factory + +std::unique_ptr klee::getPTree(ExecutionState &state, bool inMemory, + InterpreterHandler &ih) { + if (WritePTree) + return std::make_unique(state, ih); + + if (inMemory) + return std::make_unique(state); + + return std::make_unique(); +}; diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index dbee70dda9..54ed3e217f 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -10,57 +10,175 @@ #ifndef KLEE_PTREE_H #define KLEE_PTREE_H +#include "PTreeWriter.h" +#include "UserSearcher.h" #include "klee/Core/BranchTypes.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Expr/Expr.h" #include "klee/Support/ErrorHandling.h" + #include "llvm/ADT/PointerIntPair.h" +#include "llvm/Support/Casting.h" + +#include namespace klee { - class ExecutionState; - class PTreeNode; - /* PTreeNodePtr is used by the Random Path Searcher object to efficiently - record which PTreeNode belongs to it. PTree is a global structure that - captures all states, whereas a Random Path Searcher might only care about - a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which - Random Path Searchers PTreeNode belongs to. */ - constexpr int PtrBitCount = 3; - using PTreeNodePtr = llvm::PointerIntPair; - - class PTreeNode { - public: - PTreeNode *parent = nullptr; - - PTreeNodePtr left; - PTreeNodePtr right; - ExecutionState *state = nullptr; - - PTreeNode(const PTreeNode&) = delete; - PTreeNode(PTreeNode *parent, ExecutionState *state); - ~PTreeNode() = default; - }; - - class PTree { - // Number of registered ID - int registeredIds = 0; - - public: - PTreeNodePtr root; - explicit PTree(ExecutionState *initialState); - ~PTree() = default; - - void attach(PTreeNode *node, ExecutionState *leftState, - ExecutionState *rightState, BranchType reason); - void remove(PTreeNode *node); - void dump(llvm::raw_ostream &os); - std::uint8_t getNextId() { - std::uint8_t id = 1 << registeredIds++; - if (registeredIds > PtrBitCount) { - klee_error("PTree cannot support more than %d RandomPathSearchers", - PtrBitCount); - } - return id; - } - }; -} +class ExecutionState; +class Executor; +class InMemoryPTree; +class InterpreterHandler; +class PTreeNode; +class Searcher; + +/* PTreeNodePtr is used by the Random Path Searcher object to efficiently +record which PTreeNode belongs to it. PTree is a global structure that +captures all states, whereas a Random Path Searcher might only care about +a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which +Random Path Searchers PTreeNode belongs to. */ +constexpr std::uint8_t PtrBitCount = 3; +using PTreeNodePtr = llvm::PointerIntPair; + +class PTreeNode { +public: + enum NodeType { NT_Basic, NT_Annotated }; + + PTreeNode *parent{nullptr}; + PTreeNodePtr left; + PTreeNodePtr right; + ExecutionState *state{nullptr}; + + PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept; + virtual ~PTreeNode() = default; + PTreeNode(const PTreeNode &) = delete; + PTreeNode &operator=(PTreeNode const &) = delete; + PTreeNode(PTreeNode &&) = delete; + PTreeNode &operator=(PTreeNode &&) = delete; + + [[nodiscard]] NodeType getType() const { return nodeType; } + static bool classof(const PTreeNode *N) { return true; } + +private: + NodeType nodeType; + +protected: + PTreeNode(PTreeNode *parent, ExecutionState *state, NodeType nt) noexcept; +}; + +class AnnotatedPTreeNode : public PTreeNode { + inline static std::uint32_t nextID{1}; + +public: + std::uint32_t id{0}; + std::uint32_t stateID{0}; + std::uint32_t asmLine{0}; + std::variant kind{BranchType::NONE}; + + AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept; + ~AnnotatedPTreeNode() override = default; + + static bool classof(const PTreeNode *N) { + return N->getType() == NT_Annotated; + } +}; + +class PTree { +public: + enum PTreeType { PT_Basic, PT_Noop, PT_InMemory, PT_Persistent }; + + /// Branch from PTreeNode and attach states, convention: rightState is + /// parent + virtual void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, BranchType reason) = 0; + /// Dump process tree in .dot format into os (debug) + virtual void dump(llvm::raw_ostream &os) = 0; + /// Remove node from tree + virtual void remove(PTreeNode *node) = 0; + /// Set termination type (on state removal) + virtual void setTerminationType(ExecutionState &state, + StateTerminationType type){}; + + virtual ~PTree() = default; + PTree(PTree const &) = delete; + PTree &operator=(PTree const &) = delete; + PTree(PTree &&) = delete; + PTree &operator=(PTree &&) = delete; + + [[nodiscard]] PTreeType getType() const { return ptreeType; } + static bool classof(const PTreeNode *N) { return true; } + +protected: + explicit PTree(PTreeType pt) noexcept : ptreeType{pt} {}; + +private: + PTreeType ptreeType; +}; + +/// @brief A pseudo process tree that does not maintain any nodes. +class NoopPTree final : public PTree { +public: + NoopPTree() noexcept; + ~NoopPTree() override = default; + void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, + BranchType reason) noexcept override{}; + void dump(llvm::raw_ostream &os) noexcept override; + void remove(PTreeNode *node) noexcept override{}; + + static bool classof(const PTree *T) { return T->getType() == PT_Noop; } +}; + +/// @brief An in-memory process tree required by RandomPathSearcher +class InMemoryPTree : public PTree { +public: + PTreeNodePtr root; + +private: + /// Number of registered IDs ("users", e.g. RandomPathSearcher) + std::uint8_t registeredIds = 0; + + virtual PTreeNode *createNode(PTreeNode *parent, ExecutionState *state); + virtual void updateBranchingNode(PTreeNode &node, BranchType reason){}; + virtual void updateTerminatingNode(PTreeNode &node){}; + +public: + explicit InMemoryPTree(ExecutionState &initialState) noexcept; + ~InMemoryPTree() override = default; + + void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState, BranchType reason) noexcept override; + void dump(llvm::raw_ostream &os) noexcept override; + std::uint8_t getNextId() noexcept; + void remove(PTreeNode *node) noexcept override; + + static bool classof(const PTree *T) { + return (T->getType() == PT_InMemory) || (T->getType() == PT_Persistent); + } + +protected: + InMemoryPTree(ExecutionState &initialState, PTreeType pt) noexcept; +}; + +/// @brief An in-memory process tree that also writes its nodes into an SQLite +/// database (ptree.db) with a PTreeWriter +class PersistentPTree : public InMemoryPTree { + PTreeWriter writer; + + PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override; + void updateBranchingNode(PTreeNode &node, BranchType reason) override; + void updateTerminatingNode(PTreeNode &node) override; + +public: + explicit PersistentPTree(ExecutionState &initialState, + InterpreterHandler &ih) noexcept; + void dump(llvm::raw_ostream &os) noexcept override; + void setTerminationType(ExecutionState &state, + StateTerminationType type) override; + + static bool classof(const PTree *T) { return T->getType() == PT_Persistent; } +}; + +std::unique_ptr getPTree(ExecutionState &state, bool inMemory, + InterpreterHandler &ih); +} // namespace klee #endif /* KLEE_PTREE_H */ diff --git a/lib/Core/PTreeWriter.cpp b/lib/Core/PTreeWriter.cpp new file mode 100644 index 0000000000..3dd6076fb7 --- /dev/null +++ b/lib/Core/PTreeWriter.cpp @@ -0,0 +1,184 @@ +//===-- PTreeWriter.cpp ---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "PTreeWriter.h" + +#include "PTree.h" +#include "klee/Support/ErrorHandling.h" +#include "klee/Support/OptionCategories.h" + +#include "llvm/Support/CommandLine.h" + +namespace { +llvm::cl::opt BatchSize( + "ptree-batch-size", llvm::cl::init(100U), + llvm::cl::desc("Number of process tree nodes to batch for writing, " + "see --write-ptree (default=100)"), + llvm::cl::cat(klee::PTreeCat)); +} // namespace + +using namespace klee; + +void prepare_statement(sqlite3 *db, std::string &query, sqlite3_stmt **stmt) { + int result; +#ifdef SQLITE_PREPARE_PERSISTENT + result = sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT, + stmt, nullptr); +#else + result = sqlite3_prepare_v3(db, query.c_str(), -1, 0, stmt, nullptr); +#endif + if (result != SQLITE_OK) { + klee_warning("Process tree database: can't prepare query: %s [%s]", + sqlite3_errmsg(db), query.c_str()); + sqlite3_close(db); + klee_error("Process tree database: can't prepare query: %s", query.c_str()); + } +} + +PTreeWriter::PTreeWriter(const std::string &dbPath) { + // create database file + if (sqlite3_open(dbPath.c_str(), &db) != SQLITE_OK) + klee_error("Can't create process tree database: %s", sqlite3_errmsg(db)); + + // - set options: asynchronous + WAL + char *errMsg = nullptr; + if (sqlite3_exec(db, "PRAGMA synchronous = OFF;", nullptr, nullptr, + &errMsg) != SQLITE_OK) { + klee_warning("Process tree database: can't set option: %s", errMsg); + sqlite3_free(errMsg); + } + if (sqlite3_exec(db, "PRAGMA journal_mode = WAL;", nullptr, nullptr, + &errMsg) != SQLITE_OK) { + klee_warning("Process tree database: can't set option: %s", errMsg); + sqlite3_free(errMsg); + } + + // - create table + std::string query = + "CREATE TABLE IF NOT EXISTS nodes (" + "ID INT PRIMARY KEY, stateID INT, leftID INT, rightID INT," + "asmLine INT, kind INT);"; + char *zErr = nullptr; + if (sqlite3_exec(db, query.c_str(), nullptr, nullptr, &zErr) != SQLITE_OK) { + klee_warning("Process tree database: initialisation error: %s", zErr); + sqlite3_free(zErr); + sqlite3_close(db); + klee_error("Process tree database: initialisation error."); + } + + // create prepared statements + // - insertStmt + query = "INSERT INTO nodes VALUES (?, ?, ?, ?, ?, ?);"; + prepare_statement(db, query, &insertStmt); + // - transactionBeginStmt + query = "BEGIN TRANSACTION"; + prepare_statement(db, query, &transactionBeginStmt); + // - transactionCommitStmt + query = "COMMIT TRANSACTION"; + prepare_statement(db, query, &transactionCommitStmt); + + // begin transaction + auto rc = sqlite3_step(transactionBeginStmt); + if (rc != SQLITE_DONE) { + klee_warning("Process tree database: can't begin transaction: %s", + sqlite3_errmsg(db)); + } + sqlite3_reset(transactionBeginStmt); +} + +void PTreeWriter::finalize() { + batchCommit(!flushed); + + // finalize prepared statements + sqlite3_finalize(insertStmt); + sqlite3_finalize(transactionBeginStmt); + sqlite3_finalize(transactionCommitStmt); + + // commit + sqlite3_exec(db, "END TRANSACTION", nullptr, nullptr, nullptr); +} + +PTreeWriter::~PTreeWriter() { + finalize(); + sqlite3_close(db); +} + +void PTreeWriter::batchCommit(bool force) { + ++batch; + if (batch < BatchSize && !force) + return; + + // commit and begin transaction + auto rc = sqlite3_step(transactionCommitStmt); + if (rc != SQLITE_DONE) { + klee_warning("Process tree database: transaction commit error: %s", + sqlite3_errmsg(db)); + } + sqlite3_reset(transactionCommitStmt); + + rc = sqlite3_step(transactionBeginStmt); + if (rc != SQLITE_DONE) { + klee_warning("Process tree database: transaction begin error: %s", + sqlite3_errmsg(db)); + } + sqlite3_reset(transactionBeginStmt); + batch = 0; + flushed = true; +} + +void PTreeWriter::write(const AnnotatedPTreeNode &node) { + int rc = 0; + + // bind values (SQLITE_OK is defined as 0 - just check success once at the + // end) + rc += sqlite3_bind_int64(insertStmt, 1, node.id); + rc += sqlite3_bind_int(insertStmt, 2, node.stateID); + rc += sqlite3_bind_int64( + insertStmt, 3, + node.left.getPointer() + ? (static_cast(node.left.getPointer()))->id + : 0); + rc += sqlite3_bind_int64( + insertStmt, 4, + node.right.getPointer() + ? (static_cast(node.right.getPointer()))->id + : 0); + rc += sqlite3_bind_int(insertStmt, 5, node.asmLine); + std::uint8_t value{0}; + if (std::holds_alternative(node.kind)) { + value = static_cast(std::get(node.kind)); + } else if (std::holds_alternative(node.kind)) { + value = + static_cast(std::get(node.kind)); + } else { + assert(false && "PTreeWriter: Illegal node kind!"); + } + rc += sqlite3_bind_int(insertStmt, 6, value); + if (rc != SQLITE_OK) { + // This is either a programming error (e.g. SQLITE_MISUSE) or we ran out of + // resources (e.g. SQLITE_NOMEM). Calling sqlite3_errmsg() after a possible + // successful call above is undefined, hence no error message here. + klee_error("Process tree database: can't persist data for node: %u", + node.id); + } + + // insert + rc = sqlite3_step(insertStmt); + if (rc != SQLITE_DONE) { + klee_warning("Process tree database: can't persist data for node: %u: %s", + node.id, sqlite3_errmsg(db)); + } + rc = sqlite3_reset(insertStmt); + if (rc != SQLITE_OK) { + klee_warning("Process tree database: error reset node: %u: %s", node.id, + sqlite3_errmsg(db)); + } + + batchCommit(); +} diff --git a/lib/Core/PTreeWriter.h b/lib/Core/PTreeWriter.h new file mode 100644 index 0000000000..66f24e11ee --- /dev/null +++ b/lib/Core/PTreeWriter.h @@ -0,0 +1,47 @@ +//===-- PTreeWriter.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#pragma once + +#include + +#include + +namespace klee { +class AnnotatedPTreeNode; + +/// @brief Writes process tree nodes into an SQLite database +class PTreeWriter { + friend class PersistentPTree; + + ::sqlite3 *db{nullptr}; + ::sqlite3_stmt *insertStmt{nullptr}; + ::sqlite3_stmt *transactionBeginStmt{nullptr}; + ::sqlite3_stmt *transactionCommitStmt{nullptr}; + std::uint32_t batch{0}; + bool flushed{true}; + + /// Writes nodes in batches + void batchCommit(bool force = false); + /// Commit data and finalize prepared statements + void finalize(); + +public: + explicit PTreeWriter(const std::string &dbPath); + ~PTreeWriter(); + PTreeWriter(const PTreeWriter &other) = delete; + PTreeWriter(PTreeWriter &&other) noexcept = delete; + PTreeWriter &operator=(const PTreeWriter &other) = delete; + PTreeWriter &operator=(PTreeWriter &&other) noexcept = delete; + + /// Write new node into database + void write(const AnnotatedPTreeNode &node); +}; + +} // namespace klee diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 047a1e4fd8..f9ebb6afb8 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -257,10 +257,13 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) { #define IS_OUR_NODE_VALID(n) \ (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0)) -RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng) - : processTree{processTree}, - theRNG{rng}, - idBitMask{processTree.getNextId()} {}; +RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng) + : processTree{*processTree}, theRNG{rng}, idBitMask{static_cast( + processTree + ? processTree->getNextId() + : 0)} { + assert(processTree); +}; ExecutionState &RandomPathSearcher::selectState() { unsigned flips=0, bits=0; diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 4eda838d64..1608181aa1 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -172,7 +172,7 @@ namespace klee { /// /// The ownership bits are maintained in the update method. class RandomPathSearcher final : public Searcher { - PTree &processTree; + InMemoryPTree &processTree; RNG &theRNG; // Unique bitmask of this searcher @@ -181,7 +181,7 @@ namespace klee { public: /// \param processTree The process tree. /// \param RNG A random number generator. - RandomPathSearcher(PTree &processTree, RNG &rng); + RandomPathSearcher(InMemoryPTree *processTree, RNG &rng); ~RandomPathSearcher() override = default; ExecutionState &selectState() override; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 7996499cc8..283aab482b 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -506,12 +506,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, state.constraints, e, res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (res) { - if (SilentKleeAssume) { - executor.terminateState(state); - } else { - executor.terminateStateOnUserError( - state, "invalid klee_assume call (provably false)"); - } + executor.terminateStateOnUserError( + state, "invalid klee_assume call (provably false)", !SilentKleeAssume); } else { executor.addConstraint(state, e); } diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 398c44a98c..e704363935 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -102,8 +102,11 @@ bool klee::userSearcherRequiresMD2U() { std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end()); } +bool klee::userSearcherRequiresInMemoryPTree() { + return std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end(); +} -Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &processTree) { +Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree *processTree) { Searcher *searcher = nullptr; switch (type) { case Searcher::DFS: searcher = new DFSSearcher(); break; @@ -123,15 +126,15 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &process } Searcher *klee::constructUserSearcher(Executor &executor) { - - Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, *executor.processTree); + auto *ptree = llvm::dyn_cast(executor.processTree.get()); + Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, ptree); if (CoreSearch.size() > 1) { std::vector s; s.push_back(searcher); for (unsigned i = 1; i < CoreSearch.size(); i++) - s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, *executor.processTree)); + s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, ptree)); searcher = new InterleavedSearcher(s); } diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h index b0df8239ed..fe75eb6d63 100644 --- a/lib/Core/UserSearcher.h +++ b/lib/Core/UserSearcher.h @@ -16,6 +16,7 @@ namespace klee { // XXX gross, should be on demand? bool userSearcherRequiresMD2U(); + bool userSearcherRequiresInMemoryPTree(); void initializeSearchOptions(); diff --git a/test/Feature/KleePtreeBogus.test b/test/Feature/KleePtreeBogus.test new file mode 100644 index 0000000000..8f957a21eb --- /dev/null +++ b/test/Feature/KleePtreeBogus.test @@ -0,0 +1,64 @@ +fail on broken db (not sqlite) +RUN: not %klee-ptree tree-info %S/ptree-dbs/not_a.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-CORRUPT -input-file=%t.err %s +CHECK-CORRUPT: Can't prepare read statement: file is not a database + +empty tree +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/empty_db.csv nodes" +RUN: %klee-ptree tree-info %t.db > %t.err +RUN: FileCheck -check-prefix=CHECK-EMPTY -input-file=%t.err %s +CHECK-EMPTY: Empty tree. + +REQUIRES: sqlite3 +fail on tree with duplicate node IDs +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/duplicated_node.csv nodes" +RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-DUP -input-file=%t.err %s +CHECK-DUP: PTree DB contains duplicate child reference or circular structure. Affected node: 2 + +fail on invalid branch type +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_btype.csv nodes" +RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-BTYPE -input-file=%t.err %s +CHECK-BTYPE: PTree DB contains unknown branch type (123) in node 1 + +fail on invalid termination type +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_ttype.csv nodes" +RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-TTYPE -input-file=%t.err %s +CHECK-TTYPE: PTree DB contains unknown termination type (123) in node 3 + +fail on tree with looping nodes +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/loop.csv nodes" +RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-LOOP -input-file=%t.err %s +CHECK-LOOP: PTree DB contains duplicate child reference or circular structure. Affected node: 1 + +fail on tree with missing node (child node ID > max. ID) +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_after_max.csv nodes" +RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-MISSA -input-file=%t.err %s +CHECK-MISSA: PTree DB contains references to non-existing nodes (> max. ID) in node 3 + +fail on tree with missing node (child node ID < max. ID) +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_before_max.csv nodes" +RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-MISSB -input-file=%t.err %s +CHECK-MISSB: PTree DB references undefined node. Affected node: 4 + +fail on illegal node ID (0) +RUN: rm -f %t.db +RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/node_id0.csv nodes" +RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: FileCheck -check-prefix=CHECK-ID0 -input-file=%t.err %s +CHECK-ID0: PTree DB contains illegal node ID (0) + +cleanup +RUN rm -f %t.db diff --git a/test/Feature/WritePtree.c b/test/Feature/WritePtree.c new file mode 100644 index 0000000000..e7bf59ce67 --- /dev/null +++ b/test/Feature/WritePtree.c @@ -0,0 +1,78 @@ +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee -write-ptree --output-dir=%t.klee-out %t.bc +// RUN: %klee-ptree branches %t.klee-out/ptree.db | FileCheck --check-prefix=CHECK-BRANCH %s +// RUN: %klee-ptree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s +// RUN: %klee-ptree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s +// RUN: %klee-ptree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s +// RUN: %klee-ptree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s +// RUN: %klee-ptree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s +// RUN: not %klee-ptree dot %t.klee-out/ptree-doesnotexist.db + +#include "klee/klee.h" + +#include + +int main(void) { + int a = 42; + int c0, c1, c2, c3; + klee_make_symbolic(&c0, sizeof(c0), "c0"); + klee_make_symbolic(&c1, sizeof(c1), "c1"); + klee_make_symbolic(&c2, sizeof(c2), "c2"); + klee_make_symbolic(&c3, sizeof(c3), "c3"); + + if (c0) { + a += 17; + } else { + a -= 4; + } + + if (c1) { + klee_assume(!c1); + } else if (c2) { + char *p = NULL; + p[4711] = '!'; + } else if (c3) { + klee_silent_exit(0); + } else { + return a; + } + + return 0; +} + +// CHECK-BRANCH: branch type,count +// CHECK-BRANCH: Conditional,7 + +// CHECK-DEPTH: depth,count +// CHECK-DEPTH: 3,2 +// CHECK-DEPTH: 4,2 +// CHECK-DEPTH: 5,4 + +// CHECK-INSTR: asm line,branches,terminations,termination types +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,User(2) +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Ptr(2) +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,SilentExit(2) +// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Exit(2) + +// CHECK-TERM: termination type,count +// CHECK-TERM-DAG: Exit,2 +// CHECK-TERM-DAG: Ptr,2 +// CHECK-TERM-DAG: User,2 +// CHECK-TERM-DAG: SilentExit,2 + +// CHECK-DOT: strict digraph PTree { +// CHECK-DOT: node[shape=point,width=0.15,color=darkgrey]; +// CHECK-DOT: edge[color=darkgrey]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Conditional\nnode: {{[0-9]+}}\nstate: 0\nasm: {{[0-9]+}}"]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Exit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=green]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="SilentExit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=orange]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Ptr\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=red]; +// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="User\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=blue]; +// CHECK-DOT-DAG: N{{[0-9]+}}->{N{{[0-9]+}} N{{[0-9]+}}}; +// CHECK-DOT-DAG: } + +// CHECK-TINFO: nodes: 15 +// CHECK-TINFO: leaf nodes: 8 +// CHECK-TINFO: max. depth: 5 +// CHECK-TINFO: avg. depth: 4.2 diff --git a/test/Feature/ptree-dbs/duplicated_node.csv b/test/Feature/ptree-dbs/duplicated_node.csv new file mode 100644 index 0000000000..7882b911e2 --- /dev/null +++ b/test/Feature/ptree-dbs/duplicated_node.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,2,62,1 +4,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/empty_db.csv b/test/Feature/ptree-dbs/empty_db.csv new file mode 100644 index 0000000000..4dac8a1748 --- /dev/null +++ b/test/Feature/ptree-dbs/empty_db.csv @@ -0,0 +1 @@ +ID,stateID,leftID,rightID,asmLine,kind diff --git a/test/Feature/ptree-dbs/invalid_btype.csv b/test/Feature/ptree-dbs/invalid_btype.csv new file mode 100644 index 0000000000..01ee428cc9 --- /dev/null +++ b/test/Feature/ptree-dbs/invalid_btype.csv @@ -0,0 +1,4 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,123 +2,0,0,0,61,36 +3,1,0,0,61,1 diff --git a/test/Feature/ptree-dbs/invalid_ttype.csv b/test/Feature/ptree-dbs/invalid_ttype.csv new file mode 100644 index 0000000000..0d185bee80 --- /dev/null +++ b/test/Feature/ptree-dbs/invalid_ttype.csv @@ -0,0 +1,4 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,0,0,61,123 diff --git a/test/Feature/ptree-dbs/loop.csv b/test/Feature/ptree-dbs/loop.csv new file mode 100644 index 0000000000..4fc2b9f281 --- /dev/null +++ b/test/Feature/ptree-dbs/loop.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,1,62,1 +4,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/missing_after_max.csv b/test/Feature/ptree-dbs/missing_after_max.csv new file mode 100644 index 0000000000..16e99a357c --- /dev/null +++ b/test/Feature/ptree-dbs/missing_after_max.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,5,62,1 +4,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/missing_before_max.csv b/test/Feature/ptree-dbs/missing_before_max.csv new file mode 100644 index 0000000000..2131ea56f9 --- /dev/null +++ b/test/Feature/ptree-dbs/missing_before_max.csv @@ -0,0 +1,5 @@ +ID,stateID,leftID,rightID,asmLine,kind +1,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,5,62,1 +5,1,0,0,63,80 diff --git a/test/Feature/ptree-dbs/node_id0.csv b/test/Feature/ptree-dbs/node_id0.csv new file mode 100644 index 0000000000..51a31e4996 --- /dev/null +++ b/test/Feature/ptree-dbs/node_id0.csv @@ -0,0 +1,6 @@ +ID,stateID,leftID,rightID,asmLine,kind +0,0,2,3,44,1 +2,0,0,0,61,36 +3,1,4,5,62,1 +4,1,0,0,63,80 +5,2,0,0,63,36 diff --git a/test/Feature/ptree-dbs/not_a.db b/test/Feature/ptree-dbs/not_a.db new file mode 100644 index 0000000000..d81cc0710e --- /dev/null +++ b/test/Feature/ptree-dbs/not_a.db @@ -0,0 +1 @@ +42 diff --git a/test/lit.cfg b/test/lit.cfg index cb47d3d4c5..8abf7012d1 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -116,6 +116,11 @@ config.substitutions.append( ('%libkleeruntest', config.libkleeruntest) ) +# Add a substition for sqlite3 +config.substitutions.append( + ('%sqlite3', os.path.abspath(config.sqlite3)) +) + # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line # e.g. llvm-lit --param klee_opts=--help klee_extra_params = lit_config.params.get('klee_opts',"") @@ -134,6 +139,7 @@ if len(kleaver_extra_params) != 0: # If a tool's name is a prefix of another, the longer name has # to come first, e.g., klee-replay should come before klee subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), + ('%klee-ptree', 'klee-ptree', ''), ('%klee-replay', 'klee-replay', ''), ('%klee-stats', 'klee-stats', ''), ('%klee-zesti', 'klee-zesti', ''), @@ -233,3 +239,6 @@ config.available_features.add('{}32bit-support'.format('' if config.have_32bit_s config.available_features.add('{}asan'.format('' if config.have_asan else 'not-')) config.available_features.add('{}ubsan'.format('' if config.have_ubsan else 'not-')) config.available_features.add('{}msan'.format('' if config.have_msan else 'not-')) + +# SQLite +config.available_features.add('{}sqlite3'.format('' if config.have_sqlite3 else 'not-')) diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index c7063057da..d82b8a2cd1 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -26,6 +26,8 @@ config.cxx = "@NATIVE_CXX@" # test/Concrete/CMakeLists.txt config.O0opt = "-O0 -Xclang -disable-O0-optnone" +config.sqlite3 = "@SQLITE_CLI@" + # Features config.enable_uclibc = True if @SUPPORT_KLEE_UCLIBC@ == 1 else False config.enable_posix_runtime = True if @ENABLE_POSIX_RUNTIME@ == 1 else False @@ -39,6 +41,7 @@ config.have_asan = True if @IS_ASAN_BUILD@ == 1 else False config.have_ubsan = True if @IS_UBSAN_BUILD@ == 1 else False config.have_msan = True if @IS_MSAN_BUILD@ == 1 else False config.have_32bit_support = True if @M32_SUPPORTED@ == 1 else False +config.have_sqlite3 = True if "@SQLITE_CLI@".strip() != "" else False # Add sanitizer list config.environment['LSAN_OPTIONS'] = "suppressions=@KLEE_UTILS_DIR@/sanitizers/lsan.txt" diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index b641885cc1..40089c4075 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -10,6 +10,7 @@ add_subdirectory(ktest-gen) add_subdirectory(ktest-randgen) add_subdirectory(kleaver) add_subdirectory(klee) +add_subdirectory(klee-ptree) add_subdirectory(klee-replay) add_subdirectory(klee-stats) add_subdirectory(klee-zesti) diff --git a/tools/klee-ptree/CMakeLists.txt b/tools/klee-ptree/CMakeLists.txt new file mode 100644 index 0000000000..eceb52720b --- /dev/null +++ b/tools/klee-ptree/CMakeLists.txt @@ -0,0 +1,16 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +add_executable(klee-ptree main.cpp Tree.cpp DFSVisitor.cpp Printers.cpp) + +target_compile_features(klee-ptree PRIVATE cxx_std_17) +target_include_directories(klee-ptree PRIVATE ${KLEE_INCLUDE_DIRS} ${SQLITE3_INCLUDE_DIRS}) +target_link_libraries(klee-ptree PUBLIC ${SQLITE3_LIBRARIES}) + +install(TARGETS klee-ptree DESTINATION bin) diff --git a/tools/klee-ptree/DFSVisitor.cpp b/tools/klee-ptree/DFSVisitor.cpp new file mode 100644 index 0000000000..c87afc3ebf --- /dev/null +++ b/tools/klee-ptree/DFSVisitor.cpp @@ -0,0 +1,46 @@ +//===-- DFSVisitor.cpp ------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "DFSVisitor.h" + +#include + +DFSVisitor::DFSVisitor(const Tree &tree, callbackT cb_intermediate, + callbackT cb_leaf) noexcept + : tree{tree}, + cb_intermediate{std::move(cb_intermediate)}, cb_leaf{std::move(cb_leaf)} { + run(); +} + +void DFSVisitor::run() const noexcept { + // empty tree + if (tree.nodes.size() <= 1) + return; + + std::vector> stack{ + {1, 1}}; // (id, depth) + while (!stack.empty()) { + std::uint32_t id, depth; + std::tie(id, depth) = stack.back(); + stack.pop_back(); + const auto &node = tree.nodes[id]; + + if (node.left || node.right) { + if (cb_intermediate) + cb_intermediate(id, node, depth); + if (node.right) + stack.emplace_back(node.right, depth + 1); + if (node.left) + stack.emplace_back(node.left, depth + 1); + } else { + if (cb_leaf) + cb_leaf(id, node, depth); + } + } +} diff --git a/tools/klee-ptree/DFSVisitor.h b/tools/klee-ptree/DFSVisitor.h new file mode 100644 index 0000000000..60d7b3bdb0 --- /dev/null +++ b/tools/klee-ptree/DFSVisitor.h @@ -0,0 +1,31 @@ +//===-- DFSVisitor.h --------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#pragma once + +#include "Tree.h" + +#include + +/// @brief Traverses a process tree and calls registered callbacks for +/// intermediate and leaf nodes (not the classical Visitor pattern). +class DFSVisitor { + // void _(node ID, node, depth) + using callbackT = std::function; + + const Tree &tree; + callbackT cb_intermediate; + callbackT cb_leaf; + void run() const noexcept; + +public: + DFSVisitor(const Tree &tree, callbackT cb_intermediate, + callbackT cb_leaf) noexcept; + ~DFSVisitor() = default; +}; diff --git a/tools/klee-ptree/Printers.cpp b/tools/klee-ptree/Printers.cpp new file mode 100644 index 0000000000..950d1b0943 --- /dev/null +++ b/tools/klee-ptree/Printers.cpp @@ -0,0 +1,266 @@ +//===-- Printers.cpp --------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "Printers.h" + +#include "DFSVisitor.h" +#include "klee/Core/BranchTypes.h" +#include "klee/Core/TerminationTypes.h" + +#include +#include +#include +#include +#include +#include +#include +#include + +// branches + +void printBranches(const Tree &tree) { + if (tree.nodes.size() <= 1) { + std::cout << "Empty tree.\n"; + return; + } + + std::unordered_map branchTypes; + + DFSVisitor visitor( + tree, + [&branchTypes](std::uint32_t id, Node node, std::uint32_t depth) { + branchTypes[std::get(node.kind)]++; + }, + nullptr); + + // sort output + std::vector> sortedBranchTypes( + branchTypes.begin(), branchTypes.end()); + std::sort(sortedBranchTypes.begin(), sortedBranchTypes.end(), + [](const auto &lhs, const auto &rhs) { + return (lhs.second > rhs.second) || + (lhs.second == rhs.second && lhs.first < rhs.first); + }); + + std::cout << "branch type,count\n"; + for (const auto &[branchType, count] : sortedBranchTypes) + std::cout << branchTypeNames[branchType] << ',' << count << '\n'; +} + +// depths + +struct DepthInfo { + std::vector depths; + std::uint32_t maxDepth{0}; + std::uint32_t noLeaves{0}; + std::uint32_t noNodes{0}; +}; + +DepthInfo getDepthInfo(const Tree &tree) { + DepthInfo I; + + DFSVisitor visitor( + tree, + [&](std::uint32_t id, Node node, std::uint32_t depth) { ++I.noNodes; }, + [&I](std::uint32_t id, Node node, std::uint32_t depth) { + ++I.noLeaves; + ++I.noNodes; + if (depth > I.maxDepth) + I.maxDepth = depth; + if (depth >= I.depths.size()) + I.depths.resize(depth + 1, 0); + ++I.depths[depth]; + }); + + return I; +} + +void printDepths(const Tree &tree) { + if (tree.nodes.size() <= 1) { + std::cout << "Empty tree.\n"; + return; + } + + const auto DI = getDepthInfo(tree); + std::cout << "depth,count\n"; + for (size_t depth = 1; depth <= DI.maxDepth; ++depth) { + auto count = DI.depths[depth]; + if (count) + std::cout << depth << ',' << count << '\n'; + } +} + +// dot + +std::array NodeColours = {"green", "orange", "red", + "blue", "darkblue", "darkgrey"}; + +std::string_view terminationTypeColour(StateTerminationType type) { + // Exit + if (type == StateTerminationType::Exit) + return NodeColours[0]; + + // Early + if ((StateTerminationType::EXIT < type && + type <= StateTerminationType::EARLY) || + (StateTerminationType::EXECERR < type && + type <= StateTerminationType::END)) { + return NodeColours[1]; + } + + // Program error + if (StateTerminationType::SOLVERERR < type && + type <= StateTerminationType::PROGERR) + return NodeColours[2]; + + // User error + if (StateTerminationType::PROGERR < type && + type <= StateTerminationType::USERERR) + return NodeColours[3]; + + // Execution/Solver error + if ((StateTerminationType::USERERR < type && + type <= StateTerminationType::EXECERR) || + (StateTerminationType::EARLY < type && + type <= StateTerminationType::SOLVERERR)) + return NodeColours[4]; + + return NodeColours[5]; +} + +void printIntermediateNode(std::uint32_t id, Node node, std::uint32_t depth) { + std::cout << 'N' << id << '[' << "tooltip=\"" + << branchTypeNames[std::get(node.kind)] << "\\n" + << "node: " << id << "\\nstate: " << node.stateID + << "\\nasm: " << node.asmLine << "\"];\n"; +} + +void printLeafNode(std::uint32_t id, Node node, std::uint32_t depth) { + const auto terminationType = std::get(node.kind); + const auto colour = terminationTypeColour(terminationType); + std::cout << 'N' << id << '[' << "tooltip=\"" + << terminationTypeNames[terminationType] << "\\n" + << "node: " << id << "\\nstate: " << node.stateID + << "\\nasm: " << node.asmLine << "\",color=" << colour << "];\n"; +} + +void printEdges(std::uint32_t id, Node node, std::uint32_t depth) { + std::cout << 'N' << id << "->{"; + if (node.left && node.right) { + std::cout << 'N' << node.left << " N" << node.right; + } else { + std::cout << 'N' << (node.left ? node.left : node.right); + } + std::cout << "};\n"; +} + +void printDOT(const Tree &tree) { + // header + // - style defaults to intermediate nodes + std::cout << "strict digraph PTree {\n" + "node[shape=point,width=0.15,color=darkgrey];\n" + "edge[color=darkgrey];\n\n"; + + // nodes + // - change colour for leaf nodes + // - attach branch and location info as tooltips + DFSVisitor nodeVisitor(tree, printIntermediateNode, printLeafNode); + + // edges + DFSVisitor edgeVisitor(tree, printEdges, nullptr); + + // footer + std::cout << '}' << std::endl; +} + +// instructions + +struct Info { + std::uint32_t noBranches{0}; + std::uint32_t noTerminations{0}; + std::map terminationTypes; +}; + +void printInstructions(const Tree &tree) { + std::map asmInfo; + + DFSVisitor visitor( + tree, + [&asmInfo](std::uint32_t id, Node node, std::uint32_t depth) { + asmInfo[node.asmLine].noBranches++; + }, + [&asmInfo](std::uint32_t id, Node node, std::uint32_t depth) { + auto &info = asmInfo[node.asmLine]; + info.noTerminations++; + info.terminationTypes[std::get(node.kind)]++; + }); + + std::cout << "asm line,branches,terminations,termination types\n"; + for (const auto &[asmLine, info] : asmInfo) { + std::cout << asmLine << ',' << info.noBranches << ',' << info.noTerminations + << ','; + std::string sep{""}; + for (const auto &[terminationType, count] : info.terminationTypes) { + std::cout << sep << terminationTypeNames[terminationType] << '(' << count + << ')'; + sep = ";"; + } + std::cout << '\n'; + } +} + +// terminations + +void printTerminations(const Tree &tree) { + if (tree.nodes.size() <= 1) { + std::cout << "Empty tree.\n"; + return; + } + + std::map terminations; + + DFSVisitor visitor( + tree, nullptr, + [&terminations](std::uint32_t id, Node node, std::uint32_t depth) { + terminations[std::get(node.kind)]++; + }); + + std::cout << "termination type,count\n"; + for (const auto &[terminationType, count] : terminations) + std::cout << terminationTypeNames[terminationType] << ',' << count << '\n'; +} + +// tree info + +void printTreeInfo(const Tree &tree) { + if (tree.nodes.size() <= 1) { + std::cout << "Empty tree.\n"; + return; + } + + const auto DI = getDepthInfo(tree); + + // determine average depth + std::uint64_t sum{0}; + for (size_t depth = 1; depth <= DI.maxDepth; ++depth) { + auto count = DI.depths[depth]; + if (count) + sum += count * depth; + } + double avgDepth = (double)sum / DI.noLeaves; + + std::cout << "nodes: " << DI.noNodes << '\n' + << "leaf nodes: " << DI.noLeaves + << (DI.noNodes && (DI.noLeaves != DI.noNodes / 2 + 1) + ? " (not a binary tree?!)" + : "") + << '\n' + << "max. depth: " << DI.maxDepth << '\n' + << "avg. depth: " << std::setprecision(2) << avgDepth << '\n'; +} diff --git a/tools/klee-ptree/Printers.h b/tools/klee-ptree/Printers.h new file mode 100644 index 0000000000..d20db4a107 --- /dev/null +++ b/tools/klee-ptree/Printers.h @@ -0,0 +1,30 @@ +//===-- Printers.h ----------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#pragma once + +#include "Tree.h" + +/// print branch types in csv format +void printBranches(const Tree &tree); + +/// print depths in csv format +void printDepths(const Tree &tree); + +/// print tree in dot format +void printDOT(const Tree &tree); + +/// print instruction information in csv format +void printInstructions(const Tree &tree); + +/// print termination types in csv format +void printTerminations(const Tree &tree); + +/// print tree/node information +void printTreeInfo(const Tree &tree); diff --git a/tools/klee-ptree/Tree.cpp b/tools/klee-ptree/Tree.cpp new file mode 100644 index 0000000000..207726005c --- /dev/null +++ b/tools/klee-ptree/Tree.cpp @@ -0,0 +1,208 @@ +//===-- Tree.cpp ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "Tree.h" + +#include + +#include +#include +#include + +Tree::Tree(const std::filesystem::path &path) { + // open db + ::sqlite3 *db; + if (sqlite3_open_v2(path.c_str(), &db, SQLITE_OPEN_READONLY, nullptr) != + SQLITE_OK) { + std::cerr << "Can't open process tree database: " << sqlite3_errmsg(db) + << std::endl; + exit(EXIT_FAILURE); + } + + // initialise prepared statement + ::sqlite3_stmt *readStmt; + std::string query{ + "SELECT ID, stateID, leftID, rightID, asmLine, kind FROM nodes;"}; + if (sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT, + &readStmt, nullptr) != SQLITE_OK) { + std::cerr << "Can't prepare read statement: " << sqlite3_errmsg(db) + << std::endl; + exit(EXIT_FAILURE); + } + + ::sqlite3_stmt *maxStmt; + query = "SELECT MAX(ID) FROM nodes;"; + if (sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT, + &maxStmt, nullptr) != SQLITE_OK) { + std::cerr << "Can't prepare max statement: " << sqlite3_errmsg(db) + << std::endl; + exit(EXIT_FAILURE); + } + + // read max id + int rc; + std::uint64_t maxID; + if ((rc = sqlite3_step(maxStmt)) == SQLITE_ROW) { + maxID = static_cast(sqlite3_column_int(maxStmt, 0)); + } else { + std::cerr << "Can't read maximum ID: " << sqlite3_errmsg(db) << std::endl; + exit(EXIT_FAILURE); + } + + // reserve space + nodes.resize(maxID + 1, {}); + + // read rows into vector + while ((rc = sqlite3_step(readStmt)) == SQLITE_ROW) { + const auto ID = static_cast(sqlite3_column_int(readStmt, 0)); + const auto stateID = + static_cast(sqlite3_column_int(readStmt, 1)); + const auto left = + static_cast(sqlite3_column_int(readStmt, 2)); + const auto right = + static_cast(sqlite3_column_int(readStmt, 3)); + const auto asmLine = + static_cast(sqlite3_column_int(readStmt, 4)); + const auto tmpKind = + static_cast(sqlite3_column_int(readStmt, 5)); + + // sanity checks: valid indices + if (ID == 0) { + std::cerr << "PTree DB contains illegal node ID (0)" << std::endl; + exit(EXIT_FAILURE); + } + + if (left > maxID || right > maxID) { + std::cerr << "PTree DB contains references to non-existing nodes (> max. " + "ID) in node " + << ID << std::endl; + exit(EXIT_FAILURE); + } + + if ((left == 0 && right != 0) || (left != 0 && right == 0)) { + std::cerr << "Warning: PTree DB contains ambiguous node (0 vs. non-0 " + "children): " + << ID << std::endl; + } + + // determine node kind (branch or leaf node) + decltype(Node::kind) kind; + if (left == 0 && right == 0) { + kind = static_cast(tmpKind); + } else { + kind = static_cast(tmpKind); + } + + // store children + nodes[ID] = {.left = left, + .right = right, + .stateID = stateID, + .asmLine = asmLine, + .kind = kind}; + } + + if (rc != SQLITE_DONE) { + std::cerr << "Error while reading database: " << sqlite3_errmsg(db) + << std::endl; + exit(EXIT_FAILURE); + } + + // close db + sqlite3_finalize(maxStmt); + sqlite3_finalize(readStmt); + sqlite3_close(db); + + // initialise global sets/maps and sanity check + initialiseValidTypes(); + sanityCheck(); + initialiseTypeNames(); +} + +void Tree::initialiseTypeNames() { +// branch types +#undef BTYPE +#define BTYPE(Name, I) branchTypeNames[BranchType::Name] = #Name; + BRANCH_TYPES + +// termination types +#undef TTYPE +#define TTYPE(Name, I, S) \ + terminationTypeNames[StateTerminationType::Name] = #Name; + TERMINATION_TYPES +} + +void Tree::initialiseValidTypes() { +// branch types +#undef BTYPE +#define BTYPE(Name, I) validBranchTypes.insert(BranchType::Name); + BRANCH_TYPES + +// termination types +#undef TTYPE +#define TTYPE(Name, I, S) \ + validTerminationTypes.insert(StateTerminationType::Name); + TERMINATION_TYPES +} + +void Tree::sanityCheck() { + if (nodes.size() <= 1) // [0] is unused + return; + + std::vector stack{1}; // root ID + std::unordered_set visited; + while (!stack.empty()) { + const auto id = stack.back(); + stack.pop_back(); + + if (!visited.insert(id).second) { + std::cerr << "PTree DB contains duplicate child reference or circular " + "structure. Affected node: " + << id << std::endl; + exit(EXIT_FAILURE); + } + + const auto &node = nodes[id]; + + // default constructed "gap" in vector + if (!node.left && !node.right && + std::holds_alternative(node.kind) && + static_cast(std::get(node.kind)) == 0u) { + std::cerr << "PTree DB references undefined node. Affected node: " << id + << std::endl; + exit(EXIT_FAILURE); + } + + if (node.left || node.right) { + if (node.right) + stack.push_back(node.right); + if (node.left) + stack.push_back(node.left); + // valid branch types + assert(std::holds_alternative(node.kind)); + const auto branchType = std::get(node.kind); + if (validBranchTypes.count(branchType) == 0) { + std::cerr << "PTree DB contains unknown branch type (" + << (unsigned)static_cast(branchType) + << ") in node " << id << std::endl; + exit(EXIT_FAILURE); + } + } else { + // valid termination types + assert(std::holds_alternative(node.kind)); + const auto terminationType = std::get(node.kind); + if (validTerminationTypes.count(terminationType) == 0 || + terminationType == StateTerminationType::RUNNING) { + std::cerr << "PTree DB contains unknown termination type (" + << (unsigned)static_cast(terminationType) + << ") in node " << id << std::endl; + exit(EXIT_FAILURE); + } + } + } +} diff --git a/tools/klee-ptree/Tree.h b/tools/klee-ptree/Tree.h new file mode 100644 index 0000000000..65b7baeb1f --- /dev/null +++ b/tools/klee-ptree/Tree.h @@ -0,0 +1,53 @@ +//===-- Tree.h --------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#pragma once + +#include "klee/Core/BranchTypes.h" +#include "klee/Core/TerminationTypes.h" + +#include +#include +#include +#include +#include +#include + +inline std::unordered_set validBranchTypes; +inline std::unordered_set validTerminationTypes; +inline std::unordered_map branchTypeNames; +inline std::unordered_map + terminationTypeNames; + +///@brief A Tree node representing a PTreeNode +struct Node final { + std::uint32_t left{0}; + std::uint32_t right{0}; + std::uint32_t stateID{0}; + std::uint32_t asmLine{0}; + std::variant kind{BranchType::NONE}; +}; + +///@brief An in-memory representation of a complete process tree +class Tree final { + /// Creates branchTypeNames and terminationTypeNames maps + static void initialiseTypeNames(); + /// Creates validBranchTypes and validTerminationTypes sets + static void initialiseValidTypes(); + /// Checks tree properties (e.g. valid branch/termination types) + void sanityCheck(); + +public: + /// sorted vector of Nodes default initialised with BranchType::NONE + std::vector nodes; // PTree node IDs start with 1! + + /// Reads complete ptree.db into memory + explicit Tree(const std::filesystem::path &path); + ~Tree() = default; +}; diff --git a/tools/klee-ptree/main.cpp b/tools/klee-ptree/main.cpp new file mode 100644 index 0000000000..d5cd305794 --- /dev/null +++ b/tools/klee-ptree/main.cpp @@ -0,0 +1,69 @@ +//===-- main.cpp ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include +#include +#include + +#include "Printers.h" + +namespace fs = std::filesystem; + +void print_usage() { + std::cout << "Usage: klee-ptree