cprover
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 "expr_iterator.h"
13 #include "range.h"
14 #include "std_expr.h"
15 #include "std_types.h"
16 
17 enum class kindt { F_TYPE, F_TYPE_NON_PTR, F_EXPR, F_BOTH };
18 
20 {
21  find_symbols(src, dest, true, true);
22 }
23 
25  const exprt &src,
26  find_symbols_sett &dest,
27  bool current,
28  bool next)
29 {
30  src.visit_pre([&dest, current, next](const exprt &e) {
31  if(e.id() == ID_symbol && current)
32  dest.insert(to_symbol_expr(e).get_identifier());
33  else if(e.id() == ID_next_symbol && next)
34  dest.insert(e.get(ID_identifier));
35  });
36 }
37 
39  const exprt &src,
40  const find_symbols_sett &symbols,
41  bool current,
42  bool next)
43 {
44  if(src.id() == ID_symbol && current)
45  return symbols.count(to_symbol_expr(src).get_identifier()) != 0;
46  else if(src.id() == ID_next_symbol && next)
47  return symbols.count(src.get(ID_identifier))!=0;
48  else
49  {
50  forall_operands(it, src)
51  if(has_symbol(*it, symbols, current, next))
52  return true;
53  }
54 
55  return false;
56 }
57 
59  const exprt &src,
60  const find_symbols_sett &symbols)
61 {
62  return has_symbol(src, symbols, true, true);
63 }
64 
66  const exprt &src,
67  std::set<symbol_exprt> &dest)
68 {
69  src.visit_pre([&dest](const exprt &e) {
70  if(e.id() == ID_symbol)
71  dest.insert(to_symbol_expr(e));
72  });
73 }
74 
75 std::set<symbol_exprt> find_symbols(const exprt &src)
76 {
77  return make_range(src.depth_begin(), src.depth_end())
78  .filter([](const exprt &e) { return e.id() == ID_symbol; })
79  .map([](const exprt &e) { return to_symbol_expr(e); });
80 }
81 
82 std::unordered_set<irep_idt> find_symbol_identifiers(const exprt &src)
83 {
84  std::unordered_set<irep_idt> result;
85  src.visit_pre([&](const exprt &e) {
86  if(e.id() == ID_symbol)
87  result.insert(to_symbol_expr(e).get_identifier());
88  });
89  return result;
90 }
91 
92 void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest);
93 
94 void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)
95 {
96  forall_operands(it, src)
97  find_symbols(kind, *it, dest);
98 
99  find_symbols(kind, src.type(), dest);
100 
101  if(kind==kindt::F_BOTH || kind==kindt::F_EXPR)
102  {
103  if(src.id() == ID_symbol)
104  dest.insert(to_symbol_expr(src).get_identifier());
105  else if(src.id() == ID_next_symbol)
106  dest.insert(src.get(ID_identifier));
107  }
108 
109  const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
110 
111  if(c_sizeof_type.is_not_nil())
112  find_symbols(kind, static_cast<const typet &>(c_sizeof_type), dest);
113 
114  const irept &va_arg_type=src.find(ID_C_va_arg_type);
115 
116  if(va_arg_type.is_not_nil())
117  find_symbols(kind, static_cast<const typet &>(va_arg_type), dest);
118 }
119 
120 void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
121 {
122  if(kind!=kindt::F_TYPE_NON_PTR ||
123  src.id()!=ID_pointer)
124  {
125  if(src.has_subtype())
126  find_symbols(kind, to_type_with_subtype(src).subtype(), dest);
127 
128  for(const typet &subtype : to_type_with_subtypes(src).subtypes())
129  find_symbols(kind, subtype, dest);
130 
131  const irep_idt &typedef_name=src.get(ID_C_typedef);
132  if(!typedef_name.empty())
133  dest.insert(typedef_name);
134  }
135 
136  if(src.id()==ID_struct ||
137  src.id()==ID_union)
138  {
139  const struct_union_typet &struct_union_type=to_struct_union_type(src);
140 
141  for(const auto &c : struct_union_type.components())
142  find_symbols(kind, c, dest);
143  }
144  else if(src.id()==ID_code)
145  {
146  const code_typet &code_type=to_code_type(src);
147  find_symbols(kind, code_type.return_type(), dest);
148 
149  for(const auto &p : code_type.parameters())
150  {
151  find_symbols(kind, p, dest);
152 
153  // irep_idt identifier=it->get_identifier();
154  // if(!identifier.empty() && (kind==F_TYPE || kind==F_BOTH))
155  // dest.insert(identifier);
156  }
157  }
158  else if(src.id()==ID_array)
159  {
160  // do the size -- the subtype is already done
161  find_symbols(kind, to_array_type(src).size(), dest);
162  }
163  else if(src.id()==ID_c_enum_tag)
164  {
165  dest.insert(to_c_enum_tag_type(src).get_identifier());
166  }
167  else if(src.id()==ID_struct_tag)
168  {
169  dest.insert(to_struct_tag_type(src).get_identifier());
170  }
171  else if(src.id()==ID_union_tag)
172  {
173  dest.insert(to_union_tag_type(src).get_identifier());
174  }
175 }
176 
178 {
179  find_symbols(kindt::F_TYPE, src, dest);
180 }
181 
183 {
184  find_symbols(kindt::F_TYPE, src, dest);
185 }
186 
188  const exprt &src,
189  find_symbols_sett &dest)
190 {
191  find_symbols(kindt::F_TYPE_NON_PTR, src, dest);
192 }
193 
195  const typet &src,
196  find_symbols_sett &dest)
197 {
198  find_symbols(kindt::F_TYPE_NON_PTR, src, dest);
199 }
200 
202 {
203  find_symbols(kindt::F_BOTH, src, dest);
204 }
205 
207 {
208  find_symbols(kindt::F_BOTH, src, dest);
209 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
find_type_and_expr_symbols
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:201
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:292
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:208
typet
The type of an expression, extends irept.
Definition: type.h:28
find_symbols_or_nexts
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
Definition: find_symbols.cpp:19
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
find_non_pointer_type_symbols
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:187
find_symbol_identifiers
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
Definition: find_symbols.cpp:82
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:154
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
exprt
Base class for all expressions.
Definition: expr.h:54
kindt
kindt
Definition: find_symbols.cpp:17
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
find_symbols.h
to_c_enum_tag_type
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:317
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
std_types.h
Pre-defined types.
find_type_symbols
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:177
kindt::F_TYPE
@ F_TYPE
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:533
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
dstringt::empty
bool empty() const
Definition: dstring.h:88
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
Definition: find_symbols.cpp:24
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
has_symbol
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
Definition: find_symbols.cpp:38
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:272
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:294
std_expr.h
API to expression classes.
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
c_types.h