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 {
32  bool result=true;
33 
34  // first look at type
35 
36  if(have_to_replace(dest.type()))
37  if(!replace(dest.type()))
38  result=false;
39 
40  // now do expression itself
41 
42  if(!have_to_replace(dest))
43  return result;
44 
45  if(dest.id()==ID_symbol)
46  {
47  expr_mapt::const_iterator it=
48  expr_map.find(dest.get(ID_identifier));
49 
50  if(it!=expr_map.end())
51  {
52  dest=it->second;
53  return false;
54  }
55  }
56 
57  Forall_operands(it, dest)
58  if(!replace(*it))
59  result=false;
60 
61  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
62 
63  if(c_sizeof_type.is_not_nil() &&
64  !replace(static_cast<typet&>(dest.add(ID_C_c_sizeof_type))))
65  result=false;
66 
67  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
68 
69  if(va_arg_type.is_not_nil() &&
70  !replace(static_cast<typet&>(dest.add(ID_C_va_arg_type))))
71  result=false;
72 
73  return result;
74 }
75 
76 bool replace_symbolt::have_to_replace(const exprt &dest) const
77 {
78  // first look at type
79 
80  if(have_to_replace(dest.type()))
81  return true;
82 
83  // now do expression itself
84 
85  if(dest.id()==ID_symbol)
86  return expr_map.find(dest.get(ID_identifier))!=expr_map.end();
87 
88  forall_operands(it, dest)
89  if(have_to_replace(*it))
90  return true;
91 
92  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
93 
94  if(c_sizeof_type.is_not_nil())
95  if(have_to_replace(static_cast<const typet &>(c_sizeof_type)))
96  return true;
97 
98  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
99 
100  if(va_arg_type.is_not_nil())
101  if(have_to_replace(static_cast<const typet &>(va_arg_type)))
102  return true;
103 
104  return false;
105 }
106 
108 {
109  if(!have_to_replace(dest))
110  return true;
111 
112  bool result=true;
113 
114  if(dest.has_subtype())
115  if(!replace(dest.subtype()))
116  result=false;
117 
118  Forall_subtypes(it, dest)
119  if(!replace(*it))
120  result=false;
121 
122  if(dest.id()==ID_struct ||
123  dest.id()==ID_union)
124  {
125  struct_union_typet &struct_union_type=to_struct_union_type(dest);
127  struct_union_type.components();
128 
129  for(struct_union_typet::componentst::iterator
130  it=components.begin();
131  it!=components.end();
132  it++)
133  if(!replace(*it))
134  result=false;
135  }
136  else if(dest.id()==ID_code)
137  {
138  code_typet &code_type=to_code_type(dest);
139  replace(code_type.return_type());
140  code_typet::parameterst &parameters=code_type.parameters();
141  for(code_typet::parameterst::iterator it = parameters.begin();
142  it!=parameters.end();
143  it++)
144  if(!replace(*it))
145  result=false;
146  }
147  else if(dest.id()==ID_symbol)
148  {
149  type_mapt::const_iterator it=
150  type_map.find(dest.get(ID_identifier));
151 
152  if(it!=type_map.end())
153  {
154  dest=it->second;
155  result=false;
156  }
157  }
158  else if(dest.id()==ID_array)
159  {
160  array_typet &array_type=to_array_type(dest);
161  if(!replace(array_type.size()))
162  result=false;
163  }
164 
165  return result;
166 }
167 
169 {
170  if(dest.has_subtype())
171  if(have_to_replace(dest.subtype()))
172  return true;
173 
174  forall_subtypes(it, dest)
175  if(have_to_replace(*it))
176  return true;
177 
178  if(dest.id()==ID_struct ||
179  dest.id()==ID_union)
180  {
181  const struct_union_typet &struct_union_type=
182  to_struct_union_type(dest);
183 
184  const struct_union_typet::componentst &components=
185  struct_union_type.components();
186 
187  for(struct_union_typet::componentst::const_iterator
188  it=components.begin();
189  it!=components.end();
190  it++)
191  if(have_to_replace(*it))
192  return true;
193  }
194  else if(dest.id()==ID_code)
195  {
196  const code_typet &code_type=to_code_type(dest);
197  if(have_to_replace(code_type.return_type()))
198  return true;
199 
200  const code_typet::parameterst &parameters=code_type.parameters();
201 
202  for(code_typet::parameterst::const_iterator
203  it=parameters.begin();
204  it!=parameters.end();
205  it++)
206  if(have_to_replace(*it))
207  return true;
208  }
209  else if(dest.id()==ID_symbol)
210  return type_map.find(dest.get(ID_identifier))!=type_map.end();
211  else if(dest.id()==ID_array)
212  return have_to_replace(to_array_type(dest).size());
213 
214  return false;
215 }
The type of an expression.
Definition: type.h:20
#define forall_subtypes(it, type)
Definition: type.h:159
Base type of functions.
Definition: std_types.h:734
bool is_not_nil() const
Definition: irep.h:104
bool has_subtype() const
Definition: type.h:77
const irep_idt & get_identifier() const
Definition: std_expr.h:120
std::vector< componentt > componentst
Definition: std_types.h:240
std::vector< parametert > parameterst
Definition: std_types.h:829
virtual bool replace(exprt &dest) const
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
bool have_to_replace(const exprt &dest) const
const exprt & size() const
Definition: std_types.h:915
Base class for tree-like data structures with sharing.
Definition: irep.h:87
#define forall_operands(it, expr)
Definition: expr.h:17
virtual ~replace_symbolt()
API to type classes.
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
#define Forall_subtypes(it, type)
Definition: type.h:165
#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:901
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const typet & subtype() const
Definition: type.h:31
expr_mapt expr_map
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const typet & return_type() const
Definition: std_types.h:831