49 lhs.
type() == rhs.
type(),
"assignments must be type consistent");
53 mstream <<
"Assignment to " << format(lhs) <<
" ["
54 << pointer_offset_bits(lhs.type(), ns).value_or(0) <<
" bits]"
101 if(state.
source.
pc->source_location().get_hide())
139 static_assert(
CHAR_BIT == 8,
"bitwidth of char assumed to be 8");
144 sizeof(std::size_t) >=
n_chars,
145 "size_t shall be large enough to represent a character");
155 const char c_chunk =
static_cast<char>((
c_val >> (
i * 8)) & 0xff);
267 "symbol shall have value derived from char array content");
347 const exprt &content)
391 const auto &length_type =
f_type.domain().at(0);
399 f_l1.arguments().size() >= 2,
400 "empty string primitive requires two output arguments");
419 const auto &length_type =
f_type.domain().at(0);
448 operands.end(),
s2_data.operands().begin(),
s2_data.operands().end());
474 const auto &length_type =
f_type.domain().at(0);
566 const auto &length_type =
f_type.domain().at(0);
613 std::back_inserter(operands),
614 [&
char_type](
const char c) { return from_integer(tolower(c), char_type); });
642 const auto &length_type =
f_type.domain().at(0);
675 operands.reserve(
s_data.operands().size() - 1);
681 s_data.operands().begin(),
682 std::next(
s_data.operands().begin(),
i));
686 std::next(
s_data.operands().begin(),
i + 1),
716 const auto &length_type =
f_type.domain().at(0);
775 s_data.operands().begin(),
809 const auto &length_type =
f_type.domain().at(0);
853 s_data.operands().begin(),
855 s_data.operands().begin(),
891 const auto &length_type =
f_type.domain().at(0);
954 const auto &length_type =
f_type.domain().at(0);
1015 const auto &length_type =
f_type.domain().at(0);
1123 const auto &length_type =
f_type.domain().at(0);
1134 return character >
' ';
1138 auto &operands =
s_data_opt->get().operands();
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
bitvector_typet char_type()
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
const typet & element_type() const
The type of the elements of the array.
A constant literal expression.
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.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
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.
Application of (mathematical) function.
sharing_mapt< irep_idt, exprt > propagation
Central data structure: state.
call_stackt & call_stack()
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 exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
std::vector< threadt > threads
virtual void symex_assume(statet &state, const exprt &cond)
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
bool constant_propagate_delete_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a character from a string.
bool constant_propagate_set_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the char at the given index.
bool constant_propagate_assignment_with_side_effects(statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)
Attempt to constant propagate side effects of the assignment (if any)
bool constant_propagate_delete(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a substring from a string.
void constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Create an empty string constant.
symex_target_equationt & target
The equation that this execution is building up.
bool constant_propagate_case_change(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)
Attempt to constant propagate case changes, both upper and lower.
virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has an allocate on the right hand side.
bool constant_propagate_integer_to_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate converting an integer to a string.
bool constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate trim operations.
static optionalt< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
const symbolt & get_new_string_data_symbol(statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)
Installs a new symbol in the symbol table to represent the given character array, and assigns the cha...
void associate_array_to_pointer(statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)
Generate array to pointer association primitive.
virtual void do_simplify(exprt &expr)
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
bool constant_propagate_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the length of a string.
messaget log
The messaget to write log messages to.
const symex_configt symex_config
The configuration to use for this symbolic execution.
bool constant_propagate_string_substring(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate getting a substring of a string.
bool constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant proagate character replacement.
bool constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate string concatenation.
void assign_string_constant(statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)
Assign constant string length and string data given by a char array to given ssa variables.
optionalt< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
const irep_idt & id() const
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const typet & base_type() const
The type of the data what we point to.
const exprt & content() const
An expression containing a side effect.
Expression providing an SSA-renamed symbol of expressions.
const irep_idt & get_identifier() const
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Functor for symex assignment.
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.
static std::string get_alnum_string(const array_exprt &char_array)
Maps the given array expression containing constant characters to a string containing only alphanumer...
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
const std::string integer2string(const mp_integer &n, unsigned base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool simplify(exprt &expr, const namespacet &ns)
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
side_effect_exprt & to_side_effect_expr(exprt &expr)
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
std::string escape_non_alnum(const std::string &to_escape)
Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.
goto_programt::const_targett pc
Symbolic Execution of assignments.