CBMC
field_sensitivity.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-sensitive SSA
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
10 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
11 
12 #include <util/ssa_expr.h>
13 
14 class namespacet;
15 class goto_symex_statet;
16 class symex_targett;
17 
19 {
20 public:
22  : exprt(ID_field_sensitive_ssa, ssa.type(), std::move(fields))
23  {
24  add(ID_expression, ssa);
25  }
26 
27  const ssa_exprt &get_object_ssa() const
28  {
29  return static_cast<const ssa_exprt &>(find(ID_expression));
30  }
31 };
32 
33 template <>
35 {
36  return base.id() == ID_field_sensitive_ssa;
37 }
38 
39 inline const field_sensitive_ssa_exprt &
41 {
42  PRECONDITION(expr.id() == ID_field_sensitive_ssa);
43  const field_sensitive_ssa_exprt &ret =
44  static_cast<const field_sensitive_ssa_exprt &>(expr);
45  return ret;
46 }
47 
49 {
50  PRECONDITION(expr.id() == ID_field_sensitive_ssa);
52  static_cast<field_sensitive_ssa_exprt &>(expr);
53  return ret;
54 }
55 
117 {
118 public:
122  field_sensitivityt(std::size_t max_array_size, bool should_simplify)
123  : max_field_sensitivity_array_size(max_array_size),
125  {
126  }
127 
139  void field_assignments(
140  const namespacet &ns,
141  goto_symex_statet &state,
142  const ssa_exprt &lhs,
143  const exprt &rhs,
144  symex_targett &target,
145  bool allow_pointer_unsoundness) const;
146 
160  [[nodiscard]] exprt
161  apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
162  const;
164  [[nodiscard]] exprt apply(
165  const namespacet &ns,
166  goto_symex_statet &state,
167  ssa_exprt expr,
168  bool write) const;
169 
182  [[nodiscard]] exprt get_fields(
183  const namespacet &ns,
184  goto_symex_statet &state,
185  const ssa_exprt &ssa_expr,
186  bool disjoined_fields_only) const;
187 
197  [[nodiscard]] bool
198  is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
199 
200 private:
202 
203  const bool should_simplify;
204 
206  const namespacet &ns,
207  goto_symex_statet &state,
208  const exprt &lhs_fs,
209  const exprt &ssa_rhs,
210  symex_targett &target,
211  bool allow_pointer_unsoundness) const;
212 
213  [[nodiscard]] exprt simplify_opt(exprt e, const namespacet &ns) const;
214 };
215 
216 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
field_sensitive_ssa_exprt(const ssa_exprt &ssa, exprt::operandst &&fields)
const ssa_exprt & get_object_ssa() const
Control granularity of object accesses.
exprt simplify_opt(exprt e, const namespacet &ns) const
const std::size_t max_field_sensitivity_array_size
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.
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.
field_sensitivityt(std::size_t max_array_size, bool should_simplify)
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...
Central data structure: state.
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & id() const
Definition: irep.h:384
irept & add(const irep_idt &name)
Definition: irep.cpp:103
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
bool can_cast_expr< field_sensitive_ssa_exprt >(const exprt &base)
const field_sensitive_ssa_exprt & to_field_sensitive_ssa_expr(const exprt &expr)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition: unistd.c:195