Skip to content

Commit 1cebd76

Browse files
Avoid infinite recursion in has_subtype
Type containing themselves, through pointers for instance, could lead to infinite recursions in this function. We solve the porblem by keeping track of the visited types.
1 parent d229ad9 commit 1cebd76

File tree

1 file changed

+28
-20
lines changed

1 file changed

+28
-20
lines changed

src/util/expr_util.cpp

+28-20
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99

10+
#include <unordered_set>
1011
#include "expr_util.h"
1112

1213
#include "expr.h"
@@ -140,28 +141,35 @@ bool has_subtype(
140141
const std::function<bool(const typet &)> &pred,
141142
const namespacet &ns)
142143
{
143-
if(pred(type))
144-
return true;
145-
else if(type.id() == ID_symbol)
146-
return has_subtype(ns.follow(type), pred, ns);
147-
else if(type.id() == ID_c_enum_tag)
148-
return has_subtype(ns.follow_tag(to_c_enum_tag_type(type)), pred, ns);
149-
else if(type.id() == ID_struct || type.id() == ID_union)
150-
{
151-
const struct_union_typet &struct_union_type = to_struct_union_type(type);
144+
std::vector<typet> stack(1, type);
145+
std::unordered_set<typet, irep_hash> visited;
152146

153-
for(const auto &comp : struct_union_type.components())
154-
if(has_subtype(comp.type(), pred, ns))
155-
return true;
156-
}
157-
// do not look into pointer subtypes as this could cause unbounded recursion
158-
else if(type.id() == ID_array || type.id() == ID_vector)
159-
return has_subtype(type.subtype(), pred, ns);
160-
else if(type.has_subtypes())
147+
const auto push_if_not_visited = [&](const typet &t) {
148+
if(!visited.insert(t).second)
149+
stack.push_back(t);
150+
};
151+
152+
while(!stack.empty())
161153
{
162-
for(const auto &subtype : type.subtypes())
163-
if(has_subtype(subtype, pred, ns))
164-
return true;
154+
const typet &top= stack.back();
155+
stack.pop_back();
156+
157+
if(pred(top))
158+
return true;
159+
else if(top.id() == ID_symbol && !visited.insert(top).second)
160+
push_if_not_visited(ns.follow(top));
161+
else if(top.id() == ID_c_enum_tag)
162+
push_if_not_visited(to_c_enum_tag_type(top));
163+
else if(top.id() == ID_struct || top.id() == ID_union)
164+
{
165+
for(const auto &comp : to_struct_union_type(top).components())
166+
push_if_not_visited(comp.type());
167+
}
168+
else if(top.has_subtypes())
169+
{
170+
for(const auto &subtype : top.subtypes())
171+
push_if_not_visited(subtype);
172+
}
165173
}
166174

167175
return false;

0 commit comments

Comments
 (0)