Nice patch by Hristina Palikareva that removes the dependency on STP

arrays from the Array and UpdateNode classes.



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

8 files changed, 109 insertions, 46 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 2852bf81..41d980a6 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -535,12 +535,9 @@ public:
 
 /// Class representing a byte update of an array.
 class UpdateNode {
-  friend class UpdateList;
-  friend class STPBuilder; // for setting STPArray
+  friend class UpdateList;  
 
   mutable unsigned refCount;
-  // gross
-  mutable void *stpArray;
   // cache instead of recalc
   unsigned hashValue;
 
@@ -563,7 +560,7 @@ public:
   unsigned hash() const { return hashValue; }
 
 private:
-  UpdateNode() : refCount(0), stpArray(0) {}
+  UpdateNode() : refCount(0) {}
   ~UpdateNode();
 
   unsigned computeHash();
@@ -573,16 +570,13 @@ class Array {
 public:
   const std::string name;
   // FIXME: Not 64-bit clean.
-  unsigned size;
+  unsigned size;  
 
   /// constantValues - The constant initial values for this array, or empty for
   /// a symbolic array. If non-empty, this size of this array is equivalent to
   /// the array size.
   const std::vector< ref<ConstantExpr> > constantValues;
-
-  // FIXME: This does not belong here.
-  mutable void *stpInitialArray;
-
+  
 public:
   /// Array - Construct a new array object.
   ///
@@ -595,10 +589,10 @@ public:
         const ref<ConstantExpr> *constantValuesBegin = 0,
         const ref<ConstantExpr> *constantValuesEnd = 0)
     : name(_name), size(_size), 
-      constantValues(constantValuesBegin, constantValuesEnd), 
-      stpInitialArray(0) {
+      constantValues(constantValuesBegin, constantValuesEnd) {      
     assert((isSymbolicArray() || constantValues.size() == size) &&
            "Invalid size for constant array!");
+    computeHash();
 #ifndef NDEBUG
     for (const ref<ConstantExpr> *it = constantValuesBegin;
          it != constantValuesEnd; ++it)
@@ -613,6 +607,12 @@ public:
 
   Expr::Width getDomain() const { return Expr::Int32; }
   Expr::Width getRange() const { return Expr::Int8; }
+  
+  unsigned computeHash();
+  unsigned hash() const { return hashValue; }
+   
+private:
+  unsigned hashValue;
 };
 
 /// Class representing a complete list of updates into an array.
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index e2fa0d35..f81d19d8 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -372,6 +372,9 @@ void StatsTracker::writeStatsHeader() {
              << "'CexCacheTime',"
              << "'ForkTime',"
              << "'ResolveTime',"
+#ifdef DEBUG
+	     << "'ArrayHashTime',"
+#endif
              << ")\n";
   statsFile->flush();
 }
@@ -399,6 +402,9 @@ void StatsTracker::writeStatsLine() {
              << "," << stats::cexCacheTime / 1000000.
              << "," << stats::forkTime / 1000000.
              << "," << stats::resolveTime / 1000000.
+#ifdef DEBUG
+             << "," << stats::arrayHashTime / 1000000.
+#endif
              << ")\n";
   statsFile->flush();
 }
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 089e78b3..fa8525b6 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -488,11 +488,13 @@ ref<Expr>  NotOptimizedExpr::create(ref<Expr> src) {
 extern "C" void vc_DeleteExpr(void*);
 
 Array::~Array() {
-  // FIXME: This shouldn't be necessary.
-  if (stpInitialArray) {
-    ::vc_DeleteExpr(stpInitialArray);
-    stpInitialArray = 0;
-  }
+}
+
+unsigned Array::computeHash() {
+  unsigned res = 0;
+  for (unsigned i = 0, e = name.size(); i != e; ++i)
+    res = (res * Expr::MAGIC_HASH_CONSTANT) + name[i];
+  return res; 
 }
 
 /***/
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 379f1c8d..14fd8308 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -18,8 +18,7 @@ using namespace klee;
 UpdateNode::UpdateNode(const UpdateNode *_next, 
                        const ref<Expr> &_index, 
                        const ref<Expr> &_value) 
-  : refCount(0),
-    stpArray(0),
+  : refCount(0),    
     next(_next),
     index(_index),
     value(_value) {
@@ -36,9 +35,6 @@ UpdateNode::UpdateNode(const UpdateNode *_next,
 extern "C" void vc_DeleteExpr(void*);
 
 UpdateNode::~UpdateNode() {
-  // XXX gross
-  if (stpArray)
-    ::vc_DeleteExpr(stpArray);
 }
 
 int UpdateNode::compare(const UpdateNode &b) const {
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index b1289f8d..789eb244 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -50,6 +50,32 @@ namespace {
 
 ///
 
+
+STPArrayExprHash::~STPArrayExprHash() {
+  
+  // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run;
+  // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled.
+  
+   /*
+  for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) {
+    ::VCExpr array_expr = it->second;
+    if (array_expr) {
+      ::vc_DeleteExpr(array_expr);
+      array_expr = 0;
+    }
+  }
+  
+  
+  for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) {
+    ::VCExpr un_expr = it->second;
+    if (un_expr) {
+      ::vc_DeleteExpr(un_expr);
+      un_expr = 0;
+    }
+  }
+  */
+}
+
 /***/
 
 STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides) 
@@ -62,6 +88,7 @@ STPBuilder::STPBuilder(::VC _vc, bool _optimizeDivides)
 }
 
 STPBuilder::~STPBuilder() {
+  
 }
 
 ///
@@ -399,9 +426,12 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
 }
 
 ::VCExpr STPBuilder::getInitialArray(const Array *root) {
-  if (root->stpInitialArray) {
-    return root->stpInitialArray;
-  } else {
+  
+  assert(root);
+  ::VCExpr array_expr;
+  bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
+  
+  if (!hashed) {
     // STP uniques arrays by name, so we make sure the name is unique by
     // including the address.
     char buf[32];
@@ -410,24 +440,25 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
     memmove(buf + space, buf, addrlen); // moving the address part to the end
     memcpy(buf, root->name.c_str(), space); // filling out the name part
     
-    root->stpInitialArray = buildArray(buf, 32, 8);
-
+    array_expr = buildArray(buf, 32, 8);
+    
     if (root->isConstantArray()) {
       // FIXME: Flush the concrete values into STP. Ideally we would do this
       // using assertions, which is much faster, but we need to fix the caching
       // to work correctly in that case.
       for (unsigned i = 0, e = root->size; i != e; ++i) {
-        ::VCExpr prev = root->stpInitialArray;
-        root->stpInitialArray = 
-          vc_writeExpr(vc, prev,
+	::VCExpr prev = array_expr;
+	array_expr = vc_writeExpr(vc, prev,
                        construct(ConstantExpr::alloc(i, root->getDomain()), 0),
                        construct(root->constantValues[i], 0));
-        vc_DeleteExpr(prev);
+	vc_DeleteExpr(prev);
       }
     }
-
-    return root->stpInitialArray;
+    
+    _arr_hash.hashArrayExpr(root, array_expr);
   }
+  
+  return(array_expr); 
 }
 
 ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) {
@@ -437,16 +468,23 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) {
 ::VCExpr STPBuilder::getArrayForUpdate(const Array *root, 
                                        const UpdateNode *un) {
   if (!un) {
-    return getInitialArray(root);
-  } else {
-    // FIXME: This really needs to be non-recursive.
-    if (!un->stpArray)
-      un->stpArray = vc_writeExpr(vc,
-                                  getArrayForUpdate(root, un->next),
-                                  construct(un->index, 0),
-                                  construct(un->value, 0));
-
-    return un->stpArray;
+      return(getInitialArray(root));
+  }
+  else {
+      // FIXME: This really needs to be non-recursive.
+      ::VCExpr un_expr;
+      bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
+      
+      if (!hashed) {
+	un_expr = vc_writeExpr(vc,
+                               getArrayForUpdate(root, un->next),
+                               construct(un->index, 0),
+                               construct(un->value, 0));
+	
+	_arr_hash.hashUpdateNodeExpr(un, un_expr);
+      }
+      
+      return(un_expr);
   }
 }
 
@@ -884,3 +922,5 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     return vc_trueExpr(vc);
   }
 }
+
+
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 3a19a639..0a99b753 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -11,10 +11,10 @@
 #define __UTIL_STPBUILDER_H__
 
 #include "klee/util/ExprHashMap.h"
+#include "klee/util/ArrayExprHash.h"
 #include "klee/Config/config.h"
 
 #include <vector>
-#include <map>
 
 #define Expr VCExpr
 #include <stp/c_interface.h>
@@ -56,6 +56,15 @@ namespace klee {
     operator bool () { return H->expr; }
     operator ::VCExpr () { return H->expr; }
   };
+  
+  class STPArrayExprHash : public ArrayExprHash< ::VCExpr > {
+    
+    friend class STPBuilder;
+    
+  public:
+    STPArrayExprHash() {};
+    virtual ~STPArrayExprHash();
+  };
 
 class STPBuilder {
   ::VC vc;
@@ -67,7 +76,9 @@ class STPBuilder {
   /// use.
   bool optimizeDivides;
 
-private:
+  STPArrayExprHash _arr_hash;
+
+private:  
   unsigned getShiftBits(unsigned amount) {
     unsigned bits = 1;
     amount--;
@@ -109,7 +120,7 @@ private:
   
   ::VCExpr buildVar(const char *name, unsigned width);
   ::VCExpr buildArray(const char *name, unsigned indexWidth, unsigned valueWidth);
-
+ 
 public:
   STPBuilder(::VC _vc, bool _optimizeDivides=true);
   ~STPBuilder();
diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp
index 9d48792a..1f85fe88 100644
--- a/lib/Solver/SolverStats.cpp
+++ b/lib/Solver/SolverStats.cpp
@@ -21,3 +21,7 @@ Statistic stats::queryConstructTime("QueryConstructTime", "QBtime") ;
 Statistic stats::queryConstructs("QueriesConstructs", "QB");
 Statistic stats::queryCounterexamples("QueriesCEX", "Qcex");
 Statistic stats::queryTime("QueryTime", "Qtime");
+
+#ifdef DEBUG
+Statistic stats::arrayHashTime("ArrayHashTime", "AHtime");
+#endif
diff --git a/lib/Solver/SolverStats.h b/lib/Solver/SolverStats.h
index 6fee7699..56bdf999 100644
--- a/lib/Solver/SolverStats.h
+++ b/lib/Solver/SolverStats.h
@@ -25,6 +25,10 @@ namespace stats {
   extern Statistic queryConstructs;
   extern Statistic queryCounterexamples;
   extern Statistic queryTime;
+  
+#ifdef DEBUG
+  extern Statistic arrayHashTime;
+#endif
 
 }
 }