Pull array_pool class out of constraint generator

Pull out this part of constraint generator to decrease the size of the
class, make unit test easier and the code more modular and reusable.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -38,6 +38,51 @@ class symbol_generatort final
   unsigned symbol_count = 0;
 };
 
+/// Correspondance between arrays and pointers string representations
+class array_poolt final
+{
+public:
+  explicit array_poolt(symbol_generatort &symbol_generator)
+    : fresh_symbol(symbol_generator)
+  {
+  }
+
+  const std::unordered_map<exprt, array_string_exprt, irep_hash> &
+  get_arrays_of_pointers() const
+  {
+    return arrays_of_pointers;
+  }
+
+  exprt get_length(const array_string_exprt &s) const;
+
+  void insert(const exprt &pointer_expr, array_string_exprt &array);
+
+  array_string_exprt find(const exprt &pointer, const exprt &length);
+
+  array_string_exprt find(const refined_string_exprt &str);
+
+  /// Converts a struct containing a length and pointer to an array.
+  /// This allows to get a string expression from arguments of a string
+  /// builtion function, because string arguments in these function calls
+  /// are given as a struct containing a length and pointer to an array.
+  array_string_exprt of_argument(const exprt &arg);
+
+private:
+  // associate arrays to char pointers
+  std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
+
+  // associate length to arrays of infinite size
+  std::unordered_map<array_string_exprt, symbol_exprt, irep_hash>
+    length_of_array;
+
+  // generates fresh symbols
+  symbol_generatort &fresh_symbol;
+
+  array_string_exprt make_char_array_for_char_pointer(
+    const exprt &char_pointer,
+    const typet &char_array_type);
+};
+
 class string_constraint_generatort final
 {
 public:
@@ -85,15 +130,12 @@ class string_constraint_generatort final
 
   symbol_generatort fresh_symbol;
 
-  const std::map<exprt, array_string_exprt> &get_arrays_of_pointers() const
-  {
-    return arrays_of_pointers_;
-  }
   symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
 
-  exprt get_length_of_string_array(const array_string_exprt &s) const;
   symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
 
+  array_poolt array_pool;
+
   // Type used by primitives to signal errors
   const signedbv_typet get_return_code_type()
   {
@@ -107,9 +149,6 @@ class string_constraint_generatort final
   array_string_exprt get_string_expr(const exprt &expr);
   plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2);
 
-  array_string_exprt associate_char_array_to_char_pointer(
-    const exprt &char_pointer,
-    const typet &char_array_type);
 
   static constant_exprt constant_char(int i, const typet &char_type);
 
@@ -371,12 +410,6 @@ class string_constraint_generatort final
 
   // Pool used for the intern method
   std::map<array_string_exprt, symbol_exprt> intern_of_string;
-
-  // associate arrays to char pointers
-  std::map<exprt, array_string_exprt> arrays_of_pointers_;
-
-  // associate length to arrays of infinite size
-  std::map<array_string_exprt, symbol_exprt> length_of_array_;
 };
 
 exprt is_digit_with_radix(

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -31,8 +31,7 @@ Author: Romain Brenguier, [email protected]
 string_constraint_generatort::string_constraint_generatort(
   const string_constraint_generatort::infot &info,
   const namespacet &ns)
-  : max_string_length(info.string_max_length),
-    ns(ns)
+  : array_pool(fresh_symbol), max_string_length(info.string_max_length), ns(ns)
 {
 }
 
@@ -157,13 +156,12 @@ plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check(
 /// Associate an actual finite length to infinite arrays
 /// \param s: array expression representing a string
 /// \return expression for the length of `s`
-exprt string_constraint_generatort::get_length_of_string_array(
-  const array_string_exprt &s) const
+exprt array_poolt::get_length(const array_string_exprt &s) const
 {
   if(s.length() == infinity_exprt(s.length().type()))
   {
-    auto it = length_of_array_.find(s);
-    if(it != length_of_array_.end())
+    auto it = length_of_array.find(s);
+    if(it != length_of_array.end())
       return it->second;
   }
   return s.length();
@@ -185,10 +183,9 @@ array_string_exprt string_constraint_generatort::fresh_string(
   return str;
 }
 
-// Associate a char array to a char pointer. The size of the char array is a
+// Make a new char array for a char pointer. The size of the char array is a
 // variable with no constraint.
-array_string_exprt
-string_constraint_generatort::associate_char_array_to_char_pointer(
+array_string_exprt array_poolt::make_char_array_for_char_pointer(
   const exprt &char_pointer,
   const typet &char_array_type)
 {
@@ -214,10 +211,10 @@ string_constraint_generatort::associate_char_array_to_char_pointer(
   else if(char_pointer.id() == ID_if)
   {
     const if_exprt &if_expr = to_if_expr(char_pointer);
-    const array_string_exprt t = associate_char_array_to_char_pointer(
-      if_expr.true_case(), char_array_type);
-    const array_string_exprt f = associate_char_array_to_char_pointer(
-      if_expr.false_case(), char_array_type);
+    const array_string_exprt t =
+      make_char_array_for_char_pointer(if_expr.true_case(), char_array_type);
+    const array_string_exprt f =
+      make_char_array_for_char_pointer(if_expr.false_case(), char_array_type);
     array_typet array_type(
       char_array_type.subtype(),
       if_exprt(
@@ -247,15 +244,32 @@ string_constraint_generatort::associate_char_array_to_char_pointer(
   array_string_exprt array_sym =
     to_array_string_expr(fresh_symbol(symbol_name, char_array_type));
   auto insert_result =
-    arrays_of_pointers_.insert(std::make_pair(char_pointer, array_sym));
+    arrays_of_pointers.insert(std::make_pair(char_pointer, array_sym));
   array_string_exprt result = to_array_string_expr(insert_result.first->second);
   return result;
 }
 
+void array_poolt::insert(
+  const exprt &pointer_expr,
+  array_string_exprt &array_expr)
+{
+  const exprt &length = array_expr.length();
+  if(length == infinity_exprt(length.type()))
+  {
+    auto pair = length_of_array.insert(
+      std::make_pair(array_expr, fresh_symbol("string_length", length.type())));
+    array_expr.length() = pair.first->second;
+  }
+
+  const auto it_bool =
+    arrays_of_pointers.insert(std::make_pair(pointer_expr, array_expr));
+  INVARIANT(
+    it_bool.second, "should not associate two arrays to the same pointer");
+}
+
 /// Associate a char array to a char pointer.
-/// Insert in `arrays_of_pointers_` a binding from `ptr` to `arr`.
-/// If the length of `arr` is infinite, we create a new integer symbol and add
-/// a binding from `arr` to this length in `length_of_array_`.
+/// Insert in `array_pool` a binding from `ptr` to `arr`. If the length of `arr`
+/// is infinite, a new integer symbol is created and stored in `array_pool`.
 /// This also adds the default axioms for `arr`.
 /// \param f: a function application with argument a character array `arr` and
 /// a character pointer `ptr`.
@@ -271,21 +285,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
                                       : f.arguments()[0]);
 
   const exprt &pointer_expr = f.arguments()[1];
-
-  const auto &length = array_expr.length();
-  if(length == infinity_exprt(length.type()))
-  {
-    auto pair = length_of_array_.insert(
-      std::make_pair(array_expr, fresh_symbol("string_length", length.type())));
-    array_expr.length() = pair.first->second;
-  }
-
-  /// \todo We should use a function for inserting the correspondance
-  /// between array and pointers.
-  const auto it_bool =
-    arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
-  INVARIANT(
-    it_bool.second, "should not associate two arrays to the same pointer");
+  array_pool.insert(pointer_expr, array_expr);
   add_default_axioms(to_array_string_expr(array_expr));
   return from_integer(0, f.type());
 }
@@ -302,7 +302,7 @@ exprt string_constraint_generatort::associate_length_to_array(
   array_string_exprt array_expr = to_array_string_expr(f.arguments()[0]);
   const exprt &new_length = f.arguments()[1];
 
-  const auto &length = get_length_of_string_array(array_expr);
+  const auto &length = array_pool.get_length(array_expr);
   lemmas.push_back(equal_exprt(length, new_length));
   return from_integer(0, f.type());
 }
@@ -400,19 +400,36 @@ exprt string_constraint_generatort::add_axioms_for_constrain_characters(
   return from_integer(0, get_return_code_type());
 }
 
+/// Creates a new array if the pointer is not pointing to an array
+/// \todo This should be replaced by make_char_array_for_char_pointer
+array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
+{
+  const array_typet array_type(pointer.type().subtype(), length);
+  return make_char_array_for_char_pointer(pointer, array_type);
+}
+
 /// Adds creates a new array if it does not already exists
 /// \todo This should be replaced by associate_char_array_to_char_pointer
 array_string_exprt string_constraint_generatort::char_array_of_pointer(
   const exprt &pointer,
   const exprt &length)
 {
-  const array_typet array_type(pointer.type().subtype(), length);
-  const array_string_exprt array =
-    associate_char_array_to_char_pointer(pointer, array_type);
+  const array_string_exprt array = array_pool.find(pointer, length);
   add_default_axioms(array);
   return array;
 }
 
+array_string_exprt array_poolt::find(const refined_string_exprt &str)
+{
+  return find(str.content(), str.length());
+}
+
+array_string_exprt array_poolt::of_argument(const exprt &arg)
+{
+  const auto string_argument = expr_checked_cast<struct_exprt>(arg);
+  return find(string_argument.op1(), string_argument.op0());
+}
+
 /// strings contained in this call are converted to objects of type
 /// `string_exprt`, through adding axioms. Axioms are then added to enforce that
 /// the result corresponds to the function application.

src/solvers/refinement/string_refinement.cpp

@@ -801,7 +801,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
 #ifdef DEBUG
   debug() << "dec_solve: arrays_of_pointers:" << eom;
-  for(auto pair : generator.get_arrays_of_pointers())
+  for(auto pair :
+      generator.array_pointer_correspondance.get_arrays_of_pointers())
   {
     debug() << "  * " << format(pair.first) << "\t--> " << format(pair.second)
             << " : " << format(pair.second.type()) << eom;
@@ -1193,7 +1194,7 @@ void debug_model(
   static const std::string indent("  ");
 
   stream << "debug_model:" << '\n';
-  for(const auto &pointer_array : generator.get_arrays_of_pointers())
+  for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers())
   {
     const auto arr = pointer_array.second;
     const exprt model = get_char_array_and_concretize(
@@ -2418,7 +2419,7 @@ exprt string_refinementt::get(const exprt &expr) const
   if(is_char_array_type(ecopy.type(), ns))
   {
     array_string_exprt &arr = to_array_string_expr(ecopy);
-    arr.length() = generator.get_length_of_string_array(arr);
+    arr.length() = generator.array_pool.get_length(arr);
     const auto arr_model_opt =
       get_array(super_get, ns, generator.max_string_length, debug(), arr);
     // \todo Refactor with get array in model