1/*******************************************************************\
3Module: Symbolic Execution
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
23// We can either use with_exprt or update_exprt when building expressions that
24// modify components of an array or a struct. Set USE_UPDATE to use
68 // Allocate shadow memory
95 // should have been replaced by byte_extract
97 "assign_rec: unexpected assignment to union member");
101 "assign_rec: unexpected assignment to member of '" + type.
id_string() +
119 // this is stuff like __real__ x = 1;
142 "assignment to '" + lhs.
id_string() +
"' not handled");
171 const auto &components =
184 "member of symbol should be susceptible to field-sensitivity");
199 // put assignment guard into the rhs
225 // Note any other symbols mentioned in the skeleton are rvalues -- for example
226 // array indices -- and were renamed to L2 at the start of
227 // goto_symext::symex_assign.
237 ns.lookup(
l2_lhs.get_object_name()).is_auxiliary &&
255 // Split composite symbol lhs into its components
272 // Shortcut the common case of a whole-struct initializer:
285 // these may come from dereferencing on the lhs
292template <
bool use_update>
310 // a'==UPDATE(a, [i], e)
329template <
bool use_update>
336 // Symbolic execution of a struct member assignment.
338 // lhs must be member operand, which
339 // takes one operand, which must be a structure.
343 // typecasts involved? C++ does that for inheritance.
348 // ignore, and give up
353 // remove the type cast, we assume that the member is there
359 return;
// ignore and give up
370 // a'==UPDATE(a, .c, e)
398 // we have (c?a:b)=e;
415 // we have byte_extract_X(object, offset)=value
416 // turn into object=byte_update_X(object, offset, value)
static irep_idt byte_update_id()
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
static exprt guard(const exprt::operandst &guards, exprt cond)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Complex constructor from a pair of numbers.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Expression in which some part is missing and can be substituted for another expression.
expr_skeletont compose(expr_skeletont other) const
Replace the missing part of the current skeleton by another skeleton, ending in a bigger skeleton cor...
static expr_skeletont remove_op0(exprt e)
Create a skeleton by removing the first operand of e.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
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.
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...
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
std::stack< bool > record_events
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...
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
irep_idt get_component_name() const
Expression providing an SSA-renamed symbol of expressions.
Struct constructor from list of elements.
void assign_byte_extract(const byte_extract_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_if(const if_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
const irep_idt & language_mode
const symex_configt & symex_config
void assign_non_struct_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
goto_symex_statet & state
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_rec(const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1}...
void assign_struct_member(const member_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett::assignment_typet assignment_type
void assign_from_struct(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const struct_exprt &rhs, const exprt::operandst &guard)
Assign a struct expression to a symbol.
void assign_typecast(const typecast_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
std::optional< shadow_memoryt > shadow_memory
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.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Thrown when we encounter an instruction, parameters to an instruction etc.
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt get_original_name(exprt expr)
Undo all levels of renaming.
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
#define SHADOW_MEMORY_SYMBOL_PREFIX
#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.
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_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 complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Assignment from the rhs value to the lhs variable.
expr_skeletont original_lhs_skeleton
Skeleton to reconstruct the original lhs in the assignment.
constexpr bool use_update()
static bool is_string_constant_initialization(const exprt &rhs)
Determine whether the RHS expression is a string constant initialization.
Symbolic Execution of assignments.