Go to the documentation of this file.
48 lhs.
type() == rhs.
type(),
"assignments must be type consistent");
52 mstream <<
"Assignment to " << format(lhs) <<
" ["
53 << pointer_offset_bits(lhs.type(), ns).value_or(0) <<
" bits]"
64 if(rhs.
id() == ID_side_effect)
70 statement == ID_cpp_new || statement == ID_cpp_new_array ||
71 statement == ID_java_new_array_data)
75 else if(statement == ID_allocate)
77 else if(statement == ID_va_start)
88 lhs.
id() == ID_symbol &&
100 if(state.
source.
pc->source_location.get_hide())
132 const auto &ibv_type =
135 const std::size_t n_bits = ibv_type.get_width();
138 static_assert(CHAR_BIT == 8,
"bitwidth of char assumed to be 8");
140 const std::size_t n_chars = n_bits / 8;
143 sizeof(std::size_t) >= n_chars,
144 "size_t shall be large enough to represent a character");
148 for(
const auto &c : char_array.
operands())
152 for(std::size_t i = 0; i < n_chars; i++)
154 const char c_chunk =
static_cast<char>((c_val >> (i * 8)) & 0xff);
155 result.push_back(c_chunk);
168 if(rhs.
id() == ID_function_application)
177 if(func_id == ID_cprover_string_concat_func)
181 else if(func_id == ID_cprover_string_empty_string_func)
188 else if(func_id == ID_cprover_string_substring_func)
193 func_id == ID_cprover_string_of_int_func ||
194 func_id == ID_cprover_string_of_long_func)
198 else if(func_id == ID_cprover_string_delete_char_at_func)
202 else if(func_id == ID_cprover_string_delete_func)
206 else if(func_id == ID_cprover_string_set_length_func)
210 else if(func_id == ID_cprover_string_char_set_func)
214 else if(func_id == ID_cprover_string_trim_func)
218 else if(func_id == ID_cprover_string_to_lower_case_func)
222 else if(func_id == ID_cprover_string_to_upper_case_func)
226 else if(func_id == ID_cprover_string_replace_func)
252 const std::string aux_symbol_name =
255 const bool string_constant_exists =
259 string_constant_exists
262 state,
symex_assign, aux_symbol_name, char_array, new_char_array);
265 aux_symbol.
value == new_char_array,
266 "symbol shall have value derived from char array content");
273 if(!string_constant_exists)
283 const std::string &aux_symbol_name,
288 new_char_array_type.
set(ID_C_constant,
true);
306 new_aux_symbol.
value = new_char_array;
313 return new_aux_symbol;
322 const symbolt &function_symbol =
323 ns.
lookup(ID_cprover_associate_array_to_pointer_func);
326 function_symbol.
symbol_expr(), {new_char_array, string_data}};
333 function_symbol.
mode,
346 const exprt &content)
348 if(content.
id() != ID_symbol)
353 const auto s_pointer_opt =
367 if(expr.
id() != ID_symbol)
372 const auto constant_expr_opt =
375 if(!constant_expr_opt || constant_expr_opt->get().id() != ID_constant)
390 const auto &length_type = f_type.
domain().at(0);
399 "empty string primitive requires two output arguments");
418 const auto &length_type = f_type.
domain().at(0);
437 const std::size_t new_size =
449 const array_exprt new_char_array(std::move(operands), new_char_array_type);
455 new_char_array_length,
467 const std::size_t num_operands = f_l1.
arguments().size();
473 const auto &length_type = f_type.
domain().at(0);
486 if(num_operands == 5)
488 const auto end_index_expr_opt =
491 if(!end_index_expr_opt)
499 if(end_index < 0 || end_index > s_data.
operands().size())
506 end_index = s_data.
operands().size();
509 const auto start_index_expr_opt =
512 if(!start_index_expr_opt)
520 if(start_index < 0 || start_index > end_index)
532 s_data.
operands().begin(), numeric_cast_v<std::size_t>(start_index)),
534 s_data.
operands().begin(), numeric_cast_v<std::size_t>(end_index)));
536 const array_exprt new_char_array(std::move(operands), new_char_array_type);
542 new_char_array_length,
559 const std::size_t num_operands = f_l1.
arguments().size();
565 const auto &length_type = f_type.
domain().at(0);
568 const auto &integer_opt =
576 const mp_integer integer = numeric_cast_v<mp_integer>(integer_opt->get());
580 if(num_operands == 4)
582 const auto &base_constant_opt =
585 if(!base_constant_opt)
590 const auto base_opt = numeric_cast<unsigned>(base_constant_opt->get());
612 std::back_inserter(operands),
613 [&
char_type](
const char c) { return from_integer(tolower(c), char_type); });
615 const array_exprt new_char_array(std::move(operands), new_char_array_type);
621 new_char_array_length,
641 const auto &length_type = f_type.
domain().at(0);
661 const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());
663 if(index < 0 || index >= s_data.
operands().size())
674 operands.reserve(s_data.
operands().size() - 1);
676 const std::size_t i = numeric_cast_v<std::size_t>(index);
681 std::next(s_data.
operands().begin(), i));
685 std::next(s_data.
operands().begin(), i + 1),
688 const array_exprt new_char_array(std::move(operands), new_char_array_type);
694 new_char_array_length,
715 const auto &length_type = f_type.
domain().at(0);
735 const mp_integer start = numeric_cast_v<mp_integer>(start_opt->get());
737 if(start < 0 || start > s_data.
operands().size())
749 const mp_integer end = numeric_cast_v<mp_integer>(end_opt->get());
756 const std::size_t start_index = numeric_cast_v<std::size_t>(start);
758 const std::size_t end_index =
759 std::min(numeric_cast_v<std::size_t>(end), s_data.
operands().size());
761 const std::size_t new_size =
762 s_data.
operands().size() - end_index + start_index;
770 operands.reserve(new_size);
775 std::next(s_data.
operands().begin(), start_index));
779 std::next(s_data.
operands().begin(), end_index),
782 const array_exprt new_char_array(std::move(operands), new_char_array_type);
788 new_char_array_length,
808 const auto &length_type = f_type.
domain().at(0);
811 const auto &new_length_opt =
820 numeric_cast_v<mp_integer>(new_length_opt->get());
827 const std::size_t new_size = numeric_cast_v<std::size_t>(new_length);
838 operands.reserve(new_size);
855 std::min(new_size, s_data.
operands().size())));
859 new_size - std::min(new_size, s_data.
operands().size()),
863 const array_exprt new_char_array(std::move(operands), new_char_array_type);
869 new_char_array_length,
890 const auto &length_type = f_type.
domain().at(0);
910 const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());
912 if(index < 0 || index >= s_data.
operands().size())
917 const auto &new_char_opt =
930 s_data.
operands()[numeric_cast_v<std::size_t>(index)] = new_char_opt->get();
933 std::move(s_data.
operands()), new_char_array_type);
939 new_char_array_length,
953 const auto &length_type = f_type.
domain().at(0);
964 auto &operands = string_data.
operands();
965 for(
auto &operand : operands)
968 auto character = numeric_cast_v<unsigned int>(constant_value);
974 if(isalpha(character))
978 if(islower(character))
980 from_integer(toupper(character), constant_value.type());
984 if(isupper(character))
986 from_integer(tolower(character), constant_value.type());
995 const array_exprt new_char_array(std::move(operands), new_char_array_type);
1001 new_char_array_length,
1014 const auto &length_type = f_type.
domain().at(0);
1023 auto &new_data = f_l1.
arguments().at(4);
1024 auto &old_data = f_l1.
arguments().at(3);
1030 bool is_single_character = new_data.type().id() == ID_unsignedbv &&
1031 old_data.type().id() == ID_unsignedbv;
1032 if(is_single_character)
1037 if(!new_char_pointer || !old_char_pointer)
1042 characters_to_find.emplace_back(old_char_pointer->get());
1043 characters_to_replace.emplace_back(new_char_pointer->get());
1050 const auto new_char_array_opt =
1053 const auto old_char_array_opt =
1056 if(!new_char_array_opt || !old_char_array_opt)
1061 characters_to_find = old_char_array_opt->get().operands();
1062 characters_to_replace = new_char_array_opt->get().operands();
1067 auto found_pattern = std::search(
1070 characters_to_find.begin(),
1071 characters_to_find.end());
1074 while(found_pattern != existing_data.
operands().end())
1077 auto match_end = found_pattern + characters_to_find.size();
1080 found_pattern = existing_data.
operands().erase(found_pattern, match_end);
1084 found_pattern = existing_data.
operands().insert(
1086 characters_to_replace.begin(),
1087 characters_to_replace.end()) +
1088 characters_to_replace.size();
1091 found_pattern = std::search(
1094 characters_to_find.begin(),
1095 characters_to_find.end());
1103 std::move(existing_data.
operands()), new_char_array_type);
1109 new_char_array_length,
1122 const auto &length_type = f_type.
domain().at(0);
1131 auto is_not_whitespace = [](
const exprt &expr) {
1133 return character >
' ';
1137 auto &operands = s_data_opt->get().operands();
1139 std::find_if(operands.rbegin(), operands.rend(), is_not_whitespace);
1141 std::find_if(operands.begin(), operands.end(), is_not_whitespace);
1147 if(start_iter != operands.end())
1155 std::move(new_operands), new_char_array_type);
1161 new_char_array_length,
#define UNREACHABLE
This should be used to mark dead code.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & subtype() const
Symbolic Execution of assignments.
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
optionalt< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
#define CHECK_RETURN(CONDITION)
std::string escape_non_alnum(const std::string &to_escape)
Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.
refined_string_exprt & to_string_expr(exprt &expr)
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
Fresh auxiliary symbol creation.
goto_programt::const_targett pc
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
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.
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.
symex_target_equationt & target
The equation that this execution is building up.
typet type
Type of symbol.
Central data structure: state.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
bool constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate trim operations.
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.
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.
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...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Base class for all expressions.
symex_targett::sourcet source
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.
Functor for symex assignment.
side_effect_exprt & to_side_effect_expr(exprt &expr)
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.
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.
bitvector_typet index_type()
const exprt & get_original_expr() const
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.
sharing_mapt< irep_idt, exprt > propagation
messaget log
The messaget to write log messages to.
Expression providing an SSA-renamed symbol of expressions.
const mathematical_function_typet & function_type() const
This helper method provides the type of the expression returned by function.
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const array_typet & type() const
std::vector< threadt > threads
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.
bool constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate string concatenation.
call_stackt & call_stack()
irep_idt mode
Language mode.
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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const std::string & id2string(const irep_idt &d)
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
void constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Create an empty string constant.
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_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the length of a string.
#define PRECONDITION(CONDITION)
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.
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
const irep_idt & get_identifier() const
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
bool simplify(exprt &expr, const namespacet &ns)
Application of (mathematical) function.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
std::vector< exprt > operandst
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
nonstd::optional< T > optionalt
virtual void do_simplify(exprt &expr)
field_sensitivityt field_sensitivity
const irep_idt & get_statement() const
bitvector_typet char_type()
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
exprt value
Initial value of symbol.
const exprt & content() const
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
virtual void symex_assume(statet &state, const exprt &cond)
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
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...
const symex_configt symex_config
The configuration to use for this symbolic execution.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
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)
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...
static optionalt< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)
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...
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A constant literal expression.
bool constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant proagate character replacement.
String expressions for the string solver.
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.
Array constructor from list of elements.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
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 ...
An expression containing a side effect.
Expression in which some part is missing and can be substituted for another expression.
API to expression classes for 'mathematical' expressions.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)