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 "std_types.h"
12 #include "std_expr.h"
13 
15 
17  const exprt &src,
18  find_symbols_sett &dest)
19 {
20  find_symbols(src, dest, true, true);
21 }
22 
24  const exprt &src,
25  find_symbols_sett &dest,
26  bool current,
27  bool next)
28 {
29  if(src.id() == ID_symbol && current)
30  dest.insert(to_symbol_expr(src).get_identifier());
31  else if(src.id() == ID_next_symbol && next)
32  dest.insert(src.get(ID_identifier));
33  else
34  {
35  forall_operands(it, src)
36  find_symbols(*it, dest, current, next);
37  }
38 }
39 
41  const exprt &src,
42  const find_symbols_sett &symbols,
43  bool current,
44  bool next)
45 {
46  if(src.id() == ID_symbol && current)
47  return symbols.count(to_symbol_expr(src).get_identifier()) != 0;
48  else if(src.id() == ID_next_symbol && next)
49  return symbols.count(src.get(ID_identifier))!=0;
50  else
51  {
52  forall_operands(it, src)
53  if(has_symbol(*it, symbols, current, next))
54  return true;
55  }
56 
57  return false;
58 }
59 
61  const exprt &src,
62  const find_symbols_sett &symbols)
63 {
64  return has_symbol(src, symbols, true, true);
65 }
66 
68  const exprt &src,
69  std::set<exprt> &dest)
70 {
71  if(src.id()==ID_symbol || src.id()==ID_next_symbol)
72  dest.insert(src);
73  else
74  {
75  forall_operands(it, src)
76  find_symbols(*it, dest);
77  }
78 }
79 
81  const exprt &src,
82  std::set<symbol_exprt> &dest)
83 {
84  if(src.id()==ID_symbol)
85  dest.insert(to_symbol_expr(src));
86  else
87  {
88  forall_operands(it, src)
89  find_symbols(*it, dest);
90  }
91 }
92 
93 void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest);
94 
95 void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)
96 {
97  forall_operands(it, src)
98  find_symbols(kind, *it, dest);
99 
100  find_symbols(kind, src.type(), dest);
101 
102  if(kind==kindt::F_BOTH || kind==kindt::F_EXPR)
103  {
104  if(src.id() == ID_symbol)
105  dest.insert(to_symbol_expr(src).get_identifier());
106  else if(src.id() == ID_next_symbol)
107  dest.insert(src.get(ID_identifier));
108  }
109 
110  const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
111 
112  if(c_sizeof_type.is_not_nil())
113  find_symbols(kind, static_cast<const typet &>(c_sizeof_type), dest);
114 
115  const irept &va_arg_type=src.find(ID_C_va_arg_type);
116 
117  if(va_arg_type.is_not_nil())
118  find_symbols(kind, static_cast<const typet &>(va_arg_type), dest);
119 }
120 
121 void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
122 {
123  if(kind!=kindt::F_TYPE_NON_PTR ||
124  src.id()!=ID_pointer)
125  {
126  if(src.has_subtype())
127  find_symbols(kind, src.subtype(), dest);
128 
129  forall_subtypes(it, src)
130  find_symbols(kind, *it, dest);
131 
132  const irep_idt &typedef_name=src.get(ID_C_typedef);
133  if(!typedef_name.empty())
134  dest.insert(typedef_name);
135  }
136 
137  if(src.id()==ID_struct ||
138  src.id()==ID_union)
139  {
140  const struct_union_typet &struct_union_type=to_struct_union_type(src);
141  const struct_union_typet::componentst &components=
142  struct_union_type.components();
143 
144  for(struct_union_typet::componentst::const_iterator
145  it=components.begin();
146  it!=components.end();
147  it++)
148  find_symbols(kind, *it, dest);
149  }
150  else if(src.id()==ID_code)
151  {
152  const code_typet &code_type=to_code_type(src);
153  find_symbols(kind, code_type.return_type(), dest);
154  const code_typet::parameterst &parameters=code_type.parameters();
155 
156  for(code_typet::parameterst::const_iterator
157  it=parameters.begin();
158  it!=parameters.end();
159  it++)
160  {
161  find_symbols(kind, *it, dest);
162 
163  // irep_idt identifier=it->get_identifier();
164  // if(!identifier.empty() && (kind==F_TYPE || kind==F_BOTH))
165  // dest.insert(identifier);
166  }
167  }
168  else if(src.id()==ID_symbol)
169  dest.insert(to_symbol_type(src).get_identifier());
170  else if(src.id()==ID_array)
171  {
172  // do the size -- the subtype is already done
173  find_symbols(kind, to_array_type(src).size(), dest);
174  }
175  else if(src.id()==ID_c_enum_tag)
176  {
177  dest.insert(to_c_enum_tag_type(src).get_identifier());
178  }
179  else if(src.id()==ID_struct_tag)
180  {
181  dest.insert(to_struct_tag_type(src).get_identifier());
182  }
183  else if(src.id()==ID_union_tag)
184  {
185  dest.insert(to_union_tag_type(src).get_identifier());
186  }
187 }
188 
190 {
191  find_symbols(kindt::F_TYPE, src, dest);
192 }
193 
195 {
196  find_symbols(kindt::F_TYPE, src, dest);
197 }
198 
200  const exprt &src,
201  find_symbols_sett &dest)
202 {
204 }
205 
207  const typet &src,
208  find_symbols_sett &dest)
209 {
211 }
212 
214 {
215  find_symbols(kindt::F_BOTH, src, dest);
216 }
217 
219 {
220  find_symbols(kindt::F_BOTH, src, dest);
221 }
The type of an expression.
Definition: type.h:22
#define forall_subtypes(it, type)
Definition: type.h:161
Base type of functions.
Definition: std_types.h:764
bool is_not_nil() const
Definition: irep.h:103
bool has_subtype() const
Definition: type.h:79
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
std::vector< componentt > componentst
Definition: std_types.h:243
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
std::vector< parametert > parameterst
Definition: std_types.h:767
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
kindt
const irep_idt & id() const
Definition: irep.h:189
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:603
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:566
Base class for tree-like data structures with sharing.
Definition: irep.h:86
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:747
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
API to type classes.
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
const typet & subtype() const
Definition: type.h:33
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void find_symbols(const exprt &src, find_symbols_sett &dest)
const typet & return_type() const
Definition: std_types.h:895