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, to_type_with_subtype(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 
142  for(const auto &c : struct_union_type.components())
143  find_symbols(kind, c, dest);
144  }
145  else if(src.id()==ID_code)
146  {
147  const code_typet &code_type=to_code_type(src);
148  find_symbols(kind, code_type.return_type(), dest);
149 
150  for(const auto &p : code_type.parameters())
151  {
152  find_symbols(kind, p, dest);
153 
154  // irep_idt identifier=it->get_identifier();
155  // if(!identifier.empty() && (kind==F_TYPE || kind==F_BOTH))
156  // dest.insert(identifier);
157  }
158  }
159  else if(src.id() == ID_symbol_type)
160  dest.insert(to_symbol_type(src).get_identifier());
161  else if(src.id()==ID_array)
162  {
163  // do the size -- the subtype is already done
164  find_symbols(kind, to_array_type(src).size(), dest);
165  }
166  else if(src.id()==ID_c_enum_tag)
167  {
168  dest.insert(to_c_enum_tag_type(src).get_identifier());
169  }
170  else if(src.id()==ID_struct_tag)
171  {
172  dest.insert(to_struct_tag_type(src).get_identifier());
173  }
174  else if(src.id()==ID_union_tag)
175  {
176  dest.insert(to_union_tag_type(src).get_identifier());
177  }
178 }
179 
181 {
182  find_symbols(kindt::F_TYPE, src, dest);
183 }
184 
186 {
187  find_symbols(kindt::F_TYPE, src, dest);
188 }
189 
191  const exprt &src,
192  find_symbols_sett &dest)
193 {
195 }
196 
198  const typet &src,
199  find_symbols_sett &dest)
200 {
202 }
203 
205 {
206  find_symbols(kindt::F_BOTH, src, dest);
207 }
208 
210 {
211  find_symbols(kindt::F_BOTH, src, dest);
212 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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: std_types.h:737
typet::subtype
const typet & subtype() const
Definition: type.h:38
find_type_and_expr_symbols
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:204
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:260
typet
The type of an expression, extends irept.
Definition: type.h:27
typet::has_subtype
bool has_subtype() const
Definition: type.h:56
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:114
find_non_pointer_type_symbols
void find_non_pointer_type_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:190
kindt::F_EXPR
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:156
exprt
Base class for all expressions.
Definition: expr.h:54
kindt
kindt
Definition: find_symbols.cpp:14
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:16
find_symbols.h
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
std_types.h
find_type_symbols
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:180
kindt::F_TYPE
kindt::F_TYPE_NON_PTR
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_typet
Base type of functions.
Definition: std_types.h:751
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:543
dstringt::empty
bool empty() const
Definition: dstring.h:75
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
forall_subtypes
#define forall_subtypes(it, type)
Definition: type.h:216
to_symbol_type
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
has_symbol
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
Definition: find_symbols.cpp:40
kindt::F_BOTH
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std_expr.h