From 1c21929692bf5b6c063c3faaba9da90d04b2e332 Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Fri, 5 Jun 2009 10:09:13 +0000
Subject: 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
---
 lib/Solver/PCLoggingSolver.cpp | 28 +++++++++++++++++++++++-----
 1 file changed, 23 insertions(+), 5 deletions(-)

(limited to 'lib/Solver')

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);
-- 
cgit 1.4.1