Modified -debug-print-instructions to allow to write directly on log file.

The option now contains 4 different options:
1) all:stderr,     which logs all instructions to file in format [src, inst_id, llvm_inst];
2) src:stderr,     which logs all instructions to file in format [src, inst_id];
3) compact:stderr, which logs all instructions to file in format [inst_id];
4) all:file,     which logs all instructions to file in format [src, inst_id, llvm_inst];
5) src:file,     which logs all instructions to file in format [src, inst_id];
6) compact:file, which logs all instructions to file in format [inst_id];
Writing to file gives a speedup of ~50x.

3 files changed, 158 insertions, 35 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 3b2a860e..ff346487 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -126,9 +126,38 @@ namespace {
                         cl::init(false),
 			cl::desc("Allow calls with symbolic arguments to external functions.  This concretizes the symbolic arguments.  (default=off)"));
 
-  cl::opt<bool>
-  DebugPrintInstructions("debug-print-instructions", 
-                         cl::desc("Print instructions during execution."));
+  /// The different query logging solvers that can switched on/off
+  enum PrintDebugInstructionsType {
+    STDERR_ALL, ///
+    STDERR_SRC,
+    STDERR_COMPACT,
+    FILE_ALL,    ///
+    FILE_SRC,    ///
+    FILE_COMPACT ///
+  };
+
+  llvm::cl::list<PrintDebugInstructionsType> DebugPrintInstructions(
+      "debug-print-instructions",
+      llvm::cl::desc("Log instructions during execution."),
+      llvm::cl::values(
+          clEnumValN(STDERR_ALL, "all:stderr", "Log all instructions to stderr "
+                                               "in format [src, inst_id, "
+                                               "llvm_inst]"),
+          clEnumValN(STDERR_SRC, "src:stderr",
+                     "Log all instructions to stderr in format [src, inst_id]"),
+          clEnumValN(STDERR_COMPACT, "compact:stderr",
+                     "Log all instructions to stderr in format [inst_id]"),
+          clEnumValN(FILE_ALL, "all:file", "Log all instructions to file "
+                                           "instructions.txt in format [src, "
+                                           "inst_id, llvm_inst]"),
+          clEnumValN(FILE_SRC, "src:file", "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]"),
+          clEnumValEnd),
+      llvm::cl::CommaSeparated);
 
   cl::opt<bool>
   DebugCheckForImpliedValues("debug-check-for-implied-values");
@@ -269,30 +298,18 @@ namespace klee {
   RNG theRNG;
 }
 
+Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih)
+    : Interpreter(opts), kmodule(0), interpreterHandler(ih), searcher(0),
+      externalDispatcher(new ExternalDispatcher()), statsTracker(0),
+      pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
+      processTree(0), replayKTest(0), replayPath(0), usingSeeds(0),
+      atMemoryLimit(false), inhibitForking(false), haltExecution(false),
+      ivcEnabled(false),
+      coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
+                            ? std::min(MaxCoreSolverTime, MaxInstructionTime)
+                            : std::max(MaxCoreSolverTime, MaxInstructionTime)),
+      debugInstFile(0), debugLogBuffer(debugBufferString) {
 
-Executor::Executor(const InterpreterOptions &opts,
-                   InterpreterHandler *ih) 
-  : Interpreter(opts),
-    kmodule(0),
-    interpreterHandler(ih),
-    searcher(0),
-    externalDispatcher(new ExternalDispatcher()),
-    statsTracker(0),
-    pathWriter(0),
-    symPathWriter(0),
-    specialFunctionHandler(0),
-    processTree(0),
-    replayKTest(0),
-    replayPath(0),    
-    usingSeeds(0),
-    atMemoryLimit(false),
-    inhibitForking(false),
-    haltExecution(false),
-    ivcEnabled(false),
-    coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
-      ? std::min(MaxCoreSolverTime,MaxInstructionTime)
-      : std::max(MaxCoreSolverTime,MaxInstructionTime)) {
-      
   if (coreSolverTimeout) UseForkedCoreSolver = true;
   Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
   if (!coreSolver) {
@@ -308,6 +325,21 @@ Executor::Executor(const InterpreterOptions &opts,
 
   this->solver = new TimingSolver(solver, EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
+
+  if (optionIsSet(DebugPrintInstructions, FILE_ALL) ||
+      optionIsSet(DebugPrintInstructions, FILE_COMPACT) ||
+      optionIsSet(DebugPrintInstructions, FILE_SRC)) {
+    std::string debug_file_name =
+        interpreterHandler->getOutputFilename("instructions.txt");
+    std::string ErrorInfo;
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
+    debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo,
+                                             llvm::sys::fs::OpenFlags::F_Text),
+#else
+    debugInstFile =
+        new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo);
+#endif
+  }
 }
 
 
@@ -357,6 +389,9 @@ Executor::~Executor() {
     delete timers.back();
     timers.pop_back();
   }
+  if (debugInstFile) {
+    delete debugInstFile;
+  }
 }
 
 /***/
@@ -1115,13 +1150,41 @@ void Executor::executeGetValue(ExecutionState &state,
   }
 }
 
-void Executor::stepInstruction(ExecutionState &state) {
-  if (DebugPrintInstructions) {
-    printFileLine(state, state.pc);
-    llvm::errs().indent(10) << stats::instructions << " ";
-    llvm::errs() << *(state.pc->inst) << '\n';
+void Executor::printDebugInstructions(ExecutionState &state) {
+  // check do not print
+  if (DebugPrintInstructions.size() == 0)
+	  return;
+
+  llvm::raw_ostream *stream = 0;
+  if (optionIsSet(DebugPrintInstructions, STDERR_ALL) ||
+      optionIsSet(DebugPrintInstructions, STDERR_SRC) ||
+      optionIsSet(DebugPrintInstructions, STDERR_COMPACT))
+    stream = &llvm::errs();
+  else
+    stream = &debugLogBuffer;
+
+  if (!optionIsSet(DebugPrintInstructions, STDERR_COMPACT) &&
+      !optionIsSet(DebugPrintInstructions, FILE_COMPACT))
+    printFileLine(state, state.pc, *stream);
+
+  (*stream) << state.pc->info->id;
+
+  if (optionIsSet(DebugPrintInstructions, STDERR_ALL) ||
+      optionIsSet(DebugPrintInstructions, FILE_ALL))
+    (*stream) << ":" << *(state.pc->inst);
+  (*stream) << "\n";
+
+  if (optionIsSet(DebugPrintInstructions, FILE_ALL) ||
+      optionIsSet(DebugPrintInstructions, FILE_COMPACT) ||
+      optionIsSet(DebugPrintInstructions, FILE_SRC)) {
+    debugLogBuffer.flush();
+    (*debugInstFile) << debugLogBuffer.str();
+    debugBufferString = "";
   }
+}
 
+void Executor::stepInstruction(ExecutionState &state) {
+  printDebugInstructions(state);
   if (statsTracker)
     statsTracker->stepInstruction(state);
 
@@ -1317,12 +1380,13 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
   }
 }
 
-void Executor::printFileLine(ExecutionState &state, KInstruction *ki) {
+void Executor::printFileLine(ExecutionState &state, KInstruction *ki,
+                             llvm::raw_ostream &debugFile) {
   const InstructionInfo &ii = *ki->info;
   if (ii.file != "")
-    llvm::errs() << "     " << ii.file << ":" << ii.line << ":";
+    debugFile << "     " << ii.file << ":" << ii.line << ":";
   else
-    llvm::errs() << "     [no debug info]:";
+    debugFile << "     [no debug info]:";
 }
 
 /// Compute the true target of a function call, resolving LLVM and KLEE aliases
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 1997bad2..600c7b90 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -21,6 +21,7 @@
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Module/KModule.h"
 #include "klee/util/ArrayCache.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include "llvm/ADT/Twine.h"
 
@@ -183,12 +184,22 @@ private:
   /// Assumes ownership of the created array objects
   ArrayCache arrayCache;
 
+  /// File to print executed instructions to
+  llvm::raw_ostream *debugInstFile;
+
+  // @brief Buffer used by logBuffer
+  std::string debugBufferString;
+
+  // @brief buffer to store logs before flushing to file
+  llvm::raw_string_ostream debugLogBuffer;
+
   llvm::Function* getTargetFunction(llvm::Value *calledVal,
                                     ExecutionState &state);
   
   void executeInstruction(ExecutionState &state, KInstruction *ki);
 
-  void printFileLine(ExecutionState &state, KInstruction *ki);
+  void printFileLine(ExecutionState &state, KInstruction *ki,
+                     llvm::raw_ostream &file);
 
   void run(ExecutionState &initialState);
 
@@ -400,6 +411,7 @@ private:
   void processTimers(ExecutionState *current,
                      double maxInstTime);
   void checkMemoryUsage();
+  void printDebugInstructions(ExecutionState &state);
 
 public:
   Executor(const InterpreterOptions &opts, InterpreterHandler *ie);
diff --git a/test/Feature/LoggingInstructions.c b/test/Feature/LoggingInstructions.c
new file mode 100644
index 00000000..049aa9da
--- /dev/null
+++ b/test/Feature/LoggingInstructions.c
@@ -0,0 +1,47 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t2.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=all:stderr %t2.bc 2>%t3.txt
+// RUN: FileCheck -input-file=%t3.txt -check-prefix=CHECK-FILE-SRC %s
+// RUN: FileCheck -input-file=%t3.txt -check-prefix=CHECK-FILE-DBG %s
+// RUN: not test -f %t.klee-out/instructions.txt
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=all:file %t2.bc
+// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-DBG %s
+// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-SRC %s
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=src:file %t2.bc
+// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-SRC %s
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --debug-print-instructions=compact:file %t2.bc
+// RUN: FileCheck -input-file=%t.klee-out/instructions.txt -check-prefix=CHECK-FILE-COMPACT %s
+//
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdio.h>
+
+char array[5] = { 1, 2, 3, -4, 5 };
+
+int main() {
+  unsigned k;
+
+  klee_make_symbolic(&k, sizeof(k), "k");
+  klee_assume(k < 5);
+
+  if (array[k] == -4)
+    printf("Yes\n");
+
+  // CHECK-FILE-SRC: LoggingInstructions.c:27
+  // CHECK-FILE-SRC: LoggingInstructions.c:28
+  // CHECK-FILE-SRC: LoggingInstructions.c:30
+  // CHECK-FILE-SRC: LoggingInstructions.c:31
+
+  // CHECK-FILE-DBG: call void @klee_make_symbolic
+  // CHECK-FILE-DBG: load
+
+  // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:21
+  // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:22
+  // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:24
+  // CHECK-FILE-COMPACT-NOT: LoggingInstructions.c:25
+
+  return 0;
+}