cprover
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/magic.h>
13 #include <util/nodiscard.h>
14 
15 class exprt;
16 class ssa_exprt;
17 class namespacet;
18 class goto_symex_statet;
19 class symex_targett;
20 
82 {
83 public:
86  explicit field_sensitivityt(std::size_t max_array_size)
87  : max_field_sensitivity_array_size(max_array_size)
88  {
89  }
90 
100  void field_assignments(
101  const namespacet &ns,
102  goto_symex_statet &state,
103  const ssa_exprt &lhs,
104  symex_targett &target,
105  bool allow_pointer_unsoundness);
106 
120  NODISCARD
121  exprt
122  apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
123  const;
125  exprt apply(
126  const namespacet &ns,
127  goto_symex_statet &state,
128  ssa_exprt expr,
129  bool write) const;
130 
140  const namespacet &ns,
141  goto_symex_statet &state,
142  const ssa_exprt &ssa_expr) const;
143 
151  bool is_divisible(const ssa_exprt &expr) const;
152 
153 private:
155  bool run_apply = true;
156 
158 
160  const namespacet &ns,
161  goto_symex_statet &state,
162  const exprt &lhs_fs,
163  const exprt &lhs,
164  symex_targett &target,
165  bool allow_pointer_unsoundness);
166 };
167 
168 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
nodiscard.h
exprt
Base class for all expressions.
Definition: expr.h:54
field_sensitivityt
Control granularity of object accesses.
Definition: field_sensitivity.h:82
field_sensitivityt::apply
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.
Definition: field_sensitivity.cpp:33
field_sensitivityt::max_field_sensitivity_array_size
const std::size_t max_field_sensitivity_array_size
Definition: field_sensitivity.h:157
magic.h
Magic numbers used throughout the codebase.
field_sensitivityt::run_apply
bool run_apply
whether or not to invoke field_sensitivityt::apply
Definition: field_sensitivity.h:155
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
field_sensitivityt::field_sensitivityt
field_sensitivityt(std::size_t max_array_size)
Definition: field_sensitivity.h:86
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:227
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:349
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:253
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:156
symex_targett
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:26