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/.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 }} diff --git a/CMakeLists.txt b/CMakeLists.txt index 024d8a5003..cbdb6a71e5 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") @@ -319,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/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/ 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/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/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/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/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 { 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/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/CoreStats.cpp b/lib/Core/CoreStats.cpp index 2589d7dac4..48eb1e85b6 100644 --- a/lib/Core/CoreStats.cpp +++ b/lib/Core/CoreStats.cpp @@ -8,14 +8,18 @@ //===----------------------------------------------------------------------===// #include "CoreStats.h" +#include "klee/Support/ErrorHandling.h" + 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"); +Statistic stats::inhibitedForks("InhibitedForks", "InhibForks"); Statistic stats::instructionRealTime("InstructionRealTimes", "Ireal"); Statistic stats::instructionTime("InstructionTimes", "Itime"); Statistic stats::instructions("Instructions", "I"); @@ -26,3 +30,28 @@ 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)); + } +} + + +// 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 354706f589..609e976a6a 100644 --- a/lib/Core/CoreStats.h +++ b/lib/Core/CoreStats.h @@ -10,6 +10,8 @@ #ifndef KLEE_CORESTATS_H #define KLEE_CORESTATS_H +#include "klee/Core/BranchTypes.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Statistics/Statistic.h" namespace klee { @@ -27,9 +29,15 @@ namespace stats { extern Statistic forkTime; extern Statistic solverTime; + /// The number of external calls. + extern Statistic externalCalls; + /// 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; @@ -43,6 +51,18 @@ 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 + + /// 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/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/Executor.cpp b/lib/Core/Executor.cpp index d644d647dd..e78b45a5fe 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" @@ -437,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]")), @@ -898,8 +898,10 @@ void Executor::branch(ExecutionState &state, result.push_back(nullptr); } } + 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); @@ -952,7 +954,7 @@ void Executor::branch(ExecutionState &state, if (OnlyReplaySeeds) { for (unsigned i=0; i condition, addConstraint(current, Expr::createIsZero(condition)); res = Solver::False; } + ++stats::inhibitedForks; } } } @@ -1179,6 +1182,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 @@ -1956,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. @@ -1977,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. @@ -2195,7 +2202,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 @@ -2268,7 +2275,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) { @@ -3164,8 +3171,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (iIdx >= vt->getNumElements()) { // Out of bounds write - terminateStateOnError(state, "Out of bounds write when inserting element", - StateTerminationType::BadVectorAccess); + terminateStateOnProgramError(state, + "Out of bounds write when inserting element", + StateTerminationType::BadVectorAccess); return; } @@ -3205,8 +3213,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; } @@ -3622,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); @@ -3655,41 +3665,57 @@ 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, terminationTypeFileExtension(StateTerminationType::Exit).c_str()); interpreterHandler->incPathsCompleted(); - terminateState(state); + terminateState(state, StateTerminationType::Exit); } 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); + terminateState(state, reason); +} + +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::terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message) { - terminateStateOnError(state, message, StateTerminationType::User, ""); +void Executor::terminateStateEarlyUser(ExecutionState &state, + const llvm::Twine &message) { + ++stats::terminationEarlyUser; + terminateStateEarly(state, message, StateTerminationType::SilentExit); } const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state, @@ -3782,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; @@ -3790,15 +3816,41 @@ 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, + bool writeErr) { + ++stats::terminationUserError; + if (writeErr) { + terminateStateOnError(state, message, StateTerminationType::User, ""); + } else { + terminateState(state, StateTerminationType::User); + } +} + // XXX shoot me static const char *okExternalsList[] = { "printf", "fprintf", @@ -3942,14 +3994,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; } @@ -4132,8 +4185,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()); } } } @@ -4162,13 +4216,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); @@ -4212,14 +4266,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)); } } @@ -4277,8 +4332,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); @@ -4321,8 +4376,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); @@ -4347,9 +4402,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; @@ -4361,17 +4416,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)); } } } @@ -4544,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 c821b987bb..ca311e9168 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -410,8 +410,9 @@ class Executor : public Interpreter { const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, llvm::Instruction** lastInstruction); - /// Remove state from queue and delete state - void terminateState(ExecutionState &state); + /// Remove state from queue and delete state. This function should only be + /// used in the termination functions below. + void terminateState(ExecutionState &state, StateTerminationType reason); /// Call exit handler and terminate state normally /// (end of execution path) @@ -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) @@ -444,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/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/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/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 f4b09f367e..283aab482b 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()); @@ -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); } @@ -759,19 +755,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 539b913c42..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" @@ -430,28 +431,41 @@ 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," - << "FullBranches INTEGER," - << "PartialBranches INTEGER," - << "NumBranches INTEGER," - << "UserTime REAL," - << "NumStates INTEGER," - << "MallocUsage INTEGER," - << "NumQueries INTEGER," - << "NumQueryConstructs INTEGER," - << "WallTime REAL," - << "CoveredInstructions INTEGER," - << "UncoveredInstructions INTEGER," - << "QueryTime INTEGER," - << "SolverTime INTEGER," - << "CexCacheTime INTEGER," - << "ForkTime INTEGER," - << "ResolveTime INTEGER," - << "QueryCexCacheMisses INTEGER," - << "QueryCexCacheHits 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 + TERMINATION_CLASSES + << "ArrayHashTime INTEGER" << ')'; char *zErrMsg = nullptr; if(sqlite3_exec(statsFile, create.str().c_str(), nullptr, nullptr, &zErrMsg)) { @@ -464,48 +478,75 @@ 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 "," + #undef TCLASS + #define TCLASS(Name, I) << "Termination" #Name "," insert << "INSERT OR FAIL INTO stats (" - << "Instructions," - << "FullBranches," - << "PartialBranches," - << "NumBranches," - << "UserTime," - << "NumStates," - << "MallocUsage," - << "NumQueries," - << "NumQueryConstructs," - << "WallTime," - << "CoveredInstructions," - << "UncoveredInstructions," - << "QueryTime," - << "SolverTime," - << "CexCacheTime," - << "ForkTime," - << "ResolveTime," - << "QueryCexCacheMisses," - << "QueryCexCacheHits," - << "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 + TERMINATION_CLASSES + << "ArrayHashTime" + << ')'; + #undef BTYPE + #define BTYPE(Name, I) << "?," + #undef TCLASS + #define TCLASS(Name, I) << "?," + insert << " VALUES (" + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + << "?," + BRANCH_TYPES + TERMINATION_CLASSES + << "? " << ')'; if(sqlite3_prepare_v2(statsFile, insert.str().c_str(), -1, &insertStmt, nullptr) != SQLITE_OK) { @@ -518,29 +559,43 @@ 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::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::queryCexCacheMisses); - sqlite3_bind_int64(insertStmt, 19, stats::queryCexCacheHits); + #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); + 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 + TERMINATION_CLASSES #ifdef KLEE_ARRAY_DEBUG - sqlite3_bind_int64(insertStmt, 20, stats::arrayHashTime); + sqlite3_bind_int64(insertStmt, arg++, stats::arrayHashTime); #else - sqlite3_bind_int64(insertStmt, 20, -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/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/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/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(); } } 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/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); 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/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 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/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/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 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 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/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/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/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/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/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/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/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; 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/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-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