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)
162 for(
const auto &comp : components)
178 return std::move(result);
180 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
182 ssa_expr.
type().
id() == ID_array &&
185 const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
191 const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
198 for(std::size_t i = 0; i < array_size; ++i)
214 return std::move(result);
216 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
226 bool allow_pointer_unsoundness)
228 const exprt lhs_fs =
apply(ns, state, lhs,
false);
233 ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
253 bool allow_pointer_unsoundness)
257 else if(lhs_fs.
id() == ID_symbol && lhs_fs.
get_bool(ID_C_SSA_symbol))
269 allow_pointer_unsoundness)
282 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
288 components.empty() ||
291 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
292 for(
const auto &comp : components)
295 const exprt &member_lhs = *fs_it;
298 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
302 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
303 else if(
const auto &type = type_try_dynamic_cast<array_typet>(lhs.
type()))
305 const std::size_t array_size =
312 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
313 for(std::size_t i = 0; i < array_size; ++i)
316 const exprt &index_lhs = *fs_it;
319 ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
323 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
329 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
333 ns, state, *fs_it, op, target, allow_pointer_unsoundness);
345 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
348 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
350 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
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.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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 ...
void reserve_operands(operandst::size_type n)
Array constructor from list of elements.
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.