cprover
renaming_level.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "renaming_level.h"
13 
14 #include <util/namespace.h>
15 #include <util/ssa_expr.h>
16 #include <util/symbol.h>
17 
18 #include "goto_symex_state.h"
19 
21  const symex_renaming_levelt &current_names,
22  std::unordered_set<ssa_exprt, irep_hash> &vars)
23 {
25  current_names.get_view(view);
26 
27  for(const auto &pair : view)
28  {
29  vars.insert(pair.second.first);
30  }
31 }
32 
34 symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
35 {
36  // already renamed?
37  if(!ssa_expr.get_level_0().empty())
38  return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
39 
40  const irep_idt &obj_identifier = ssa_expr.get_object_name();
41 
42  // guards are not L0-renamed
43  if(obj_identifier == goto_symex_statet::guard_identifier())
44  return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
45 
46  const symbolt *s;
47  const bool found_l0 = !ns.lookup(obj_identifier, s);
48  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
49 
50  // don't rename shared variables or functions
51  if(s->type.id() == ID_code || s->is_shared())
52  return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
53 
54  // rename!
55  ssa_expr.set_level_0(thread_nr);
56  return renamedt<ssa_exprt, L0>{ssa_expr};
57 }
58 
60  const renamedt<ssa_exprt, L0> &ssa,
61  std::size_t index)
62 {
64  ssa.get().get_identifier(), std::make_pair(ssa.get(), index));
65 }
66 
68  const renamedt<ssa_exprt, L0> &ssa,
69  std::size_t index)
70 {
71  const irep_idt &identifier = ssa.get().get_identifier();
72  const auto old_value = current_names.find(identifier);
73  if(old_value)
74  {
75  std::pair<ssa_exprt, std::size_t> result = *old_value;
76  current_names.replace(identifier, std::make_pair(ssa.get(), index));
77  return result;
78  }
79  current_names.insert(identifier, std::make_pair(ssa.get(), index));
80  return {};
81 }
82 
84 {
85  return current_names.has_key(ssa.get().get_identifier());
86 }
87 
90 {
91  if(
92  !l0_expr.get().get_level_1().empty() ||
93  !l0_expr.get().get_level_2().empty())
94  {
95  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
96  }
97 
98  const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
99 
100  const auto r_opt = current_names.find(l0_name);
101 
102  if(!r_opt)
103  {
104  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
105  }
106 
107  // rename!
108  l0_expr.value().set_level_1(r_opt->get().second);
109  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
110 }
111 
114 {
115  if(!l1_expr.get().get_level_2().empty())
116  return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
117  l1_expr.value().set_level_2(latest_index(l1_expr.get().get_identifier()));
118  return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
119 }
120 
122 {
124  other.current_names.get_delta_view(current_names, delta_view, false);
125 
126  for(const auto &delta_item : delta_view)
127  {
128  if(!delta_item.is_in_both_maps())
129  {
130  current_names.insert(delta_item.k, delta_item.m);
131  }
132  else
133  {
134  if(delta_item.m != delta_item.get_other_map_value())
135  {
136  current_names.replace(delta_item.k, delta_item.m);
137  }
138  }
139  }
140 }
141 
142 unsigned symex_level2t::latest_index(const irep_idt &identifier) const
143 {
144  const auto r_opt = current_names.find(identifier);
145  return !r_opt ? 0 : r_opt->get().second;
146 }
147 
149  const irep_idt &l1_identifier,
150  const ssa_exprt &lhs,
151  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
152 {
153  const std::size_t n = fresh_l2_name_provider(l1_identifier);
154 
155  if(const auto r_opt = current_names.find(l1_identifier))
156  {
157  std::pair<ssa_exprt, std::size_t> copy = r_opt->get();
158  copy.second = n;
159  current_names.replace(l1_identifier, std::move(copy));
160  }
161  else
162  {
163  current_names.insert(l1_identifier, std::make_pair(lhs, n));
164  }
165 
166  return n;
167 }
168 
170 {
171  expr.type() = get_original_name(std::move(expr.type()));
172 
173  if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol))
174  return to_ssa_expr(expr).get_original_expr();
175  else
176  {
177  Forall_operands(it, expr)
178  *it = get_original_name(std::move(*it));
179  return expr;
180  }
181 }
182 
184 {
185  // rename all the symbols with their last known value
186 
187  if(type.id() == ID_array)
188  {
189  auto &array_type = to_array_type(type);
190  array_type.subtype() = get_original_name(std::move(array_type.subtype()));
191  array_type.size() = get_original_name(std::move(array_type.size()));
192  }
193  else if(type.id() == ID_struct || type.id() == ID_union)
194  {
195  struct_union_typet &s_u_type = to_struct_union_type(type);
196  struct_union_typet::componentst &components = s_u_type.components();
197 
198  for(auto &component : components)
199  component.type() = get_original_name(std::move(component.type()));
200  }
201  else if(type.id() == ID_pointer)
202  {
203  type.subtype() =
204  get_original_name(std::move(to_pointer_type(type).subtype()));
205  }
206  return type;
207 }
208 
209 bool check_renaming(const typet &type)
210 {
211  if(type.id() == ID_array)
212  return check_renaming(to_array_type(type).size());
213  else if(type.id() == ID_struct || type.id() == ID_union)
214  {
215  for(const auto &c : to_struct_union_type(type).components())
216  if(check_renaming(c.type()))
217  return true;
218  }
219  else if(type.has_subtype())
221 
222  return false;
223 }
224 
225 bool check_renaming_l1(const exprt &expr)
226 {
227  if(check_renaming(expr.type()))
228  return true;
229 
230  if(expr.id() == ID_symbol)
231  {
232  const auto &type = expr.type();
233  if(!expr.get_bool(ID_C_SSA_symbol))
234  return type.id() != ID_code && type.id() != ID_mathematical_function;
235  if(!to_ssa_expr(expr).get_level_2().empty())
236  return true;
237  if(to_ssa_expr(expr).get_original_expr().type() != type)
238  return true;
239  }
240  else
241  {
242  forall_operands(it, expr)
243  if(check_renaming_l1(*it))
244  return true;
245  }
246 
247  return false;
248 }
249 
250 bool check_renaming(const exprt &expr)
251 {
252  if(check_renaming(expr.type()))
253  return true;
254 
255  if(
256  expr.id() == ID_address_of &&
257  to_address_of_expr(expr).object().id() == ID_symbol)
258  {
259  return check_renaming_l1(to_address_of_expr(expr).object());
260  }
261  else if(
262  expr.id() == ID_address_of &&
263  to_address_of_expr(expr).object().id() == ID_index)
264  {
265  const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
266  return check_renaming_l1(index_expr.array()) ||
267  check_renaming(index_expr.index());
268  }
269  else if(expr.id() == ID_symbol)
270  {
271  const auto &type = expr.type();
272  if(!expr.get_bool(ID_C_SSA_symbol))
273  return type.id() != ID_code && type.id() != ID_mathematical_function;
274  if(to_ssa_expr(expr).get_level_2().empty())
275  return true;
276  if(to_ssa_expr(expr).get_original_expr().type() != type)
277  return true;
278  }
279  else
280  {
281  forall_operands(it, expr)
282  if(check_renaming(*it))
283  return true;
284  }
285 
286  return false;
287 }
sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >::delta_viewt
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Definition: sharing_map.h:405
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:36
ssa_exprt::set_level_0
void set_level_0(std::size_t i)
sharing_mapt::get_delta_view
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
Definition: sharing_map.h:881
typet::subtype
const typet & subtype() const
Definition: type.h:47
check_renaming_l1
bool check_renaming_l1(const exprt &expr)
Check that expr is correctly renamed to level 1 and return true in case an error is detected.
Definition: renaming_level.cpp:225
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
symex_level1t::restore_from
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
Definition: renaming_level.cpp:121
symex_level2t::operator()
renamedt< ssa_exprt, L2 > operator()(renamedt< ssa_exprt, L1 > l1_expr) const
Set L2 tag to correspond to the current count of the identifier of l1_expr's.
Definition: renaming_level.cpp:113
ssa_exprt::get_level_0
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >
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
goto_symex_statet::guard_identifier
static irep_idt guard_identifier()
Definition: goto_symex_state.h:141
typet
The type of an expression, extends irept.
Definition: type.h:28
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symex_statet::fresh_l2_name_provider
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
Definition: goto_symex_state.h:260
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:162
exprt
Base class for all expressions.
Definition: expr.h:52
ssa_exprt::get_object_name
irep_idt get_object_name() const
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
symex_level2t::increase_generation
std::size_t increase_generation(const irep_idt &l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this pat...
Definition: renaming_level.cpp:148
symex_level0
renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
Set the level 0 renaming of SSA expressions.
Definition: renaming_level.cpp:34
namespace.h
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
renamedt::get
const underlyingt & get() const
Definition: renamed.h:34
ssa_exprt::set_level_1
void set_level_1(std::size_t i)
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >::viewt
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Definition: sharing_map.h:365
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
renaming_level.h
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symex_level1t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:75
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
get_variables
void get_variables(const symex_renaming_levelt &current_names, std::unordered_set< ssa_exprt, irep_hash > &vars)
Definition: renaming_level.cpp:20
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:169
symbol.h
Symbol table entry.
symbolt::is_shared
bool is_shared() const
Definition: symbol.h:95
irept::id
const irep_idt & id() const
Definition: irep.h:418
symex_level1t::insert
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
Definition: renaming_level.cpp:59
dstringt::empty
bool empty() const
Definition: dstring.h:88
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
sharing_mapt::has_key
bool has_key(const key_type &k) const
Check if key is in map.
Definition: sharing_map.h:354
sharing_mapt::insert
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
Definition: sharing_map.h:1282
sharing_mapt::get_view
void get_view(viewt &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
Definition: sharing_map.h:782
ssa_expr.h
sharing_mapt::replace
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
Definition: sharing_map.h:1359
ssa_exprt::get_l1_object_identifier
const irep_idt get_l1_object_identifier() const
ssa_exprt::set_level_2
void set_level_2(std::size_t i)
goto_symex_state.h
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:83
symbolt
Symbol table entry.
Definition: symbol.h:27
ssa_exprt::get_level_1
const irep_idt get_level_1() const
Definition: ssa_expr.h:68
check_renaming
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
Definition: renaming_level.cpp:209
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
symex_level1t
Functor to set the level 1 renaming of SSA expressions.
Definition: renaming_level.h:52
symex_level1t::has
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
Definition: renaming_level.cpp:83
symex_level1t::operator()
renamedt< ssa_exprt, L1 > operator()(renamedt< ssa_exprt, L0 > l0_expr) const
Definition: renaming_level.cpp:89
symex_level2t::latest_index
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.cpp:142
renamedt::value
underlyingt & value()
Definition: renamed.h:48
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:26
validation_modet::INVARIANT
sharing_mapt::find
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1385
symex_level1t::insert_or_replace
optionalt< std::pair< ssa_exprt, std::size_t > > insert_or_replace(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Set the index for ssa to index.
Definition: renaming_level.cpp:67