Skip to content

Commit 8ae2d8c

Browse files
tautschnigtautschnig
committed
Make find_symbols implementations uniform
Each function used a different approach, with different potential omissions of symbols. Instead, use a single way to traverse expressions (and types), and configure the operation done via a parameter. All other (non-deprecated) functions are now just thin wrappers.
1 parent a606bd1 commit 8ae2d8c

File tree

2 files changed

+146
-83
lines changed

2 files changed

+146
-83
lines changed

‎src/util/find_symbols.cpp

Lines changed: 134 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -40,83 +40,95 @@ bool has_symbol(
4040
return has_symbol(src, symbols, true, true);
4141
}
4242

43-
void find_symbols(
44-
const exprt &src,
45-
std::set<symbol_exprt> &dest)
46-
{
47-
src.visit_pre([&dest](const exprt &e) {
48-
if(e.id() == ID_symbol)
49-
dest.insert(to_symbol_expr(e));
50-
});
51-
}
52-
53-
std::set<symbol_exprt> find_symbols(const exprt &src)
54-
{
55-
return make_range(src.depth_begin(), src.depth_end())
56-
.filter([](const exprt &e) { return e.id() == ID_symbol; })
57-
.map([](const exprt &e) { return to_symbol_expr(e); });
58-
}
43+
static bool find_symbols(
44+
kindt,
45+
const typet &,
46+
std::function<bool(const symbol_exprt &)>);
5947

60-
std::unordered_set<irep_idt> find_symbol_identifiers(const exprt &src)
61-
{
62-
std::unordered_set<irep_idt> result;
63-
src.visit_pre([&](const exprt &e) {
64-
if(e.id() == ID_symbol)
65-
result.insert(to_symbol_expr(e).get_identifier());
66-
});
67-
return result;
68-
}
69-
70-
void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest);
71-
72-
void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)
48+
static bool find_symbols(
49+
kindt kind,
50+
const exprt &src,
51+
std::function<bool(const symbol_exprt &)> op)
7352
{
7453
forall_operands(it, src)
75-
find_symbols(kind, *it, dest);
54+
{
55+
if(!find_symbols(kind, *it, op))
56+
return false;
57+
}
7658

77-
find_symbols(kind, src.type(), dest);
59+
if(!find_symbols(kind, src.type(), op))
60+
return false;
7861

7962
if(
8063
kind == kindt::F_ALL || kind == kindt::F_EXPR_CURRENT ||
8164
kind == kindt::F_EXPR_BOTH)
8265
{
83-
if(src.id() == ID_symbol)
84-
dest.insert(to_symbol_expr(src).get_identifier());
66+
if(src.id() == ID_symbol && !op(to_symbol_expr(src)))
67+
return false;
8568
}
8669

8770
if(
8871
kind == kindt::F_ALL || kind == kindt::F_EXPR_NEXT ||
8972
kind == kindt::F_EXPR_BOTH)
9073
{
91-
if(src.id() == ID_next_symbol)
92-
dest.insert(src.get(ID_identifier));
74+
if(
75+
src.id() == ID_next_symbol &&
76+
!op(symbol_exprt{src.get(ID_identifier), typet{}}))
77+
{
78+
return false;
79+
}
9380
}
9481

9582
const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
9683

97-
if(c_sizeof_type.is_not_nil())
98-
find_symbols(kind, static_cast<const typet &>(c_sizeof_type), dest);
84+
if(
85+
c_sizeof_type.is_not_nil() &&
86+
!find_symbols(kind, static_cast<const typet &>(c_sizeof_type), op))
87+
{
88+
return false;
89+
}
9990

10091
const irept &va_arg_type=src.find(ID_C_va_arg_type);
10192

102-
if(va_arg_type.is_not_nil())
103-
find_symbols(kind, static_cast<const typet &>(va_arg_type), dest);
93+
if(
94+
va_arg_type.is_not_nil() &&
95+
!find_symbols(kind, static_cast<const typet &>(va_arg_type), op))
96+
{
97+
return false;
98+
}
99+
100+
return true;
104101
}
105102

106-
void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
103+
static bool find_symbols(
104+
kindt kind,
105+
const typet &src,
106+
std::function<bool(const symbol_exprt &)> op)
107107
{
108108
if(kind!=kindt::F_TYPE_NON_PTR ||
109109
src.id()!=ID_pointer)
110110
{
111-
if(src.has_subtype())
112-
find_symbols(kind, to_type_with_subtype(src).subtype(), dest);
111+
if(
112+
src.has_subtype() &&
113+
!find_symbols(kind, to_type_with_subtype(src).subtype(), op))
114+
{
115+
return false;
116+
}
113117

114118
for(const typet &subtype : to_type_with_subtypes(src).subtypes())
115-
find_symbols(kind, subtype, dest);
119+
{
120+
if(!find_symbols(kind, subtype, op))
121+
return false;
122+
}
116123

117-
const irep_idt &typedef_name=src.get(ID_C_typedef);
118-
if(!typedef_name.empty())
119-
dest.insert(typedef_name);
124+
if(
125+
kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR ||
126+
kind == kindt::F_ALL)
127+
{
128+
const irep_idt &typedef_name = src.get(ID_C_typedef);
129+
if(!typedef_name.empty() && !op(symbol_exprt{typedef_name, typet{}}))
130+
return false;
131+
}
120132
}
121133

122134
if(src.id()==ID_struct ||
@@ -125,81 +137,126 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
125137
const struct_union_typet &struct_union_type=to_struct_union_type(src);
126138

127139
for(const auto &c : struct_union_type.components())
128-
find_symbols(kind, c, dest);
140+
{
141+
if(!find_symbols(kind, c, op))
142+
return false;
143+
}
129144
}
130145
else if(src.id()==ID_code)
131146
{
132147
const code_typet &code_type=to_code_type(src);
133-
find_symbols(kind, code_type.return_type(), dest);
148+
if(!find_symbols(kind, code_type.return_type(), op))
149+
return false;
134150

135151
for(const auto &p : code_type.parameters())
136152
{
137-
find_symbols(kind, p, dest);
153+
if(!find_symbols(kind, p, op))
154+
return false;
138155
}
139156
}
140157
else if(src.id()==ID_array)
141158
{
142159
// do the size -- the subtype is already done
143-
find_symbols(kind, to_array_type(src).size(), dest);
144-
}
145-
else if(src.id()==ID_c_enum_tag)
146-
{
147-
dest.insert(to_c_enum_tag_type(src).get_identifier());
160+
if(!find_symbols(kind, to_array_type(src).size(), op))
161+
return false;
148162
}
149-
else if(src.id()==ID_struct_tag)
163+
else if(
164+
kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR ||
165+
kind == kindt::F_ALL)
150166
{
151-
dest.insert(to_struct_tag_type(src).get_identifier());
152-
}
153-
else if(src.id()==ID_union_tag)
154-
{
155-
dest.insert(to_union_tag_type(src).get_identifier());
167+
if(src.id() == ID_c_enum_tag)
168+
{
169+
if(!op(symbol_exprt{to_c_enum_tag_type(src).get_identifier(), typet{}}))
170+
return false;
171+
}
172+
else if(src.id() == ID_struct_tag)
173+
{
174+
if(!op(symbol_exprt{to_struct_tag_type(src).get_identifier(), typet{}}))
175+
return false;
176+
}
177+
else if(src.id() == ID_union_tag)
178+
{
179+
if(!op(symbol_exprt{to_union_tag_type(src).get_identifier(), typet{}}))
180+
return false;
181+
}
156182
}
183+
184+
return true;
185+
}
186+
187+
void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
188+
{
189+
find_symbols(kindt::F_EXPR_CURRENT, src, [&dest](const symbol_exprt &e) {
190+
dest.insert(e);
191+
return true;
192+
});
157193
}
158194

159195
bool has_symbol(const exprt &src, const irep_idt &identifier, kindt kind)
160196
{
161-
find_symbols_sett tmp_dest;
162-
find_symbols(kind, src, tmp_dest);
163-
return tmp_dest.find(identifier) != tmp_dest.end();
197+
return !find_symbols(kind, src, [&identifier](const symbol_exprt &e) {
198+
return e.get_identifier() != identifier;
199+
});
164200
}
165201

166202
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
167203
{
168-
find_symbols(kindt::F_TYPE, src, dest);
204+
find_symbols(kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
205+
dest.insert(e.get_identifier());
206+
return true;
207+
});
169208
}
170209

171210
void find_type_symbols(const typet &src, find_symbols_sett &dest)
172211
{
173-
find_symbols(kindt::F_TYPE, src, dest);
212+
find_symbols(kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
213+
dest.insert(e.get_identifier());
214+
return true;
215+
});
174216
}
175217

176218
void find_non_pointer_type_symbols(
177219
const exprt &src,
178220
find_symbols_sett &dest)
179221
{
180-
find_symbols(kindt::F_TYPE_NON_PTR, src, dest);
222+
find_symbols(kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
223+
dest.insert(e.get_identifier());
224+
return true;
225+
});
181226
}
182227

183228
void find_non_pointer_type_symbols(
184229
const typet &src,
185230
find_symbols_sett &dest)
186231
{
187-
find_symbols(kindt::F_TYPE_NON_PTR, src, dest);
232+
find_symbols(kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
233+
dest.insert(e.get_identifier());
234+
return true;
235+
});
188236
}
189237

190238
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
191239
{
192-
find_symbols(kindt::F_ALL, src, dest);
240+
find_symbols(kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
241+
dest.insert(e.get_identifier());
242+
return true;
243+
});
193244
}
194245

195246
void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
196247
{
197-
find_symbols(kindt::F_ALL, src, dest);
248+
find_symbols(kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
249+
dest.insert(e.get_identifier());
250+
return true;
251+
});
198252
}
199253

200254
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
201255
{
202-
find_symbols(kindt::F_EXPR_BOTH, src, dest);
256+
find_symbols(kindt::F_EXPR_BOTH, src, [&dest](const symbol_exprt &e) {
257+
dest.insert(e.get_identifier());
258+
return true;
259+
});
203260
}
204261

205262
void find_symbols(
@@ -208,13 +265,17 @@ void find_symbols(
208265
bool current,
209266
bool next)
210267
{
268+
auto store = [&dest](const symbol_exprt &e) {
269+
dest.insert(e.get_identifier());
270+
return true;
271+
};
211272
if(current)
212273
{
213274
if(next)
214-
find_symbols(kindt::F_EXPR_BOTH, src, dest);
275+
find_symbols(kindt::F_EXPR_BOTH, src, store);
215276
else
216-
find_symbols(kindt::F_EXPR_CURRENT, src, dest);
277+
find_symbols(kindt::F_EXPR_CURRENT, src, store);
217278
}
218279
else if(next)
219-
find_symbols(kindt::F_EXPR_NEXT, src, dest);
280+
find_symbols(kindt::F_EXPR_NEXT, src, store);
220281
}

‎src/util/find_symbols.h

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -72,24 +72,26 @@ find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end)
7272
return result;
7373
}
7474

75-
/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if
76-
/// \p current is true, and ID_next_symbol if \p next is true
77-
void find_symbols(
78-
const exprt &src,
79-
find_symbols_sett &dest,
80-
bool current,
81-
bool next);
82-
8375
/// Find sub expressions with id ID_symbol
8476
void find_symbols(
8577
const exprt &src,
8678
std::set<symbol_exprt> &dest);
8779

8880
/// Find sub expressions with id ID_symbol
89-
std::set<symbol_exprt> find_symbols(const exprt &src);
81+
inline std::set<symbol_exprt> find_symbols(const exprt &src)
82+
{
83+
std::set<symbol_exprt> syms;
84+
find_symbols(src, syms);
85+
return syms;
86+
}
9087

9188
/// Find identifiers of the sub expressions with id ID_symbol
92-
std::unordered_set<irep_idt> find_symbol_identifiers(const exprt &src);
89+
inline find_symbols_sett find_symbol_identifiers(const exprt &src)
90+
{
91+
find_symbols_sett identifiers;
92+
find_symbols(src, identifiers, true, false);
93+
return identifiers;
94+
}
9395

9496
DEPRECATED(SINCE(2022, 3, 14, "use has_symbol(exprt, irep_idt, symbol_kindt)"))
9597
/// \return true if one of the symbols in \p src is present in \p symbols

0 commit comments

Comments
 (0)