about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2014-05-29 23:15:59 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2014-05-29 23:57:45 +0200
commitd934d983692c8952cdb887cbcd59f2df0001b9c0 (patch)
tree9179a257bb053ba0a0da0e9dc4d2c030202c0f28 /lib/Core/Executor.cpp
parentc2dec441f3f89916962175f0307b5c33473fa616 (diff)
downloadklee-d934d983692c8952cdb887cbcd59f2df0001b9c0.tar.gz
Refactoring from std::ostream to llvm::raw_ostream
According to LLVM: lightweight and simpler implementation of streams.
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r--lib/Core/Executor.cpp117
1 files changed, 58 insertions, 59 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index abb023eb..3a07138d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -86,8 +86,8 @@
 
 #include <cassert>
 #include <algorithm>
-#include <iostream>
 #include <iomanip>
+#include <iosfwd>
 #include <fstream>
 #include <sstream>
 #include <vector>
@@ -316,7 +316,7 @@ Executor::Executor(const InterpreterOptions &opts,
               assert(false);
               break;
     };
-    std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n";
+    llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
   }
   else {
     coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
@@ -1105,12 +1105,13 @@ Executor::toConstant(ExecutionState &state,
   bool success = solver->getValue(state, e, value);
   assert(success && "FIXME: Unhandled solver failure");
   (void) success;
-    
-  std::ostringstream os;
-  os << "silently concretizing (reason: " << reason << ") expression " << e 
-     << " to value " << value 
-     << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
-      
+
+  std::string str;
+  llvm::raw_string_ostream os(str);
+  os << "silently concretizing (reason: " << reason << ") expression " << e
+     << " to value " << value << " (" << (*(state.pc)).info->file << ":"
+     << (*(state.pc)).info->line << ")";
+
   if (AllExternalWarnings)
     klee_warning(reason, os.str().c_str());
   else
@@ -1167,7 +1168,7 @@ void Executor::executeGetValue(ExecutionState &state,
 void Executor::stepInstruction(ExecutionState &state) {
   if (DebugPrintInstructions) {
     printFileLine(state, state.pc);
-    std::cerr << std::setw(10) << stats::instructions << " ";
+    llvm::errs().indent(10) << stats::instructions << " ";
     llvm::errs() << *(state.pc->inst) << '\n';
   }
 
@@ -1351,10 +1352,10 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
 
 void Executor::printFileLine(ExecutionState &state, KInstruction *ki) {
   const InstructionInfo &ii = *ki->info;
-  if (ii.file != "") 
-    std::cerr << "     " << ii.file << ":" << ii.line << ":";
+  if (ii.file != "")
+    llvm::errs() << "     " << ii.file << ":" << ii.line << ":";
   else
-    std::cerr << "     [no debug info]:";
+    llvm::errs() << "     [no debug info]:";
 }
 
 /// Compute the true target of a function call, resolving LLVM and KLEE aliases
@@ -2624,7 +2625,7 @@ void Executor::run(ExecutionState &initialState) {
   
  dump:
   if (DumpStatesOnHalt && !states.empty()) {
-    std::cerr << "KLEE: halting execution, dumping remaining states\n";
+    llvm::errs() << "KLEE: halting execution, dumping remaining states\n";
     for (std::set<ExecutionState*>::iterator
            it = states.begin(), ie = states.end();
          it != ie; ++it) {
@@ -2638,7 +2639,8 @@ void Executor::run(ExecutionState &initialState) {
 
 std::string Executor::getAddressInfo(ExecutionState &state, 
                                      ref<Expr> address) const{
-  std::ostringstream info;
+  std::string Str;
+  llvm::raw_string_ostream info(Str);
   info << "\taddress: " << address << "\n";
   uint64_t example;
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
@@ -2786,8 +2788,9 @@ void Executor::terminateStateOnError(ExecutionState &state,
     }
     if (!EmitAllErrors)
       klee_message("NOTE: now ignoring this error at this location");
-    
-    std::ostringstream msg;
+
+    std::string MsgString;
+    llvm::raw_string_ostream msg(MsgString);
     msg << "Error: " << message << "\n";
     if (ii.file != "") {
       msg << "File: " << ii.file << "\n";
@@ -2800,7 +2803,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
     std::string info_str = info.str();
     if (info_str != "")
       msg << "Info: \n" << info_str;
-    interpreterHandler->processTestCase(state, msg.str().c_str(), suffix);
+    interpreterHandler->processTestCase(state, MsgString.c_str(), suffix);
   }
     
   terminateState(state);
@@ -2824,8 +2827,8 @@ void Executor::callExternalFunction(ExecutionState &state,
     return;
   
   if (NoExternals && !okExternals.count(function->getName())) {
-    std::cerr << "KLEE:ERROR: Calling not-OK external function : " 
-              << function->getName().str() << "\n";
+    llvm::errs() << "KLEE:ERROR: Calling not-OK external function : "
+                 << function->getName().str() << "\n";
     terminateStateOnError(state, "externals disallowed", "user.err");
     return;
   }
@@ -2864,7 +2867,9 @@ void Executor::callExternalFunction(ExecutionState &state,
   state.addressSpace.copyOutConcretes();
 
   if (!SuppressExternalWarnings) {
-    std::ostringstream os;
+
+    std::string TmpStr;
+    llvm::raw_string_ostream os(TmpStr);
     os << "calling external: " << function->getName().str() << "(";
     for (unsigned i=0; i<arguments.size(); i++) {
       os << arguments[i];
@@ -2923,7 +2928,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
                                  Expr::getMinBytesForWidth(e->getWidth()));
   ref<Expr> res = Expr::createTempRead(array, e->getWidth());
   ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
-  std::cerr << "Making symbolic: " << eq << "\n";
+  llvm::errs() << "Making symbolic: " << eq << "\n";
   state.addConstraint(eq);
   return res;
 }
@@ -3035,7 +3040,9 @@ void Executor::executeAlloc(ExecutionState &state,
         }
         
         if (hugeSize.second) {
-          std::ostringstream info;
+
+          std::string Str;
+          llvm::raw_string_ostream info(Str);
           ExprPPrinter::printOne(info, "  size expr", size);
           info << "  concretization : " << example << "\n";
           info << "  unbound example: " << tmp << "\n";
@@ -3433,48 +3440,41 @@ unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) {
   return state.symPathOS.getID();
 }
 
-void Executor::getConstraintLog(const ExecutionState &state,
-                                std::string &res,
+void Executor::getConstraintLog(const ExecutionState &state, std::string &res,
                                 Interpreter::LogType logFormat) {
 
   std::ostringstream info;
 
-  switch(logFormat)
-  {
-  case STP:
-  {
-	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-	  char *log = solver->getConstraintLog(query);
-	  res = std::string(log);
-	  free(log);
-  }
-	  break;
-
-  case KQUERY:
-  {
-	  std::ostringstream info;
-	  ExprPPrinter::printConstraints(info, state.constraints);
-	  res = info.str();
-  }
-	  break;
-
-  case SMTLIB2:
-  {
-	  std::ostringstream info;
-	  ExprSMTLIBPrinter* printer = createSMTLIBPrinter();
-	  printer->setOutput(info);
-	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-	  printer->setQuery(query);
-	  printer->generateOutput();
-	  res = info.str();
-	  delete printer;
-  }
-	  break;
+  switch (logFormat) {
+  case STP: {
+    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+    char *log = solver->getConstraintLog(query);
+    res = std::string(log);
+    free(log);
+  } break;
+
+  case KQUERY: {
+    std::string Str;
+    llvm::raw_string_ostream info(Str);
+    ExprPPrinter::printConstraints(info, state.constraints);
+    res = info.str();
+  } break;
+
+  case SMTLIB2: {
+    std::string Str;
+    llvm::raw_string_ostream info(Str);
+    ExprSMTLIBPrinter *printer = createSMTLIBPrinter();
+    printer->setOutput(info);
+    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+    printer->setQuery(query);
+    printer->generateOutput();
+    res = info.str();
+    delete printer;
+  } break;
 
   default:
-	  klee_warning("Executor::getConstraintLog() : Log format not supported!");
+    klee_warning("Executor::getConstraintLog() : Log format not supported!");
   }
-
 }
 
 bool Executor::getSymbolicSolution(const ExecutionState &state,
@@ -3509,8 +3509,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   solver->setTimeout(0);
   if (!success) {
     klee_warning("unable to compute initial values (invalid constraints?)!");
-    ExprPPrinter::printQuery(std::cerr,
-                             state.constraints, 
+    ExprPPrinter::printQuery(llvm::errs(), state.constraints,
                              ConstantExpr::alloc(0, Expr::Bool));
     return false;
   }