Added factory method for Arrays + hid constructors from outside calls

The way that Arrays were handled in the past led to the possibility of
aliasing issues.  This occured whenever a new branch discovered an array
for the first time.  Each branch would create a new instance of the same
array without seeing if it had been created before. Therefore, should a
new branch encounter the same state as some previous branch, the
previous branch's solution wouldn't satisfy the new state since they
didn't recognize they were referencing the same array.  By creating an
array factory that creates a single symbolic array, that problem is
handled.  Note: Concrete arrays should not be created by the factory
method since their values are never shared between branches.

The factory works by seeing if an array with a similar hash has been
created before (the hash is based on the name and size of array).  If
there has been it then searches through all of the arrays with the same
hash (stored in a vector) to see if there is one with an exact match.
If there is one, the address of this previously created equivalent
array is returned.  Otherwise, the newly created array is unique, it is
added to the map, and it's address is returned.

This aliasing issue can be seen by comparing the output of the
Dogfood/ImmutableSet.cpp test cases with and with out this commit.
Both act correctly, but the number of queries making it to the solver
in the previous version is much greater 244 vs 211.  This is because
the UBTree in the CexCachingSolver and the cache in the CachingSolver
do not recognize queries whose solutions were previously calculated
because it doesn't think the arrays in the two queries are the same.
While this does not cause an error, it does mean that extra calls are
made.

1 files changed, 36 insertions, 0 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index d54b8f4d..46ea30fc 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -490,10 +490,46 @@ unsigned Array::computeHash() {
   unsigned res = 0;
   for (unsigned i = 0, e = name.size(); i != e; ++i)
     res = (res * Expr::MAGIC_HASH_CONSTANT) + name[i];
+  res = (res * Expr::MAGIC_HASH_CONSTANT) + size;
   hashValue = res;
   return hashValue; 
 }
 
+std::map<unsigned, std::vector<const Array *> *> Array::symbolicArraySingletonMap;
+
+const Array * Array::CreateArray(const std::string &_name, uint64_t _size,
+                                 const ref<ConstantExpr> *constantValuesBegin,
+                                 const ref<ConstantExpr> *constantValuesEnd,
+                                 Expr::Width _domain,
+								 Expr::Width _range){
+
+  const Array * array = new Array(_name, _size, constantValuesBegin, constantValuesEnd, _domain,_range);
+  if(array->constantValues.size() == 0){
+    //means is a symbolic array and we should look up the values;
+    unsigned hash = array->hash();
+    std::vector<const Array *> * bucket = Array::symbolicArraySingletonMap[hash];
+    if(bucket){
+      for(std::vector<const Array*>::const_iterator it = bucket->begin();
+          it != bucket->end(); it ++){
+        const Array* prospect = *it;
+    	if(prospect->size == array->size && prospect->name == array->name){
+    	  delete array;
+    	  return prospect;
+    	}
+      }
+      bucket->push_back(array);
+      return array;
+    }else{
+      bucket = new std::vector<const Array *>();
+      bucket->push_back(array);
+      Array::symbolicArraySingletonMap[hash] = bucket;
+      return array;
+    }
+  }else{
+    return array;
+  }
+}
+
 /***/
 
 ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {