18#define ENABLE_ARRAY_FIELD_SENSITIVITY
27 return std::move(ssa_expr);
41 if(expr.
id() != ID_address_of)
44 *it =
apply(ns, state, std::move(*it), write);
52 !write && expr.
id() == ID_member &&
57#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
59 !write && expr.
id() == ID_index &&
65 else if(expr.
id() == ID_member)
86 return state.
rename(std::move(tmp), ns).get();
88 return std::move(tmp);
91#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
92 else if(expr.
id() == ID_index)
102 index.
index().
id() == ID_constant)
108 l2_index.simplify(ns);
118 if(array_from_symbol_table !=
nullptr)
123 l2_size.
id() == ID_constant &&
127 if(l2_index.get().id() == ID_constant)
137 return state.
rename(std::move(tmp), ns).get();
139 return std::move(tmp);
144 exprt expanded_array =
160 if(ssa_expr.
type().
id() == ID_struct || ssa_expr.
type().
id() == ID_struct_tag)
166 fields.reserve(components.size());
170 for(
const auto &comp : components)
186#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
188 ssa_expr.
type().
id() == ID_array &&
191 const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
197 const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
200 elements.reserve(array_size);
204 for(std::size_t i = 0; i < array_size; ++i)
216 elements.push_back(
get_fields(ns, state, tmp));
231 bool allow_pointer_unsoundness)
233 const exprt lhs_fs =
apply(ns, state, lhs,
false);
238 ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
258 bool allow_pointer_unsoundness)
274 allow_pointer_unsoundness)
287 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
293 components.empty() ||
296 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
297 for(
const auto &comp : components)
300 const exprt &member_lhs = *fs_it;
303 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
307#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
308 else if(
const auto &type = type_try_dynamic_cast<array_typet>(lhs.
type()))
310 const std::size_t array_size =
317 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
318 for(std::size_t i = 0; i < array_size; ++i)
321 const exprt &index_lhs = *fs_it;
324 ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
334 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
338 ns, state, *fs_it, op, target, allow_pointer_unsoundness);
350 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
353#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
355 expr.
type().
id() == ID_array &&
Array constructor from list of elements.
typet index_type() const
The type of the index expressions into any instance of this type.
const exprt & size() const
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
typet & type()
Return the type of the expression.
bool run_apply
whether or not to invoke field_sensitivityt::apply
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
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.
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.
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 ...
const std::size_t max_field_sensitivity_array_size
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.
Central data structure: state.
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...
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)
symex_targett::sourcet source
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Expression providing an SSA-renamed symbol of expressions.
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
const irep_idt get_level_2() const
const exprt & get_original_expr() const
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
typet type
Type of symbol.
The interface of the target container for symbolic execution to record its symbolic steps into.
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.
#define Forall_operands(it, expr)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Generate Equation using Symbolic Execution.