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 &va_arg_type =
104  static_cast<const typet&>(dest.find(ID_C_va_arg_type));
105  if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type))
106  result &= replace(static_cast<typet&>(dest.add(ID_C_va_arg_type)));
107 
108  return result;
109 }
110 
112 {
113  if(expr_map.empty() && type_map.empty())
114  return false;
115 
116  // first look at type
117 
118  if(have_to_replace(dest.type()))
119  return true;
120 
121  // now do expression itself
122 
123  if(dest.id()==ID_symbol)
124  {
125  const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
126  return expr_map.find(identifier) != expr_map.end();
127  }
128 
129  forall_operands(it, dest)
130  if(have_to_replace(*it))
131  return true;
132 
133  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
134 
135  if(c_sizeof_type.is_not_nil())
136  if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
137  return true;
138 
139  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
140 
141  if(va_arg_type.is_not_nil())
142  if(have_to_replace(static_cast<const typet &>(va_arg_type)))
143  return true;
144 
145  return false;
146 }
147 
149 {
150  if(!have_to_replace(dest))
151  return true;
152 
153  bool result=true;
154 
155  if(dest.has_subtype())
156  if(!replace(dest.subtype()))
157  result=false;
158 
159  Forall_subtypes(it, dest)
160  if(!replace(*it))
161  result=false;
162 
163  if(dest.id()==ID_struct ||
164  dest.id()==ID_union)
165  {
166  struct_union_typet &struct_union_type=to_struct_union_type(dest);
168  struct_union_type.components();
169 
170  for(struct_union_typet::componentst::iterator
171  it=components.begin();
172  it!=components.end();
173  it++)
174  if(!replace(*it))
175  result=false;
176  }
177  else if(dest.id()==ID_code)
178  {
179  code_typet &code_type=to_code_type(dest);
180  if(!replace(code_type.return_type()))
181  result = false;
182  code_typet::parameterst &parameters=code_type.parameters();
183  for(code_typet::parameterst::iterator it = parameters.begin();
184  it!=parameters.end();
185  it++)
186  if(!replace(*it))
187  result=false;
188  }
189  else if(dest.id()==ID_symbol)
190  {
191  type_mapt::const_iterator it =
192  type_map.find(to_symbol_type(dest).get_identifier());
193 
194  if(it!=type_map.end())
195  {
196  dest=it->second;
197  result=false;
198  }
199  }
200  else if(dest.id()==ID_array)
201  {
202  array_typet &array_type=to_array_type(dest);
203  if(!replace(array_type.size()))
204  result=false;
205  }
206 
207  return result;
208 }
209 
211 {
212  if(expr_map.empty() && type_map.empty())
213  return false;
214 
215  if(dest.has_subtype())
216  if(have_to_replace(dest.subtype()))
217  return true;
218 
219  forall_subtypes(it, dest)
220  if(have_to_replace(*it))
221  return true;
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  const struct_union_typet::componentst &components=
230  struct_union_type.components();
231 
232  for(struct_union_typet::componentst::const_iterator
233  it=components.begin();
234  it!=components.end();
235  it++)
236  if(have_to_replace(*it))
237  return true;
238  }
239  else if(dest.id()==ID_code)
240  {
241  const code_typet &code_type=to_code_type(dest);
242  if(have_to_replace(code_type.return_type()))
243  return true;
244 
245  const code_typet::parameterst &parameters=code_type.parameters();
246 
247  for(code_typet::parameterst::const_iterator
248  it=parameters.begin();
249  it!=parameters.end();
250  it++)
251  if(have_to_replace(*it))
252  return true;
253  }
254  else if(dest.id()==ID_symbol)
255  {
256  const irep_idt &identifier = to_symbol_type(dest).get_identifier();
257  return type_map.find(identifier) != type_map.end();
258  }
259  else if(dest.id()==ID_array)
260  return have_to_replace(to_array_type(dest).size());
261 
262  return false;
263 }
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:173
exprt & object()
Definition: std_expr.h:3178
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:993
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:3199
Extract member of struct or union.
Definition: std_expr.h:3869
const irep_idt & id() const
Definition: irep.h:259
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:3953
const exprt & size() const
Definition: std_types.h:1023
Base class for tree-like data structures with sharing.
Definition: irep.h:156
#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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
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:1054
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3909
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:1013
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