From beff419a34661fb9531262aacda5891b06a22c98 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 3 Apr 2018 15:10:04 +0100
Subject: [PATCH] Use sparse arrays in get_array

This ensures that arrays from the underlying solver are interpreted in a
consistent manner in the solver (always using interval_sparse_arrayt).
---
 src/solvers/refinement/string_refinement.cpp | 55 +++++---------------
 src/solvers/refinement/string_refinement.h   |  2 +
 2 files changed, 15 insertions(+), 42 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 99477f1adbb..bc5b1c48019 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -935,50 +935,21 @@ static optionalt<exprt> get_array(
   }
   std::size_t n = *n_opt;
 
-  const array_typet ret_type(char_type, from_integer(n, index_type));
-  array_exprt ret(ret_type);
-
-  if(n>max_string_length)
+  if(n > MAX_CONCRETE_STRING_SIZE)
   {
     stream << "(sr::get_array) long string (size=" << n << ")" << eom;
-    return {};
-  }
-
-  if(n==0)
-    return empty_ret;
-
-  if(arr_val.id()=="array-list")
-  {
-    DATA_INVARIANT(
-      arr_val.operands().size()%2==0,
-      string_refinement_invariantt("and index expression must be on a symbol, "
-                                   "with, array_of, if, or array, and all "
-                                   "cases besides array are handled above"));
-    std::map<std::size_t, exprt> initial_map;
-    for(size_t i = 0; i < arr_val.operands().size(); i += 2)
-    {
-      exprt index = arr_val.operands()[i];
-      if(auto idx = numeric_cast<std::size_t>(index))
-      {
-        if(*idx < n)
-          initial_map[*idx] = arr_val.operands()[i + 1];
-      }
-    }
-
-    // Pad the concretized values to the left to assign the uninitialized
-    // values of result.
-    ret.operands()=fill_in_map_as_vector(initial_map);
-    return ret;
-  }
-  else if(arr_val.id()==ID_array)
-  {
-    // copy the `n` first elements of `arr_val`
-    for(size_t i=0; i<arr_val.operands().size() && i<n; i++)
-      ret.move_to_operands(arr_val.operands()[i]);
-    return ret;
-  }
-  else
-    return {};
+    std::ostringstream msg;
+    msg << "consider reducing string-max-input-length so that no string "
+        << "exceeds " << MAX_CONCRETE_STRING_SIZE << " in length and make sure"
+        << " all functions returning strings are available in the classpath";
+    throw string_refinement_invariantt(msg.str());
+  }
+
+  if(
+    const auto &array = interval_sparse_arrayt::of_expr(
+      arr_val, from_integer(CHARACTER_FOR_UNKNOWN, char_type)))
+    return array->concretize(n, index_type);
+  return {};
 }
 
 /// convert the content of a string to a more readable representation. This
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 281f004da87..9289b3a78f4 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -31,6 +31,8 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 
 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
 #define CHARACTER_FOR_UNKNOWN '?'
+// Limit the size of strings in traces to 64M chars to avoid memout
+#define MAX_CONCRETE_STRING_SIZE (1 << 26)
 
 class string_refinementt final: public bv_refinementt
 {