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