cprover
Loading...
Searching...
No Matches
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
30static bool find_symbols(
32 const typet &,
33 std::function<bool(const symbol_exprt &)>,
34 std::unordered_set<irep_idt> &bindings);
35
36static bool find_symbols(
37 symbol_kindt kind,
38 const exprt &src,
39 std::function<bool(const symbol_exprt &)> op,
40 std::unordered_set<irep_idt> &bindings)
41{
43 {
44 if(src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
45 {
46 const auto &binding_expr = to_binding_expr(src);
47 std::unordered_set<irep_idt> new_bindings{bindings};
48 for(const auto &v : binding_expr.variables())
49 new_bindings.insert(v.get_identifier());
50
51 if(!find_symbols(kind, binding_expr.where(), op, new_bindings))
52 return false;
53
54 return find_symbols(kind, binding_expr.type(), op, bindings);
55 }
56 else if(src.id() == ID_let)
57 {
58 const auto &let_expr = to_let_expr(src);
59 std::unordered_set<irep_idt> new_bindings{bindings};
60 for(const auto &v : let_expr.variables())
61 new_bindings.insert(v.get_identifier());
62
63 if(!find_symbols(kind, let_expr.where(), op, new_bindings))
64 return false;
65
66 if(!find_symbols(kind, let_expr.op1(), op, new_bindings))
67 return false;
68
69 return find_symbols(kind, let_expr.type(), op, bindings);
70 }
71 }
72
73 for(const auto &src_op : src.operands())
74 {
75 if(!find_symbols(kind, src_op, op, bindings))
76 return false;
77 }
78
79 if(!find_symbols(kind, src.type(), op, bindings))
80 return false;
81
82 if(src.id() == ID_symbol)
83 {
84 const symbol_exprt &s = to_symbol_expr(src);
85
86 if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR)
87 {
88 if(!op(s))
89 return false;
90 }
91 else if(kind == symbol_kindt::F_EXPR_FREE)
92 {
93 if(bindings.find(s.get_identifier()) == bindings.end() && !op(s))
94 return false;
95 }
96 }
97
99
100 if(
101 c_sizeof_type.is_not_nil() &&
103 kind, static_cast<const typet &>(c_sizeof_type), op, bindings))
104 {
105 return false;
106 }
107
109
110 if(
111 va_arg_type.is_not_nil() &&
112 !find_symbols(kind, static_cast<const typet &>(va_arg_type), op, bindings))
113 {
114 return false;
115 }
116
117 return true;
118}
119
120static bool find_symbols(
121 symbol_kindt kind,
122 const typet &src,
123 std::function<bool(const symbol_exprt &)> op,
124 std::unordered_set<irep_idt> &bindings)
125{
126 if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
127 {
128 if(
129 src.has_subtype() &&
130 !find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings))
131 {
132 return false;
133 }
134
135 for(const typet &subtype : to_type_with_subtypes(src).subtypes())
136 {
137 if(!find_symbols(kind, subtype, op, bindings))
138 return false;
139 }
140
141 if(
143 kind == symbol_kindt::F_ALL)
144 {
145 const irep_idt &typedef_name = src.get(ID_C_typedef);
146 if(!typedef_name.empty() && !op(symbol_exprt{typedef_name, typet{}}))
147 return false;
148 }
149 }
150
151 if(src.id()==ID_struct ||
152 src.id()==ID_union)
153 {
155
156 for(const auto &c : struct_union_type.components())
157 {
158 if(!find_symbols(kind, c, op, bindings))
159 return false;
160 }
161 }
162 else if(src.id()==ID_code)
163 {
165 if(!find_symbols(kind, code_type.return_type(), op, bindings))
166 return false;
167
168 for(const auto &p : code_type.parameters())
169 {
170 if(!find_symbols(kind, p, op, bindings))
171 return false;
172 }
173 }
174 else if(src.id()==ID_array)
175 {
176 // do the size -- the subtype is already done
177 if(!find_symbols(kind, to_array_type(src).size(), op, bindings))
178 return false;
179 }
180 else if(
182 kind == symbol_kindt::F_ALL)
183 {
184 if(src.id() == ID_c_enum_tag)
185 {
186 if(!op(symbol_exprt{to_c_enum_tag_type(src).get_identifier(), typet{}}))
187 return false;
188 }
189 else if(src.id() == ID_struct_tag)
190 {
191 if(!op(symbol_exprt{to_struct_tag_type(src).get_identifier(), typet{}}))
192 return false;
193 }
194 else if(src.id() == ID_union_tag)
195 {
196 if(!op(symbol_exprt{to_union_tag_type(src).get_identifier(), typet{}}))
197 return false;
198 }
199 }
200
201 return true;
202}
203
204static bool find_symbols(
205 symbol_kindt kind,
206 const typet &type,
207 std::function<bool(const symbol_exprt &)> op)
208{
209 std::unordered_set<irep_idt> bindings;
210 return find_symbols(kind, type, op, bindings);
211}
212
213static bool find_symbols(
214 symbol_kindt kind,
215 const exprt &src,
216 std::function<bool(const symbol_exprt &)> op)
217{
218 std::unordered_set<irep_idt> bindings;
219 return find_symbols(kind, src, op, bindings);
220}
221
222void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
223{
224 find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
225 dest.insert(e);
226 return true;
227 });
228}
229
231 const exprt &src,
232 const irep_idt &identifier,
234{
235 return !find_symbols(
237 src,
238 [&identifier](const symbol_exprt &e) {
239 return e.get_identifier() != identifier;
240 });
241}
242
244{
245 find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
246 dest.insert(e.get_identifier());
247 return true;
248 });
249}
250
252{
253 find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
254 dest.insert(e.get_identifier());
255 return true;
256 });
257}
258
260 const exprt &src,
261 find_symbols_sett &dest)
262{
264 symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
265 dest.insert(e.get_identifier());
266 return true;
267 });
268}
269
271 const typet &src,
272 find_symbols_sett &dest)
273{
275 symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
276 dest.insert(e.get_identifier());
277 return true;
278 });
279}
280
282{
283 find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
284 dest.insert(e.get_identifier());
285 return true;
286 });
287}
288
290{
291 find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
292 dest.insert(e.get_identifier());
293 return true;
294 });
295}
296
297void find_symbols(const exprt &src, find_symbols_sett &dest)
298{
299 find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
300 dest.insert(e.get_identifier());
301 return true;
302 });
303}
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:563
Base type of functions.
Definition std_types.h:539
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool empty() const
Definition dstring.h:90
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:372
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:396
Base type for structs and unions.
Definition std_types.h:62
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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)
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables,...
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...
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:3273
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:3121
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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:219
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175