cprover
|
Generates string constraints to link results from string functions with their arguments. More...
#include <limits>
#include <util/string_expr.h>
#include <util/replace_expr.h>
#include <util/refined_string_type.h>
#include <util/constexpr.def>
#include <util/deprecate.h>
#include <solvers/refinement/string_constraint.h>
Go to the source code of this file.
Classes | |
class | symbol_generatort |
Generation of fresh symbols of a given type. More... | |
class | array_poolt |
Correspondance between arrays and pointers string representations. More... | |
struct | string_constraintst |
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation). More... | |
class | string_constraint_generatort |
Functions | |
array_string_exprt | of_argument (array_poolt &array_pool, const exprt &arg) |
Converts a struct containing a length and pointer to an array. More... | |
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. More... | |
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 symbol. More... | |
void | merge (string_constraintst &result, string_constraintst other) |
Merge two sets of constraints by appending to the first one. More... | |
signedbv_typet | get_return_code_type () |
std::pair< exprt, string_constraintst > | add_axioms_for_concat (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) |
Add axioms enforcing that res is equal to the concatenation of s1 and s2 . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_concat_substr (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index) |
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘start_index’and ending at index end_index'`. More... | |
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 . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_string_of_int_with_radix (const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size, const namespacet &ns) |
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String.valueOf(JI) Java functions applied on the integer expression. More... | |
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. More... | |
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. More... | |
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. More... | |
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 More... | |
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 More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
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 to 0 and the first string is a prefix of the second one, starting at position offset. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_is_prefix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool) |
Test if the target is a prefix of the string. More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_length (const function_application_exprt &f, array_poolt &array_pool) |
Length of a string. More... | |
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. More... | |
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 application More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_constant (const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt()) |
Add axioms ensuring that the provided string expression and constant are equal. More... | |
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 positions start (included) and end (not included). More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_delete (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Remove a portion of a string. More... | |
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 More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_format (symbol_generatort &fresh_symbol, const array_string_exprt &res, const std::string &s, const exprt::operandst &args, array_poolt &array_pool, const messaget &message, const namespacet &ns) |
Parse s and add axioms ensuring the output corresponds to the output of String.format. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_insert (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool) |
Insertion of a string in another at a specific index. More... | |
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 More... | |
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 More... | |
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. More... | |
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. More... | |
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 More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_cprover_string (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &arg, const exprt &guard) |
Convert an expression of type string_typet to a string_exprt. More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_string_of_int (const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns) |
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression. More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_int_hex (const function_application_exprt &f, array_poolt &array_pool) |
Add axioms corresponding to the Integer.toHexString(I) java function. More... | |
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. More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_bool (const array_string_exprt &res, const exprt &i) |
Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_char (const function_application_exprt &f, array_poolt &array_pool) |
Conversion from char to string. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_char (const array_string_exprt &res, const exprt &i) |
Add axiom stating that string res has length 1 and the character it contains equals c . More... | |
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 of needle (c ) starting the search at from_index , or is -1 if no such character occurs at or after position from_index . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_index_of_string (symbol_generatort &fresh_symbol, const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index) |
Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index , or -1 if needle does not occur at or after position from_index . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Index of the first occurence of a target inside the string. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_last_index_of_string (symbol_generatort &fresh_symbol, const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index) |
Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. More... | |
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 of needle (c ) starting the search backward at from_index , or -1 if no such character occurs at or before position from_index . More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_last_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Index of the last occurence of a target inside the string. More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_string_of_float (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns) |
Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_fractional_part (const array_string_exprt &res, const exprt &i, size_t max_size) |
Add axioms for representing the fractional part of a floating point starting with a dot. More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_float_scientific_notation (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) |
Representation of a float value in scientific notation. More... | |
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. More... | |
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. More... | |
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. More... | |
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(start, 0)and end' = max(min(end, |str|), start')`. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_substring (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) |
Substring of a string between two indices. More... | |
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. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_code_point (const array_string_exprt &res, const exprt &code_point) |
add axioms for the conversion of an integer representing a java code point to a utf-16 string More... | |
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 More... | |
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. More... | |
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. More... | |
string_constraintst | add_axioms_for_characters_in_integer_string (const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul) |
Add axioms connecting the characters in the input string to the value of the output integer. More... | |
string_constraintst | add_axioms_for_correct_number_format (const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting) |
Add axioms making the return value true if the given string is a correct number in the given radix. More... | |
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. More... | |
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. More... | |
exprt | is_digit_with_radix (const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul) |
Check if a character is a digit with respect to the given radix, e.g. More... | |
exprt | get_numeric_value_from_character (const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, unsigned long radix_ul) |
Get the numeric value of a character, assuming that the radix is large enough. More... | |
size_t | max_printed_string_length (const typet &type, unsigned long ul_radix) |
Calculate the string length needed to represent any value of the given type using the given radix. More... | |
std::string | utf16_constant_array_to_java (const array_exprt &arr, std::size_t length) |
Construct a string from a constant array. More... | |
exprt | is_positive (const exprt &x) |
exprt | minimum (const exprt &a, const exprt &b) |
exprt | maximum (const exprt &a, const exprt &b) |
exprt | sum_overflows (const plus_exprt &sum) |
exprt | length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with. More... | |
exprt | length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 More... | |
exprt | length_constraint_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index) |
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at index end'`. More... | |
exprt | length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2) |
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2 . More... | |
exprt | zero_if_negative (const exprt &expr) |
Returns a non-negative version of the argument. More... | |
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 the constraints. More... | |
Generates string constraints to link results from string functions with their arguments.
This is inspired by the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh, which gives examples of constraints for several functions.
Definition in file string_constraint_generator.h.
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.
Add axioms stating that the character of the string at position given by second argument is equal to the returned value. This axiom is \( char = str[i] \).
fresh_symbol | generator of fresh symbols |
f | function application with arguments string str and integer i |
array_pool | pool of arrays representing strings |
char
Definition at line 566 of file string_constraint_generator_main.cpp.
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
f | function application with one character argument |
Definition at line 532 of file string_constraint_generator_main.cpp.
string_constraintst add_axioms_for_characters_in_integer_string | ( | const exprt & | input_int, |
const typet & | type, | ||
const bool | strict_formatting, | ||
const array_string_exprt & | str, | ||
const std::size_t | max_string_length, | ||
const exprt & | radix, | ||
const unsigned long | radix_ul | ||
) |
Add axioms connecting the characters in the input string to the value of the output integer.
It is constructive because it gives a formula for input_int in terms of the characters in str.
input_int | the integer represented by str |
type | the type for input_int |
strict_formatting | if true, don't allow a leading plus, redundant zeros or upper case letters |
str | input string |
max_string_length | the maximum length str can have |
radix | the radix, with the same type as input_int |
radix_ul | the radix as an unsigned long, or 0 if that can't be determined |
Deal with size==1 case separately. There are axioms from add_axioms_for_correct_number_format which say that the string must contain at least one digit, so we don't have to worry about "+" or "-".
Definition at line 415 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point | ( | const array_string_exprt & | res, |
const exprt & | code_point | ||
) |
add axioms for the conversion of an integer representing a java code point to a utf-16 string
res | array of characters corresponding to the result fo the function |
code_point | an expression representing a java code point |
Definition at line 20 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point_at | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms corresponding to the String.codePointAt java function
fresh_symbol | generator of fresh symbols |
f | function application with arguments a string and an index |
array_pool | pool of arrays representing strings |
Definition at line 122 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point_before | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms corresponding to the String.codePointBefore java function
Definition at line 155 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_code_point_count | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Add axioms corresponding the String.codePointCount java function.
Add axioms corresponding the String.codePointCount java function.
fresh_symbol | generator of fresh symbols |
f | function application with three arguments string str , integer begin and integer end . |
array_pool | pool of arrays representing strings |
Definition at line 193 of file string_constraint_generator_code_points.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_compare_to | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | pool | ||
) |
Lexicographic comparison of two strings.
Add axioms ensuring the result corresponds to that of the String.compareTo
Java function. In the lexicographic comparison, x
representing the first point where the two strings differ, we add axioms:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s1 and refined_string s2 |
pool | pool of arrays representing strings |
res
Definition at line 241 of file string_constraint_generator_comparison.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_concat | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2 | ||
) |
Add axioms enforcing that res
is equal to the concatenation of s1
and s2
.
fresh_symbol | generator of fresh symbols |
res | string_expression corresponding to the result |
s1 | the string expression to append to |
s2 | the string expression to append to the first one |
Definition at line 126 of file string_constraint_generator_concat.cpp.
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.
fresh_symbol | generator of fresh symbols |
f | function application with two arguments: a string and a code point |
array_pool | pool of arrays representing strings |
Definition at line 143 of file string_constraint_generator_concat.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_concat_substr | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2, | ||
const exprt & | start_index, | ||
const exprt & | end_index | ||
) |
Add axioms enforcing that res
is the concatenation of s1
with the substring of s2
starting at index ‘start_index’and ending at index
end_index'`.
Where start_index' is max(0, start_index) and end_index' is max(min(end_index, s2.length), start_index') If s1.length + end_index' - start_index' is greater than the maximal integer of the type of res.length, then the result gets truncated to the size of this maximal integer.
These axioms are:
fresh_symbol | generator of fresh symbols |
res | an array of characters expression |
s1 | an array of characters expression |
s2 | an array of characters expression |
start_index | integer expression |
end_index | integer expression |
0
Definition at line 38 of file string_constraint_generator_concat.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_constant | ( | const array_string_exprt & | res, |
irep_idt | sval, | ||
const exprt & | guard | ||
) |
Add axioms ensuring that the provided string expression and constant are equal.
res | array of characters for the result |
sval | a string constant |
guard | condition under which the axiom should apply, true by default |
Definition at line 24 of file string_constraint_generator_constants.cpp.
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.
The axiom is: \(\forall i \in [start, end).\ s[i] \in char_set \), where char_set
is given by the string char_set_string
composed of three characters low_char
, -
and high_char
. Character c
belongs to char_set
if \(low_char \le c \le high_char\).
fresh_symbol | generator of fresh symbols |
f | a function application with arguments: integer |s| , character pointer &s[0] , string char_set_string , optional integers start and end |
array_pool | pool of arrays representing strings |
Definition at line 290 of file string_constraint_generator_main.cpp.
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.
Add axioms ensuring the returned value is true when the first string contains the second. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s0 refined_string s1 |
array_pool | pool of arrays representing strings |
contains
Definition at line 233 of file string_constraint_generator_testing.cpp.
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 application
fresh_symbol | generator of fresh symbols |
f | function application with one argument, which is a string, or three arguments: string, integer offset and count |
array_pool | pool of arrays representing strings |
Definition at line 490 of file string_constraint_generator_main.cpp.
string_constraintst add_axioms_for_correct_number_format | ( | const array_string_exprt & | str, |
const exprt & | radix_as_char, | ||
const unsigned long | radix_ul, | ||
const std::size_t | max_size, | ||
const bool | strict_formatting | ||
) |
Add axioms making the return value true if the given string is a correct number in the given radix.
str | string expression |
radix_as_char | the radix as an expression of the same type as the characters in str |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
max_size | maximum number of characters |
strict_formatting | if true, don't allow a leading plus, redundant zeros or upper case letters |
index < length => is_digit_with_radix(str[index], radix)
Definition at line 329 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_cprover_string | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const exprt & | arg, | ||
const exprt & | guard | ||
) |
Convert an expression of type string_typet to a string_exprt.
fresh_symbol | generator of fresh symbols |
res | string expression for the result |
arg | expression of type string typet |
guard | condition under which res should be equal to arg |
Definition at line 82 of file string_constraint_generator_constants.cpp.
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 positions start
(included) and end
(not included).
These axioms are the same as would be generated for: concat(substring(str, 0, start), substring(end, |str|))
(see add_axioms_for_substring and add_axioms_for_concat_substr).
fresh_symbol | generator of fresh symbols |
res | array of characters expression |
str | array of characters expression |
start | integer expression |
end | integer expression |
array_pool | pool of arrays representing strings |
Definition at line 374 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_delete | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Remove a portion of a string.
Add axioms stating that res
corresponds to the input str
where we removed characters between the positions start
(included) and end
(not included). (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , integer start and integer end |
array_pool | pool of arrays representing strings |
Definition at line 412 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
add axioms corresponding to the StringBuilder.deleteCharAt java function
fresh_symbol | generator of fresh symbols |
f | function application with two arguments, the first is a string and the second is an index |
array_pool | pool of arrays representing strings |
Definition at line 339 of file string_constraint_generator_transformation.cpp.
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.
f | function application with arguments integer length and character pointer ptr . |
Definition at line 63 of file string_constraint_generator_constants.cpp.
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.
Add axioms stating that the result is true exactly when the strings represented by the arguments are equal. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s1 and refined_string s2 |
pool | pool of arrays representing strings |
eq
Definition at line 31 of file string_constraint_generator_comparison.cpp.
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.
Add axioms ensuring the result is true when the two strings are equal if case is ignored. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string s1 and refined_string s2 |
pool | pool of arrays representing strings |
eq
Definition at line 132 of file string_constraint_generator_comparison.cpp.
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.
Add axioms to specify the Java String.format function.
fresh_symbol | generator of fresh symbols |
f | a function application |
array_pool | pool of arrays representing strings |
message | message handler for warnings |
ns | namespace |
Definition at line 510 of file string_constraint_generator_format.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_format | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const std::string & | s, | ||
const exprt::operandst & | args, | ||
array_poolt & | array_pool, | ||
const messaget & | message, | ||
const namespacet & | ns | ||
) |
Parse s
and add axioms ensuring the output corresponds to the output of String.format.
fresh_symbol | generator of fresh symbols |
res | string expression for the result of the format function |
s | a format string |
args | a vector of arguments |
array_pool | pool of arrays representing strings |
message | message handler for warnings |
ns | namespace |
Definition at line 381 of file string_constraint_generator_format.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_fractional_part | ( | const array_string_exprt & | res, |
const exprt & | int_expr, | ||
size_t | max_size | ||
) |
Add axioms for representing the fractional part of a floating point starting with a dot.
res | string expression for the result |
int_expr | an integer expression |
max_size | a maximal size for the string, this includes the potential minus sign and therefore should be greater than 2 |
Definition at line 255 of file string_constraint_generator_float.cpp.
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 of needle
(c
) starting the search at from_index
, or is -1
if no such character occurs at or after position from_index
.
These axioms are:
fresh_symbol | generator of fresh symbols |
str | an array of characters expression |
c | a character expression |
from_index | an integer expression |
index
Definition at line 38 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_index_of | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Index of the first occurence of a target inside the string.
If the target is a character: Add axioms stating that the returned value is the index within haystack
(str
) of the first occurrence of needle
(c
) starting the search at from_index
, or is -1
if no such character occurs at or after position from_index
. (More...)
If the target is a refined_string: Add axioms stating that the returned value index
is the index within haystack
of the first occurrence of needle
starting the search at from_index
, or -1
if needle does not occur at or after position from_index
. (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string haystack , refined_string or character needle , and optional integer from_index with default value 0 |
array_pool | pool of arrays representing strings |
Definition at line 291 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_index_of_string | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | haystack, | ||
const array_string_exprt & | needle, | ||
const exprt & | from_index | ||
) |
Add axioms stating that the returned value index
is the index within haystack
of the first occurrence of needle
starting the search at from_index
, or -1
if needle does not occur at or after position from_index
.
If needle is an empty string then the result is from_index
.
These axioms are:
fresh_symbol | generator of fresh symbols |
haystack | an array of character expression |
needle | an array of character expression |
from_index | an integer expression |
index
representing the first index of needle
in haystack
Definition at line 111 of file string_constraint_generator_indexof.cpp.
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
.
We write offset' for max(0, min(res.length, offset))
. These axioms are:
fresh_symbol | generator of fresh symbols |
res | array of characters expression |
s1 | array of characters expression |
s2 | array of characters expression |
offset | integer expression |
Definition at line 33 of file string_constraint_generator_insert.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_insert | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | pool | ||
) |
Insertion of a string in another at a specific index.
Add axioms ensuring the result res
corresponds to s1
where we inserted s2
at position offset
. (More...)
If start
and end
arguments are given then substring(s2, start, end)
is considered instead of s2
.
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string s1 , refined_strings2 , integer offset , optional integer start and optional integer end |
pool | pool of arrays representing strings |
Definition at line 106 of file string_constraint_generator_insert.cpp.
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
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a Boolean |
array_pool | pool of arrays representing strings |
Definition at line 171 of file string_constraint_generator_insert.cpp.
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.
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a character |
array_pool | pool of arrays representing strings |
Definition at line 196 of file string_constraint_generator_insert.cpp.
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
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a double |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 223 of file string_constraint_generator_insert.cpp.
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.
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and a float |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 252 of file string_constraint_generator_insert.cpp.
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
fresh_symbol | generator of fresh symbols |
f | function application with three arguments: a string, an integer offset, and an integer |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 144 of file string_constraint_generator_insert.cpp.
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.
string_length(s)==0
instead fresh_symbol | generator of fresh symbols |
f | function application with a string argument |
array_pool | pool of arrays representing strings |
Definition at line 126 of file string_constraint_generator_testing.cpp.
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 to 0 and the first string is a prefix of the second one, starting at position offset.
These axioms are:
where offset_within_bounds is: offset >= 0 && offset <= |str| && |str| - offset >= |prefix|
fresh_symbol | generator of fresh symbols |
prefix | an array of characters |
str | an array of characters |
offset | an integer |
isprefix
Definition at line 37 of file string_constraint_generator_testing.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_is_prefix | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
bool | swap_arguments, | ||
array_poolt & | array_pool | ||
) |
Test if the target is a prefix of the string.
Add axioms ensuring the return value is true when the string starts with the given target. These axioms are detailed here: string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
fresh_symbol | generator of fresh symbols |
f | a function application with arguments refined_string s0 , refined string s1 and optional integer argument offset whose default value is 0 |
swap_arguments | a Boolean telling whether the prefix is the second argument or the first argument |
array_pool | pool of arrays representing strings |
isprefix
Definition at line 99 of file string_constraint_generator_testing.cpp.
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.
Add axioms ensuring the return value is true when the first string ends with the given target. These axioms are:
fresh_symbol | generator of fresh symbols |
f | a function application with arguments refined_string s0 and refined_string s1 |
swap_arguments | boolean flag telling whether the suffix is the second argument or the first argument |
array_pool | pool of arrays representing strings |
issuffix
Definition at line 168 of file string_constraint_generator_testing.cpp.
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 of needle
(c
) starting the search backward at from_index
, or -1
if no such character occurs at or before position from_index
.
These axioms are :
fresh_symbol | generator of fresh symbols |
str | an array of characters expression |
c | a character expression |
from_index | an integer expression |
index
representing the last index of needle
in haystack
before or at from_index
, or -1
if there is none Definition at line 346 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_last_index_of | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Index of the last occurence of a target inside the string.
If the target is a character: Add axioms stating that the returned value is the index within haystack
(str
) of the last occurrence of needle
(c
) starting the search backward at from_index
, or -1
if no such character occurs at or before position from_index
. (More...)
If the target is a refined_string: Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments refined_string haystack , refined_string or character needle , and optional integer from_index with default value |haystack|-1 |
array_pool | pool of arrays representing strings |
Definition at line 415 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | haystack, | ||
const array_string_exprt & | needle, | ||
const exprt & | from_index | ||
) |
Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index.
If needle
is the empty string, the result is from_index
.
These axioms are:
fresh_symbol | generator of fresh symbols |
haystack | an array of characters expression |
needle | an array of characters expression |
from_index | integer expression |
index
representing the last index of needle
in haystack
before or at from_index
, or -1 if there is none Definition at line 205 of file string_constraint_generator_indexof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_length | ( | const function_application_exprt & | f, |
array_poolt & | array_pool | ||
) |
Length of a string.
Returns the length of the string argument of the given function application
f | function application with argument string str |
array_pool | pool of arrays representing strings |
|str|
Definition at line 513 of file string_constraint_generator_main.cpp.
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.
Add axioms corresponding the String.offsetByCodePointCount java function.
We approximate the result by saying the result is between index + offset and index + 2 * offset
fresh_symbol | generator of fresh symbols |
f | function application with arguments string str , integer index and integer offset . |
Definition at line 222 of file string_constraint_generator_code_points.cpp.
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.
Add axioms ensuring the value of the returned integer corresponds to the value represented by str
fresh_symbol | generator of fresh symbols |
f | a function application with arguments refined_string str and an optional integer for the radix |
array_pool | pool of arrays representing strings |
ns | namespace |
str
Definition at line 507 of file string_constraint_generator_valueof.cpp.
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.
Add axioms ensuring that res
corresponds to str
where occurences of old_char
have been replaced by new_char
. These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , character old_char and character new_char |
array_pool | pool of arrays representing strings |
Definition at line 297 of file string_constraint_generator_transformation.cpp.
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.
Add axioms ensuring the returned string expression res
has length k
and characters at position i
in res
are equal to the character at position i
in s1
if i
is smaller that the length of s1
, otherwise it is the null character \u0000
.
These axioms are:
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string s1 , integer k |
array_pool | pool of arrays representing strings |
0
Definition at line 37 of file string_constraint_generator_transformation.cpp.
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.
We currently only specify that the string for NaN is "NaN", for infinity and minus infinity the string are "Infinity" and "-Infinity respectively otherwise the string contains only characters in [0123456789.] and '-' at the start for negative number
Add axioms corresponding to the String.valueOf(F) java function
fresh_symbol | generator of fresh symbols |
f | function application with one float argument |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 158 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_string_of_float | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '.
', followed by one or more decimal digits representing the fractional part of m. This specification is correct for inputs that do not exceed 100000 and the function is unspecified for other values.
fresh_symbol | generator of fresh symbols |
res | string expression corresponding to the result |
f | a float expression, which is positive |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 201 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_string_of_int | ( | const array_string_exprt & | res, |
const exprt & | input_int, | ||
size_t | max_size, | ||
const namespacet & | ns | ||
) |
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression.
res | string expression for the result |
input_int | a signed integer expression |
max_size | a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type") |
ns | namespace |
Definition at line 132 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix | ( | const array_string_exprt & | res, |
const exprt & | input_int, | ||
const exprt & | radix, | ||
size_t | max_size, | ||
const namespacet & | ns | ||
) |
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String.valueOf(JI) Java functions applied on the integer expression.
res | string expression for the result |
input_int | a signed integer expression |
radix | the radix to use |
max_size | a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type") |
ns | namespace |
Most of the time we can evaluate radix as an integer. The value 0 is used to indicate when we can't tell what the radix is.
Definition at line 153 of file string_constraint_generator_valueof.cpp.
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(start, 0)and
end' = max(min(end, |str|), start')`.
An actual java program should throw an exception in that case.
These axioms are:
fresh_symbol | generator of fresh symbols |
res | array of characters expression |
str | array of characters expression |
start | integer expression |
end | integer expression |
Definition at line 124 of file string_constraint_generator_transformation.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_substring | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool | ||
) |
Substring of a string between two indices.
Add axioms ensuring that res
corresponds to the substring of str
between indexes ‘start’ = max(start, 0)and
end' = max(min(end, |str|), start')`. (More...)
fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , integer start , optional integer end with default value |str| . |
array_pool | pool of arrays representing strings |
Definition at line 94 of file string_constraint_generator_transformation.cpp.
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.
Add axioms ensuring res
corresponds to str
from which leading and trailing whitespaces have been removed. Are considered whitespaces, characters whose ascii code are smaller than that of ' ' (space).
These axioms are:
idx
represents the index of the first non-space character.fresh_symbol | generator of fresh symbols |
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str . |
array_pool | pool of arrays representing strings |
Definition at line 183 of file string_constraint_generator_transformation.cpp.
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.
f | function application with a Boolean argument |
array_pool | pool of arrays representing strings |
Definition at line 66 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_bool | ( | const array_string_exprt & | res, |
const exprt & | b | ||
) |
Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false.
res | string expression for the result |
b | Boolean expression |
Definition at line 83 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_char | ( | const function_application_exprt & | f, |
array_poolt & | array_pool | ||
) |
Conversion from char to string.
Add axiom stating that string res
has length 1 and the character it contains equals c
. (More...)
f | function application with arguments integer |res| , character pointer &res[0] and character c |
array_pool | pool of arrays representing strings |
Definition at line 294 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_char | ( | const array_string_exprt & | res, |
const exprt & | c | ||
) |
Add axiom stating that string res
has length 1 and the character it contains equals c
.
This axiom is: \( |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \).
res | array of characters expression |
c | character expression |
Definition at line 311 of file string_constraint_generator_valueof.cpp.
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.
fresh_symbol | generator of fresh symbols |
f | function application with one double argument |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 177 of file string_constraint_generator_float.cpp.
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.
A float is represented as \(f = m * 2^e\) where \(0 <= m < 2\) is the significand and \(-126 <= e <= 127\) is the exponent. We want an alternate representation by finding \(n\) and \(d\) such that \(f=n*10^d\). We can estimate \(d\) the following way: \(d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)\) \(d = floor(log_10(2) * e)\) Then \(n\) can be expressed by the equation: \(log_10(n) = log_10(m) + log_10(2) * e - d\) \(n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\)
fresh_symbol | generator of fresh symbols |
res | string expression representing the float in scientific notation |
f | a float expression, which is positive |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 344 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Representation of a float value in scientific notation.
Add axioms corresponding to the scientific representation of floating point values
fresh_symbol | generator of fresh symbols |
f | a function application expression |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 540 of file string_constraint_generator_float.cpp.
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.
res | string expression for the result |
i | an integer argument |
Definition at line 216 of file string_constraint_generator_valueof.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_int_hex | ( | const function_application_exprt & | f, |
array_poolt & | array_pool | ||
) |
Add axioms corresponding to the Integer.toHexString(I) java function.
f | function application with an integer argument |
array_pool | pool of arrays representing strings |
Definition at line 273 of file string_constraint_generator_valueof.cpp.
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.
Add axioms ensuring that the returned string expression is equal to the string literal.
fresh_symbol | generator of fresh symbols |
f | function application with an argument which is a string literal that is a constant with a string value. |
array_pool | pool of arrays representing strings |
Definition at line 114 of file string_constraint_generator_constants.cpp.
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.
f | function application with one long argument |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 45 of file string_constraint_generator_valueof.cpp.
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.
This constraint is \( \forall i \in [start, end), low\_char \le s[i] \le high\_char \)
fresh_symbol | generator of fresh symbols |
s | a string expression |
start | index of the first character to constrain |
end | index at which we stop adding constraints |
char_set | a string of the form "<low_char>-<high_char>" where <low_char> and <high_char> are two characters, which represents the set of characters that are between low_char and high_char . |
Definition at line 254 of file string_constraint_generator_main.cpp.
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.
Definition at line 325 of file string_constraint_generator_main.cpp.
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 the constraints.
Definition at line 598 of file string_constraint_generator_main.cpp.
exprt get_numeric_value_from_character | ( | const exprt & | chr, |
const typet & | char_type, | ||
const typet & | type, | ||
const bool | strict_formatting, | ||
const unsigned long | radix_ul | ||
) |
Get the numeric value of a character, assuming that the radix is large enough.
'+' and '-' yield 0.
chr | the character to get the numeric value of |
char_type | the type to use for characters |
type | the type to use for the return value |
strict_formatting | if true, don't allow upper case characters |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
There are four cases, which occur in ASCII in the following order: '+' and '-', digits, upper case letters, lower case letters
return char >= '0' ? (char - '0') : 0
return char >= 'a' ? (char - 'a' + 10) : char >= '0' ? (char - '0') : 0
return char >= 'a' ? (char - 'a' + 10) : char >= 'A' ? (char - 'A' + 10) : char >= '0' ? (char - '0') : 0
Definition at line 630 of file string_constraint_generator_valueof.cpp.
signedbv_typet get_return_code_type | ( | ) |
Definition at line 339 of file string_constraint_generator_main.cpp.
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 symbol.
pool | pool of arrays representing strings |
expr | an expression of refined string type |
Definition at line 210 of file string_constraint_generator_main.cpp.
exprt is_digit_with_radix | ( | const exprt & | chr, |
const bool | strict_formatting, | ||
const exprt & | radix_as_char, | ||
const unsigned long | radix_ul | ||
) |
Check if a character is a digit with respect to the given radix, e.g.
if the radix is 10 then check if the character is in the range 0-9.
chr | the character |
strict_formatting | if true, don't allow upper case characters |
radix_as_char | the radix as an expression of the same type as chr |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
Definition at line 560 of file string_constraint_generator_valueof.cpp.
x | an expression |
x
is positive Definition at line 524 of file string_constraint_generator_main.cpp.
exprt length_constraint_for_concat | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2 | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with s2
Definition at line 99 of file string_constraint_generator_concat.cpp.
exprt length_constraint_for_concat_char | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1 | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with.
Definition at line 109 of file string_constraint_generator_concat.cpp.
exprt length_constraint_for_concat_substr | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2, | ||
const exprt & | start, | ||
const exprt & | end | ||
) |
Add axioms enforcing that the length of res
is that of the concatenation of s1
with the substring of s2
starting at index ‘start’ and ending at index
end'`.
Where start_index' is max(0, start) and end' is max(min(end, s2.length), start')
Definition at line 81 of file string_constraint_generator_concat.cpp.
exprt length_constraint_for_insert | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const array_string_exprt & | s2 | ||
) |
Add axioms ensuring the length of res
corresponds to that of s1
where we inserted s2
.
Definition at line 80 of file string_constraint_generator_insert.cpp.
size_t max_printed_string_length | ( | const typet & | type, |
unsigned long | radix_ul | ||
) |
Calculate the string length needed to represent any value of the given type using the given radix.
Due to floating point rounding errors we sometimes return a value 1 larger than needed, which is fine for our purposes.
type | the type that we are considering values of |
radix_ul | the radix we are using, or 0, in which case the return value will work for any radix |
We want to calculate max, the maximum number of characters needed to represent any value of the given type.
For signed types, the longest string will be for -2^(n_bits-1), so max = 1 + min{k: 2^(n_bits-1) < radix^k} (the 1 is for the minus sign) = 1 + min{k: n_bits-1 < k log_2(radix)} = 1 + min{k: k > (n_bits-1) / log_2(radix)} = 1 + min{k: k > floor((n_bits-1) / log_2(radix))} = 1 + (1 + floor((n_bits-1) / log_2(radix))) = 2 + floor((n_bits-1) / log_2(radix))
For unsigned types, the longest string will be for (2^n_bits)-1, so max = min{k: (2^n_bits)-1 < radix^k} = min{k: 2^n_bits <= radix^k} = min{k: n_bits <= k log_2(radix)} = min{k: k >= n_bits / log_2(radix)} = min{k: k >= ceil(n_bits / log_2(radix))} = ceil(n_bits / log_2(radix))
Definition at line 704 of file string_constraint_generator_valueof.cpp.
Definition at line 583 of file string_constraint_generator_main.cpp.
void merge | ( | string_constraintst & | result, |
string_constraintst | other | ||
) |
Merge two sets of constraints by appending to the first one.
Definition at line 225 of file string_constraint_generator_main.cpp.
Definition at line 578 of file string_constraint_generator_main.cpp.
array_string_exprt of_argument | ( | array_poolt & | array_pool, |
const exprt & | arg | ||
) |
Converts a struct containing a length and pointer to an array.
This allows to get a string expression from arguments of a string builtion function, because string arguments in these function calls are given as a struct containing a length and pointer to an array.
Definition at line 333 of file string_constraint_generator_main.cpp.
exprt sum_overflows | ( | const plus_exprt & | sum | ) |
Definition at line 54 of file string_constraint_generator_main.cpp.
std::string utf16_constant_array_to_java | ( | const array_exprt & | arr, |
std::size_t | length | ||
) |
Construct a string from a constant array.
arr | an array expression containing only constants |
length | an unsigned value representing the length of the array |
length
represented by the array assuming each field in arr
represents a character. Definition at line 483 of file string_constraint_generator_format.cpp.
Returns a non-negative version of the argument.
expr | expression of which we want a non-negative version |
max(0, expr)
Definition at line 591 of file string_constraint_generator_main.cpp.