Go to the documentation of this file.
19 #define ENABLE_ARRAY_FIELD_SENSITIVITY
30 if(expr.
id() != ID_address_of)
33 *it =
apply(ns, state, std::move(*it), write);
36 if(expr.
id() == ID_symbol && expr.
get_bool(ID_C_SSA_symbol) && !write)
41 !write && expr.
id() == ID_member &&
46 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
48 !write && expr.
id() == ID_index &&
53 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
54 else if(expr.
id() == ID_member)
76 return state.
rename(std::move(tmp), ns).get();
78 return std::move(tmp);
81 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
82 else if(expr.
id() == ID_index)
91 index.
array().
id() == ID_symbol &&
94 index.
index().
id() == ID_constant)
100 l2_index.simplify(ns);
110 if(array_from_symbol_table !=
nullptr)
115 l2_size.
id() == ID_constant &&
119 if(l2_index.get().id() == ID_constant)
129 return state.
rename(std::move(tmp), ns).get();
131 return std::move(tmp);
136 exprt expanded_array =
143 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
152 if(ssa_expr.
type().
id() == ID_struct || ssa_expr.
type().
id() == ID_struct_tag)
158 fields.reserve(components.size());
162 for(
const auto &comp : components)
179 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
181 ssa_expr.
type().
id() == ID_array &&
184 const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
190 const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
193 elements.reserve(array_size);
197 for(std::size_t i = 0; i < array_size; ++i)
209 elements.push_back(
get_fields(ns, state, tmp));
214 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
224 bool allow_pointer_unsoundness)
226 const exprt lhs_fs =
apply(ns, state, lhs,
false);
231 ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
251 bool allow_pointer_unsoundness)
255 else if(lhs_fs.
id() == ID_symbol && lhs_fs.
get_bool(ID_C_SSA_symbol))
267 allow_pointer_unsoundness)
280 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
286 components.empty() ||
289 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
290 for(
const auto &comp : components)
293 const exprt &member_lhs = *fs_it;
296 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
300 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
301 else if(
const auto &type = type_try_dynamic_cast<array_typet>(lhs.
type()))
303 const std::size_t array_size =
310 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
311 for(std::size_t i = 0; i < array_size; ++i)
314 const exprt &index_lhs = *fs_it;
317 ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
321 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
327 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
331 ns, state, *fs_it, op, target, allow_pointer_unsoundness);
343 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
346 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
348 expr.
type().
id() == ID_array &&
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
#define Forall_operands(it, expr)
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)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
typet type
Type of symbol.
Central data structure: state.
Base class for all expressions.
std::vector< componentt > componentst
symex_targett::sourcet source
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
const std::size_t max_field_sensitivity_array_size
bitvector_typet index_type()
const exprt & get_original_expr() const
bool run_apply
whether or not to invoke field_sensitivityt::apply
Struct constructor from list of elements.
Expression providing an SSA-renamed symbol of expressions.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
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.
bool has_operands() const
Return true if there is at least one operand.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const exprt & struct_op() const
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
const irep_idt get_level_2() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
std::vector< exprt > operandst
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.
Extract member of struct or union.
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Structure type, corresponds to C style structs.
void set_expression(const exprt &expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
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.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
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...
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 ...
API to expression classes.
Array constructor from list of elements.
Generate Equation using Symbolic Execution.
The interface of the target container for symbolic execution to record its symbolic steps into.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.