cprover
rename_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "rename_symbol.h"
10
11#include "expr_iterator.h"
12#include "std_expr.h"
13
15{
16}
17
19{
20}
21
23 const symbol_exprt &old_expr,
24 const symbol_exprt &new_expr)
25{
26 insert_expr(old_expr.get_identifier(), new_expr.get_identifier());
27}
28
30{
31 bool result=true;
32
33 for(auto it = dest.depth_begin(), end = dest.depth_end(); it != end; ++it)
34 {
35 exprt * modifiable_expr = nullptr;
36
37 // first look at type
38 if(have_to_rename(it->type()))
39 {
40 modifiable_expr = &it.mutate();
41 result &= rename(modifiable_expr->type());
42 }
43
44 // now do expression itself
45 if(it->id()==ID_symbol)
46 {
47 expr_mapt::const_iterator entry =
49
50 if(entry != expr_map.end())
51 {
52 if(!modifiable_expr)
53 modifiable_expr = &it.mutate();
54 to_symbol_expr(*modifiable_expr).set_identifier(entry->second);
55 result = false;
56 }
57 }
58
59 const typet &c_sizeof_type =
60 static_cast<const typet&>(it->find(ID_C_c_sizeof_type));
61 if(c_sizeof_type.is_not_nil() && have_to_rename(c_sizeof_type))
62 {
63 if(!modifiable_expr)
64 modifiable_expr = &it.mutate();
65 result &=
66 rename(static_cast<typet&>(modifiable_expr->add(ID_C_c_sizeof_type)));
67 }
68
69 const typet &va_arg_type =
70 static_cast<const typet&>(it->find(ID_C_va_arg_type));
71 if(va_arg_type.is_not_nil() && have_to_rename(va_arg_type))
72 {
73 if(!modifiable_expr)
74 modifiable_expr = &it.mutate();
75 result &=
76 rename(static_cast<typet&>(modifiable_expr->add(ID_C_va_arg_type)));
77 }
78 }
79
80 return result;
81}
82
84{
85 if(expr_map.empty() && type_map.empty())
86 return false;
87
88 // first look at type
89
90 if(have_to_rename(dest.type()))
91 return true;
92
93 // now do expression itself
94
95 if(dest.id()==ID_symbol)
96 {
97 const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
98 return expr_map.find(identifier) != expr_map.end();
99 }
100
101 forall_operands(it, dest)
102 if(have_to_rename(*it))
103 return true;
104
105 const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
106
107 if(c_sizeof_type.is_not_nil())
108 if(have_to_rename(static_cast<const typet &>(c_sizeof_type)))
109 return true;
110
111 const irept &va_arg_type=dest.find(ID_C_va_arg_type);
112
113 if(va_arg_type.is_not_nil())
114 if(have_to_rename(static_cast<const typet &>(va_arg_type)))
115 return true;
116
117 return false;
118}
119
121{
122 if(!have_to_rename(dest))
123 return true;
124
125 bool result=true;
126
127 if(dest.has_subtype())
128 if(!rename(dest.subtype()))
129 result=false;
130
131 for(typet &subtype : to_type_with_subtypes(dest).subtypes())
132 {
133 if(!rename(subtype))
134 result=false;
135 }
136
137 if(dest.id()==ID_struct ||
138 dest.id()==ID_union)
139 {
140 struct_union_typet &struct_union_type=to_struct_union_type(dest);
141
142 for(auto &c : struct_union_type.components())
143 if(!rename(c))
144 result=false;
145 }
146 else if(dest.id()==ID_code)
147 {
148 code_typet &code_type=to_code_type(dest);
149 rename(code_type.return_type());
150
151 for(auto &p : code_type.parameters())
152 {
153 if(!rename(p.type()))
154 result=false;
155
156 expr_mapt::const_iterator e_it = expr_map.find(p.get_identifier());
157
158 if(e_it!=expr_map.end())
159 {
160 p.set_identifier(e_it->second);
161 result=false;
162 }
163 }
164 }
165 else if(dest.id()==ID_c_enum_tag ||
166 dest.id()==ID_struct_tag ||
167 dest.id()==ID_union_tag)
168 {
169 type_mapt::const_iterator it=
170 type_map.find(to_tag_type(dest).get_identifier());
171
172 if(it!=type_map.end())
173 {
174 to_tag_type(dest).set_identifier(it->second);
175 result=false;
176 }
177 }
178 else if(dest.id()==ID_array)
179 {
180 array_typet &array_type=to_array_type(dest);
181 if(!rename(array_type.size()))
182 result=false;
183 }
184
185 return result;
186}
187
189{
190 if(expr_map.empty() && type_map.empty())
191 return false;
192
193 if(dest.has_subtype())
194 if(have_to_rename(to_type_with_subtype(dest).subtype()))
195 return true;
196
197 for(const typet &subtype : to_type_with_subtypes(dest).subtypes())
198 {
199 if(have_to_rename(subtype))
200 return true;
201 }
202
203 if(dest.id()==ID_struct ||
204 dest.id()==ID_union)
205 {
206 const struct_union_typet &struct_union_type=
208
209 for(const auto &c : struct_union_type.components())
210 if(have_to_rename(c))
211 return true;
212 }
213 else if(dest.id()==ID_code)
214 {
215 const code_typet &code_type=to_code_type(dest);
216 if(have_to_rename(code_type.return_type()))
217 return true;
218
219 for(const auto &p : code_type.parameters())
220 {
221 if(have_to_rename(p.type()))
222 return true;
223
224 if(expr_map.find(p.get_identifier()) != expr_map.end())
225 return true;
226 }
227 }
228 else if(dest.id()==ID_c_enum_tag ||
229 dest.id()==ID_struct_tag ||
230 dest.id()==ID_union_tag)
231 return type_map.find(to_tag_type(dest).get_identifier())!=type_map.end();
232 else if(dest.id()==ID_array)
233 return have_to_rename(to_array_type(dest).size());
234
235 return false;
236}
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
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
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
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
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
void insert(const class symbol_exprt &old_expr, const class symbol_exprt &new_expr)
virtual ~rename_symbolt()
bool have_to_rename(const exprt &dest) const
expr_mapt expr_map
Definition: rename_symbol.h:63
bool rename(exprt &dest) const
type_mapt type_map
Definition: rename_symbol.h:64
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
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:80
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
const irep_idt & get_identifier() const
Definition: std_expr.h:109
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:405
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
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,...
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 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 tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:434
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