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 "std_types.h"
12 #include "std_expr.h"
13 
15 {
16 }
17 
19 {
20 }
21 
23  const symbol_exprt &old_expr,
24  const exprt &new_expr)
25 {
26  expr_map.insert(std::pair<irep_idt, exprt>(
27  old_expr.get_identifier(), new_expr));
28 }
29 
31  exprt &dest,
32  const bool replace_with_const) const
33 {
34  bool result=true; // unchanged
35 
36  // first look at type
37 
38  const exprt &const_dest(dest);
39  if(have_to_replace(const_dest.type()))
40  if(!replace(dest.type()))
41  result=false;
42 
43  // now do expression itself
44 
45  if(!have_to_replace(dest))
46  return result;
47 
48  if(dest.id()==ID_member)
49  {
50  member_exprt &me=to_member_expr(dest);
51 
52  if(!replace(me.struct_op(), replace_with_const)) // Could give non l-value.
53  result=false;
54  }
55  else if(dest.id()==ID_index)
56  {
57  index_exprt &ie=to_index_expr(dest);
58 
59  if(!replace(ie.array(), replace_with_const)) // Could give non l-value.
60  result=false;
61 
62  if(!replace(ie.index()))
63  result=false;
64  }
65  else if(dest.id()==ID_address_of)
66  {
68 
69  if(!replace(aoe.object(), false))
70  result=false;
71  }
72  else if(dest.id()==ID_symbol)
73  {
74  const symbol_exprt &s=to_symbol_expr(dest);
75 
76  expr_mapt::const_iterator it=
77  expr_map.find(s.get_identifier());
78 
79  if(it!=expr_map.end())
80  {
81  const exprt &e=it->second;
82 
83  if(!replace_with_const && e.is_constant()) // Would give non l-value.
84  return true;
85 
86  dest=e;
87 
88  return false;
89  }
90  }
91  else
92  {
93  Forall_operands(it, dest)
94  if(!replace(*it))
95  result=false;
96  }
97 
98  const typet &c_sizeof_type =
99  static_cast<const typet&>(dest.find(ID_C_c_sizeof_type));
100  if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type))
101  result &= replace(static_cast<typet&>(dest.add(ID_C_c_sizeof_type)));
102 
103  const typet &type_arg = static_cast<const typet &>(dest.find(ID_type_arg));
104  if(type_arg.is_not_nil() && have_to_replace(type_arg))
105  result &= replace(static_cast<typet &>(dest.add(ID_type_arg)));
106 
107  const typet &va_arg_type =
108  static_cast<const typet&>(dest.find(ID_C_va_arg_type));
109  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
110  result &= replace(static_cast<typet&>(dest.add(ID_C_va_arg_type)));
111 
112  return result;
113 }
114 
116 {
117  if(expr_map.empty() && type_map.empty())
118  return false;
119 
120  // first look at type
121 
122  if(have_to_replace(dest.type()))
123  return true;
124 
125  // now do expression itself
126 
127  if(dest.id()==ID_symbol)
128  {
129  const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
130  return expr_map.find(identifier) != expr_map.end();
131  }
132 
133  forall_operands(it, dest)
134  if(have_to_replace(*it))
135  return true;
136 
137  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
138 
139  if(c_sizeof_type.is_not_nil())
140  if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
141  return true;
142 
143  const irept &type_arg = dest.find(ID_type_arg);
144 
145  if(type_arg.is_not_nil())
146  if(have_to_replace(static_cast<const typet &>(type_arg)))
147  return true;
148 
149  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
150 
151  if(va_arg_type.is_not_nil())
152  if(have_to_replace(static_cast<const typet &>(va_arg_type)))
153  return true;
154 
155  return false;
156 }
157 
159 {
160  if(!have_to_replace(dest))
161  return true;
162 
163  bool result=true;
164 
165  if(dest.has_subtype())
166  if(!replace(dest.subtype()))
167  result=false;
168 
169  Forall_subtypes(it, dest)
170  if(!replace(*it))
171  result=false;
172 
173  if(dest.id()==ID_struct ||
174  dest.id()==ID_union)
175  {
176  struct_union_typet &struct_union_type=to_struct_union_type(dest);
178  struct_union_type.components();
179 
180  for(struct_union_typet::componentst::iterator
181  it=components.begin();
182  it!=components.end();
183  it++)
184  if(!replace(*it))
185  result=false;
186  }
187  else if(dest.id()==ID_code)
188  {
189  code_typet &code_type=to_code_type(dest);
190  (void)replace(code_type.return_type());
191  code_typet::parameterst &parameters=code_type.parameters();
192  for(code_typet::parameterst::iterator it = parameters.begin();
193  it!=parameters.end();
194  it++)
195  if(!replace(*it))
196  result=false;
197  }
198  else if(dest.id()==ID_symbol)
199  {
200  type_mapt::const_iterator it =
201  type_map.find(to_symbol_type(dest).get_identifier());
202 
203  if(it!=type_map.end())
204  {
205  dest=it->second;
206  result=false;
207  }
208  }
209  else if(dest.id()==ID_array)
210  {
211  array_typet &array_type=to_array_type(dest);
212  if(!replace(array_type.size()))
213  result=false;
214  }
215 
216  return result;
217 }
218 
220 {
221  if(expr_map.empty() && type_map.empty())
222  return false;
223 
224  if(dest.has_subtype())
225  if(have_to_replace(dest.subtype()))
226  return true;
227 
228  forall_subtypes(it, dest)
229  if(have_to_replace(*it))
230  return true;
231 
232  if(dest.id()==ID_struct ||
233  dest.id()==ID_union)
234  {
235  const struct_union_typet &struct_union_type=
236  to_struct_union_type(dest);
237 
238  const struct_union_typet::componentst &components=
239  struct_union_type.components();
240 
241  for(struct_union_typet::componentst::const_iterator
242  it=components.begin();
243  it!=components.end();
244  it++)
245  if(have_to_replace(*it))
246  return true;
247  }
248  else if(dest.id()==ID_code)
249  {
250  const code_typet &code_type=to_code_type(dest);
251  if(have_to_replace(code_type.return_type()))
252  return true;
253 
254  const code_typet::parameterst &parameters=code_type.parameters();
255 
256  for(code_typet::parameterst::const_iterator
257  it=parameters.begin();
258  it!=parameters.end();
259  it++)
260  if(have_to_replace(*it))
261  return true;
262  }
263  else if(dest.id()==ID_symbol)
264  {
265  const irep_idt &identifier = to_symbol_type(dest).get_identifier();
266  return type_map.find(identifier) != type_map.end();
267  }
268  else if(dest.id()==ID_array)
269  return have_to_replace(to_array_type(dest).size());
270 
271  return false;
272 }
The type of an expression.
Definition: type.h:22
#define forall_subtypes(it, type)
Definition: type.h:161
Base type of functions.
Definition: std_types.h:764
bool is_not_nil() const
Definition: irep.h:103
exprt & object()
Definition: std_expr.h:3180
bool has_subtype() const
Definition: type.h:79
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::vector< componentt > componentst
Definition: std_types.h:243
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
std::vector< parametert > parameterst
Definition: std_types.h:767
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3201
Extract member of struct or union.
Definition: std_expr.h:3871
const irep_idt & id() const
Definition: irep.h:189
API to expression classes.
bool have_to_replace(const exprt &dest) const
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
const exprt & size() const
Definition: std_types.h:1014
Base class for tree-like data structures with sharing.
Definition: irep.h:86
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Operator to return the address of an object.
Definition: std_expr.h:3170
bool is_constant() const
Definition: expr.cpp:119
virtual ~replace_symbolt()
API to type classes.
virtual bool replace(exprt &dest, const bool replace_with_const=true) const
Replaces a symbol with a constant If you are replacing symbols with constants in an l-value...
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
exprt & index()
Definition: std_expr.h:1496
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3911
const parameterst & parameters() const
Definition: std_types.h:905
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
irept & add(const irep_namet &name)
Definition: irep.cpp:306
#define Forall_subtypes(it, type)
Definition: type.h:167
#define Forall_operands(it, expr)
Definition: expr.h:23
void insert(const irep_idt &identifier, const exprt &expr)
type_mapt type_map
arrays with given size
Definition: std_types.h:1004
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const typet & subtype() const
Definition: type.h:33
expr_mapt expr_map
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const typet & return_type() const
Definition: std_types.h:895
const irep_idt & get_identifier() const
Definition: std_types.h:123
array index operator
Definition: std_expr.h:1462