has_subtype(type, pred, ns) to search for contained type matching pred

This is the counterpart to has_subexpr; the previous local implementation in
string_refinement_util is promoted to expr_util and extended to work with types
that require a namespace lookup.

Author: tautschnig

src/solvers/refinement/string_refinement.cpp

@@ -23,6 +23,7 @@ Author: Alberto Griggio, [email protected]
 #include <numeric>
 #include <stack>
 #include <util/expr_iterator.h>
+#include <util/expr_util.h>
 #include <util/simplify_expr.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_constraint_instantiation.h>
@@ -341,7 +342,7 @@ static union_find_replacet generate_symbol_resolution_from_equations(
       // in the convert_function_application step of dec_solve
     }
     else if(lhs.type().id() != ID_pointer &&
-      has_char_pointer_subtype(lhs.type()))
+      has_char_pointer_subtype(lhs.type(), ns))
     {
       if(rhs.type().id() == ID_struct)
       {
@@ -432,7 +433,7 @@ static void add_string_equation_to_symbol_resolution(
   {
     symbol_resolve.make_union(eq.lhs(), eq.rhs());
   }
-  else if(has_string_subtype(eq.lhs().type()))
+  else if(has_subtype(eq.lhs().type(), ID_string, ns))
   {
     if(eq.rhs().type().id() == ID_struct)
     {
@@ -485,7 +486,7 @@ union_find_replacet string_identifiers_resolution_from_equations(
         equation_map.add(i, expr);
     }
     else if(eq.lhs().type().id() != ID_pointer &&
-       has_string_subtype(eq.lhs().type()))
+       has_subtype(eq.lhs().type(), ID_string, ns))
     {
       std::vector<exprt> lhs_strings = extract_strings_from_lhs(eq.lhs());
 

src/solvers/refinement/string_refinement_util.cpp

@@ -11,6 +11,7 @@
 #include <functional>
 #include <iostream>
 #include <util/arith_tools.h>
+#include <util/expr_util.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 #include <util/expr_iterator.h>
@@ -45,40 +46,9 @@ 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)
+bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
 {
-  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(); });
+  return has_subtype(type, is_char_pointer_type, ns);
 }
 
 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)

src/solvers/refinement/string_refinement_util.h

@@ -35,34 +35,13 @@ bool is_char_array_type(const typet &type, const namespacet &ns);
 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
+/// \param ns: namespace
 /// \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);
+bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
 
 /// \param expr: an expression
 /// \param ns: namespace

src/util/expr_util.cpp

@@ -132,6 +132,44 @@ bool has_subexpr(const exprt &src, const irep_idt &id)
   return false;
 }
 
+bool has_subtype(
+  const typet &type,
+  const std::function<bool(const typet &)> &pred,
+  const namespacet &ns)
+{
+  if(pred(type))
+    return true;
+  else if(type.id() == ID_symbol)
+    return has_subtype(ns.follow(type), pred, ns);
+  else if(type.id() == ID_c_enum_tag)
+    return has_subtype(ns.follow_tag(to_c_enum_tag_type(type)), pred, ns);
+  else if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    const struct_union_typet &struct_union_type = to_struct_union_type(type);
+
+    for(const auto &comp : struct_union_type.components())
+      if(has_subtype(comp.type(), pred, ns))
+        return true;
+  }
+  // do not look into pointer subtypes as this could cause unbounded recursion
+  else if(type.id() == ID_array || type.id() == ID_vector)
+    return has_subtype(type.subtype(), pred, ns);
+  else if(type.has_subtypes())
+  {
+    for(const auto &subtype : type.subtypes())
+      if(has_subtype(subtype, pred, ns))
+        return true;
+  }
+
+  return false;
+}
+
+bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
+{
+  return has_subtype(
+    type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
+}
+
 if_exprt lift_if(const exprt &src, std::size_t operand_number)
 {
   PRECONDITION(operand_number<src.operands().size());

src/util/expr_util.h

@@ -44,6 +44,26 @@ exprt boolean_negate(const exprt &);
 /// returns true if the expression has a subexpression with given ID
 bool has_subexpr(const exprt &, const irep_idt &);
 
+/// returns true if any of the contained types satisfies pred
+/// \param type: a type
+/// \param pred: a predicate
+/// \param ns: namespace for symbol type lookups
+/// \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,
+  const namespacet &ns);
+
+/// returns true if any of the contained types is id
+bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
+
 /// lift up an if_exprt one level
 if_exprt lift_if(const exprt &, std::size_t operand_number);