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 symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
22 {
23  // already renamed?
24  if(!ssa_expr.get_level_0().empty())
25  return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
26 
27  const irep_idt &obj_identifier = ssa_expr.get_object_name();
28 
29  // guards are not L0-renamed
30  if(obj_identifier == goto_symex_statet::guard_identifier())
31  return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
32 
33  const symbolt *s;
34  const bool found_l0 = !ns.lookup(obj_identifier, s);
35  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
36 
37  // don't rename shared variables or functions
38  if(s->type.id() == ID_code || s->is_shared())
39  return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
40 
41  // rename!
42  ssa_expr.set_level_0(thread_nr);
43  return renamedt<ssa_exprt, L0>{ssa_expr};
44 }
45 
47  const renamedt<ssa_exprt, L0> &ssa,
48  std::size_t index)
49 {
51  ssa.get().get_identifier(), std::make_pair(ssa.get(), index));
52 }
53 
55  const renamedt<ssa_exprt, L0> &ssa,
56  std::size_t index)
57 {
58  const irep_idt &identifier = ssa.get().get_identifier();
59  const auto old_value = current_names.find(identifier);
60  if(old_value)
61  {
62  std::pair<ssa_exprt, std::size_t> result = *old_value;
63  current_names.replace(identifier, std::make_pair(ssa.get(), index));
64  return result;
65  }
66  current_names.insert(identifier, std::make_pair(ssa.get(), index));
67  return {};
68 }
69 
71 {
72  return current_names.has_key(ssa.get().get_identifier());
73 }
74 
77 {
78  if(
79  !l0_expr.get().get_level_1().empty() ||
80  !l0_expr.get().get_level_2().empty())
81  {
82  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
83  }
84 
85  const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
86 
87  const auto r_opt = current_names.find(l0_name);
88 
89  if(!r_opt)
90  {
91  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
92  }
93 
94  // rename!
95  l0_expr.value().set_level_1(r_opt->get().second);
96  return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
97 }
98 
100 operator()(renamedt<ssa_exprt, L1> l1_expr) const
101 {
102  if(!l1_expr.get().get_level_2().empty())
103  return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
104  l1_expr.value().set_level_2(latest_index(l1_expr.get().get_identifier()));
105  return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
106 }
107 
109 {
111  other.current_names.get_delta_view(current_names, delta_view, false);
112 
113  for(const auto &delta_item : delta_view)
114  {
115  if(!delta_item.is_in_both_maps())
116  {
117  current_names.insert(delta_item.k, delta_item.m);
118  }
119  else
120  {
121  if(delta_item.m != delta_item.get_other_map_value())
122  {
123  current_names.replace(delta_item.k, delta_item.m);
124  }
125  }
126  }
127 }
128 
129 unsigned symex_level2t::latest_index(const irep_idt &identifier) const
130 {
131  const auto r_opt = current_names.find(identifier);
132  return !r_opt ? 0 : r_opt->get().second;
133 }
134 
136  const irep_idt &l1_identifier,
137  const ssa_exprt &lhs,
138  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
139 {
140  const std::size_t n = fresh_l2_name_provider(l1_identifier);
141 
142  if(const auto r_opt = current_names.find(l1_identifier))
143  {
144  std::pair<ssa_exprt, std::size_t> copy = r_opt->get();
145  copy.second = n;
146  current_names.replace(l1_identifier, std::move(copy));
147  }
148  else
149  {
150  current_names.insert(l1_identifier, std::make_pair(lhs, n));
151  }
152 
153  return n;
154 }
155 
157 {
158  expr.type() = get_original_name(std::move(expr.type()));
159 
160  if(is_ssa_expr(expr))
161  return to_ssa_expr(expr).get_original_expr();
162  else
163  {
164  Forall_operands(it, expr)
165  *it = get_original_name(std::move(*it));
166  return expr;
167  }
168 }
169 
171 {
172  // rename all the symbols with their last known value
173 
174  if(type.id() == ID_array)
175  {
176  auto &array_type = to_array_type(type);
177  array_type.subtype() = get_original_name(std::move(array_type.subtype()));
178  array_type.size() = get_original_name(std::move(array_type.size()));
179  }
180  else if(type.id() == ID_struct || type.id() == ID_union)
181  {
182  struct_union_typet &s_u_type = to_struct_union_type(type);
183  struct_union_typet::componentst &components = s_u_type.components();
184 
185  for(auto &component : components)
186  component.type() = get_original_name(std::move(component.type()));
187  }
188  else if(type.id() == ID_pointer)
189  {
190  type.subtype() =
191  get_original_name(std::move(to_pointer_type(type).subtype()));
192  }
193  return type;
194 }
195 
196 bool check_renaming(const typet &type)
197 {
198  if(type.id() == ID_array)
199  return check_renaming(to_array_type(type).size());
200  else if(type.id() == ID_struct || type.id() == ID_union)
201  {
202  for(const auto &c : to_struct_union_type(type).components())
203  if(check_renaming(c.type()))
204  return true;
205  }
206  else if(type.has_subtype())
207  return check_renaming(to_type_with_subtype(type).subtype());
208 
209  return false;
210 }
211 
212 bool check_renaming_l1(const exprt &expr)
213 {
214  if(check_renaming(expr.type()))
215  return true;
216 
217  if(expr.id() == ID_symbol)
218  {
219  const auto &type = expr.type();
220  if(!expr.get_bool(ID_C_SSA_symbol))
221  return type.id() != ID_code && type.id() != ID_mathematical_function;
222  if(!to_ssa_expr(expr).get_level_2().empty())
223  return true;
224  if(to_ssa_expr(expr).get_original_expr().type() != type)
225  return true;
226  }
227  else
228  {
229  forall_operands(it, expr)
230  if(check_renaming_l1(*it))
231  return true;
232  }
233 
234  return false;
235 }
236 
237 bool check_renaming(const exprt &expr)
238 {
239  if(check_renaming(expr.type()))
240  return true;
241 
242  if(
243  expr.id() == ID_address_of &&
244  to_address_of_expr(expr).object().id() == ID_symbol)
245  {
246  return check_renaming_l1(to_address_of_expr(expr).object());
247  }
248  else if(
249  expr.id() == ID_address_of &&
250  to_address_of_expr(expr).object().id() == ID_index)
251  {
252  const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
253  return check_renaming_l1(index_expr.array()) ||
254  check_renaming(index_expr.index());
255  }
256  else if(expr.id() == ID_symbol)
257  {
258  const auto &type = expr.type();
259  if(!expr.get_bool(ID_C_SSA_symbol))
260  return type.id() != ID_code && type.id() != ID_mathematical_function;
261  if(to_ssa_expr(expr).get_level_2().empty())
262  return true;
263  if(to_ssa_expr(expr).get_original_expr().type() != type)
264  return true;
265  }
266  else if(expr.id() == ID_nil)
267  {
268  return expr != nil_exprt{};
269  }
270  else
271  {
272  forall_operands(it, expr)
273  if(check_renaming(*it))
274  return true;
275  }
276 
277  return false;
278 }
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:439
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
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:936
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:212
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
symex_level1t::restore_from
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
Definition: renaming_level.cpp:108
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:100
ssa_exprt::get_level_0
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
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:1297
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
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:154
exprt
Base class for all expressions.
Definition: expr.h:54
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:55
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:135
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:21
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:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
renaming_level.h
Renaming levels.
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
symex_level1t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:69
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:156
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:407
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:46
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:1533
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:377
sharing_mapt::insert
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
Definition: sharing_map.h:1346
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:1423
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
Symbolic Execution.
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:77
symbolt
Symbol table entry.
Definition: symbol.h:28
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:196
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
symex_level1t
Functor to set the level 1 renaming of SSA expressions.
Definition: renaming_level.h:47
symex_level1t::has
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
Definition: renaming_level.cpp:70
symex_level1t::operator()
renamedt< ssa_exprt, L1 > operator()(renamedt< ssa_exprt, L0 > l0_expr) const
Definition: renaming_level.cpp:76
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
symex_level2t::latest_index
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.cpp:129
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
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:27
sharing_mapt::find
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1449
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:54