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 {
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  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  {
77  member_exprt &me=to_member_expr(dest);
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  Forall_subtypes(it, dest)
173  if(!replace(*it))
174  result=false;
175 
176  if(dest.id()==ID_struct ||
177  dest.id()==ID_union)
178  {
179  struct_union_typet &struct_union_type=to_struct_union_type(dest);
180 
181  for(auto &c : struct_union_type.components())
182  if(!replace(c))
183  result=false;
184  }
185  else if(dest.id()==ID_code)
186  {
187  code_typet &code_type=to_code_type(dest);
188  if(!replace(code_type.return_type()))
189  result = false;
190 
191  for(auto &p : code_type.parameters())
192  if(!replace(p))
193  result=false;
194  }
195  else if(dest.id()==ID_array)
196  {
197  array_typet &array_type=to_array_type(dest);
198  if(!replace(array_type.size()))
199  result=false;
200  }
201 
202  return result;
203 }
204 
206 {
207  if(expr_map.empty())
208  return false;
209 
210  if(dest.has_subtype())
211  if(have_to_replace(dest.subtype()))
212  return true;
213 
214  forall_subtypes(it, dest)
215  if(have_to_replace(*it))
216  return true;
217 
218  if(dest.id()==ID_struct ||
219  dest.id()==ID_union)
220  {
221  const struct_union_typet &struct_union_type=
222  to_struct_union_type(dest);
223 
224  for(const auto &c : struct_union_type.components())
225  if(have_to_replace(c))
226  return true;
227  }
228  else if(dest.id()==ID_code)
229  {
230  const code_typet &code_type=to_code_type(dest);
231  if(have_to_replace(code_type.return_type()))
232  return true;
233 
234  for(const auto &p : code_type.parameters())
235  if(have_to_replace(p))
236  return true;
237  }
238  else if(dest.id()==ID_array)
239  return have_to_replace(to_array_type(dest).size());
240 
241  return false;
242 }
243 
245  const symbol_exprt &old_expr,
246  const exprt &new_expr)
247 {
248  expr_map.emplace(old_expr.get_identifier(), new_expr);
249 }
250 
252 {
253  expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
254 
255  if(it == expr_map.end())
256  return true;
257 
258  static_cast<exprt &>(s) = it->second;
259 
260  return false;
261 }
262 
264 {
265  const exprt &const_dest(dest);
266  if(!require_lvalue && const_dest.id() != ID_address_of)
268 
269  bool result = true; // unchanged
270 
271  // first look at type
272  if(have_to_replace(const_dest.type()))
273  {
274  const set_require_lvalue_and_backupt backup(require_lvalue, false);
276  result = false;
277  }
278 
279  // now do expression itself
280 
281  if(!have_to_replace(dest))
282  return result;
283 
284  if(dest.id() == ID_index)
285  {
286  index_exprt &ie = to_index_expr(dest);
287 
288  // Could yield non l-value.
289  if(!replace(ie.array()))
290  result = false;
291 
292  const set_require_lvalue_and_backupt backup(require_lvalue, false);
293  if(!replace(ie.index()))
294  result = false;
295  }
296  else if(dest.id() == ID_address_of)
297  {
299 
301  if(!replace(aoe.object()))
302  result = false;
303  }
304  else
305  {
307  return false;
308  }
309 
310  const set_require_lvalue_and_backupt backup(require_lvalue, false);
311 
312  const typet &c_sizeof_type =
313  static_cast<const typet &>(dest.find(ID_C_c_sizeof_type));
314  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
316  static_cast<typet &>(dest.add(ID_C_c_sizeof_type)));
317 
318  const typet &va_arg_type =
319  static_cast<const typet &>(dest.find(ID_C_va_arg_type));
320  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
322  static_cast<typet &>(dest.add(ID_C_va_arg_type)));
323 
324  return result;
325 }
326 
328  symbol_exprt &s) const
329 {
330  symbol_exprt s_copy = s;
332  return true;
333 
334  if(require_lvalue && !is_lvalue(s_copy))
335  return true;
336 
337  // Note s_copy is no longer a symbol_exprt due to the replace operation,
338  // and after this line `s` won't be either
339  s = s_copy;
340 
341  return false;
342 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
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:20
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:124
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:24
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
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:209
typet
The type of an expression, extends irept.
Definition: type.h:29
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
replace_symbolt::replace_symbolt
replace_symbolt()
Definition: replace_symbol.cpp:16
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
replace_symbol.h
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
exprt
Base class for all expressions.
Definition: expr.h:53
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:82
array_typet::size
const exprt & size() const
Definition: std_types.h:973
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
replace_symbolt::replace_symbol_expr
virtual bool replace_symbol_expr(symbol_exprt &dest) const
Definition: replace_symbol.cpp:43
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
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
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
address_of_aware_replace_symbolt::replace
bool replace(exprt &dest) const override
Definition: replace_symbol.cpp:263
std_types.h
Pre-defined types.
Forall_subtypes
#define Forall_subtypes(it, type)
Definition: type.h:222
replace_symbolt::replace
virtual bool replace(exprt &dest) const
Definition: replace_symbol.cpp:59
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:24
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
forall_subtypes
#define forall_subtypes(it, type)
Definition: type.h:216
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:3405
expr_util.h
Deprecated expression utility functions.
array_typet
Arrays with given size.
Definition: std_types.h:965
unchecked_replace_symbolt::insert
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Definition: replace_symbol.cpp:244
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:1011
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
address_of_aware_replace_symbolt::replace_symbol_expr
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: replace_symbol.cpp:327
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
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:251
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:36
is_lvalue
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:23