[Solver]Add support to dump STP qeries using

Use "-debug-dump-stp-queries" argument for KLEE/Kleaver
to print out each STP query sent to the STP Solver.

Queries have the format which `stp` frontend can understand.

1 files changed, 7 insertions, 2 deletions

diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 07331fa4..341ca17c 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -21,6 +21,7 @@
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprUtil.h"
 #include "klee/Internal/Support/Timer.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/CommandLine.h"
 
 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
@@ -45,6 +46,10 @@ IgnoreSolverFailures("ignore-solver-failures",
                      llvm::cl::init(false),
                      llvm::cl::desc("Ignore any solver failures (default=off)"));
 
+llvm::cl::opt<bool>
+DebugDumpSTPQueries("debug-dump-stp-queries",
+                     llvm::cl::init(false),
+                     llvm::cl::desc("Dump every STP query to stderr (default=off)"));
 
 using namespace klee;
 
@@ -812,11 +817,11 @@ STPSolverImpl::computeInitialValues(const Query &query,
 
   ExprHandle stp_e = builder->construct(query.expr);
      
-  if (0) {
+  if (DebugDumpSTPQueries) {
     char *buf;
     unsigned long len;
     vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
-    fprintf(stderr, "note: STP query: %.*s\n", (unsigned) len, buf);
+    klee_warning("STP query:\n%.*s\n", (unsigned) len, buf);
   }
 
   bool success;