about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--autoconf/configure.ac11
-rwxr-xr-xconfigure15
-rw-r--r--include/klee/Config/config.h.in3
-rw-r--r--include/klee/Internal/Support/Debug.h27
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp4
-rw-r--r--lib/Module/InstructionInfoTable.cpp1
-rw-r--r--lib/Module/KModule.cpp13
-rw-r--r--lib/Module/ModuleUtil.cpp36
-rw-r--r--lib/Solver/FastCexSolver.cpp9
-rw-r--r--lib/Solver/IndependentSolver.cpp6
-rw-r--r--lib/Support/TreeStream.cpp17
-rw-r--r--tools/klee/main.cpp14
12 files changed, 112 insertions, 44 deletions
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 <klee/Config/config.h>
+#include <llvm/Support/Debug.h>
+
+// 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 <errno.h>
 
@@ -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 <map>
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 <llvm/Transforms/Utils/Cloning.h>
 #include <llvm/Support/InstIterator.h>
-#include <llvm/Support/Debug.h>
 
 #include <sstream>
 
@@ -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<std::string> &UndefinedSymbols) {
   static const std::string llvmIntrinsicPrefix="llvm.";
   std::set<std::string> 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<std::string> &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<std::string> &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<std::string> 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 <sstream>
 #include <cassert>
@@ -441,7 +441,8 @@ public:
   }
 
   void propogatePossibleValues(ref<Expr> 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 <map>
 #include <vector>
@@ -251,7 +251,7 @@ IndependentElementSet getIndependentConstraints(const Query& query,
     worklist.swap(newWorklist);
   } while (!done);
 
-DEBUG(
+  KLEE_DEBUG(
     std::set< ref<Expr> > 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 <cassert>
 #include <iomanip>
 #include <fstream>
 #include <iterator>
 #include <map>
 
-#include "llvm/Support/Debug.h"
 #include "llvm/Support/raw_ostream.h"
 #include <string.h>
 
@@ -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<unsigned,unsigned> 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();
 }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-10 22:54:29 +0000