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>
@@ -340,8 +341,8 @@ static union_find_replacet generate_symbol_resolution_from_equations(
       // function applications can be ignored because they will be replaced
       // in the convert_function_application step of dec_solve
     }
-    else if(lhs.type().id() != ID_pointer &&
-      has_char_pointer_subtype(lhs.type()))
+    else if(
+      lhs.type().id() != ID_pointer && 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)
     {
@@ -484,8 +485,9 @@ union_find_replacet string_identifiers_resolution_from_equations(
       for(const auto &expr : rhs_strings)
         equation_map.add(i, expr);
     }
-    else if(eq.lhs().type().id() != ID_pointer &&
-       has_string_subtype(eq.lhs().type()))
+    else if(
+      eq.lhs().type().id() != ID_pointer &&
+      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

@@ -19,6 +19,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "irep.h"
 
+#include <functional>
+
 class exprt;
 class symbol_exprt;
 class update_exprt;
@@ -44,6 +46,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);
 

unit/Makefile

@@ -38,13 +38,13 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
        solvers/refinement/string_refinement/concretize_array.cpp \
        solvers/refinement/string_refinement/dependency_graph.cpp \
-       solvers/refinement/string_refinement/has_subtype.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/string_symbol_resolution.cpp \
        solvers/refinement/string_refinement/sparse_array.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \
+       util/has_subtype.cpp \
        util/irep.cpp \
        util/irep_sharing.cpp \
        util/message.cpp \

unit/solvers/refinement/string_refinement/has_subtype.cpp renamed to unit/util/has_subtype.cpp

@@ -1,7 +1,6 @@
 /*******************************************************************\
 
- Module: Unit tests for has_subtype in
-   solvers/refinement/string_refinement.cpp
+ Module: Unit tests for has_subtype in expr_util.cpp
 
  Author: Diffblue Ltd.
 
@@ -10,7 +9,10 @@
 #include <testing-utils/catch.hpp>
 
 #include <util/c_types.h>
-#include <solvers/refinement/string_refinement.h>
+#include <util/expr_util.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
 #include <java_bytecode/java_types.h>
 
 // Curryfied version of type comparison.
@@ -23,12 +25,15 @@ static std::function<bool(const typet &)> is_type(const typet &t1)
 
 SCENARIO("has_subtype", "[core][solvers][refinement][string_refinement]")
 {
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
   const typet char_type = java_char_type();
   const typet int_type = java_int_type();
   const typet bool_type = java_boolean_type();
 
-  REQUIRE(has_subtype(char_type, is_type(char_type)));
-  REQUIRE_FALSE(has_subtype(char_type, is_type(int_type)));
+  REQUIRE(has_subtype(char_type, is_type(char_type), ns));
+  REQUIRE_FALSE(has_subtype(char_type, is_type(int_type), ns));
 
   GIVEN("a struct with char and int fields")
   {
@@ -37,12 +42,12 @@ SCENARIO("has_subtype", "[core][solvers][refinement][string_refinement]")
     struct_type.components().emplace_back("int_field", int_type);
     THEN("char and int are subtypes")
     {
-      REQUIRE(has_subtype(struct_type, is_type(char_type)));
-      REQUIRE(has_subtype(struct_type, is_type(int_type)));
+      REQUIRE(has_subtype(struct_type, is_type(char_type), ns));
+      REQUIRE(has_subtype(struct_type, is_type(int_type), ns));
     }
     THEN("bool is not a subtype")
     {
-      REQUIRE_FALSE(has_subtype(struct_type, is_type(bool_type)));
+      REQUIRE_FALSE(has_subtype(struct_type, is_type(bool_type), ns));
     }
   }
 
@@ -51,11 +56,11 @@ SCENARIO("has_subtype", "[core][solvers][refinement][string_refinement]")
     pointer_typet ptr_type = pointer_type(char_type);
     THEN("char is a subtype")
     {
-      REQUIRE(has_subtype(ptr_type, is_type(char_type)));
+      REQUIRE(has_subtype(ptr_type, is_type(char_type), ns));
     }
     THEN("int is not a subtype")
     {
-      REQUIRE_FALSE(has_subtype(ptr_type, is_type(int_type)));
+      REQUIRE_FALSE(has_subtype(ptr_type, is_type(int_type), ns));
     }
   }
 }