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

7 files changed, 337 insertions, 290 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);
   };
 
 }
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();
 }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index c20c5d66..9b3a2687 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -396,13 +396,17 @@ DeclResult ParserImpl::ParseCommandDecl() {
 /// ParseQueryCommand - Parse query command. The lexer should be
 /// positioned at the 'query' keyword.
 /// 
-/// 'query' expressions-list expression [expression-list [array-list]]
+/// 'query' expressions-list expression [expressions-list [array-list]]
 DeclResult ParserImpl::ParseQueryCommand() {
+  std::vector<ExprHandle> Constraints;
+  std::vector<ExprHandle> Values;
+  std::vector<const Array*> Objects;
+  ExprResult Res;
+
   // FIXME: We need a command for this. Or something.
   ExprSymTab.clear();
   VersionSymTab.clear();
 
-  std::vector<ExprHandle> Constraints;
   ConsumeExpectedToken(Token::KWQuery);
   if (Tok.kind != Token::LSquare) {
     Error("malformed query, expected constraint list.");
@@ -415,24 +419,77 @@ DeclResult ParserImpl::ParseQueryCommand() {
   while (Tok.kind != Token::RSquare) {
     if (Tok.kind == Token::EndOfFile) {
       Error("unexpected end of file.");
-      return new QueryCommand(Constraints.begin(), Constraints.end(),
-                              ConstantExpr::alloc(false, Expr::Bool));
+      Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool));
+      goto exit;
     }
 
-    ExprResult Res = ParseExpr(TypeResult(Expr::Bool));
-    if (Res.isValid())
-      Constraints.push_back(Res.get());
+    ExprResult Constraint = ParseExpr(TypeResult(Expr::Bool));
+    if (Constraint.isValid())
+      Constraints.push_back(Constraint.get());
   }
-
   ConsumeRSquare();
 
-  ExprResult Res = ParseExpr(TypeResult());
+  Res = ParseExpr(TypeResult(Expr::Bool));
   if (!Res.isValid()) // Error emitted by ParseExpr.
     Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool));
 
-  ExpectRParen("unexpected argument to 'query'.");  
-  return new QueryCommand(Constraints.begin(), Constraints.end(),
-                          Res.get());
+  // Return if there are no optional lists of things to evaluate.
+  if (Tok.kind == Token::RParen)
+    goto exit;
+  
+  ConsumeExpectedToken(Token::LSquare);
+  // FIXME: Should avoid reading past unbalanced parens here.
+  while (Tok.kind != Token::RSquare) {
+    if (Tok.kind == Token::EndOfFile) {
+      Error("unexpected end of file.");
+      goto exit;
+    }
+
+    ExprResult Res = ParseExpr(TypeResult());
+    if (Res.isValid())
+      Values.push_back(Res.get());
+  }
+  ConsumeRSquare();
+
+  // Return if there are no optional lists of things to evaluate.
+  if (Tok.kind == Token::RParen)
+    goto exit;
+
+  ConsumeExpectedToken(Token::LSquare);
+  // FIXME: Should avoid reading past unbalanced parens here.
+  while (Tok.kind != Token::RSquare) {
+    if (Tok.kind == Token::EndOfFile) {
+      Error("unexpected end of file.");
+      goto exit;
+    }
+
+    // FIXME: Factor out.
+    if (Tok.kind != Token::Identifier) {
+      Error("unexpected token.");
+      ConsumeToken();
+      continue;
+    }
+
+    Token LTok = Tok;
+    const Identifier *Label = GetOrCreateIdentifier(Tok);
+    ConsumeToken();
+
+    // Declare or create array.
+    const ArrayDecl *AD = ArraySymTab[Label];
+    if (!AD) {
+      // FIXME: Don't make up arrays.
+      unsigned Id = atoi(&Label->Name.c_str()[3]);
+      AD = new ArrayDecl(Label, 0, 32, 8, new Array(0, Id, 0));
+    }
+    
+    Objects.push_back(AD->Root);
+  }
+  ConsumeRSquare();
+
+ exit:
+  if (Tok.kind != Token::EndOfFile)
+    ExpectRParen("unexpected argument to 'query'.");  
+  return new QueryCommand(Constraints, Res.get(), Values, Objects);
 }
 
 /// ParseNumberOrExpr - Parse an expression whose type cannot be
@@ -1035,12 +1092,13 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
       // Declare or create array.
       const ArrayDecl *&A = ArraySymTab[Label];
       if (!A) {
-        //        Array = new ArrayDecl(Label, 0, 32, 8);
         unsigned id = atoi(&Label->Name.c_str()[3]);
         Array *root = new Array(0, id, 0);
+        ArrayDecl *AD = new ArrayDecl(Label, 0, 32, 8, root);
         // Create update list mapping of name -> array.
         VersionSymTab.insert(std::make_pair(Label,
                                             UpdateList(root, true, NULL)));
+        ArraySymTab.insert(std::make_pair(Label, AD));
       }
     }
 
@@ -1312,12 +1370,39 @@ void ParserImpl::Error(const char *Message, const Token &At) {
 
 Decl::Decl(DeclKind _Kind) : Kind(_Kind) {}
 
+void ArrayDecl::dump() {
+  std::cout << "array " << Name->Name << " : "
+            << 'w' << Domain << " -> "
+            << 'w' << Range << " = ";
+
+  if (Contents.empty()) {
+    std::cout << "symbolic\n";
+  } else {
+    std::cout << '{';
+    for (std::vector<ExprHandle>::const_iterator it = Contents.begin(),
+           ie = Contents.end(); it != ie;) {
+      std::cout << *it;
+      if (++it != ie)
+        std::cout << " ";
+    }
+    std::cout << "}\n";
+  }
+}
+
 void QueryCommand::dump() {
-  // FIXME: This is masking the difference between an actual query and
-  // a query decl.
-  ExprPPrinter::printQuery(std::cout, 
-                           ConstraintManager(Constraints), 
-                           Query);
+  const ExprHandle *ValuesBegin = 0, *ValuesEnd = 0;
+  const Array * const* ObjectsBegin = 0, * const* ObjectsEnd = 0;
+  if (!Values.empty()) {
+    ValuesBegin = &Values[0];
+    ValuesEnd = ValuesBegin + Values.size();
+  }
+  if (!Objects.empty()) {
+    ObjectsBegin = &Objects[0];
+    ObjectsEnd = ObjectsBegin + Objects.size();
+  }
+  ExprPPrinter::printQuery(std::cout, ConstraintManager(Constraints), 
+                           Query, ValuesBegin, ValuesEnd,
+                           ObjectsBegin, ObjectsEnd);
 }
 
 // Public parser API
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);
diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.pc
index 3d37bf9b..9357e0c1 100644
--- a/test/Expr/Parser/Exprs.pc
+++ b/test/Expr/Parser/Exprs.pc
@@ -1,390 +1,288 @@
+# Taken from Features/ExprLogging.c
+
 # FIXME: Make this test actual check for something (other than
 #  crashing/errors).
 
 # RUN: %kleaver -print-ast %s
 
-# Query 0 -- Type: Truth, Instructions: 33
-(query [] (Not (Ult (Concat w32 (Read w8 3 arr65)
-                                (Concat w24 (Read w8 2 arr65)
-                                            (ReadLSB w16 0 arr65)))
+# Query 0 -- Type: Truth, Instructions: 36
+(query [] (Not (Ult (ReadLSB w32 0 arr119)
                     16)))
-#   OK -- Elapsed: 0.000977993
+#   OK -- Elapsed: 0.000962901
 #   Is Valid: false
 
-# Query 1 -- Type: Value, Instructions: 41
-(query [(Ult N0:(Concat w32 (Read w8 3 arr65)
-                            (Concat w24 (Read w8 2 arr65)
-                                        (ReadLSB w16 0 arr65)))
+# Query 1 -- Type: Value, Instructions: 45
+(query [(Ult N0:(ReadLSB w32 0 arr119)
              16)]
-       (Add w32 174331008 (Mul w32 4 N0)))
-#   OK -- Elapsed: 3.38554e-05
-#   Result: 174331008
+       false
+       [(Add w32 168649296 (Mul w32 4 N0))])
+#   OK -- Elapsed: 4.09303e-05
+#   Result: 168649296
 
-# Query 2 -- Type: Truth, Instructions: 41
-(query [(Ult N0:(Concat w32 (Read w8 3 arr65)
-                            (Concat w24 (Read w8 2 arr65)
-                                        (ReadLSB w16 0 arr65)))
+# Query 2 -- Type: Truth, Instructions: 45
+(query [(Ult N0:(ReadLSB w32 0 arr119)
              16)]
        (Ult (Mul w32 4 N0) 61))
-#   OK -- Elapsed: 0.00113606
+#   OK -- Elapsed: 0.00111999
 #   Is Valid: true
 
-# Query 3 -- Type: Truth, Instructions: 57
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 3 -- Type: Truth, Instructions: 66
+(query [(Ult (ReadLSB w32 0 arr119)
              16)]
-       (Not (Ult (Concat w32 (Read w8 3 arr72)
-                             (Concat w24 (Read w8 2 arr72)
-                                         (ReadLSB w16 0 arr72)))
+       (Not (Ult (ReadLSB w32 0 arr126)
                  16)))
-#   OK -- Elapsed: 0.000864983
+#   OK -- Elapsed: 0.000853909
 #   Is Valid: false
 
-# Query 4 -- Type: Value, Instructions: 62
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 4 -- Type: Value, Instructions: 72
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult N0:(Concat w32 (Read w8 3 arr72)
-                            (Concat w24 (Read w8 2 arr72)
-                                        (ReadLSB w16 0 arr72)))
+        (Ult N0:(ReadLSB w32 0 arr126)
              16)]
-       (Add w32 174331008 (Mul w32 4 N0)))
-#   OK -- Elapsed: 3.60012e-05
-#   Result: 174331008
+       false
+       [(Add w32 168649296 (Mul w32 4 N0))])
+#   OK -- Elapsed: 3.89818e-05
+#   Result: 168649296
 
-# Query 5 -- Type: Truth, Instructions: 62
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 5 -- Type: Truth, Instructions: 72
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult N0:(Concat w32 (Read w8 3 arr72)
-                            (Concat w24 (Read w8 2 arr72)
-                                        (ReadLSB w16 0 arr72)))
+        (Ult N0:(ReadLSB w32 0 arr126)
              16)]
        (Ult (Mul w32 4 N0) 61))
-#   OK -- Elapsed: 0.00109196
+#   OK -- Elapsed: 0.00109102
 #   Is Valid: true
 
-# Query 6 -- Type: Truth, Instructions: 79
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 6 -- Type: Truth, Instructions: 94
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)]
-       (Not (Ult (Concat w32 (Read w8 3 arr79)
-                             (Concat w24 (Read w8 2 arr79)
-                                         (ReadLSB w16 0 arr79)))
+       (Not (Ult (ReadLSB w32 0 arr133)
                  16)))
-#   OK -- Elapsed: 0.00089097
+#   OK -- Elapsed: 0.000877942
 #   Is Valid: false
 
-# Query 7 -- Type: Value, Instructions: 87
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 7 -- Type: Value, Instructions: 103
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult N0:(Concat w32 (Read w8 3 arr79)
-                            (Concat w24 (Read w8 2 arr79)
-                                        (ReadLSB w16 0 arr79)))
+        (Ult N0:(ReadLSB w32 0 arr133)
              16)]
-       (Add w32 174331008 (Mul w32 4 N0)))
-#   OK -- Elapsed: 4.41074e-05
-#   Result: 174331008
+       false
+       [(Add w32 168649296 (Mul w32 4 N0))])
+#   OK -- Elapsed: 4.81055e-05
+#   Result: 168649296
 
-# Query 8 -- Type: Truth, Instructions: 87
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 8 -- Type: Truth, Instructions: 103
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult N0:(Concat w32 (Read w8 3 arr79)
-                            (Concat w24 (Read w8 2 arr79)
-                                        (ReadLSB w16 0 arr79)))
+        (Ult N0:(ReadLSB w32 0 arr133)
              16)]
        (Ult (Mul w32 4 N0) 61))
-#   OK -- Elapsed: 0.00111794
+#   OK -- Elapsed: 0.00110997
 #   Is Valid: true
 
-# Query 9 -- Type: Truth, Instructions: 103
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 9 -- Type: Truth, Instructions: 124
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult (Concat w32 (Read w8 3 arr79)
-                         (Concat w24 (Read w8 2 arr79)
-                                     (ReadLSB w16 0 arr79)))
+        (Ult (ReadLSB w32 0 arr133)
              16)]
        (And (Not (Eq 3
-                     N0:(Concat w32 (Read w8 3 arr86)
-                                    (Concat w24 (Read w8 2 arr86)
-                                                (ReadLSB w16 0 arr86)))))
+                     N0:(ReadLSB w32 0 arr140)))
             (And (Not (Eq 2 N0))
                  (And (Not (Eq 1 N0))
                       (Not (Eq 0 N0))))))
-#   OK -- Elapsed: 0.00117898
+#   OK -- Elapsed: 0.00117305
 #   Is Valid: false
 
-# Query 10 -- Type: Value, Instructions: 108
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 10 -- Type: Value, Instructions: 130
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult (Concat w32 (Read w8 3 arr79)
-                         (Concat w24 (Read w8 2 arr79)
-                                     (ReadLSB w16 0 arr79)))
+        (Ult (ReadLSB w32 0 arr133)
              16)
         (Not (And (Not (Eq 3
-                           N0:(Concat w32 (Read w8 3 arr86)
-                                          (Concat w24 (Read w8 2 arr86)
-                                                      (ReadLSB w16 0 arr86)))))
+                           N0:(ReadLSB w32 0 arr140)))
                   (And (Not (Eq 2 N0))
                        (And (Not (Eq 1 N0))
                             (Not (Eq 0 N0))))))]
-       (Add w32 174291904 N0))
-#   OK -- Elapsed: 5.91278e-05
-#   Result: 174291907
+       false
+       [(Add w32 168742656 N0)])
+#   OK -- Elapsed: 6.11061e-05
+#   Result: 168742659
 
-# Query 11 -- Type: Truth, Instructions: 108
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 11 -- Type: Truth, Instructions: 130
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult (Concat w32 (Read w8 3 arr79)
-                         (Concat w24 (Read w8 2 arr79)
-                                     (ReadLSB w16 0 arr79)))
+        (Ult (ReadLSB w32 0 arr133)
              16)
         (Not (And (Not N0:(Eq 3
-                              N1:(Concat w32 (Read w8 3 arr86)
-                                             (Concat w24 (Read w8 2 arr86)
-                                                         (ReadLSB w16 0 arr86)))))
+                              N1:(ReadLSB w32 0 arr140)))
                   (And (Not N2:(Eq 2 N1))
                        (And (Not N3:(Eq 1 N1))
                             (Not N4:(Eq 0 N1))))))]
        (Or N0
            (Or N2 (Or N3 N4))))
-#   OK -- Elapsed: 0.00145888
+#   OK -- Elapsed: 0.00146289
 #   Is Valid: true
 
-# Query 12 -- Type: Truth, Instructions: 114
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 12 -- Type: Truth, Instructions: 136
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult (Concat w32 (Read w8 3 arr79)
-                         (Concat w24 (Read w8 2 arr79)
-                                     (ReadLSB w16 0 arr79)))
+        (Ult (ReadLSB w32 0 arr133)
              16)
         (Not (And (Not (Eq 3
-                           N0:(Concat w32 (Read w8 3 arr86)
-                                          (Concat w24 (Read w8 2 arr86)
-                                                      (ReadLSB w16 0 arr86)))))
+                           N0:(ReadLSB w32 0 arr140)))
                   (And (Not (Eq 2 N0))
                        (And (Not (Eq 1 N0))
                             (Not (Eq 0 N0))))))]
        (Not (Eq 104
                 (Read w8 0 [N0=0,
-                            1=97] @ arr60))))
-#   OK -- Elapsed: 0.00247502
+                            1=97] @ arr115))))
+#   OK -- Elapsed: 0.00246791
 #   Is Valid: false
 
-# Query 13 -- Type: Truth, Instructions: 124
-(query [(Ult (Concat w32 (Read w8 3 arr65)
-                         (Concat w24 (Read w8 2 arr65)
-                                     (ReadLSB w16 0 arr65)))
+# Query 13 -- Type: Truth, Instructions: 146
+(query [(Ult (ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult (Concat w32 (Read w8 3 arr79)
-                         (Concat w24 (Read w8 2 arr79)
-                                     (ReadLSB w16 0 arr79)))
+        (Ult (ReadLSB w32 0 arr133)
              16)
         (Not (And (Not (Eq 3
-                           N0:(Concat w32 (Read w8 3 arr86)
-                                          (Concat w24 (Read w8 2 arr86)
-                                                      (ReadLSB w16 0 arr86)))))
+                           N0:(ReadLSB w32 0 arr140)))
                   (And (Not (Eq 2 N0))
                        (And (Not (Eq 1 N0))
                             (Not (Eq 0 N0))))))
         (Eq 104
             (Read w8 0 U0:[N0=0,
-                           1=97] @ arr60))]
+                           1=97] @ arr115))]
        (Not (Slt 2
                  (Concat w32 (Read w8 3 U0)
                              (Concat w24 (Read w8 2 U0)
                                          (Concat w16 (Read w8 1 U0) (w8 104)))))))
-#   OK -- Elapsed: 0.000127077
+#   OK -- Elapsed: 0.000145945
 #   Is Valid: false
 
-# Query 14 -- Type: Truth, Instructions: 130
-(query [(Ult N0:(Concat w32 (Read w8 3 arr65)
-                            (Concat w24 (Read w8 2 arr65)
-                                        (ReadLSB w16 0 arr65)))
+# Query 14 -- Type: Truth, Instructions: 152
+(query [(Ult N0:(ReadLSB w32 0 arr119)
              16)
-        (Ult (Concat w32 (Read w8 3 arr72)
-                         (Concat w24 (Read w8 2 arr72)
-                                     (ReadLSB w16 0 arr72)))
+        (Ult (ReadLSB w32 0 arr126)
              16)
-        (Ult N1:(Concat w32 (Read w8 3 arr79)
-                            (Concat w24 (Read w8 2 arr79)
-                                        (ReadLSB w16 0 arr79)))
+        (Ult N1:(ReadLSB w32 0 arr133)
              16)
         (Not (And (Not (Eq 3
-                           N2:(Concat w32 (Read w8 3 arr86)
-                                          (Concat w24 (Read w8 2 arr86)
-                                                      (ReadLSB w16 0 arr86)))))
+                           N2:(ReadLSB w32 0 arr140)))
                   (And (Not (Eq 2 N2))
                        (And (Not (Eq 1 N2))
                             (Not (Eq 0 N2))))))
         (Eq 104
             (Read w8 0 U0:[N2=0,
-                           1=97] @ arr60))
+                           1=97] @ arr115))
         (Slt 2
              N3:(Concat w32 (Read w8 3 U0)
                             (Concat w24 (Read w8 2 U0)
                                         (Concat w16 (Read w8 1 U0) (w8 104)))))]
-       (Not (Eq (Concat w32 (Read w8 51 U1:[N4:(Mul w32 4 N1)=(Extract w8 0 N5:(SExt w32 (Read w8 3 arr60))),
-                                            (Add w32 1 N4)=(Extract w8 8 N5),
-                                            (Add w32 2 N4)=(Extract w8 16 N5),
-                                            (Add w32 3 N4)=(Extract w8 24 N5),
-                                            N6:(Mul w32 4 N0)=(Extract w8 0 N7:(SExt w32 (Read w8 0 arr60))),
-                                            (Add w32 1 N6)=(Extract w8 8 N7),
-                                            (Add w32 2 N6)=(Extract w8 16 N7),
-                                            (Add w32 3 N6)=(Extract w8 24 N7),
-                                            63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1])
-                            (Concat w24 (Read w8 50 U1)
-                                        (ReadLSB w16 48 U1)))
+       (Not (Eq (ReadLSB w32 48 U1:[N4:(Mul w32 4 N1)=(Extract w8 0 N5:(SExt w32 (Read w8 3 arr115))),
+                                    (Add w32 1 N4)=(Extract w8 8 N5),
+                                    (Add w32 2 N4)=(Extract w8 16 N5),
+                                    (Add w32 3 N4)=(Extract w8 24 N5),
+                                    N6:(Mul w32 4 N0)=(Extract w8 0 N7:(SExt w32 (Read w8 0 arr115))),
+                                    (Add w32 1 N6)=(Extract w8 8 N7),
+                                    (Add w32 2 N6)=(Extract w8 16 N7),
+                                    (Add w32 3 N6)=(Extract w8 24 N7),
+                                    63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1])
                 N3)))
-#   OK -- Elapsed: 0.0158381
+#   OK -- Elapsed: 0.016117
 #   Is Valid: false
 
-# Query 15 -- Type: Truth, Instructions: 135
-(query [(Ult N0:(Concat w32 (Read w8 3 arr65)
-                            (Concat w24 (Read w8 2 arr65)
-                                        (ReadLSB w16 0 arr65)))
+# Query 15 -- Type: Truth, Instructions: 157
+(query [(Ult N0:(ReadLSB w32 0 arr119)
              16)
-        (Ult N1:(Concat w32 (Read w8 3 arr72)
-                            (Concat w24 (Read w8 2 arr72)
-                                        (ReadLSB w16 0 arr72)))
+        (Ult N1:(ReadLSB w32 0 arr126)
              16)
-        (Ult N2:(Concat w32 (Read w8 3 arr79)
-                            (Concat w24 (Read w8 2 arr79)
-                                        (ReadLSB w16 0 arr79)))
+        (Ult N2:(ReadLSB w32 0 arr133)
              16)
         (Not (And (Not (Eq 3
-                           N3:(Concat w32 (Read w8 3 arr86)
-                                          (Concat w24 (Read w8 2 arr86)
-                                                      (ReadLSB w16 0 arr86)))))
+                           N3:(ReadLSB w32 0 arr140)))
                   (And (Not (Eq 2 N3))
                        (And (Not (Eq 1 N3))
                             (Not (Eq 0 N3))))))
         (Eq 104
             (Read w8 0 U0:[N3=0,
-                           1=97] @ arr60))
+                           1=97] @ arr115))
         (Slt 2
              N4:(Concat w32 (Read w8 3 U0)
                             (Concat w24 (Read w8 2 U0)
                                         (Concat w16 (Read w8 1 U0) (w8 104)))))
-        (Eq (Concat w32 (Read w8 51 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr60))),
-                                        (Add w32 1 N5)=(Extract w8 8 N6),
-                                        (Add w32 2 N5)=(Extract w8 16 N6),
-                                        (Add w32 3 N5)=(Extract w8 24 N6)] @
-                                    U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr60))),
-                                        (Add w32 1 N7)=(Extract w8 8 N8),
-                                        (Add w32 2 N7)=(Extract w8 16 N8),
-                                        (Add w32 3 N7)=(Extract w8 24 N8),
-                                        63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1])
-                        (Concat w24 (Read w8 50 U1)
-                                    (ReadLSB w16 48 U1)))
+        (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr115))),
+                                (Add w32 1 N5)=(Extract w8 8 N6),
+                                (Add w32 2 N5)=(Extract w8 16 N6),
+                                (Add w32 3 N5)=(Extract w8 24 N6)] @
+                            U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr115))),
+                                (Add w32 1 N7)=(Extract w8 8 N8),
+                                (Add w32 2 N7)=(Extract w8 16 N8),
+                                (Add w32 3 N7)=(Extract w8 24 N8),
+                                63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1])
             N4)]
        (Eq 32
-           (Concat w32 (Read w8 (Add w32 3 N9:(Mul w32 4 N1))
-                                U2)
-                       (Concat w24 (Read w8 (Add w32 2 N9)
-                                            U2)
-                                   (ReadLSB w16 N9 U2)))))
-#   OK -- Elapsed: 0.000321865
+           (ReadLSB w32 N9:(Mul w32 4 N1) U2)))
+#   OK -- Elapsed: 0.00037605
 #   Is Valid: false
 
-# Query 16 -- Type: InitialValues, Instructions: 137
-(query [(Ult N0:(Concat w32 (Read w8 3 arr65)
-                            (Concat w24 (Read w8 2 arr65)
-                                        (ReadLSB w16 0 arr65)))
+# Query 16 -- Type: InitialValues, Instructions: 159
+(query [(Ult N0:(ReadLSB w32 0 arr119)
              16)
-        (Ult N1:(Concat w32 (Read w8 3 arr72)
-                            (Concat w24 (Read w8 2 arr72)
-                                        (ReadLSB w16 0 arr72)))
+        (Ult N1:(ReadLSB w32 0 arr126)
              16)
-        (Ult N2:(Concat w32 (Read w8 3 arr79)
-                            (Concat w24 (Read w8 2 arr79)
-                                        (ReadLSB w16 0 arr79)))
+        (Ult N2:(ReadLSB w32 0 arr133)
              16)
         (Not (And (Not (Eq 3
-                           N3:(Concat w32 (Read w8 3 arr86)
-                                          (Concat w24 (Read w8 2 arr86)
-                                                      (ReadLSB w16 0 arr86)))))
+                           N3:(ReadLSB w32 0 arr140)))
                   (And (Not (Eq 2 N3))
                        (And (Not (Eq 1 N3))
                             (Not (Eq 0 N3))))))
         (Eq 104
             (Read w8 0 U0:[N3=0,
-                           1=97] @ arr60))
+                           1=97] @ arr115))
         (Slt 2
              N4:(Concat w32 (Read w8 3 U0)
                             (Concat w24 (Read w8 2 U0)
                                         (Concat w16 (Read w8 1 U0) (w8 104)))))
-        (Eq (Concat w32 (Read w8 51 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr60))),
-                                        (Add w32 1 N5)=(Extract w8 8 N6),
-                                        (Add w32 2 N5)=(Extract w8 16 N6),
-                                        (Add w32 3 N5)=(Extract w8 24 N6)] @
-                                    U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr60))),
-                                        (Add w32 1 N7)=(Extract w8 8 N8),
-                                        (Add w32 2 N7)=(Extract w8 16 N8),
-                                        (Add w32 3 N7)=(Extract w8 24 N8),
-                                        63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1])
-                        (Concat w24 (Read w8 50 U1)
-                                    (ReadLSB w16 48 U1)))
+        (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr115))),
+                                (Add w32 1 N5)=(Extract w8 8 N6),
+                                (Add w32 2 N5)=(Extract w8 16 N6),
+                                (Add w32 3 N5)=(Extract w8 24 N6)] @
+                            U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr115))),
+                                (Add w32 1 N7)=(Extract w8 8 N8),
+                                (Add w32 2 N7)=(Extract w8 16 N8),
+                                (Add w32 3 N7)=(Extract w8 24 N8),
+                                63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1])
             N4)
         (Not (Eq 32
-                 (Concat w32 (Read w8 (Add w32 3 N9:(Mul w32 4 N1))
-                                      U2)
-                             (Concat w24 (Read w8 (Add w32 2 N9)
-                                                  U2)
-                                         (ReadLSB w16 N9 U2)))))]
-       false)
-#   OK -- Elapsed: 0.000178814
+                 (ReadLSB w32 N9:(Mul w32 4 N1) U2)))]
+       false []
+       [arr115
+        arr119
+        arr126
+        arr133
+        arr140])
+#   OK -- Elapsed: 0.000240058
 #   Solvable: true
-#     arr60 = [104,0,0,0]
-#     arr65 = [12,0,0,0]
-#     arr72 = [0,0,0,0]
-#     arr79 = [0,0,0,0]
-#     arr86 = [1,0,0,0]
+#     arr115 = [104,0,0,0]
+#     arr119 = [12,0,0,0]
+#     arr126 = [0,0,0,0]
+#     arr133 = [0,0,0,0]
+#     arr140 = [1,0,0,0]
+
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index 2abf0070..2329279d 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,9 +1,8 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
 // RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log
-// RUN: %kleaver -print-ast klee-last/test000001.pc
-
-// FIXME: Ideally we would verify a roundtrip that we parsed the pc
-// file and can dump it back out as the same file.
+// RUN: %kleaver -print-ast klee-last/queries.pc > %t3.log
+// RUN: %kleaver -print-ast %t3.log > %t4.log
+// RUN: diff %t3.log %t4.log
 
 #include <assert.h>