CBMC
find_symbols.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
15 enum class symbol_kindt
16 {
18  F_TYPE,
23  F_EXPR,
27  F_ALL
28 };
29 
33 static 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 
40 static 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 {
47  if(kind == symbol_kindt::F_EXPR_FREE)
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 
120  const irept &c_sizeof_type = src.find(ID_C_c_sizeof_type);
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,
128  subs_to_find))
129  {
130  return false;
131  }
132 
133  const irept &va_arg_type=src.find(ID_C_va_arg_type);
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,
141  subs_to_find))
142  {
143  return false;
144  }
145 
146  return true;
147 }
148 
152 static 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() &&
163  !find_symbols(
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  {
188  const struct_union_typet &struct_union_type=to_struct_union_type(src);
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  {
198  const code_typet &code_type=to_code_type(src);
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  {
222  return false;
223  }
224  else if(src.id() == ID_struct_tag)
225  {
227  return false;
228  }
229  else if(src.id() == ID_union_tag)
230  {
232  return false;
233  }
234  }
235 
236  return true;
237 }
238 
239 static 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 
249 static 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 
259 void 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,
270  bool include_bound_symbols)
271 {
272  return !find_symbols(
273  include_bound_symbols ? symbol_kindt::F_EXPR : symbol_kindt::F_EXPR_FREE,
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 {
300  find_symbols(
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 {
311  find_symbols(
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 {
323  find_symbols(
325  src,
326  [&dest](const symbol_exprt &e) {
327  dest.insert(e.get_identifier());
328  return true;
329  },
330  subs_to_find);
331 }
332 
334  const typet &src,
335  find_symbols_sett &dest,
336  const std::vector<irep_idt> &subs_to_find)
337 {
338  find_symbols(
340  src,
341  [&dest](const symbol_exprt &e) {
342  dest.insert(e.get_identifier());
343  return true;
344  },
345  subs_to_find);
346 }
347 
348 void 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 union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
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
Base type of functions.
Definition: std_types.h:583
const typet & return_type() const
Definition: std_types.h:689
const parameterst & parameters() const
Definition: std_types.h:699
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
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
const irep_idt & get_identifier() const
Definition: std_types.h:410
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
Definition: find_symbols.h:20
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3333
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition: std_expr.h:3181
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
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