20#define ENABLE_ARRAY_FIELD_SENSITIVITY
29 return std::move(ssa_expr);
40 if(expr.
id() != ID_address_of)
43 *it =
apply(ns, state, std::move(*it), write);
51 !write && expr.
id() == ID_member &&
56#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
58 !write && expr.
id() == ID_index &&
64 else if(expr.
id() == ID_member)
87 return apply(ns, state, state.
rename(std::move(tmp), ns).get(), write);
89 return apply(ns, state, std::move(tmp), write);
93 !write && (expr.
id() == ID_byte_extract_little_endian ||
94 expr.
id() == ID_byte_extract_big_endian))
99 be.
op().
type().
id() == ID_union_tag) &&
112 auto recursive_member =
115 recursive_member.has_value() &&
116 (recursive_member->id() == ID_member ||
117 recursive_member->id() == ID_index))
124 ns, state, state.
rename(std::move(tmp), ns).get(), write);
127 return apply(ns, state, std::move(tmp), write);
130 recursive_member.has_value() && recursive_member->id() == ID_typecast)
137 state.
rename(std::move(*recursive_member), ns).get(),
141 return apply(ns, state, std::move(*recursive_member), write);
146#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
147 else if(expr.
id() == ID_index)
166 auto l2_index = state.
rename(index.
index(), ns).get();
181 if(array_from_symbol_table !=
nullptr)
190 if(l2_index.is_constant())
197 index.
index() = l2_index;
202 ns, state, state.
rename(std::move(tmp), ns).get(), write);
205 return apply(ns, state, std::move(tmp), write);
210 exprt expanded_array =
225 bool disjoined_fields_only)
const
228 ssa_expr.
type().
id() == ID_struct ||
229 ssa_expr.
type().
id() == ID_struct_tag ||
230 (!disjoined_fields_only && (ssa_expr.
type().
id() == ID_union ||
231 ssa_expr.
type().
id() == ID_union_tag)))
234 (ssa_expr.
type().
id() == ID_struct_tag ||
235 ssa_expr.
type().
id() == ID_union_tag)
241 fields.reserve(components.size());
245 for(
const auto &comp : components)
255 fields.emplace_back(state.
rename(std::move(field), ns).get());
258 fields.emplace_back(std::move(field));
262 disjoined_fields_only && (ssa_expr.
type().
id() == ID_struct ||
263 ssa_expr.
type().
id() == ID_struct_tag))
270#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
272 ssa_expr.
type().
id() == ID_array &&
284 elements.reserve(array_size);
288 for(std::size_t i = 0; i < array_size; ++i)
298 elements.emplace_back(state.
rename(std::move(element), ns).get());
301 elements.emplace_back(std::move(element));
304 if(disjoined_fields_only)
320 bool allow_pointer_unsoundness)
const
327 ns, state, lhs_fs, rhs, target, allow_pointer_unsoundness);
353 const exprt &ssa_rhs,
355 bool allow_pointer_unsoundness)
const
362 .
assignment(l1_lhs, ssa_rhs, ns,
true,
true, allow_pointer_unsoundness)
384 ssa_rhs.
type().
id() == ID_struct || ssa_rhs.
type().
id() == ID_struct_tag)
387 ssa_rhs.
type().
id() == ID_struct_tag
393 components.empty() ||
396 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
397 for(
const auto &comp : components)
408 const exprt &member_lhs = *fs_it;
416 fs_ssa->get_object_ssa(),
419 allow_pointer_unsoundness);
423 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
428 ssa_rhs.
type().
id() == ID_union || ssa_rhs.
type().
id() == ID_union_tag)
431 ssa_rhs.
type().
id() == ID_union_tag
437 components.empty() ||
440 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
441 for(
const auto &comp : components)
453 const exprt &member_lhs = *fs_it;
461 fs_ssa->get_object_ssa(),
464 allow_pointer_unsoundness);
468 ns, state, member_lhs, member_rhs, target, allow_pointer_unsoundness);
472#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
475 const std::size_t array_size =
482 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
483 for(std::size_t i = 0; i < array_size; ++i)
494 const exprt &index_lhs = *fs_it;
502 fs_ssa->get_object_ssa(),
505 allow_pointer_unsoundness);
509 ns, state, index_lhs, index_rhs, target, allow_pointer_unsoundness);
520 exprt::operandst::const_iterator fs_it = lhs_fs.
operands().begin();
528 fs_ssa->get_object_ssa(),
531 allow_pointer_unsoundness);
535 ns, state, *fs_it, op, target, allow_pointer_unsoundness);
547 bool disjoined_fields_only)
const
549 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
552#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
554 expr.
type().
id() == ID_array &&
564 !disjoined_fields_only &&
565 (expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag))
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
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.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
exprt simplify_opt(exprt e, const value_sett &value_set, const namespacet &ns) const
const bool should_simplify
const std::size_t max_field_sensitivity_array_size
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.
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.
const irep_idt & language_mode
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...
sharing_mapt< irep_idt, exprt > propagation
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Central data structure: state.
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)
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...
symex_targett::sourcet source
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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.
virtual bool simplify(exprt &expr)
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.
State type in value_set_domaint, used in value-set analysis and goto-symex.
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
#define Forall_operands(it, expr)
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, 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.
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Generate Equation using Symbolic Execution.