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

2 files changed, 28 insertions, 16 deletions

diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index 08ec66aa..5caf0027 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -70,8 +70,8 @@ namespace expr {
   /// ArrayDecl - Array declarations.
   ///
   /// For example:
-  ///   array obj : 32 -> 8 = symbolic
-  ///   array obj[32] : 32 -> 8 = { ... }
+  ///   array obj[] : w32 -> w8 = symbolic
+  ///   array obj[32] : w32 -> w8 = { ... }
   class ArrayDecl : public Decl {
   public:
     /// Name - The name of this array.
@@ -86,20 +86,25 @@ namespace expr {
 
     /// Range - The width of array contents.
     const unsigned Range;
-    
+
+    /// Root - The root array object defined by this decl.
+    const Array *Root;
+
     /// Contents - The initial contents of the array. The array is
     /// symbolic if no contents are specified. The contained
     /// expressions are guaranteed to be constants.
     const std::vector<ExprHandle> Contents;
 
   public:
-    template<typename InputIterator>
     ArrayDecl(const Identifier *_Name, unsigned _Size, 
               unsigned _Domain, unsigned _Range,
-              InputIterator ContentsBegin=InputIterator(), 
-              InputIterator ContentsEnd=InputIterator()) 
-      : Name(_Name), Size(_Size), Domain(_Domain), Range(_Range),
-        Contents(ContentsBegin, ContentsEnd) {}
+              const Array *_Root)
+      : Decl(ArrayDeclKind), Name(_Name), 
+        Size(_Size), Domain(_Domain), Range(_Range), 
+        Root(_Root) {
+    }
+
+    virtual void dump();
 
     static bool classof(const Decl *D) {
       return D->getKind() == Decl::ArrayDeclKind;
@@ -182,16 +187,19 @@ namespace expr {
 
     /// Objects - Symbolic arrays whose initial contents should be
     /// given if the query is invalid.
-    const std::vector<ArrayDecl> Objects;
+    const std::vector<const Array*> Objects;
 
   public:
-    template<typename InputIterator>
-    QueryCommand(InputIterator ConstraintsBegin, 
-                 InputIterator ConstraintsEnd,
-                 ExprHandle _Query)
+    QueryCommand(const std::vector<ExprHandle> &_Constraints,
+                 ExprHandle _Query,
+                 const std::vector<ExprHandle> &_Values,
+                 const std::vector<const Array*> &_Objects
+                 )
       : CommandDecl(QueryCommandDeclKind),
-        Constraints(ConstraintsBegin, ConstraintsEnd),
-        Query(_Query) {}
+        Constraints(_Constraints),
+        Query(_Query),
+        Values(_Values),
+        Objects(_Objects) {}
 
     virtual void dump();
 
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
index 63e6611d..50ccd203 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/util/ExprPPrinter.h
@@ -61,7 +61,11 @@ namespace klee {
 
     static void printQuery(std::ostream &os,
                            const ConstraintManager &constraints,
-                           const ref<Expr> &q);
+                           const ref<Expr> &q,
+                           const ref<Expr> *evalExprsBegin = 0,
+                           const ref<Expr> *evalExprsEnd = 0,
+                           const Array * const* evalArraysBegin = 0,
+                           const Array * const* evalArraysEnd = 0);
   };
 
 }