cprover
field_sensitivity.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-sensitive SSA
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #include "field_sensitivity.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/c_types.h>
13 #include <util/simplify_expr.h>
14 #include <util/std_expr.h>
15 
16 #include "goto_symex_state.h"
17 #include "symex_target.h"
18 
19 #define ENABLE_ARRAY_FIELD_SENSITIVITY
20 
22  const namespacet &ns,
23  goto_symex_statet &state,
24  ssa_exprt ssa_expr,
25  bool write) const
26 {
27  if(!run_apply || write)
28  return std::move(ssa_expr);
29  else
30  return get_fields(ns, state, ssa_expr);
31 }
32 
34  const namespacet &ns,
35  goto_symex_statet &state,
36  exprt expr,
37  bool write) const
38 {
39  if(!run_apply)
40  return expr;
41 
42  if(expr.id() != ID_address_of)
43  {
44  Forall_operands(it, expr)
45  *it = apply(ns, state, std::move(*it), write);
46  }
47 
48  if(!write && is_ssa_expr(expr))
49  {
50  return apply(ns, state, to_ssa_expr(expr), write);
51  }
52  else if(
53  !write && expr.id() == ID_member &&
54  to_member_expr(expr).struct_op().id() == ID_struct)
55  {
56  return simplify_expr(std::move(expr), ns);
57  }
58 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
59  else if(
60  !write && expr.id() == ID_index &&
61  to_index_expr(expr).array().id() == ID_array)
62  {
63  return simplify_expr(std::move(expr), ns);
64  }
65 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
66  else if(expr.id() == ID_member)
67  {
68  // turn a member-of-an-SSA-expression into a single SSA expression, thus
69  // encoding the member as an individual symbol rather than only the full
70  // struct
71  member_exprt &member = to_member_expr(expr);
72 
73  if(
74  is_ssa_expr(member.struct_op()) &&
75  (member.struct_op().type().id() == ID_struct ||
76  member.struct_op().type().id() == ID_struct_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 state.rename(std::move(tmp), ns).get();
88  else
89  return std::move(tmp);
90  }
91  }
92 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
93  else if(expr.id() == ID_index)
94  {
95  // turn a index-of-an-SSA-expression into a single SSA expression, thus
96  // encoding the index access into an array as an individual symbol rather
97  // than only the full array
98  index_exprt &index = to_index_expr(expr);
99  simplify(index.index(), ns);
100 
101  if(
102  is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
103  index.index().id() == ID_constant)
104  {
105  // place the entire index expression, not just the array operand, in an
106  // SSA expression
107  ssa_exprt tmp = to_ssa_expr(index.array());
108  auto l2_index = state.rename(index.index(), ns);
109  l2_index.simplify(ns);
110  bool was_l2 = !tmp.get_level_2().empty();
111  exprt l2_size =
112  state.rename(to_array_type(index.array().type()).size(), ns).get();
113  if(l2_size.is_nil() && index.array().id() == ID_symbol)
114  {
115  // In case the array type was incomplete, attempt to retrieve it from
116  // the symbol table.
117  const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup(
118  to_symbol_expr(index.array()).get_identifier());
119  if(array_from_symbol_table != nullptr)
120  l2_size = to_array_type(array_from_symbol_table->type).size();
121  }
122 
123  if(
124  l2_size.id() == ID_constant &&
125  numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
127  {
128  if(l2_index.get().id() == ID_constant)
129  {
130  // place the entire index expression, not just the array operand,
131  // in an SSA expression
132  ssa_exprt ssa_array = to_ssa_expr(index.array());
133  ssa_array.remove_level_2();
134  index.array() = ssa_array.get_original_expr();
135  index.index() = l2_index.get();
136  tmp.set_expression(index);
137  if(was_l2)
138  return state.rename(std::move(tmp), ns).get();
139  else
140  return std::move(tmp);
141  }
142  else if(!write)
143  {
144  // Expand the array and return `{array[0]; array[1]; ...}[index]`
145  exprt expanded_array =
146  get_fields(ns, state, to_ssa_expr(index.array()));
147  return index_exprt{std::move(expanded_array), index.index()};
148  }
149  }
150  }
151  }
152 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
153  return expr;
154 }
155 
157  const namespacet &ns,
158  goto_symex_statet &state,
159  const ssa_exprt &ssa_expr) const
160 {
161  if(ssa_expr.type().id() == ID_struct || ssa_expr.type().id() == ID_struct_tag)
162  {
163  const struct_typet &type = to_struct_type(ns.follow(ssa_expr.type()));
164  const struct_union_typet::componentst &components = type.components();
165 
167  fields.reserve(components.size());
168 
169  const exprt &struct_op = ssa_expr.get_original_expr();
170 
171  for(const auto &comp : components)
172  {
173  const member_exprt member(struct_op, comp.get_name(), comp.type());
174  ssa_exprt tmp = ssa_expr;
175  bool was_l2 = !tmp.get_level_2().empty();
176  tmp.remove_level_2();
177  tmp.set_expression(member);
178  if(was_l2)
179  {
180  fields.push_back(state.rename(get_fields(ns, state, tmp), ns).get());
181  }
182  else
183  fields.push_back(get_fields(ns, state, tmp));
184  }
185 
186  return struct_exprt(std::move(fields), ssa_expr.type());
187  }
188 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
189  else if(
190  ssa_expr.type().id() == ID_array &&
191  to_array_type(ssa_expr.type()).size().id() == ID_constant)
192  {
193  const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
194  to_constant_expr(to_array_type(ssa_expr.type()).size()));
195  if(mp_array_size < 0 || mp_array_size > max_field_sensitivity_array_size)
196  return ssa_expr;
197 
198  const array_typet &type = to_array_type(ssa_expr.type());
199  const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
200 
201  array_exprt::operandst elements;
202  elements.reserve(array_size);
203 
204  const exprt &array = ssa_expr.get_original_expr();
205 
206  for(std::size_t i = 0; i < array_size; ++i)
207  {
208  const index_exprt index(array, from_integer(i, index_type()));
209  ssa_exprt tmp = ssa_expr;
210  bool was_l2 = !tmp.get_level_2().empty();
211  tmp.remove_level_2();
212  tmp.set_expression(index);
213  if(was_l2)
214  {
215  elements.push_back(state.rename(get_fields(ns, state, tmp), ns).get());
216  }
217  else
218  elements.push_back(get_fields(ns, state, tmp));
219  }
220 
221  return array_exprt(std::move(elements), type);
222  }
223 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
224  else
225  return ssa_expr;
226 }
227 
229  const namespacet &ns,
230  goto_symex_statet &state,
231  const ssa_exprt &lhs,
232  symex_targett &target,
233  bool allow_pointer_unsoundness)
234 {
235  const exprt lhs_fs = apply(ns, state, lhs, false);
236 
237  bool run_apply_bak = run_apply;
238  run_apply = false;
240  ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
241  run_apply = run_apply_bak;
242 }
243 
255  const namespacet &ns,
256  goto_symex_statet &state,
257  const exprt &lhs_fs,
258  const exprt &lhs,
259  symex_targett &target,
260  bool allow_pointer_unsoundness)
261 {
262  if(lhs == lhs_fs)
263  return;
264  else if(is_ssa_expr(lhs_fs))
265  {
266  exprt ssa_rhs = state.rename(lhs, ns).get();
267  simplify(ssa_rhs, ns);
268 
269  const ssa_exprt ssa_lhs = state
270  .assignment(
271  to_ssa_expr(lhs_fs),
272  ssa_rhs,
273  ns,
274  true,
275  true,
276  allow_pointer_unsoundness)
277  .get();
278 
279  // do the assignment
280  target.assignment(
281  state.guard.as_expr(),
282  ssa_lhs,
283  ssa_lhs,
284  ssa_lhs.get_original_expr(),
285  ssa_rhs,
286  state.source,
288  }
289  else if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
290  {
291  const struct_typet &type = to_struct_type(ns.follow(lhs.type()));
292  const struct_union_typet::componentst &components = type.components();
293 
294  PRECONDITION(
295  components.empty() ||
296  (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
297 
298  exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
299  for(const auto &comp : components)
300  {
301  const member_exprt member_rhs(lhs, comp.get_name(), comp.type());
302  const exprt &member_lhs = *fs_it;
303 
305  ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
306  ++fs_it;
307  }
308  }
309 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
310  else if(const auto &type = type_try_dynamic_cast<array_typet>(lhs.type()))
311  {
312  const std::size_t array_size =
313  numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
314  PRECONDITION(lhs_fs.operands().size() == array_size);
315 
316  if(array_size > max_field_sensitivity_array_size)
317  return;
318 
319  exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
320  for(std::size_t i = 0; i < array_size; ++i)
321  {
322  const index_exprt index_rhs(lhs, from_integer(i, index_type()));
323  const exprt &index_lhs = *fs_it;
324 
326  ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
327  ++fs_it;
328  }
329  }
330 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
331  else if(lhs_fs.has_operands())
332  {
333  PRECONDITION(
334  lhs.has_operands() && lhs_fs.operands().size() == lhs.operands().size());
335 
336  exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
337  for(const exprt &op : lhs.operands())
338  {
340  ns, state, *fs_it, op, target, allow_pointer_unsoundness);
341  ++fs_it;
342  }
343  }
344  else
345  {
346  UNREACHABLE;
347  }
348 }
349 
351 {
352  if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
353  return true;
354 
355 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
356  if(
357  expr.type().id() == ID_array &&
358  to_array_type(expr.type()).size().id() == ID_constant &&
359  numeric_cast_v<mp_integer>(to_constant_expr(
361  {
362  return true;
363  }
364 #endif
365 
366  return false;
367 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:16
Array constructor from list of elements.
Definition: std_expr.h:1382
Arrays with given size.
Definition: std_types.h:968
const exprt & size() const
Definition: std_types.h:976
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:93
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
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:54
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:49
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & struct_op() const
Definition: std_expr.h:2558
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void remove_level_2()
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
void set_expression(const exprt &expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
Struct constructor from list of elements.
Definition: std_expr.h:1583
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const componentst & components() const
Definition: std_types.h:142
std::vector< componentt > componentst
Definition: std_types.h:135
const irep_idt & get_identifier() const
Definition: std_expr.h:110
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:26
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.
BigInt mp_integer
Definition: mp_arith.h:19
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
Generate Equation using Symbolic Execution.