1 files changed, 134 insertions, 0 deletions
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
new file mode 100644
index 00000000..4b787acb
--- /dev/null
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -0,0 +1,134 @@
+//===-- PCLoggingSolver.cpp -----------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Solver.h"
+
+// FIXME: This should not be here.
+#include "klee/ExecutionState.h"
+#include "klee/Expr.h"
+#include "klee/SolverImpl.h"
+#include "klee/Statistics.h"
+#include "klee/util/ExprPPrinter.h"
+#include "klee/Internal/Support/QueryLog.h"
+#include "klee/Internal/System/Time.h"
+
+#include "llvm/Support/CommandLine.h"
+
+#include <fstream>
+
+using namespace klee;
+using namespace llvm;
+using namespace klee::util;
+
+///
+
+class PCLoggingSolver : public SolverImpl {
+  Solver *solver;
+  std::ofstream os;
+  ExprPPrinter *printer;
+  unsigned queryCount;
+  double startTime;
+
+  void startQuery(const Query& query, const char *typeName) {
+    Statistic *S = theStatisticManager->getStatisticByName("Instructions");
+    uint64_t instructions = S ? S->getValue() : 0;
+    os << "# Query " << queryCount++ << " -- "
+       << "Type: " << typeName << ", "
+       << "Instructions: " << instructions << "\n";
+    printer->printQuery(os, query.constraints, query.expr);
+    
+    startTime = getWallTime();
+  }
+
+  void finishQuery(bool success) {
+    double delta = getWallTime() - startTime;
+    os << "#   " << (success ? "OK" : "FAIL") << " -- "
+       << "Elapsed: " << delta << "\n";
+  }
+  
+public:
+  PCLoggingSolver(Solver *_solver, std::string path) 
+  : solver(_solver),
+    os(path.c_str(), std::ios::trunc),
+    printer(ExprPPrinter::create(os)),
+    queryCount(0) {
+  }                                                      
+  ~PCLoggingSolver() {
+    delete printer;
+    delete solver;
+  }
+  
+  bool computeTruth(const Query& query, bool &isValid) {
+    startQuery(query, "Truth");
+    bool success = solver->impl->computeTruth(query, isValid);
+    finishQuery(success);
+    if (success)
+      os << "#   Is Valid: " << (isValid ? "true" : "false") << "\n";
+    os << "\n";
+    return success;
+  }
+
+  bool computeValidity(const Query& query, Solver::Validity &result) {
+    startQuery(query, "Validity");
+    bool success = solver->impl->computeValidity(query, result);
+    finishQuery(success);
+    if (success)
+      os << "#   Validity: " << result << "\n";
+    os << "\n";
+    return success;
+  }
+
+  bool computeValue(const Query& query, ref<Expr> &result) {
+    startQuery(query, "Value");
+    bool success = solver->impl->computeValue(query, result);
+    finishQuery(success);
+    if (success)
+      os << "#   Result: " << result << "\n";
+    os << "\n";
+    return success;
+  }
+
+  bool computeInitialValues(const Query& query,
+                            const std::vector<const Array*> &objects,
+                            std::vector< std::vector<unsigned char> > &values,
+                            bool &hasSolution) {
+    // FIXME: Add objects to output.
+    startQuery(query, "InitialValues");
+    bool success = solver->impl->computeInitialValues(query, objects, 
+                                                      values, hasSolution);
+    finishQuery(success);
+    if (success) {
+      os << "#   Solvable: " << (hasSolution ? "true" : "false") << "\n";
+      if (hasSolution) {
+        std::vector< std::vector<unsigned char> >::iterator
+          values_it = values.begin();
+        for (std::vector<const Array*>::const_iterator i = objects.begin(),
+               e = objects.end(); i != e; ++i, ++values_it) {
+          const Array *array = *i;
+          std::vector<unsigned char> &data = *values_it;
+          os << "#     arr" << array->id << " = [";
+          for (unsigned j = 0; j < array->size; j++) {
+            os << (int) data[j];
+            if (j+1 < array->size)
+              os << ",";
+          }
+          os << "]\n";
+        }
+      }
+    }
+    os << "\n";
+    return success;
+  }
+};
+
+///
+
+Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path) {
+  return new Solver(new PCLoggingSolver(_solver, path));
+}