Move utility functions to string_refinement_util

This reduces the size of string_refinement files and seperate functions
that could be reused outside of string_refinement, for instace for unit testing.

src/solvers/refinement/string_refinement.cpp

@@ -287,107 +287,6 @@ static void substitute_function_applications_in_equations(
     substitute_function_applications(eq.rhs(), generator);
 }
 
-/// For now, any unsigned bitvector type of width smaller or equal to 16 is
-/// considered a character.
-/// \note type that are not characters maybe detected as characters (for
-/// instance unsigned char in C), this will make dec_solve do unnecessary
-/// steps for these, but should not affect correctness.
-/// \param type: a type
-/// \return true if the given type represents characters
-bool is_char_type(const typet &type)
-{
-  return type.id() == ID_unsignedbv &&
-         to_unsignedbv_type(type).get_width() <= 16;
-}
-
-/// Distinguish char array from other types.
-/// For now, any unsigned bitvector type is considered a character.
-/// \param type: a type
-/// \param ns: namespace
-/// \return true if the given type is an array of characters
-bool is_char_array_type(const typet &type, const namespacet &ns)
-{
-  if(type.id()==ID_symbol)
-    return is_char_array_type(ns.follow(type), ns);
-  return type.id() == ID_array && is_char_type(type.subtype());
-}
-
-/// For now, any unsigned bitvector type is considered a character.
-/// \param type: a type
-/// \return true if the given type represents a pointer to characters
-bool is_char_pointer_type(const typet &type)
-{
-  return type.id() == ID_pointer && is_char_type(type.subtype());
-}
-
-/// \param type: a type
-/// \param pred: a predicate
-/// \return true if one of the subtype of `type` satisfies predicate `pred`.
-///         The meaning of "subtype" is in the algebraic datatype sense:
-///         for example, the subtypes of a struct are the types of its
-///         components, the subtype of a pointer is the type it points to,
-///         etc...
-///         For instance in the type `t` defined by
-///         `{ int a; char[] b; double * c; { bool d} e}`, `int`, `char`,
-///         `double` and `bool` are subtypes of `t`.
-bool has_subtype(
-  const typet &type,
-  const std::function<bool(const typet &)> &pred)
-{
-  if(pred(type))
-    return true;
-
-  if(type.id() == ID_struct || type.id() == ID_union)
-  {
-    const struct_union_typet &struct_type = to_struct_union_type(type);
-    return std::any_of(
-      struct_type.components().begin(),
-      struct_type.components().end(), // NOLINTNEXTLINE
-      [&](const struct_union_typet::componentt &comp) {
-        return has_subtype(comp.type(), pred);
-      });
-  }
-
-  return std::any_of( // NOLINTNEXTLINE
-    type.subtypes().begin(), type.subtypes().end(), [&](const typet &t) {
-      return has_subtype(t, pred);
-    });
-}
-
-/// \param type: a type
-/// \return true if a subtype of `type` is an pointer of characters.
-///         The meaning of "subtype" is in the algebraic datatype sense:
-///         for example, the subtypes of a struct are the types of its
-///         components, the subtype of a pointer is the type it points to,
-///         etc...
-static bool has_char_pointer_subtype(const typet &type)
-{
-  return has_subtype(type, is_char_pointer_type);
-}
-
-/// \param type: a type
-/// \return true if a subtype of `type` is string_typet.
-///         The meaning of "subtype" is in the algebraic datatype sense:
-///         for example, the subtypes of a struct are the types of its
-///         components, the subtype of a pointer is the type it points to,
-///         etc...
-static bool has_string_subtype(const typet &type)
-{
-  // NOLINTNEXTLINE
-  return has_subtype(
-    type, [](const typet &subtype) { return subtype == string_typet(); });
-}
-
-/// \param expr: an expression
-/// \param ns: namespace
-/// \return true if a subexpression of `expr` is an array of characters
-static bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
-{
-  for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
-    if(is_char_array_type(it->type(), ns))
-      return true;
-  return false;
-}
 
 void replace_symbols_in_equations(
   const union_find_replacet &symbol_resolve,

src/solvers/refinement/string_refinement.h

@@ -93,12 +93,6 @@ exprt concretize_arrays_in_expression(
   std::size_t string_max_length,
   const namespacet &ns);
 
-bool is_char_array_type(const typet &type, const namespacet &ns);
-
-bool has_subtype(
-  const typet &type,
-  const std::function<bool(const typet &)> &pred);
-
 // Declaration required for unit-test:
 union_find_replacet string_identifiers_resolution_from_equations(
   std::vector<equal_exprt> &equations,

src/solvers/refinement/string_refinement_util.cpp

@@ -10,8 +10,74 @@
 #include <numeric>
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
+#include <util/expr_iterator.h>
+#include <util/magic.h>
 #include "string_refinement_util.h"
 
+bool is_char_type(const typet &type)
+{
+  return type.id() == ID_unsignedbv &&
+         to_unsignedbv_type(type).get_width() <=
+           STRING_REFINEMENT_MAX_CHAR_WIDTH;
+}
+
+bool is_char_array_type(const typet &type, const namespacet &ns)
+{
+  if(type.id() == ID_symbol)
+    return is_char_array_type(ns.follow(type), ns);
+  return type.id() == ID_array && is_char_type(type.subtype());
+}
+
+bool is_char_pointer_type(const typet &type)
+{
+  return type.id() == ID_pointer && is_char_type(type.subtype());
+}
+
+bool has_subtype(
+  const typet &type,
+  const std::function<bool(const typet &)> &pred)
+{
+  if(pred(type))
+    return true;
+
+  if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    const struct_union_typet &struct_type = to_struct_union_type(type);
+    return std::any_of(
+      struct_type.components().begin(),
+      struct_type.components().end(), // NOLINTNEXTLINE
+      [&](const struct_union_typet::componentt &comp) {
+        return has_subtype(comp.type(), pred);
+      });
+  }
+
+  return std::any_of( // NOLINTNEXTLINE
+    type.subtypes().begin(), type.subtypes().end(), [&](const typet &t) {
+      return has_subtype(t, pred);
+    });
+}
+
+bool has_char_pointer_subtype(const typet &type)
+{
+  return has_subtype(type, is_char_pointer_type);
+}
+
+bool has_string_subtype(const typet &type)
+{
+  // NOLINTNEXTLINE
+  return has_subtype(
+    type, [](const typet &subtype) { return subtype == string_typet(); });
+}
+
+bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
+{
+  const auto it = std::find_if(
+    expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT
+      return is_char_array_type(e.type(), ns);
+    });
+  return it != expr.depth_end();
+}
+
 sparse_arrayt::sparse_arrayt(const with_exprt &expr)
 {
   auto ref = std::ref(static_cast<const exprt &>(expr));

src/solvers/refinement/string_refinement_util.h

@@ -11,6 +11,62 @@
 
 #include "string_constraint.h"
 
+/// For now, any unsigned bitvector type of width smaller or equal to 16 is
+/// considered a character.
+/// \note type that are not characters maybe detected as characters (for
+/// instance unsigned char in C), this will make dec_solve do unnecessary
+/// steps for these, but should not affect correctness.
+/// \param type: a type
+/// \return true if the given type represents characters
+bool is_char_type(const typet &type);
+
+/// Distinguish char array from other types.
+/// For now, any unsigned bitvector type is considered a character.
+/// \param type: a type
+/// \param ns: namespace
+/// \return true if the given type is an array of characters
+bool is_char_array_type(const typet &type, const namespacet &ns);
+
+/// For now, any unsigned bitvector type is considered a character.
+/// \param type: a type
+/// \return true if the given type represents a pointer to characters
+bool is_char_pointer_type(const typet &type);
+
+/// \param type: a type
+/// \param pred: a predicate
+/// \return true if one of the subtype of `type` satisfies predicate `pred`.
+///         The meaning of "subtype" is in the algebraic datatype sense:
+///         for example, the subtypes of a struct are the types of its
+///         components, the subtype of a pointer is the type it points to,
+///         etc...
+///         For instance in the type `t` defined by
+///         `{ int a; char[] b; double * c; { bool d} e}`, `int`, `char`,
+///         `double` and `bool` are subtypes of `t`.
+bool has_subtype(
+  const typet &type,
+  const std::function<bool(const typet &)> &pred);
+
+/// \param type: a type
+/// \return true if a subtype of `type` is an pointer of characters.
+///         The meaning of "subtype" is in the algebraic datatype sense:
+///         for example, the subtypes of a struct are the types of its
+///         components, the subtype of a pointer is the type it points to,
+///         etc...
+bool has_char_pointer_subtype(const typet &type);
+
+/// \param type: a type
+/// \return true if a subtype of `type` is string_typet.
+///         The meaning of "subtype" is in the algebraic datatype sense:
+///         for example, the subtypes of a struct are the types of its
+///         components, the subtype of a pointer is the type it points to,
+///         etc...
+bool has_string_subtype(const typet &type);
+
+/// \param expr: an expression
+/// \param ns: namespace
+/// \return true if a subexpression of `expr` is an array of characters
+bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
+
 struct index_set_pairt
 {
   std::map<exprt, std::set<exprt>> cumulative;

src/util/magic.h

@@ -8,5 +8,6 @@
 #include <cstddef>
 
 const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000;
+const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16;
 
 #endif