cprover
Loading...
Searching...
No Matches
renaming_level.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
11
12#include "renaming_level.h"
13
14#include <util/namespace.h>
15#include <util/pointer_expr.h>
16#include <util/ssa_expr.h>
17#include <util/symbol.h>
18
19#include "goto_symex_state.h"
20
22symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
23{
24 // already renamed?
25 if(!ssa_expr.get_level_0().empty())
26 return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
27
28 const irep_idt &obj_identifier = ssa_expr.get_object_name();
29
30 // guards are not L0-renamed
31 if(obj_identifier == goto_symex_statet::guard_identifier())
32 return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
33
34 const symbolt *s;
35 const bool found_l0 = !ns.lookup(obj_identifier, s);
36 INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
37
38 // don't rename shared variables or functions
39 if(s->type.id() == ID_code || s->is_shared())
40 return renamedt<ssa_exprt, L0>{std::move(ssa_expr)};
41
42 // rename!
43 ssa_expr.set_level_0(thread_nr);
44 return renamedt<ssa_exprt, L0>{ssa_expr};
45}
46
48 const renamedt<ssa_exprt, L0> &ssa,
49 std::size_t index)
50{
52 ssa.get().get_identifier(), std::make_pair(ssa.get(), index));
53}
54
56 const renamedt<ssa_exprt, L0> &ssa,
57 std::size_t index)
58{
59 const irep_idt &identifier = ssa.get().get_identifier();
60 const auto old_value = current_names.find(identifier);
61 if(old_value)
62 {
63 std::pair<ssa_exprt, std::size_t> result = *old_value;
64 current_names.replace(identifier, std::make_pair(ssa.get(), index));
65 return result;
66 }
67 current_names.insert(identifier, std::make_pair(ssa.get(), index));
68 return {};
69}
70
72{
73 return current_names.has_key(ssa.get().get_identifier());
74}
75
78{
79 if(
80 !l0_expr.get().get_level_1().empty() ||
81 !l0_expr.get().get_level_2().empty())
82 {
83 return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
84 }
85
86 const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
87
88 const auto r_opt = current_names.find(l0_name);
89
90 if(!r_opt)
91 {
92 return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
93 }
94
95 // rename!
96 l0_expr.value().set_level_1(r_opt->get().second);
97 return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
98}
99
102{
103 if(!l1_expr.get().get_level_2().empty())
104 return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
105 l1_expr.value().set_level_2(latest_index(l1_expr.get().get_identifier()));
106 return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
107}
108
110{
112 other.current_names.get_delta_view(current_names, delta_view, false);
113
114 for(const auto &delta_item : delta_view)
115 {
116 if(!delta_item.is_in_both_maps())
117 {
118 current_names.insert(delta_item.k, delta_item.m);
119 }
120 else
121 {
122 if(delta_item.m != delta_item.get_other_map_value())
123 {
124 current_names.replace(delta_item.k, delta_item.m);
125 }
126 }
127 }
128}
129
130unsigned symex_level2t::latest_index(const irep_idt &identifier) const
131{
132 const auto r_opt = current_names.find(identifier);
133 return !r_opt ? 0 : r_opt->get().second;
134}
135
137 const irep_idt &l1_identifier,
138 const ssa_exprt &lhs,
139 std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
140{
141 const std::size_t n = fresh_l2_name_provider(l1_identifier);
142
143 if(const auto r_opt = current_names.find(l1_identifier))
144 {
145 std::pair<ssa_exprt, std::size_t> copy = r_opt->get();
146 copy.second = n;
147 current_names.replace(l1_identifier, std::move(copy));
148 }
149 else
150 {
151 current_names.insert(l1_identifier, std::make_pair(lhs, n));
152 }
153
154 return n;
155}
156
158{
159 expr.type() = get_original_name(std::move(expr.type()));
160
161 if(is_ssa_expr(expr))
162 return to_ssa_expr(expr).get_original_expr();
163 else
164 {
165 Forall_operands(it, expr)
166 *it = get_original_name(std::move(*it));
167 return expr;
168 }
169}
170
172{
173 // rename all the symbols with their last known value
174
175 if(type.id() == ID_array)
176 {
177 auto &array_type = to_array_type(type);
178 array_type.element_type() =
179 get_original_name(std::move(array_type.element_type()));
180 array_type.size() = get_original_name(std::move(array_type.size()));
181 }
182 else if(type.id() == ID_struct || type.id() == ID_union)
183 {
185 struct_union_typet::componentst &components = s_u_type.components();
186
187 for(auto &component : components)
188 component.type() = get_original_name(std::move(component.type()));
189 }
190 else if(type.id() == ID_pointer)
191 {
192 to_pointer_type(type).base_type() =
193 get_original_name(std::move(to_pointer_type(type).base_type()));
194 }
195 return type;
196}
197
198bool check_renaming(const typet &type)
199{
200 if(type.id() == ID_array)
201 return check_renaming(to_array_type(type).size());
202 else if(type.id() == ID_struct || type.id() == ID_union)
203 {
204 for(const auto &c : to_struct_union_type(type).components())
205 if(check_renaming(c.type()))
206 return true;
207 }
208 else if(type.has_subtype())
209 return check_renaming(to_type_with_subtype(type).subtype());
210
211 return false;
212}
213
214bool check_renaming_l1(const exprt &expr)
215{
216 if(check_renaming(expr.type()))
217 return true;
218
219 if(expr.id() == ID_symbol)
220 {
221 const auto &type = expr.type();
222 if(!expr.get_bool(ID_C_SSA_symbol))
223 return type.id() != ID_code && type.id() != ID_mathematical_function;
224 if(!to_ssa_expr(expr).get_level_2().empty())
225 return true;
226 if(to_ssa_expr(expr).get_original_expr().type() != type)
227 return true;
228 }
229 else
230 {
231 forall_operands(it, expr)
232 if(check_renaming_l1(*it))
233 return true;
234 }
235
236 return false;
237}
238
239bool check_renaming(const exprt &expr)
240{
241 if(check_renaming(expr.type()))
242 return true;
243
244 if(
245 expr.id() == ID_address_of &&
246 to_address_of_expr(expr).object().id() == ID_symbol)
247 {
248 return check_renaming_l1(to_address_of_expr(expr).object());
249 }
250 else if(
251 expr.id() == ID_address_of &&
252 to_address_of_expr(expr).object().id() == ID_index)
253 {
254 const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
255 return check_renaming_l1(index_expr.array()) ||
256 check_renaming(index_expr.index());
257 }
258 else if(expr.id() == ID_symbol)
259 {
260 const auto &type = expr.type();
261 if(!expr.get_bool(ID_C_SSA_symbol))
262 return type.id() != ID_code && type.id() != ID_mathematical_function;
263 if(to_ssa_expr(expr).get_level_2().empty())
264 return true;
265 if(to_ssa_expr(expr).get_original_expr().type() != type)
266 return true;
267 }
268 else if(expr.id() == ID_nil)
269 {
270 return expr != nil_exprt{};
271 }
272 else
273 {
274 forall_operands(it, expr)
275 if(check_renaming(*it))
276 return true;
277 }
278
279 return false;
280}
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
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_idt &name) const
Definition: irep.cpp:58
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
underlyingt & value()
Definition: renamed.h:54
const underlyingt & get() const
Definition: renamed.h:40
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
Definition: sharing_map.h:1348
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:1425
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:1451
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:939
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
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
void set_level_0(std::size_t i)
Definition: ssa_expr.cpp:180
irep_idt get_object_name() const
Definition: ssa_expr.cpp:144
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
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:29
bool has_subtype() const
Definition: type.h:66
#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:47
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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:423
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
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:177