Merge pull request #444 from andreamattavelli/refactor_warnings

Refactoring logging information

6 files changed, 37 insertions, 40 deletions

diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 2df87d51..debb1e9e 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -12,6 +12,7 @@
  */
 #include "klee/Common.h"
 #include "klee/CommandLine.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "llvm/Support/raw_ostream.h"
 
 namespace klee {
@@ -24,15 +25,15 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
   if (optionIsSet(queryLoggingOptions, SOLVER_PC)) {
     solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath,
                                    MinQueryTimeToLog);
-    llvm::errs() << "Logging queries that reach solver in .pc format to "
-                 << baseSolverQueryPCLogPath.c_str() << "\n";
+    klee_message("Logging queries that reach solver in .pc format to %s\n",
+                 baseSolverQueryPCLogPath.c_str());
   }
 
   if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) {
     solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath,
                                        MinQueryTimeToLog);
-    llvm::errs() << "Logging queries that reach solver in .smt2 format to "
-                 << baseSolverQuerySMT2LogPath.c_str() << "\n";
+    klee_message("Logging queries that reach solver in .smt2 format to %s\n",
+                 baseSolverQuerySMT2LogPath.c_str());
   }
 
   if (UseFastCexSolver)
@@ -52,15 +53,15 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
 
   if (optionIsSet(queryLoggingOptions, ALL_PC)) {
     solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog);
-    llvm::errs() << "Logging all queries in .pc format to "
-                 << queryPCLogPath.c_str() << "\n";
+    klee_message("Logging all queries in .pc format to %s\n",
+                 queryPCLogPath.c_str());
   }
 
   if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) {
     solver =
         createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog);
-    llvm::errs() << "Logging all queries in .smt2 format to "
-                 << querySMT2LogPath.c_str() << "\n";
+    klee_message("Logging all queries in .smt2 format to %s\n",
+                 querySMT2LogPath.c_str());
   }
   if (DebugCrossCheckCoreSolverWith != NO_SOLVER) {
     Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 8b885527..1df51b4d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -356,8 +356,7 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih)
   if (coreSolverTimeout) UseForkedCoreSolver = true;
   Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
   if (!coreSolver) {
-    llvm::errs() << "Failed to create core solver\n";
-    exit(1);
+    klee_error("Failed to create core solver\n");
   }
   Solver *solver = constructSolverChain(
       coreSolver,
@@ -1481,9 +1480,8 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) {
         GlobalValue *old_gv = gv;
         gv = currModule->getNamedValue(alias);
         if (!gv) {
-          llvm::errs() << "Function " << alias << "(), alias for " 
-                       << old_gv->getName() << " not found!\n";
-          assert(0 && "function alias not found");
+          klee_error("Function %s(), alias for %s not found!\n", alias.c_str(),
+                     old_gv->getName().str().c_str());
         }
       }
      
@@ -3018,8 +3016,8 @@ void Executor::callExternalFunction(ExecutionState &state,
     return;
   
   if (NoExternals && !okExternals.count(function->getName())) {
-    llvm::errs() << "KLEE:ERROR: Calling not-OK external function : "
-                 << function->getName().str() << "\n";
+    klee_warning("Calling not-OK external function : %s\n",
+               function->getName().str().c_str());
     terminateStateOnError(state, "externals disallowed", User);
     return;
   }
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 973057c3..3bfcd6b3 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -527,8 +527,8 @@ ExecutionState &BatchingSearcher::selectState() {
     if (lastState) {
       double delta = util::getWallTime()-lastStartTime;
       if (delta>timeBudget*1.1) {
-        llvm::errs() << "KLEE: increased time budget from " << timeBudget
-                     << " to " << delta << "\n";
+        klee_message("KLEE: increased time budget from %f to %f\n", timeBudget,
+                     delta);
         timeBudget = delta;
       }
     }
@@ -601,7 +601,7 @@ void IterativeDeepeningTimeSearcher::update(
 
   if (baseSearcher->empty()) {
     time *= 2;
-    llvm::errs() << "KLEE: increasing time budget to: " << time << "\n";
+    klee_message("KLEE: increased time budget to %f\n", time);
     std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
     baseSearcher->update(0, ps, std::vector<ExecutionState *>());
     pausedStates.clear();
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 411c07b1..6bfd79c1 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -397,9 +397,9 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
     // "occasion" return a status when the process was terminated by a
     // signal, so test signal first.
     if (WIFSIGNALED(status) || !WIFEXITED(status)) {
-      fprintf(stderr,
-              "error: metaSMT did not return successfully (status = %d) \n",
-              WTERMSIG(status));
+      klee_warning(
+          "error: metaSMT did not return successfully (status = %d) \n",
+          WTERMSIG(status));
       return (SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED);
     }
 
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 96a7dafa..1cbca566 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -7,6 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 #include "klee/Config/config.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #ifdef ENABLE_Z3
 #include "Z3Builder.h"
 #include "klee/Constraints.h"
@@ -285,8 +286,7 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse(
     if (strcmp(reason, "unknown") == 0) {
       return SolverImpl::SOLVER_RUN_STATUS_FAILURE;
     }
-    llvm::errs() << "Unexpected solver failure. Reason is \"" << reason
-                 << "\"\n";
+    klee_warning("Unexpected solver failure. Reason is \"%s,\"\n", reason);
     abort();
   }
   default:
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 1eab170f..e198697c 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -393,7 +393,7 @@ llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string &filename) {
   f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::raw_fd_ostream::F_Binary);
 #endif
   if (!Error.empty()) {
-    klee_error("error opening file \"%s\".  KLEE may have run out of file "
+    klee_warning("error opening file \"%s\".  KLEE may have run out of file "
                "descriptors: try to increase the maximum number of open file "
                "descriptors by using ulimit (%s).",
                filename.c_str(), Error.c_str());
@@ -1011,9 +1011,7 @@ static char *format_tdiff(char *buf, long seconds)
 
 #ifndef SUPPORT_KLEE_UCLIBC
 static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) {
-  fprintf(stderr, "error: invalid libc, no uclibc support!\n");
-  exit(1);
-  return 0;
+  klee_error("invalid libc, no uclibc support!\n");
 }
 #else
 static void replaceOrRenameFunction(llvm::Module *module,
@@ -1176,7 +1174,7 @@ int main(int argc, char **argv, char **envp) {
     if (pid<0) {
       klee_error("unable to fork watchdog");
     } else if (pid) {
-      fprintf(stderr, "KLEE: WATCHDOG: watching %d\n", pid);
+      klee_message("KLEE: WATCHDOG: watching %d\n", pid);
       fflush(stderr);
       sys::SetInterruptFunction(interrupt_handle_watchdog);
 
@@ -1193,7 +1191,7 @@ int main(int argc, char **argv, char **envp) {
           if (errno==ECHILD) { // No child, no need to watch but
                                // return error since we didn't catch
                                // the exit.
-            fprintf(stderr, "KLEE: watchdog exiting (no child)\n");
+            klee_warning("KLEE: watchdog exiting (no child)\n");
             return 1;
           } else if (errno!=EINTR) {
             perror("watchdog waitpid");
@@ -1208,13 +1206,16 @@ int main(int argc, char **argv, char **envp) {
             ++level;
 
             if (level==1) {
-              fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via INT\n");
+              klee_warning(
+                  "KLEE: WATCHDOG: time expired, attempting halt via INT\n");
               kill(pid, SIGINT);
             } else if (level==2) {
-              fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via gdb\n");
+              klee_warning(
+                  "KLEE: WATCHDOG: time expired, attempting halt via gdb\n");
               halt_via_gdb(pid);
             } else {
-              fprintf(stderr, "KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)\n");
+              klee_warning(
+                  "KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)\n");
               kill(pid, SIGKILL);
               return 1; // what more can we do
             }
@@ -1425,7 +1426,7 @@ int main(int argc, char **argv, char **envp) {
       if (out) {
         kTests.push_back(out);
       } else {
-        llvm::errs() << "KLEE: unable to open: " << *it << "\n";
+        klee_warning("unable to open: %s\n", (*it).c_str());
       }
     }
 
@@ -1462,8 +1463,7 @@ int main(int argc, char **argv, char **envp) {
          it != ie; ++it) {
       KTest *out = kTest_fromFile(it->c_str());
       if (!out) {
-        llvm::errs() << "KLEE: unable to open: " << *it << "\n";
-        exit(1);
+        klee_error("unable to open: %s\n", (*it).c_str());
       }
       seeds.push_back(out);
     }
@@ -1477,19 +1477,17 @@ int main(int argc, char **argv, char **envp) {
            it2 != ie; ++it2) {
         KTest *out = kTest_fromFile(it2->c_str());
         if (!out) {
-          llvm::errs() << "KLEE: unable to open: " << *it2 << "\n";
-          exit(1);
+          klee_error("unable to open: %s\n", (*it2).c_str());
         }
         seeds.push_back(out);
       }
       if (kTestFiles.empty()) {
-        llvm::errs() << "KLEE: seeds directory is empty: " << *it << "\n";
-        exit(1);
+        klee_error("seeds directory is empty: %s\n", (*it).c_str());
       }
     }
 
     if (!seeds.empty()) {
-      llvm::errs() << "KLEE: using " << seeds.size() << " seeds\n";
+      klee_message("KLEE: using %lu seeds\n", seeds.size());
       interpreter->useSeeds(&seeds);
     }
     if (RunInDir != "") {