33 : array_pool(fresh_symbol), ns(ns)
44 std::ostringstream buf;
45 buf <<
"string_refinement#" << prefix <<
"#" << ++
symbol_count;
49 created_symbols.push_back(result);
100 const exprt &char_pointer,
101 const typet &char_array_type)
106 char_array_type.
subtype().
id() == ID_unsignedbv ||
107 char_array_type.
subtype().
id() == ID_signedbv);
109 if(char_pointer.
id() == ID_if)
124 const bool is_constant_array =
125 char_pointer.
id() == ID_address_of &&
127 char_pointer.
op0().
op0().
id() == ID_array;
128 if(is_constant_array)
133 const std::string symbol_name =
"char_array_" +
id2string(char_pointer.
id());
134 const auto array_sym =
136 const auto insert_result =
142 const exprt &pointer_expr,
150 array_expr.
length() = pair.first->second;
157 it_bool.second,
"should not associate two arrays to the same pointer");
259 const std::string &char_set)
264 const char &low_char = char_set[0];
265 const char &high_char = char_set[2];
269 const exprt chr = s[qvar];
275 return {{}, {sc}, {}};
305 const exprt &end = args.size() >= 5 ? args[4] : s.
length();
307 fresh_symbol, s, start, end, char_set_string.
c_str());
327 const exprt &pointer,
330 return pool.
find(pointer, length);
336 return array_pool.
find(string_argument.op1(), string_argument.op0());
356 if(
id == ID_cprover_associate_array_to_pointer_func)
358 else if(
id == ID_cprover_associate_length_to_array_func)
369 std::pair<exprt, string_constraintst>
376 if(
id==ID_cprover_char_literal_func)
378 else if(
id==ID_cprover_string_length_func)
380 else if(
id==ID_cprover_string_equal_func)
382 else if(
id==ID_cprover_string_equals_ignore_case_func)
384 else if(
id==ID_cprover_string_is_empty_func)
386 else if(
id==ID_cprover_string_char_at_func)
388 else if(
id==ID_cprover_string_is_prefix_func)
390 else if(
id==ID_cprover_string_is_suffix_func)
392 else if(
id==ID_cprover_string_startswith_func)
394 else if(
id==ID_cprover_string_endswith_func)
396 else if(
id==ID_cprover_string_contains_func)
398 else if(
id==ID_cprover_string_hash_code_func)
400 else if(
id==ID_cprover_string_index_of_func)
402 else if(
id==ID_cprover_string_last_index_of_func)
404 else if(
id==ID_cprover_string_parse_int_func)
406 else if(
id==ID_cprover_string_code_point_at_func)
408 else if(
id==ID_cprover_string_code_point_before_func)
410 else if(
id==ID_cprover_string_code_point_count_func)
412 else if(
id==ID_cprover_string_offset_by_code_point_func)
414 else if(
id==ID_cprover_string_compare_to_func)
416 else if(
id==ID_cprover_string_literal_func)
418 else if(
id==ID_cprover_string_concat_code_point_func)
420 else if(
id==ID_cprover_string_insert_func)
422 else if(
id==ID_cprover_string_insert_int_func)
424 else if(
id==ID_cprover_string_insert_long_func)
426 else if(
id==ID_cprover_string_insert_bool_func)
428 else if(
id==ID_cprover_string_insert_char_func)
430 else if(
id==ID_cprover_string_insert_double_func)
432 else if(
id==ID_cprover_string_insert_float_func)
434 else if(
id==ID_cprover_string_substring_func)
436 else if(
id==ID_cprover_string_trim_func)
438 else if(
id==ID_cprover_string_empty_string_func)
440 else if(
id==ID_cprover_string_copy_func)
442 else if(
id==ID_cprover_string_of_int_hex_func)
444 else if(
id==ID_cprover_string_of_float_func)
446 else if(
id==ID_cprover_string_of_float_scientific_notation_func)
449 else if(
id==ID_cprover_string_of_double_func)
451 else if(
id==ID_cprover_string_of_long_func)
453 else if(
id==ID_cprover_string_of_bool_func)
455 else if(
id==ID_cprover_string_of_char_func)
457 else if(
id==ID_cprover_string_set_length_func)
459 else if(
id==ID_cprover_string_delete_func)
461 else if(
id==ID_cprover_string_delete_char_at_func)
463 else if(
id==ID_cprover_string_replace_func)
465 else if(
id==ID_cprover_string_intern_func)
467 else if(
id==ID_cprover_string_format_func)
469 else if(
id == ID_cprover_string_constrain_characters_func)
474 "string_constraint_generator::function_application: unknown symbol :");
495 const auto &args=f.arguments();
502 const exprt count = args.size() == 3 ? str.
length() : args[4];
504 fresh_symbol, res, str, offset,
plus_exprt(offset, count));
519 return {str.
length(), {}};
538 const exprt &arg=args[0];
541 if(arg.operands().size()==1 &&
542 arg.op0().operands().size()==1 &&
543 arg.op0().op0().operands().size()==2 &&
544 arg.op0().op0().op0().id()==ID_string_constant)
549 return {
from_integer(
unsigned(sval[0]), arg.type()), {}};
573 symbol_exprt char_sym = fresh_symbol(
"char", str.type().subtype());
575 return {char_sym, {{constraint}}};
599 std::pair<exprt, string_constraintst> result1,
600 std::pair<exprt, string_constraintst> result2)
602 const exprt return_code =
maximum(result1.first, result2.first);
603 merge(result2.second, std::move(result1.second));
604 return {return_code, std::move(result2.second)};
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The type of an expression, extends irept.
Generates string constraints to link results from string functions with their arguments.
exprt sum_overflows(const plus_exprt &sum)
A base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
std::pair< exprt, string_constraintst > add_axioms_for_delete(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
Application of (mathematical) function.
static irep_idt get_function_name(const function_application_exprt &expr)
std::pair< exprt, string_constraintst > add_axioms_for_equals(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Equality of the content of two strings.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
String representation of a float value.
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Lexicographic comparison of two strings.
const exprt & content() const
const irep_idt & get_identifier() const
std::pair< exprt, string_constraintst > add_axioms_for_contains(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Test whether a string contains another.
std::pair< symbol_exprt, string_constraintst > add_axioms_for_intern(symbol_generatort &fresh_symbol, const function_application_exprt &f)
Add axioms corresponding to the String.intern java function.
std::pair< exprt, string_constraintst > add_axioms_for_code_point_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
add axioms corresponding to the String.codePointAt java function
exprt minimum(const exprt &a, const exprt &b)
Generation of fresh symbols of a given type.
exprt is_positive(const exprt &x)
const irep_idt & get_value() const
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Equality of the content ignoring case of characters.
std::pair< exprt, string_constraintst > add_axioms_for_is_suffix(symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
Test if the target is a suffix of the string.
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
exprt associate_array_to_pointer(const function_application_exprt &f)
Associate a char array to a char pointer.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
The trinary if-then-else operator.
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
typet & type()
Return the type of the expression.
exprt associate_length_to_array(const function_application_exprt &f)
Associate an integer length to a char array.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const std::set< array_string_exprt > & created_strings() const
std::pair< exprt, string_constraintst > add_axioms_for_insert_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
add axioms corresponding to the StringBuilder.insert(I) java function
std::pair< exprt, string_constraintst > add_axioms_for_copy(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
add axioms to say that the returned string expression is equal to the argument of the function applic...
#define CHECK_RETURN(CONDITION)
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the String.valueOf(Z) java function.
Correspondance between arrays and pointers string representations.
std::pair< exprt, string_constraintst > add_axioms_for_offset_by_code_point(symbol_generatort &fresh_symbol, const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
std::pair< exprt, string_constraintst > add_axioms_for_format(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const messaget &message, const namespacet &ns)
Formatted string using a format string and list of arguments.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
std::pair< exprt, string_constraintst > add_axioms_from_double(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the String.valueOf(D) java function.
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Integer value represented by a string.
std::pair< exprt, string_constraintst > add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(st...
const irep_idt & id() const
void clear()
Clear all constraints.
std::pair< exprt, string_constraintst > add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Remove leading and trailing whitespaces.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
An expression denoting infinity.
std::pair< exprt, string_constraintst > add_axioms_for_insert_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the StringBuilder.insert(F) java function.
std::pair< exprt, string_constraintst > add_axioms_for_function_application(symbol_generatort &fresh_symbol, const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
std::set< array_string_exprt > created_strings_value
array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
Converts a struct containing a length and pointer to an array.
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the String.valueOf(J) java function.
Fixed-width bit-vector with two's complement interpretation.
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &expr, array_poolt &array_pool)
add axioms corresponding to the StringBuilder.deleteCharAt java function
nonstd::optional< T > optionalt
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(symbol_generatort &fresh_symbol, const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
std::vector< string_not_contains_constraintt > not_contains
std::pair< exprt, string_constraintst > add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Character at a given position.
refined_string_exprt & to_string_expr(exprt &expr)
exprt::operandst argumentst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
std::pair< exprt, string_constraintst > add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Reduce or extend a string to have the given length.
The plus expression Associativity is not specified.
std::pair< exprt, string_constraintst > add_axioms_for_constrain_characters(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms to ensure all characters of a string belong to a given set.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
bitvector_typet index_type()
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
std::pair< exprt, string_constraintst > add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
String corresponding to an internal cprover string.
string_constraintst add_constraint_on_characters(symbol_generatort &fresh_symbol, const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
Add constraint on characters of a string.
Various predicates over pointers in programs.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
symbol_exprt & function()
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
std::pair< exprt, string_constraintst > add_axioms_for_code_point_before(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
add axioms corresponding to the String.codePointBefore java function
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
string_constraintst constraints
std::vector< exprt > existential
void insert(const exprt &pointer_expr, array_string_exprt &array)
std::pair< exprt, string_constraintst > add_axioms_for_code_point_count(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Add axioms corresponding the String.codePointCount java function.
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the last occurrence ...
std::pair< exprt, string_constraintst > add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal...
string_constraint_generatort(const namespacet &ns)
signedbv_typet get_return_code_type()
const string_constantt & to_string_constant(const exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
bool is_refined_string_type(const typet &type)
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
std::vector< string_constraintt > universal
std::pair< exprt, string_constraintst > add_axioms_for_is_empty(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms stating that the returned value is true exactly when the argument string is empty...
irep_idt get_object_name() const
std::pair< exprt, string_constraintst > add_axioms_for_insert_double(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
add axioms corresponding to the StringBuilder.insert(D) java function
#define UNREACHABLE
This should be used to mark dead code.
bool is_ssa_expr(const exprt &expr)
const exprt & length() const
#define string_refinement_invariantt(reason)
std::pair< exprt, string_constraintst > add_axioms_for_index_of(symbol_generatort &fresh_symbol, const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the first occurrence...
Universally quantified string constraint
std::pair< exprt, string_constraintst > add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
Length of a string.
Expression to hold a symbol (variable)
const char * c_str() const
std::pair< exprt, string_constraintst > add_axioms_for_insert_char(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the StringBuilder.insert(C) java function.
std::pair< exprt, string_constraintst > add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
const typet & subtype() const
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
const irep_idt & get_value() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
std::unordered_map< array_string_exprt, symbol_exprt, irep_hash > length_of_array
Struct constructor from list of elements.
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms to write the float in scientific notation.
const array_string_exprt & find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
std::pair< exprt, string_constraintst > add_axioms_for_hash_code(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Value that is identical for strings with the same content.
std::pair< exprt, string_constraintst > add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Replace a character by another in a string.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
std::pair< exprt, string_constraintst > add_axioms_for_insert_bool(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
add axioms corresponding to the StringBuilder.insert(Z) java function
bitvector_typet char_type()
exprt maximum(const exprt &a, const exprt &b)
std::pair< exprt, string_constraintst > add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
std::pair< exprt, string_constraintst > add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
array_string_exprt & to_array_string_expr(exprt &expr)
symbol_generatort & fresh_symbol
symbol_generatort fresh_symbol