From 2ce22af434e383cf0c2c65e4da829de630b6cd9d Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sat, 13 Sep 2014 11:29:19 -0700 Subject: Add KLEE specific DEBUG macros. - This allows us to build in +Asserts mode even when LLVM isn't (by disabling the checks in that mode). - Eventually it would be nice to just move off of LLVM's DEBUG infrastructure entirely and just have our own copy, but this works for now. - Fixes #150. --- autoconf/configure.ac | 11 +++++++++++ configure | 15 +++++++++++++++ include/klee/Config/config.h.in | 3 +++ include/klee/Internal/Support/Debug.h | 27 ++++++++++++++++++++++++++ lib/Core/SpecialFunctionHandler.cpp | 4 ++-- lib/Module/InstructionInfoTable.cpp | 1 - lib/Module/KModule.cpp | 13 ++++++++----- lib/Module/ModuleUtil.cpp | 36 ++++++++++++++++++++--------------- lib/Solver/FastCexSolver.cpp | 9 +++++---- lib/Solver/IndependentSolver.cpp | 6 +++--- lib/Support/TreeStream.cpp | 17 ++++++++++------- tools/klee/main.cpp | 14 +++++++------- 12 files changed, 112 insertions(+), 44 deletions(-) create mode 100644 include/klee/Internal/Support/Debug.h diff --git a/autoconf/configure.ac b/autoconf/configure.ac index edeacc8c..18822396 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -179,6 +179,17 @@ fi AC_MSG_RESULT([$llvm_build_mode]) AC_SUBST(LLVM_BUILD_MODE,$llvm_build_mode) +dnl Check if we are building against a +Asserts LLVM, and enable the DEBUG_* +dnl macros if so (they use symbols only available in +Asserts builds). +AC_MSG_CHECKING([llvm has asserts enabled]) +if test `expr "$llvm_build_mode" : ".*Asserts.*"` -ne 0; then + llvm_has_asserts_enabled=1 + AC_DEFINE_UNQUOTED(ENABLE_KLEE_DEBUG, 1, [Enable KLEE DEBUG checks]) +else + llvm_has_asserts_enabled=0 +fi +AC_MSG_RESULT([$llvm_has_asserts_enabled]) + dnl ************************************************************************** dnl Detect a LLVM Bitcode compiler for building KLEE runtime library diff --git a/configure b/configure index 039617d7..38404d73 100755 --- a/configure +++ b/configure @@ -2145,6 +2145,21 @@ echo "${ECHO_T}$llvm_build_mode" >&6; } LLVM_BUILD_MODE=$llvm_build_mode +{ echo "$as_me:$LINENO: checking llvm has asserts enabled" >&5 +echo $ECHO_N "checking llvm has asserts enabled... $ECHO_C" >&6; } +if test `expr "$llvm_build_mode" : ".*Asserts.*"` -ne 0; then + llvm_has_asserts_enabled=1 + +cat >>confdefs.h <<_ACEOF +#define ENABLE_KLEE_DEBUG 1 +_ACEOF + +else + llvm_has_asserts_enabled=0 +fi +{ echo "$as_me:$LINENO: result: $llvm_has_asserts_enabled" >&5 +echo "${ECHO_T}$llvm_has_asserts_enabled" >&6; } + { echo "$as_me:$LINENO: checking LLVM Bitcode compiler" >&5 echo $ECHO_N "checking LLVM Bitcode compiler... $ECHO_C" >&6; } diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index b97f0b05..6f24cde3 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -3,6 +3,9 @@ #ifndef KLEE_CONFIG_CONFIG_H #define KLEE_CONFIG_CONFIG_H +/* Enable KLEE DEBUG checks */ +#undef ENABLE_KLEE_DEBUG + /* Does the platform use __ctype_b_loc, etc. */ #undef HAVE_CTYPE_EXTERNALS diff --git a/include/klee/Internal/Support/Debug.h b/include/klee/Internal/Support/Debug.h new file mode 100644 index 00000000..8f46b93b --- /dev/null +++ b/include/klee/Internal/Support/Debug.h @@ -0,0 +1,27 @@ +//===-- Debug.h -------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_INTERNAL_SUPPORT_DEBUG_H +#define KLEE_INTERNAL_SUPPORT_DEBUG_H + +#include +#include + +// We define wrappers around the LLVM DEBUG macros that are conditionalized on +// whether the LLVM we are building against has the symbols needed by these +// checks. + +#ifdef ENABLE_KLEE_DEBUG +#define KLEE_DEBUG_WITH_TYPE(TYPE, X) DEBUG_WITH_TYPE(TYPE, X) +#else +#define KLEE_DEBUG_WITH_TYPE(TYPE, X) do { } while (0) +#endif +#define KLEE_DEBUG(X) KLEE_DEBUG_WITH_TYPE(DEBUG_TYPE, X) + +#endif diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index a7a1b32e..8625fa63 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -17,6 +17,7 @@ #include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Module/KModule.h" +#include "klee/Internal/Support/Debug.h" #include "Executor.h" #include "MemoryManager.h" @@ -27,7 +28,6 @@ #include "llvm/Module.h" #endif #include "llvm/ADT/Twine.h" -#include "llvm/Support/Debug.h" #include @@ -280,7 +280,7 @@ void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state, "invalid number of arguments to klee_alias_function"); std::string old_fn = readStringAtAddress(state, arguments[0]); std::string new_fn = readStringAtAddress(state, arguments[1]); - DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn + KLEE_DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn << "() with " << new_fn << "()\n"); if (old_fn == new_fn) state.removeFnAlias(old_fn); diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp index 82d60708..8d27e426 100644 --- a/lib/Module/InstructionInfoTable.cpp +++ b/lib/Module/InstructionInfoTable.cpp @@ -33,7 +33,6 @@ #include "llvm/Analysis/DebugInfo.h" #endif #include "llvm/Analysis/ValueTracking.h" -#include "llvm/Support/Debug.h" #include "llvm/Support/ErrorHandling.h" #include diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 697b6ea9..57e0c4fe 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -19,6 +19,7 @@ #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Module/InstructionInfoTable.h" +#include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/ModuleUtil.h" #include "llvm/Bitcode/ReaderWriter.h" @@ -51,7 +52,6 @@ #include #include -#include #include @@ -234,7 +234,8 @@ static void inlineChecks(Module *module, const char * functionName) { Function* runtimeCheckCall = module->getFunction(functionName); if (runtimeCheckCall == 0) { - DEBUG( klee_warning("Failed to inline %s because no calls were made to it in module", functionName) ); + KLEE_DEBUG(klee_warning("Failed to inline %s because no calls were made " + "to it in module", functionName)); return; } @@ -264,17 +265,19 @@ static void inlineChecks(Module *module, const char * functionName) { } } - DEBUG( klee_message("Tried to inline calls to %s. %u successes, %u failures",functionName, successCount, failCount) ); + KLEE_DEBUG(klee_message("Tried to inline calls to %s. %u successes, " + "%u failures", functionName, successCount, + failCount)); } void KModule::addInternalFunction(const char* functionName){ Function* internalFunction = module->getFunction(functionName); if (!internalFunction) { - DEBUG_WITH_TYPE("KModule", klee_warning( + KLEE_DEBUG_WITH_TYPE("KModule", klee_warning( "Failed to add internal function %s. Not found.", functionName)); return ; } - DEBUG( klee_message("Added function %s.",functionName)); + KLEE_DEBUG(klee_message("Added function %s.",functionName)); internalFunctions.insert(internalFunction); } diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index d00cf574..be1ea4c1 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -8,7 +8,10 @@ //===----------------------------------------------------------------------===// #include "klee/Internal/Support/ModuleUtil.h" + #include "klee/Config/Version.h" +#include "klee/Internal/Support/Debug.h" + // FIXME: This does not belong here. #include "../Core/Common.h" #include "../Core/SpecialFunctionHandler.h" @@ -42,7 +45,6 @@ #include "llvm/Assembly/AssemblyAnnotationWriter.h" #include "llvm/Support/CFG.h" #include "llvm/Support/CallSite.h" -#include "llvm/Support/Debug.h" #include "llvm/Support/InstIterator.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Analysis/ValueTracking.h" @@ -77,7 +79,8 @@ GetAllUndefinedSymbols(Module *M, std::set &UndefinedSymbols) { static const std::string llvmIntrinsicPrefix="llvm."; std::set DefinedSymbols; UndefinedSymbols.clear(); - DEBUG_WITH_TYPE("klee_linker", dbgs() << "*** Computing undefined symbols ***\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", + dbgs() << "*** Computing undefined symbols ***\n"); for (Module::iterator I = M->begin(), E = M->end(); I != E; ++I) if (I->hasName()) { @@ -124,14 +127,15 @@ GetAllUndefinedSymbols(Module *M, std::set &UndefinedSymbols) { if ( (I->size() >= llvmIntrinsicPrefix.size() ) && (I->compare(0, llvmIntrinsicPrefix.size(), llvmIntrinsicPrefix) == 0) ) { - DEBUG_WITH_TYPE("klee_linker", dbgs() << "LLVM intrinsic " << *I << + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "LLVM intrinsic " << *I << " has will be removed from undefined symbols"<< "\n"); SymbolsToRemove.push_back(*I); continue; } // Symbol really is undefined - DEBUG_WITH_TYPE("klee_linker", dbgs() << "Symbol " << *I << " is undefined.\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", + dbgs() << "Symbol " << *I << " is undefined.\n"); } // Remove KLEE intrinsics from set of undefined symbols @@ -142,15 +146,17 @@ GetAllUndefinedSymbols(Module *M, std::set &UndefinedSymbols) { continue; SymbolsToRemove.push_back(sf->name); - DEBUG_WITH_TYPE("klee_linker", dbgs() << "KLEE intrinsic " << sf->name << - " has will be removed from undefined symbols"<< "\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", + dbgs() << "KLEE intrinsic " << sf->name << + " has will be removed from undefined symbols"<< "\n"); } // Now remove the symbols from undefined set. for (size_t i = 0, j = SymbolsToRemove.size(); i < j; ++i ) UndefinedSymbols.erase(SymbolsToRemove[i]); - DEBUG_WITH_TYPE("klee_linker", dbgs() << "*** Finished computing undefined symbols ***\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", + dbgs() << "*** Finished computing undefined symbols ***\n"); } @@ -187,11 +193,11 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er if (undefinedSymbols.size() == 0) { // Nothing to do - DEBUG_WITH_TYPE("klee_linker", dbgs() << "No undefined symbols. Not linking anything in!\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "No undefined symbols. Not linking anything in!\n"); return true; } - DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading modules\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading modules\n"); // Load all bitcode files in to memory so we can examine their symbols for (object::Archive::child_iterator AI = archive->begin_children(), AE = archive->end_children(); AI != AE; ++AI) @@ -202,7 +208,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er if ( ec == errc::success ) { - DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading archive member " << memberName << "\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading archive member " << memberName << "\n"); } else { @@ -262,7 +268,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er } - DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loaded " << archiveModules.size() << " modules\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loaded " << archiveModules.size() << " modules\n"); std::set previouslyUndefinedSymbols; @@ -294,7 +300,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er { if (GV->isDeclaration()) continue; // Not a definition - DEBUG_WITH_TYPE("klee_linker", dbgs() << "Found " << GV->getName() << + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Found " << GV->getName() << " in " << M->getModuleIdentifier() << "\n"); @@ -310,7 +316,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er { // Link succeed, now clean up modulesLoadedOnPass++; - DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking succeeded.\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking succeeded.\n"); delete M; archiveModules[i] = 0; @@ -327,7 +333,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er } passCounter++; - DEBUG_WITH_TYPE("klee_linker", dbgs() << "Completed " << passCounter << + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Completed " << passCounter << " linker passes.\n" << modulesLoadedOnPass << " modules loaded on the last pass\n"); } while (undefinedSymbols != previouslyUndefinedSymbols); // Iterate until we reach a fixed point @@ -344,7 +350,7 @@ static bool linkBCA(object::Archive* archive, Module* composite, std::string& er Module *klee::linkWithLibrary(Module *module, const std::string &libraryName) { -DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking file " << libraryName << "\n"); + KLEE_DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking file " << libraryName << "\n"); #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) if (!sys::fs::exists(libraryName)) { klee_error("Link with library %s failed. No such file.", diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 57e44806..73403882 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// +#define DEBUG_TYPE "cex-solver" #include "klee/Solver.h" #include "klee/Constraints.h" @@ -16,10 +17,9 @@ #include "klee/util/ExprRangeEvaluator.h" #include "klee/util/ExprVisitor.h" // FIXME: Use APInt. +#include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/IntEvaluation.h" -#define DEBUG_TYPE "cex-solver" -#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include #include @@ -441,7 +441,8 @@ public: } void propogatePossibleValues(ref e, CexValueData range) { - DEBUG(llvm::errs() << "propogate: " << range << " for\n" << e << "\n";); + KLEE_DEBUG(llvm::errs() << "propogate: " << range << " for\n" + << e << "\n"); switch (e->getKind()) { case Expr::Constant: @@ -1008,7 +1009,7 @@ static bool propogateValues(const Query& query, CexData &cd, cd.propogateExactValue(query.expr, 0); } - DEBUG(cd.dump();); + KLEE_DEBUG(cd.dump()); // Check the result. bool hasSatisfyingAssignment = true; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 46b4ee56..dcaecb05 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -7,16 +7,16 @@ // //===----------------------------------------------------------------------===// +#define DEBUG_TYPE "independent-solver" #include "klee/Solver.h" #include "klee/Expr.h" #include "klee/Constraints.h" #include "klee/SolverImpl.h" +#include "klee/Internal/Support/Debug.h" #include "klee/util/ExprUtil.h" -#define DEBUG_TYPE "independent-solver" -#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include #include @@ -251,7 +251,7 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); -DEBUG( + KLEE_DEBUG( std::set< ref > reqset(result.begin(), result.end()); errs() << "--\n"; errs() << "Q: " << query.expr << "\n"; diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp index 0d5e4568..74ffe3ba 100644 --- a/lib/Support/TreeStream.cpp +++ b/lib/Support/TreeStream.cpp @@ -9,13 +9,14 @@ #include "klee/Internal/ADT/TreeStream.h" +#include "klee/Internal/Support/Debug.h" + #include #include #include #include #include -#include "llvm/Support/Debug.h" #include "llvm/Support/raw_ostream.h" #include @@ -106,7 +107,7 @@ void TreeStreamWriter::readStream(TreeStreamID streamID, std::ifstream is(path.c_str(), std::ios::in | std::ios::binary); assert(is.good()); - DEBUG_WITH_TYPE("TreeStreamWriter", + KLEE_DEBUG_WITH_TYPE("TreeStreamWriter", llvm::errs() << "finding chain for: " << streamID << "\n"); std::map parents; @@ -137,11 +138,13 @@ void TreeStreamWriter::readStream(TreeStreamID streamID, while (size--) is.get(); } } - DEBUG(llvm::errs() << "roots: "; - for (size_t i = 0, e = roots.size(); i < e; ++i) { - llvm::errs() << roots[i] << " "; - } - llvm::errs() << "\n";); + KLEE_DEBUG({ + llvm::errs() << "roots: "; + for (size_t i = 0, e = roots.size(); i < e; ++i) { + llvm::errs() << roots[i] << " "; + } + llvm::errs() << "\n"; + }); is.seekg(0, std::ios::beg); for (;;) { unsigned id; diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index f0f8cbe2..4411f73a 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -10,6 +10,7 @@ #include "klee/Config/Version.h" #include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/TreeStream.h" +#include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" @@ -41,7 +42,6 @@ #include "llvm/Support/FileSystem.h" #include "llvm/Bitcode/ReaderWriter.h" #include "llvm/Support/CommandLine.h" -#include "llvm/Support/Debug.h" #include "llvm/Support/ManagedStatic.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/raw_ostream.h" @@ -584,21 +584,21 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { if ( strcmp(toolRoot.c_str(), KLEE_INSTALL_BIN_DIR ) == 0) { - DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << - "Using installed KLEE library runtime: "); + KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << + "Using installed KLEE library runtime: "); libDir = KLEE_INSTALL_LIB_DIR ; } else { - DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << - "Using build directory KLEE library runtime :"); + KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << + "Using build directory KLEE library runtime :"); libDir = KLEE_DIR; llvm::sys::path::append(libDir,RUNTIME_CONFIGURATION); llvm::sys::path::append(libDir,"lib"); } - DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << - libDir.c_str() << "\n"); + KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << + libDir.c_str() << "\n"); return libDir.str(); } -- cgit 1.4.1