CBMC
replace_symbol.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 "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 
36 void 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  source_locationt previous_source_location{s.source_location()};
55  static_cast<exprt &>(s) = it->second;
56  // back-end generated or internal symbols (like rounding mode) might not have
57  // a source location
58  if(s.source_location().is_nil() && previous_source_location.is_not_nil())
59  s.add_source_location() = std::move(previous_source_location);
60 
61  return false;
62 }
63 
65 {
66  bool result=true; // unchanged
67 
68  // first look at type
69 
70  const exprt &const_dest(dest);
71  if(have_to_replace(const_dest.type()))
72  if(!replace(dest.type()))
73  result=false;
74 
75  // now do expression itself
76 
77  if(!have_to_replace(dest))
78  return result;
79 
80  if(dest.id()==ID_member)
81  {
82  member_exprt &me=to_member_expr(dest);
83 
84  if(!replace(me.struct_op()))
85  result=false;
86  }
87  else if(dest.id()==ID_index)
88  {
89  index_exprt &ie=to_index_expr(dest);
90 
91  if(!replace(ie.array()))
92  result=false;
93 
94  if(!replace(ie.index()))
95  result=false;
96  }
97  else if(dest.id()==ID_address_of)
98  {
100 
101  if(!replace(aoe.object()))
102  result=false;
103  }
104  else if(dest.id()==ID_symbol)
105  {
107  return false;
108  }
109  else if(dest.id() == ID_let)
110  {
111  auto &let_expr = to_let_expr(dest);
112 
113  // first replace the assigned value expressions
114  for(auto &op : let_expr.values())
115  if(replace(op))
116  result = false;
117 
118  // now set up the binding
119  auto old_bindings = bindings;
120  for(auto &variable : let_expr.variables())
121  bindings.insert(variable.get_identifier());
122 
123  // now replace in the 'where' expression
124  if(!replace(let_expr.where()))
125  result = false;
126 
127  bindings = std::move(old_bindings);
128  }
129  else if(
130  dest.id() == ID_array_comprehension || dest.id() == ID_exists ||
131  dest.id() == ID_forall || dest.id() == ID_lambda)
132  {
133  auto &binding_expr = to_binding_expr(dest);
134 
135  auto old_bindings = bindings;
136  for(auto &binding : binding_expr.variables())
137  bindings.insert(binding.get_identifier());
138 
139  if(!replace(binding_expr.where()))
140  result = false;
141 
142  bindings = std::move(old_bindings);
143  }
144  else
145  {
146  Forall_operands(it, dest)
147  if(!replace(*it))
148  result=false;
149  }
150 
151  const typet &c_sizeof_type =
152  static_cast<const typet&>(dest.find(ID_C_c_sizeof_type));
153  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
154  result &= replace(static_cast<typet&>(dest.add(ID_C_c_sizeof_type)));
155 
156  const typet &va_arg_type =
157  static_cast<const typet&>(dest.find(ID_C_va_arg_type));
158  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
159  result &= replace(static_cast<typet&>(dest.add(ID_C_va_arg_type)));
160 
161  return result;
162 }
163 
165 {
166  if(empty())
167  return false;
168 
169  // first look at type
170 
171  if(have_to_replace(dest.type()))
172  return true;
173 
174  // now do expression itself
175 
176  if(dest.id()==ID_symbol)
177  {
178  const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
179  if(bindings.find(identifier) != bindings.end())
180  return false;
181  else
182  return replaces_symbol(identifier);
183  }
184 
185  for(const auto &op : dest.operands())
186  {
187  if(have_to_replace(op))
188  return true;
189  }
190 
191  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
192 
193  if(c_sizeof_type.is_not_nil())
194  if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
195  return true;
196 
197  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
198 
199  if(va_arg_type.is_not_nil())
200  if(have_to_replace(static_cast<const typet &>(va_arg_type)))
201  return true;
202 
203  return false;
204 }
205 
207 {
208  if(!have_to_replace(dest))
209  return true;
210 
211  bool result=true;
212 
213  if(dest.has_subtype())
214  if(!replace(to_type_with_subtype(dest).subtype()))
215  result=false;
216 
217  for(typet &subtype : to_type_with_subtypes(dest).subtypes())
218  {
219  if(!replace(subtype))
220  result=false;
221  }
222 
223  if(dest.id()==ID_struct ||
224  dest.id()==ID_union)
225  {
226  struct_union_typet &struct_union_type=to_struct_union_type(dest);
227 
228  for(auto &c : struct_union_type.components())
229  if(!replace(c))
230  result=false;
231  }
232  else if(dest.id()==ID_code)
233  {
234  code_typet &code_type=to_code_type(dest);
235  if(!replace(code_type.return_type()))
236  result = false;
237 
238  for(auto &p : code_type.parameters())
239  if(!replace(p))
240  result=false;
241 
242  const exprt &spec_assigns =
243  static_cast<const exprt &>(dest.find(ID_C_spec_assigns));
244  if(spec_assigns.is_not_nil() && have_to_replace(spec_assigns))
245  result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_assigns)));
246 
247  const exprt &spec_frees =
248  static_cast<const exprt &>(dest.find(ID_C_spec_frees));
249  if(spec_frees.is_not_nil() && have_to_replace(spec_frees))
250  result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_frees)));
251 
252  const exprt &spec_ensures =
253  static_cast<const exprt &>(dest.find(ID_C_spec_ensures));
254  if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures))
255  result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_ensures)));
256 
257  const exprt &spec_requires =
258  static_cast<const exprt &>(dest.find(ID_C_spec_requires));
259  if(spec_requires.is_not_nil() && have_to_replace(spec_requires))
260  result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_requires)));
261  }
262  else if(dest.id()==ID_array)
263  {
264  array_typet &array_type=to_array_type(dest);
265  if(!replace(array_type.size()))
266  result=false;
267  }
268 
269  return result;
270 }
271 
273 {
274  if(expr_map.empty())
275  return false;
276 
277  if(dest.has_subtype())
278  if(have_to_replace(to_type_with_subtype(dest).subtype()))
279  return true;
280 
281  for(const typet &subtype : to_type_with_subtypes(dest).subtypes())
282  {
283  if(have_to_replace(subtype))
284  return true;
285  }
286 
287  if(dest.id()==ID_struct ||
288  dest.id()==ID_union)
289  {
290  const struct_union_typet &struct_union_type=
291  to_struct_union_type(dest);
292 
293  for(const auto &c : struct_union_type.components())
294  if(have_to_replace(c))
295  return true;
296  }
297  else if(dest.id()==ID_code)
298  {
299  const code_typet &code_type=to_code_type(dest);
300  if(have_to_replace(code_type.return_type()))
301  return true;
302 
303  for(const auto &p : code_type.parameters())
304  if(have_to_replace(p))
305  return true;
306 
307  const exprt &spec_assigns =
308  static_cast<const exprt &>(dest.find(ID_C_spec_assigns));
309  if(spec_assigns.is_not_nil() && have_to_replace(spec_assigns))
310  return true;
311 
312  const exprt &spec_ensures =
313  static_cast<const exprt &>(dest.find(ID_C_spec_ensures));
314  if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures))
315  return true;
316 
317  const exprt &spec_requires =
318  static_cast<const exprt &>(dest.find(ID_C_spec_requires));
319  if(spec_requires.is_not_nil() && have_to_replace(spec_requires))
320  return true;
321  }
322  else if(dest.id()==ID_array)
323  return have_to_replace(to_array_type(dest).size());
324 
325  return false;
326 }
327 
329  const symbol_exprt &old_expr,
330  const exprt &new_expr)
331 {
332  expr_map.emplace(old_expr.get_identifier(), new_expr);
333 }
334 
336 {
337  expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
338 
339  if(it == expr_map.end())
340  return true;
341 
342  source_locationt previous_source_location{s.source_location()};
343  static_cast<exprt &>(s) = it->second;
344  // back-end generated or internal symbols (like rounding mode) might not have
345  // a source location
346  if(s.source_location().is_nil() && previous_source_location.is_not_nil())
347  s.add_source_location() = std::move(previous_source_location);
348 
349  return false;
350 }
351 
353 {
354  const exprt &const_dest(dest);
355  if(!require_lvalue && const_dest.id() != ID_address_of)
357 
358  bool result = true; // unchanged
359 
360  // first look at type
361  if(have_to_replace(const_dest.type()))
362  {
363  const set_require_lvalue_and_backupt backup(require_lvalue, false);
365  result = false;
366  }
367 
368  // now do expression itself
369 
370  if(!have_to_replace(dest))
371  return result;
372 
373  if(dest.id() == ID_index)
374  {
375  index_exprt &ie = to_index_expr(dest);
376 
377  // Could yield non l-value.
378  if(!replace(ie.array()))
379  result = false;
380 
381  const set_require_lvalue_and_backupt backup(require_lvalue, false);
382  if(!replace(ie.index()))
383  result = false;
384  }
385  else if(dest.id() == ID_address_of)
386  {
388 
390  if(!replace(aoe.object()))
391  result = false;
392  }
393  else
394  {
396  return false;
397  }
398 
399  const set_require_lvalue_and_backupt backup(require_lvalue, false);
400 
401  const typet &c_sizeof_type =
402  static_cast<const typet &>(dest.find(ID_C_c_sizeof_type));
403  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
405  static_cast<typet &>(dest.add(ID_C_c_sizeof_type)));
406 
407  const typet &va_arg_type =
408  static_cast<const typet &>(dest.find(ID_C_va_arg_type));
409  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
411  static_cast<typet &>(dest.add(ID_C_va_arg_type)));
412 
413  return result;
414 }
415 
417  symbol_exprt &s) const
418 {
419  symbol_exprt s_copy = s;
421  return true;
422 
423  if(require_lvalue && !is_assignable(s_copy))
424  return true;
425 
426  // Note s_copy is no longer a symbol_exprt due to the replace operation,
427  // and after this line `s` won't be either
428  source_locationt previous_source_location{s.source_location()};
429  s = s_copy;
430  // back-end generated or internal symbols (like rounding mode) might not have
431  // a source location
432  if(s.source_location().is_nil() && previous_source_location.is_not_nil())
433  s.add_source_location() = std::move(previous_source_location);
434 
435  return false;
436 }
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:540
exprt & object()
Definition: pointer_expr.h:549
Arrays with given size.
Definition: std_types.h:807
const exprt & size() const
Definition: std_types.h:840
Base type of functions.
Definition: std_types.h:583
const typet & return_type() const
Definition: std_types.h:689
const parameterst & parameters() const
Definition: std_types.h:699
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
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:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
bool is_not_nil() const
Definition: irep.h:368
const irep_idt & id() const
Definition: irep.h:384
irept & add(const irep_idt &name)
Definition: irep.cpp:103
bool is_nil() const
Definition: irep.h:364
Extract member of struct or union.
Definition: std_expr.h:2841
const exprt & struct_op() const
Definition: std_expr.h:2879
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
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:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
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.
Definition: pointer_expr.h:577
#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 let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3320
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition: std_expr.h:3168
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
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:252
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208