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  exprt expr,
25  bool write) const
26 {
27  if(!run_apply)
28  return expr;
29 
30  if(expr.id() != ID_address_of)
31  {
32  Forall_operands(it, expr)
33  *it = apply(ns, state, std::move(*it), write);
34  }
35 
36  if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) && !write)
37  {
38  return get_fields(ns, state, to_ssa_expr(expr));
39  }
40  else if(
41  !write && expr.id() == ID_member &&
42  to_member_expr(expr).struct_op().id() == ID_struct)
43  {
44  return simplify_expr(std::move(expr), ns);
45  }
46 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
47  else if(
48  !write && expr.id() == ID_index &&
49  to_index_expr(expr).array().id() == ID_array)
50  {
51  return simplify_expr(std::move(expr), ns);
52  }
53 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
54  else if(expr.id() == ID_member)
55  {
56  // turn a member-of-an-SSA-expression into a single SSA expression, thus
57  // encoding the member as an individual symbol rather than only the full
58  // struct
59  member_exprt &member = to_member_expr(expr);
60 
61  if(
62  member.struct_op().id() == ID_symbol &&
63  member.struct_op().get_bool(ID_C_SSA_symbol) &&
64  (member.struct_op().type().id() == ID_struct ||
65  member.struct_op().type().id() == ID_struct_tag))
66  {
67  // place the entire member expression, not just the struct operand, in an
68  // SSA expression
69  ssa_exprt tmp = to_ssa_expr(member.struct_op());
70  bool was_l2 = !tmp.get_level_2().empty();
71 
72  tmp.remove_level_2();
73  member.struct_op() = tmp.get_original_expr();
74  tmp.set_expression(member);
75  if(was_l2)
76  return state.rename(std::move(tmp), ns).get();
77  else
78  return std::move(tmp);
79  }
80  }
81 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
82  else if(expr.id() == ID_index)
83  {
84  // turn a index-of-an-SSA-expression into a single SSA expression, thus
85  // encoding the index access into an array as an individual symbol rather
86  // than only the full array
87  index_exprt &index = to_index_expr(expr);
88  simplify(index.index(), ns);
89 
90  if(
91  index.array().id() == ID_symbol &&
92  index.array().get_bool(ID_C_SSA_symbol) &&
93  index.array().type().id() == ID_array &&
94  index.index().id() == ID_constant)
95  {
96  // place the entire index expression, not just the array operand, in an
97  // SSA expression
98  ssa_exprt tmp = to_ssa_expr(index.array());
99  auto l2_index = state.rename(index.index(), ns);
100  l2_index.simplify(ns);
101  bool was_l2 = !tmp.get_level_2().empty();
102  exprt l2_size =
103  state.rename(to_array_type(index.array().type()).size(), ns).get();
104  if(l2_size.is_nil() && index.array().id() == ID_symbol)
105  {
106  // In case the array type was incomplete, attempt to retrieve it from
107  // the symbol table.
108  const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup(
109  to_symbol_expr(index.array()).get_identifier());
110  if(array_from_symbol_table != nullptr)
111  l2_size = to_array_type(array_from_symbol_table->type).size();
112  }
113 
114  if(
115  l2_size.id() == ID_constant &&
116  numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
118  {
119  if(l2_index.get().id() == ID_constant)
120  {
121  // place the entire index expression, not just the array operand,
122  // in an SSA expression
123  ssa_exprt ssa_array = to_ssa_expr(index.array());
124  ssa_array.remove_level_2();
125  index.array() = ssa_array.get_original_expr();
126  index.index() = l2_index.get();
127  tmp.set_expression(index);
128  if(was_l2)
129  return state.rename(std::move(tmp), ns).get();
130  else
131  return std::move(tmp);
132  }
133  else if(!write)
134  {
135  // Expand the array and return `{array[0]; array[1]; ...}[index]`
136  exprt expanded_array =
137  get_fields(ns, state, to_ssa_expr(index.array()));
138  return index_exprt{std::move(expanded_array), index.index()};
139  }
140  }
141  }
142  }
143 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
144  return expr;
145 }
146 
148  const namespacet &ns,
149  goto_symex_statet &state,
150  const ssa_exprt &ssa_expr) const
151 {
152  if(ssa_expr.type().id() == ID_struct || ssa_expr.type().id() == ID_struct_tag)
153  {
154  const struct_typet &type = to_struct_type(ns.follow(ssa_expr.type()));
155  const struct_union_typet::componentst &components = type.components();
156 
157  struct_exprt result(ssa_expr.type());
158  result.reserve_operands(components.size());
159 
160  const exprt &struct_op = ssa_expr.get_original_expr();
161 
162  for(const auto &comp : components)
163  {
164  const member_exprt member(struct_op, comp.get_name(), comp.type());
165  ssa_exprt tmp = ssa_expr;
166  bool was_l2 = !tmp.get_level_2().empty();
167  tmp.remove_level_2();
168  tmp.set_expression(member);
169  if(was_l2)
170  {
171  result.add_to_operands(
172  state.rename(get_fields(ns, state, tmp), ns).get());
173  }
174  else
175  result.add_to_operands(get_fields(ns, state, tmp));
176  }
177 
178  return std::move(result);
179  }
180 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
181  else if(
182  ssa_expr.type().id() == ID_array &&
183  to_array_type(ssa_expr.type()).size().id() == ID_constant)
184  {
185  const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
186  to_constant_expr(to_array_type(ssa_expr.type()).size()));
187  if(mp_array_size < 0 || mp_array_size > max_field_sensitivity_array_size)
188  return ssa_expr;
189 
190  const array_typet &type = to_array_type(ssa_expr.type());
191  const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
192 
193  array_exprt result(type);
194  result.reserve_operands(array_size);
195 
196  const exprt &array = ssa_expr.get_original_expr();
197 
198  for(std::size_t i = 0; i < array_size; ++i)
199  {
200  const index_exprt index(array, from_integer(i, index_type()));
201  ssa_exprt tmp = ssa_expr;
202  bool was_l2 = !tmp.get_level_2().empty();
203  tmp.remove_level_2();
204  tmp.set_expression(index);
205  if(was_l2)
206  {
207  result.add_to_operands(
208  state.rename(get_fields(ns, state, tmp), ns).get());
209  }
210  else
211  result.add_to_operands(get_fields(ns, state, tmp));
212  }
213 
214  return std::move(result);
215  }
216 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
217  else
218  return ssa_expr;
219 }
220 
222  const namespacet &ns,
223  goto_symex_statet &state,
224  const ssa_exprt &lhs,
225  symex_targett &target,
226  bool allow_pointer_unsoundness)
227 {
228  const exprt lhs_fs = apply(ns, state, lhs, false);
229 
230  bool run_apply_bak = run_apply;
231  run_apply = false;
233  ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
234  run_apply = run_apply_bak;
235 }
236 
248  const namespacet &ns,
249  goto_symex_statet &state,
250  const exprt &lhs_fs,
251  const exprt &lhs,
252  symex_targett &target,
253  bool allow_pointer_unsoundness)
254 {
255  if(lhs == lhs_fs)
256  return;
257  else if(lhs_fs.id() == ID_symbol && lhs_fs.get_bool(ID_C_SSA_symbol))
258  {
259  exprt ssa_rhs = state.rename(lhs, ns).get();
260  simplify(ssa_rhs, ns);
261 
262  const ssa_exprt ssa_lhs = state
263  .assignment(
264  to_ssa_expr(lhs_fs),
265  ssa_rhs,
266  ns,
267  true,
268  true,
269  allow_pointer_unsoundness)
270  .get();
271 
272  // do the assignment
273  target.assignment(
274  state.guard.as_expr(),
275  ssa_lhs,
276  ssa_lhs,
277  ssa_lhs.get_original_expr(),
278  ssa_rhs,
279  state.source,
281  }
282  else if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
283  {
284  const struct_typet &type = to_struct_type(ns.follow(lhs.type()));
285  const struct_union_typet::componentst &components = type.components();
286 
287  PRECONDITION(
288  components.empty() ||
289  (lhs_fs.has_operands() && lhs_fs.operands().size() == components.size()));
290 
291  exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
292  for(const auto &comp : components)
293  {
294  const member_exprt member_rhs(lhs, comp.get_name(), comp.type());
295  const exprt &member_lhs = *fs_it;
296 
298  ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
299  ++fs_it;
300  }
301  }
302 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
303  else if(const auto &type = type_try_dynamic_cast<array_typet>(lhs.type()))
304  {
305  const std::size_t array_size =
306  numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
307  PRECONDITION(lhs_fs.operands().size() == array_size);
308 
309  if(array_size > max_field_sensitivity_array_size)
310  return;
311 
312  exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
313  for(std::size_t i = 0; i < array_size; ++i)
314  {
315  const index_exprt index_rhs(lhs, from_integer(i, index_type()));
316  const exprt &index_lhs = *fs_it;
317 
319  ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
320  ++fs_it;
321  }
322  }
323 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
324  else if(lhs_fs.has_operands())
325  {
326  PRECONDITION(
327  lhs.has_operands() && lhs_fs.operands().size() == lhs.operands().size());
328 
329  exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
330  for(const exprt &op : lhs.operands())
331  {
333  ns, state, *fs_it, op, target, allow_pointer_unsoundness);
334  ++fs_it;
335  }
336  }
337  else
338  {
339  UNREACHABLE;
340  }
341 }
342 
344 {
345  if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
346  return true;
347 
348 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
349  if(
350  expr.type().id() == ID_array &&
351  to_array_type(expr.type()).size().id() == ID_constant &&
352  numeric_cast_v<mp_integer>(to_constant_expr(
354  {
355  return true;
356  }
357 #endif
358 
359  return false;
360 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
arith_tools.h
ssa_exprt::remove_level_2
void remove_level_2()
goto_symex_statet::assignment
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)
Definition: goto_symex_state.cpp:76
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1353
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
field_sensitivityt::apply
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
Definition: field_sensitivity.cpp:21
field_sensitivityt::max_field_sensitivity_array_size
const std::size_t max_field_sensitivity_array_size
Definition: field_sensitivity.h:149
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
field_sensitivityt::run_apply
bool run_apply
whether or not to invoke field_sensitivityt::apply
Definition: field_sensitivity.h:147
symex_targett::assignment_typet::STATE
@ STATE
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1645
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
symex_targett::assignment
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.
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3464
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
goto_statet::guard
guardt guard
Definition: goto_state.h:50
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1325
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
index_exprt::array
exprt & array()
Definition: std_expr.h:1315
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
simplify_expr.h
field_sensitivityt::field_assignments
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.
Definition: field_sensitivity.cpp:221
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3434
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
array_typet
Arrays with given size.
Definition: std_types.h:965
ssa_exprt::set_expression
void set_expression(const exprt &expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
goto_symex_state.h
field_sensitivityt::is_divisible
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Definition: field_sensitivity.cpp:343
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
field_sensitivityt::field_assignments_rec
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.
Definition: field_sensitivity.cpp:247
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:155
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3518
goto_symex_statet::rename
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...
field_sensitivityt::get_fields
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 ...
Definition: field_sensitivity.cpp:147
exprt::operands
operandst & operands()
Definition: expr.h:95
field_sensitivity.h
index_exprt
Array index operator.
Definition: std_expr.h:1299
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:125
std_expr.h
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1438
c_types.h
symex_target.h
symex_targett
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:26
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3968