From 95a9886b32c1b0086b60f828f3f2c139dd863211 Mon Sep 17 00:00:00 2001
From: Daniel Schemmel <daniel@schemmel.net>
Date: Fri, 24 Jun 2022 15:27:25 +0100
Subject: Implement getArrayForUpdate iteratively

---
 lib/Solver/STPBuilder.cpp | 38 +++++++++++++++++++++++---------------
 1 file changed, 23 insertions(+), 15 deletions(-)

(limited to 'lib/Solver/STPBuilder.cpp')

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,
-- 
cgit 1.4.1