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

4 files changed, 83 insertions, 24 deletions

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
 
 }
 }