Switch Array* print-outs to use name instead of ID, and update a few

constructors I missed.


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

7 files changed, 18 insertions, 15 deletions

diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 831a4d91..e3a83f9a 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -167,7 +167,9 @@ private:
 
     // Special case empty list.
     if (!head) {
-      PC << "arr" << updates.root->id;
+      // FIXME: We need to do something (assert, mangle, etc.) so that printing
+      // distinct arrays with the same name doesn't fail.
+      PC << updates.root->name;
       return;
     }
 
@@ -217,7 +219,7 @@ private:
     if (openedList)
       PC << ']';
 
-    PC << " @ arr" << updates.root->id;
+    PC << " @ " << updates.root->name;
   }
 
   void printWidth(PrintContext &PC, ref<Expr> e) {
@@ -528,7 +530,7 @@ void ExprPPrinter::printQuery(std::ostream &os,
            ie = p.usedArrays.end(); it != ie; ++it) {
       const Array *A = *it;
       // FIXME: Print correct name, domain, and range.
-      PC << "array " << "arr" << A->id 
+      PC << "array " << A->name
          << "[" << A->size << "]"
          << " : " << "w32" << " -> " << "w8"
          << " = symbolic";
@@ -572,7 +574,7 @@ void ExprPPrinter::printQuery(std::ostream &os,
     PC.breakLine(indent - 1);
     PC << '[';
     for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it) {
-      PC << "arr" << (*it)->id;
+      PC << (*it)->name;
       if (it + 1 != evalArraysEnd)
         PC.breakLine(indent);
     }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 77596727..8c18fe73 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -1557,7 +1557,7 @@ Decl::Decl(DeclKind _Kind) : Kind(_Kind) {}
 
 void ArrayDecl::dump() {
   // FIXME: For now, print using the Array* "name".
-  std::cout << "array " << "arr" << Root->id
+  std::cout << "array " << Root->name
             << "[" << Size << "]"
             << " : " << 'w' << Domain << " -> " << 'w' << Range << " = ";
 
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 7ebee1c7..69f9567c 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -131,7 +131,7 @@ public:
         os << ", ";
       }
 
-      os << "MO" << array->id;
+      os << "MO" << array->name;
     }
     for (elements_ty::const_iterator it = elements.begin(), ie = elements.end();
          it != ie; ++it) {
@@ -144,7 +144,7 @@ public:
         os << ", ";
       }
 
-      os << "MO" << array->id << " : " << dis;
+      os << "MO" << array->name << " : " << dis;
     }
     os << "}";
   }
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
index 3c605256..03146251 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/PCLoggingSolver.cpp
@@ -128,7 +128,7 @@ public:
                e = objects.end(); i != e; ++i, ++values_it) {
           const Array *array = *i;
           std::vector<unsigned char> &data = *values_it;
-          os << "#     arr" << array->id << " = [";
+          os << "#     " << array->name << " = [";
           for (unsigned j = 0; j < array->size; j++) {
             os << (int) data[j];
             if (j+1 < array->size)
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index a575c086..fca83905 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -171,7 +171,7 @@ static bool EvaluateInputAST(const char *Filename,
 
           for (unsigned i = 0, e = result.size(); i != e; ++i) {
             llvm::cout << "\tArray " << i << ":\t"
-                       << "arr" << QC->Objects[i]->id
+                       << QC->Objects[i]->name
                        << "[";
             for (unsigned j = 0; j != QC->Objects[i]->size; ++j) {
               llvm::cout << (unsigned) result[i][j];
diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp
index 7b37973a..f86af1aa 100644
--- a/unittests/Expr/ExprTest.cpp
+++ b/unittests/Expr/ExprTest.cpp
@@ -28,9 +28,9 @@ TEST(ExprTest, BasicConstruction) {
 }
 
 TEST(ExprTest, ConcatExtract) {
-  Array *array = new Array(0, 1, 256);
+  Array *array = new Array("arr0", 0, 1, 256);
   ref<Expr> read8 = Expr::createTempRead(array, 8);
-  Array *array2 = new Array(0, 2, 256);
+  Array *array2 = new Array("arr1", 0, 2, 256);
   ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
   ref<Expr> c100 = getConstant(100, 8);
 
@@ -80,10 +80,10 @@ TEST(ExprTest, ConcatExtract) {
 }
 
 TEST(ExprTest, ExtractConcat) {
-  Array *array = new Array(0, 3, 256);
+  Array *array = new Array("arr0", 0, 3, 256);
   ref<Expr> read64 = Expr::createTempRead(array, 64);
 
-  Array *array2 = new Array(0, 4, 256);
+  Array *array2 = new Array("arr1", 0, 4, 256);
   ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
   
   ref<Expr> extract1 = ExtractExpr::create(read64, 36, 4);
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index 1b1e0f3f..a6130716 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -12,6 +12,7 @@
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/Solver.h"
+#include "llvm/ADT/StringExtras.h"
 
 using namespace klee;
 
@@ -43,8 +44,8 @@ void testOperation(Solver &solver,
       return;
 
     unsigned size = Expr::getMinBytesForWidth(operandWidth);
-    static unsigned id = 0;
-    Array *array = new Array(0, ++id, size);
+    static uint64_t id = 0;
+    Array *array = new Array("arr" + llvm::utostr(id), 0, ++id, size);
     symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(array, 
                                                                 operandWidth)));
   }