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