cprover
rename_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 "rename_symbol.h"
10 
11 #include "expr_iterator.h"
12 #include "std_types.h"
13 #include "std_expr.h"
14 
16 {
17 }
18 
20 {
21 }
22 
24  const symbol_exprt &old_expr,
25  const symbol_exprt &new_expr)
26 {
27  insert_expr(old_expr.get_identifier(), new_expr.get_identifier());
28 }
29 
30 bool rename_symbolt::rename(exprt &dest) const
31 {
32  bool result=true;
33 
34  for(auto it = dest.depth_begin(), end = dest.depth_end(); it != end; ++it)
35  {
36  exprt * modifiable_expr = nullptr;
37 
38  // first look at type
39  if(have_to_rename(it->type()))
40  {
41  modifiable_expr = &it.mutate();
42  result &= rename(modifiable_expr->type());
43  }
44 
45  // now do expression itself
46  if(it->id()==ID_symbol)
47  {
48  expr_mapt::const_iterator entry =
50 
51  if(entry != expr_map.end())
52  {
53  if(!modifiable_expr)
54  modifiable_expr = &it.mutate();
55  to_symbol_expr(*modifiable_expr).set_identifier(entry->second);
56  result = false;
57  }
58  }
59 
60  const typet &c_sizeof_type =
61  static_cast<const typet&>(it->find(ID_C_c_sizeof_type));
62  if(c_sizeof_type.is_not_nil() && have_to_rename(c_sizeof_type))
63  {
64  if(!modifiable_expr)
65  modifiable_expr = &it.mutate();
66  result &=
67  rename(static_cast<typet&>(modifiable_expr->add(ID_C_c_sizeof_type)));
68  }
69 
70  const typet &va_arg_type =
71  static_cast<const typet&>(it->find(ID_C_va_arg_type));
72  if(va_arg_type.is_not_nil() && have_to_rename(va_arg_type))
73  {
74  if(!modifiable_expr)
75  modifiable_expr = &it.mutate();
76  result &=
77  rename(static_cast<typet&>(modifiable_expr->add(ID_C_va_arg_type)));
78  }
79  }
80 
81  return result;
82 }
83 
84 bool rename_symbolt::have_to_rename(const exprt &dest) const
85 {
86  if(expr_map.empty() && type_map.empty())
87  return false;
88 
89  // first look at type
90 
91  if(have_to_rename(dest.type()))
92  return true;
93 
94  // now do expression itself
95 
96  if(dest.id()==ID_symbol)
97  {
98  const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
99  return expr_map.find(identifier) != expr_map.end();
100  }
101 
102  forall_operands(it, dest)
103  if(have_to_rename(*it))
104  return true;
105 
106  const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type);
107 
108  if(c_sizeof_type.is_not_nil())
109  if(have_to_rename(static_cast<const typet &>(c_sizeof_type)))
110  return true;
111 
112  const irept &va_arg_type=dest.find(ID_C_va_arg_type);
113 
114  if(va_arg_type.is_not_nil())
115  if(have_to_rename(static_cast<const typet &>(va_arg_type)))
116  return true;
117 
118  return false;
119 }
120 
121 bool rename_symbolt::rename(typet &dest) const
122 {
123  if(!have_to_rename(dest))
124  return true;
125 
126  bool result=true;
127 
128  if(dest.has_subtype())
129  if(!rename(dest.subtype()))
130  result=false;
131 
132  Forall_subtypes(it, dest)
133  if(!rename(*it))
134  result=false;
135 
136  if(dest.id()==ID_struct ||
137  dest.id()==ID_union)
138  {
139  struct_union_typet &struct_union_type=to_struct_union_type(dest);
140 
141  for(auto &c : struct_union_type.components())
142  if(!rename(c))
143  result=false;
144  }
145  else if(dest.id()==ID_code)
146  {
147  code_typet &code_type=to_code_type(dest);
148  rename(code_type.return_type());
149 
150  for(auto &p : code_type.parameters())
151  {
152  if(!rename(p.type()))
153  result=false;
154 
155  expr_mapt::const_iterator e_it = expr_map.find(p.get_identifier());
156 
157  if(e_it!=expr_map.end())
158  {
159  p.set_identifier(e_it->second);
160  result=false;
161  }
162  }
163  }
164  else if(dest.id()==ID_c_enum_tag ||
165  dest.id()==ID_struct_tag ||
166  dest.id()==ID_union_tag)
167  {
168  type_mapt::const_iterator it=
169  type_map.find(to_tag_type(dest).get_identifier());
170 
171  if(it!=type_map.end())
172  {
173  to_tag_type(dest).set_identifier(it->second);
174  result=false;
175  }
176  }
177  else if(dest.id()==ID_array)
178  {
179  array_typet &array_type=to_array_type(dest);
180  if(!rename(array_type.size()))
181  result=false;
182  }
183 
184  return result;
185 }
186 
187 bool rename_symbolt::have_to_rename(const typet &dest) const
188 {
189  if(expr_map.empty() && type_map.empty())
190  return false;
191 
192  if(dest.has_subtype())
193  if(have_to_rename(dest.subtype()))
194  return true;
195 
196  forall_subtypes(it, dest)
197  if(have_to_rename(*it))
198  return true;
199 
200  if(dest.id()==ID_struct ||
201  dest.id()==ID_union)
202  {
203  const struct_union_typet &struct_union_type=
204  to_struct_union_type(dest);
205 
206  for(const auto &c : struct_union_type.components())
207  if(have_to_rename(c))
208  return true;
209  }
210  else if(dest.id()==ID_code)
211  {
212  const code_typet &code_type=to_code_type(dest);
213  if(have_to_rename(code_type.return_type()))
214  return true;
215 
216  for(const auto &p : code_type.parameters())
217  {
218  if(have_to_rename(p.type()))
219  return true;
220 
221  if(expr_map.find(p.get_identifier()) != expr_map.end())
222  return true;
223  }
224  }
225  else if(dest.id()==ID_c_enum_tag ||
226  dest.id()==ID_struct_tag ||
227  dest.id()==ID_union_tag)
228  return type_map.find(to_tag_type(dest).get_identifier())!=type_map.end();
229  else if(dest.id()==ID_array)
230  return have_to_rename(to_array_type(dest).size());
231 
232  return false;
233 }
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
tag_typet::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:446
typet::subtype
const typet & subtype() const
Definition: type.h:47
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
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
rename_symbolt::have_to_rename
bool have_to_rename(const exprt &dest) const
Definition: rename_symbol.cpp:84
typet
The type of an expression, extends irept.
Definition: type.h:29
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
rename_symbolt::expr_map
expr_mapt expr_map
Definition: rename_symbol.h:63
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
exprt
Base class for all expressions.
Definition: expr.h:53
rename_symbolt::rename_symbolt
rename_symbolt()
Definition: rename_symbol.cpp:15
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
rename_symbol.h
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
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
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:475
rename_symbolt::insert
void insert(const class symbol_exprt &old_expr, const class symbol_exprt &new_expr)
Definition: rename_symbol.cpp:23
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
std_types.h
Pre-defined types.
Forall_subtypes
#define Forall_subtypes(it, type)
Definition: type.h:222
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
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
forall_subtypes
#define forall_subtypes(it, type)
Definition: type.h:216
rename_symbolt::~rename_symbolt
virtual ~rename_symbolt()
Definition: rename_symbol.cpp:19
array_typet
Arrays with given size.
Definition: std_types.h:965
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
rename_symbolt::insert_expr
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
rename_symbolt::type_map
type_mapt type_map
Definition: rename_symbol.h:64
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
rename_symbolt::rename
bool rename(exprt &dest) const
Definition: rename_symbol.cpp:30
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
std_expr.h
API to expression classes.
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:106