cprover
Loading...
Searching...
No Matches
replace_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "replace_symbol.h"
10
11#include "expr_util.h"
12#include "invariant.h"
13#include "pointer_expr.h"
14#include "std_expr.h"
15
17{
18}
19
21{
22}
23
25 const symbol_exprt &old_expr,
26 const exprt &new_expr)
27{
29 old_expr.type() == new_expr.type(),
30 "types to be replaced should match. old type:\n" +
31 old_expr.type().pretty() + "\nnew.type:\n" + new_expr.type().pretty());
32 expr_map.insert(std::pair<irep_idt, exprt>(
33 old_expr.get_identifier(), new_expr));
34}
35
36void replace_symbolt::set(const symbol_exprt &old_expr, const exprt &new_expr)
37{
38 PRECONDITION(old_expr.type() == new_expr.type());
39 expr_map[old_expr.get_identifier()] = new_expr;
40}
41
42
44{
45 expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
46
47 if(it == expr_map.end())
48 return true;
49
51 s.type() == it->second.type(),
52 "types to be replaced should match. s.type:\n" + s.type().pretty() +
53 "\nit->second.type:\n" + it->second.type().pretty());
54 static_cast<exprt &>(s) = it->second;
55
56 return false;
57}
58
60{
61 bool result=true; // unchanged
62
63 // first look at type
64
65 const exprt &const_dest(dest);
66 if(have_to_replace(const_dest.type()))
67 if(!replace(dest.type()))
68 result=false;
69
70 // now do expression itself
71
72 if(!have_to_replace(dest))
73 return result;
74
75 if(dest.id()==ID_member)
76 {
78
79 if(!replace(me.struct_op()))
80 result=false;
81 }
82 else if(dest.id()==ID_index)
83 {
84 index_exprt &ie=to_index_expr(dest);
85
86 if(!replace(ie.array()))
87 result=false;
88
89 if(!replace(ie.index()))
90 result=false;
91 }
92 else if(dest.id()==ID_address_of)
93 {
95
96 if(!replace(aoe.object()))
97 result=false;
98 }
99 else if(dest.id()==ID_symbol)
100 {
102 return false;
103 }
104 else
105 {
106 Forall_operands(it, dest)
107 if(!replace(*it))
108 result=false;
109 }
110
111 const typet &c_sizeof_type =
112 static_cast<const typet&>(dest.find(ID_C_c_sizeof_type));
113 if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
114 result &= replace(static_cast<typet&>(dest.add(ID_C_c_sizeof_type)));
115
116 const typet &va_arg_type =
117 static_cast<const typet&>(dest.find(ID_C_va_arg_type));
118 if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
119 result &= replace(static_cast<typet&>(dest.add(ID_C_va_arg_type)));
120
121 return result;
122}
123
125{
126 if(empty())
127 return false;
128
129 // first look at type
130
131 if(have_to_replace(dest.type()))
132 return true;
133
134 // now do expression itself
135
136 if(dest.id()==ID_symbol)
137 {
138 const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
139 return replaces_symbol(identifier);
140 }
141
142 forall_operands(it, dest)
143 if(have_to_replace(*it))
144 return true;
145
146 const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
147
148 if(c_sizeof_type.is_not_nil())
149 if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
150 return true;
151
152 const irept &va_arg_type=dest.find(ID_C_va_arg_type);
153
154 if(va_arg_type.is_not_nil())
155 if(have_to_replace(static_cast<const typet &>(va_arg_type)))
156 return true;
157
158 return false;
159}
160
162{
163 if(!have_to_replace(dest))
164 return true;
165
166 bool result=true;
167
168 if(dest.has_subtype())
169 if(!replace(dest.subtype()))
170 result=false;
171
172 for(typet &subtype : to_type_with_subtypes(dest).subtypes())
173 {
174 if(!replace(subtype))
175 result=false;
176 }
177
178 if(dest.id()==ID_struct ||
179 dest.id()==ID_union)
180 {
181 struct_union_typet &struct_union_type=to_struct_union_type(dest);
182
183 for(auto &c : struct_union_type.components())
184 if(!replace(c))
185 result=false;
186 }
187 else if(dest.id()==ID_code)
188 {
189 code_typet &code_type=to_code_type(dest);
190 if(!replace(code_type.return_type()))
191 result = false;
192
193 for(auto &p : code_type.parameters())
194 if(!replace(p))
195 result=false;
196 }
197 else if(dest.id()==ID_array)
198 {
199 array_typet &array_type=to_array_type(dest);
200 if(!replace(array_type.size()))
201 result=false;
202 }
203
204 return result;
205}
206
208{
209 if(expr_map.empty())
210 return false;
211
212 if(dest.has_subtype())
213 if(have_to_replace(to_type_with_subtype(dest).subtype()))
214 return true;
215
216 for(const typet &subtype : to_type_with_subtypes(dest).subtypes())
217 {
218 if(have_to_replace(subtype))
219 return true;
220 }
221
222 if(dest.id()==ID_struct ||
223 dest.id()==ID_union)
224 {
225 const struct_union_typet &struct_union_type=
227
228 for(const auto &c : struct_union_type.components())
229 if(have_to_replace(c))
230 return true;
231 }
232 else if(dest.id()==ID_code)
233 {
234 const code_typet &code_type=to_code_type(dest);
235 if(have_to_replace(code_type.return_type()))
236 return true;
237
238 for(const auto &p : code_type.parameters())
239 if(have_to_replace(p))
240 return true;
241 }
242 else if(dest.id()==ID_array)
243 return have_to_replace(to_array_type(dest).size());
244
245 return false;
246}
247
249 const symbol_exprt &old_expr,
250 const exprt &new_expr)
251{
252 expr_map.emplace(old_expr.get_identifier(), new_expr);
253}
254
256{
257 expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
258
259 if(it == expr_map.end())
260 return true;
261
262 static_cast<exprt &>(s) = it->second;
263
264 return false;
265}
266
268{
269 const exprt &const_dest(dest);
270 if(!require_lvalue && const_dest.id() != ID_address_of)
272
273 bool result = true; // unchanged
274
275 // first look at type
276 if(have_to_replace(const_dest.type()))
277 {
280 result = false;
281 }
282
283 // now do expression itself
284
285 if(!have_to_replace(dest))
286 return result;
287
288 if(dest.id() == ID_index)
289 {
290 index_exprt &ie = to_index_expr(dest);
291
292 // Could yield non l-value.
293 if(!replace(ie.array()))
294 result = false;
295
297 if(!replace(ie.index()))
298 result = false;
299 }
300 else if(dest.id() == ID_address_of)
301 {
303
305 if(!replace(aoe.object()))
306 result = false;
307 }
308 else
309 {
311 return false;
312 }
313
315
316 const typet &c_sizeof_type =
317 static_cast<const typet &>(dest.find(ID_C_c_sizeof_type));
318 if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
320 static_cast<typet &>(dest.add(ID_C_c_sizeof_type)));
321
322 const typet &va_arg_type =
323 static_cast<const typet &>(dest.find(ID_C_va_arg_type));
324 if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
326 static_cast<typet &>(dest.add(ID_C_va_arg_type)));
327
328 return result;
329}
330
332 symbol_exprt &s) const
333{
334 symbol_exprt s_copy = s;
336 return true;
337
338 if(require_lvalue && !is_assignable(s_copy))
339 return true;
340
341 // Note s_copy is no longer a symbol_exprt due to the replace operation,
342 // and after this line `s` won't be either
343 s = s_copy;
344
345 return false;
346}
bool replace_symbol_expr(symbol_exprt &dest) const override
bool replace(exprt &dest) const override
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
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
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
virtual bool replace(exprt &dest) const
bool empty() const
bool have_to_replace(const exprt &dest) const
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
virtual ~replace_symbolt()
virtual bool replace_symbol_expr(symbol_exprt &dest) const
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
bool replaces_symbol(const irep_idt &id) const
expr_mapt expr_map
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
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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
bool replace_symbol_expr(symbol_exprt &dest) const override
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:21
Deprecated expression utility functions.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
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 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