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 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
static irep_idt guard_identifier()
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
The NIL expression.
Definition: std_expr.h:2735
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
const underlyingt & get() const
Definition: renamed.h:34
underlyingt & value()
Definition: renamed.h:48
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
Definition: sharing_map.h:1346
bool has_key(const key_type &k) const
Check if key is in map.
Definition: sharing_map.h:377
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
Definition: sharing_map.h:1423
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Definition: sharing_map.h:439
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1449
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
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
void set_level_0(std::size_t i)
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
irep_idt get_object_name() const
Base type for structs and unions.
Definition: std_types.h:57
const componentst & components() const
Definition: std_types.h:142
std::vector< componentt > componentst
Definition: std_types.h:135
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
bool is_shared() const
Definition: symbol.h:95
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
bool has_subtype() const
Definition: type.h:65
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
Symbolic Execution.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
nonstd::optional< T > optionalt
Definition: optional.h:35
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
exprt get_original_name(exprt expr)
Undo all levels of 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.
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.
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.
Renaming levels.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
Functor to set the level 1 renaming of SSA expressions.
symex_renaming_levelt current_names
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
renamedt< ssa_exprt, L1 > operator()(renamedt< ssa_exprt, L0 > l0_expr) const
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
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.
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
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.
symex_renaming_levelt current_names
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...
Symbol table entry.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:154