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