cprover
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 #include "std_types.h"
16 
18 {
19 }
20 
22 {
23 }
24 
26  const symbol_exprt &old_expr,
27  const exprt &new_expr)
28 {
30  old_expr.type() == new_expr.type(),
31  "types to be replaced should match. old type:\n" +
32  old_expr.type().pretty() + "\nnew.type:\n" + new_expr.type().pretty());
33  expr_map.insert(std::pair<irep_idt, exprt>(
34  old_expr.get_identifier(), new_expr));
35 }
36 
37 void replace_symbolt::set(const symbol_exprt &old_expr, const exprt &new_expr)
38 {
39  PRECONDITION(old_expr.type() == new_expr.type());
40  expr_map[old_expr.get_identifier()] = new_expr;
41 }
42 
43 
45 {
46  expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
47 
48  if(it == expr_map.end())
49  return true;
50 
52  s.type() == it->second.type(),
53  "types to be replaced should match. s.type:\n" + s.type().pretty() +
54  "\nit->second.type:\n" + it->second.type().pretty());
55  static_cast<exprt &>(s) = it->second;
56 
57  return false;
58 }
59 
61 {
62  bool result=true; // unchanged
63 
64  // first look at type
65 
66  const exprt &const_dest(dest);
67  if(have_to_replace(const_dest.type()))
68  if(!replace(dest.type()))
69  result=false;
70 
71  // now do expression itself
72 
73  if(!have_to_replace(dest))
74  return result;
75 
76  if(dest.id()==ID_member)
77  {
78  member_exprt &me=to_member_expr(dest);
79 
80  if(!replace(me.struct_op()))
81  result=false;
82  }
83  else if(dest.id()==ID_index)
84  {
85  index_exprt &ie=to_index_expr(dest);
86 
87  if(!replace(ie.array()))
88  result=false;
89 
90  if(!replace(ie.index()))
91  result=false;
92  }
93  else if(dest.id()==ID_address_of)
94  {
96 
97  if(!replace(aoe.object()))
98  result=false;
99  }
100  else if(dest.id()==ID_symbol)
101  {
103  return false;
104  }
105  else
106  {
107  Forall_operands(it, dest)
108  if(!replace(*it))
109  result=false;
110  }
111 
112  const typet &c_sizeof_type =
113  static_cast<const typet&>(dest.find(ID_C_c_sizeof_type));
114  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
115  result &= replace(static_cast<typet&>(dest.add(ID_C_c_sizeof_type)));
116 
117  const typet &va_arg_type =
118  static_cast<const typet&>(dest.find(ID_C_va_arg_type));
119  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
120  result &= replace(static_cast<typet&>(dest.add(ID_C_va_arg_type)));
121 
122  return result;
123 }
124 
126 {
127  if(empty())
128  return false;
129 
130  // first look at type
131 
132  if(have_to_replace(dest.type()))
133  return true;
134 
135  // now do expression itself
136 
137  if(dest.id()==ID_symbol)
138  {
139  const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
140  return replaces_symbol(identifier);
141  }
142 
143  forall_operands(it, dest)
144  if(have_to_replace(*it))
145  return true;
146 
147  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
148 
149  if(c_sizeof_type.is_not_nil())
150  if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
151  return true;
152 
153  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
154 
155  if(va_arg_type.is_not_nil())
156  if(have_to_replace(static_cast<const typet &>(va_arg_type)))
157  return true;
158 
159  return false;
160 }
161 
163 {
164  if(!have_to_replace(dest))
165  return true;
166 
167  bool result=true;
168 
169  if(dest.has_subtype())
170  if(!replace(dest.subtype()))
171  result=false;
172 
173  for(typet &subtype : to_type_with_subtypes(dest).subtypes())
174  {
175  if(!replace(subtype))
176  result=false;
177  }
178 
179  if(dest.id()==ID_struct ||
180  dest.id()==ID_union)
181  {
182  struct_union_typet &struct_union_type=to_struct_union_type(dest);
183 
184  for(auto &c : struct_union_type.components())
185  if(!replace(c))
186  result=false;
187  }
188  else if(dest.id()==ID_code)
189  {
190  code_typet &code_type=to_code_type(dest);
191  if(!replace(code_type.return_type()))
192  result = false;
193 
194  for(auto &p : code_type.parameters())
195  if(!replace(p))
196  result=false;
197  }
198  else if(dest.id()==ID_array)
199  {
200  array_typet &array_type=to_array_type(dest);
201  if(!replace(array_type.size()))
202  result=false;
203  }
204 
205  return result;
206 }
207 
209 {
210  if(expr_map.empty())
211  return false;
212 
213  if(dest.has_subtype())
214  if(have_to_replace(dest.subtype()))
215  return true;
216 
217  for(const typet &subtype : to_type_with_subtypes(dest).subtypes())
218  {
219  if(have_to_replace(subtype))
220  return true;
221  }
222 
223  if(dest.id()==ID_struct ||
224  dest.id()==ID_union)
225  {
226  const struct_union_typet &struct_union_type=
227  to_struct_union_type(dest);
228 
229  for(const auto &c : struct_union_type.components())
230  if(have_to_replace(c))
231  return true;
232  }
233  else if(dest.id()==ID_code)
234  {
235  const code_typet &code_type=to_code_type(dest);
236  if(have_to_replace(code_type.return_type()))
237  return true;
238 
239  for(const auto &p : code_type.parameters())
240  if(have_to_replace(p))
241  return true;
242  }
243  else if(dest.id()==ID_array)
244  return have_to_replace(to_array_type(dest).size());
245 
246  return false;
247 }
248 
250  const symbol_exprt &old_expr,
251  const exprt &new_expr)
252 {
253  expr_map.emplace(old_expr.get_identifier(), new_expr);
254 }
255 
257 {
258  expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
259 
260  if(it == expr_map.end())
261  return true;
262 
263  static_cast<exprt &>(s) = it->second;
264 
265  return false;
266 }
267 
269 {
270  const exprt &const_dest(dest);
271  if(!require_lvalue && const_dest.id() != ID_address_of)
273 
274  bool result = true; // unchanged
275 
276  // first look at type
277  if(have_to_replace(const_dest.type()))
278  {
279  const set_require_lvalue_and_backupt backup(require_lvalue, false);
281  result = false;
282  }
283 
284  // now do expression itself
285 
286  if(!have_to_replace(dest))
287  return result;
288 
289  if(dest.id() == ID_index)
290  {
291  index_exprt &ie = to_index_expr(dest);
292 
293  // Could yield non l-value.
294  if(!replace(ie.array()))
295  result = false;
296 
297  const set_require_lvalue_and_backupt backup(require_lvalue, false);
298  if(!replace(ie.index()))
299  result = false;
300  }
301  else if(dest.id() == ID_address_of)
302  {
304 
306  if(!replace(aoe.object()))
307  result = false;
308  }
309  else
310  {
312  return false;
313  }
314 
315  const set_require_lvalue_and_backupt backup(require_lvalue, false);
316 
317  const typet &c_sizeof_type =
318  static_cast<const typet &>(dest.find(ID_C_c_sizeof_type));
319  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
321  static_cast<typet &>(dest.add(ID_C_c_sizeof_type)));
322 
323  const typet &va_arg_type =
324  static_cast<const typet &>(dest.find(ID_C_va_arg_type));
325  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
327  static_cast<typet &>(dest.add(ID_C_va_arg_type)));
328 
329  return result;
330 }
331 
333  symbol_exprt &s) const
334 {
335  symbol_exprt s_copy = s;
337  return true;
338 
339  if(require_lvalue && !is_lvalue(s_copy))
340  return true;
341 
342  // Note s_copy is no longer a symbol_exprt due to the replace operation,
343  // and after this line `s` won't be either
344  s = s_copy;
345 
346  return false;
347 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
replace_symbolt::~replace_symbolt
virtual ~replace_symbolt()
Definition: replace_symbol.cpp:21
typet::subtype
const typet & subtype() const
Definition: type.h:47
replace_symbolt::have_to_replace
bool have_to_replace(const exprt &dest) const
Definition: replace_symbol.cpp:125
replace_symbolt::replaces_symbol
bool replaces_symbol(const irep_idt &id) const
Definition: replace_symbol.h:71
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:339
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:208
typet
The type of an expression, extends irept.
Definition: type.h:28
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
replace_symbolt::replace_symbolt
replace_symbolt()
Definition: replace_symbol.cpp:17
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
replace_symbol.h
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
exprt
Base class for all expressions.
Definition: expr.h:54
replace_symbolt::expr_map
expr_mapt expr_map
Definition: replace_symbol.h:90
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
array_typet::size
const exprt & size() const
Definition: std_types.h:765
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
replace_symbolt::replace_symbol_expr
virtual bool replace_symbol_expr(symbol_exprt &dest) const
Definition: replace_symbol.cpp:44
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2557
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
address_of_aware_replace_symbolt::replace
bool replace(exprt &dest) const override
Definition: replace_symbol.cpp:268
std_types.h
Pre-defined types.
pointer_expr.h
API to expression classes for Pointers.
replace_symbolt::replace
virtual bool replace(exprt &dest) const
Definition: replace_symbol.cpp:60
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:533
irept::id
const irep_idt & id() const
Definition: irep.h:407
replace_symbolt::empty
bool empty() const
Definition: replace_symbol.h:56
replace_symbolt::insert
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...
Definition: replace_symbol.cpp:25
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
address_of_aware_replace_symbolt::require_lvalue
bool require_lvalue
Definition: replace_symbol.h:125
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
expr_util.h
Deprecated expression utility functions.
array_typet
Arrays with given size.
Definition: std_types.h:757
unchecked_replace_symbolt::insert
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Definition: replace_symbol.cpp:249
PRECONDITION_WITH_DIAGNOSTICS
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:465
invariant.h
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
address_of_aware_replace_symbolt::replace_symbol_expr
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: replace_symbol.cpp:332
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
index_exprt
Array index operator.
Definition: std_expr.h:1242
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
address_of_aware_replace_symbolt::set_require_lvalue_and_backupt
Definition: replace_symbol.h:128
std_expr.h
API to expression classes.
unchecked_replace_symbolt::replace_symbol_expr
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: replace_symbol.cpp:256
replace_symbolt::set
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
Definition: replace_symbol.cpp:37
is_lvalue
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:25