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
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);
45}
46
49 std::size_t index)
50{
52 ssa.get().get_identifier(), std::make_pair(ssa.get(), index));
53}
54
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{
113
114 for(const auto &delta_item : delta_view)
115 {
116 if(!delta_item.is_in_both_maps())
117 {
119 }
120 else
121 {
122 if(delta_item.m != delta_item.get_other_map_value())
123 {
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 for(const auto &op : expr.operands())
232 {
233 if(check_renaming_l1(op))
234 return true;
235 }
236 }
237
238 return false;
239}
240
241bool check_renaming(const exprt &expr)
242{
243 if(check_renaming(expr.type()))
244 return true;
245
246 if(
247 expr.id() == ID_address_of &&
248 to_address_of_expr(expr).object().id() == ID_symbol)
249 {
250 return check_renaming_l1(to_address_of_expr(expr).object());
251 }
252 else if(
253 expr.id() == ID_address_of &&
254 to_address_of_expr(expr).object().id() == ID_index)
255 {
256 const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
257 return check_renaming_l1(index_expr.array()) ||
258 check_renaming(index_expr.index());
259 }
260 else if(expr.id() == ID_symbol)
261 {
262 const auto &type = expr.type();
263 if(!expr.get_bool(ID_C_SSA_symbol))
264 return type.id() != ID_code && type.id() != ID_mathematical_function;
265 if(to_ssa_expr(expr).get_level_2().empty())
266 return true;
267 if(to_ssa_expr(expr).get_original_expr().type() != type)
268 return true;
269 }
270 else if(expr.id() == ID_nil)
271 {
272 return expr != nil_exprt{};
273 }
274 else
275 {
276 for(const auto &op : expr.operands())
277 {
278 if(check_renaming(op))
279 return true;
280 }
281 }
282
283 return false;
284}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
static irep_idt guard_identifier()
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
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().
The NIL expression.
Definition std_expr.h:3026
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
bool has_key(const key_type &k) const
Check if key is in map.
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
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.
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Base type for structs and unions.
Definition std_types.h:62
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:101
The type of an expression, extends irept.
Definition type.h:29
bool has_subtype() const
Definition type.h:64
#define Forall_operands(it, expr)
Definition expr.h:27
Symbolic Execution.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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:77
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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:175