Implement getArrayForUpdate iteratively

3 files changed, 70 insertions, 41 deletions

diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 376ffe25..7a3d7837 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -20,6 +20,7 @@
 
 #ifdef ENABLE_METASMT
 
+#include "llvm/ADT/iterator_range.h"
 #include "llvm/Support/CommandLine.h"
 
 #include <metaSMT/frontend/Logic.hpp>
@@ -172,22 +173,32 @@ template <typename SolverContext>
 typename SolverContext::result_type
 MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root,
                                                  const UpdateNode *un) {
-
+  // Iterate over the update nodes, until we find a cached version of the node,
+  // or no more update nodes remain
+  typename SolverContext::result_type un_expr;
+  std::vector<const UpdateNode *> update_nodes;
+  for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr);
+       un = un->next.get()) {
+    update_nodes.push_back(un);
+  }
   if (!un) {
-    return (getInitialArray(root));
-  } else {
-    typename SolverContext::result_type un_expr;
-    bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
-
-    if (!hashed) {
-      un_expr = evaluate(_solver,
-                         metaSMT::logic::Array::store(
-                             getArrayForUpdate(root, un->next.get()),
-                             construct(un->index, 0), construct(un->value, 0)));
-      _arr_hash.hashUpdateNodeExpr(un, un_expr);
-    }
-    return (un_expr);
+    un_expr = getInitialArray(root);
+  }
+  // `un_expr` now holds an expression for the array - either from cache or by
+  // virtue of being the initial array expression
+
+  // Create and cache solver expressions based on the update nodes starting from
+  // the oldest
+  for (const auto &un :
+       llvm::make_range(update_nodes.crbegin(), update_nodes.crend())) {
+    un_expr = evaluate(
+        _solver, metaSMT::logic::Array::store(un_expr, construct(un->index, 0),
+                                              construct(un->value, 0)));
+
+    _arr_hash.hashUpdateNodeExpr(un, un_expr);
   }
+
+  return un_expr;
 }
 
 template <typename SolverContext>
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 13a42513..9a38183d 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -18,6 +18,7 @@
 #include "ConstantDivision.h"
 
 #include "llvm/ADT/StringExtras.h"
+#include "llvm/ADT/iterator_range.h"
 #include "llvm/Support/CommandLine.h"
 
 #include <cstdio>
@@ -465,26 +466,33 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) {
   return vc_readExpr(vc, getInitialArray(root), bvConst32(32, index));
 }
 
-::VCExpr STPBuilder::getArrayForUpdate(const Array *root, 
+::VCExpr STPBuilder::getArrayForUpdate(const Array *root,
                                        const UpdateNode *un) {
+  // Iterate over the update nodes, until we find a cached version of the node,
+  // or no more update nodes remain
+  ::VCExpr un_expr;
+  std::vector<const UpdateNode *> update_nodes;
+  for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr);
+       un = un->next.get()) {
+    update_nodes.push_back(un);
+  }
   if (!un) {
-      return getInitialArray(root);
+    un_expr = 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.get()),
-                         construct(un->index, 0), construct(un->value, 0));
+  // `un_expr` now holds an expression for the array - either from cache or by
+  // virtue of being the initial array expression
 
-        _arr_hash.hashUpdateNodeExpr(un, un_expr);
-      }
-      
-      return un_expr;
+  // Create and cache solver expressions based on the update nodes starting from
+  // the oldest
+  for (const auto &un :
+       llvm::make_range(update_nodes.crbegin(), update_nodes.crend())) {
+    un_expr = vc_writeExpr(vc, un_expr, construct(un->index, 0),
+                           construct(un->value, 0));
+
+    _arr_hash.hashUpdateNodeExpr(un, un_expr);
   }
+
+  return un_expr;
 }
 
 /** if *width_out!=1 then result is a bitvector,
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index 950bd879..e1937158 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -17,6 +17,7 @@
 #include "klee/Support/ErrorHandling.h"
 
 #include "llvm/ADT/StringExtras.h"
+#include "llvm/ADT/iterator_range.h"
 #include "llvm/Support/CommandLine.h"
 
 using namespace klee;
@@ -427,22 +428,31 @@ Z3ASTHandle Z3Builder::getInitialRead(const Array *root, unsigned index) {
 
 Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root,
                                          const UpdateNode *un) {
+  // Iterate over the update nodes, until we find a cached version of the node,
+  // or no more update nodes remain
+  Z3ASTHandle un_expr;
+  std::vector<const UpdateNode *> update_nodes;
+  for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr);
+       un = un->next.get()) {
+    update_nodes.push_back(un);
+  }
   if (!un) {
-    return (getInitialArray(root));
-  } else {
-    // FIXME: This really needs to be non-recursive.
-    Z3ASTHandle un_expr;
-    bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
-
-    if (!hashed) {
-      un_expr = writeExpr(getArrayForUpdate(root, un->next.get()),
-                          construct(un->index, 0), construct(un->value, 0));
+    un_expr = getInitialArray(root);
+  }
+  // `un_expr` now holds an expression for the array - either from cache or by
+  // virtue of being the initial array expression
 
-      _arr_hash.hashUpdateNodeExpr(un, un_expr);
-    }
+  // Create and cache solver expressions based on the update nodes starting from
+  // the oldest
+  for (const auto &un :
+       llvm::make_range(update_nodes.crbegin(), update_nodes.crend())) {
+    un_expr =
+        writeExpr(un_expr, construct(un->index, 0), construct(un->value, 0));
 
-    return (un_expr);
+    _arr_hash.hashUpdateNodeExpr(un, un_expr);
   }
+
+  return un_expr;
 }
 
 /** if *width_out!=1 then result is a bitvector,