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/byte_operators.h>
13#include <util/c_types.h>
15#include <util/simplify_expr.h>
16
17#include "goto_symex_state.h"
18#include "symex_target.h"
19
20#define ENABLE_ARRAY_FIELD_SENSITIVITY
21
23 const namespacet &ns,
24 goto_symex_statet &state,
25 ssa_exprt ssa_expr,
26 bool write) const
27{
28 if(write)
29 return std::move(ssa_expr);
30 else
31 return get_fields(ns, state, ssa_expr, true);
32}
33
35 const namespacet &ns,
36 goto_symex_statet &state,
37 exprt expr,
38 bool write) const
39{
40 if(expr.id() != ID_address_of)
41 {
42 Forall_operands(it, expr)
43 *it = apply(ns, state, std::move(*it), write);
44 }
45
46 if(!write && is_ssa_expr(expr))
47 {
48 return get_fields(ns, state, to_ssa_expr(expr), true);
49 }
50 else if(
51 !write && expr.id() == ID_member &&
52 to_member_expr(expr).struct_op().id() == ID_struct)
53 {
54 return simplify_opt(std::move(expr), ns);
55 }
56#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
57 else if(
58 !write && expr.id() == ID_index &&
59 to_index_expr(expr).array().id() == ID_array)
60 {
61 return simplify_opt(std::move(expr), ns);
62 }
63#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
64 else if(expr.id() == ID_member)
65 {
66 // turn a member-of-an-SSA-expression into a single SSA expression, thus
67 // encoding the member as an individual symbol rather than only the full
68 // struct
69 member_exprt &member = to_member_expr(expr);
70
71 if(
72 is_ssa_expr(member.struct_op()) &&
73 (member.struct_op().type().id() == ID_struct ||
74 member.struct_op().type().id() == ID_struct_tag ||
75 member.struct_op().type().id() == ID_union ||
76 member.struct_op().type().id() == ID_union_tag))
77 {
78 // place the entire member expression, not just the struct operand, in an
79 // SSA expression
80 ssa_exprt tmp = to_ssa_expr(member.struct_op());
81 bool was_l2 = !tmp.get_level_2().empty();
82
83 tmp.remove_level_2();
84 member.struct_op() = tmp.get_original_expr();
85 tmp.set_expression(member);
86 if(was_l2)
87 return apply(ns, state, state.rename(std::move(tmp), ns).get(), write);
88 else
89 return apply(ns, state, std::move(tmp), write);
90 }
91 }
92 else if(
93 !write && (expr.id() == ID_byte_extract_little_endian ||
94 expr.id() == ID_byte_extract_big_endian))
95 {
97 if(
98 (be.op().type().id() == ID_union ||
99 be.op().type().id() == ID_union_tag) &&
100 is_ssa_expr(be.op()) && be.offset().is_constant())
101 {
102 const union_typet &type = to_union_type(ns.follow(be.op().type()));
103 for(const auto &comp : type.components())
104 {
105 ssa_exprt tmp = to_ssa_expr(be.op());
106 bool was_l2 = !tmp.get_level_2().empty();
107 tmp.remove_level_2();
108 const member_exprt member{tmp.get_original_expr(), comp};
109 auto recursive_member =
110 get_subexpression_at_offset(member, be.offset(), be.type(), ns);
111 if(
112 recursive_member.has_value() &&
113 (recursive_member->id() == ID_member ||
114 recursive_member->id() == ID_index))
115 {
116 tmp.type() = be.type();
117 tmp.set_expression(*recursive_member);
118 if(was_l2)
119 {
120 return apply(
121 ns, state, state.rename(std::move(tmp), ns).get(), write);
122 }
123 else
124 return apply(ns, state, std::move(tmp), write);
125 }
126 else if(
127 recursive_member.has_value() && recursive_member->id() == ID_typecast)
128 {
129 if(was_l2)
130 {
131 return apply(
132 ns,
133 state,
134 state.rename(std::move(*recursive_member), ns).get(),
135 write);
136 }
137 else
138 return apply(ns, state, std::move(*recursive_member), write);
139 }
140 }
141 }
142 }
143#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
144 else if(expr.id() == ID_index)
145 {
146 // turn a index-of-an-SSA-expression into a single SSA expression, thus
147 // encoding the index access into an array as an individual symbol rather
148 // than only the full array
149 index_exprt &index = to_index_expr(expr);
151 simplify(index.index(), ns);
152
153 if(
154 is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
155 index.index().is_constant())
156 {
157 // place the entire index expression, not just the array operand, in an
158 // SSA expression
159 ssa_exprt tmp = to_ssa_expr(index.array());
160 auto l2_index = state.rename(index.index(), ns);
162 l2_index.simplify(ns);
163 bool was_l2 = !tmp.get_level_2().empty();
164 exprt l2_size =
165 state.rename(to_array_type(index.array().type()).size(), ns).get();
166 if(l2_size.is_nil() && index.array().id() == ID_symbol)
167 {
168 // In case the array type was incomplete, attempt to retrieve it from
169 // the symbol table.
170 const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup(
172 if(array_from_symbol_table != nullptr)
173 l2_size = to_array_type(array_from_symbol_table->type).size();
174 }
175
176 if(
177 l2_size.is_constant() &&
180 {
181 if(l2_index.get().is_constant())
182 {
183 // place the entire index expression, not just the array operand,
184 // in an SSA expression
185 ssa_exprt ssa_array = to_ssa_expr(index.array());
186 ssa_array.remove_level_2();
187 index.array() = ssa_array.get_original_expr();
188 index.index() = l2_index.get();
189 tmp.set_expression(index);
190 if(was_l2)
191 {
192 return apply(
193 ns, state, state.rename(std::move(tmp), ns).get(), write);
194 }
195 else
196 return apply(ns, state, std::move(tmp), write);
197 }
198 else if(!write)
199 {
200 // Expand the array and return `{array[0]; array[1]; ...}[index]`
201 exprt expanded_array =
202 get_fields(ns, state, to_ssa_expr(index.array()), true);
203 return index_exprt{std::move(expanded_array), index.index()};
204 }
205 }
206 }
207 }
208#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
209 return expr;
210}
211
213 const namespacet &ns,
214 goto_symex_statet &state,
215 const ssa_exprt &ssa_expr,
216 bool disjoined_fields_only) const
217{
218 if(
219 ssa_expr.type().id() == ID_struct ||
220 ssa_expr.type().id() == ID_struct_tag ||
221 (!disjoined_fields_only && (ssa_expr.type().id() == ID_union ||
222 ssa_expr.type().id() == ID_union_tag)))
223 {
224 const struct_union_typet &type =
225 to_struct_union_type(ns.follow(ssa_expr.type()));
226 const struct_union_typet::componentst &components = type.components();
227
228 exprt::operandst fields;
229 fields.reserve(components.size());
230
231 const exprt &compound_op = ssa_expr.get_original_expr();
232
233 for(const auto &comp : components)
234 {
235 ssa_exprt tmp = ssa_expr;
236 bool was_l2 = !tmp.get_level_2().empty();
237 tmp.remove_level_2();
238 tmp.set_expression(
239 member_exprt{compound_op, comp.get_name(), comp.type()});
240 exprt field = get_fields(ns, state, tmp, disjoined_fields_only);
241 if(was_l2)
242 {
243 fields.emplace_back(state.rename(std::move(field), ns).get());
244 }
245 else
246 fields.emplace_back(std::move(field));
247 }
248
249 if(
250 disjoined_fields_only && (ssa_expr.type().id() == ID_struct ||
251 ssa_expr.type().id() == ID_struct_tag))
252 {
253 return struct_exprt{std::move(fields), ssa_expr.type()};
254 }
255 else
256 return field_sensitive_ssa_exprt{ssa_expr, std::move(fields)};
257 }
258#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
259 else if(
260 ssa_expr.type().id() == ID_array &&
261 to_array_type(ssa_expr.type()).size().is_constant())
262 {
263 const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
264 to_constant_expr(to_array_type(ssa_expr.type()).size()));
265 if(mp_array_size < 0 || mp_array_size > max_field_sensitivity_array_size)
266 return ssa_expr;
267
268 const array_typet &type = to_array_type(ssa_expr.type());
269 const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
270
271 array_exprt::operandst elements;
272 elements.reserve(array_size);
273
274 const exprt &array = ssa_expr.get_original_expr();
275
276 for(std::size_t i = 0; i < array_size; ++i)
277 {
278 const index_exprt index(array, from_integer(i, type.index_type()));
279 ssa_exprt tmp = ssa_expr;
280 bool was_l2 = !tmp.get_level_2().empty();
281 tmp.remove_level_2();
282 tmp.set_expression(index);
283 exprt element = get_fields(ns, state, tmp, disjoined_fields_only);
284 if(was_l2)
285 {
286 elements.emplace_back(state.rename(std::move(element), ns).get());
287 }
288 else
289 elements.emplace_back(std::move(element));
290 }
291
292 if(disjoined_fields_only)
293 return array_exprt(std::move(elements), type);
294 else
295 return field_sensitive_ssa_exprt{ssa_expr, std::move(elements)};
296 }
297#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
298 else
299 return ssa_expr;
300}
301
303 const namespacet &ns,
304 goto_symex_statet &state,
305 const ssa_exprt &lhs,
306 const exprt &rhs,
307 symex_targett &target,
308 bool allow_pointer_unsoundness) const
309{
310 const exprt lhs_fs = get_fields(ns, state, lhs, false);
311
312 if(lhs != lhs_fs)
313 {
315 ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness);
316 // Erase the composite symbol from our working state. Note that we need to
317 // have it in the propagation table and the value set while doing the field
318 // assignments, thus we cannot skip putting it in there above.
319 if(is_divisible(lhs, true))
320 {
321 state.propagation.erase_if_exists(lhs.get_identifier());
322 state.value_set.erase_symbol(lhs, ns);
323 }
324 }
325}
326
338 const namespacet &ns,
339 goto_symex_statet &state,
340 const exprt &lhs_fs,
341 const exprt &ssa_rhs,
342 symex_targett &target,
343 bool allow_pointer_unsoundness) const
344{
345 if(is_ssa_expr(lhs_fs))
346 {
347 const ssa_exprt &l1_lhs = to_ssa_expr(lhs_fs);
348 const ssa_exprt ssa_lhs =
349 state
350 .assignment(l1_lhs, ssa_rhs, ns, true, true, allow_pointer_unsoundness)
351 .get();
352
353 // do the assignment
354 target.assignment(
355 state.guard.as_expr(),
356 ssa_lhs,
357 ssa_lhs,
358 ssa_lhs.get_original_expr(),
359 ssa_rhs,
360 state.source,
362 // Erase the composite symbol from our working state. Note that we need to
363 // have it in the propagation table and the value set while doing the field
364 // assignments, thus we cannot skip putting it in there above.
365 if(is_divisible(l1_lhs, true))
366 {
367 state.propagation.erase_if_exists(l1_lhs.get_identifier());
368 state.value_set.erase_symbol(l1_lhs, ns);
369 }
370 }
371 else if(
372 ssa_rhs.type().id() == ID_struct || ssa_rhs.type().id() == ID_struct_tag)
373 {
374 const struct_typet &type = to_struct_type(ns.follow(ssa_rhs.type()));
375 const struct_union_typet::componentst &components = type.components();
376
378 components.empty() ||
379 (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
380
381 exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
382 for(const auto &comp : components)
383 {
384 const exprt member_rhs = apply(
385 ns,
386 state,
387 simplify_opt(member_exprt{ssa_rhs, comp.get_name(), comp.type()}, ns),
388 false);
389
390 const exprt &member_lhs = *fs_it;
391 if(
392 auto fs_ssa =
394 {
396 ns,
397 state,
398 fs_ssa->get_object_ssa(),
399 member_rhs,
400 target,
401 allow_pointer_unsoundness);
402 }
403
405 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
406 ++fs_it;
407 }
408 }
409 else if(
410 ssa_rhs.type().id() == ID_union || ssa_rhs.type().id() == ID_union_tag)
411 {
412 const union_typet &type = to_union_type(ns.follow(ssa_rhs.type()));
413 const struct_union_typet::componentst &components = type.components();
414
416 components.empty() ||
417 (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
418
419 exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
420 for(const auto &comp : components)
421 {
422 const exprt member_rhs = apply(
423 ns,
424 state,
427 ssa_rhs, from_integer(0, c_index_type()), comp.type()),
428 ns),
429 false);
430
431 const exprt &member_lhs = *fs_it;
432 if(
433 auto fs_ssa =
435 {
437 ns,
438 state,
439 fs_ssa->get_object_ssa(),
440 member_rhs,
441 target,
442 allow_pointer_unsoundness);
443 }
444
446 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
447 ++fs_it;
448 }
449 }
450#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
451 else if(const auto &type = type_try_dynamic_cast<array_typet>(ssa_rhs.type()))
452 {
453 const std::size_t array_size =
455 PRECONDITION(lhs_fs.operands().size() == array_size);
456
457 if(array_size > max_field_sensitivity_array_size)
458 return;
459
460 exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
461 for(std::size_t i = 0; i < array_size; ++i)
462 {
463 const exprt index_rhs = apply(
464 ns,
465 state,
467 index_exprt{ssa_rhs, from_integer(i, type->index_type())}, ns),
468 false);
469
470 const exprt &index_lhs = *fs_it;
471 if(
472 auto fs_ssa =
474 {
476 ns,
477 state,
478 fs_ssa->get_object_ssa(),
479 index_rhs,
480 target,
481 allow_pointer_unsoundness);
482 }
483
485 ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
486 ++fs_it;
487 }
488 }
489#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
490 else if(lhs_fs.has_operands())
491 {
493 ssa_rhs.has_operands() &&
494 lhs_fs.operands().size() == ssa_rhs.operands().size());
495
496 exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
497 for(const exprt &op : ssa_rhs.operands())
498 {
500 {
502 ns,
503 state,
504 fs_ssa->get_object_ssa(),
505 op,
506 target,
507 allow_pointer_unsoundness);
508 }
509
511 ns, state, *fs_it, op, target, allow_pointer_unsoundness);
512 ++fs_it;
513 }
514 }
515 else
516 {
518 }
519}
520
522 const ssa_exprt &expr,
523 bool disjoined_fields_only) const
524{
525 if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
526 return true;
527
528#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
529 if(
530 expr.type().id() == ID_array &&
531 to_array_type(expr.type()).size().is_constant() &&
534 {
535 return true;
536 }
537#endif
538
539 if(
540 !disjoined_fields_only &&
541 (expr.type().id() == ID_union || expr.type().id() == ID_union_tag))
542 {
543 return true;
544 }
545
546 return false;
547}
548
550{
551 if(!should_simplify)
552 return e;
553
554 return simplify_expr(std::move(e), ns);
555}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
Definition c_types.cpp:16
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
Array constructor from list of elements.
Definition std_expr.h:1563
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:796
Expression of type type extracted from some object op starting at position offset (given in number of...
bool empty() const
Definition dstring.h:90
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
NODISCARD exprt simplify_opt(exprt e, const namespacet &ns) const
const std::size_t max_field_sensitivity_array_size
NODISCARD exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr, bool disjoined_fields_only) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
void field_assignments_rec(const namespacet &ns, goto_symex_statet &state, const exprt &lhs_fs, const exprt &ssa_rhs, symex_targett &target, bool allow_pointer_unsoundness) const
Assign to the individual fields lhs_fs of a non-expanded symbol lhs.
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.
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, const exprt &rhs, symex_targett &target, bool allow_pointer_unsoundness) const
Assign to the individual fields of a non-expanded symbol lhs.
NODISCARD bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
guardt guard
Definition goto_state.h:58
sharing_mapt< irep_idt, exprt > propagation
Definition goto_state.h:71
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition goto_state.h:51
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:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
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:2794
const exprt & struct_op() const
Definition std_expr.h:2832
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:1819
Structure type, corresponds to C style structs.
Definition std_types.h:231
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
const irep_idt & get_identifier() const
Definition std_expr.h:142
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.
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.
The union type.
Definition c_types.h:147
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
#define Forall_operands(it, expr)
Definition expr.h:27
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
Symbolic Execution.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:18
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#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
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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: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
Generate Equation using Symbolic Execution.