CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
find_symbols.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "find_symbols.h"
10
11#include "c_types.h"
12#include "std_expr.h"
13
15enum class symbol_kindt
16{
18 F_TYPE,
23 F_EXPR,
27 F_ALL
28};
29
33static bool find_symbols(
35 const typet &,
36 std::function<bool(const symbol_exprt &)>,
37 std::unordered_set<irep_idt> &bindings,
38 const std::vector<irep_idt> &subs_to_find);
39
40static bool find_symbols(
41 symbol_kindt kind,
42 const exprt &src,
43 std::function<bool(const symbol_exprt &)> op,
44 std::unordered_set<irep_idt> &bindings,
45 const std::vector<irep_idt> &subs_to_find)
46{
48 {
49 if(src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
50 {
51 const auto &binding_expr = to_binding_expr(src);
52 std::unordered_set<irep_idt> new_bindings{bindings};
53 for(const auto &v : binding_expr.variables())
54 new_bindings.insert(v.get_identifier());
55
56 if(!find_symbols(
57 kind, binding_expr.where(), op, new_bindings, subs_to_find))
58 return false;
59
60 return find_symbols(
61 kind, binding_expr.type(), op, bindings, subs_to_find);
62 }
63 else if(src.id() == ID_let)
64 {
65 const auto &let_expr = to_let_expr(src);
66 std::unordered_set<irep_idt> new_bindings{bindings};
67 for(const auto &v : let_expr.variables())
68 new_bindings.insert(v.get_identifier());
69
70 if(!find_symbols(kind, let_expr.where(), op, new_bindings, subs_to_find))
71 return false;
72
73 if(!find_symbols(kind, let_expr.op1(), op, new_bindings, subs_to_find))
74 return false;
75
76 return find_symbols(kind, let_expr.type(), op, bindings, subs_to_find);
77 }
78 }
79
80 for(const auto &src_op : src.operands())
81 {
82 if(!find_symbols(kind, src_op, op, bindings, subs_to_find))
83 return false;
84 }
85
86 // Go over all named subs with id in subs_to_find
87 // and find symbols recursively.
88 for(const auto &sub_to_find : subs_to_find)
89 {
90 auto sub_expr = static_cast<const exprt &>(src.find(sub_to_find));
91 if(sub_expr.is_not_nil())
92 {
93 for(const auto &sub_op : sub_expr.operands())
94 {
95 if(!find_symbols(kind, sub_op, op, bindings, subs_to_find))
96 return false;
97 }
98 }
99 }
100
101 if(!find_symbols(kind, src.type(), op, bindings, subs_to_find))
102 return false;
103
104 if(src.id() == ID_symbol)
105 {
106 const symbol_exprt &s = to_symbol_expr(src);
107
108 if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR)
109 {
110 if(!op(s))
111 return false;
112 }
113 else if(kind == symbol_kindt::F_EXPR_FREE)
114 {
115 if(bindings.find(s.get_identifier()) == bindings.end() && !op(s))
116 return false;
117 }
118 }
119
121
122 if(
123 c_sizeof_type.is_not_nil() && !find_symbols(
124 kind,
125 static_cast<const typet &>(c_sizeof_type),
126 op,
127 bindings,
129 {
130 return false;
131 }
132
134
135 if(
136 va_arg_type.is_not_nil() && !find_symbols(
137 kind,
138 static_cast<const typet &>(va_arg_type),
139 op,
140 bindings,
142 {
143 return false;
144 }
145
146 return true;
147}
148
152static bool find_symbols(
153 symbol_kindt kind,
154 const typet &src,
155 std::function<bool(const symbol_exprt &)> op,
156 std::unordered_set<irep_idt> &bindings,
157 const std::vector<irep_idt> &subs_to_find)
158{
159 if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
160 {
161 if(
162 src.has_subtype() &&
164 kind, to_type_with_subtype(src).subtype(), op, bindings, subs_to_find))
165 {
166 return false;
167 }
168
169 for(const typet &subtype : to_type_with_subtypes(src).subtypes())
170 {
171 if(!find_symbols(kind, subtype, op, bindings, subs_to_find))
172 return false;
173 }
174
175 if(
177 kind == symbol_kindt::F_ALL)
178 {
179 const irep_idt &typedef_name = src.get(ID_C_typedef);
180 if(!typedef_name.empty() && !op(symbol_exprt{typedef_name, typet{}}))
181 return false;
182 }
183 }
184
185 if(src.id()==ID_struct ||
186 src.id()==ID_union)
187 {
189
190 for(const auto &c : struct_union_type.components())
191 {
192 if(!find_symbols(kind, c, op, bindings, subs_to_find))
193 return false;
194 }
195 }
196 else if(src.id()==ID_code)
197 {
199 if(!find_symbols(kind, code_type.return_type(), op, bindings, subs_to_find))
200 return false;
201
202 for(const auto &p : code_type.parameters())
203 {
204 if(!find_symbols(kind, p, op, bindings, subs_to_find))
205 return false;
206 }
207 }
208 else if(src.id()==ID_array)
209 {
210 // do the size -- the subtype is already done
211 if(!find_symbols(
212 kind, to_array_type(src).size(), op, bindings, subs_to_find))
213 return false;
214 }
215 else if(
217 kind == symbol_kindt::F_ALL)
218 {
219 if(src.id() == ID_c_enum_tag)
220 {
221 if(!op(symbol_exprt{to_c_enum_tag_type(src).get_identifier(), typet{}}))
222 return false;
223 }
224 else if(src.id() == ID_struct_tag)
225 {
226 if(!op(symbol_exprt{to_struct_tag_type(src).get_identifier(), typet{}}))
227 return false;
228 }
229 else if(src.id() == ID_union_tag)
230 {
231 if(!op(symbol_exprt{to_union_tag_type(src).get_identifier(), typet{}}))
232 return false;
233 }
234 }
235
236 return true;
237}
238
239static bool find_symbols(
240 symbol_kindt kind,
241 const typet &type,
242 std::function<bool(const symbol_exprt &)> op,
243 const std::vector<irep_idt> &subs_to_find = {})
244{
245 std::unordered_set<irep_idt> bindings;
246 return find_symbols(kind, type, op, bindings, subs_to_find);
247}
248
249static bool find_symbols(
250 symbol_kindt kind,
251 const exprt &src,
252 std::function<bool(const symbol_exprt &)> op,
253 const std::vector<irep_idt> &subs_to_find = {})
254{
255 std::unordered_set<irep_idt> bindings;
256 return find_symbols(kind, src, op, bindings, subs_to_find);
257}
258
259void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
260{
261 find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
262 dest.insert(e);
263 return true;
264 });
265}
266
268 const exprt &src,
269 const irep_idt &identifier,
271{
272 return !find_symbols(
274 src,
275 [&identifier](const symbol_exprt &e) {
276 return e.get_identifier() != identifier;
277 });
278}
279
281{
282 find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
283 dest.insert(e.get_identifier());
284 return true;
285 });
286}
287
289{
290 find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
291 dest.insert(e.get_identifier());
292 return true;
293 });
294}
295
297 const exprt &src,
298 find_symbols_sett &dest)
299{
301 symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
302 dest.insert(e.get_identifier());
303 return true;
304 });
305}
306
308 const typet &src,
309 find_symbols_sett &dest)
310{
312 symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
313 dest.insert(e.get_identifier());
314 return true;
315 });
316}
317
319 const exprt &src,
320 find_symbols_sett &dest,
321 const std::vector<irep_idt> &subs_to_find)
322{
325 src,
326 [&dest](const symbol_exprt &e) {
327 dest.insert(e.get_identifier());
328 return true;
329 },
331}
332
334 const typet &src,
335 find_symbols_sett &dest,
336 const std::vector<irep_idt> &subs_to_find)
337{
340 src,
341 [&dest](const symbol_exprt &e) {
342 dest.insert(e.get_identifier());
343 return true;
344 },
346}
347
348void find_symbols(const exprt &src, find_symbols_sett &dest)
349{
350 find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
351 dest.insert(e.get_identifier());
352 return true;
353 });
354}
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base type of functions.
Definition std_types.h:583
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
Base type for structs and unions.
Definition std_types.h:62
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
The type of an expression, extends irept.
Definition type.h:29
bool has_subtype() const
Definition type.h:64
symbol_kindt
Kinds of symbols to be considered by find_symbols.
@ F_ALL
All of the above.
@ F_TYPE_NON_PTR
Struct, union, or enum tag symbols when the expression using them is not a pointer.
@ F_TYPE
Struct, union, or enum tag symbols.
@ F_EXPR_FREE
Symbol expressions, but excluding bound variables.
@ F_EXPR
Symbol expressions.
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
Collect type tags contained in src when the expression of such a type is not a pointer,...
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
Collect all type tags contained in src and add them to dest.
bool has_symbol_expr(const exprt &src, const irep_idt &identifier, bool include_bound_symbols)
Returns true if one of the symbol expressions in src has identifier identifier; if include_bound_symb...
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
std::unordered_set< irep_idt > find_symbols_sett
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3455
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:3303
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:252
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208