Implement getArrayForUpdate iteratively

1 files changed, 23 insertions, 15 deletions

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,