Implement array declarations.

 - Printing current prints all declarations, and we allow redefinition, since
   the printer doesn't know what has already been printed.

 - Names don't print right yet, since the Array* object doesn't have the name.

 - Various things are unsupported.
   o Array domain/range must be w32/w8.
   o Concrete initializers for arrays are unsupported.


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

1 files changed, 24 insertions, 2 deletions

diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index affde4ad..7bfb6567 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -81,6 +81,9 @@ public:
 };
 
 class PPrinter : public ExprPPrinter {
+public:
+  std::set<const Array*> usedArrays;
+private:
   std::map<ref<Expr>, unsigned> bindings;
   std::map<const UpdateNode*, unsigned> updateBindings;
   std::set< ref<Expr> > couldPrint, shouldPrint;
@@ -131,6 +134,7 @@ class PPrinter : public ExprPPrinter {
   }
   
   void scanUpdate(const UpdateNode *un) {
+    // FIXME: This needs to be non-recursive.
     if (un) {
       if (couldPrintUpdates.insert(un).second) {
         scanUpdate(un->next);
@@ -148,8 +152,10 @@ class PPrinter : public ExprPPrinter {
         Expr *ep = e.get();
         for (unsigned i=0; i<ep->getNumKids(); i++)
           scan1(ep->getKid(i));
-        if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) 
+        if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
+          usedArrays.insert(re->updates.root);
           scanUpdate(re->updates.head);
+        }
       } else {
         shouldPrint.insert(e);
       }
@@ -507,7 +513,8 @@ void ExprPPrinter::printQuery(std::ostream &os,
                               const ref<Expr> *evalExprsBegin,
                               const ref<Expr> *evalExprsEnd,
                               const Array * const *evalArraysBegin,
-                              const Array * const *evalArraysEnd) {
+                              const Array * const *evalArraysEnd,
+                              bool printArrayDecls) {
   PPrinter p(os);
   
   for (ConstraintManager::const_iterator it = constraints.begin(),
@@ -519,6 +526,21 @@ void ExprPPrinter::printQuery(std::ostream &os,
     p.scan(*it);
 
   PrintContext PC(os);
+  
+  // Print array declarations.
+  if (printArrayDecls) {
+    for (std::set<const Array*>::iterator it = p.usedArrays.begin(), 
+           ie = p.usedArrays.end(); it != ie; ++it) {
+      const Array *A = *it;
+      // FIXME: Print correct name, domain, and range.
+      PC << "array " << "arr" << A->id 
+         << "[" << A->size << "]"
+         << " : " << "w32" << " -> " << "w8"
+         << " = symbolic";
+      PC.breakLine();
+    }
+  }
+
   PC << "(query [";
   
   // Ident at constraint list;