Support the extended query command syntax.

 - There are two optional lists following the constraints and the
   query expression. The first is a list of expressions to give values
   for and the second is a list of arrays to provide values for.

 - Update ExprPPrinter to accept extra arguments to print these
   arguments.

 - Add Parser support.

 - Add more ArrayDecl support.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72938 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 23 insertions, 5 deletions

diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
index 4b787acb..81cf7688 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -35,13 +35,19 @@ class PCLoggingSolver : public SolverImpl {
   unsigned queryCount;
   double startTime;
 
-  void startQuery(const Query& query, const char *typeName) {
+  void startQuery(const Query& query, const char *typeName,
+                  const ref<Expr> *evalExprsBegin = 0,
+                  const ref<Expr> *evalExprsEnd = 0,
+                  const Array * const* evalArraysBegin = 0,
+                  const Array * const* evalArraysEnd = 0) {
     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);
+    printer->printQuery(os, query.constraints, query.expr,
+                        evalExprsBegin, evalExprsEnd,
+                        evalArraysBegin, evalArraysEnd);
     
     startTime = getWallTime();
   }
@@ -85,7 +91,8 @@ public:
   }
 
   bool computeValue(const Query& query, ref<Expr> &result) {
-    startQuery(query, "Value");
+    startQuery(query.withFalse(), "Value", 
+               &query.expr, &query.expr + 1);
     bool success = solver->impl->computeValue(query, result);
     finishQuery(success);
     if (success)
@@ -98,8 +105,19 @@ public:
                             const std::vector<const Array*> &objects,
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution) {
-    // FIXME: Add objects to output.
-    startQuery(query, "InitialValues");
+    const ref<Expr> *evalExprBegin = 0, *evalExprEnd = 0;
+    if (!query.expr->isFalse()) {
+      evalExprBegin = &query.expr;
+      evalExprEnd = evalExprBegin + 1;
+    } 
+    if (objects.empty()) {
+      startQuery(query.withFalse(), "InitialValues",
+                 evalExprBegin, evalExprEnd);
+    } else {
+      startQuery(query.withFalse(), "InitialValues",
+                 evalExprBegin, evalExprEnd,
+                 &objects[0], &objects[0] + objects.size());
+    }
     bool success = solver->impl->computeInitialValues(query, objects, 
                                                       values, hasSolution);
     finishQuery(success);