50 if(expr.
id()==ID_byte_extract_little_endian ||
51 expr.
id()==ID_byte_extract_big_endian)
61 if(be.
op().
type().
id() == ID_array && result.
id() == ID_address_of)
67 t->id() == ID_array && expr.
type() != *t;
79 result=plus_exprt(result, offset);
82 const typet &expr_type = expr.
type();
83 typet dest_type_subtype;
85 if(expr_type.
id()==ID_array && !keep_array)
88 dest_type_subtype=expr_type;
90 result=typecast_exprt(result,
pointer_type(dest_type_subtype));
92 else if(expr.
id()==ID_index ||
95 object_descriptor_exprt ode;
98 const byte_extract_exprt be =
106 else if(expr.
id()==ID_dereference)
115 else if(expr.
id()==ID_if)
130 else if(expr.
id()==ID_symbol ||
131 expr.
id()==ID_string_constant ||
132 expr.
id()==ID_label ||
140 if(result.
type().
id() == ID_array && !keep_array)
149 offset = *offset_opt;
164 result=address_of_exprt(result);
166 else if(expr.
id() == ID_typecast)
173 const typet &expr_type = expr.
type();
174 typet dest_type_subtype;
176 if(expr_type.
id() == ID_array && !keep_array)
179 dest_type_subtype = expr_type;
181 result = typecast_exprt(result,
pointer_type(dest_type_subtype));
184 throw unsupported_operation_exceptiont(
185 "goto_symext::address_arithmetic does not handle " + expr.
id_string());
187 const typet &expr_type = expr.
type();
189 (expr_type.
id() == ID_array && !keep_array) ||
191 "either non-persistent array or pointer to result");
199 auto const cache_key = [&] {
201 state.field_sensitivity.apply(
ns, state, dereference_result,
false);
204 let_expr->value() = state.rename<
L2>(let_expr->value(),
ns).get();
208 cache_key = state.rename<
L2>(cache_key,
ns).get();
213 if(
auto cached = state.dereference_cache.find(cache_key))
230 auto cache_value = cache_key;
231 lift_lets(state, cache_value);
233 auto assign = symex_assignt{
242 assign.assign_symbol(
248 state.dereference_cache.insert(cache_key, cache_symbol_expr);
249 return cache_symbol_expr;
267 bool is_in_binding_expression)
269 if(expr.
id()==ID_dereference)
271 bool expr_is_not_null =
false;
273 if(state.threads.size() == 1)
275 const irep_idt &expr_function = state.source.function_id;
276 if(!expr_function.
empty())
278 const dereference_exprt to_check =
281 expr_is_not_null = path_storage.safe_pointers.at(expr_function)
282 .is_safe_dereference(to_check, state.source.pc);
319 "simplify re-introduced dereferencing");
322 tmp1 = state.field_sensitivity.apply(
ns, state, std::move(tmp1),
false);
330 symex_dereference_state,
333 log.get_message_handler());
354 symex_config.cache_dereferences && !write && !is_in_binding_expression &&
355 (tmp2.
id() == ID_if || tmp2.
id() == ID_let))
361 expr = std::move(tmp2);
365 expr.
id() == ID_index &&
to_index_expr(expr).array().
id() == ID_member &&
374 address_of_exprt address_of_expr(index_expr.
array());
377 dereference_exprt tmp{plus_exprt{address_of_expr, index_expr.
index()}};
385 else if(expr.
id()==ID_index &&
391 else if(expr.
id()==ID_address_of)
395 exprt &
object=address_of_expr.
object();
400 else if(expr.
id()==ID_typecast)
406 tc_op.
id() == ID_address_of &&
412 expr = address_of_exprt(index_exprt(
424 bool is_binding_expression =
429 *it, state, write, is_in_binding_expression || is_binding_expression);
439 deref->op() = f(std::move(deref->op()));
494 ns, state, state.
rename<
L1>(std::move(e),
ns).get(),
false);
501 expr = state.
rename<
L1>(std::move(expr),
ns).get();
526 "simplify re-introduced dereferencing");
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)
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
bitvector_typet c_index_type()
const typet & element_type() const
The type of the elements of the array.
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
call_stackt & call_stack()
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...
field_sensitivityt field_sensitivity
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
symex_target_equationt & target
The equation that this execution is building up.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
void trigger_auto_object(const exprt &, statet &)
friend class symex_dereference_statet
virtual void do_simplify(exprt &expr, const value_sett &value_set)
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
symbol_exprt cache_dereference(exprt &dereference_result, statet &state)
messaget log
The messaget to write log messages to.
const symex_configt symex_config
The configuration to use for this symbolic execution.
void dereference_rec(exprt &expr, statet &state, bool write, bool is_in_quantifier)
const std::string & id_string() const
const irep_idt & id() const
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
const typet & base_type() const
The type of the data what we point to.
Expression to hold a symbol (variable)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const typet & subtype() const
#define Forall_operands(it, expr)
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.
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Storage of symbolic execution paths to resume.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
@ L1_WITH_CONSTANT_PROPAGATION
exprt get_original_name(exprt expr)
Undo all levels of renaming.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.
bool can_cast_expr< binding_exprt >(const exprt &base)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool can_cast_expr< let_exprt >(const exprt &base)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Symbolic Execution of assignments.
static exprt apply_to_objects_in_dereference(exprt e, const std::function< exprt(exprt)> &f)
Symbolic Execution of ANSI-C.
const type_with_subtypet & to_type_with_subtype(const typet &type)