19 #define ENABLE_ARRAY_FIELD_SENSITIVITY
28 return std::move(ssa_expr);
42 if(expr.
id() != ID_address_of)
45 *it =
apply(ns, state, std::move(*it), write);
53 !write && expr.
id() == ID_member &&
58 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
60 !write && expr.
id() == ID_index &&
66 else if(expr.
id() == ID_member)
87 return state.
rename(std::move(tmp), ns).get();
89 return std::move(tmp);
92 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
93 else if(expr.
id() == ID_index)
103 index.
index().
id() == ID_constant)
109 l2_index.simplify(ns);
119 if(array_from_symbol_table !=
nullptr)
124 l2_size.
id() == ID_constant &&
128 if(l2_index.get().id() == ID_constant)
138 return state.
rename(std::move(tmp), ns).get();
140 return std::move(tmp);
145 exprt expanded_array =
161 if(ssa_expr.
type().
id() == ID_struct || ssa_expr.
type().
id() == ID_struct_tag)
167 fields.reserve(components.size());
171 for(
const auto &comp : components)
187 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
189 ssa_expr.
type().
id() == ID_array &&
192 const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
198 const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
201 elements.reserve(array_size);
205 for(std::size_t i = 0; i < array_size; ++i)
217 elements.push_back(
get_fields(ns, state, tmp));
232 bool allow_pointer_unsoundness)
234 const exprt lhs_fs =
apply(ns, state, lhs,
false);
239 ns, state, lhs_fs, lhs, target, allow_pointer_unsoundness);
259 bool allow_pointer_unsoundness)
275 allow_pointer_unsoundness)
288 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
294 components.empty() ||
297 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
298 for(
const auto &comp : components)
301 const exprt &member_lhs = *fs_it;
304 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
308 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
309 else if(
const auto &type = type_try_dynamic_cast<array_typet>(lhs.
type()))
311 const std::size_t array_size =
318 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
319 for(std::size_t i = 0; i < array_size; ++i)
322 const exprt &index_lhs = *fs_it;
325 ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
335 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
339 ns, state, *fs_it, op, target, allow_pointer_unsoundness);
351 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
354 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
356 expr.
type().
id() == ID_array &&
bitvector_typet index_type()
Array constructor from list of elements.
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 & id() const
const irep_idt & get(const irep_namet &name) 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)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
bool is_ssa_expr(const exprt &expr)
API to expression classes.
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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_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.