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>
24 #include <util/string_expr.h>
25 #include <util/replace_expr.h>
27 #include <util/constexpr.def>
28 #include <util/deprecate.h>
30 
32 class symbol_generatort final
33 {
34 public:
36  operator()(const irep_idt &prefix, const typet &type = bool_typet());
37 
38 private:
39  unsigned symbol_count = 0;
40 
41 #ifdef DEBUG
42 public:
44  std::vector<symbol_exprt> created_symbols;
45 #endif
46 };
47 
49 class array_poolt final
50 {
51 public:
52  explicit array_poolt(symbol_generatort &symbol_generator)
53  : fresh_symbol(symbol_generator)
54  {
55  }
56 
57  const std::unordered_map<exprt, array_string_exprt, irep_hash> &
59  {
60  return arrays_of_pointers;
61  }
62 
63  exprt get_length(const array_string_exprt &s) const;
64 
65  void insert(const exprt &pointer_expr, array_string_exprt &array);
66 
67  const array_string_exprt &find(const exprt &pointer, const exprt &length);
68 
69  const std::set<array_string_exprt> &created_strings() const;
70 
73 
74 private:
75  // associate arrays to char pointers
76  std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
77 
78  // associate length to arrays of infinite size
79  std::unordered_map<array_string_exprt, symbol_exprt, irep_hash>
81 
82  // generates fresh symbols
84 
85  // Strings created in the pool
86  std::set<array_string_exprt> created_strings_value;
87 
89  const exprt &char_pointer,
90  const typet &char_array_type);
91 };
92 
97 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg);
98 
100  array_poolt &pool,
101  const exprt &pointer,
102  const exprt &length);
103 
105 
109 {
110  std::vector<exprt> existential;
111  std::vector<string_constraintt> universal;
112  std::vector<string_not_contains_constraintt> not_contains;
113 
115  void clear();
116 };
117 
118 void merge(string_constraintst &result, string_constraintst other);
119 
121 {
122 public:
123  // This module keeps a list of axioms. It has methods which generate
124  // string constraints for different string functions and add them
125  // to the axiom list.
126 
127  explicit string_constraint_generatort(const namespacet &ns);
128 
129  std::pair<exprt, string_constraintst> add_axioms_for_function_application(
131  const function_application_exprt &expr);
132 
134 
136 
138 
139  const namespacet ns;
140 
146 
147 private:
152  std::pair<symbol_exprt, string_constraintst> add_axioms_for_intern(
154  const function_application_exprt &f);
155 
157 
159 
160  // Add axioms corresponding to the String.hashCode java function
161  // The specification is partial: the actual value is not actually computed
162  // but we ensure that hash codes of equal strings are equal.
163  std::pair<exprt, string_constraintst> add_axioms_for_hash_code(
166  array_poolt &pool);
167 
168  // MEMBERS
170 
171  // To each string on which hash_code was called we associate a symbol
172  // representing the return value of the hash_code function.
173  std::map<array_string_exprt, exprt> hash_code_of_string;
174 
175  // Pool used for the intern method
176  std::map<array_string_exprt, symbol_exprt> intern_of_string;
177 };
178 
179 // Type used by primitives to signal errors
181 
182 std::pair<exprt, string_constraintst> add_axioms_for_concat(
183  symbol_generatort &fresh_symbol,
184  const array_string_exprt &res,
185  const array_string_exprt &s1,
186  const array_string_exprt &s2);
187 std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
188  symbol_generatort &fresh_symbol,
189  const array_string_exprt &res,
190  const array_string_exprt &s1,
191  const array_string_exprt &s2,
192  const exprt &start_index,
193  const exprt &end_index);
194 std::pair<exprt, string_constraintst> add_axioms_for_insert(
195  symbol_generatort &fresh_symbol,
196  const array_string_exprt &res,
197  const array_string_exprt &s1,
198  const array_string_exprt &s2,
199  const exprt &offset);
200 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
201  const array_string_exprt &res,
202  const exprt &input_int,
203  const exprt &radix,
204  size_t max_size,
205  const namespacet &ns);
206 
208  symbol_generatort &fresh_symbol,
209  const array_string_exprt &s,
210  const exprt &start,
211  const exprt &end,
212  const std::string &char_set);
213 std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters(
214  symbol_generatort &fresh_symbol,
216  array_poolt &array_pool);
217 
218 // The following functions add axioms for the returned value
219 // to be equal to the result of the function given as argument.
220 // They are not accessed directly from other classes: they call
221 // `add_axioms_for_function_application` which determines which of
222 // these methods should be called.
223 
224 std::pair<exprt, string_constraintst> add_axioms_for_char_at(
225  symbol_generatort &fresh_symbol,
227  array_poolt &array_pool);
228 std::pair<exprt, string_constraintst> add_axioms_for_code_point_at(
229  symbol_generatort &fresh_symbol,
231  array_poolt &pool);
232 std::pair<exprt, string_constraintst> add_axioms_for_code_point_before(
233  symbol_generatort &fresh_symbol,
235  array_poolt &pool);
236 std::pair<exprt, string_constraintst> add_axioms_for_contains(
237  symbol_generatort &fresh_symbol,
239  array_poolt &array_pool);
240 std::pair<exprt, string_constraintst> add_axioms_for_equals(
241  symbol_generatort &fresh_symbol,
243  array_poolt &pool);
244 std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
245  symbol_generatort &fresh_symbol,
247  array_poolt &pool);
248 
249 std::pair<exprt, string_constraintst> add_axioms_for_is_empty(
250  symbol_generatort &fresh_symbol,
252  array_poolt &array_pool);
253 std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
254  symbol_generatort &fresh_symbol,
255  const array_string_exprt &prefix,
256  const array_string_exprt &str,
257  const exprt &offset);
258 std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
259  symbol_generatort &fresh_symbol,
261  bool swap_arguments,
262  array_poolt &array_pool);
263 std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
264  symbol_generatort &fresh_symbol,
266  bool swap_arguments,
267  array_poolt &array_pool);
268 std::pair<exprt, string_constraintst> add_axioms_for_length(
270  array_poolt &array_pool);
271 std::pair<exprt, string_constraintst> add_axioms_for_empty_string(
272  const function_application_exprt &f);
273 
274 std::pair<exprt, string_constraintst> add_axioms_for_copy(
275  symbol_generatort &fresh_symbol,
277  array_poolt &array_pool);
278 
279 std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
280  symbol_generatort &fresh_symbol,
282  array_poolt &array_pool);
283 std::pair<exprt, string_constraintst> add_axioms_for_constant(
284  const array_string_exprt &res,
285  irep_idt sval,
286  const exprt &guard = true_exprt());
287 
288 std::pair<exprt, string_constraintst> add_axioms_for_delete(
289  symbol_generatort &fresh_symbol,
290  const array_string_exprt &res,
291  const array_string_exprt &str,
292  const exprt &start,
293  const exprt &end,
294  array_poolt &array_pool);
295 std::pair<exprt, string_constraintst> add_axioms_for_delete(
296  symbol_generatort &fresh_symbol,
298  array_poolt &array_pool);
299 std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at(
300  symbol_generatort &fresh_symbol,
301  const function_application_exprt &expr,
302  array_poolt &array_pool);
303 std::pair<exprt, string_constraintst> add_axioms_for_format(
304  symbol_generatort &fresh_symbol,
306  array_poolt &array_pool,
307  const messaget &message,
308  const namespacet &ns);
309 std::pair<exprt, string_constraintst> add_axioms_for_format(
310  symbol_generatort &fresh_symbol,
311  const array_string_exprt &res,
312  const std::string &s,
313  const exprt::operandst &args,
314  array_poolt &array_pool,
315  const messaget &message,
316  const namespacet &ns);
317 
318 std::pair<exprt, string_constraintst> add_axioms_for_insert(
319  symbol_generatort &fresh_symbol,
321  array_poolt &pool);
322 std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
323  symbol_generatort &fresh_symbol,
325  array_poolt &array_pool,
326  const namespacet &ns);
327 std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
328  symbol_generatort &fresh_symbol,
330  array_poolt &array_pool);
331 std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
332  symbol_generatort &fresh_symbol,
334  array_poolt &array_pool);
335 std::pair<exprt, string_constraintst> add_axioms_for_insert_float(
336  symbol_generatort &fresh_symbol,
338  array_poolt &array_pool,
339  const namespacet &ns);
340 std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
341  symbol_generatort &fresh_symbol,
343  array_poolt &array_pool,
344  const namespacet &ns);
345 
346 std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
347  symbol_generatort &fresh_symbol,
348  const array_string_exprt &res,
349  const exprt &arg,
350  const exprt &guard);
351 std::pair<exprt, string_constraintst> add_axioms_from_literal(
352  symbol_generatort &fresh_symbol,
354  array_poolt &array_pool);
355 
356 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
357  const array_string_exprt &res,
358  const exprt &input_int,
359  size_t max_size,
360  const namespacet &ns);
361 std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
362  const array_string_exprt &res,
363  const exprt &i);
364 std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
366  array_poolt &array_pool);
367 std::pair<exprt, string_constraintst> add_axioms_from_long(
369  array_poolt &array_pool,
370  const namespacet &ns);
371 std::pair<exprt, string_constraintst> add_axioms_from_bool(
373  array_poolt &array_pool);
374 std::pair<exprt, string_constraintst> add_axioms_from_bool(
375  const array_string_exprt &res,
376  const exprt &i);
377 std::pair<exprt, string_constraintst> add_axioms_from_char(
379  array_poolt &array_pool);
380 std::pair<exprt, string_constraintst> add_axioms_from_char(
381  const array_string_exprt &res,
382  const exprt &i);
383 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
384  symbol_generatort &fresh_symbol,
385  const array_string_exprt &str,
386  const exprt &c,
387  const exprt &from_index);
388 std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
389  symbol_generatort &fresh_symbol,
390  const array_string_exprt &haystack,
391  const array_string_exprt &needle,
392  const exprt &from_index);
393 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
394  symbol_generatort &fresh_symbol,
396  array_poolt &array_pool);
397 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
398  symbol_generatort &fresh_symbol,
399  const array_string_exprt &haystack,
400  const array_string_exprt &needle,
401  const exprt &from_index);
402 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
403  symbol_generatort &fresh_symbol,
404  const array_string_exprt &str,
405  const exprt &c,
406  const exprt &from_index);
407 
408 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
409  symbol_generatort &fresh_symbol,
411  array_poolt &array_pool);
412 
418 std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
419  symbol_generatort &fresh_symbol,
421  array_poolt &array_pool,
422  const namespacet &ns);
423 std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
424  symbol_generatort &fresh_symbol,
425  const array_string_exprt &res,
426  const exprt &f,
427  array_poolt &array_pool,
428  const namespacet &ns);
429 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
430  const array_string_exprt &res,
431  const exprt &i,
432  size_t max_size);
433 std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
434  symbol_generatort &fresh_symbol,
435  const array_string_exprt &res,
436  const exprt &f,
437  array_poolt &array_pool,
438  const namespacet &ns);
439 std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
440  symbol_generatort &fresh_symbol,
442  array_poolt &array_pool,
443  const namespacet &ns);
444 
447 std::pair<exprt, string_constraintst> add_axioms_from_double(
448  symbol_generatort &fresh_symbol,
450  array_poolt &array_pool,
451  const namespacet &ns);
452 
453 std::pair<exprt, string_constraintst> add_axioms_for_replace(
454  symbol_generatort &fresh_symbol,
456  array_poolt &array_pool);
457 std::pair<exprt, string_constraintst> add_axioms_for_set_length(
458  symbol_generatort &fresh_symbol,
460  array_poolt &array_pool);
461 
465 std::pair<exprt, string_constraintst> add_axioms_for_substring(
466  symbol_generatort &fresh_symbol,
467  const array_string_exprt &res,
468  const array_string_exprt &str,
469  const exprt &start,
470  const exprt &end);
471 std::pair<exprt, string_constraintst> add_axioms_for_substring(
472  symbol_generatort &fresh_symbol,
474  array_poolt &array_pool);
475 
476 std::pair<exprt, string_constraintst> add_axioms_for_trim(
477  symbol_generatort &fresh_symbol,
479  array_poolt &array_pool);
480 
481 std::pair<exprt, string_constraintst> add_axioms_for_code_point(
482  const array_string_exprt &res,
483  const exprt &code_point);
484 std::pair<exprt, string_constraintst> add_axioms_for_char_literal(
485  const function_application_exprt &f);
486 
491 DEPRECATED("This is Java specific and should be implemented in Java")
493  symbol_generatort &fresh_symbol,
495  array_poolt &pool);
496 
504  symbol_generatort &fresh_symbol,
505  const function_application_exprt &f);
506 
508  const exprt &input_int,
509  const typet &type,
510  const bool strict_formatting,
511  const array_string_exprt &str,
512  const std::size_t max_string_length,
513  const exprt &radix,
514  const unsigned long radix_ul);
516  const array_string_exprt &str,
517  const exprt &radix_as_char,
518  const unsigned long radix_ul,
519  const std::size_t max_size,
520  const bool strict_formatting);
522  symbol_generatort &fresh_symbol,
524  array_poolt &array_pool,
525  const namespacet &ns);
527  symbol_generatort &fresh_symbol,
529  array_poolt &array_pool);
530 
532  const exprt &chr,
533  const bool strict_formatting,
534  const exprt &radix_as_char,
535  const unsigned long radix_ul);
536 
538  const exprt &chr,
539  const typet &char_type,
540  const typet &type,
541  const bool strict_formatting,
542  unsigned long radix_ul);
543 
544 size_t max_printed_string_length(const typet &type, unsigned long ul_radix);
545 
546 std::string
547 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
548 
549 exprt is_positive(const exprt &x);
550 
552 exprt minimum(const exprt &a, const exprt &b);
553 
555 exprt maximum(const exprt &a, const exprt &b);
556 
558 exprt sum_overflows(const plus_exprt &sum);
559 
561  const array_string_exprt &res,
562  const array_string_exprt &s1);
564  const array_string_exprt &res,
565  const array_string_exprt &s1,
566  const array_string_exprt &s2);
568  const array_string_exprt &res,
569  const array_string_exprt &s1,
570  const array_string_exprt &s2,
571  const exprt &start_index,
572  const exprt &end_index);
574  const array_string_exprt &res,
575  const array_string_exprt &s1,
576  const array_string_exprt &s2);
577 
578 exprt zero_if_negative(const exprt &expr);
579 
581  std::pair<exprt, string_constraintst> result1,
582  std::pair<exprt, string_constraintst> result2);
583 #endif
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
add_axioms_for_copy
std::pair< exprt, string_constraintst > add_axioms_for_copy(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
add axioms to say that the returned string expression is equal to the argument of the function applic...
Definition: string_constraint_generator_main.cpp:490
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
string_constraint_generatort::add_axioms_for_intern
std::pair< symbol_exprt, string_constraintst > add_axioms_for_intern(symbol_generatort &fresh_symbol, const function_application_exprt &f)
Add axioms corresponding to the String.intern java function.
Definition: string_constraint_generator_comparison.cpp:310
sum_overflows
exprt sum_overflows(const plus_exprt &sum)
Definition: string_constraint_generator_main.cpp:54
string_constraint_generatort::associate_length_to_array
exprt associate_length_to_array(const function_application_exprt &f)
Associate an integer length to a char array.
Definition: string_constraint_generator_main.cpp:193
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_index, const exprt &end_index)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
Definition: string_constraint_generator_concat.cpp:81
symbol_generatort::operator()
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
Definition: string_constraint_generator_main.cpp:42
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:63
array_poolt::get_arrays_of_pointers
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
Definition: string_constraint_generator.h:58
array_poolt::length_of_array
std::unordered_map< array_string_exprt, symbol_exprt, irep_hash > length_of_array
Definition: string_constraint_generator.h:80
add_axioms_for_delete
std::pair< exprt, string_constraintst > add_axioms_for_delete(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
Definition: string_constraint_generator_transformation.cpp:374
array_poolt::array_poolt
array_poolt(symbol_generatort &symbol_generator)
Definition: string_constraint_generator.h:52
add_axioms_for_concat_code_point
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.
Definition: string_constraint_generator_concat.cpp:143
add_axioms_for_substring
std::pair< exprt, string_constraintst > add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(st...
Definition: string_constraint_generator_transformation.cpp:124
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:578
add_axioms_for_is_suffix
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.
Definition: string_constraint_generator_testing.cpp:168
typet
The type of an expression, extends irept.
Definition: type.h:27
add_axioms_from_char
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
Definition: string_constraint_generator_valueof.cpp:294
add_axioms_for_string_of_float
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.
Definition: string_constraint_generator_float.cpp:158
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
array_poolt::get_length
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
Definition: string_constraint_generator_main.cpp:72
add_axioms_for_insert_float
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.
Definition: string_constraint_generator_insert.cpp:252
add_axioms_for_insert_int
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
Definition: string_constraint_generator_insert.cpp:144
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:216
add_axioms_for_format
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.
Definition: string_constraint_generator_format.cpp:510
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:133
s1
int8_t s1
Definition: bytecode_info.h:59
add_axioms_from_literal
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.
Definition: string_constraint_generator_constants.cpp:114
add_axioms_from_double
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.
Definition: string_constraint_generator_float.cpp:177
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
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:20
exprt
Base class for all expressions.
Definition: expr.h:54
length_constraint_for_insert
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: string_constraint_generator_insert.cpp:80
add_axioms_for_insert_char
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.
Definition: string_constraint_generator_insert.cpp:196
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, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
Definition: string_constraint_generator_valueof.cpp:153
char_array_of_pointer
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: string_constraint_generator_main.cpp:325
string_constraint_generatort::add_axioms_for_function_application
std::pair< exprt, string_constraintst > add_axioms_for_function_application(symbol_generatort &fresh_symbol, const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
Definition: string_constraint_generator_main.cpp:370
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
string_constraint_generatort::make_array_pointer_association
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
Definition: string_constraint_generator_main.cpp:352
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
bool_typet
The Boolean type.
Definition: std_types.h:28
string_constraint_generatort::string_constraint_generatort
string_constraint_generatort(const namespacet &ns)
Definition: string_constraint_generator_main.cpp:32
add_axioms_for_index_of_string
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...
Definition: string_constraint_generator_indexof.cpp:111
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:135
string_constraint_generatort::hash_code_of_string
std::map< array_string_exprt, exprt > hash_code_of_string
Definition: string_constraint_generator.h:173
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:598
add_axioms_for_insert_bool
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
Definition: string_constraint_generator_insert.cpp:171
string_constraint_generatort
Definition: string_constraint_generator.h:120
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:225
get_string_expr
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
Definition: string_constraint_generator_main.cpp:210
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
add_axioms_for_fractional_part
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.
Definition: string_constraint_generator_float.cpp:255
add_axioms_for_char_at
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.
Definition: string_constraint_generator_main.cpp:566
add_axioms_for_is_empty
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.
Definition: string_constraint_generator_testing.cpp:126
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
add_axioms_for_length
std::pair< exprt, string_constraintst > add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
Length of a string.
Definition: string_constraint_generator_main.cpp:513
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:583
add_axioms_from_float_scientific_notation
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.
Definition: string_constraint_generator_float.cpp:344
add_axioms_from_long
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.
Definition: string_constraint_generator_valueof.cpp:45
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:139
deprecate.h
length_constraint_for_concat_char
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: string_constraint_generator_concat.cpp:109
of_argument
array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
Converts a struct containing a length and pointer to an array.
Definition: string_constraint_generator_main.cpp:333
array_poolt::created_strings_value
std::set< array_string_exprt > created_strings_value
Definition: string_constraint_generator.h:86
add_axioms_for_concat_substr
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 â...
Definition: string_constraint_generator_concat.cpp:38
add_axioms_for_cprover_string
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.
Definition: string_constraint_generator_constants.cpp:82
string_constraint_generatort::constraints
string_constraintst constraints
Definition: string_constraint_generator.h:137
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
add_axioms_for_trim
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.
Definition: string_constraint_generator_transformation.cpp:183
string_constraintst::clear
void clear()
Clear all constraints.
Definition: string_constraint_generator_main.cpp:217
add_axioms_for_equals_ignore_case
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.
Definition: string_constraint_generator_comparison.cpp:132
add_axioms_for_code_point_count
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.
Definition: string_constraint_generator_code_points.cpp:193
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
add_axioms_for_equals
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.
Definition: string_constraint_generator_comparison.cpp:31
add_axioms_for_constrain_characters
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.
Definition: string_constraint_generator_main.cpp:290
add_axioms_for_last_index_of
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 ...
Definition: string_constraint_generator_indexof.cpp:346
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:339
symbol_generatort::symbol_count
unsigned symbol_count
Definition: string_constraint_generator.h:39
utf16_constant_array_to_java
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Definition: string_constraint_generator_format.cpp:483
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
add_axioms_for_insert_double
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
Definition: string_constraint_generator_insert.cpp:223
add_axioms_for_code_point_at
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
Definition: string_constraint_generator_code_points.cpp:122
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:532
add_constraint_on_characters
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.
Definition: string_constraint_generator_main.cpp:254
add_axioms_for_last_index_of_string
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 nee...
Definition: string_constraint_generator_indexof.cpp:205
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
string_constraint.h
array_poolt::find
const array_string_exprt & find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: string_constraint_generator_main.cpp:314
array_poolt::insert
void insert(const exprt &pointer_expr, array_string_exprt &array)
Definition: string_constraint_generator_main.cpp:141
string_constraint_generatort::add_axioms_for_hash_code
std::pair< exprt, string_constraintst > add_axioms_for_hash_code(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Value that is identical for strings with the same content.
Definition: string_constraint_generator_comparison.cpp:190
string_constraint_generatort::associate_array_to_pointer
exprt associate_array_to_pointer(const function_application_exprt &f)
Associate a char array to a char pointer.
Definition: string_constraint_generator_main.cpp:171
refined_string_type.h
add_axioms_for_replace
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.
Definition: string_constraint_generator_transformation.cpp:297
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:415
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:560
string_constraint_generatort::message
const messaget message
Definition: string_constraint_generator.h:169
add_axioms_for_insert
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.
Definition: string_constraint_generator_insert.cpp:33
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:591
is_positive
exprt is_positive(const exprt &x)
Definition: string_constraint_generator_main.cpp:524
array_poolt::fresh_symbol
symbol_generatort & fresh_symbol
Definition: string_constraint_generator.h:83
add_axioms_from_bool
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.
Definition: string_constraint_generator_valueof.cpp:66
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, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
Definition: string_constraint_generator_valueof.cpp:132
add_axioms_for_set_length
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.
Definition: string_constraint_generator_transformation.cpp:37
add_axioms_for_concat
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.
Definition: string_constraint_generator_concat.cpp:126
add_axioms_for_code_point_before
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
Definition: string_constraint_generator_code_points.cpp:155
array_poolt::created_strings
const std::set< array_string_exprt > & created_strings() const
Definition: string_constraint_generator_main.cpp:160
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:112
add_axioms_for_compare_to
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.
Definition: string_constraint_generator_comparison.cpp:241
replace_expr.h
string_constraint_generatort::intern_of_string
std::map< array_string_exprt, symbol_exprt > intern_of_string
Definition: string_constraint_generator.h:176
array_poolt::make_char_array_for_char_pointer
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
Definition: string_constraint_generator_main.cpp:99
length_constraint_for_concat
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: string_constraint_generator_concat.cpp:99
s2
int16_t s2
Definition: bytecode_info.h:60
add_axioms_for_offset_by_code_point
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.
Definition: string_constraint_generator_code_points.cpp:222
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
string_expr.h
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
add_axioms_for_parse_int
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.
Definition: string_constraint_generator_valueof.cpp:507
add_axioms_for_is_prefix
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(symbol_generatort &fresh_symbol, const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
Definition: string_constraint_generator_testing.cpp:37
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:630
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:704
array_poolt::arrays_of_pointers
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
Definition: string_constraint_generator.h:76
add_axioms_for_delete_char_at
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
Definition: string_constraint_generator_transformation.cpp:339
array_poolt::fresh_string
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
Definition: string_constraint_generator_main.cpp:87
add_axioms_for_contains
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.
Definition: string_constraint_generator_testing.cpp:233
add_axioms_for_correct_number_format
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.
Definition: string_constraint_generator_valueof.cpp:329
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:111
add_axioms_for_index_of
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...
Definition: string_constraint_generator_indexof.cpp:38