cprover
Loading...
Searching...
No Matches
field_sensitivity.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-sensitive SSA
4
5Author: 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/nodiscard.h>
13#include <util/ssa_expr.h>
14
15class namespacet;
17class symex_targett;
18
20{
21public:
23 : exprt(ID_field_sensitive_ssa, ssa.type(), std::move(fields))
24 {
25 add(ID_expression, ssa);
26 }
27
29 {
30 return static_cast<const ssa_exprt &>(find(ID_expression));
31 }
32};
33
34template <>
36{
37 return base.id() == ID_field_sensitive_ssa;
38}
39
40inline const field_sensitive_ssa_exprt &
42{
43 PRECONDITION(expr.id() == ID_field_sensitive_ssa);
44 const field_sensitive_ssa_exprt &ret =
45 static_cast<const field_sensitive_ssa_exprt &>(expr);
46 return ret;
47}
48
50{
51 PRECONDITION(expr.id() == ID_field_sensitive_ssa);
53 static_cast<field_sensitive_ssa_exprt &>(expr);
54 return ret;
55}
56
118{
119public:
123 field_sensitivityt(std::size_t max_array_size, bool should_simplify)
124 : max_field_sensitivity_array_size(max_array_size),
126 {
127 }
128
141 const namespacet &ns,
142 goto_symex_statet &state,
143 const ssa_exprt &lhs,
144 const exprt &rhs,
145 symex_targett &target,
146 bool allow_pointer_unsoundness) const;
147
162 exprt
163 apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
164 const;
167 exprt apply(
168 const namespacet &ns,
169 goto_symex_statet &state,
170 ssa_exprt expr,
171 bool write) const;
172
187 const namespacet &ns,
188 goto_symex_statet &state,
189 const ssa_exprt &ssa_expr,
190 bool disjoined_fields_only) const;
191
202 bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
203
204private:
206
207 const bool should_simplify;
208
210 const namespacet &ns,
211 goto_symex_statet &state,
212 const exprt &lhs_fs,
213 const exprt &ssa_rhs,
214 symex_targett &target,
215 bool allow_pointer_unsoundness) const;
216
218 exprt simplify_opt(exprt e, const namespacet &ns) const;
219};
220
221#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.
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.
field_sensitivityt(std::size_t max_array_size, bool should_simplify)
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...
Central data structure: state.
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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.
bool can_cast_expr< field_sensitive_ssa_exprt >(const exprt &base)
const field_sensitive_ssa_exprt & to_field_sensitive_ssa_expr(const exprt &expr)
STL namespace.
#define NODISCARD
Definition nodiscard.h:22
#define PRECONDITION(CONDITION)
Definition invariant.h:463