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, 36 insertions, 1 deletions

diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index c27e265e..f8c6cabc 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -498,9 +498,14 @@ void ExprPPrinter::printConstraints(std::ostream &os,
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
+
 void ExprPPrinter::printQuery(std::ostream &os,
                               const ConstraintManager &constraints,
-                              const ref<Expr> &q) {
+                              const ref<Expr> &q,
+                              const ref<Expr> *evalExprsBegin,
+                              const ref<Expr> *evalExprsEnd,
+                              const Array * const *evalArraysBegin,
+                              const Array * const *evalArraysEnd) {
   PPrinter p(os);
   
   for (ConstraintManager::const_iterator it = constraints.begin(),
@@ -508,6 +513,9 @@ void ExprPPrinter::printQuery(std::ostream &os,
     p.scan(*it);
   p.scan(q);
 
+  for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it)
+    p.scan(*it);
+
   PrintContext PC(os);
   PC << "(query [";
   
@@ -525,6 +533,33 @@ void ExprPPrinter::printQuery(std::ostream &os,
   p.printSeparator(PC, constraints.empty(), indent-1);
   p.print(q, PC);
 
+  // Print expressions to obtain values for, if any.
+  if (evalExprsBegin != evalExprsEnd) {
+    PC.breakLine(indent - 1);
+    PC << '[';
+    for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it) {
+      p.print(*it, PC);
+      if (it + 1 != evalExprsEnd)
+        PC.breakLine(indent);
+    }
+    PC << ']';
+  }
+
+  // Print arrays to obtain values for, if any.
+  if (evalArraysBegin != evalArraysEnd) {
+    if (evalExprsBegin == evalExprsEnd)
+      PC << " []";
+
+    PC.breakLine(indent - 1);
+    PC << '[';
+    for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it) {
+      PC << "arr" << (*it)->id;
+      if (it + 1 != evalArraysEnd)
+        PC.breakLine(indent);
+    }
+    PC << ']';
+  }
+
   PC << ')';
   PC.breakLine();
 }