cprover
Loading...
Searching...
No Matches
field_sensitivity.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-sensitive SSA
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
9#include "field_sensitivity.h"
10
11#include <util/arith_tools.h>
12#include <util/simplify_expr.h>
13#include <util/std_expr.h>
14
15#include "goto_symex_state.h"
16#include "symex_target.h"
17
18#define ENABLE_ARRAY_FIELD_SENSITIVITY
19
21 const namespacet &ns,
22 goto_symex_statet &state,
23 ssa_exprt ssa_expr,
24 bool write) const
25{
26 if(!run_apply || write)
27 return std::move(ssa_expr);
28 else
29 return get_fields(ns, state, ssa_expr);
30}
31
33 const namespacet &ns,
34 goto_symex_statet &state,
35 exprt expr,
36 bool write) const
37{
38 if(!run_apply)
39 return expr;
40
41 if(expr.id() != ID_address_of)
42 {
43 Forall_operands(it, expr)
44 *it = apply(ns, state, std::move(*it), write);
45 }
46
47 if(!write && is_ssa_expr(expr))
48 {
49 return apply(ns, state, to_ssa_expr(expr), write);
50 }
51 else if(
52 !write && expr.id() == ID_member &&
53 to_member_expr(expr).struct_op().id() == ID_struct)
54 {
55 return simplify_expr(std::move(expr), ns);
56 }
57#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
58 else if(
59 !write && expr.id() == ID_index &&
60 to_index_expr(expr).array().id() == ID_array)
61 {
62 return simplify_expr(std::move(expr), ns);
63 }
64#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
65 else if(expr.id() == ID_member)
66 {
67 // turn a member-of-an-SSA-expression into a single SSA expression, thus
68 // encoding the member as an individual symbol rather than only the full
69 // struct
70 member_exprt &member = to_member_expr(expr);
71
72 if(
73 is_ssa_expr(member.struct_op()) &&
74 (member.struct_op().type().id() == ID_struct ||
75 member.struct_op().type().id() == ID_struct_tag))
76 {
77 // place the entire member expression, not just the struct operand, in an
78 // SSA expression
79 ssa_exprt tmp = to_ssa_expr(member.struct_op());
80 bool was_l2 = !tmp.get_level_2().empty();
81
82 tmp.remove_level_2();
83 member.struct_op() = tmp.get_original_expr();
84 tmp.set_expression(member);
85 if(was_l2)
86 return state.rename(std::move(tmp), ns).get();
87 else
88 return std::move(tmp);
89 }
90 }
91#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
92 else if(expr.id() == ID_index)
93 {
94 // turn a index-of-an-SSA-expression into a single SSA expression, thus
95 // encoding the index access into an array as an individual symbol rather
96 // than only the full array
97 index_exprt &index = to_index_expr(expr);
98 simplify(index.index(), ns);
99
100 if(
101 is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
102 index.index().id() == ID_constant)
103 {
104 // place the entire index expression, not just the array operand, in an
105 // SSA expression
106 ssa_exprt tmp = to_ssa_expr(index.array());
107 auto l2_index = state.rename(index.index(), ns);
108 l2_index.simplify(ns);
109 bool was_l2 = !tmp.get_level_2().empty();
110 exprt l2_size =
111 state.rename(to_array_type(index.array().type()).size(), ns).get();
112 if(l2_size.is_nil() && index.array().id() == ID_symbol)
113 {
114 // In case the array type was incomplete, attempt to retrieve it from
115 // the symbol table.
116 const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup(
118 if(array_from_symbol_table != nullptr)
119 l2_size = to_array_type(array_from_symbol_table->type).size();
120 }
121
122 if(
123 l2_size.id() == ID_constant &&
124 numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
126 {
127 if(l2_index.get().id() == ID_constant)
128 {
129 // place the entire index expression, not just the array operand,
130 // in an SSA expression
131 ssa_exprt ssa_array = to_ssa_expr(index.array());
132 ssa_array.remove_level_2();
133 index.array() = ssa_array.get_original_expr();
134 index.index() = l2_index.get();
135 tmp.set_expression(index);
136 if(was_l2)
137 return state.rename(std::move(tmp), ns).get();
138 else
139 return std::move(tmp);
140 }
141 else if(!write)
142 {
143 // Expand the array and return `{array[0]; array[1]; ...}[index]`
144 exprt expanded_array =
145 get_fields(ns, state, to_ssa_expr(index.array()));
146 return index_exprt{std::move(expanded_array), index.index()};
147 }
148 }
149 }
150 }
151#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
152 return expr;
153}
154
156 const namespacet &ns,
157 goto_symex_statet &state,
158 const ssa_exprt &ssa_expr) const
159{
160 if(ssa_expr.type().id() == ID_struct || ssa_expr.type().id() == ID_struct_tag)
161 {
162 const struct_typet &type = to_struct_type(ns.follow(ssa_expr.type()));
163 const struct_union_typet::componentst &components = type.components();
164
166 fields.reserve(components.size());
167
168 const exprt &struct_op = ssa_expr.get_original_expr();
169
170 for(const auto &comp : components)
171 {
172 ssa_exprt tmp = ssa_expr;
173 bool was_l2 = !tmp.get_level_2().empty();
174 tmp.remove_level_2();
175 tmp.set_expression(member_exprt{struct_op, comp.get_name(), comp.type()});
176 if(was_l2)
177 {
178 fields.push_back(state.rename(get_fields(ns, state, tmp), ns).get());
179 }
180 else
181 fields.push_back(get_fields(ns, state, tmp));
182 }
183
184 return struct_exprt(std::move(fields), ssa_expr.type());
185 }
186#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
187 else if(
188 ssa_expr.type().id() == ID_array &&
189 to_array_type(ssa_expr.type()).size().id() == ID_constant)
190 {
191 const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
192 to_constant_expr(to_array_type(ssa_expr.type()).size()));
193 if(mp_array_size < 0 || mp_array_size > max_field_sensitivity_array_size)
194 return ssa_expr;
195
196 const array_typet &type = to_array_type(ssa_expr.type());
197 const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
198
199 array_exprt::operandst elements;
200 elements.reserve(array_size);
201
202 const exprt &array = ssa_expr.get_original_expr();
203
204 for(std::size_t i = 0; i < array_size; ++i)
205 {
206 const index_exprt index(array, from_integer(i, type.index_type()));
207 ssa_exprt tmp = ssa_expr;
208 bool was_l2 = !tmp.get_level_2().empty();
209 tmp.remove_level_2();
210 tmp.set_expression(index);
211 if(was_l2)
212 {
213 elements.push_back(state.rename(get_fields(ns, state, tmp), ns).get());
214 }
215 else
216 elements.push_back(get_fields(ns, state, tmp));
217 }
218
219 return array_exprt(std::move(elements), type);
220 }
221#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
222 else
223 return ssa_expr;
224}
225
227 const namespacet &ns,
228 goto_symex_statet &state,
229 const ssa_exprt &lhs,
230 symex_targett &target,
231 bool allow_pointer_unsoundness)
232{
233 const exprt lhs_fs = apply(ns, state, lhs, false);
234
235 bool run_apply_bak = run_apply;
236 run_apply = false;
238 ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
239 run_apply = run_apply_bak;
240}
241
253 const namespacet &ns,
254 goto_symex_statet &state,
255 const exprt &lhs_fs,
256 const exprt &lhs,
257 symex_targett &target,
258 bool allow_pointer_unsoundness)
259{
260 if(lhs == lhs_fs)
261 return;
262 else if(is_ssa_expr(lhs_fs))
263 {
264 exprt ssa_rhs = state.rename(lhs, ns).get();
265 simplify(ssa_rhs, ns);
266
267 const ssa_exprt ssa_lhs = state
268 .assignment(
269 to_ssa_expr(lhs_fs),
270 ssa_rhs,
271 ns,
272 true,
273 true,
274 allow_pointer_unsoundness)
275 .get();
276
277 // do the assignment
278 target.assignment(
279 state.guard.as_expr(),
280 ssa_lhs,
281 ssa_lhs,
282 ssa_lhs.get_original_expr(),
283 ssa_rhs,
284 state.source,
286 }
287 else if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
288 {
289 const struct_typet &type = to_struct_type(ns.follow(lhs.type()));
290 const struct_union_typet::componentst &components = type.components();
291
293 components.empty() ||
294 (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
295
296 exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
297 for(const auto &comp : components)
298 {
299 const member_exprt member_rhs(lhs, comp.get_name(), comp.type());
300 const exprt &member_lhs = *fs_it;
301
303 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
304 ++fs_it;
305 }
306 }
307#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
308 else if(const auto &type = type_try_dynamic_cast<array_typet>(lhs.type()))
309 {
310 const std::size_t array_size =
311 numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
312 PRECONDITION(lhs_fs.operands().size() == array_size);
313
314 if(array_size > max_field_sensitivity_array_size)
315 return;
316
317 exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
318 for(std::size_t i = 0; i < array_size; ++i)
319 {
320 const index_exprt index_rhs(lhs, from_integer(i, type->index_type()));
321 const exprt &index_lhs = *fs_it;
322
324 ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
325 ++fs_it;
326 }
327 }
328#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
329 else if(lhs_fs.has_operands())
330 {
332 lhs.has_operands() && lhs_fs.operands().size() == lhs.operands().size());
333
334 exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
335 for(const exprt &op : lhs.operands())
336 {
338 ns, state, *fs_it, op, target, allow_pointer_unsoundness);
339 ++fs_it;
340 }
341 }
342 else
343 {
345 }
346}
347
349{
350 if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
351 return true;
352
353#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
354 if(
355 expr.type().id() == ID_array &&
356 to_array_type(expr.type()).size().id() == ID_constant &&
357 numeric_cast_v<mp_integer>(to_constant_expr(
359 {
360 return true;
361 }
362#endif
363
364 return false;
365}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:33
const exprt & size() const
Definition: std_types.h:790
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
bool run_apply
whether or not to invoke field_sensitivityt::apply
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
Assign to the individual fields of a non-expanded symbol lhs.
void field_assignments_rec(const namespacet &ns, goto_symex_statet &state, const exprt &lhs_fs, const exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
Assign to the individual fields lhs_fs of a non-expanded symbol lhs.
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
const std::size_t max_field_sensitivity_array_size
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
guardt guard
Definition: goto_state.h:58
Central data structure: state.
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
symex_targett::sourcet source
exprt as_expr() const
Definition: guard_expr.h:46
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void remove_level_2()
Definition: ssa_expr.cpp:198
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
Definition: ssa_expr.cpp:137
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
Struct constructor from list of elements.
Definition: std_expr.h:1722
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
Write to a local variable.
#define Forall_operands(it, expr)
Definition: expr.h:25
Symbolic Execution.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
Generate Equation using Symbolic Execution.