cprover
string_constraint_generator.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints to link results from string functions
4  with their arguments. This is inspired by the PASS paper at HVC'13:
5  "PASS: String Solving with Parameterized Array and Interval Automaton"
6  by Guodong Li and Indradeep Ghosh, which gives examples of constraints
7  for several functions.
8 
9 Author: Romain Brenguier, romain.brenguier@diffblue.com
10 
11 \*******************************************************************/
12 
19 
20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
22 
23 #include <limits>
25 #include <util/constexpr.def>
26 #include <util/deprecate.h>
27 #include <util/namespace.h>
29 #include <util/replace_expr.h>
30 #include <util/string_expr.h>
31 
32 #include "array_pool.h"
33 
35 
38 struct string_constraintst final
39 {
40  std::vector<exprt> existential;
41  std::vector<string_constraintt> universal;
42  std::vector<string_not_contains_constraintt> not_contains;
43 };
44 
45 void merge(string_constraintst &result, string_constraintst other);
46 
48 {
49 public:
50  // This module keeps a list of axioms. It has methods which generate
51  // string constraints for different string functions and add them
52  // to the axiom list.
53 
55 
56  std::pair<exprt, string_constraintst>
58 
60 
62 
63  const namespacet ns;
64 
69  const exprt &return_code,
70  const function_application_exprt &expr);
71 
72 private:
74  const exprt &return_code,
76 
78  const exprt &return_code,
80 
81 public:
82  std::pair<exprt, string_constraintst> add_axioms_for_concat(
83  const array_string_exprt &res,
84  const array_string_exprt &s1,
85  const array_string_exprt &s2);
86 
87  std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
88  const array_string_exprt &res,
89  const array_string_exprt &s1,
90  const array_string_exprt &s2,
91  const exprt &start_index,
92  const exprt &end_index);
93  std::pair<exprt, string_constraintst> add_axioms_for_insert(
94  const array_string_exprt &res,
95  const array_string_exprt &s1,
96  const array_string_exprt &s2,
97  const exprt &offset);
98  std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
99  const array_string_exprt &res,
100  const exprt &input_int,
101  const exprt &radix,
102  size_t max_size);
103 
105  const array_string_exprt &s,
106  const exprt &start,
107  const exprt &end,
108  const std::string &char_set);
109  std::pair<exprt, string_constraintst>
111 
112  // The following functions add axioms for the returned value
113  // to be equal to the result of the function given as argument.
114  // They are not accessed directly from other classes: they call
115  // `add_axioms_for_function_application` which determines which of
116  // these methods should be called.
117 
118  std::pair<exprt, string_constraintst>
120  std::pair<exprt, string_constraintst>
122 
123  std::pair<exprt, string_constraintst>
125  std::pair<exprt, string_constraintst>
127  std::pair<exprt, string_constraintst>
129  std::pair<exprt, string_constraintst>
131 
132  std::pair<exprt, string_constraintst>
134  std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
135  const array_string_exprt &prefix,
136  const array_string_exprt &str,
137  const exprt &offset);
138  std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
140  bool swap_arguments);
141 
142  std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
144  bool swap_arguments);
145  std::pair<exprt, string_constraintst>
147  std::pair<exprt, string_constraintst>
149 
150  std::pair<exprt, string_constraintst>
152 
153  std::pair<exprt, string_constraintst>
155  std::pair<exprt, string_constraintst> add_axioms_for_constant(
156  const array_string_exprt &res,
157  irep_idt sval,
158  const exprt &guard = true_exprt());
159 
160  std::pair<exprt, string_constraintst> add_axioms_for_delete(
161  const array_string_exprt &res,
162  const array_string_exprt &str,
163  const exprt &start,
164  const exprt &end);
165  std::pair<exprt, string_constraintst>
167  std::pair<exprt, string_constraintst>
169 
170  std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
171  const array_string_exprt &res,
172  const exprt &arg,
173  const exprt &guard);
174  std::pair<exprt, string_constraintst>
176 
177  std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
178  const array_string_exprt &res,
179  const exprt &input_int,
180  size_t max_size);
181  std::pair<exprt, string_constraintst>
182  add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i);
183  std::pair<exprt, string_constraintst>
185  std::pair<exprt, string_constraintst>
187  std::pair<exprt, string_constraintst>
189  std::pair<exprt, string_constraintst>
190  add_axioms_from_bool(const array_string_exprt &res, const exprt &b);
191  std::pair<exprt, string_constraintst>
193  std::pair<exprt, string_constraintst>
195  std::pair<exprt, string_constraintst> add_axioms_for_index_of(
196  const array_string_exprt &str,
197  const exprt &c,
198  const exprt &from_index);
199  std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
200  const array_string_exprt &haystack,
201  const array_string_exprt &needle,
202  const exprt &from_index);
203  std::pair<exprt, string_constraintst>
205  std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
206  const array_string_exprt &haystack,
207  const array_string_exprt &needle,
208  const exprt &from_index);
209  std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
210  const array_string_exprt &str,
211  const exprt &c,
212  const exprt &from_index);
213 
214  std::pair<exprt, string_constraintst>
216 
222  std::pair<exprt, string_constraintst>
224  std::pair<exprt, string_constraintst>
226  std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
227  const array_string_exprt &res,
228  const exprt &int_expr,
229  size_t max_size);
230  std::pair<exprt, string_constraintst>
232  const array_string_exprt &res,
233  const exprt &f);
234  std::pair<exprt, string_constraintst>
236  const function_application_exprt &f);
237 
240  std::pair<exprt, string_constraintst>
242 
243  std::pair<exprt, string_constraintst>
245  std::pair<exprt, string_constraintst>
247 
251  std::pair<exprt, string_constraintst> add_axioms_for_substring(
252  const array_string_exprt &res,
253  const array_string_exprt &str,
254  const exprt &start,
255  const exprt &end);
256  std::pair<exprt, string_constraintst>
258 
259  std::pair<exprt, string_constraintst>
261 
262  std::pair<exprt, string_constraintst> add_axioms_for_code_point(
263  const array_string_exprt &res,
264  const exprt &code_point);
265  std::pair<exprt, string_constraintst>
267 
272  DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
273  std::pair<exprt, string_constraintst>
275 
282  DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
283  std::pair<exprt, string_constraintst>
285 
287  const exprt &input_int,
288  const typet &type,
289  const bool strict_formatting,
290  const array_string_exprt &str,
291  const std::size_t max_string_length,
292  const exprt &radix,
293  const unsigned long radix_ul);
295  const array_string_exprt &str,
296  const exprt &radix_as_char,
297  const unsigned long radix_ul,
298  const std::size_t max_size,
299  const bool strict_formatting);
300  std::pair<exprt, string_constraintst>
302  std::pair<exprt, string_constraintst>
304  std::pair<exprt, string_constraintst>
306 
308  std::pair<exprt, string_constraintst> result1,
309  std::pair<exprt, string_constraintst> result2);
310 
314  {
320  unsigned long radix_ul;
322  // (or pessimistic assumption of base-2 if unknown) and result type. For
323  // example, the longest possible decimal int64 is 16 characters long in hex.
324  std::size_t max_string_length;
325  };
326 
329  const typet &target_int_type);
330 };
331 
333  const array_string_exprt &res,
334  const array_string_exprt &s1,
335  array_poolt &array_pool);
337  const array_string_exprt &res,
338  const array_string_exprt &s1,
339  const array_string_exprt &s2,
340  array_poolt &array_pool);
342  const array_string_exprt &res,
343  const array_string_exprt &s1,
344  const array_string_exprt &s2,
345  const exprt &start,
346  const exprt &end,
347  array_poolt &array_pool);
348 
349 size_t max_printed_string_length(const typet &type, unsigned long ul_radix);
350 
351 exprt is_positive(const exprt &x);
352 
354 exprt minimum(const exprt &a, const exprt &b);
355 
357 exprt maximum(const exprt &a, const exprt &b);
358 
360 exprt sum_overflows(const plus_exprt &sum);
361 
362 // Type used by primitives to signal errors
364 
365 exprt zero_if_negative(const exprt &expr);
366 
368  const exprt &chr,
369  const bool strict_formatting,
370  const exprt &radix_as_char,
371  const unsigned long radix_ul);
372 
374  const exprt &chr,
375  const typet &char_type,
376  const typet &type,
377  const bool strict_formatting,
378  unsigned long radix_ul);
379 
380 #endif
length_constraint_for_concat
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2
Definition: string_concatenation_builtin_function.cpp:123
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
sum_overflows
exprt sum_overflows(const plus_exprt &sum)
Definition: string_constraint_generator_main.cpp:38
string_constraint_generatort::add_axioms_from_literal
std::pair< exprt, string_constraintst > add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
Definition: string_constraint_generator_constants.cpp:111
string_constraint_generatort::add_axioms_for_code_point_count
std::pair< exprt, string_constraintst > add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
Definition: string_constraint_generator_code_points.cpp:191
string_constraint_generatort::add_axioms_for_index_of
std::pair< exprt, string_constraintst > add_axioms_for_index_of(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...
Definition: string_constraint_generator_indexof.cpp:41
string_constraint_generatort::add_axioms_for_substring
std::pair< exprt, string_constraintst > add_axioms_for_substring(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,...
Definition: string_constraint_generator_transformation.cpp:122
array_pool.h
Associates arrays and length to pointers, so that the string refinement can transform builtin functio...
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:394
string_constraint_generatort::add_axioms_from_long
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(J) java function.
Definition: string_constraint_generator_valueof.cpp:44
string_constraint_generatort::add_axioms_from_char
std::pair< exprt, string_constraintst > add_axioms_from_char(const array_string_exprt &res, const exprt &c)
typet
The type of an expression, extends irept.
Definition: type.h:28
array_poolt
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
length_constraint_for_concat_substr
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, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
Definition: string_concatenation_builtin_function.cpp:100
string_constraint_generatort::add_axioms_for_char_at
std::pair< exprt, string_constraintst > add_axioms_for_char_at(const function_application_exprt &f)
Character at a given position.
Definition: string_constraint_generator_main.cpp:383
length_constraint_for_concat_char
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
Definition: string_concatenation_builtin_function.cpp:138
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:59
string_constraint_generatort::add_axioms_for_delete
std::pair< exprt, string_constraintst > add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
Definition: string_constraint_generator_transformation.cpp:375
string_constraint_generatort::add_axioms_for_contains
std::pair< exprt, string_constraintst > add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
Definition: string_constraint_generator_testing.cpp:248
string_constraint_generatort::add_axioms_for_trim
std::pair< exprt, string_constraintst > add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
Definition: string_constraint_generator_transformation.cpp:180
string_constraint_generatort::add_axioms_from_char
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f)
s1
int8_t s1
Definition: bytecode_info.h:59
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
exprt
Base class for all expressions.
Definition: expr.h:54
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:39
string_constraint_generatort::string_constraint_generatort
string_constraint_generatort(const namespacet &ns)
Definition: string_constraint_generator_main.cpp:33
string_constraint_generatort::add_axioms_for_string_of_float
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
Definition: string_constraint_generator_float.cpp:162
string_constraint_generatort::add_axioms_for_equals
std::pair< exprt, string_constraintst > add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
Definition: string_constraint_generator_comparison.cpp:31
namespace.h
string_constraint_generatort::parseint_argumentst::radix_ul
unsigned long radix_ul
Radix as an unsigned long (or 0 if unknown)
Definition: string_constraint_generator.h:320
string_constraint_generatort::get_conjuncts_for_correct_number_format
std::vector< exprt > get_conjuncts_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.
Definition: string_constraint_generator_valueof.cpp:279
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:61
string_constraint_generatort
Definition: string_constraint_generator.h:48
string_constraint_generatort::add_axioms_for_last_index_of_string
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of_string(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 nee...
Definition: string_constraint_generator_indexof.cpp:213
merge
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Definition: string_constraint_generator_main.cpp:99
string_constraint_generatort::add_axioms_for_offset_by_code_point
std::pair< exprt, string_constraintst > add_axioms_for_offset_by_code_point(const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
Definition: string_constraint_generator_code_points.cpp:217
string_constraint_generatort::add_axioms_for_characters_in_integer_string
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.
Definition: string_constraint_generator_valueof.cpp:373
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
string_constraint_generatort::add_constraint_on_characters
string_constraintst add_constraint_on_characters(const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
Add constraint on characters of a string.
Definition: string_constraint_generator_main.cpp:127
string_constraint_generatort::add_axioms_for_concat_code_point
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
Definition: string_concatenation_builtin_function.cpp:173
symbol_generatort
Generation of fresh symbols of a given type.
Definition: array_pool.h:22
string_constraint_generatort::add_axioms_for_compare_to
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
Definition: string_constraint_generator_comparison.cpp:207
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:399
string_constraint_generatort::add_axioms_for_replace
std::pair< exprt, string_constraintst > add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
Definition: string_constraint_generator_transformation.cpp:306
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:63
deprecate.h
string_constraint_generatort::add_axioms_for_parse_int
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
Definition: string_constraint_generator_valueof.cpp:524
string_constraint_generatort::unpack_parseint_arguments
parseint_argumentst unpack_parseint_arguments(const function_application_exprt &f, const typet &target_int_type)
Definition: string_constraint_generator_valueof.cpp:458
string_constraint_generatort::add_axioms_for_is_empty
std::pair< exprt, string_constraintst > add_axioms_for_is_empty(const function_application_exprt &f)
Add axioms stating that the returned value is true exactly when the argument string is empty.
Definition: string_constraint_generator_testing.cpp:129
string_constraint_generatort::add_axioms_for_cprover_string
std::pair< exprt, string_constraintst > add_axioms_for_cprover_string(const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
Definition: string_constraint_generator_constants.cpp:83
string_constraint_generatort::associate_length_to_array
exprt associate_length_to_array(const exprt &return_code, const function_application_exprt &f)
Associate an integer length to a char array.
Definition: string_constraint_generator_main.cpp:85
string_constraint_generatort::add_axioms_for_is_valid_int
std::pair< exprt, string_constraintst > add_axioms_for_is_valid_int(const function_application_exprt &f)
Check a string is a valid integer, using the same rules as Java Integer.parseInt.
Definition: string_constraint_generator_valueof.cpp:489
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
string_constraint_generatort::add_axioms_for_is_suffix
std::pair< exprt, string_constraintst > add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments)
Test if the target is a suffix of the string.
Definition: string_constraint_generator_testing.cpp:170
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:192
string_constraint_generatort::add_axioms_for_delete_char_at
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
Definition: string_constraint_generator_transformation.cpp:348
string_constraint_generatort::add_axioms_from_double
std::pair< exprt, string_constraintst > add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
Definition: string_constraint_generator_float.cpp:174
string_constraint_generatort::add_axioms_for_function_application
std::pair< exprt, string_constraintst > add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
Definition: string_constraint_generator_main.cpp:210
string_constraint_generatort::parseint_argumentst::str
array_string_exprt str
String being parsed.
Definition: string_constraint_generator.h:316
string_constraint_generatort::add_axioms_for_set_length
std::pair< exprt, string_constraintst > add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
Definition: string_constraint_generator_transformation.cpp:39
string_constraint_generatort::make_array_pointer_association
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
Definition: string_constraint_generator_main.cpp:192
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:179
string_constraint_generatort::add_axioms_for_last_index_of
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(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 ...
Definition: string_constraint_generator_indexof.cpp:359
string_constraint_generatort::add_axioms_for_insert
std::pair< exprt, string_constraintst > add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
string_constraint_generatort::add_axioms_for_equals_ignore_case
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
Definition: string_constraint_generator_comparison.cpp:135
string_constraint_generatort::add_axioms_for_constrain_characters
std::pair< exprt, string_constraintst > add_axioms_for_constrain_characters(const function_application_exprt &f)
Add axioms to ensure all characters of a string belong to a given set.
Definition: string_constraint_generator_main.cpp:160
string_constraint_generatort::add_axioms_for_is_prefix
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(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...
Definition: string_constraint_generator_testing.cpp:38
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
string_constraint_generatort::add_axioms_for_fractional_part
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.
Definition: string_constraint_generator_float.cpp:245
string_constraint_generatort::add_axioms_for_constant
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.
Definition: string_constraint_generator_constants.cpp:24
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
string_constraint.h
Defines string constraints.
refined_string_type.h
Type for string expressions used by the string solver.
string_constraint_generatort::add_axioms_for_length
std::pair< exprt, string_constraintst > add_axioms_for_length(const function_application_exprt &f)
Length of a string.
Definition: string_constraint_generator_main.cpp:327
string_constraint_generatort::add_axioms_for_char_literal
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
Definition: string_constraint_generator_main.cpp:346
string_constraint_generatort::parseint_argumentst
Argument block for parseInt and cousins, common to parseInt itself and CProverString....
Definition: string_constraint_generator.h:314
string_constraint_generatort::parseint_argumentst::max_string_length
std::size_t max_string_length
Max string length (assuming no leading zeroes) considering the radix.
Definition: string_constraint_generator.h:324
is_digit_with_radix
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.
Definition: string_constraint_generator_valueof.cpp:554
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:407
is_positive
exprt is_positive(const exprt &x)
Definition: string_constraint_generator_main.cpp:337
string_constraint_generatort::add_axioms_for_concat_substr
std::pair< exprt, string_constraintst > add_axioms_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 res is the concatenation of s1 with the substring of s2 starting at index ‘...
Definition: string_concatenation_builtin_function.cpp:53
string_constraint_generatort::add_axioms_for_copy
std::pair< exprt, string_constraintst > add_axioms_for_copy(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the argument of the function applic...
Definition: string_constraint_generator_main.cpp:307
string_constraint_generatort::add_axioms_from_bool
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f)
string_constraint_generatort::add_axioms_from_int_hex
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.
Definition: string_constraint_generator_valueof.cpp:200
string_constraint_generatort::add_axioms_for_string_of_int
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
Definition: string_constraint_generator_valueof.cpp:117
string_constraint_generatort::combine_results
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 ...
Definition: string_constraint_generator_main.cpp:415
string_constraint_generatort::associate_array_to_pointer
exprt associate_array_to_pointer(const exprt &return_code, const function_application_exprt &f)
Associate a char array to a char pointer.
Definition: string_constraint_generator_main.cpp:61
string_constraint_generatort::add_axioms_from_float_scientific_notation
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
Definition: string_constraint_generator_float.cpp:338
string_constraint_generatort::add_axioms_for_concat
std::pair< exprt, string_constraintst > add_axioms_for_concat(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.
Definition: string_concatenation_builtin_function.cpp:158
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:42
string_constraint_generatort::add_axioms_for_code_point_at
std::pair< exprt, string_constraintst > add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
Definition: string_constraint_generator_code_points.cpp:124
string_constraint_generatort::parseint_argumentst::radix
exprt radix
Radix, as parseInt's result type.
Definition: string_constraint_generator.h:318
replace_expr.h
string_constraint_generatort::add_axioms_for_index_of_string
std::pair< exprt, string_constraintst > add_axioms_for_index_of_string(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...
Definition: string_constraint_generator_indexof.cpp:113
s2
int16_t s2
Definition: bytecode_info.h:60
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
string_constraint_generatort::add_axioms_for_code_point
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
Definition: string_constraint_generator_code_points.cpp:23
string_constraint_generatort::add_axioms_for_string_of_int_with_radix
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)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
Definition: string_constraint_generator_valueof.cpp:137
string_expr.h
String expressions for the string solver.
get_numeric_value_from_character
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.
Definition: string_constraint_generator_valueof.cpp:622
string_constraint_generatort::add_axioms_for_code_point_before
std::pair< exprt, string_constraintst > add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
Definition: string_constraint_generator_code_points.cpp:156
array_string_exprt
Definition: string_expr.h:67
max_printed_string_length
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.
Definition: string_constraint_generator_valueof.cpp:696
string_constraint_generatort::add_axioms_for_empty_string
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.
Definition: string_constraint_generator_constants.cpp:64
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:40
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:41