Go to the documentation of this file.
44 lhs.
type() == rhs.
type(),
"assignments must be type consistent");
48 mstream <<
"Assignment to " << format(lhs) <<
" ["
49 << pointer_offset_bits(lhs.type(), ns).value_or(0) <<
" bits]"
60 if(rhs.
id() == ID_side_effect)
66 statement == ID_cpp_new || statement == ID_cpp_new_array ||
67 statement == ID_java_new_array_data)
71 else if(statement == ID_allocate)
73 else if(statement == ID_va_start)
84 lhs.
id() == ID_symbol &&
96 if(state.
source.
pc->source_location.get_hide())
128 const auto &ibv_type =
131 const std::size_t n_bits = ibv_type.get_width();
134 static_assert(CHAR_BIT == 8,
"bitwidth of char assumed to be 8");
136 const std::size_t n_chars = n_bits / 8;
139 sizeof(std::size_t) >= n_chars,
140 "size_t shall be large enough to represent a character");
144 for(
const auto &c : char_array.
operands())
148 for(std::size_t i = 0; i < n_chars; i++)
150 const char c_chunk =
static_cast<char>((c_val >> (i * 8)) & 0xff);
151 result.push_back(c_chunk);
164 if(rhs.
id() == ID_function_application)
173 if(func_id == ID_cprover_string_concat_func)
177 else if(func_id == ID_cprover_string_empty_string_func)
184 else if(func_id == ID_cprover_string_substring_func)
189 func_id == ID_cprover_string_of_int_func ||
190 func_id == ID_cprover_string_of_long_func)
194 else if(func_id == ID_cprover_string_delete_char_at_func)
198 else if(func_id == ID_cprover_string_delete_func)
202 else if(func_id == ID_cprover_string_set_length_func)
206 else if(func_id == ID_cprover_string_char_set_func)
210 else if(func_id == ID_cprover_string_trim_func)
214 else if(func_id == ID_cprover_string_to_lower_case_func)
218 else if(func_id == ID_cprover_string_to_upper_case_func)
222 else if(func_id == ID_cprover_string_replace_func)
248 const std::string aux_symbol_name =
251 const bool string_constant_exists =
255 string_constant_exists
258 state,
symex_assign, aux_symbol_name, char_array, new_char_array);
261 aux_symbol.
value == new_char_array,
262 "symbol shall have value derived from char array content");
269 if(!string_constant_exists)
279 const std::string &aux_symbol_name,
284 new_char_array_type.
set(ID_C_constant,
true);
302 new_aux_symbol.
value = new_char_array;
309 return new_aux_symbol;
318 const symbolt &function_symbol =
319 ns.
lookup(ID_cprover_associate_array_to_pointer_func);
322 function_symbol.
symbol_expr(), {new_char_array, string_data}};
329 function_symbol.
mode,
342 const exprt &content)
344 if(content.
id() != ID_symbol)
349 const auto s_pointer_opt =
363 if(expr.
id() != ID_symbol)
368 const auto constant_expr_opt =
371 if(!constant_expr_opt || constant_expr_opt->get().id() != ID_constant)
386 const auto &length_type = f_type.domain().at(0);
395 "empty string primitive requires two output arguments");
414 const auto &length_type = f_type.domain().at(0);
433 const std::size_t new_size =
445 const array_exprt new_char_array(std::move(operands), new_char_array_type);
451 new_char_array_length,
463 const std::size_t num_operands = f_l1.
arguments().size();
469 const auto &length_type = f_type.domain().at(0);
482 if(num_operands == 5)
484 const auto end_index_expr_opt =
487 if(!end_index_expr_opt)
495 if(end_index < 0 || end_index > s_data.
operands().size())
502 end_index = s_data.
operands().size();
505 const auto start_index_expr_opt =
508 if(!start_index_expr_opt)
516 if(start_index < 0 || start_index > end_index)
528 s_data.
operands().begin(), numeric_cast_v<std::size_t>(start_index)),
530 s_data.
operands().begin(), numeric_cast_v<std::size_t>(end_index)));
532 const array_exprt new_char_array(std::move(operands), new_char_array_type);
538 new_char_array_length,
555 const std::size_t num_operands = f_l1.
arguments().size();
561 const auto &length_type = f_type.domain().at(0);
564 const auto &integer_opt =
572 const mp_integer integer = numeric_cast_v<mp_integer>(integer_opt->get());
576 if(num_operands == 4)
578 const auto &base_constant_opt =
581 if(!base_constant_opt)
586 const auto base_opt = numeric_cast<unsigned>(base_constant_opt->get());
608 std::back_inserter(operands),
609 [&
char_type](
const char c) { return from_integer(tolower(c), char_type); });
611 const array_exprt new_char_array(std::move(operands), new_char_array_type);
617 new_char_array_length,
637 const auto &length_type = f_type.domain().at(0);
657 const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());
659 if(index < 0 || index >= s_data.
operands().size())
670 operands.reserve(s_data.
operands().size() - 1);
672 const std::size_t i = numeric_cast_v<std::size_t>(index);
677 std::next(s_data.
operands().begin(), i));
681 std::next(s_data.
operands().begin(), i + 1),
684 const array_exprt new_char_array(std::move(operands), new_char_array_type);
690 new_char_array_length,
711 const auto &length_type = f_type.domain().at(0);
731 const mp_integer start = numeric_cast_v<mp_integer>(start_opt->get());
733 if(start < 0 || start > s_data.
operands().size())
745 const mp_integer end = numeric_cast_v<mp_integer>(end_opt->get());
752 const std::size_t start_index = numeric_cast_v<std::size_t>(start);
754 const std::size_t end_index =
755 std::min(numeric_cast_v<std::size_t>(end), s_data.
operands().size());
757 const std::size_t new_size =
758 s_data.
operands().size() - end_index + start_index;
766 operands.reserve(new_size);
771 std::next(s_data.
operands().begin(), start_index));
775 std::next(s_data.
operands().begin(), end_index),
778 const array_exprt new_char_array(std::move(operands), new_char_array_type);
784 new_char_array_length,
804 const auto &length_type = f_type.domain().at(0);
807 const auto &new_length_opt =
816 numeric_cast_v<mp_integer>(new_length_opt->get());
823 const std::size_t new_size = numeric_cast_v<std::size_t>(new_length);
834 operands.reserve(new_size);
851 std::min(new_size, s_data.
operands().size())));
855 new_size - std::min(new_size, s_data.
operands().size()),
859 const array_exprt new_char_array(std::move(operands), new_char_array_type);
865 new_char_array_length,
886 const auto &length_type = f_type.domain().at(0);
906 const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());
908 if(index < 0 || index >= s_data.
operands().size())
913 const auto &new_char_opt =
926 s_data.
operands()[numeric_cast_v<std::size_t>(index)] = new_char_opt->get();
929 std::move(s_data.
operands()), new_char_array_type);
935 new_char_array_length,
949 const auto &length_type = f_type.domain().at(0);
960 auto &operands = string_data.
operands();
961 for(
auto &operand : operands)
964 auto character = numeric_cast_v<unsigned int>(constant_value);
970 if(isalpha(character))
974 if(islower(character))
976 from_integer(toupper(character), constant_value.type());
980 if(isupper(character))
982 from_integer(tolower(character), constant_value.type());
991 const array_exprt new_char_array(std::move(operands), new_char_array_type);
997 new_char_array_length,
1010 const auto &length_type = f_type.domain().at(0);
1019 auto &new_data = f_l1.
arguments().at(4);
1020 auto &old_data = f_l1.
arguments().at(3);
1026 bool is_single_character = new_data.type().id() == ID_unsignedbv &&
1027 old_data.type().id() == ID_unsignedbv;
1028 if(is_single_character)
1033 if(!new_char_pointer || !old_char_pointer)
1038 characters_to_find.emplace_back(old_char_pointer->get());
1039 characters_to_replace.emplace_back(new_char_pointer->get());
1046 const auto new_char_array_opt =
1049 const auto old_char_array_opt =
1052 if(!new_char_array_opt || !old_char_array_opt)
1057 characters_to_find = old_char_array_opt->get().operands();
1058 characters_to_replace = new_char_array_opt->get().operands();
1063 auto found_pattern = std::search(
1066 characters_to_find.begin(),
1067 characters_to_find.end());
1070 while(found_pattern != existing_data.
operands().end())
1073 auto match_end = found_pattern + characters_to_find.size();
1076 found_pattern = existing_data.
operands().erase(found_pattern, match_end);
1080 found_pattern = existing_data.
operands().insert(
1082 characters_to_replace.begin(),
1083 characters_to_replace.end()) +
1084 characters_to_replace.size();
1087 found_pattern = std::search(
1090 characters_to_find.begin(),
1091 characters_to_find.end());
1099 std::move(existing_data.
operands()), new_char_array_type);
1105 new_char_array_length,
1118 const auto &length_type = f_type.domain().at(0);
1127 auto is_not_whitespace = [](
const exprt &expr) {
1129 return character >
' ';
1133 auto &operands = s_data_opt->get().operands();
1135 std::find_if(operands.rbegin(), operands.rend(), is_not_whitespace);
1137 std::find_if(operands.begin(), operands.end(), is_not_whitespace);
1143 if(start_iter != operands.end())
1151 std::move(new_operands), new_char_array_type);
1157 new_char_array_length,
#define UNREACHABLE
This should be used to mark dead code.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
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
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.
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)
Symbolically execute an assignment instruction that has a CPP new or new array or a Java new array on...
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)
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 symex_assign(statet &state, const code_assignt &code)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
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.
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 integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_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
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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)
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.
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 codet representing an assignment in the program.
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.
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)