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
19
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 if(dest.id() == ID_let)
105 {
106 auto &let_expr = to_let_expr(dest);
107
108 // first replace the assigned value expressions
109 for(auto &op : let_expr.values())
110 if(replace(op))
111 result = false;
112
113 // now set up the binding
114 auto old_bindings = bindings;
115 for(auto &variable : let_expr.variables())
116 bindings.insert(variable.get_identifier());
117
118 // now replace in the 'where' expression
119 if(!replace(let_expr.where()))
120 result = false;
121
122 bindings = std::move(old_bindings);
123 }
124 else if(
125 dest.id() == ID_array_comprehension || dest.id() == ID_exists ||
126 dest.id() == ID_forall || dest.id() == ID_lambda)
127 {
128 auto &binding_expr = to_binding_expr(dest);
129
130 auto old_bindings = bindings;
131 for(auto &binding : binding_expr.variables())
132 bindings.insert(binding.get_identifier());
133
134 if(!replace(binding_expr.where()))
135 result = false;
136
137 bindings = std::move(old_bindings);
138 }
139 else
140 {
141 Forall_operands(it, dest)
142 if(!replace(*it))
143 result=false;
144 }
145
146 const typet &c_sizeof_type =
147 static_cast<const typet&>(dest.find(ID_C_c_sizeof_type));
148 if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
149 result &= replace(static_cast<typet&>(dest.add(ID_C_c_sizeof_type)));
150
151 const typet &va_arg_type =
152 static_cast<const typet&>(dest.find(ID_C_va_arg_type));
153 if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
154 result &= replace(static_cast<typet&>(dest.add(ID_C_va_arg_type)));
155
156 return result;
157}
158
160{
161 if(empty())
162 return false;
163
164 // first look at type
165
166 if(have_to_replace(dest.type()))
167 return true;
168
169 // now do expression itself
170
171 if(dest.id()==ID_symbol)
172 {
173 const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
174 if(bindings.find(identifier) != bindings.end())
175 return false;
176 else
177 return replaces_symbol(identifier);
178 }
179
180 for(const auto &op : dest.operands())
181 {
182 if(have_to_replace(op))
183 return true;
184 }
185
186 const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
187
188 if(c_sizeof_type.is_not_nil())
189 if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
190 return true;
191
192 const irept &va_arg_type=dest.find(ID_C_va_arg_type);
193
194 if(va_arg_type.is_not_nil())
195 if(have_to_replace(static_cast<const typet &>(va_arg_type)))
196 return true;
197
198 return false;
199}
200
202{
203 if(!have_to_replace(dest))
204 return true;
205
206 bool result=true;
207
208 if(dest.has_subtype())
209 if(!replace(to_type_with_subtype(dest).subtype()))
210 result=false;
211
212 for(typet &subtype : to_type_with_subtypes(dest).subtypes())
213 {
214 if(!replace(subtype))
215 result=false;
216 }
217
218 if(dest.id()==ID_struct ||
219 dest.id()==ID_union)
220 {
221 struct_union_typet &struct_union_type=to_struct_union_type(dest);
222
223 for(auto &c : struct_union_type.components())
224 if(!replace(c))
225 result=false;
226 }
227 else if(dest.id()==ID_code)
228 {
229 code_typet &code_type=to_code_type(dest);
230 if(!replace(code_type.return_type()))
231 result = false;
232
233 for(auto &p : code_type.parameters())
234 if(!replace(p))
235 result=false;
236
237 const exprt &spec_assigns =
238 static_cast<const exprt &>(dest.find(ID_C_spec_assigns));
239 if(spec_assigns.is_not_nil() && have_to_replace(spec_assigns))
240 result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_assigns)));
241
242 const exprt &spec_frees =
243 static_cast<const exprt &>(dest.find(ID_C_spec_frees));
244 if(spec_frees.is_not_nil() && have_to_replace(spec_frees))
245 result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_frees)));
246
247 const exprt &spec_ensures =
248 static_cast<const exprt &>(dest.find(ID_C_spec_ensures));
249 if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures))
250 result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_ensures)));
251
252 const exprt &spec_requires =
253 static_cast<const exprt &>(dest.find(ID_C_spec_requires));
254 if(spec_requires.is_not_nil() && have_to_replace(spec_requires))
255 result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_requires)));
256 }
257 else if(dest.id()==ID_array)
258 {
259 array_typet &array_type=to_array_type(dest);
260 if(!replace(array_type.size()))
261 result=false;
262 }
263
264 return result;
265}
266
268{
269 if(expr_map.empty())
270 return false;
271
272 if(dest.has_subtype())
273 if(have_to_replace(to_type_with_subtype(dest).subtype()))
274 return true;
275
276 for(const typet &subtype : to_type_with_subtypes(dest).subtypes())
277 {
278 if(have_to_replace(subtype))
279 return true;
280 }
281
282 if(dest.id()==ID_struct ||
283 dest.id()==ID_union)
284 {
285 const struct_union_typet &struct_union_type=
287
288 for(const auto &c : struct_union_type.components())
289 if(have_to_replace(c))
290 return true;
291 }
292 else if(dest.id()==ID_code)
293 {
294 const code_typet &code_type=to_code_type(dest);
295 if(have_to_replace(code_type.return_type()))
296 return true;
297
298 for(const auto &p : code_type.parameters())
299 if(have_to_replace(p))
300 return true;
301
302 const exprt &spec_assigns =
303 static_cast<const exprt &>(dest.find(ID_C_spec_assigns));
304 if(spec_assigns.is_not_nil() && have_to_replace(spec_assigns))
305 return true;
306
307 const exprt &spec_ensures =
308 static_cast<const exprt &>(dest.find(ID_C_spec_ensures));
309 if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures))
310 return true;
311
312 const exprt &spec_requires =
313 static_cast<const exprt &>(dest.find(ID_C_spec_requires));
314 if(spec_requires.is_not_nil() && have_to_replace(spec_requires))
315 return true;
316 }
317 else if(dest.id()==ID_array)
318 return have_to_replace(to_array_type(dest).size());
319
320 return false;
321}
322
324 const symbol_exprt &old_expr,
325 const exprt &new_expr)
326{
327 expr_map.emplace(old_expr.get_identifier(), new_expr);
328}
329
331{
332 expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
333
334 if(it == expr_map.end())
335 return true;
336
337 static_cast<exprt &>(s) = it->second;
338
339 return false;
340}
341
343{
344 const exprt &const_dest(dest);
345 if(!require_lvalue && const_dest.id() != ID_address_of)
347
348 bool result = true; // unchanged
349
350 // first look at type
351 if(have_to_replace(const_dest.type()))
352 {
355 result = false;
356 }
357
358 // now do expression itself
359
360 if(!have_to_replace(dest))
361 return result;
362
363 if(dest.id() == ID_index)
364 {
365 index_exprt &ie = to_index_expr(dest);
366
367 // Could yield non l-value.
368 if(!replace(ie.array()))
369 result = false;
370
372 if(!replace(ie.index()))
373 result = false;
374 }
375 else if(dest.id() == ID_address_of)
376 {
378
380 if(!replace(aoe.object()))
381 result = false;
382 }
383 else
384 {
386 return false;
387 }
388
390
391 const typet &c_sizeof_type =
392 static_cast<const typet &>(dest.find(ID_C_c_sizeof_type));
393 if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
395 static_cast<typet &>(dest.add(ID_C_c_sizeof_type)));
396
397 const typet &va_arg_type =
398 static_cast<const typet &>(dest.find(ID_C_va_arg_type));
399 if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
401 static_cast<typet &>(dest.add(ID_C_va_arg_type)));
402
403 return result;
404}
405
407 symbol_exprt &s) const
408{
409 symbol_exprt s_copy = s;
411 return true;
412
413 if(require_lvalue && !is_assignable(s_copy))
414 return true;
415
416 // Note s_copy is no longer a symbol_exprt due to the replace operation,
417 // and after this line `s` won't be either
418 s = s_copy;
419
420 return false;
421}
bool replace_symbol_expr(symbol_exprt &dest) const override
bool replace(exprt &dest) const override
Operator to return the address of an object.
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:796
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:39
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
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:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
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:111
Extract member of struct or union.
Definition std_expr.h:2794
const exprt & struct_op() const
Definition std_expr.h:2832
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.
std::set< irep_idt > bindings
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
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:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
subtypest & subtypes()
Definition type.h:204
The type of an expression, extends irept.
Definition type.h:29
bool has_subtype() const
Definition type.h:64
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:27
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:24
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.
#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:534
#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:1478
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3273
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:3121
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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:844
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:219
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175